The model and the question

Pyrochlore ice is the six-vertex constraint on the pyrochlore lattice. Take the diamond lattice, put a spin on every bond, and read the spin as an arrow along that bond. The pyrochlore sites are the bonds, and the tetrahedra are the diamond vertices. The ice rule asks that exactly two of the four arrows at every vertex point in. Positions are integers in units of \(a/4\), a quarter of the conventional cubic edge, so a conventional cell is four units on a side and an \((a,b,c)\) block of cells is a torus with box \((4a, 4b, 4c)\) holding \(8abc\) vertices and \(16abc\) spins. The physics behind the model is standard (Bramwell and Gingras 2001; Castelnovo, Moessner, and Sondhi 2008), and what follows is a finite, combinatorial question about it.

The elementary move on the ice manifold reverses the arrows around a hexagonal plaquette of the diamond lattice, which is legal exactly when the six arrows already circulate head to tail. A hexagon on which they do is flippable, and a state with no flippable hexagon is frozen: an isolated point of the flip dynamics, and in the Rokhsar–Kivelson reading an exact zero-energy eigenstate that is not the uniform superposition (Rokhsar and Kivelson 1988). Hexagons are derived rather than tabulated, as closed non-backtracking six-walks of zero unwrapped displacement, because the quotient graph of a small torus also contains six-cycles that wind and whose reversal would change the flux sector.

Flux is the net arrow current through the three coordinate cut planes, written \(W = (W_x, W_y, W_z)\), and it is conserved by hexagon flips. This note is about the zero-flux sector alone.

The torus carries an abelian group of FCC translations, generated by \((0,2,2)\), \((2,0,2)\) and \((2,2,0)\) modulo the box, of order \(4abc\): 32 elements at \(L = 2\), 108 at \(L = 3\), 256 at \(L = 4\). Each translation permutes the bonds, hence acts on states. The stabiliser of a state is the subgroup fixing it, and a state whose stabiliser is trivial is aperiodic. The question is whether a frozen zero-flux state of a cubic cell can be aperiodic.

At the thin cells the answer is plainly yes, and often. At the first cubic cell it is no, and the census below says so exhaustively. The result of this note is that it is also no at the second cubic cell, where no enumeration is possible, and that the same computation at the third cubic cell did not finish. Why the phenomenon should hold at every \(L\) is a separate question, partly answered by an analytic reduction of the conjecture to a statement about dipole types that is not about cubic cells at all. That work is recorded in docs/frozen-structure-2026-09-05.md and is not covered here.

The encoding

One CNF encoding serves every claim in this note, and its variables are the arrow bits themselves: bond \(e\) is DIMACS variable \(e + 1\), true when the arrow points from the A-sublattice end of the bond to the B end. Auxiliary variables are allocated above the bond variables and are never projected on, so a model restricted to the bond variables is a state and nothing else.

Ice rule. At either sublattice the condition “exactly two of the four incident arrows point in” reduces to “exactly two of the four incident bits are set”, and exactly-two-of-four over four literals is eight clauses with no auxiliaries: forbid any three true, forbid any three false.

Zero flux. Because flux is conserved, one cut plane per axis is enough. The plane \(x_j = 1/2\) is a good choice, since A-sites have even coordinates, so the only bond segments crossing it leave an A-site at \(x_j = 0\) with \(\mathrm{sgn}(d_j) = +1\). There are exactly \(4abc/\text{cells}_j\) of them and every one carries \(+1\), so \(W_j = 2\,\mathrm{popcount} - n_{\text{cross}}\) and the constraint \(W_j = 0\) is the single cardinality condition that exactly half of the crossing bits are set, encoded with a sequential counter. That this cut-plane flux agrees bit for bit with the project’s own winding function is checked over every ice state of three cells rather than assumed.

Frozen. Walking a hexagon in cycle order, the traversal alternates with respect to each bond’s own A-to-B orientation, so flippability is the statement that the six bits alternate: positions 0, 2, 4 all equal to \(b\) and positions 1, 3, 5 all equal to \(1 - b\). Blocking both patterns is two six-clauses per hexagon, with no auxiliaries at all, which is why the frozen formula stays small and prunes hard. The encoding was cross-checked against a reference implementation written directly from the definition, over every hexagon of three cells, with no mismatches.

