Independent check of Theorem S, Theorem S2, Corollary H, Lemma J, Lemma T′, the repair of Theorem R1 and the law of line fractions (attack proposal of 28 September)
2026-09-28
Verdicts
| # | claim | verdict | one sentence |
|---|---|---|---|
| 1 | Sheet lemma; Lemma T′; the record’s Lemma T is false as stated (counterexample on \(\mathbb{Z}_3 \times \mathbb{Z}_3\)) | CONFIRMED | Every step checks. The counterexample is exact, and it meets the record’s hypotheses as written (‘real functions on the closed lines’), so the author has not misread them. Smaller counterexamples exist on \(\mathbb{Z}_2 \times \mathbb{Z}_2\) (correction 3). |
| 2 | Lemma J (jumps of \(\Phi_S\) are integers when \(\gcd(b,c) = 1\)) | CONFIRMED | The argument is right, including \(g_z = 1\) or \(g_y = 1\) and extents 1 and 2. An exact fit of (C) on 920 (solution, sublattice, axis) triples across 7 cells finds the jumps determined and integral every time, and not defined on cells without the hypothesis. |
| 3 | Theorem S | CONFIRMED | Both cases hold. I redid the line-meeting congruences and enumerated them on 12 cells. My own encoding gives UNSAT on (4,3,3), (5,3,3), (6,2,3), (6,3,4), (5,4,4), (6,2,9) and (7,3,6), and SAT on (3,3,3), (4,4,6) and (2,2,4). (10,4,5) gave no verdict. On 258 solutions of 7 cells with a coprime pair the finer structure has no exception. |
| 4 | Theorem S2, forms \((P_z)\), \((P_y)\), \((Q)\) | CONFIRMED | The proof is right. On every sampled solution of the five cells where it applies, each sublattice has one of the three forms (0 NONE). |
| 5 | Corollary H, and its second proof without Theorem \(M'\) | CONFIRMED WITH CORRECTIONS | The logic is right: the rods are in \(S\) and of two types, and Theorem \(M'\) is used exactly as the note states it. The geometry of \(b_x\), \(b_y\), \(b_z\) in the second proof is right. But the Summary’s ‘needs … no certificate’ is wrong: Theorem \(M'\) rests on finite lemmas with DRAT certificates (correction 1). |
| 6 | Theorem R1 survives with Lemma T′ + Lemma J in place of Lemma T | CONFIRMED | Both uses in R1 (the grids \(Y_q\) and \(Z_p\)) have \(F_x = \Phi(x)\) with \(\gcd(b,c) = 1\). So Lemma J applies, and Lemma T′ gives the same three alternatives (Z1–Z3, Y1–Y3) that R1 uses. |
| 7 | Law of line fractions | CONFIRMED | The derivation from (C) and (S1)-type averaging is right. I checked it exactly with rationals on 495 solutions of 10 non-cubic cells, including (2,2,4), (2,4,6) and (4,4,6), which have no coprime pair, and 28 of (3,3,3), with no violation. In every run the number of states with a fractional line equalled the number of odd states (I compared counts, not state by state). |
No gap was found. The corrections below are about wording and scope. None affects a theorem.
T1. Reading, step by step
Ingredients
- (C): taken as given, as instructed. As a by-product, my least-squares fit of (C) had residual below \(5 \times 10^{-14}\) on every sampled solution of every cell, including cells with no coprime pair. So (C) is consistent with 523 solutions of 11 cells.
- (S1): CONFIRMED. Take a chain of family {0,1} with A-vertices \(p + n(0,2,2)\). It closes after \(2\,\mathrm{lcm}(b,c)\) steps, and a plane of A holds \(2bc\) vertices, so a pair of planes holds \(\gcd(b,c)\) such chains. I walked all chains of all six families on 12 cells, including the thin cells (1,2,3) and (2,1,1). The count per pair of planes equals the gcd of the transverse extents in every case (h430). I also found that a pair of planes \((x_0, x_0+1)\) holds chains of one family only: {0,1} when \(x_0\) is a plane of A, {2,3} when it is a plane of B. So \(\Phi(x_0) = w_{01}(x_0, x_0+1) + w_{23}(x_0-1, x_0)\). This does not affect anything.
- Sheet lemma: CONFIRMED.
- Grids as products (task point a): CONFIRMED.
- On the cover, the vertices of a plane \(z = z_0\) of \(S\) are all of \(\mathbb{Z}^2\) in \((m,n)\).
- The periods are \((a,a)\) and \((b,-b)\), so the chain labels are \(n\) and \(m\) modulo \(\gcd(a,b)\). Every pair of classes occurs trivially.
- I also checked on the torus, by enumerating the chain labels on every plane of every axis of 6 cells (including (1,2,3) and (2,1,1)), that every pair (label of family 1, label of family 2) occurs. The same holds for every coordinate pair \((x,z)\), \((y,z)\) and \((x,y)\) of the parity of \(S\): 0 failures.
Lemma T′
CONFIRMED.
- \(q(m) = [\varepsilon(m+1,n) - \varepsilon(m,n)] - c(m+n)\) is an integer when \(c\) is.
- \(\varepsilon(m,n+1) - \varepsilon(m+1,n) = p(n) - q(m)\) is correct: the \(\gamma\) terms cancel.
- The integer zero-sum argument forces \(q \equiv 0\) once \(p \not\equiv 0\).
- The final use of the sheet lemma is right in both sub-cases. The conclusion ‘γ constant, or α and β constant’ is what Theorem S and R1 need.
The failure of Lemma T (T2)
CONFIRMED by exact rationals (h430).
- With \(\alpha = \beta = (2/3, 1/3, 0)\) and \(\gamma = (-1/3, 0, -2/3)\), \(\varepsilon = 1\) exactly at (0,0), (0,1) and (1,0), and 0 at the six other points. It is not a function of \(i\), of \(j\) or of \(i+j\). The jumps of \(\gamma\) are \(1/3\), \(-2/3\), \(1/3\).
- The record’s hypotheses (route proposal, §3) are ‘\(\varepsilon: \mathbb{Z}^2/\Gamma \to \{0,1\}\) … with \(\alpha, \beta, \gamma\) real functions on the closed lines’. \(\mathbb{Z}_3 \times \mathbb{Z}_3\) with \(\Gamma = 3\mathbb{Z} \times 3\mathbb{Z}\) is such a torus. So Lemma T is false as stated, and the author’s reading is right.
- The faulty step is the one the author names: ‘\(a\) takes a value \(\geq 1\) and a value \(\leq -1\)’ holds only for integer \(a\).
- By enumeration, the 0/1 functions in the tri-separable span that are not functions of one of \(i\), \(j\), \(i+j\) number 8 on \(\mathbb{Z}_2^2\), 36 on \(\mathbb{Z}_3^2\) and 96 on \(\mathbb{Z}_4^2\) (correction 3).
Lemma J
Task point b. CONFIRMED. Redone:
- Since \(c(k_0) - q(m) \in \mathbb{Z}\) for all \(m\) (take \(n = k_0 - m\)), every \(q(m) \equiv \theta\). Then every \(c(k) \equiv \theta\).
- Each has zero sum over its period (period \(2a\) for \(c\), \(g_z\) for \(q\)) and no integral value. So each has a value \(\geq \theta\) and a value \(\leq \theta - 1\).
- \(\max c \leq 1 + \min q \leq \theta\) and \(\min c \geq \max q - 1 \geq \theta - 1\). So both take only the values \(\theta\) and \(\theta - 1\).
- Then \(g_z \theta \in \mathbb{Z}\). On a plane \(y = y_0\) the same jumps \(c\) occur, because \(x\) runs over every value of the parity of \(S\) there too, with \(-c\) in place of \(c\). That gives \(g_y \theta \in \mathbb{Z}\).
- \(\gcd(g_y, g_z) = \gcd(a,b,c)\), which divides \(\gcd(b,c) = 1\).
Edge cases:
- \(g_z = 1\): \(Q\) is constant, so \(q = 0 \not\equiv \theta\). The contradiction is immediate, which the argument covers.
- Thin cells: \(a = 1\) gives \(\gamma\) period 2. \(b = 1\) or \(c = 1\) gives \(g = 1\). Nothing breaks.
- Observation (not a gap): the last step needs only \(\gcd(a,b,c) = 1\). \(\gcd(b,c) = 1\) enters Lemma J only through (S1).
Numerical check (h432). I solved (C) by least squares on each sampled solution and computed the null space. For each jump \(\Phi_S(x+2) - \Phi_S(x)\) I tested that it is orthogonal to the null space, so it is determined by the solution, and that it is integral. Result: \(\Phi_S\) well defined, jumps determined and jumps integral in 920 of 920 (solution, sublattice, coprime axis) cases. The cells were (6,2,3), (4,3,3), (6,3,4), (2,1,3), (1,2,3), (6,2,1) and (2,3,2), on every axis with coprime transverse extents. As a control, on (4,4,6) and (3,3,3) \(\Phi_S\) is not a function of the plane: 0 of 276 well defined.
Theorem S
Absorption of constants (task point d): CONFIRMED.
- On \(S\), put \(\Phi_S := \Phi + \sigma_S\alpha\) and absorb \(\sigma_S(\alpha+\beta)\) into \(F_y\).
- This is legitimate because every later use of \(F_y\) and \(F_z\) is through their separable form on planes of \(S\), where adding a constant keeps the form.
- The jumps of \(\Phi_S\) do not change.
Case 1: CONFIRMED.
- Lemma T′ applies on each plane \(z = z_0\), with \(\alpha = -P\), \(\beta = -Q\) and \(\gamma\) non-constant. \(\gamma\) is non-constant because \(x\) runs over every value of the parity of \(S\) on that plane. So \(P\) and \(Q\) are constant on the plane.
- The sheet lemma on the full product (x, z) forces \(\kappa\) constant. The same holds for \(\kappa'\).
- The two-value argument gives \(\kappa' = \kappa + 1\), so \(X = 0\) on \(S\), and each \(x\)-plane is all \(y\) or all \(z\).
Case 2 (task point c): CONFIRMED. I redid the congruences.
- The equations are:
- \(2t - 2s \equiv -d_x \pmod{4a}\)
- \(2\epsilon t \equiv -d_y \pmod{4b}\)
- \(-2\epsilon' s \equiv -d_z \pmod{4c}\)
- They fix \(t\) modulo \(2b\) and \(s\) modulo \(2c\). Then \(t - s\) runs over a coset of \(2\gcd(b,c)\mathbb{Z} = 2\mathbb{Z}\).
- Its parity is that of \((d_y + d_z)/2\), and the target \(-d_x/2\) has the same parity because \(d_x + d_y + d_z \equiv 0 \pmod 4\). So a solution modulo \(2a\) exists.
Enumeration (h430): every line \(q + t(2, \pm 2, 0)\) of \(S\) was tested against every line \(r + s(2, 0, \pm 2)\) of \(S\), on both sublattices:
| cells | \(\gcd(b,c)\) | pairs of lines that do not meet |
|---|---|---|
| (6,2,3), (6,3,4), (4,2,3), (2,1,3) | 1 | 0 |
| (4,3,3), (5,3,3), (3,4,4) | 3, 3, 4 | 0 |
| (3,3,3) | 3 | 864 |
| (4,4,6) | 2 | 1536 |
| (2,2,4) | 2 | 256 |
| (4,2,4) | 2 | 512 |
| (6,3,6) | 3 | 3456 |
The lines meet exactly when \(\gcd(a,b,c) = 1\) (observation, correction 2).
Theorem S2
CONFIRMED.
- \(F_y = \Upsilon(y)\) needs \(\gcd(a,c) = 1\) and \(F_z = \mathrm{Z}(z)\) needs \(\gcd(a,b) = 1\), both from (S1).
- The sheet lemma on the full product (y, z) makes \(X\) a function of \(z\) alone or of \(y\) alone.
- In \((P_z)\), \(Z = \mathrm{const} - F_x\) on \(S\). On each \(x\)-plane (a full product of the two families’ labels) it is constant along one family.
- The line \(z = z_1\) of an \(x\)-plane has points 4 apart in \(y\) with \(y - z\) and \(y + z\) running over all classes modulo \(4\gcd(b,c)\), so it meets every chain of both families. Hence \(Z = 0\). \((P_y)\) and \((Q)\) follow the same way.
- The notation ‘$Z = - F_x + $ const’ is consistent with $(y) = F_y + $ const, with \(\upsilon\) constant.
Corollary H
Task point e. CONFIRMED.
- The rods of a hole \(O\) are its methylenes \(O \pm 2e_k\), which lie in the sublattice of \(O\). A rod on axis \(k\) has type \(k\). A corner has rods on two axes, so on \(S\) there are two types \(j \neq k\).
- Theorem S makes \(S\) lack a type, necessarily the third type \(i\).
- Theorem \(M'\) as stated in the note (line 455: ‘a frozen state in which one sublattice has no vertex of type \(k\) and the other has one has even curl’, extended to every cell in the subsection on non-cubic cells and by check6 §1) is exactly the form used.
- ‘Odd ⇒ some corner’ is the forward half of Lemma 1. I checked that it holds when an extent is 1, where \(O + 2e_x = O - 2e_x\). \(N(O,\sigma) = 2\) still puts two rods of distinct axes in one octant.
- Sampling agrees. Every odd state sampled on a cell with a coprime pair lacks a type. On (6,2,3), (6,3,4), (6,2,1) and (2,3,2) the absent type is the one Theorem S names. On (4,3,3) it is always \(x\), as the corollary of S2 says.
- Scope correction (correction 1): Theorem \(M'\) is not certificate-free.
Corollary of Theorem S2 without Theorem M′
Task point f. CONFIRMED.
- \(O' = O + \sigma\) is a B-hole when \(O\) is an A-hole, since \(\sigma\) has product \(+1\) and is one of the \(d_k\).
- \(b_k = O' - 2\sigma_k e_k \in S'\). \(N(O', -\sigma) = 0\) says \(\tau(b_k) \neq k\).
- \(b_x\) and \(b_y\) both have \(z = z_{O'}\), and \(b_x\) and \(b_z\) both have \(y = y_{O'}\). So \((P_z)\) and \((P_y)\) on \(S'\) each lead to a contradiction.
- The step ‘a corner of \(S\) cannot have a rod of type \(x\)’ uses that the two rods of a corner share the coordinate of the axis neither of them lies on. That is correct.
Theorem R1 with Lemma T′ and Lemma J
CONFIRMED.
- R1 has exactly the hypothesis \(\gcd(b,c) = 1\).
- Its grids \(Y_q = \{y = 2\}\) and \(Z_p = \{z = 0\}\) are planes of A, with \(\gamma(i+j) = X(x)\), the restriction \(\Phi_A\). So Lemma J gives integral jumps.
- Lemma T′’s three alternatives are functions of \(i\), of \(j\) and of \(i+j\), which are the directions \((2,0,-2)\), \((2,0,2)\) and \((0,0,4)\) on \(Y_q\). Those are R1’s Z1, Z2 and Z3, and likewise Y1, Y2 and Y3.
- Steps 2–4 of R1 do not use Lemma T.
- R1 is stated for frozen states, whose types solve the type model, so Lemma J applies.
Law of line fractions
CONFIRMED.
- Averaging \(F_x\) along a \(y\)-line: the label \(y - z\) modulo \(4g_x\) of the {0,1}-chain runs uniformly over its \(g_x\) classes, since \(g_x \mid b\). The {2,3}-chain behaves likewise. The average is therefore the mean chain weight of the two pairs of planes through \(x\): a function \(P(x)\). Along a \(z\)-line the average is the same \(P(x)\), since \(g_x \mid c\).
- \(F_z\) along a \(y\)-line gives \(R(z)\), and \(F_y\) along a \(z\)-line gives \(Q(y)\).
- With the constants absorbed per sublattice (\(P_S = P + \sigma\alpha\), \(Q_S = Q + \sigma(\alpha+\beta)\)), the three formulas and their sum 1 follow.
- ‘Even curl exactly when every fraction is 0 or 1’: forward by Lemma 1. Backward because a type-\(k\) vertex on an all-\(k\) line makes both rods of each adjacent hole lie on that line, so there is no corner and, by Lemma 1, no odd hexagon.
- In every one of my samples the number of states with a fractional line equalled the number of odd states.
T3. Computations
Every command was run from scratch_h with the project .venv, PYTHONPATH and TMPDIR as instructed. Every SAT query went through h32_cap (one or run_batch), one process at a time, with a cap of at most 300 s per query. The scripts are my own:
h430_geom.py: exact geometry, the Lemma T counterexample and search, (S1), line meeting, products.h431_sl.py: Theorem S by solver.h432_sample.py: sampling, finer structure, the law, and the (C) fit for Lemma J.
They import only icemix.lattice, a4_typemodel.TypeModel (one-hot + (T2)) and h32_cap. I did not read or import h420–h423. Every SAT model from h431 was re-checked against (T2) in Python.
Encodings of the negation of Theorem S (‘A has a vertex of each type’), by translation and the half-turns
- plain: the origin has type \(x\), and A has a \(y\) and a \(z\).
- pair: A is FCC-connected, so two FCC-neighbours of A with different types exist. Translate one to the origin. The half-turns \(R_x\), \(R_y\), \(R_z\) (which preserve A, the bonds and the types) together with the reversal reduce \(\delta\) to \((2,2,0)\), \((2,0,2)\) or \((0,2,2)\) and the ordered pair of types to \(xy\), \(xz\) or \(yz\). The third type must then occur on A. That gives 9 queries whose disjunction is the negation.
- Law C was added as a redundant cardinality constraint. It is a sum of (T2), so it is sound.
- Controls:
- plain: the same query without one of the ‘A has’ clauses. These must be SAT and were SAT on every cell.
- pair: the same query without the third type. Four of these controls came out UNSAT: (4,3,3) pair 0 and 4, (6,2,9) pair 8, (7,3,6) pair 0 and 4. That is predicted:
- an \(x\) next to a \(y\) along a \(z\)-plane diagonal is impossible under \((P_z)\) of S2;
- a \(y\) next to a \(z\) inside an \(x\)-plane is impossible under Theorem S (i).
| command | tested | verdict | wall |
|---|---|---|---|
h430_geom.py |
Lemma T counterexample and search on \(\mathbb{Z}_n^2\), \(n = 2,3,4\); (S1) on 12 cells; line meeting on 12 cells; products on 6 cells | as reported above | 2.8 s |
h431_sl.py 4,3,3 plain --cap 120 |
SL, controls | UNSAT 4.6 s; controls SAT | 6.4 s |
h431_sl.py 4,3,3 plain --lawc --cap 120 |
the same with Law C | UNSAT 4.0 s; controls SAT | 5.0 s |
h431_sl.py 4,3,3 pair --lawc --cap 120 |
9 pair queries | 9 UNSAT (1.1–4.1 s); controls 7 SAT, 2 UNSAT (predicted) | 24.7 s |
h431_sl.py 5,3,3 plain --lawc --cap 120 |
SL | UNSAT 10.5 s; controls SAT | 11.9 s |
h431_sl.py 6,2,3 plain --lawc --cap 120 |
SL | UNSAT 2.4 s; controls SAT | 3.5 s |
h431_sl.py 3,3,3 plain --lawc --cap 120 |
negative control | SAT 0.1 s (model: all three types on A and B, (T2) ok) | 1.3 s |
h431_sl.py 4,4,6 plain --lawc --cap 120 |
negative control | SAT 1.3 s (the same) | 2.4 s |
h431_sl.py 2,2,4 plain --lawc --cap 120 |
negative control | SAT 0.2 s (the same) | 1.4 s |
h431_sl.py 6,3,4 plain --lawc --cap 250 |
SL | UNSAT 37.2 s; controls SAT | 38.4 s |
h431_sl.py 5,4,4 plain --lawc --cap 300 |
SL | UNSAT 198.3 s (the author had no verdict at 120 s); controls SAT | 199.4 s |
h431_sl.py 6,2,9 plain --lawc --cap 300 |
SL | no verdict (cap 300 s); controls SAT | 301 s |
h431_sl.py 6,2,9 pair --lawc --cap 150 --only 0,1,2 |
pair 0–2 | UNSAT 38.0, 86.2, 31.7 s; controls SAT | 158 s |
… 6,2,9 … --only 3,4,5 |
pair 3–5 | UNSAT 55.9, 30.3, 40.5 s; controls SAT | 129 s |
… 6,2,9 … --only 6,7,8 |
pair 6–8 | UNSAT 63.5, 75.3, 14.7 s; controls SAT, SAT, UNSAT (predicted) | 170 s |
| (6,2,9) SL: UNSAT (all 9 cases) | |||
h431_sl.py 7,3,6 pair --lawc --cap 180 --only 0,1,2 |
pair 0–2 | pair 0 UNSAT 94.9 s (control UNSAT 64.5 s, predicted); pair 1 and 2 no verdict (cap 180 s) | 521 s |
… 7,3,6 … --cap 280 --only 1 |
pair 1 | UNSAT 212.8 s; control SAT | 214 s |
… 7,3,6 … --cap 280 --only 2,3 |
pair 2–3 | UNSAT 251.8, 126.6 s; controls SAT | 380 s |
… 7,3,6 … --cap 280 --only 4,5 |
pair 4–5 | UNSAT 72.2 s (control UNSAT, predicted), UNSAT 252.0 s | 395 s |
… 7,3,6 … --cap 280 --only 6,7 |
pair 6–7 | UNSAT 165.7, 220.7 s; controls SAT | 388 s |
… 7,3,6 … --cap 280 --only 8 |
pair 8 | UNSAT 118.3 s; control SAT | 120 s |
| (7,3,6) SL: UNSAT (all 9 cases) | |||
h431_sl.py 10,4,5 pair --lawc --cap 280 --only 0 |
pair 0 | UNSAT 147.7 s; control SAT | 150 s |
… 10,4,5 … --only 1,2 |
pair 1–2 | pair 1 no verdict (cap 280 s); pair 2 UNSAT 168.0 s | 449 s |
… 10,4,5 … --only 3,4 |
pair 3–4 | pair 3 no verdict (cap 280 s); pair 4 UNSAT 175.3 s | 457 s |
| (10,4,5) SL: no verdict (4 cases UNSAT, 2 capped, 3 not run) | |||
h432_sample.py 6,2,3 30 1 --cap 120 (run twice, the second time with the non-vacuity count) |
sampling, S structure, law, Lemma J | 20 solutions; see below | 2.5 s |
h432_sample.py 6,2,3 60 2 --odd --cap 120 |
the same, with odd hexagons | 21 solutions, all odd | 4.7 s |
h432_sample.py 4,3,3 60 3 --cap 120 |
the same, plus S2 | 36 solutions | 14.1 s |
h432_sample.py 4,3,3 60 4 --odd --cap 120 |
the same, odd | 11 solutions | 36.8 s |
h432_sample.py 6,3,4 60 5 --cap 150 (run twice, the same) |
the same | 45 solutions | 57 s |
h432_sample.py 6,3,4 40 6 --odd --cap 150 |
the same, odd | 16 solutions | 83 s |
h432_sample.py C 40 7 and … 40 8 --odd for C = (2,1,3), (1,2,3), (6,2,1), (2,3,2), run twice (the second time for the Lemma J lines) |
thin cells | 22+0, 24+0, 27+4, 28+4 solutions. With --odd, all 40 queries were UNSAT on the pairwise-coprime (2,1,3) and (1,2,3), consistent with R1 |
under 1 s each |
h432_sample.py C 40 9 and … 40 10 --odd for C = (2,2,4), (2,4,6), (4,4,6) |
law on cells with no coprime pair | 36+35, 38+34, 37+39 solutions | 0.5 s to 61 s |
h432_sample.py 4,4,6 30 11 --odd --cap 150 --forceaxes --sanity |
sanity: checks where the hypotheses fail; law and (C) on random fields | 18 solutions; 9 sampling queries capped (the batch cap), which is not a result | 155 s |
h432_sample.py 3,3,3 30 12 --odd --cap 100 --forceaxes |
sanity on a cubic cell | 28 solutions | 1.4 s |
Finer structure on sampled solutions
The cells have a coprime pair. For each axis \(k\) whose transverse extents are coprime I applied Theorem S with \(k\) in the role of \(x\). The case prediction (\(\Phi_S\) non-constant) was read off the line fractions: \(h_i/\ell_i\) depends on \(x_k\).
| cell (axes tested) | solutions | (sol, sublattice, axis) triples | S holds | case 1: (i) holds | case 2: lines in a chain direction for both types, and S lacks \(i\) or \(j\) | S2 forms (axis) |
|---|---|---|---|---|---|---|
| (6,2,3) (\(x\)) | 41 | 82 | 82 | 22/22 | 60/60 | – |
| (4,3,3) (\(y\), \(z\)) | 47 | 188 | 188 | 45/45 | 143/143 | 26 \((P_j)\), 19 \((P_i)\), 49 \((Q)\), 0 NONE (\(x\)) |
| (6,3,4) (\(x\)) | 61 | 122 | 122 | 36/36 | 86/86 | – |
| (2,1,3) (all) | 22 | 132 | 132 | 43/43 | 89/89 | 0 NONE (every axis) |
| (1,2,3) (all) | 24 | 144 | 144 | 46/46 | 98/98 | 0 NONE |
| (6,2,1) (\(x\), \(y\)) | 31 | 124 | 124 | 34/34 | 90/90 | 0 NONE (\(z\)) |
| (2,3,2) (\(x\), \(z\)) | 32 | 128 | 128 | 34/34 | 94/94 | 0 NONE (\(y\)) |
The first three rows have at least 20 distinct solutions each, diversified by random type assumptions on 1–3 vertices of each sublattice and, in the --odd runs, an odd selector on a random hexagon.
Exceptions: none.
Non-vacuity:
- In case 1 the chain-line test fails (22/22 on (6,2,3), 36/36 on (6,3,4)), as it should, since the \(y\)-set there is a union of lines $x = $ const.
- With
--forceaxeson (4,4,6) and (3,3,3), where no hypothesis holds, Theorem S fails for 92 of 108 and 160 of 168 triples, and S2 gives NONE on most sublattices.
Law of line fractions
Exact, with fractions.Fraction. The checks were:
- \(f_y\) separable as \(P(x) - R(z)\);
- \(f_z + P(x)\) a function of \(y\) alone;
- \(f_x = 1 + R - Q\);
- \(f_x + f_y + f_z = 1\) at every vertex.
| cells | solutions satisfying the law |
|---|---|
| (6,2,3), (4,3,3), (6,3,4), (2,1,3), (1,2,3), (6,2,1), (2,3,2) (coprime pair) | 258/258 |
| (2,2,4), (2,4,6), (4,4,6) (no coprime pair) | 237/237, including 18 from the --forceaxes run |
| (3,3,3) (cubic) | 28/28 |
That is 495 solutions on 10 non-cubic cells with 0 violations. Sanity: 3 random type fields on (4,4,6) violate the law (20 violations each) and fit (C) with residual about 1.
(S1) by enumeration of chains
Done on 12 cells (h430), not just four: (4,3,3), (5,3,3), (6,2,3), (6,3,4), (5,4,4), (4,2,3), (3,3,3), (4,4,6), (2,2,4), (1,2,3), (2,1,1) and (7,3,6). For all six families the number of chains per pair of planes equals the gcd of the transverse extents.
Corrections and gaps
No gap.
- Summary item 2 (‘This needs no \(K_u\), no Theorem U, no Theorem R1 and no certificate’) is wrong in its last clause. Corollary H uses Theorem \(M'\). Theorem \(M'\) is proved (note, line 460; check6 §1) with finite lemmas on four hexagons that carry DRAT certificates: PLAQ_K, K4 and, for the first proof, PLAQ_C and EDGE_X. The certificates are window lemmas that pull back to every torus, so they do not limit the scope, but the corollary is not certificate-free. The route through Theorem S2 is free of \(M'\) and of certificates, but only on cells with \(\gcd(a,b) = \gcd(a,c) = 1\).
- Scope observation (not an error). In Case 2 of Theorem S the two lines meet whenever \(\gcd(a,b,c) = 1\): enumerated on (4,3,3), (5,3,3) and (3,4,4), where \(\gcd(b,c) \geq 3\). The last step of Lemma J likewise needs only \(\gcd(g_y, g_z) = \gcd(a,b,c) = 1\). The hypothesis \(\gcd(b,c) = 1\) is used essentially only through (S1), which is what makes \(F_x\) a function of the plane. The proof as written is correct. This locates what fails on cells without a coprime pair: (S1), not the meeting.
- The counterexample to Lemma T can be smaller. On \(\mathbb{Z}_2 \times \mathbb{Z}_2\) every 0/1 function is tri-separable (the span has rank 4). For example, \(\varepsilon = \delta_{(0,0)}\) with \(\alpha = \beta = (1/2, 0)\) and \(\gamma = (0, -1/2)\). Exhaustively, the failing 0/1 patterns number 8, 36 and 96 on \(\mathbb{Z}_2^2\), \(\mathbb{Z}_3^2\) and \(\mathbb{Z}_4^2\). The author’s \(\mathbb{Z}_3\) example is correct. The record should say that Lemma T fails on every square torus tried, and that its proof is right only for integer jumps.
- Minor (wording in the S2 proof). ‘$Z = - F_x + $ const’ is correct but relies on the reader identifying \(\upsilon\) with \(F_y\) up to a constant. It would read more safely as ‘\(Z = F_y - F_x + \sigma\beta\), and \(F_y\) is constant on \(S\)’.
- Thin cells (the author’s caveat 4) are not a problem for any step I read:
- (T2) is taken on the lattice-derived hexagons of
lattice.build, which raises on a degenerate hexagon and did not on (1,2,3), (2,1,3), (6,2,1) or (2,3,2). - Lemma 1’s forward direction survives \(O + 2e_x = O - 2e_x\).
- Every structural claim held on the thin-cell samples.
- (T2) is taken on the lattice-derived hexagons of
What I could not check
- Theorem S by solver on (10,4,5): no verdict. Of the 9 pair cases, 4 were UNSAT, 2 hit the 280 s cap and 3 were not run once a verdict was impossible.
- Completeness (C) itself, Theorem \(M'\), Lemma A and Theorem P were taken from the record as instructed. My (C) fits are consistent with (C) on 523 solutions but are not a proof.
- ‘What this does to the record’, item 4 (the LP of (V) positive on (5,3,3) and (5,4,4)): not re-run.
- The corpus statistics of ‘What is left’ and package B: not re-run.
Rules
I believe none was broken:
- Every solve went through
h32_cap, one process at a time, with caps of at most 300 s. The longest command took 521 s. - There were no heredocs and no writes to /tmp.
- No existing file was modified. I edited only my own new
h432_sample.py, between runs. - There were no git operations.
- Neither Theorem H nor ‘odd and all six directions’ was run. The sampling used ‘some hexagon odd’ as an assumption only, with no condition on directions or types.
- One point is borderline: the six-minute pair runs on (7,3,6) and (10,4,5) were not preceded by a separate timing of a smaller instance of the same cell. The pre-flight was the (6,2,9) pair runs and a capped first batch on (7,3,6).