tilting-modules

The p-part of the sandpile group of the Hamming graph K_q^d at the primes p dividing q, called hard by Jacobson-Niedermaier-Reiner (2003), determined for every prime p dividing q and every d via explicit Z_p-lattices for the tilting modules of SL_2. Every theorem checked in Lean 4. Paper, Lean proof, code, sealed predictions, logs, cold readings.

The whole 2-part of the sandpile group (critical group) of the hypercube Q_n, for every n, open since Bai (2003): an explicit rule through tilting modules of SL_2 in characteristic 2, the fold law for the folded cube, and proofs of conjectures of Gao, Marx-Kuo, McDonald and Yuen. Paper, checks and the full record of verification.