Verdict

FAMILY GROWS (computed for b = 3, 4, 5; not decided for b >= 6, see T1.4). Every integral family that closes the LP of the box at one value of b that I found fails at the next: the 3-vertex family that closes b = 3 leaves 2 feasible branches at b = 4, the 7-vertex family that closes b = 4 leaves 10 at b = 5, and the 24-vertex set that closes b = 5 is MILP-feasible at b = 6 and b = 7. The smallest L1 ball of integral vertices about the next hole O_1 = (6,0,0) that closes the LP has radius 4, 5, 6 for b = 3, 4, 5, but radius 6 still suffices at b = 6, so growth beyond b = 5 is not established. Holding the family fixed (the 7-vertex family, which closes both b = 3 and b = 4), the branch certificates split cleanly into two kinds: local certificates (support 4 to 40 rows), identical row for row at b = 3 and b = 4, and global certificates whose support takes every y-value of the closed circle and whose support, L1 norm and number of distinct multiplier values grow with b (the all-x branch: 118 rows, L1 199, 22 values at b = 3; 283 rows, L1 1367/2, 58 values at b = 4). No rule uniform in b is visible in the global ones. A closed form, if there is one, has to be sought in sums over the closed y-lines (the parameter that grows), not in branch certificates on a fixed integral family.

Statement tested

Exactly h633’s box lemma, type model (h360_lib), cell (a, b, c), O = (2,0,0). Variables X, Y, Z >= 0 at every vertex lying on a box hexagon (vertices on no box hexagon carry only their own one-hot row, which is always satisfiable, so they are dropped). Equality rows:

• one-hot X + Y + Z = 1 at each such vertex;
• (T2) linear: the sum of the six matching indicators equals 2, on every hexagon all six of whose vertices have -3 <= x - 2 <= 2b+1 and |z| <= 2b-1 (y unrestricted, the y-circle of length 4b closed);
• the four literals X(v_0) = X(v_1) = 1, Y(beta) = 1, Y(gamma’) = 0 with v_0 = (0,0,0), v_1 = (4,0,0), beta = (1,1,1), gamma’ = (3,-1,1);
• the negated conclusion X(v_2) = 0, v_2 = (8,0,0);
• on a branch, rows t(u,k) = 1 (“u has type k”) for the family vertices.

Cells (12,3,8), (12,4,8), (12,5,6), (12,6,8), (12,7,8): the box does not wrap (4a > 2b+5, 4c > 4b-1). Positions below are relative to O (absolute = relative + (2,0,0)) unless marked absolute.

Symmetry group (proved by inspection). The lattice symmetries that fix O, the x-axis and its direction, and the box are the identity, the C2 rotation (x,y,z) -> (x,-y,-z) about the rod axis, and the two mirrors exchanging y and z (which exchange types y and z). The mirrors move Y(beta) = 1 to a Z literal; C2 maps the hypothesis pair {beta, gamma’} to the other pair {beta’ = (1,-1,-1), gamma = (3,1,-1)} (cubethree’s “by symmetry”). So the symmetry group of the hypothesis set is trivial, and no symmetry was imposed on the duals. Explored: with X(v_2) = 0 the LP itself forces Y(beta’) = 1 and Y(gamma) = 0 (h684 maxima), so the LP closure of the hypotheses is C2-symmetric; I did not exploit this.

T1. The LP and the integral family

T1.1 R has no linear content in the box (computed, HiGHS, controls).

One LP takes 0.6 to 2.2 s in a child process (mostly start-up), so the pre-flight put every T1 sweep under a minute; the MILPs were the cost.

T1.2 The A x-line through O + 2e_y does not close the box (computed). Restricted to the box it has 2, 3, 3 vertices at b = 3, 4, 5 (relative (4n, 2, 0), 4n in [-3, 2b+1], so about b/2 of them). Branching on X only: 3 of 4, 6 of 8 and 7 of 8 branches stay feasible; the line through O - 2e_y at b = 4: 6 of 8. Cubethree’s sufficiency of this line was on the torus (6,3,3), where the line closes round the x-circle; in the box it is cut and does not suffice. I did not try full type patterns on it, because (T1.3) found thinner families nearer the rod.

