DRAT certificates for Theorem U′, (R⁺) and (S≥1) on the (L,L,L) torus at L = 4, 5 and 6, with controls, an independent encoding and a corpus check; Theorem H at L = 4, 5, 6 modulo the 2026-09-27 reduction and K_u

Status tags as in the note. certified means: the CNF is written to a file, cadical 3.0.1 refutes it with a DRAT proof, drat-trim prints s VERIFIED, and the control CNF is SAT with its witness decoded and re-checked by arithmetic. All computation ran on the primary Mac in the project .venv, one solver or checker process at a time, each a child process with a hard subprocess.run timeout. No Spark was used, nothing was committed, and no tracked file was edited. New scripts are scratch_h/h280_certlib.py, h281_cagecheck.py, h282_certify.py, h283_symcheck.py, h284_corpus.py and h285_summary.py. Certificates are in scratch_h/certs/h282_*, with results in certs/h28x_results.jsonl and SHA-256 sums in certs/h28x_sha256_2026-09-27.txt.

Notes by the main loop (2026-09-27). (i) The independent check of the reduction has since landed (2026-09-27-opus-check.md: confirmed, no gap), so the first caveat of §6 is met. (ii) Lemma A in §6 (iii) is not needed for H: a state with a type absent has an empty axis. (iii) Main-loop verification of these certificates: drat-trim re-run on two kept proofs (U′ at L = 4, (R⁺) at L = 6, separation 11), s VERIFIED; one proof that was not kept (U′ at L = 5) regenerated with cadical, its SHA-256 equal to the recorded one, s VERIFIED in 4.1 s, its control SAT. (iv) The h282_* files are not committed (738 MB); the hashes and the verdict file are.

1. Verdict table

Each row covers every query of that statement at that L. Times are wall-clock per query (maximum over the row). Proof sizes are in bytes.

All 114 certificates are listed individually in certs/h28x_results.jsonl. The finite side facts were also checked:

• The cage table (§2.1) is correct on all six cages (A and B, axes x, y, z), at both L = 3 and L = 4.
• Every symmetry used (§3) preserves the base CNF, checked as a clause-set identity at L = 4, 5 and 6.
• The corpus check (§4) found 0 failures on the odd corpus at L = 3 (637 states) and L = 4 (720 states).

Timing estimates made before each batch (brief’s rule):

• U′: one query at L = 4 took about 5 s including drat-trim, so 16 queries ≈ 1.5 min (actual 80 s). One query at L = 5 took 12 s, so 15 more ≈ 3.3 min (actual about 3.5 min). One query at L = 6 took 32 s, which is under the two-minute threshold for L = 6, so 3 more ≈ 1.7 min (actual 1.8 min).
• (R⁺) and (S≥1): under 10 s per query at every L, so each batch was under 2 min.

Every batch ran in the foreground, and nothing went to the queue.

Proofs not kept. 20 proofs are larger than 50 MB: U′ at L = 5 (16 proofs) and at L = 6 (4 proofs). Each was deleted after drat-trim verified it. Its SHA-256 and size are recorded, and its CNF is kept.

certs/h282_* is large: 437 MB of CNFs and 301 MB of kept proofs. Of the proofs, 152 MB are the four U′ proofs at L = 4 and most of the rest are (R⁺) at L = 6. Everything is regenerable with h282_certify.py. Before committing, decide whether to commit the files, gzip them, or keep only the hash file and results.

2. What each certificate proves

Models. The encoding is h280_certlib.Model. It was written from the definitions in rods §1, not from a4_typemodel or h213, and has no auxiliary variables.

• Type-only model 𝒯. One-hot types. (T2) on every hexagon: at most two of the six match literals are true (every triple is forbidden), and at least two are true (every five-subset contains a true literal). The match literal of v in h is t(v, a), where a is the one coordinate in which the displacements from v to its two hexagon neighbours agree. It is computed from positions.
• Sign model 𝒮. 𝒯 plus one sign variable per vertex, with the bond rule d_{τ(a)} ε(a) = d_{τ(b)} ε(b) on every bond (d = b − a). The rule is written as 18 clauses per bond, one pair for each (τ(a), τ(b)).
• “Some hexagon odd”. Each hexagon has a selector s(h). s(h) forbids a match on A together with a match on B, so with (T2) it forces both matches onto one sublattice, which means odd curl (A-count form, rods §1). The clause ⋁_h s(h) is the negated conclusion of U′.

Theorem U′ (certified at L = 4, 5, 6). Setting: the (L,L,L) torus. Let:

• O be a hole of either sublattice;
• k be an axis, and {a, b} the other two axes, in either order;
• v = O − 2e_k and v′ = O + 2e_k both have type k;
• one bridgehead O + s with s_k = −1 has type a, and one bridgehead with s_k = +1 has type b.

Then no type field of 𝒯 has an odd hexagon. The same therefore holds for every frozen state (§5).

