(V) at g = 2 (agent gtwo): the linear programme is positive on every slab and on every cell whose rod axis has even length, and exactly 0 on every cell with odd rod-axis length tested, so at g = 2 the integrality is a parity-type step along the rod axis that a closed odd x-circle supplies linearly; the thinnest integral family found that is uniform in the geometry of the pattern is one x-chain, the chain next to the rod’s chain in the slab of the rod and the lower bridgeheads, and the same family closes at g = 3 and 4; the case split lives on a contiguous run of that chain beside the cage, lengthens with the torus, and is a caterpillar only on the thinnest tori; the degree-two Sherali-Adams lift refutes (V) on the slab over (2,2) and (2,4), gave no verdict on (4,6) and is feasible for every thin lift tried at g = 3. Nothing about (V) is proved
2026-09-27
Status tags as in the note: proved (proof written here), computed (exact and reproducible without a SAT solver: rational LP points or Farkas certificates checked in Fraction arithmetic, or HiGHS LP/MILP verdicts, which are floating point and marked as such), solver (SAT verdict through h32_cap, or a HiGHS MILP verdict), conjecture. New scripts experiments/08_frozen_structure/scratch_h/h350_lib.py … h359_chainsplit.py; no existing file was modified; nothing committed. Setting and notation as in the brief and in 2026-09-27-aniso.md: cell \((a,b,c)\), rod axis \(x\), hole \(O\), rods \(v = O - 2e_x\), \(v' = O + 2e_x\), the four literals of Theorem U′ with lower bridgehead \((-1,1,1)\) of type \(y\) and upper bridgehead \((1,1,-1)\) of type \(z\); coordinates relative to \(O\); “grid \(d\)” is \(\{dx = d\}\) (A-grids even, B-grids odd); the target is the type-\(x\) mass of B-grid \(-1\). “Slab \(R\)” is (T2) on the hexagons with \(|dx| \le R\), “window \(p{:}q\)” is (T2) on \(-p \le dx \le q\). \(a = 12\) unless stated. The x-chains of the slab \(\{d, d+1\}\) are labelled by \(y - z\) (lower grid A) or \(y + z\) (lower grid B) modulo \(4g\); the rod \(v\) and both lower bridgeheads lie on the chain \((-2, 0)\) of the slab \(\{-2,-1\}\), and the chains \((-2, \pm 4)\) are its two neighbours (one chain at \(g = 2\)).
Status table
| # | statement | status |
|---|---|---|
| 1 | LP code validated: 26/3 on (3,3,3), 178/9 on (4,4,4) with the six literals, exact rational optimal points | computed |
| 2 | Reach at \(g = 2\): first \(R\) = 3 on (2,2), (2,4), (4,6), (6,10), (2,6), (6,8); (10,14) timed out at \(R = 3\) (120 s cap) | solver (reproduces aniso §2.2) |
| 3 | At \(g = 2\) the LP optimum is positive on every slab, decreases with \(R\) and never reaches 0 (to \(R = 11\)–15, and to \(R = 40\) with \(a = 24\)); whole cells with even \(a\) are positive (12/5, 24/5, 86/5 at \(a = 12\); 140/9 on (6,4,6)) | computed (exact rational points on the small tori; floating point on (6,8), (6,10), (10,14)) |
| 4 | At \(g = 2\) the LP optimum is exactly 0 on every cell with odd \(a\) tested: \(a\) = 1, 3, 5, 7, 9, 11, 13 on (2,4); 1, 3, 5, 7 on (4,6); 3, 5 on (2,2), (2,6), (6,8); 3 on (6,10); every control SAT. Exact Farkas certificates on (3,2,2), (5,2,2), (3,2,4), with support wrapping the x-circle. At \(g = 3, 4\) odd \(a\) does not help ((1,3,3) 6, (5,3,3) 6, (5,3,6) 12, (3,4,4), (5,4,4), (7,4,4) 32/3) | computed |
| 5 | Thinnest integral family uniform in the geometry: one-hot integrality on one x-chain, the chain next to the rod’s chain in the slab \(\{-2,-1\}\); closes on (2,4), (4,6), (2,6), (6,8), (6,10) at \(g = 2\), on (3,3), (3,6) at \(g = 3\), on (4,4) at \(g = 4\). Its A-half or B-half alone, or one type on it, does not close | computed (HiGHS MILP, floating point) |
| 6 | Other closing families at \(g = 2\): every (type, sublattice) family; grid 0 with any one type; grid \(-1\) with \(x\) or \(y\); grid \(+1\) with \(x\) or \(z\); each chain of the slabs \(\{-1,0\}\), \(\{0,1\}\) (all types; \(x\) alone only on the smaller tori); the grid-0 half of such a chain (on (2,6), (4,6), (6,8)). Lines and single vertices: only small-torus coincidences | computed |
| 7 | At \(g = 3\) no single grid closes (any type set) but every pair of consecutive grids does | computed |
| 8 | Smallest uniform split (greedy, all indicators): 3, 3, 6, 5 indicators on (2,2), (2,4), (2,6), (4,6), scattered over the slab, different sets on each torus. Restricted to the neighbouring chain (deletion-minimal from a contiguous ordering): 5 indicators on 4 vertices (2,6), 10 on 6 (4,6); 6 on 5 (3,3), 8 on 6 (3,6); 10 on 7 (4,4). The vertices form a contiguous run of the chain beside the cage. Caterpillars only on the thin tori (2,2), (2,4), (2,6) | computed |
| 9 | Exact L1-minimised Farkas certificates for all 65 leaves of the (4,6) chain split: 9 are one-hot contradictions, 7 use 12–20 (T2) rows, 49 use 234–375 of the 384 (T2) rows of the slab | computed (exact) |
| 10 | Degree-2 Sherali–Adams on the slab \(R = 3\): (2,2) full lift optimum 0 and negation INFEASIBLE; (2,4) negation INFEASIBLE already when lifted only by grid 0 (so the full lift is infeasible); the chain-half lift refutes on (2,2), (2,4), (2,6) and is FEASIBLE on (4,6); (4,6) grid-0 lift no verdict (450 s); (3,3) window \(4{:}5\): every thin lift tried is FEASIBLE; the full lift not run | computed (HiGHS IPM; validity of the lift checked on an integral model) |
| 11 | (V) at \(g = 2\) by hand | not proved; the non-linear step is not one of the three known ones (§6) |
1. Reproduction, and the LP by slab and by cell
h350_lib.Slab builds the programme of h331 on a window: variables only for the vertices of the window’s hexagons, one-hot, (T2) = 2, the four literals, objective the type-\(x\) mass of B-grid \(-1\). Validation first (h351_lp.py 3,3,3 all --six --exact, 4,4,4): 26/3 and 178/9, the optimal points rationalised and every equation checked in Fraction. The reach (h330_aniso.py 12,b,c reach x 10): first non-SAT \(R = 3\) on (2,2), (2,4), (4,6), (6,10), (2,6), (6,8) with every control SAT; on (10,14) the \(R = 3\) query hit the 120 s cap, so no verdict there. At \(g = 3\) ((3,3), (3,6)) 5 and at \(g = 4\) ((4,4)) 6, as aniso §2.2 (solver).
LP optimum (computed; exact = rationalised optimal point checked exactly):
| torus | \(R\) = 3 | 4–5 | 7 | 9 | 11 | 15 | whole, \(a = 12\) |
|---|---|---|---|---|---|---|---|
| (2,2) | 8/3 | 12/5 | 12/5 | 12/5 | 12/5 | — | 12/5 |
| (2,4) | 6 | 24/5 | 24/5 | 24/5 | 24/5 (also \(R\) = 21; \(a\) = 24, \(R\) = 23, 40) | — | 24/5 |
| (2,6) | 10 | 15/2 | 52/7 | 59/8 | 59/8 | — | — |
| (4,6) | 22 | 92/5 | 124/7 | 406/23 | 669/38 | 714/41 | 86/5 |
| (6,8) | 44.82 | 39.90 | 38.96 | — | 37.93 | — | — |
| (6,10) | 56.82 | 50.74 | 49.52 | — | 48.26 | — | — |
| (10,14) | 135.77 | 124.38 | — | — | — | — | — |
More room along \(x\) lowers the optimum, by less each time, and on the tori with \(b = 2\) it is constant from \(R = 4\) or 5; it never reaches 0. As a fraction of the grid it is 0.30–0.47, and it grows with the torus. The 15.56 of aniso §2.4 on (4,6) is the cell \(a = 6\): I get 140/9 there, and 86/5 at \(a = 12\).
Short cells with the x-circle closed (following the main loop’s correction 2). The dependence on \(a\) is a parity:
| torus | \(a\) = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 9, 11, 13 |
|---|---|---|---|---|---|---|---|---|
| (2,2) | — | 12/5 | 0 | 12/5 | 0 | — | — | — |
| (2,4) | 0 | 24/5 | 0 | 24/5 | 0 | 24/5 | 0 | 0 |
| (2,6) | — | 22/3 | 0 | — | 0 | — | — | — |
| (4,6) | 0 | 44/3 | 0 | 31/2 | 0 | 140/9 | 0 | — |
| (6,8) | — | 212/7 | 0 | — | 0 | — | — | — |
| (6,10) | — | 268/7 | 0 | — | — | — | — | — |
| \(g = 3\): (3,3) | 6 | — | 26/3 | — | 6 | — | — | — |
| \(g = 3\): (3,6) | — | — | 18 | — | 12 | — | — | — |
| \(g = 4\): (4,4) | — | — | 32/3 | 44/3 | 32/3 | 44/3 | 32/3 | — |
Every control on the odd cells is SAT ((3,2,2), (3,2,4), (5,2,4), (3,4,6), (1,2,4); h330_aniso.py CELL full), so the zeros are not vacuous. Exact certificates (h356_cert.py, checked in Fraction): (3,2,2) 140 (T2) + 81 one-hot + 4 hypothesis rows; (5,2,2) 162 + 104 + 4, multipliers in \(\{\pm 1/8, \pm 1/4, \pm 3/8, \pm 1/2, \pm 3/4, \pm 1, 9/8\}\); (3,2,4) 331 + 186 + 4. Each uses hexagons in every x-layer, including the ones that wrap the x-circle. On (7,2,4) the float optimum is 0 but the rationalisation of the L1-minimal dual failed at denominator \(10^4\); I did not pursue it (the later version of h350_lib retries to \(10^8\) but was not re-run on that cell).
Reading (conjecture). At \(g = 2\) the relaxation is closed by the x-circle exactly when the circle has an odd number of cubes. A relation of the form \(f(n) + f(n+1) = c_n\) round a circle determines \(f\) when the length is odd and leaves an alternating solution when it is even; the LP witnesses on even cells and on slabs are presumably of that alternating kind. The witness on (4,2,4) has x-mass exactly 6.4 on every A-grid and 4.8 on every B-grid (h351_lp.py 4,2,4 all --grids), and its \(y\) and \(z\) masses are not periodic with one cube, so the alternation, if it is one, is in the transverse structure and not in the grid counts. At \(g = 3, 4\) nothing of the kind happens. So the clean statement that \(g = 2\) needs integrality is: it needs it on every slab and on every cell of even rod-axis length; on odd rod-axis length it does not (computed on the cells listed). A slab certificate cannot use this, since a slab has no circle.
2. The thinnest integral family
h352_int.py (HiGHS MILP, the named indicators integral, all others continuous, 60 s limit unless stated; “closes” = optimum < \(10^{-6}\) or infeasible). All on the slab \(R = 3\) at \(g = 2\).
- (type, sublattice) families: all six close on (2,4) and (4,6).
- One grid (on (2,4) and (4,6), the same verdicts): grid 0 closes with all types and with each single type; grid \(-1\) with \(x\) or \(y\), not \(z\); grid \(+1\) with \(x\) or \(z\), not \(y\); grids \(\pm 2\) never; grid \(+3\) never; grid \(-3\) closes on (2,4) and gave no verdict on (4,6).
- One x-chain, all types (the uniform answer): the chains of the slabs \(\{-1,0\}\) and \(\{0,+1\}\) (each contains one bridgehead) close on (2,4), (4,6), (2,6), (6,8), (6,10); with the \(x\)-indicators alone they close on (2,4), (4,6), (2,6) and gave no verdict on (6,8) at 60 s and at 400 s. The neighbouring chain \((-2, 4)\) of the rod’s slab (not through \(v\) or the bridgeheads) closes with all types on (2,4), (4,6), (2,6), (6,8) (43 s), (6,10) (82 s); with \(x\) alone it does not. The rod’s own chain \((-2, 0)\) never closes. The chains of slabs \(\{-3,-2\}\) and \(\{2,3\}\) never close.
- Half a chain: the A-half of a chain of the slab \(\{-1,0\}\) (the grid-0 vertices with \(y + z \equiv 2 \bmod 8\)) closes on (2,6), (4,6), (6,8) (92 s) and gave no verdict on (6,10) at 200 s. Its B-half does not; one type on either half does not. Neither half of the neighbouring chain closes.
- Lines (all three types): on (2,4) and (2,6) the \(z\)-lines of grid 0 at \(dy = \pm 2\) and the \(y\)-lines at \(dz = \pm 6\) close; on (4,6) only the \(z\)-lines at \(dy = \pm 6\); on (6,8) the prediction \(dy = \pm 10\) fails and \(dy = -8, -6\) gave no verdict. Not uniform. No \(x\)-line closes.
- Single vertices (all three types): none closes on (2,4).
So the family that is the same in the geometry of the pattern on at least three of the required tori is the whole of one x-chain with one-hot integrality: a chain of \(\{-1,0\}\) or \(\{0,1\}\), or the neighbouring chain of \(\{-2,-1\}\) (five tori). At \(g = 3\) and \(g = 4\) (§5) the neighbouring chain is again the answer, so it is the one to carry forward. Thinner than a chain, the only candidate is the grid-0 half-chain of \(\{-1,0\}\), on three tori.
3. The case split
h353_branch.py (uhand’s prefix-tree test with greedy growth and deletion; binary splits on single indicators \(t(u,k)\)), h359_chainsplit.py (the neighbouring chain in a contiguous order, then h353 shrink).
Unrestricted greedy (the candidates are all indicators of the slab): (2,2) 3 indicators, 4 leaves; (2,4) 3, 5 leaves; (2,6) 6, 14 leaves; (4,6) 5, 12 leaves. The sets are scattered over grids \(-3 \dots 2\) and have nothing in common from one torus to the next: e.g. (4,6): \(z(1,-3,3)\), \(x(-3,-1,1)\), \(y(0,-4,2)\), \(z(2,-2,2)\), \(x(1,1,3)\). Each is deletion-minimal but not known to be minimum.
On the neighbouring chain. Ordering the vertices of the chain \((-2,4)\) by distance from the cage and splitting on \(t(u,x)\) then \(t(u,y)\) at each, the prefix tree closes after 7, 7, 9, 15 vertices on (2,4), (2,6), (4,6), (6,8) and 5, 7, 7 on (3,3), (3,6), (4,4). Deletion-minimal subsets:
| cell, window | indicators | vertices | leaves (inf/zero) |
|---|---|---|---|
| (2,6), \(R = 3\) | 5 | \((-2,0,4)\), \((-2,2,-2)\), \((-1,-3,1)\), \((-1,1,-3)\) | 9/5 |
| (4,6), \(R = 3\) | 10 | \((-2,-2,2)\), \((-2,0,4)\), \((-2,2,-2)\), \((-1,-3,1)\), \((-1,-1,3)\), \((-1,1,-3)\) | 55/10 |
| (3,3), \(4{:}5\) | 6 | \((-2,0,-4)\), \((-2,2,-2)\), \((-2,4,0)\), \((-1,1,-3)\), \((-1,3,-1)\) | 22/7 |
| (3,6), \(4{:}5\) | 8 | the same and \((-1,5,1)\) | 44/7 |
| (4,4), \(6{:}6\) | 10 | the (3,3) five and \((-1,-1,-5)\), \((-1,5,1)\) | 64/7 |
In chain order the vertices are consecutive: at \(g = 3, 4\) the run \((-2,0,-4)\), \((-1,1,-3)\), \((-2,2,-2)\), \((-1,3,-1)\), \((-2,4,0)\), \((-1,5,1)\) of the chain \(y - z = 4\) beside the cage, extended by one step the other way at \(g = 4\); at \(g = 2\) the same chain (there \(y - z \equiv \pm 4\) is one chain) on both sides of the cage. The (2,6) set does not close on (4,6) or (6,8) (h353 test), so the run lengthens with the torus at fixed \(g\). Shape: on the thin tori the greedy split restricted to the neighbouring chain is a caterpillar, 4 indicators and 5 leaves on both (2,4) (\(y(-1,3,-1)\), \(z(-2,-2,2)\), \(y(-1,-3,1)\), \(x(-2,-4,0)\)) and (2,6) (\(y(-1,3,-1)\), \(x(-1,-1,-5)\), \(z(-2,-2,2)\), \(y(-1,-1,3)\)), and so is the unrestricted greedy split on (2,2); none of the trees in the table above is (each has an internal node neither of whose children closes at once), and the greedy on (4,6) restricted to the chain did not finish (below). It is not the choice between the two chain classes of a slab: the split is on single vertices of one chain, and the chain through the bridgeheads is never split on.
Exact branch certificates (h357_leafcerts.py 12,4,6 3 …, the 10-indicator split, 65 leaves, every one exact in Fraction): 9 leaves are one-hot contradictions (no (T2) row); 7 close with 12–20 (T2) rows, all in grids \(-3 \dots 2\); 49 use 234–375 of the slab’s 384 (T2) rows, spread evenly over the four layers of hexagons. On the greedy (4,6) split the 12 leaves use 307–371 (T2) rows except one with 10; on (2,4) 60–104 of 128. The certificates are a one-sided bound \(\sigma(t) \le y^{\mathsf T}At = y^{\mathsf T}b' \le 0\) with \(y\) minimising \(\|y\|_1\) (for an infeasible leaf this is a Farkas ray plus a dual-feasible point, so its \(L^1\) norm is larger than a pure ray’s). As at \(L = 3\) (uhand), a typical branch uses nearly every hexagon of the window.
4. The degree-two lift
h358_sa.py: the Sherali–Adams lift of h1_sa.py’s form on the slab, pair variables \(y_{ij} \ge 0\), every equality multiplied by \(x_j\) for \(j\) in a multiplier set \(M\) (the products with \(1 - x_j\) are differences), box products implied (docstring). Two questions: max (the target over the lift; 0 means a degree-2 certificate) and neg (add \(\sum_{b} t(b,x) \ge 1\) and its products with \(x_j\) and \(1 - x_j\); infeasible refutes “pattern and some type-\(x\) vertex on the grid”). Validity: an integral model of the pattern on the slab (SAT through h32_cap), lifted as \(x \otimes x\), violates 0 of 20 956 rows on (2,2) and 0 of 82 228 on (2,4) (computed).
| cell, window | \(M\) | size (pair vars / eq rows) | verdict | wall |
|---|---|---|---|---|
| (2,2), \(R = 3\) | all 168 columns | 13 860 / 20 956 | max 0; neg INFEASIBLE |
13 s; 0.9 s |
| (2,2) | grid-0 half-chain (12) | 1 926 / 1 612 | max 2.571; neg INFEASIBLE |
0.1 s |
| (2,4), \(R = 3\) | all 336 | 55 944 / 82 228 | no verdict (max 400 s, neg 400 s) |
417 s; 400 s |
| (2,4) | grid 0 (48) | 14 904 / 11 956 | neg INFEASIBLE |
1.5 s |
| (2,4) | grids \(-1,0,1\) (144) | 37 800 / 35 380 | neg INFEASIBLE |
24 s |
| (2,4) | half-chain (24) | 7 740 / 6 100 | max 5.5625; neg INFEASIBLE |
0.8 s; 0.7 s |
| (2,6), \(R = 3\) | half-chain (36); grid 0 (72) | 17 442; 33 588 pairs | neg INFEASIBLE, INFEASIBLE |
3 s; 10 s |
| (4,6), \(R = 3\) | half-chain (72) | 69 876 / 52 852 | neg FEASIBLE |
94 s |
| (4,6) | grid 0 (144) | 134 568 / 104 980 | no verdict | 450 s |
| (6,8), \(R = 3\) | half-chain (144) | 279 720 / 209 380 | no verdict | 150 s |
| (3,3), \(4{:}5\) | half-chains \(r\) = 2, 6, 10 (18 each); grid 0; grid \(-1\) (54) | 10 503; 30 537 pairs | neg FEASIBLE in all five |
1.5–23 s |
Verdicts, one per cell: (2,2): infeasible (full lift, both forms). (2,4): infeasible (the grid-0 lift’s rows are a subset of the full lift’s, so the full lift is infeasible too; the full lift itself gave no verdict in 400 s). (3,3): no verdict for the full lift (594 columns, about 176 000 pair variables and 291 000 rows; pre-flighted against the (2,4) full lift, 82 000 rows and no verdict in 400 s, and not run), and every thin lift tried is feasible. (4,6) is the first \(g = 2\) torus that is not thin in \(y\), and there the half-chain lift is feasible and the grid-0 lift gave no verdict: so the \(g = 2\) refutations above may be a small-torus effect, and I cannot say whether degree 2 suffices at \(g = 2\) in general. The HiGHS IPM verdicts are floating point; no dual certificate was extracted.
5. The trend in \(g\)
Least windows as corrected by check3: \(4{:}5\) at \(g = 3\) (both (3,3) and (3,6); LP 8.727 and 20.0), \(6{:}6\) at \(g = 4\) ((4,4); LP 19.88; \(3{:}9\) and \(9{:}3\) give 20.21).
| \(g = 2\) | \(g = 3\) | \(g = 4\) | |
|---|---|---|---|
| single grid closes | yes (grid 0, even one type) | no (none of the 10 grids, any type set; (3,3)) | not tested |
| two consecutive grids close | yes | yes (every pair, (3,3); three pairs tested on (3,6)) | not tested |
| one (type, sublattice) family | yes | yes ((3,3), \(4{:}5\), all six); none closes on \(4{:}4\) | not tested |
| neighbouring chain \((-2,\pm 4)\), all types | yes (5 tori) | yes, both neighbours ((3,3), (3,6)) | yes, both neighbours \((-2,4)\), \((-2,12)\); the opposite chain \((-2,8)\) does not |
| its halves, or one type on it | no | no | no |
| chain split, deletion-minimal | 4 v (2,6), 6 v (4,6) | 5 v (3,3), 6 v (3,6) | 7 v (4,4) |
| LP 0 on odd \(a\) | yes | no | no |
On the chain split the number of vertices is 4–6, 5–6, 7 at \(g\) = 2, 3, 4, and it grows with the torus at fixed \(g\) (4 → 6 from (2,6) to (4,6)). The data are compatible with growth like \(g + c\) on the smallest torus of each \(g\) and are not compatible with \(3(g-1)\); they do not determine a law, because the torus-size effect at fixed \(g\) is as large as the \(g\)-effect. At \(g = 3\) a single chain is an integral family that closes while no grid does, so the chain, not the grid, is the object that scales.
6. A hand proof at \(g = 2\)?
Not written. What the computations say about its shape:
- The integrality needed is one x-chain’s types (§2): a closed one-dimensional object of \(4\,\mathrm{lcm}(b,c)\) vertices, lying in two grids, the chain next to the rod’s chain. This is the analogue for (V) of uwall’s “one line of \(2L\) indicators” for the corner case, and it is uniform in \(g\) from 2 to 4.
- None of the three known non-linear steps fits as it stands. Lemma 4 needs two separable non-negative functions on a product; the chain is one-dimensional and the slab has no x-circle over which to integrate a separable count. The sheet step (\(F(i) + G(j) \in \{0,1\}\)) needs a function on a transverse product; the transverse torus of a chain slab is a single circle. Lemma T is about a single chain’s kinks at \(g = 1\); at \(g = 2\) the neighbouring chain is the second chain class of the slab, which is where a Lemma-T-type argument would have to act, but the split does not branch on the choice of chain class (§3).
- The parity phenomenon of §1 suggests a different kind of step: at \(g = 2\), a counting identity exists as soon as the x-direction closes up with odd length. A hand proof on the slab might therefore run: show by counting that on the slab some integer quantity attached to the neighbouring chain satisfies an alternating recurrence along the chain, and use its integrality (a parity argument) where the odd circle would have closed it. I have not identified that quantity. Conjecture: the step at \(g = 2\) is a parity step, of a kind the project has not yet used.
What failed, and why
- Positivity of the bridgehead type (
h354_pos.py): on (2,2), (2,4) the LP forces \(t(b,y) > 0\) at every vertex of the target grid, which with integrality would give (V) by one-sided splits. On (4,6) only 6 of 48 are forced positive, on (2,6) 20 of 24: a small-torus effect. The cumulative caterpillar on (4,6) needs all 48 vertices. - Lines and the cage’s methylenes as split sets: lines close only on thin tori, at positions that do not transfer ((0, ±2) on \(b = 2\), (0, ±6) on (4,6), not (0, ±10) on (6,8)); the eight indicators of the four transverse methylenes of \(O\) are not a uniform split on (2,6) or (4,6).
- Reading the certificates: 49 of 65 branch certificates on (4,6) use most of the slab; I could not recognise a structure. The odd-\(a\) certificates use the whole x-circle.
- Degree-two lift at \(g \ge 3\) and on (4,6): the full lifts are too large to decide in the time allowed; the thin lifts are feasible.
- Greedy splits are scattered and torus-specific (as uhand found on cubic cells); only the restriction to the neighbouring chain gave sets with a common geometry, and those still lengthen with the torus.
Rules broken. (i) One Bash call contained an empty shell heredoc (python - <<'EOF' with no body); it did nothing, but heredocs were forbidden. (ii) Two foreground commands ran past ten minutes and were moved to the background by the harness, where I stopped them: the (6,8) chains-and-lines sweep (about 7 min of chains plus the start of the lines; its chain results are reported above, the lines were cut off), and a greedy growth on (4,6) restricted to the neighbouring chain (no output, stopped). I had not pre-flighted either properly (the MILP time per family on (6,8) was 30–60 s, not the 5 s of (4,6)). Every other run finished inside ten minutes; LP and MILP calls had explicit time limits and one solver process ran at a time. Not reproduced: the (10,14) reach (SAT cap reached at \(R = 3\)); the exact certificate on (7,2,4).
Commands run
From scratch_h, .venv/bin/python, PYTHONPATH=<repo>:<repo>/experiments/08_frozen_structure, TMPDIR=<repo>/.tmp.
| command | what | verdict | wall |
|---|---|---|---|
h331_aniso_lp.py 3,3,3 --six, 4,4,4 --six, 12,2,2 3, 12,2,4 3 |
reproduce h331 | 8.6667, 19.7778, 2.6667, 6.0 | < 1 s each |
h351_lp.py 3,3,3 all --six --exact, 4,4,4 … |
validation | 26/3, 178/9 exact | 0.1, 0.4 s |
h330_aniso.py 12,b,c reach x 10, 10 tori |
reach | §1; (10,14) no verdict | 1–123 s |
h351_lp.py 12,b,c R-list [--exact], 8 tori |
LP by slab | §1 table | 0.1–31 s per LP |
h351_lp.py a,b,c all --exact, 37 cells |
short and odd cells | §1 parity table | 0.0–13 s |
h330_aniso.py CELL full, 6 cells |
SAT controls | all SAT; V UNSAT | < 3 s |
h356_cert.py 3,2,2 / 5,2,2 / 3,2,4 / 7,2,4 all |
exact odd-\(a\) certificates | exact on three; (7,2,4) rationalisation failed | < 1 s |
h351_lp.py 4,2,4 all --grids; 1,2,4, 1,4,6, 1,3,3 |
LP witness by grid; \(a = 1\) | 6.4/4.8 per grid; 0, 0, 6 | < 1 s |
h352_int.py 12,2,4 3 typesub/grids/chains/lines/verts |
families on (2,4) | §2 | 3–8 s |
h352_int.py 12,4,6 3 typesub/grids/chains/lines |
families on (4,6) | §2; grid \(-3\) no verdict | 33 s, 225 s, 137 s, 195 s |
h352_int.py 12,2,6 3 chains/lines/chainhalves |
(2,6) | §2 | 3–12 s |
h352_int.py 12,6,8 3 chains --only …, lines … |
(6,8) | chains close with all types, \(x\) alone no verdict; ran past 10 min, stopped | ≈ 11 min |
h352_int.py 12,6,8 3 lines --only "(0,10)|(0,-10)" --tl 150 |
predicted lines | open | 36 s |
h352_int.py 12,4,6 3 lines … --all --tl 20 |
all grid-0 lines | only \(dy = \pm 6\) | 32 s |
h352_int.py 12,6,8 3 chains --only "… x" --tl 400 |
one chain, \(x\) | no verdict | 443 s |
h352_int.py 12,6,10 3 chains --only "… xyz" --tl 300 |
one chain | closes | 60 s |
h352_int.py 12,6,8 / 12,6,10 3 chainhalves … --tl 200 |
half-chain | closes (92 s) / no verdict | 94 s, 201 s |
h352_int.py 12,4,6 / 12,3,3 4:5 / 12,4,4 6:6 chainhalves --only "slab -2/-1 inv 4" |
halves of the neighbouring chain | none closes | 20–40 s |
h352_int.py 12,6,8 / 12,6,10 3 chains --only "slab -2/-1 inv 4 … xyz" --tl 250 |
neighbouring chain | closes | 44 s, 84 s |
h352_int.py 12,3,3 4:5 typesub, 4:4 typesub, grids, gridsets, chains; 12,3,6 4:5 gridsets/chains; 12,4,4 6:6 chains |
\(g = 3, 4\) | §5 | 7–54 s |
h353_branch.py depth1 12,2,4 3 |
single splits | none two-sided | 4 s |
h353_branch.py grow on (2,2), (2,4), (2,6), (4,6) |
greedy splits | 3, 3, 6, 5 | 1–103 s |
h353_branch.py grow 12,2,6/12,4,6 3 … --cand half:2 |
greedy on half-chain | 5, 7 indicators | 5 s, 125 s |
h353_branch.py grow 12,2,4/12,2,6 3 … --cand chain:-2:4 |
greedy on neighbouring chain | 4, 4 | 2 s, 4 s |
h353_branch.py grow 12,4,6 3 14 40 --cand chain:-2:4 |
the same on (4,6) | ran past 10 min, stopped, no output | > 10 min |
h353_branch.py test … (cage methylenes; common sets) |
structured splits | not uniform on (4,6) | 1–15 s |
h359_chainsplit.py on (2,2), (2,4), (2,6), (4,6), (6,8), (3,3), (3,6), (4,4) |
contiguous chain split | uniform on all; 5–15 vertices | 0–145 s |
h353_branch.py shrink on (2,6), (4,6), (3,3), (3,6), (4,4) |
deletion-minimal | §3 table | 10–131 s |
h354_pos.py on (2,2), (2,4), (4,6), (2,6); cat on (4,6) |
positivity of \(y\) | positive only on thin tori; 48 splits | < 6 s |
h355_backbone.py 12,2,4 3 --map, 12,4,6 3 |
solver backbone | grid \(-1\) all \(y\), \(+1\) all \(z\), \(\pm 3\) no \(x\) | 0.1 s, 3 s |
h357_leafcerts.py 12,4,6 3 … (greedy split; chain split), 12,2,4 3 … |
exact branch certificates | all exact; §3 | 4 s, ≈ 10 s, 1 s |
h358_sa.py (15 runs) |
degree-2 lift | §4 table | 0.1–450 s |