The model and its conventions

Pyrochlore spin ice states are the two-in–two-out configurations of Ising spins on the pyrochlore lattice (Bramwell and Gingras 2001), equivalently the Eulerian orientations of the diamond lattice whose bonds carry the spins and whose sites are the tetrahedron centres. Everything below uses that second picture and the conventions of icemix/lattice.py.

Positions are integers in units of \(a/4\), a quarter of the conventional cubic edge. The A sublattice is generated by the face-centred cosets \((0,0,0)\), \((0,2,2)\), \((2,0,2)\) and \((2,2,0)\), and the B sublattice is that set translated by \((1,1,1)\). The four displacements from an A site to its B neighbours are \(d_0 = (1,1,1)\), \(d_1 = (1,-1,-1)\), \(d_2 = (-1,1,-1)\) and \(d_3 = (-1,-1,1)\), which sum to zero. An \((a,b,c)\) block of conventional cubic cells with periodic boundaries has box \((4a,4b,4c)\) and holds \(8abc\) sites and \(16abc\) bonds. A state assigns one bit to each bond, and the bit is \(1\) exactly when the arrow runs from the A end to the B end. The ice rule is that exactly two of the four arrows at each site point in, which in this encoding reduces at both sublattices to ‘exactly two of the four incident bits are set’. An ice state’s arrow field is divergence-free, so the net flux through each coordinate cut plane is conserved by any ice-preserving move; that triple is the winding \(\mathbf{W} = (W_x, W_y, W_z)\), and \(\mathbf{W} = 0\) is the largest sector and the one at issue here.

Hexagons are derived rather than hardcoded, as the closed non-backtracking six-walks whose unwrapped vector displacement is exactly zero. The displacement condition is not pedantry: on a small periodic cell the quotient graph carries six-cycles that wind round the torus instead of bounding a face, and flipping one changes the winding. At \((1,1,1)\) the quotient graph is \(K_{4,4}\), which has 96 six-cycles where the lattice has 16 hexagons. Each hexagon visits three A sites and three B sites, so its six bonds fall into a class of three traversed from A to B and a class of three traversed from B to A, alternating in cycle order. There are \(16abc\) hexagons, six through every bond and twelve through every A site.

A hexagon is flippable when its arrows run head to tail, which says that one traversal class carries all ones and the other all zeros. The chain picks a hexagon uniformly at random and reverses it with probability \(1/2\) if it is flippable. Every flip preserves the ice rule and the winding, and the chain is reversible with the uniform stationary distribution on each flux sector; its generator is, up to normalisation, the ring-exchange Hamiltonian of pyrochlore spin ice at its Rokhsar–Kivelson point (Rokhsar and Kivelson 1988; Henley 2004; Hermele, Fisher, and Balents 2004). A state with no flippable hexagon is frozen: absorbing and unreachable at once, a singleton component of the flip graph, and an exact zero-energy eigenstate of that Hamiltonian, degenerate with the equal-weight superposition over its sector. Whether frozen states exist at every size is therefore a question about the ground-space degeneracy.

The smallest cell is frozen

The single conventional cubic cell \((1,1,1)\) has sixteen bonds, eight sites and sixteen hexagons. Write a state as a \(4\times4\) zero-one matrix \(M[g][k]\) whose rows are the four A-site cosets and whose columns are the four directions, and label the B end of the bond \((g,k)\) by \(g \oplus k\); the labelling is exact because the differences of the four directions realise the Klein four-group on the cosets. The ice rule at the A sites is then ‘row sums are 2’, the ice rule at the B sites is ‘B-label sums are 2’, and \(\mathbf{W} = 0\) is ‘column sums are 2’. The first two conditions alone admit the classical 90 matrices with row and column sums two, the \(K_{4,4}\) count; all three admit exactly 12.

Theorem 1. Every \(\mathbf{W} = 0\) ice state of the \((1,1,1)\) cell is frozen.