Aperiodicity. A state is aperiodic exactly when, for every nontrivial translation \(t\), some bond disagrees with its image. That is a disjunction of disequalities, so it needs one auxiliary per moved bond per translation: \(d_{t,e}\) with the two clauses \((\neg d \vee x_e \vee x_f)\) and \((\neg d \vee \neg x_e \vee \neg x_f)\), where \(f = \pi_t(e)\), together with one long clause \((d_{t,e_1} \vee \cdots \vee d_{t,e_m})\) per translation. The definition is one-directional because only one witness per translation is wanted, which halves the clause count, and bonds fixed by \(t\) are skipped because their auxiliary could never satisfy the disjunction.

This block dominates the formula. At \(L = 3\) it is 92,555 of the 99,035 clauses, and it is what makes the instance hard: the base formula \(\text{ice} \wedge W = 0 \wedge \text{frozen}\) at \(L = 3\) is satisfiable in 1.81 s, whereas requiring 107 simultaneous disagreements is not settled in two hours.

The Cauchy reduction. The stabiliser is a subgroup of a finite abelian group, so if it is nontrivial it contains an element of prime order. Excluding invariance under the prime-order translations alone is therefore equivalent to excluding it under all of them, and the two encodings have the same models rather than merely the same satisfiability. The saving depends on the group. At \(L = 3\) the group of order 108 has 3 elements of order 2, 26 of order 3 and 78 of order 6, so 29 of the 107 nontrivial translations are of prime order and the formula falls from 48,600 variables and 99,035 clauses to 14,904 and 31,565. At \(L = 4\) the group of order 256 is a 2-group, only its seven involutions have prime order, and the reduction is larger still: 268,288 variables and 540,927 clauses become 14,336 and 32,775.

The reduction is gated rather than trusted. At \((1,1,2)\), \((1,2,2)\) and \((1,2,3)\) the models of the full and reduced encodings were enumerated separately and compared as sets, not as counts, and both were compared with a third, solver-free method: a stabiliser census of the whole frozen zero-flux set. All three agree, at 16, 64 and 336 aperiodic states respectively. A further test checks the group-theoretic step state by state, with no solver at all, over each of the 968 frozen zero-flux states of \((1,2,3)\).

The first cubic cell

At \(L = 2\) the cell has 128 spins and 128 hexagons, beyond the project’s 64-bit enumerator, but the frozen constraint prunes the SAT search so sharply that the whole set can be listed. Blocking on bond variables only, the search exhausts in 4.2 s and returns 612 frozen zero-flux states from a formula of 512 variables and 1,536 clauses. Every one of the 612 was then re-verified independently by the project’s ice-rule and winding predicates and by the C flip kernel, with no failures.

Two methods agree on the number, since the project’s own depth-first enumerator cannot reach this cell. The SAT enumeration gives 612, and a certified model count gives 612, obtained by compiling the formula with d4 and checking the compilation with cpog-check, whose own line Regular model count = 612 is what is treated as certified. The same pipeline certifies 968 at \((1,2,3)\) and reproduces the smaller counts that the enumerator and a frontier dynamic program already knew: 90, 3,618 and 181,122 ice states, 12, 388 and 15,024 zero-flux states, and 12, 68, 528 and 204 frozen states across four cells. So the encoding is known to agree with the enumerator wherever both can run, before the counts it alone can reach are believed.

The census answers the question directly. Under the 32 FCC translations the stabiliser orders of the 612 states are distributed as follows.

The minimum is 2. No frozen zero-flux state of \((2,2,2)\) is aperiodic.

The same statement was then put to a solver as an existence query, so that it carries a proof object rather than an enumeration. The formula \(\text{ice} \wedge W = 0 \wedge \text{frozen} \wedge \text{aperiodic}\) at \((2,2,2)\) has 4,480 variables and 9,503 clauses, CaDiCaL refutes it in 3.08 s, and the 5,278,492-byte DRAT proof is accepted by drat-trim in 2.24 s. The prime-order form of the same query is smaller (1,408 variables, 3,335 clauses), is refuted in 1.482 s, and its 5,245,914-byte proof is accepted in 1.073 s. An in-process solver agrees with both. The negative control drops only the frozen clauses and becomes satisfiable, and its witness is an aperiodic zero-flux ice state with 22 flippable hexagons, so the certificate is capable of failing.