• At L = 4 and 5: all 16 hypotheses at the base hole with k = x were refuted directly. That is 2 sublattices × 2 orders (lower y and upper z, or lower z and upper y) × 2 choices of lower bridgehead × 2 choices of upper bridgehead.
• At L = 6: 4 were refuted directly (sublattice × order, lower₀/upper₀). The other 12 follow from the orbit result of §3: all 16 hypotheses form one orbit.

Cage table (finite, re-derived in h281_cagecheck.py). This is the check behind Lemma O at straight holes.

• Every cage with both rods of type k has 144 (T2) patterns on its 4 hexagons.
• In every pattern, the bond rule on the 12 cage bonds is consistent.
• The hole is unoriented (ε(v) ≠ ε(v′), so both rods point in or both point out) exactly when the bridgeheads are aa/bb or bb/aa, where {a, b} are the transverse axes. That is 32 patterns per cage (96 over three axes, matching Lemma sP).
• This was checked directly on all six cages (A and B, k = x, y, z), at L = 3 and L = 4. It agrees with h97 and is independent of it: orientation is read here from the solved sign field, not from h97’s bit calculus.

Lemma O at straight holes. An unoriented straight hole carries the full pattern aa/bb or bb/aa. That pattern contains the four literals of U′ for any choice of bridgeheads, so the state has no odd hexagon. Only the trivial direction “full pattern ⇒ four literals” is used; the converse, Lemma U0, is not needed.

(R⁺) (certified at L = 4, 5, 6). In 𝒮: take u ∈ A and w ∈ B with w − u = (s, e₁, e₂) along (k, k+1, k+2), where e₁, e₂ = ±1 and s is odd. There are L residues of s mod 4L per (e₁, e₂), fixed by s + e₁ + e₂ ≡ 3 (mod 4). These are every k-separation that occurs on the torus. Then τ(u) = τ(w) = k together with ε(u) ≠ ε(w) is UNSAT.

• All 4L offsets were certified directly for k = x: 16, 20 and 24 queries.
• Every pair at transverse offset (±1, ±1) is an A–B pair, so taking u ∈ A loses nothing.
• Separation ±1 is the same-type bond (the proof is 22 bytes) and ±3 is Lemma R. At L = 6 the new separations are ±5, ±7, ±9 and ±11.

(S≥1) (certified at L = 4, 5, 6). In 𝒮, no oddness: take v of either sublattice and w = v + 4(g+1)e_k with 1 ≤ g ≤ L − 2. These are all the gaps that occur: g = L − 1 would give w = v. Then τ(v) = τ(w) = k, together with τ(v + 4r e_k) ≠ k for 1 ≤ r ≤ g, and ε(v) ≠ ε(w), is UNSAT.

• Only the arc of g vertices is constrained. The other arc, of L − 2 − g vertices, is free.
• Both sublattices and all gaps were certified directly for k = x.

Controls. Each control is the query without its negated conclusion (U′), or with the conclusion asserted, ε(u) = ε(w) (R⁺ and S≥1). All 114 are SAT. Each witness was decoded and re-checked by arithmetic, not by the CNF: one-hot, (T2) counted per hexagon, the bond rule from positions, and the hypothesis literals. The U′ control witnesses have 0 odd hexagons, as they must. Earlier runs agree with these verdicts: h119 (U′, L = 3, 4, 5), extremal §9 (R⁺, L = 3, 4, 5) and rphand row 14 (S≥1, L = 4, 5). L = 6 is new for all three.

3. Symmetries relied on

A literal permutation σ with σ(F) = F gives: F ∧ H is UNSAT ⟺ F ∧ σ(H) is UNSAT. h283_symcheck.py checks σ(F) = F as a clause-set identity on the full base CNF at L = 4, 5 and 6. The generators are:

A deliberate non-symmetry was used as a control and is rejected at every L.

What the certificates cover, and which arguments they rest on:

• Every position: the FCC translations, which act transitively on A and on B.
• Every axis: C.
• The opposite sign polarity in (R⁺) and (S≥1): the global flip.

Nothing else is needed at L = 4 and 5, because both sublattices, both orders and every bridgehead choice (U′), every offset (R⁺), and every gap on both sublattices (S≥1) were certified directly.

At L = 6, U′ also uses the orbit computation. All 32 cage-preserving lattice maps were each checked to be automorphisms of the type-only CNF, and they join the 16 U′ hypotheses into one orbit at every L tested (4, 5, 6). So a single certificate would suffice at each L. The 4 direct certificates at L = 6, one per sublattice and order, are redundant on that argument.

4. Independent encoding check (corpus)

h284_corpus.py ran on the whole odd corpus (h38_lib.load_odd_corpus). For every state:

1. Signs were obtained from the types by BFS on the bond rule. They were always consistent.
2. Both full base CNFs were evaluated clause by clause, with s(h) = [h odd]. Nothing was falsified, and the clause “some hexagon odd” held.
3. Every occurrence of each hypothesis, at every position and on every axis, was counted, and the conclusion was checked on it.
4. For the first occurrence per (state, query, axis), the state was carried by a translation composed with a power of C, plus the flip if needed, so that the occurrence sits at the certificate’s base vertex. The certificate’s own clause sets were then evaluated on the image: the hypothesis-only CNF and the control CNF must be satisfied, and the query CNF must be falsified.