Proof. A hexagon runs through the A sites \(g\), \(A_2 = g \oplus i \oplus j\) and \(A_3 = g \oplus j \oplus k\) for a triple \((i,j,k)\) of distinct directions, and carries two bonds of each of those directions, one in each traversal class. Head-to-tail circulation forces the two bonds of each direction to carry opposite bits. Let \(l\) be the fourth direction and \(A_4 = g \oplus i \oplus k\) the fourth A site, and take the three matrix cells \((A_3,k)\), \((A_3,l)\) and \((A_4,k)\), none of which lies on the hexagon. They pairwise share a line: the first two share the row \(A_3\), the first and third share the column \(k\), and the last two share the B-label \(g \oplus i\), because \(A_4 \oplus k = A_3 \oplus l = g \oplus i\). Each of those lines already carries two hexagon cells, one from each traversal class and so of opposite bit, namely \((A_3,j)\) and \((A_3,i)\) in the row, \((A_2,k)\) and \((g,k)\) in the column, and \((g,i)\) and \((A_2,j)\) in the B-label. Each line sums to two, by the A-site ice rule, zero flux and the B-site ice rule respectively, so its two remaining cells sum to one. The three off-hexagon cells would then pairwise sum to one, which three zero-one numbers cannot do. \(\square\)

Periodic tiling lifts this to arbitrary size. Identify bonds of a large cell by their A-site position reduced modulo the small box together with their direction, and repeat a state of the small cell across the large one. The ice rule is local and so is inherited; each winding component is multiplied by the tiling factor in the two transverse directions, so a zero-flux state tiles to a zero-flux state; and a hexagon of the large cell is a translate of a hexagon of the small one, so frozenness is inherited too. That was checked from scratch in each target cell’s own derived hexagon set for ten source-target pairs, with targets \((2,2,2)\), \((2,2,4)\), \((1,2,4)\) and the 432-spin \((3,3,3)\), all ten frozen with the ice rule and zero winding intact. The \(\mathbf{W} = 0\) sector of every cell therefore contains frozen states.

Translation-frozen states, and how many there are

The second construction is independent of the first and carries an exact count. For the \(z\) axis the relevant translations are the two half-diagonals perpendicular to it, \((2,2,0)\) and \((2,-2,0)\) in \(a/4\) units; the \(x\) and \(y\) axes take \((0,2,2)\), \((0,2,-2)\) and \((2,0,2)\), \((2,0,-2)\).

Theorem 2. In any cell, an ice state invariant under the two half-diagonal translations perpendicular to an axis is frozen, in every flux sector. Its \(\mathbf{W} = 0\) members number exactly \(\binom{2c}{c}^{2}\), where \(c\) is the cell’s extent along that axis, and the three axis families are disjoint.

Proof. On a hexagon with directions \((i,j,k)\) and A sites \(A_1, A_2, A_3\), the two bonds of direction \(i\) sit at \(A_1\) and \(A_3 = A_1 + (d_k - d_j)\), those of direction \(j\) at \(A_3\) and \(A_2 = A_3 + (d_i - d_k)\), and those of direction \(k\) at \(A_2\) and \(A_1 = A_2 + (d_j - d_i)\), so each direction’s pair is separated by the difference of the other two. The four directions split by the sign of their \(z\) component into \(\{d_0, d_3\}\) and \(\{d_1, d_2\}\), so any three of them contain a pair from one class, and for such a pair the difference has zero \(z\) component and equals \(\pm(d_0 - d_3) = \pm(2,2,0)\) or \(\pm(d_1 - d_2) = \pm(2,-2,0)\). One of the three directions therefore has its two bonds identified by a translation the state is invariant under, so they carry equal bits, where flippability requires them opposite. No hexagon is flippable, and neither the ice rule nor any flux condition entered the argument.