The breakdown matters downstream. Of the 612, 108 belong to the translation-invariant family that the project’s second frozen-state theorem constructs and 420 are tilings of frozen states of a proper sub-cell, the family sitting inside the tilings, which leaves 192 in neither class, every one of stabiliser order exactly 4. Read through the dipole classification of the companion note the same 612 split as 312 states in which all three dipole axes occur, all of them carrying a whole-cube coordinate period, and 300 with an axis missing, of which 108 have such a period and 192 do not. Both routes count 420 states with a whole-cube period, as they must, since that set is the tilings by definition.

The second cubic cell

Why direct solving failed

At \(L = 3\) the cell has 432 spins, 432 hexagons and a translation group of order 108. Enumeration is out of the question — the blocking-clause search was abandoned after twenty minutes without reaching a 3,000-model cap, and d4 hit a 900 s wall compiling the frozen formula, so the number of frozen zero-flux states at \(L = 3\) is still unknown. The existence query is a different matter, and it is the one that has to be asked.

Plain CaDiCaL (Biere et al. 2020) on the full 107-translation formula (48,600 variables, 99,035 clauses) reached its two-hour cap with no verdict, having logged 12,156,776 conflicts and 386,339 restarts while leaving 47,106 of 48,600 variables unassigned at the root. That last figure is the informative one, because after twelve million conflicts the search had fixed almost nothing at level zero. On the reduced formula, given the same two hours each, CaDiCaL and Kissat both timed out as well, writing 3.88 GB and 2.88 GB of partial proof that certify nothing. A 3.26-fold reduction in formula size does not put this instance inside a single-core budget.

Two facts locate the difficulty. The base formula without the aperiodicity block is satisfiable in 1.81 s. The weaker query that excludes only the 26 whole-cell shifts, asking for a frozen zero-flux state that tiles no proper sub-torus, is satisfiable in 15.29 s, and its model is a genuine frozen state whose entire symmetry is the single half-box diagonal \((0,6,6)\). So the hardness is created by the simultaneous exclusion of every translation at once, and by nothing else.

The scheme

Cube and conquer splits an instance into many easier ones by a lookahead cuber and refutes each with a CDCL solver (Heule et al. 2012). Here march_cu at depth 12 produced 3,777 cubes in 112.7 s, of which 117 were already refuted during cubing. Those cubes were sharded eight at a time across twelve workers with a one-hour cap per shard: 468 shards came back UNSAT, five hit the cap, none was satisfiable, and the refuted shards consumed 42,769 core-seconds (mean 91.4 s, maximum 2,450.9 s) in 7,138 s of wall clock.

The five unfinished shards hold forty cubes, and they turned out not to be hard at all. Re-solved with the cube’s literals written into the formula as unit clauses rather than passed through the incremental assumption interface, all forty were refuted with a mean of 48.8 s and a maximum of 276.9 s. Preprocessing is the whole difference, because probing, elimination and vivification act on unit clauses and not on assumptions. Those forty cubes were nonetheless split further, by march_cu at depth 8, into 5,485 sub-cubes, so that the leaf set handed to the certifying pass was uniformly easy. The final leaf set is therefore \(3{,}777 - 40 + 5{,}485 = 9{,}222\) cubes, and it partitions the search space exactly as the original cube set did.

That settled the answer. Certifying it is a separate problem, and the obvious route fails. Composing one DRAT proof of the whole refutation requires a serial incremental pass, because it is the sequence of learned clauses that makes the concatenation a proof. A four-hour attempt reached 11.9 GB without finishing, on the way to an object that backward DRAT checking could not have processed in any reasonable time.

The route that works replaces one monolith by 9,222 independent objects. Write \(F\) for the reduced formula and \(c_1, \dots, c_{9222}\) for the leaf cubes. The certificate has two halves.

1. Every leaf is refuted. For each \(c_i\), the CNF \(F\) with the cube’s literals appended as unit clauses is unsatisfiable, with a standalone LRAT proof that lrat-check accepts on its own. No proof depends on any other, there is no shared solver state and no ordering.

2. The leaves are exhaustive. The CNF whose 9,222 clauses are the negations of the leaf cubes is unsatisfiable, with a DRAT proof that drat-trim accepts. This says more than is needed, since it rules out any assignment escaping every leaf, not merely any model of \(F\).

Together they force \(F\) unsatisfiable. Suppose \(M\) satisfied \(F\). By (B), \(M\) satisfies some \(c_i\); then \(M\) satisfies \(F \wedge c_i\), which (A) refutes.

