HEXAGONbeta

The Dancing Sand Theorem: the 2-part of the sandpile group of the hypercube, for every n

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.GR — Group Theorymath.RT — Representation Theory

Contributed by Rafael Amichis Luengo

Version 2 / Oct 12, 2026 / CC BY 4.0

Abstract

Let K(Qn)K (Q_{n}) be the sandpile group (critical group, Jacobian) of the nn-dimensional hypercube graph QnQ_{n}. Its odd part was determined by Bai in 2003; its 22-part has been open since then. Gao, Marx-Kuo, McDonald and Yuen determined its n−1n - 1 largest cyclic factors, and Betzer the nn-th, through a remark of theirs stated without proof. We determine the whole 2-part of K(Qn)K (Q_{n}) for every nn, by an explicit rule. The group splits over the indecomposable tilting modules T(λ)T (\lambda) of SL2\mathrm{SL}_{2} in characteristic 22 that occur in V⊗nV^{\otimes n}, with their multiplicities. The contribution of T(λ)T (\lambda) at the shift i=(n−λ)/2i = (n - \lambda) / 2 consists of explicit small cyclic factors and of 2∣I∣2^{| I |} large ones, where II is the set of binary digits of λ+1\lambda + 1 below the leading one. The large ones are obtained by pooling a sequence of explicit integers — binomial valuations and carries — into a non-increasing sequence, in the manner of isotonic regression. The proof reduces each contribution, by elimination inside explicit 22-adic lattices, to the Smith form of an explicit 2∣I∣×2∣I∣2^{| I |} \times 2^{| I |} integer matrix, and computes that Smith form from the valuations of its entries. It needs a unique cheapest matching for an upper bound and an inductive potential for a lower bound. As consequences we recover Bai's counts and the theorems of Gao, Marx-Kuo, McDonald and Yuen on the largest factors, we prove their Conjecture 4.14 without that remark, and we prove their Conjecture 5.4 and the formula for the (n+1)(n + 1)-th factor stated in the 2019 poster of three of them. We also prove the fold law: the 2-part of the sandpile group of the folded cube Qn/⟨(1,…,1)⟩Q_{n} / \langle (1, \dots, 1) \rangle is 2⋅Syl⁡2K(Qn)2 \cdot \operatorname{Syl}_{2} K (Q_{n}), the group obtained by lowering every exponent by one. With the results above this gives the whole 22-part of the sandpile group of the folded cube, and, with the known odd part, its whole sandpile group. The whole proof has been checked in the proof assistant Lean 4 with the Mathlib library, with nothing cited. This work has not been refereed by a human expert.

Provenance statement

The author, Rafael Amichis Luengo, does not write mathematics. He chose the problem, directed the work, and gave the ideas that unblocked it: 27 images in plain words (for example «the dance», «dry and wet», «they take turns», «the cave»), each translated into a precise statement before anything was measured; 19 served in full and 6 in part. The attached file THE_IMAGES.md lists them, with what each became. The proofs and the text were written by instances of Claude (Anthropic), working in separate roles from written missions: constructors that proposed and wrote proofs; an auditor that re-derived every step and ran checks with its own code; and cold readers with no access to the audits, who re-derived the chains of proof and then read the whole text (thirteen cold readings in all). Computations were used as checks, never as steps of a proof. The whole proof was then formalized in Lean 4 with Mathlib (420 files, 61 285 lines, 3 470 declarations, no sorry, standard axioms only). The Lean proofs were written by Aristotle (Harmonic) from pieces written from the paper, compiled on the author's machine and audited; the Lean certificate was itself read cold. No human expert has refereed this work. Lean certificate: https://doi.org/10.5281/zenodo.23298436. Paper, version 10: https://doi.org/10.5281/zenodo.23298437. Repository with the full record (missions, reports, audits, cold readings, engines and logs): https://github.com/tretoef-estrella/dancing-sand-theorem. This TeX source was generated from the version-10 text by a script (md2tex.py) and checked against it word by word.
AI provenance filesTHE_IMAGES.md · 16 KB

Tools used

Anthropic
Claude Code
Harmonic
Aristotle
Lean
LeanVersion v4.28.0
Lean
Mathlib
Python Software Foundation
PythonVersion 3

References

  1. M. Ayer, H. D. Brunk, G. M. Ewing, W. T. Reid, E. Silverman, An empirical distribution function for sampling with incomplete information, Ann. Math. Statist. 26 (1955), 641--647.
  2. T. Akyar, A. Beliakov, K. Delchev, N. Kalinin, E. Lupercio, H. Serrano, M. Shkolnikov, D. Tabares, N. Terekhov, The 2-adic valuation of the order of the all-ones class in the sandpile group of a square, arXiv:2609.10625 (2026).arXiv
  3. H. Bai, On the critical group of the nn-cube, Linear Algebra Appl. 369 (2003), 251--261.
  4. R. E. Barlow, D. J. Bartholomew, J. M. Bremner, H. D. Brunk, Statistical Inference under Order Restrictions , Wiley, 1972.
  5. D. N. Betzer, Sandpile groups of Cayley graphs over F2r\mathbb{F}_{2}^{r}: Sylow-2 structure, isospectral counterexamples, and Boolean incidence algebra, preprint, Zenodo (August 2026), DOI 10.5281/zenodo.22065778.DOI
  6. T. Bier, Remarks on recent formulas of Wilson and Frankl, European J. Combin. 14 (1993), 1--8.
  7. N. L. Biggs, Chip-firing and the critical group of a graph, J. Algebraic Combin. 9 (1999), 25--45.
  8. T. Clausen, Lehrsatz aus einer Abhandlung über die Bernoullischen Zahlen, Astron. Nachr. 17 (1840), 351--352.
  9. D. B. Chandler, P. Sin, Q. Xiang, The Smith group of the hypercube graph, Des. Codes Cryptogr. 84 (2017), 283--294; arXiv:1511.00272.arXiv
  10. J. E. Ducey, L. Engelthaler, J. Gathje, B. Jones, I. Pfaff, J. Plute, Integer diagonal forms for subset intersection relations, arXiv:2310.09227 (2023).arXiv
