Check of the zeroflux report: Theorem U implies Theorem H on every cell without K_u. Verdict CONFIRMED, with wording corrections; every step is within the hypotheses of the note’s theorems, the corpus checks re-run by independent code with 0 exceptions, and the solver finds no oriented frozen state with six directions on both sublattices at (3,3,3) or (2,2,4)

Scripts scratch_h/h670–h672, written before reading h600–h605 and importing nothing from them. h600_stripes.py was opened once, after the verdict, only to see how it counts lines.

Verdict

CONFIRMED. Lemmas Z-1 to Z-4, Theorem Z-5 and Corollary Z-6 hold as stated. Every theorem of the note that they invoke is applied within its hypotheses. On every cell they give: an odd frozen state with every hole oriented has an axis that is empty or one-way. So Theorem U implies Theorem H on every cell, and \(K_u\) is not needed for the reduction. No gap was found. The corrections below are to wording and bookkeeping and do not touch the argument.

1. Hypotheses used lists Theorem 7 as not used, but case III of Lemma Z-2 reuses the argument of Theorem 7’s second case. Better wording: “the wall of Theorem 7 is not used; case III repeats the argument of its second case, which uses Theorems 3 and 5 and not oddness”.
2. Small extents. The lemmas are local identities (Lemma 3, \(P^k\), Theorem 9 on the lift) summed along lines, so they hold on every torus. On a cell with an extent of 1, the methylenes \(O \pm 2e_k\) coincide. The clean way to cover it is Lemma 21: a periodic repetition preserves frozenness, oddness, the moments, the type sets of each sublattice, which axes are two-way, and the charge of every hole, provided the charge is counted over the six methylene positions. Z-5 and Z-6 on a small cell therefore follow from the same statements on a cell with every extent at least 2. The report should say this in one sentence rather than leave “every cell” implicit.
3. Corollary Z-6 inherits Theorem \(M'\)’s standing on non-cubic cells. The note gives this as confirmed on every cell by a second reader, and at extent 2 as argued from lemmas on the infinite lattice and tested by solver. The report should cite that standing and not simply say “proved on every cell”.
4. The corpus contains 68 repeated type fields (7 at \(L = 3\), 61 at \(L = 4\)), so it has 1,289 distinct states. The report’s counts (1,357 states, 1,001 with three types, 429 in the table of normals) are counts with repetitions. My counts, also with repetitions, agree exactly.
5. Z-4 needs Theorem 3 only (two applications through a neighbouring vertex), as the report says. Z-2 case I needs the named planes to be non-empty only, because Z-1 makes every non-empty plane full.

Re-derivation with hypotheses

Notation: for axis \(k\) and sublattice \(S\), the \(k\)-lines of \(S\) are indexed by the pairs \((\alpha, \beta)\) of transverse coordinates of the parity of \(S\). Every such pair is a line, because for even \(\alpha\) and \(\beta\) the third coordinate is fixed modulo 4, and likewise for B. So the line functions live on a full product \(X_S \times Y_S\) on every cell. Theorem 5 and Lemma 4 need this.

Z-1. \(S\) two-way on \(k\). \(P = (h+s)/2\) and \(Q = (h-s)/2\) count the two signs. - \(h\) is separable by Theorem 5, first statement. This holds in every frozen state. - \(s\) is separable by Theorem 5, second statement. It needs every hole of the \(k\)-hole-lines of \(S'\) oriented; U supplies this. - \(PQ = 0\) by Theorem 4. It needs the holes of the line and of the Theorem 3 diamonds oriented; U supplies this. Theorem 3 holds at every separation on every torus, by the lift argument after Theorem 9. Theorem 4’s bridgeheads lie on four distinct neighbouring lines, since \(\alpha \pm 1\) differ by 2 modulo \(4a \geq 4\). - Lemma 4 needs \(P\) and \(Q\) non-negative and neither identically zero. Both signs occur on \(S\) (two-way), so this is supplied. - Conclusion: both \(P\) and \(Q\) are functions of one coordinate \(x_n\), so \(h\) is as well, and on each plane at most one of \(P(c)\) and \(Q(c)\) is positive. - The normal is unique. If \(P\) were also a function of the other coordinate it would be constant. With \(PQ = 0\), one of \(P\) and \(Q\) would then vanish identically, which is excluded.

1. Both theorems hold on every cell under “every hole oriented” as the note proves them, and the non-vanishing condition of Lemma 4 is supplied. Answer: yes.

Z-2, with \(k\) two-way globally and carried by both sublattices. - Case I (both sublattices two-way). The normals are \(n\) for A and \(m\) for B; suppose \(m \neq n\). Then \(\{n, m\}\) are exactly the two transverse axes. A has a non-empty plane \(x_n = c\) of sign \(+\) (with \(c\) even), and B has a non-empty plane \(x_m = d\) of sign \(-\) (with \(d\) odd). Both are full by Z-1. - The pair \((c+1, d)\) is odd-odd, so it is a B-line, and it exists on every cell. Its transverse offset from the A-lines \((c, d \pm 1)\) is \((-1, \pm 1)\), so they are diagonal neighbours. Those A-lines lie in the full A-plane \(c\). - Theorem 3 (U) then gives a contradiction. Only non-emptiness of the two planes is needed. - Adjacent planes: a B-line \((c \pm 1, \beta)\) neighbours the A-line \((c, \beta + 1)\), which is non-empty when the A-plane is. - Case II (A two-way, B of one sign \(\sigma\)). A has a full plane \(c\) of sign \(-\sigma\). By Theorem 3, every B-line at \(x_n = c \pm 1\) is empty. - \(h^B\) is separable (Theorem 5, first statement), non-negative and not identically zero, with a zero. So its zero set is the product of the argmins, \(I \times J\). - The zero set contains \(\{c \pm 1\} \times Y_B\), so \(J = Y_B\) and \(G\) is constant. - So \(J = Y_B\) follows, \(h^B\) is a function of \(x_n\), and its non-empty planes are full, with the same count on each line. - The sign statement is immediate, because B has one sign and the planes next to \(-\sigma\) planes of A are empty. - Case III (A of sign \(\sigma\), B of sign \(-\sigma\)). I re-derived Theorem 7’s second case as written; it uses only Theorems 3 and 5. - The empty set of A is a non-empty product. If both factors were proper, a full column and a full row of A would empty the two neighbouring columns and rows of B. B’s empty set would then be the whole product, but B carries \(k\). - So the empty lines are complete planes of one normal, and \(h^A\) is a function of it. The same holds for B. - The normal is common, by the Case I argument, which needs only that the two full planes carry opposite signs. - Full planes of A and B are never adjacent. - This is exactly what Z-2 uses, with the same normal for both sublattices. Oddness, the hypothesis of Theorem 7, is not used in this case. - Exhaustiveness. Each sublattice carries \(k\), so each is two-way or one-signed. Two one-signed sublattices of the same sign would make \(k\) one-way, so the cases (TW,TW), (TW,OS) up to exchange, and (OS,OS) with opposite signs cover everything. Answer (b): the named lines are diagonal neighbours; the B-line exists for every choice; non-empty suffices; \(J = Y_B\) follows; Theorem 7’s second case gives a common normal; the cases are exhaustive.

Z-3. Theorem 15 holds in every solution of the type model on every cell, with the same \(P\), \(Q\), \(R\) in all three identities. \(h_x/\ell_x = 1 + R(z) - Q(y)\) holds on all pairs \((y, z)\) of the parity of \(S\), and every such pair occurs (see Notation). So independence of \(z\) forces \(R\) to be constant on the \(z\)-values of \(S\), and likewise for the other axes. I checked all six (k, n) combinations: \(i(k)\) is the axis outside \(\{k, n(k)\}\). - The image of \(i\) cannot be a single axis, because \(i(k) \neq k\). - If the image contains \(a\) and \(b\), the \(h_c\) formula involves only the profiles of \(a\) and \(b\), so \(h_c\) is constant. - The normals are common to A and B by Z-2 (all three cases), so the image and \(c\) are common.

Answer (c): yes on every cell; the non-constancy exclusion is correct; the common normal is supplied by Z-2.

Z-4. The \(k\)-lines of both sublattices are the pairs \((\alpha, \beta)\) modulo \((4p, 4q)\) with \(\alpha \equiv \beta \pmod 2\). The steps \((1,1)\) and \((1,-1)\) generate that index-2 lattice in \(\mathbb{Z}^2\), and hence its image on the torus. So the graph is connected for all extents, including 1 and 2, where each line still has its four distinct neighbours. Theorem 3 applied twice, through a vertex of a neighbouring line (every line is non-empty), gives one sign. Answer (d): yes.

Z-5. Suppose all three axes are two-way. Z-2 applies to each \(k\), since both sublattices carry \(k\) by hypothesis. Z-3 then gives an axis \(c\) with \(h^A_c\) and \(h^B_c\) constant, at least 1 because each sublattice has a type-\(c\) vertex on some line. Z-4 makes \(c\) one-way, which is a contradiction.

Z-6. In an odd frozen state with every hole oriented, if some type is absent its axis is empty. Otherwise every type occurs somewhere. - The contrapositive of \(M'\) (“one sublattice lacks \(k\) and the other has it” implies even curl) applies to an odd state, with its hypotheses exactly. So both sublattices carry all three types. - Z-5 then gives an axis that is not two-way; it is non-empty, so it is one-way.

Answer (e): \(M'\) is used within its hypotheses. At extents 1 and 2, see corrections 2 and 3. The argument itself never forms a hexagon or chain that could wrap (hexagon vertices span at most 3 in each coordinate and are distinct modulo 4). The Z(L) clause relies on Corollary Z of the signed report, which I did not re-check; it is not needed for H.

(f) Hidden uses. There is no use of cubic geometry. The classification of normals into two classes “under the symmetries of the cubic cell” is commentary, not proof. There is no use of \(K_u\), walls, Lemma 5, Theorem 8 or \(W = 0\). Oddness is used only through U (as its hypothesis) and \(M'\). Theorem 15 and Theorem 5’s first statement are type-model facts. Theorems 3 and 4 and Theorem 5’s second statement are where orientation enters, as the report’s “Where U enters” says.

Computational checks

h670 rebuilds the geometry from site positions: A is the sublattice with all coordinates even, bonds are the \(\{\pm1\}^3\) offsets, holes are \(S + (2,0,0)\). It derives the signs from the types by the bond rule (BFS). For each state it checks (T2) on every hexagon and Law C, computes corners (oddness) and charges, and then the tables below. The signs agree up to global reversal with icemix.cnf.dipole_field on all 132 states stored as bond integers.

Prediction on normals (three-type states, one-way axis \(c\), two-way \(a\), \(b\)). I re-derived it: if \(i(a) \neq i(b)\), the constant axis must be \(c\), forcing \(n(a) = n(b) = c\); otherwise \(i(a) = i(b) = c\) and \((n(a), n(b)) = (b, a)\). The corpus has only the second:

These agree exactly with the report’s counts (1,723 / 91 / 0 cases, 1,814 axes, 499 full axes, 12,895 adjacent pairs, 3,537 instances, 152 / 138 / 139). The report’s larger line and plane counts (414,072; 17,800) are a different bookkeeping (it counts all lines, or only non-empty planes), not a disagreement.

Solver (h671). The model is the icemix bond model with ice clauses and frozen clauses under a selector. The script adds: - direction indicators \(D_{v,k,\pm} \leftrightarrow\) (the set pair of \(v\) is the pair of that direction), with both directions of the definition; - orientation: at every hole, no two methylenes both pointing away and no two both pointing towards. With Law C (two rods in a frozen state) this is exactly charge 0.

The encoding was tested (h672): all 18 bond-integer corpus states of (3,3,3) satisfy ice + frozen + orientation. Each query ran in its own h32_cap child with a 120 s cap, one at a time. SAT models were decoded and checked by h670’s code.

Controls: - Q’s drop-one control C4 is satisfiable and was checked: frozen by (T2) and Law C, every hole oriented, odd, all three types and five directions on each sublattice. - Q′ is UNSAT where it finished. The note predicts this: H is proved at (2,2,4) by Theorem 23 and at (3,3,3) by Theorem 24, and Z-7 excludes even states. So “drop orientation” is not a satisfiable control, contrary to the brief’s suggestion, and C4 replaces it. - No SAT result contradicts the record. - C2 is a side observation, not used: at these two cells no frozen state with every hole oriented, of either curl, has all six directions.

Disagreements with the report

None of substance. The report is right that only U enters through Theorems 3 and 4 and through Theorem 5’s second statement. The wording points are in the Verdict (1 to 5).

Scripts and timings

Rules kept or broken

Kept: - Computed from scratch_h with the project .venv, the prescribed PYTHONPATH and TMPDIR. - New scripts h670–h672 only; nothing existing modified; no git. - No import from h600–h605, and h600_stripes.py read only after the verdict. - One solver process at a time, each query in an h32_cap child capped at 120 s, no job over 10 minutes, nothing on the Sparks or through expq. - Every UNSAT paired with a satisfiable control.

Broken: none. One deviation from the brief: the suggested control “drop orientation” is itself UNSAT by the record (H and Z-7), so the drop-one control used is C4 (five directions).