Two details are where such schemes usually go wrong. The cover proof is taken over the negated cubes alone, with no reference to \(F\). Had the cuber dropped leaves it refuted during cubing, that CNF would have come back satisfiable and the fallback would have been the weaker \(F \wedge \neg c_1 \wedge \cdots \wedge \neg c_{9222}\). It did not, and drat-trim reports 9,222 of 9,222 clauses in the core, so every leaf is used and none is missing. And each leaf proof is checked against the leaf CNF regenerated deterministically from \(F\) and the cube, rather than against a stored copy, so the binding between cube and proof is real.

The run

A pre-flight on 24 leaves drawn uniformly at random projected 0.12 h of wall clock, low by a factor of about 2.5 on solver time, because the per-leaf cost is heavy tailed and 24 samples do not see the tail. Checking was cheap throughout: lrat-check ran at 19 % of the solving time, and even the 267 MB worst case took 5.7 s to check against 101 s to solve.

The cover proof is cheaper still. Its CNF is 9,222 clauses over 14,904 variables in 593,545 B, CaDiCaL refutes it in 0.078 s, the DRAT proof is 3,449,033 B, and drat-trim accepts it in 0.165 s with all 9,222 clauses in the core. Both files are small enough to live in the repository, so that half of the certificate needs no external storage.

The result:

No frozen zero-flux ice state of the cubic cell \((3,3,3)\) has trivial stabiliser under the FCC translation group of the torus. Equivalently, every frozen zero-flux state of \((3,3,3)\) is invariant under some nonzero FCC translation.

The manifest, the checker, and how to re-verify

results/aperiodic3/manifest.json (5.4 MB, schema ice-mixing/aperiodic3-cnc-certificate/1) states the claim and the scheme in prose and then records the formula’s path, sha256 and size; the reduction parameters, including the 29 of 108 translations used; the leaves file with its sha256, count and provenance; the retention policy; tool versions and source commits, namely CaDiCaL 3.0.1 at c6073042 and drat-trim/lrat-check at 2e3b2dc0; the aggregate timings; the cover-proof hashes and verdict; and one record per leaf, carrying its cube, both verdicts, both timings, the proof’s format, size and sha256, and, where retained, its path.

experiments/07_certificates/verify_cnc_certificate.py re-checks all of it and imports nothing outside the Python standard library, so it can be handed to someone who has neither the project nor its dependencies. Given cadical, lrat-check and drat-trim on the path and the proof directory in place,

python3 experiments/07_certificates/verify_cnc_certificate.py

hashes the formula and the leaves against the manifest, rebuilds the cover CNF from the leaves and re-checks its DRAT proof, then re-checks all 9,222 leaf proofs, taking retained proofs as stored and regenerating deleted ones first. A regenerated proof is a fresh object whose hash need not match the recorded one, and the verifier says so when it takes that path. A hash mismatch on a retained proof means tampering, and the verifier fails on it. The full pass reports PASS in 832.1 s on twelve workers, with 8,588 proofs checked as stored and 634 regenerated. Cheaper variants exist: --sample 20 --kept-only is about a second, and --sample 300 exercises the regeneration path in about a minute.

The verifier can fail, which was established rather than assumed. Checking leaf \(i\)’s proof against leaf \(j\)’s CNF gives c NOT VERIFIED; the same proof against its own CNF gives c VERIFIED; a deliberately wrong sha256 in the manifest is rejected before any checking; and the cover CNF with a single leaf’s clause dropped comes back satisfiable, so exhaustiveness is a real constraint and not a tautology of the encoding.

Two limits should be stated. The certificate covers the prime-order reduced formula, and the equivalence of that formula with the full 107-translation encoding is established by tests and by the two-method gate rather than by a proof object. Every leaf proof was produced by CaDiCaL and checked by lrat-check, and only the cover proof uses the second checker, so there is no cross-implementation confidence at the leaf level, and no formally verified checker was used at all.

The third cubic cell, and what it does not establish

At \(L = 4\) the cell has 1,024 spins and the translation group has order 256. Being a 2-group it has only seven prime-order elements, the nonzero half-box shifts, so the Cauchy reduction is 18.7-fold on variables and the reduced formula is smaller than the one at \(L = 3\): 14,336 variables and 32,775 clauses against 14,904 and 31,565. On formula size alone \(L = 4\) looks cheaper than \(L = 3\).