For the count, quotient by the two translations. The A sites collapse to the \(2c\) distinct coordinates along the axis and the quotient is a ring of \(4c\) sites joined by double bonds. Write \(a(z)\) for the number of A-to-B arrows among the two directions with positive axis component in layer \(z\), and \(b(z)\) for the same among the two with negative component. The A-site rule gives \(a(z) + b(z) = 2\) and the B-site rule gives \(a(z) + b(z{+}2) = 2\), which together force only that \(b\) is 2-periodic; the fully polarised state satisfies both and has \(a \equiv 2\). It is zero flux along the axis, not the ice rule, that forces one arrow up and one down on every double bond. Given that balance, the state is fixed by one sign per layer for the upward pair and one for the downward pair, and the two transverse fluxes vanish exactly when each of those two sequences of length \(2c\) is balanced. There are \(\binom{2c}{c}\) balanced sequences of each kind. A state in two of the three axis families is invariant under the whole face-centred lattice, hence a \(q = 0\) state, which has \(\mathbf{W} \neq 0\), so the families are disjoint at zero flux. \(\square\)

The corollary is a lower bound: an \(L \times L \times L\) cell holds at least \(3\binom{2L}{L}^{2}\) frozen \(\mathbf{W} = 0\) states, which grows like \(16^{L}\) up to a polynomial factor. The frozen set is exponentially large, and still negligible against a sector whose size grows like \(e^{\kappa L^{3}}\).

Both halves are checked numerically. The family is constructed and every member verified for the ice rule, zero flux and zero flippable hexagons at \((1,1,2)\), \((1,2,2)\), \((2,2,2)\) and \((3,3,3)\), the three axis families disjoint at each; and where the whole frozen set is available by enumeration the number of \((2,2,0)\)-invariant frozen states is exactly \(\binom{2c}{c}^{2}\), namely 36 at \((1,1,2)\), 400 at \((1,1,3)\) and 4,900 at \((1,1,4)\), the last by SAT enumeration (experiments/07_certificates/results/translation_family.json, which also records 5,412 frozen zero-flux states in all at \((1,1,4)\)). Neither theorem exhausts the frozen set: only four of the twelve \((1,1,1)\) states belong to Theorem 2’s family, and frozen states with no translation symmetry at all exist on the thin cells.

Two features of the \((2,2,2)\) row are worth separating. At the smallest cubic cell 192 of the 612 frozen zero-flux states, a little under a third, are neither members of Theorem 2’s family nor tilings of anything smaller, so the two theorems and tiling together still miss a substantial part of the frozen set. And every frozen zero-flux state of \((2,2,2)\) is periodic: the stabiliser-order histogram under the 32 face-centred translations is \(\{2\!:\!192,\ 4\!:\!288,\ 8\!:\!120,\ 16\!:\!12\}\), minimum order two. That is a qualitative difference from the thin cells, where aperiodic frozen states are common, and it is a fact about \(L = 2\) rather than about cubic cells in general.

What the frozen set does to the dynamics

Because frozen states exist in the \(\mathbf{W} = 0\) sector of every cell, that sector is never connected under hexagon flips and its spectral gap is exactly zero at every size. Every statement about relaxation, mixing or the Rokhsar–Kivelson gap must therefore attach to a connected component of the flip graph rather than to the sector, and any future rapid-mixing theorem must carry the same restriction. The natural component is the one containing the chain’s start state, and it should not be assumed to be the largest: at \((1,1,4)\) the canonical start sits in a component of 42,240 states while the giant component has 43,008, and reading the gap off the wrong one misstates it by a factor of 3.6.

Certification

Each theorem is checked by machine in two independent ways, and the counts above in a third. The three artefacts answer different questions and have different trust boundaries.

The Lean 4 developments

Both theorems are formalised in Lean 4 (de Moura and Ullrich 2021), each as a standalone Lake project with no dependencies: core Lean only, no Mathlib, no network fetch, toolchain pinned to leanprover/lean4:v4.33.1.

