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

Rafael Amichis Luengo

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

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatorics math.GR — Group Theory math.RT — Representation Theory

Contributed by Rafael Amichis Luengo ↗

Version 1 / Oct 12, 2026 / CC BY 4.0

Abstract

Let

K (Q_{n})

be the sandpile group (critical group, Jacobian) of the

n

-dimensional hypercube graph

Q_{n}

. Its odd part was determined by Bai in 2003; its

2

-part has been open since then, and the latest work on it determines its

n - 1

largest cyclic factors. We determine the whole 2-part of

K (Q_{n})

for every

n

, by an explicit rule. The group splits over the indecomposable tilting modules

T (\lambda)

of

\mathrm{SL}_{2}

in characteristic

2

that occur in

V^{\otimes n}

, with their multiplicities. The contribution of

T (\lambda)

at the shift

i = (n - \lambda) / 2

consists of explicit small cyclic factors and of

2^{| I |}

large ones, where

I

is the set of binary digits of

\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

2

-adic lattices, to the Smith form of an explicit

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, and we prove their Conjectures 4.14 and 5.4 and the formula for the

(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

Q_{n} / \langle (1, \dots, 1) \rangle

is

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

2

-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

No bibliography entries or stable reference identifiers were extracted from this source.

Version history

v1Submitted by Rafael Amichis LuengoInitial depositCurrentOct 12, 2026