It is not. Both CaDiCaL and Kissat time out on the reduced formula at a 15-minute cap. march_cu aborts on it at every depth and under every option combination tried, with an assertion failure in its bookkeeping of big clauses that have shrunk to binary. The seven aperiodicity clauses of length 1,024 are what trips it, and a ternary ladder over fresh variables, used for cubing only, works around it. Nothing downstream trusts the cuber: the cubes mention only original variables, so each leaf is solved against the original formula, and the exhaustiveness half of the certificate checks the cube set on its own.

Cubing at depth 20 gave 18,149 cubes, 7,473 of them refuted during cubing. Of the 18,149, some 18,115 were refuted with an lrat-check-verified proof inside a 900 s cap and 34 were not, in 5,565 s of wall clock on twelve workers. Splitting those 34 by march_cu at depth 8 produced 5,038 sub-cubes, of which 4,631 were refuted and 407 were not. The final leaf set is \(18{,}149 - 34 + 5{,}038 = 23{,}153\) cubes, with 22,746 refuted under a checked proof against 407 unrefuted. The cover proof over that leaf set verifies: CaDiCaL refutes it in 0.532 s, drat-trim accepts the 15,130,254-byte proof in 1.157 s, and all 23,153 clauses are in the core. The manifest records conclusion: INCOMPLETE, marks its claim text PARTIAL, and lists the 407 unrefuted leaves by index. The verifier passes 17,658 stored leaf proofs with none failing in 215.1 s, reporting PASS (partial run), and a further 120-leaf sample exercising the regeneration path passes as well.

What that establishes is precise. The leaves partition the assignment space, which the cover proof certifies and which summing \(2^{-|c|}\) over them confirms at exactly 1; the same sum over the 407 unrefuted leaves is \(1.516 \times 10^{-6}\). So no frozen aperiodic state exists anywhere in 99.99985 % of the search space, one part in 659,547 remaining, and no leaf anywhere at any level was satisfiable. What it does not establish is the theorem. One unrefuted leaf would be enough to leave the question open, and there are 407.

The residue resists splitting, which is the substantive finding of the stage. The 34 level-one cubes represented about 30,600 unresolved core-seconds, their 5,038 children consumed roughly 146,000 core-seconds and 407 remain. A depth-6 split of those 407 produces 17,149 sub-leaves, of which a 96-leaf uniform sample still had 11.5 % failing to close inside 300 s, projecting 767,006 solver core-seconds, or 18.2 h on twelve workers, and it would leave a residue of its own. That level was not launched. Across every level the run consumed 200,581 solver core-seconds and 9,214.9 checker core-seconds and wrote 124.6 GB of proof, the largest single proof being 2.60 GB.

The 407 are a small, named object, descending from 29 of the 34 level-one cubes with the worst single parent contributing 46, and they are isolated on disk. Finishing by brute force is affordable and unattractive, since splitting has so far increased total work rather than reduced it. A different cuber, or a hand-chosen split on the bond variables of one sub-cell rather than a lookahead choice, is the cheaper thing to try, as is understanding what makes those cubes hard, which is where the structural work of the companion note bears.

The thin cells, for contrast

Aperiodic frozen zero-flux states are not rare in general. They are common whenever some extent of the cell is 1, and they are absent from every cell enumerated so far whose three extents are all at least 2.

At \((1,3,3)\) more than half the frozen zero-flux states are aperiodic. The contrast is sharp enough to say that the periodicity phenomenon is a fact about cells thick in every direction rather than about cubic cells as such, and the \((2,2,3)\) row, an exhaustive enumeration of 4,368 states, is the cheapest evidence for that reading. It also rules out the lazy reading under which aperiodic frozen states are merely too rare to find at larger sizes. They exist in quantity, and only the thickness of the cell suppresses them.

Related work

Cube and conquer was introduced to make lookahead and CDCL solvers cooperate on instances that neither settles alone, the cuber splitting the problem into many cubes and the CDCL solver refuting each (Heule et al. 2012). It is what carried the two best-known combinatorial refutations of the last decade, the Boolean Pythagorean triples problem (Heule, Kullmann, and Marek 2016) and Schur number five (Heule 2018). In both the answer and the certificate came out of the same machinery and the certificate was the harder half. The general argument for that style of result, and for taking the proof object as the unit of trust, is Heule and Kullmann’s (Heule and Kullmann 2017). Keller’s conjecture is the other standard example (Brakensiek et al. 2020).

