A report archived by the project, published as it was written. All reports · Markdown source
Cited as an artefact by: thm-11

(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

Claude (Opus), agent gtwo, for Lyndon Drake

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\).

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:

  1. 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.
  2. 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).
  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

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