formal/theorem1/ proves Theorem 1 about the \(4\times4\) matrix model. The structured proof follows the argument above, with the three line lemmas as separate named theorems and the contradiction as one omega step over their equations; an independent brute force over all \(2^{16}\) matrices proves the same statement, evaluated by the Lean kernel through decide +kernel rather than by the compiler. The counts 90 and 12 are theorems rather than evaluations: for each list of states there is a length, a soundness, a distinctness and a completeness theorem quantified over all matrices, which together constitute a cardinality in a setting with no Fintype or Finset.

formal/theorem2/ proves Theorem 2 on the infinite lattice, in a form stronger than the statement above in four respects. The site set is all of \(\mathbb{Z}^3\) rather than the face-centred sublattice; there is no periodic cell and no modular arithmetic; no ice rule is assumed, which is why ‘in every flux sector’ costs nothing; and all three axes come from one lemma parameterised by the axis. Sharpness is formalised, by a state invariant under one of the two translations with a flippable hexagon. The translation-frozen family is formalised as far as core Lean allows: invariance, the ice rule at both sublattices, freezing, faithfulness of the parameterisation by two sign sequences, and the converse that invariance forces layer-constancy and that layer-constancy with ice and balance forces the two-sign-sequence form. The count \(\binom{2c}{c}^{2}\) is not formalised and cannot be without Mathlib, since core Lean has neither Nat.choose nor Finset; nor are the torus quotient, the flux argument or the disjointness corollary. It was the formalisation that caught an error in an earlier derivation of the count, the claim that the ice rule alone forces one arrow up and one down on each double bond; the counterexample is formalised as allUp.

The gap between the formal model and the simulation is closed in both directions. Theorem2/Walk.lean defines a hexagon as the simulation does and proves by exhaustion over all \(4^6 = 4096\) direction sequences that the closed non-backtracking six-walks of zero displacement are exactly the recipe hexagons \((i,j,k,i,j,k)\) with \(i\), \(j\), \(k\) distinct; it identifies the two traversal classes as lists in cycle order and restates Theorem 2 for walks. Theorem2/Count.lean proves the incidence counts, twelve hexagons through every A site and six through every bond, for every point of \(\mathbb{Z}^3\). Export.lean reverses the direction of trust: lake exe hexexport computes the hexagon table of a periodic cell from the Lean definitions and nothing else, and tests/test_lean_bridge.py checks the simulation against those tables at \((1,1,1)\), \((1,1,2)\), \((1,2,2)\) and \((2,2,2)\), comparing the hexagon sets, the cycle order up to rotation and reflection, the traversal partition, and the flippability verdict against the reference predicate on all 90 ice states of \((1,1,1)\).

The axiom audits are the reason to call these machine-checked rather than machine-assisted. formal/theorem1/Axioms.lean and formal/theorem2/Check.lean print #print axioms for 20 and 78 theorems respectively, and every line shows only propext, Quot.sound, or no axioms at all. Classical.choice appears nowhere, so both developments are constructive; sorryAx appears nowhere, so nothing is admitted; and Lean.ofReduceBool appears nowhere, so native_decide is unused and every finite check is carried out by the kernel. What remains unverified is one transcription: some thirty lines of Lean definitions, covering the coordinates, directions, hexagon sites, traversal classes, flippability and the exporter’s box and wrapping, have to be read against the conventions of icemix/lattice.py, and if one of those is wrong both sides are wrong together. The exporter is also a program rather than a proof, built from the same definitions as Count.lean but not verified against them.

Unsatisfiability certificates

The second check re-derives each theorem’s finite instances by a route sharing no code with the first. icemix/cnf.py encodes the model in conjunctive normal form with the arrow bits as the Boolean variables. The ice rule is ‘exactly two of four’ at every site, eight clauses with no auxiliaries. Zero flux uses one cut plane per axis, which suffices because flux is conserved, and \(W_j = 0\) becomes a single cardinality constraint; that this cut-plane flux equals the project’s winding function bit for bit is checked over every ice state at three cells rather than assumed. Flippability is ‘the six bits alternate in cycle order’, so ‘frozen’ is two six-clauses per hexagon and ‘some hexagon is flippable’ is a selector per hexagon plus one clause. Translation invariance is two clauses per bond.