Clausal proof formats are what make such results checkable. DRAT is the format solvers emit, and drat-trim checks it by backward resolution and trims it to a core (Wetzler, Heule, and Hunt 2014). Backward checking is expensive, often as expensive as solving, and LRAT removes that cost by carrying antecedent hints in the proof so that a checker verifies in one forward linear pass (Cruz-Filipe et al. 2017). That difference is what the \(L = 3\) certificate turns on. Here 9,222 LRAT proofs check in 19 % of the time it took to find them, where one composed DRAT proof of the same refutation was not checkable at any size that could be produced. LRAT also makes a formally verified checker reachable, cake_lpr being one verified in CakeML down to its machine code (Tan, Heule, and Myreen 2021). Nothing here uses one, and that is the next rung. The certified model count at \(L = 2\) uses the CPOG toolchain, which produces a checkable proof of a knowledge-compilation result and hence of a model count (Bryant et al. 2023).

On the physics side the ice-rule manifold has been studied since Pauling’s residual-entropy argument (Pauling 1935) and Anderson’s identification of the pyrochlore Ising ground-state condition with the ice rule (Anderson 1956), with the two-dimensional case solved exactly by Lieb (Lieb 1967) and the pyrochlore spin-ice realisation established experimentally by Harris and co-workers (Harris et al. 1997). The manifold carries an emergent gauge structure (Hermele, Fisher, and Balents 2004), and adding dipolar interactions selects an ordered, periodic ground state out of it (Melko, den Hertog, and Gingras 2001). The statement in this note is transverse to all of that. It concerns the states the local dynamics cannot leave rather than the states it visits, and the frozen set is where the standard height or flux description gives no purchase, because these states are isolated points and not typical members of a sector. The dimer literature has an analogous separation, its variational and limit-shape theory describing typical tilings (Cohn, Kenyon, and Propp 2001; Kenyon, Okounkov, and Sheffield 2006; Sheffield 2005) while frozen or rigid configurations sit outside it. I am not aware of a prior statement, for ice on the pyrochlore lattice, that the frozen states of a periodic cell must themselves be periodic, and what is offered here is finite evidence for one at the two smallest cubic cells rather than a proof in general.

Appendix: Artefacts

All paths are relative to the repository root.

Encoding and group theory. icemix/cnf.py — ice_clauses, zero_flux_clauses, frozen_clauses, aperiodic_clauses, translation_order, prime_order_translations, whole_cell_shifts, build_cnf, stabiliser_census_int. icemix/frozen.py — fcc_translations, translation_perm, stabiliser_census. icemix/lattice.py — the lattice and the derived hexagon set. Tests in tests/test_cnf.py, including the prime-order equivalence as model sets and the state-by-state Cauchy check.

\(L = 2\). experiments/07_certificates/results/part_D.json — the 612 states, the stabiliser histogram, the family and tiling breakdown. .../part_C.json — the certified model counts. .../results/aperiodic/gate.json — the \((2,2,2)\) refutation, its DRAT verdict and its negative control; artefacts under .../results/aperiodic/certificates/. .../results/aperiodic2/gate.json — the prime-order form of the same. experiments/08_frozen_structure/results/census.json — the dipole-type crosstabulation.

\(L = 3\). .../results/aperiodic2/build.json — formula sizes and the translation-order histogram. .../cnc.json, .../cnc_refine_pass1.json — the cube-and-conquer run. .../solvers.json — the two timed-out direct solvers. .../results/aperiodic3/manifest.json — the certificate manifest. .../results/aperiodic3/cover.cnf, .../cover.drat, .../cover.json — the exhaustiveness half. .../results/aperiodic3/leaves.icnf, .../leaves.json, .../verify_full.log — the leaves and the independent pass. Leaf proofs live outside the repository under ~/.local/state/ice-mixing-proofs/aperiodic3/.

\(L = 4\). .../results/aperiodic2/preflight_444/ — formula, ladder variant, direct-solver probes, cubing. .../results/aperiodic3-444/manifest.json — the partial manifest, with conclusion: INCOMPLETE and the 407 unrefuted leaves listed. .../aperiodic3-444/leaves_l1.json, .../leaves_l2b.json, .../cover.json.

Runners and the checker. experiments/07_certificates/run_aperiodic.py, run_aperiodic2.py, run_aperiodic3.py, verify_cnc_certificate.py; experiments/08_frozen_structure/run_structure.py.

Companion note. docs/frozen-structure-2026-09-05.md — the dipole classification, Lemma A, and the reduction of the general conjecture.

References