U′’s full pattern cannot occur in an odd state. So for U′ the sub-patterns “rods + one lower a” and “rods + one upper b” (plus “some hexagon odd”) were placed at the base cage and evaluated instead. This checks the rod and bridgehead geometry of the encoding.

An evaluator control (one type changed, or one sign changed) is caught (10, 8 and 4 clauses falsified).

So no UNSAT verdict can come from an over-constrained base or hypothesis encoding: real frozen states satisfy every hypothesis-only CNF, and every control CNF, wherever the pattern occurs.

5. Is (T2) part of the model, and are the solutions exactly the frozen states?

(T2) is legitimately part of the model. It is a theorem of frozen states on the torus (Lemma L; the note’s source–sink form, line 588). A match is a vertex where the hexagon’s two bonds are both in or both out, so the matches are the hexagon’s sources and sinks. A non-flippable hexagon has at least one source. Every vertex is the source of exactly two hexagons, so Σ_h #sources = 2|V| = |Hex|, and each hexagon has exactly one source and one sink, hence exactly two matches.

The solutions of 𝒮 are exactly the frozen ice states (rods §1):

• The six two-in-two-out arrangements at a vertex correspond one to one to the moments ε e_τ.
• The arrows of a bond agree from both ends ⟺ the bond rule holds.
• Given the ice rule, (T2) means every hexagon has two matches. A directed hexagon has none, so (T2) excludes every flippable hexagon: (T2) ⇒ frozen. Lemma L gives the converse.

𝒯 is a strict superset of the frozen type fields (there is no cocycle condition), so the U′ certificates prove more than Lemma O needs.

“Some hexagon odd” in the certificates is exactly “not curl-free”, by the A-count form κ_h ≡ 1 + #A-rev(h) (mod 2).

6. What can now be written about Theorem H

Theorem H holds on the (L,L,L) torus for L = 4, 5 and 6: in every frozen state in which all six dipole directions occur, every hexagon has even curl. This rests on the following.

• (i) The certificates of this report at that L:
  • Theorem U′: h282_U_L{L}_*. With the cage table (h281), it gives Lemma O at straight holes.
  • (R⁺) at every k-separation: h282_R_L{L}_*.
  • (S≥1) at every gap: h282_S_L{L}_*.
  • The symmetry reduction: translations, the cyclic permutation and the sign flip, verified as CNF automorphisms at that L (h283).
• (ii) K_u, as recorded in the note (Status of 2026-09-11, and “P1 and Theorem P proved for every cell”, 2026-09-17), with its window certificates (seven grids × five transverse steps, so every cell with 4a ≥ 7 and 2b, 2c ≥ 5) and the Lemma S automaton. The synthesis records K_u’s scope as (L,L,L) with L ≥ 4. I did not re-audit that scope.
• (iii) The reduction H ⇐ K_u + Lemma O + (R⁺) + (S≥1) (rphand §§1–4, audited by the main loop in synthesis §1), with the hand-proved results it uses:
  • Lemma O at corner holes;
  • law C and law Pᵏ;
  • Lemma sP (cage check), Theorem sLC, the two-product lemma, the stripe theorem, Theorem W and Lemma E;
  • Theorem D, Theorem LC, Lemma S1, Theorem M′, and Lemma A (two-type states).
• (iv) Lemma L ((T2) in frozen states; proved by hand).

Caveats to state with it:

• The reduction (iii) has been audited once and has no independent checker yet. The synthesis asks for one.
• The theorem is certified per L. Nothing here is uniform in L.
• At L = 3, K_u’s certificates are not claimed to apply, and no certificate was produced here at L = 3.

7. What was not reached

• L ≥ 7 was not attempted. At L = 6, U′ takes about 20 s and 350 MB of proof per query, so L = 7 looks feasible if wanted.
• U′ at L = 6: 4 of the 16 hypotheses were certified directly; the other 12 rest on the verified single orbit (§3).
• Proof files over 50 MB (U′ at L = 5 and 6) are not kept, and drat-trim was run on them once, here. The main loop has not re-run drat-trim on them, as it did for the 2026-09-11 certificates. Re-running needs regeneration (cadical 3.0.1; compare hashes).
• Not revisited: Lemma U0 (not needed; §2) and K_u’s certificates.
• Not attempted: the hand residue (V), the uniform-in-L forms of (R⁺) and (S≥1), and the independent checker of the reduction.

Reproduce, from scratch_h with the brief’s environment line:

• h282_certify.py U|R|S L all
• h283_symcheck.py L
• h281_cagecheck.py L
• h284_corpus.py L
• h285_summary.py

(U′ at L = 6 was run as h282_certify.py U 6 0,yz,0,0 0,zy,0,0 1,yz,0,0 1,zy,0,0.)