Each theorem becomes an unsatisfiability claim. For Theorem 1 the formula is ‘ice rule, and \(\mathbf{W} = 0\), and some hexagon is flippable’ at \((1,1,1)\); for Theorem 2 it is ‘ice rule, and invariant under both half-diagonals perpendicular to the axis, and some hexagon is flippable’, with no zero-flux constraint at all, which is what makes the certificate establish the theorem in its ‘every flux sector’ form. CaDiCaL rel-3.0.1 refutes each and writes a DRAT proof, and drat-trim (Wetzler, Heule, and Hunt 2014) checks it and must print s VERIFIED. The guarantee is proof-theoretic rather than a claim about the solver: the proof is a sequence of clause additions, each independently confirmed by the checker to preserve satisfiability, ending in the empty clause. The solver’s reasoning, heuristics and correctness are out of the trusted base; only the checker and the CNF file are in it, and the CNF file is small enough to read. The Theorem 1 formula and three Theorem 2 formulas were also given LRAT proofs and accepted by the independent lrat-check (Cruz-Filipe et al. 2017), so no single checker carries the result.

A certificate that cannot fail certifies nothing, so four negative controls drop one hypothesis each and must return satisfiable with a witness that the simulation and the C flip kernel independently confirm to be a flippable ice state. Dropping \(\mathbf{W} = 0\) from the Theorem 1 formula yields a state with four flippable hexagons and winding \((0,0,-2)\), which shows the refutation is about the flux constraint rather than an artefact of the encoding. Dropping the frozen clauses at \((1,1,2)\) yields a zero-flux state with eight flippable hexagons. Dropping one of the two half-diagonals yields 32 flippable hexagons at \((2,2,2)\) and 60 at \((3,3,3)\), which is where those controls had to be placed, since at a cell of transverse extent one the dropped translation is redundant and the control would have been vacuous.

Certified counting

A count has no short proof of the DRAT kind, so counting takes a different route, certified knowledge compilation (Bryant et al. 2025). The formula is compiled to a decision-DNNF representation by d4 (Lagniez and Marquis 2017); cpog-gen turns that representation into a CPOG proof object asserting both that the representation implies the formula and that the formula implies the representation; and cpog-check verifies the proof object against the original CNF and prints its own model count. Only cpog-check’s number is treated as certified, and the compiler’s raw number is recorded separately and required to agree.

Nineteen of twenty formulas were certified, the exception a compiler timeout at \((3,3,3)\) rather than a disagreement. The certified counts are 90, 12 and 12 at \((1,1,1)\) for ice states, zero-flux states and frozen zero-flux states; 3,618, 388 and 68 at \((1,1,2)\); 181,122, 15,024 and 528 at \((1,1,3)\); 204 for the frozen zero-flux states of \((1,2,2)\); and, at two cells the project’s 64-bit enumerator cannot reach, 612 frozen zero-flux states at \((2,2,2)\) and 968 at \((1,2,3)\). Seven further certified counts at \((1,1,1)\) underwrite an unrelated three-bond obstruction. Every count already known by two other methods came back equal to it.

One caveat is structural. A model count runs over all variables of the formula, auxiliaries included, so a certified count is a count of the encoding and agrees with the count of ice states only if every auxiliary is functionally determined by the bond variables. That it is, for the cardinality encoding used here, is checked rather than assumed: the ten rows whose certified count equals a count known independently span three constraint sets and four cells, and the 612 and 968 use the same encoding shape and are each equal to a projected enumeration whose blocking clauses were placed on the bond variables alone. Every state of both censuses was also re-verified individually by the ice-rule and winding predicates and by the C flip kernel. The CPOG proof objects run to hundreds of megabytes each and are not kept in the repository, so re-checking a count means recompiling; the DRAT and LRAT proofs are all under 25 kB and are committed.