T1.3 Irreducible families by MILP deletion (computed, floating MILP; h686). All types integral is infeasible (the SAT statement). Deleting vertices from the integral set, farthest from relative (4,0,0) first, by whole L1 shells and then singly, keeping a vertex when the MILP becomes feasible or does not finish in its time limit:

The b = 3 families sit on the cage of O_1 = relative (4,0,0): its methylenes (4,0,+-2), (4,2,0), its lower bridgehead (3,-1,-1) (absolute (5,-1,-1) = v_1 + d_1) and its upper bridgeheads (5,+-1,-+1). At b = 4 two more vertices of the same B x-chains of step (0,2,2) in the plane x = 5 appear, (5,-1,-3) and (5,1,3). The b = 5 set (partial) is the 24 vertices (1,+-1,-+1), (2,0,0), (3,-3,1), (3,-1,-1), (3,-1,3), (3,1,-3), (3,1,1), (3,3,-1), (4,+-2,0), (4,0,+-2), (5,-3,-1), (5,-1,-3), (5,-1,1), (5,1,-1), (5,1,3), (5,3,1), (6,0,0), (7,+-1,+-1) (same signs), (8,0,+-2).

T1.4 Does a fixed family survive the next b? (computed; h685 LP trees, h686 MILP).

Least L1 radius r about relative (4,0,0) such that integrality of every vertex within r closes the LP (single MILPs, h686 --startonly):

So the needed radius goes 4, 5, 6 for b = 3, 4, 5 and stays 6 at b = 6. That is the one datum against unbounded growth, and I could not decide b = 7 within the cap. The branch count on a fixed family also grows (7-vertex family: 19 leaves at b = 3, 51 at b = 4). The verdict FAMILY GROWS rests on b = 3 to 5 and on every concrete family failing at the next b; it is not established for all b.

T2. Branches and canonical certificates (computed, exact)

For each branch: least-L1 Farkas vector y (A^T y >= 0, b.y = -1) by HiGHS in a child process, rationalised (least denominator in a ladder 1, 2, 3, 4, 6, …, 10^6) and verified exactly in Fractions; the control is the same branch without X(v_2) = 0. All branches were certified; no rationalisation failed; no branch was feasible for the families named.

A branch whose control is infeasible is excluded by the hypotheses alone (its certificate does not use X(v_2) = 0); those with a feasible control use the negated conclusion. The JSON files hold, per branch, every support row with its multiplier and label (kind; vertex or hexagon hole relative to O and sigma) and the columns with positive reduced value.

Rows by kind: every certificate uses only one-hot, (T2), literal, negation and branch rows (there are no bound rows: the variables are non-negative and the positive reduced columns play the role of the r_j of Theorem 9). Typical global certificate (F7, b = 4, branch all three methylenes of type x): 130 one-hot, 145 (T2), 4 literals, 1 negation, 3 fixings; 85 positive reduced columns.

Uniqueness of the canonical form: not checked. Least L1 need not be unique; I added no secondary tie-break. The local certificates agree exactly between two independent LPs (b = 3 and b = 4), which is weak evidence of uniqueness for them; for the global ones it is open.

T3. Tabulation across b (computed; h688)

The 15 branches common to the 7-vertex family at b = 3 and b = 4:

“all 12 y / all 16 y”: the hexagon holes and one-hot vertices of the support take every y-value of the circle (4b values). The 36 branches that exist only at b = 4 split the same way: 19 with support 4 to 23, 17 with support 114 to 375.

What I read from this (explored):