Show all 37 referencesShow fewer references
  1. J. E. Ducey, I. Hill, P. Sin, The critical group of the Kneser graph on 2-subsets of an nn-element set, Linear Algebra Appl. 546 (2018), 154--168; arXiv:1707.09115.arXiv
  2. J. E. Ducey, D. M. Jalil, Integer invariants of abelian Cayley graphs, Linear Algebra Appl. 445 (2014), 316--325; arXiv:1308.2335.arXiv
  3. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction --- CADE 28 , Lecture Notes in Computer Science 12699, Springer, 2021, 625--635.
  4. S. Donkin, On tilting modules for algebraic groups and finite dimensional algebras, Math. Z. 212 (1993), 39--60.
  5. A. El-Amawy, S. Latifi, Properties and performance of folded hypercubes, IEEE Trans. Parallel Distrib. Syst. 2 (1991), 31--42.
  6. J. Gao, J. Marx-Kuo, V. McDonald, C. H. Yuen, Sandpile groups of Cayley graphs of F2r\mathbb{F}_{2}^{r}, Comm. Algebra 52 (2024), 4459--4479; arXiv:1912.06919v3 (cited by its numbering).arXiv
  7. Harmonic, Aristotle, an AI system for mathematics, https://aristotle.harmonic.fun (2026).link
  8. J. E. Humphreys, Introduction to Lie Algebras and Representation Theory , Graduate Texts in Mathematics 9, Springer, 1972.
  9. K. Iga, C. Klivans, J. Kostiuk, C. H. Yuen, Eigenvalues and critical groups of Adinkras, Adv. in Appl. Math. 143 (2023), Paper No. 102450; arXiv:2202.02821.arXiv
  10. J. C. Jantzen, Representations of Algebraic Groups , 2nd ed., Mathematical Surveys and Monographs 107, AMS, 2003.
  11. C. J. Klivans, The Mathematics of Chip-Firing , CRC Press, 2018.
  12. B. Kostant, Groups over Z\mathbb{Z}, in Algebraic Groups and Discontinuous Subgroups , Proc. Sympos. Pure Math. 9, AMS, 1966, 90--98.
  13. E. E. Kummer, Über die Ergänzungssätze zu den allgemeinen Reciprocitätsgesetzen, J. Reine Angew. Math. 44 (1852), 93--146.
  14. M. Larsen, Bounds for SL2\mathrm{SL}_{2}-indecomposables in tensor powers of the natural representation in characteristic 2, arXiv:2405.16015 (2024).arXiv
  15. R. Amichis Luengo, The Dancing Sand Theorem --- Lean certificate , version 2, Zenodo (2026), DOI 10.5281/zenodo.23298436; all versions, concept DOI 10.5281/zenodo.23296707.DOI
  16. D. J. Lorenzini, A finite group attached to the Laplacian of a graph, Discrete Math. 91 (1991), 277--282.
  17. Y. Len, D. Zakharov, Kirchhoff's theorem for Prym varieties, with an appendix by S. Casalaina-Martin, Forum Math. Sigma 10 (2022), Paper No. e11; arXiv:2012.15235.arXiv
  18. The mathlib Community, The Lean mathematical library, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , ACM, 2020, 367--381.
  19. J. Marx-Kuo, J. Gao, V. McDonald, The sandpile group of Cayley graphs, poster, Joint Mathematics Meetings, Baltimore, January 2019.
  20. The On-Line Encyclopedia of Integer Sequences, sequence A193134, accessed 5 October 2026.
  21. V. Reiner, D. Tseng, Critical groups of covering, voltage and signed graphs, Discrete Math. 318 (2014), 10--40; arXiv:1301.2977.arXiv
  22. R. Strassmann, Über den Wertevorrat von Potenzreihen im Gebiet der pp-adischen Zahlen, J. Reine Angew. Math. 159 (1928), 13--28.
  23. D. Tubbenhauer, P. Wedrich, Quivers for SL2\mathrm{SL}_{2} tilting modules, Represent. Theory 25 (2021), 440--480.
  24. K. G. C. von Staudt, Beweis eines Lehrsatzes, die Bernoullischen Zahlen betreffend, J. Reine Angew. Math. 21 (1840), 372--374.
  25. M. Vetluzhskikh, D. Zakharov, Critical groups in harmonic abelian quotients, arXiv:2409.04629 (2024).arXiv
  26. R. M. Wilson, A diagonal form for the incidence matrices of tt-subsets vs. kk-subsets, European J. Combin. 11 (1990), 609--615.
  27. C. H. Yuen, The critical groups of Adinkras up to 2-rank of Cayley graphs, Electron. J. Combin. 31 (2024), Paper No. P1.38; arXiv:2301.02517.arXiv

Version history

  1. v1Submitted by Rafael Amichis LuengoInitial depositSupersededOct 12, 2026
  2. v2Submitted by Rafael Amichis LuengoSubmitted as a new versionCurrentOct 14, 2026