Ice-mixing notes
This site publishes the results of ice-mixing, a research project on spin ice on the pyrochlore lattice: how fast the standard local dynamics (single hexagon flips) relaxes, which ice states are frozen (admit no hexagon flip at all), and whether every frozen state of zero flux is periodic. The results are issued as stand-alone contribution notes, each with a PDF. For every note that has a claims manifest, its principal results are listed below one by one: what is asserted, on which cells (the periodic boxes of the lattice on which it holds), with what standing (proved, certified by a machine-checked proof, computed, conjectured, open), what it rests on, how to regenerate its evidence, and who wrote it and who checked it. Most of the work was done by language-model agents (Anthropic's Claude models) directed by Lyndon Drake; every claim names the model that wrote it and the independent checker that read it, and says whether a person has read it line by line.
34 claims in 1 manifest; 10 notes in all (9 without a published manifest yet). Claims read line by line by a person: 0 of 34.
Dependency graph · Notes · Checker and agent reports · Certificate ledgers · llms.txt · llms-full.txt · manifest schema · repository
Open problems
Claims whose status is open or conjecture: the targets the notes name.
- Theorem H open theorem-h-orientation/thm-h
In a frozen state with a hexagon of odd curl, some axis is empty (no vertex has that type) or one-way (every vertex of that type has the same sign of moment).
- Theorem U open theorem-h-orientation/thm-u
In an odd frozen state every octahedral hole is oriented: one of its rods points towards it and the other away. Equivalent forms: an odd state has no charged hole; two consecutive vertices of type \(k\) on a \(k\)-line have the same sign; a state with an unoriented cage has even curl; and the working form (V), that in a state with the four vertices of Theorem U′ the sublattice of the bridgeheads has no vertex of the rods’ type.
Claims
| claim | what it says | kind | status | scope | note |
|---|---|---|---|---|---|
| model | Definitions: cells, ice states, vertex types, hexagons and their curl, frozen and odd states, holes and their rods. The model (first section; Holes, cages and rods) | definition | proved | every cell | theorem-h-orientation |
| thm-h | A frozen state with an odd hexagon has an axis that is either unused or used with one sign only. Theorem H | theorem | open | every cell; open on the cells with no coprime pair and more than two chains in every pair of planes that are not covered by a certificate, the cubic cells of side nine and more among them | theorem-h-orientation |
| thm-u | In an odd frozen state every octahedral hole is oriented, one rod pointing in and one out; the one open step to Theorem H. Theorem U | conjecture | open | open on cells with no coprime pair of extents and more than two chains in every pair of planes, beyond those certified | theorem-h-orientation |
| thm-1 | The reduction: on every cell, Theorem U implies Theorem H. Theorem 1 (the reduction), form of 30 September 2026, with Lemmas 22 to 25 | theorem | proved | every cell | theorem-h-orientation |
| thm-1-first-form | An earlier, superseded form of the reduction that also needed \(K_u\). Theorem 1, first form (27 September 2026), through K_u | theorem | proved | every cell on which K_u holds for all three axes | theorem-h-orientation |
| thm-2 | Theorem H by machine-checked certificate on the cubic cells of side 4 to 8, four cells that are not cubic, and their divisors. Theorem 2 | theorem | certified | cubic side 4 to 8; (3,3,9), (4,4,8), (3,3,12), (6,6,9); their divisors | theorem-h-orientation |
| thm-24 | Theorem H on the small cubic cells of side 1 to 3, deduced from side 6. Theorem 24 | theorem | certified | cubic side 1, 2, 3 | theorem-h-orientation |
| lemma-21 | Repeating a state onto a larger cell keeps it frozen and odd, so Theorem H passes from a cell to its divisors. Lemma 21 (a state repeated periodically) | lemma | proved | every cell | theorem-h-orientation |
| thm-14 | Theorem H proved by hand on every cell with a pair of coprime extents. Theorem 14 (cells with a coprime pair of extents), with Lemmas 8 to 10 and Theorems 12, 13, 15 | theorem | proved | every cell with gcd of some pair of extents equal to 1 | theorem-h-orientation |
| thm-22 | Theorem U proved by hand on the cells \((2a', 2b', 2c')\) with \(a', b', c'\) pairwise coprime. Theorem 22, with Theorems 20 and 21 (cells with two chains in every pair of planes) | theorem | proved | (2a’, 2b’, 2c’) with a’, b’, c’ pairwise coprime | theorem-h-orientation |
| thm-23 | Theorem H proved by hand on the same cells, through the signed moments. Theorem 23, with Lemmas 13 to 20 and Theorems 16 to 19 (the signed moments) | theorem | proved | (2a’, 2b’, 2c’) with a’, b’, c’ pairwise coprime | theorem-h-orientation |
| thm-10 | Holes along one axis are oriented when the other two extents are coprime. Theorem 10 (the coprime case of (V)) | theorem | proved | every cell with gcd(b, c) = 1, for holes with rods along x | theorem-h-orientation |
| thm-11 | Holes along one axis are oriented when the other two extents have greatest common divisor 2 and the axis has odd length. Theorem 11 (greatest common divisor two, odd length) | theorem | proved | gcd(b, c) = 2 and a odd, for holes with rods along x | theorem-h-orientation |
| u-prime-certificates-2026-09-27 | DRAT proofs that an unoriented hole forces even curl, on the cubic cells of side 4, 5 and 6. Theorem U′ certified at the cubic sides four, five and six | certificate-campaign | certified | cubic side 4, 5, 6 | theorem-h-orientation |
| u-prime-certificates-2026-10-01 | The same proofs at cubic sides 7 and 8 and on four cells that are not cubic; run as a search for a counterexample, which found none. Theorem U′ certified at sides seven and eight and on four cells that are not cubic; the counterexample search | certificate-campaign | certified | cubic side 7, 8; (3,3,9), (4,4,8), (3,3,12), (6,6,9) | theorem-h-orientation |
| thm-9-diagonal-law | An explicit linear certificate proving the diagonal law at every odd separation. Theorem 9 (the certificate of the diagonal law, closed form) | theorem | proved | every cell (an identity on the infinite lattice) | theorem-h-orientation |
| thm-3-diagonal-law | Two vertices of the same type on diagonally neighbouring lines have equal signs when the holes between them are oriented. Theorem 3 (the diagonal law) | theorem | proved | every cell | theorem-h-orientation |
| thm-6-separability | How the count of a type along a line depends on position: separable counts, walls, and uniform chains beside a wall. Theorems 4 to 8 (line counts, two separable functions with product zero, walls, uniform chains beside a wall) | theorem | proved | every cell | theorem-h-orientation |
| thm-15 | On each sublattice at most two of the three type profiles can vary. Theorem 15 | theorem | proved | every cell | theorem-h-orientation |
| cage-laws | The local linear laws the frozen condition imposes on the types round each hole, with the 1,200 possible patterns of one cage. Law C, law \(P^k\), Lemmas 1 to 3 (the cage laws) | lemma | proved | every cell | theorem-h-orientation |
| parametrisation-c | Every real solution of the type equations is a weighted sum of chain modes plus two constants. The parametrisation (C) (completeness of the chain modes) | theorem | proved | every cell | theorem-h-orientation |
| thm-m-prime | If one sublattice lacks a type that the other has, the state has even curl. Theorem M′ (from the project’s earlier record) | theorem | proved | every cell | theorem-h-orientation |
| ku | A chain with a single moment forces some direction to be absent; no longer used by any proof. \(K_u\) (a uniform chain forces a direction to be absent) | fact | certified | as stated | theorem-h-orientation |
| ku-first-step-hand | Given orientation, the first step of \(K_u\) follows by hand from the diagonal law on every cell. The first step of \(K_u\) given orientation, by two applications of the diagonal law | fact | proved | every cell | theorem-h-orientation |
| v-reach-law | How far round a hole the frozen condition must be used to force (V): the reach grows with \(g\), and the whole transverse torus is needed. The reach of (V) (Theorem U section, item 1) | fact | solver | twenty cells tested; the law is conjectured for every cell | theorem-h-orientation |
| closed-linear-relaxation | Closed route: no linear combination of the local laws proves (V) once \(g \geq 2\); integrality is essential. No weighted sum of laws proves (V) at \(g \geq 2\) (Theorem U section, items 3 to 5) | negative-result | closed-route | cubic sides 3 to 5 and the cells named in the note | theorem-h-orientation |
| closed-tilted-sheet | Closed route: just short of the reach of (V), the solutions that violate it carry no usable invariant. The closure of the tilted sheet carries no invariant (Theorem U section, item 7) | negative-result | closed-route | the cells with g from 3 to 7 named in the reports | theorem-h-orientation |
| statement-r-box-lemma | A weaker relative of (V): two aligned rods extend to a whole line of their type; its first step certified for \(b\) from 3 to 6. Statement R and its box lemma (Conjecture \(R_b\); Theorem U section, item 8) | conjecture | certified | certified for b = 3 to 6 on every cell meeting the box’s bounds; conjectured for all b | theorem-h-orientation |
| closed-r-then-monodromy | Closed route: Statement R, periodicities of the chain weights and height functions do not lead to (V); any proof must be integral from the start. Statement R, a monodromy in the weights, and the heights are not a route to (V) (Theorem U section, item 9) | negative-result | closed-route | the cells named in the reports; the lemmas on the grid for every cell with b | a and c | a | theorem-h-orientation |
| kink-counts-per-class | The counts of the rods’ type per chain class obey a discrete wave equation, and every chain of an axis has the same defect. The kink counts per chain class: the wave equation and one defect per axis (Theorem U section, item 10) | lemma | proved-unchecked | every cell | theorem-h-orientation |
| closed-kink-counts | Closed route: counts per class cannot prove (V); what matters is which positions are kinked, not how many. The kink counts per class cannot close (V) (Theorem U section, item 10) | negative-result | closed-route | (12,4,4), (10,5,5), (12,6,6), (12,4,8) | theorem-h-orientation |
| weights-integrality-correction | Correction: the chain weights of (C) are integral on only a few states, so earlier results on heights cover only those. The weights of (C) are rarely integral (correction of 30 September 2026) | fact | corrected | cubic sides 3 and 4; samples of (6,3,3), (12,4,4), (5,5,5) | theorem-h-orientation |
| periodicity | Where Theorem H holds and every extent is at least 2, every frozen zero-flux state has a translation symmetry. Periodicity of frozen zero-flux states (first section, with Theorem P and Lemma A of the earlier note) | corollary | proved | every cell with all extents at least two on which Theorem H holds | theorem-h-orientation |
| thin-cells-aperiodic | Counterexamples: on six thin cells (an extent of 1) some frozen zero-flux states have no translation symmetry. Frozen zero-flux states with no translation symmetry on thin cells | fact | refuted | the six thin cells named; (1,1,1) excluded | theorem-h-orientation |
The status vocabulary
Every claim has exactly one of these. They are the project's own, defined in the manifest schema and discussed in the note on the method.
- proved
- a written argument read by an independent checker with its own programs.
- proved-unchecked
- a written argument with no second reader.
- certified
- a machine-checked proof object (DRAT, LRAT, a CPOG-certified count, Lean, Isabelle) on the cells named in scope.
- solver
- a SAT or LP verdict on named cells without a checked proof object.
- computed
- an exact computation with no solver verdict.
- explored
- floating-point or sampled evidence only.
- conjecture
- believed, with evidence named.
- open
- a target with no verdict.
- closed-route
- a method shown not to reach the target.
- corrected
- a statement of an earlier version repaired here.
- refuted
- shown false, with a witness.