1. The local certificates are b-independent lemmas. Nine branches have the same certificate, row for row and multiplier for multiplier, at b = 3 and b = 4, inside x in [-1, 6] and |z| <= 3, multipliers in {+-1/2, +-1, +-2, …} with at most 9 distinct values. Example (F7, both b, branch (4,0,+-2) = x, (4,2,0) = z; 40 rows): (T2) at the hexagons of hole (0,0,0) with multipliers 3, 1, 2 for sigma = (-1,-1,1), (-1,1,-1), (1,-1,-1), of hole (4,0,0) with -1, -1 for (1,-1,-1), (1,1,1), of holes (2,+-2,0) with +-1/2 on all four sigma; literals -4 X(v_0), -2 X(v_1), -4 Y(beta), +2 Y(gamma’), +2 for X(v_2) = 0; one-hot -5/2 at (1,-1,1), -2 at (-1,-1,-1), -1 at (0,+-2,0), -1/2 at (1,-3,-1), (1,1,-1), (1,3,1), +1/2 at (3,-1,-1), (3,-3,1), (3,1,1), (3,3,-1), +1 at (4,+-2,0), (4,0,+-2), (5,-1,1), (5,1,-1). These are finite statements about the cages of O and O_1 and need no closed form.
2. The global certificates are where R lives, and they are the ones that use the whole circle. Their support grows by about a factor 2.4 from b = 3 to b = 4 (118 to 283 rows for the all-x branch, about a third of the box’s rows in each case), their L1 norm by 3.4 to 5.8, their distinct multiplier values by 2 to 3.3, and their denominators from 2 to 24. No multiplier pattern repeats between b = 3 and b = 4, and I did not find a rule tying a multiplier to its position relative to O, the rod line or the box edges.
3. So the analogue of Theorem 9’s four rules was not found, and the identity step of T3 was not reached: there was no rule to verify by formula.

What is left and a stop rule

1. Do not repeat: the A x-lines through O +- 2e_y in the box (fail); least-L1 branch certificates on a fixed vertex family (the global ones do not stabilise in b); MILP deletion over the whole box at b >= 5 (individual MILPs exceed 5 s and the filter does not finish in 10 minutes).
2. The one open datum that could reverse the verdict: whether the integral ball of radius 6 about O_1 closes the LP at b = 7 and b = 8 (the MILP did not finish in 90 s at b = 7). If it does, a bounded family exists (at most 60 vertices, which is still too many branches to tabulate by hand, so the practical conclusion would not change much). One run of at most 10 minutes per b, then stop.
3. Where a closed form should be sought instead. Every global certificate spans the full y-circle; this agrees with rodline’s reading (sums of P^y over closed y-lines of holes, whose methylene terms telescope, as in the proof of Theorem 5). The thing to tabulate is the certificate projected onto closed y-lines: for each (x, z) the sum of multipliers of the rows on the y-line of holes or vertices at (x, z). If those line sums are uniform in b while the in-line distribution is not (least L1 spreads mass arbitrarily along a line whose rows are translates of one another), the closed form exists in the line sums. That is a computation on the existing JSON files (no new solving), and it is the next step if anyone continues; stop if the projected sums of the all-x branch differ between b = 3 and b = 4 beyond translation.
4. The C2 symmetry of the LP closure (T2 note) could be imposed after adding Y(beta’) = 1 and Y(gamma) = 0 as derived rows; it would halve the search but not change the growth.

Scripts and timings

All new, in experiments/08_frozen_structure/scratch_h/; no existing script modified; nothing committed. Every LP and MILP ran in a child process with a hard subprocess.run timeout, one at a time.

Solver and LP wall time in all: about 38 minutes of the 90 allowed. One LP-tree run hung (highspy re-solving after bound changes at b = 4) and was killed at its 300 s cap; fixed by clearSolver() before each re-solve, and I checked outside the sandbox (pgrep) that no child was left running. The second b = 5 deletion run (radius 8) repeated the first to no purpose (280 s).

Rules kept or broken

Kept: read the handover block, the rodline report, the cubethree sections, the note’s sections on Theorem 9 and Theorem U, and the scripts named, before running anything; reused h633’s box and h360_lib’s hexagons exactly; pre-flight timed (one LP at b = 3, 0.6 to 4 s in a child); Mac only, no Sparks, no expq; one solver child at a time; every LP or MILP in a child with a hard timeout; no job over ten minutes; scripts numbered h680 to h688 with the required docstring and usage line; every reported certificate rationalised and verified exactly with its control recorded; no reach measurements, no (V) on any window; no commits; report under 400 lines, status tags on claims.

Bent: the h686 MILP runs at b = 4 (whole box) and b = 5 hit their caps and are reported as partial; the second b = 5 run duplicated the first. h682 was edited by me during the session (my own new script) to add modes and the clearSolver() fix. The MILP and LP-tree findings of T1 are floating-point exploration (tagged computed); only the T2 certificates are exact. No second reader.