# How the Coloured Sand was built

This note tells how «The Coloured Sand Theorem» was made, and says what belongs to whom. The work is a collaboration between the author, Rafael Amichis Luengo, and instances of the AI system Claude (Anthropic) working in separate roles; the Lean proofs were written by Aristotle (Harmonic). Each part completes the other. Nobody's merit is taken from anybody, and nobody is compared with anybody.

## The roles

- **The author** does not write proofs. He chooses the problems, directs the work, and unblocks it when it is stuck, with ideas given in plain words: images. Each image is translated piece by piece into something that can be counted, and the translation is sealed before anything is measured.
- **Constructors** (instances of Claude) propose and write proofs, from written missions.
- **An auditor** (an instance of Claude) re-derives every step, runs checks with its own code, and writes the records.
- **Cold readers** (instances of Claude, with no access to the audits) read the proofs and the Lean certificate as a referee would.
- **Aristotle** (Harmonic) writes the Lean proofs, piece by piece, from statements taken from the paper; each piece is compiled again on the author's machine and audited.

## The key was in the Dancing Sand

The route to Theorems I and J began with the author. When Conjecture I was open, he insisted that the Dancing Sand had to hold the key to closing this problem entirely, because he knew what its images had solved. The auditor checked, and he was right: the key was the dance of the Dancing Sand Theorem, §3–§4, whose open question 5 is exactly the problem of this paper. From there, a constructor carried the dance to every odd prime, a cold reader checked the proof, and Lean checked it by machine.

The dance itself, in the Dancing Sand, was an auditor's proposal, taken up by the author (row 1 of record/THE_IMAGES.md of the Dancing Sand repository). The author's part here has two pieces: knowing where the key was, and the images whose mechanisms the proof reuses.

## The images

As in the Dancing Sand, the author's part was to unblock the work. Of the 27 images he gave for the Dancing Sand, 19 became the statement or the mechanism of a result and 6 served in part (record/THE_IMAGES.md). The proofs of Theorems I and J reuse that machinery for odd primes:

- the unique cheapest matching of the natural minor is his «orphan» («one parent is gone and the one who is left takes care of everything; nobody has to be killed, it died by itself»);
- the floor of the Smith form is the flat that settles its account with its mirror («what you don't pay the landlord you give to me; that is why it has to be negotiated together»);
- the base-p carries are his climb «in the air» («colder, lower pressure, not only the altitude»).

## The checks

- The proofs of Theorems A–H were re-derived by an independent reader with no access to the audits.
- The proofs of Theorems I and J were written by one reader, re-derived by a second and read cold by a third, who wrote the floor of the Smith form for odd p out in full.
- The Lean certificate and version 5 were read cold by a fourth reader; the changes of version 6 by a fifth.
- Every theorem, A–J, is proved in Lean 4 with Mathlib for every prime, with no sorry and only the standard axioms, and the whole Lean project was rebuilt on GitHub's machines.
- No human expert has refereed this work.

The full record (code, sealed predictions, logs, cold readings, the Lean project and its certificate) is at https://github.com/tretoef-estrella/coloured-sand-theorem and in the Zenodo record https://doi.org/10.5281/zenodo.23327608.