Re-checking from the repository

From the repository root, with elan on the path:

cd formal/theorem1 && lake build && lake env lean Axioms.lean
cd formal/theorem2 && lake build && lake env lean Check.lean && lake exe hexexport export
python3 -m pytest tests/test_lean_bridge.py tests/test_frozen.py tests/test_cnf.py

Each lake build must end with Build completed successfully and no warnings, and the two audits must show only propext and Quot.sound. The unsatisfiability certificates need no project code: in experiments/07_certificates/results/certificates/ each claim has a .cnf, a .drat and the checker’s recorded output, so drat-trim thm1_111_drat.cnf thm1_111_drat.drat reproduces the Theorem 1 verdict, and likewise for the fifteen thm2_<axis>_<cell>_drat triples and the four LRAT pairs. Regenerating everything including the counts is run_certificates.py --items A,B,C,D, which needs cadical, drat-trim, lrat-check, d4, cpog-gen and cpog-check on the path.

Related work

Configurations with no flippable plaquette are a familiar feature of the dimer models pyrochlore ice sits alongside; in quantum dimer models they are the staggered configurations at the extreme of the flux range, isolated under local plaquette dynamics and hence exact eigenstates at the Rokhsar–Kivelson point (Rokhsar and Kivelson 1988; Moessner and Raman 2010). The closest three-dimensional bipartite case, the cubic-lattice dimer model, has been studied by Monte Carlo in its Coulomb phase (Huse et al. 2003) and its Rokhsar–Kivelson relaxation examined at a single size (Läuchli, Capponi, and Assaad 2008); the corresponding exponent was measured on the square lattice (Isakov et al. 2011). For spin ice the practical response to local dynamics that moves between ice states too slowly has been to replace it, the loop algorithm of Barkema and Newman (Barkema and Newman 1998) being adapted to the pyrochlore lattice by Melko and Gingras (Melko and Gingras 2004) with cluster variants following (Otsuka 2014; Shinaoka 2011). The present work runs the local chain deliberately and asks what its frozen set is, which is the question those algorithms were designed to make irrelevant.

The link to the quantum problem is the Rokhsar–Kivelson correspondence (Rokhsar and Kivelson 1988; Henley 2004), sharpened by Castelnovo and co-workers into the observation that a Hamiltonian at such a point admits a stochastic-matrix-form decomposition, so that its ground-state phase diagram is an equilibrium partition function and its excitation spectrum a set of classical relaxation rates (Castelnovo et al. 2005). Under that correspondence the generator of the hexagon-flip chain is the ring-exchange Hamiltonian of pyrochlore spin ice at its Rokhsar–Kivelson point (Hermele, Fisher, and Balents 2004; Shannon et al. 2012), so Theorem 2’s \(3\binom{2L}{L}^{2}\) is a lower bound on the ground-space degeneracy at zero flux. An exponentially large set of states inert under a local constraint-preserving dynamics is what the recent literature calls Hilbert space fragmentation, or shattering, a frozen state in the present sense being a one-dimensional Krylov sector (Sala et al. 2020; Khemani, Hermele, and Nandkishore 2020); there the mechanism is usually a set of local constraints or a conserved dipole moment, where here it is the ice rule together with the geometry of the hexagon, explicit enough to be counted exactly. The consequence for sampling is a bottleneck of the sort turned into slow-mixing theorems elsewhere, as for Glauber dynamics of the six-vertex model in its ordered phases (Fahrbach and Randall 2019), although the states counted here are isolated points rather than a barrier between two large regions, so what they support is disconnection rather than slow mixing.

Appendix: artefacts

All paths are relative to the repository root.

References