Lemma (V) by hand: the cage’s four hexagons give exactly law C and nothing else, and the neighbouring B-cages give nothing at all. Two exact delimitations of the residual: (V) has no proof by local propagation (one-hexagon closure plus depth-1 case analysis derives only the six cage exclusions, L = 3, 4, 5), and none by counting either — (V) is false in the LP relaxation of the type model, with an exactly verified rational witness, so no sum of P and C laws round the x-circle can prove it however it is weighted. What closes the gap is one sixth of the integrality: 0/1 on a single (axis, sublattice) family of indicators makes the LP optimum 0. Also: the forcing needs the transverse torus as well as the x-circle

Status tags as in the note: proved (a proof is written here), computed (exact and reproducible, no solver), solver (a SAT or MILP verdict without a checked proof), conjecture. New scripts experiments/08_frozen_structure/scratch_h/h120_uhand.py, h121_farkas.py, h122_lpcuts.py, h123_lpcert.py, h124_milp.py, h125_anatomy.py. No existing script was modified and nothing was committed. Builds on 2026-09-22-orient.md (Theorem U and lemma (V)), 2026-09-21-laws.md (the cage theorem, (P), completeness), 2026-09-21-sheetcore.md (M′) and 2026-09-21-sheetcurl.md (Lemma C, Lemma S1, Theorem B′).

Verdicts

1. (V) is not proved. Nothing x-global is proved here. What is proved by hand is the cage’s own content, and it is exactly law C: Lemma U1 below writes out the four hexagons of the A-cage and shows that under yy/zz each of them already carries its two matches (one rod, one bridgehead), so all four transverse methylenes are unmatched. No further literal follows.

2. The neighbouring cages give nothing (proved; computed). Six B-holes of grid g+1 are adjacent to β or β′; exactly two of them are adjacent to both, and their cages carry three of the four constrained bridgeheads each. One of their four hexagons is a hexagon of the A-cage itself; the other three give the three equations (K2), (K3), (K4) of Lemma U2, in six new indicators, with four or five free terms apiece. None is a unit, and no literal is forced.

3. No proof by local propagation (computed, h120). Closing one-hot and “a hexagon has exactly two matches” to a fixpoint from the hypothesis determines 6 vertices and halves the type set at 4 more — precisely the hypothesis and law C — at L = 3, 4 and 5. Adding a full round of depth-1 case analysis (assert one literal, close, look for a contradiction: a hand proof by contradiction of depth one, at every vertex and type) adds nothing: no literal fails. So no amount of one-hexagon reasoning, with or without single-vertex case splits, reaches (V).

4. No proof by counting, even with non-negativity (computed, exact; h121–h123). This is the main negative result and it closes the route the brief proposed. The type model’s equations are one-hot Σ_a t(v,a) = 1, (T2) Σ_{v∈h} t(v,α_h(v)) = 2, and the six cage literals; every law of the project (Pˣ, Pʸ, Pᶻ, C, (P), Lemma C, the grid counts) is a rational combination of them. A proof of the form “take a rational combination of the laws and read off a sum of non-negative indicators” — the shape of Lemma S1, and of every sum round the x-circle the brief suggested — exists iff the LP max { Σ_{b ∈ B-grid g+1} t(b,x) : equations, t ≥ 0 } is 0. It is not:

   L	B-sites on grid g+1	LP optimum	verified exactly
   3	18	26/3 ≈ 8.67	yes
   4	32	178/9 ≈ 19.78	yes
   5	50	299/9 ≈ 33.22	yes

   “Verified exactly” means h123_lpcert.py rationalises the LP optimum and checks with Fraction arithmetic that it satisfies every equation exactly and has no negative entry, so the verdict does not rest on floating point. Adding every cage-local clause of length ≤ 3 (136 per cage kind), on every one of the 216 cages — 29 376 extra inequalities at L = 3 — leaves the optimum at 26/3 unchanged (h122). So finite case analysis inside one cage does not help the counting route either.

5. What closes the gap is one sixth of the integrality (solver, L = 3, 4, 5; h124). Impose 0/1 on the indicators of one (axis, sublattice) family only — for example ξ = [· x] on A, 108 of the 648 variables at L = 3 — and leave all the others merely non-negative. The MILP optimum is then 0. This holds for each of the six families (xA, xB, yA, zA, yB, zB tested). So

   (V) = [the linear laws] + [t ≥ 0] + [t(·, k) ∈ {0,1} on one sublattice].

   That is the exact residual, and it is the sheet theorem’s shape (f ∈ {0,1} for one field), not Lemma S1’s.

6. (V) needs the transverse torus as well as the x-circle (computed, h100). The orient report records the x-slab threshold |dx| ≤ 2L−2 with the full transverse torus. Holding that threshold and shrinking the transverse window by one plane destroys the forcing completely: at L = 4 with RX = 6 = 2L−2, the backbone forces 368 literals at RT = 8 (the whole transverse torus) and exactly 22 — the hypothesis and law C, nothing else — at RT = 7 and RT = 6. At L = 6 with RX = 5 the same happens at RT = 12 (38 forced) versus RT = 9, 10, 11 (22 forced). So (V) is a statement about all three circles, not a “light cone along x”; the light cone of the orient report §4 only exists once the transverse torus has closed.

Setting and coordinates

The type-only model: one-hot types plus (T2) (“every hexagon has exactly two matches”), no bonds, no sign field, no ice rule. By the cage theorem (laws report), (T2) is equivalent, given one-hot, to C ∧ Pˣ ∧ Pʸ ∧ Pᶻ on every cage of both kinds.

Put the A-vertex v at the origin. Then, with d₀ = (1,1,1), d₁ = (1,−1,−1), d₂ = (−1,1,−1), d₃ = (−1,−1,1):

Grids: g = 0 is v’s A-grid, g+1 = 1 is β’s B-grid, g+3 = 3 is γ’s, g+4 = 4 is v′’s. The map (x,y,z) ↦ (x,−y,−z) is a lattice symmetry (it permutes d₀ ↔︎ d₁, d₂ ↔︎ d₃, fixes every axis label and fixes A) and it fixes the hypothesis, exchanging β ↔︎ β′ and γ ↔︎ γ′. Everything below therefore comes in mirror pairs.

(V) is: every B-site of grid g+1 is type y — equivalently (given Lemma S1 and the grid-count identity) none is type x. Everything printed in this section is checked by h125_anatomy.py, which derives the cage, its hexagons and their axes from the lattice itself.

Lemma U1 (proved): the four hexagons of the cage, and law C

Lemma U1. Under the hypothesis, the four transverse methylenes are unmatched: w_y^± is not type y and w_z^± is not type z. Nothing else follows from the cage.

The cage’s four hexagons, each written as a cycle with the hexagon axis at each vertex (h125_anatomy.py 4; three bridgeheads and three methylenes apiece, as Lemma 1 of the laws report requires):

Proof. Each bridgehead occurs in three of the four hexagons, with the three different axes (laws, Lemma 1(b)); each methylene w_k^σ occurs in two, always with axis k (Lemma 1(a)). Read off the matches:

• H₁ and H₂ contain v with axis x: v is type x, so it matches in both. H₃ and H₄ contain v′ with axis x, likewise.
• In H₁ the bridgeheads are β (axis y), γ′ (axis x), β′ (axis z). Under yy/zz exactly one of them matches, namely β. In H₂ they are β (z), γ (x), β′ (y): exactly β′ matches. In H₃ they are γ′ (y), γ (z), β (x): exactly γ. In H₄ they are γ (y), β′ (x), γ′ (z): exactly γ′.

So each hexagon already has two matches — one rod, one bridgehead — and (T2) says its two remaining vertices, which are transverse methylenes carrying their own axis, do not match:

• H₁: w_z^+ not z, w_y^− not y; H₂: w_y^+ not y, w_z^− not z;
• H₃: w_z^+ not z, w_y^+ not y; H₄: w_z^− not z, w_y^− not y.

Together these are the four exclusions. They are exactly law C at this cage: C says exactly two of the six methylenes are matched, and the two rods already are. ∎

Two remarks worth keeping.

• The hypothesis is tight for (T2) on the cage. Under yy/zz every hexagon of the cage has its match quota filled by the hypothesis alone. That is the structural reason this pattern is special, and it is why it propagates nothing locally: a saturated hexagon constrains only its own remaining vertices.
• The four exclusions are all the cage gives. The type-only closure of the whole torus under one-hexagon reasoning stops here (verdict 3).

Lemma U2 (proved; computed): the neighbouring cages

Take the B-cages centred at the B-holes of grid g+1 adjacent to β or β′. There are six such holes, and exactly two are adjacent to both β and β′: O₁ = (1,1,−1) and its mirror O₂ = (1,−1,1). Those two carry three of the four constrained bridgeheads as methylenes; the other four carry only one. At O₁ (h125_anatomy.py):

So two of the B-cage’s four bridgeheads are transverse methylenes of the A-cage, a third is a new site b₃, and the fourth is v itself.

Lemma U2. One of the four hexagons of the B-cage at O₁ is H₂, a hexagon of the A-cage. The other three give

(K2) [b₁ x] + [A₂ y] + [b₃ z] + [A₁ x] = 2 (K3) [b₂ x] + [A₃ z] + [b₃ y] + [A₁ x] = 1 (K4) [b₁ z] + [b₂ y] + [A₃ z] + [b₃ x] + [A₂ y] = 2

and law C at O₁ reads [A₁ x] + [A₂ y] + [A₃ z] = 1. None of these forces a literal, and the three together force none: every literal appearing in them is realised in some (T2) state with the cage.

Proof. The three hexagons are, with their axes,

• v (y) — β (z) — b₁ (x) — A₂ (y) — b₃ (z) — A₁ (x),
• v (z) — β′ (y) — b₂ (x) — A₃ (z) — b₃ (y) — A₁ (x),
• b₁ (z) — γ (x) — b₂ (y) — A₃ (z) — b₃ (x) — A₂ (y).

v is type x and β type y, so neither matches in the first, whence (K2). In the second, β′ is type y on axis y and matches, v (axis z) does not, whence (K3). In the third, γ is type z on axis x and does not match, whence (K4). For law C at O₁: of the three known methylenes, β = w_z^+ is type y and unmatched, γ = w_x^+ is type z and unmatched, and β′ = w_y^− is type y and matched; C’s quota of two matched methylenes therefore leaves exactly one match among A₁, A₂ and A₃ on their own axes. The non-forcing is the closure computation of verdict 3. ∎

Note (K3): exactly one of four indicators. That is the strongest of the three, and it is still a four-term disjunction. Combining (K2) and (K3) on their shared term [A₁ x] and splitting on it produces two consistent branches, so not even a depth-one case analysis closes. The mirror cage at O₂ gives the mirror equations under (x,y,z) ↦ (x,−y,−z), with γ′ in place of γ.

The A-cages at O ± 4e_x give nothing either. Their only contact with the hypothesis is one rod: the cage at O + 4e_x = (6,0,0) has v′ as its lower methylene and the pair (5,±1,±1) as its lower bridgeheads, of which nothing is known. Its Pˣ law reads [v″ x] = 1 + (#type-x upper bridgeheads) − (#type-x lower bridgeheads) with v″ = (8,0,0), and both counts are free in {0,1,2}. This is why the backbone fact “the whole A x-line through v is type x” is itself x-global, not a step-by-step propagation.

The grid-count sums (proved): both suggested sums are 0 = 0

The brief asked for the sum of Pˣ over the B-cages of one x-line of B-holes, and over all cages of one grid. Both are identities with no content, and the reason is worth recording.

Write Pˣ at a cage in neighbour form (laws, Task 4): the upper bridgeheads of the cage whose upper x-middle is M are M’s two neighbours one step down in x, and the lower bridgeheads are the two neighbours of m = M − 4e_x one step up. So Pˣ is

ξ(M) − ξ(m) = D(M) − U(m),

with D(M) the number of type-x neighbours of M one step down in x and U(m) the number one step up from m.

• Over one x-line of cages. The cages along a line have M_t = m_{t+1}, so the left side telescopes round the x-circle to 0. The right side is Σ_t [D(M_t) − U(M_{t−1})], a sum of the same shape; it is the sum of (P) along the line and is 0 by the same telescoping. No term survives.

• Over all the cages of one grid. Let the cages have their holes on grid G, so m lies on G−2 and M on G+2, the lower bridgeheads on G−1 and the upper on G+1. Each B-site on G+1 has two A-neighbours on G+2, each of which is the M of exactly one cage of grid G, so it is an upper bridgehead of exactly two of them; likewise below. Each A-site on G±2 is the M or m of exactly one cage. Summing Pˣ therefore gives

  2 n_B^x(G+1) − 2 n_B^x(G−1) = n_A^x(G+2) − n_A^x(G−2),

  which is the grid-count identity itself (both sides are 0 by Lemma C of sheetcurl read along x). The same computation with law C’s c-form over a grid gives 2(n_A^x(G−2) + n_A^x(G+2)) − 4 n_A^x(G) = 0, again the grid-count identity.

The hypothesis lives at one cage; any sum over a whole grid or a whole line averages it away. This is not a defect of the particular sums chosen: no weighting works, by verdict 4.

What the grid-count identity does do is the step after (V): n_B^x is the same on every B-grid, so (V) gives n_B^x = 0 everywhere, hence (by Lemma S1 and non-negativity) B is x-free, and the sublattice mirror of M′ gives curl-free. That half was already proved.

Why counting stops: the LP relaxation (computed, exact)

The equivalence. Let A t = b be the system {one-hot, (T2), the six cage literals} in the 648 (L = 3) type variables, and let the target be σ(t) = Σ_{b ∈ B-grid g+1} t(b,x). Suppose a hand proof of (V) has the form: take rational multipliers y for the equations; the resulting functional yᵀA t = yᵀb has every coefficient ≥ the corresponding coefficient of σ, and yᵀb ≤ 0; since t ≥ 0, σ(t) ≤ yᵀA t = yᵀb ≤ 0, so every term of σ vanishes. That is exactly Lemma S1’s argument, exactly the sheet-disjunction argument’s linear half, and exactly what “sum a P law or law C round the x-circle and read off a non-negative count” means. By LP duality such a y exists iff max { σ(t) : A t = b, t ≥ 0 } = 0. (Upper bounds t ≤ 1 are implied by one-hot and t ≥ 0, so nothing is lost by omitting them.)

The verdict. The maximum is 26/3 at L = 3, 178/9 at L = 4 and 299/9 at L = 5 — between 48 % and 66 % of the grid. h123_lpcert.py rationalises the optimal point and verifies with exact Fraction arithmetic that all 654 (L = 3) equations hold exactly and no coordinate is negative. So the witness is a genuine rational point of the polyhedron, and the negative result is computed, not solver.

Cuts do not help. h122_lpcuts.py enumerates the 1200 (T2)-feasible assignments of a cage of each kind and extracts every minimal partial assignment of at most three of its ten vertices that no feasible assignment extends: 30 of length ≤ 2 and 136 of length ≤ 3, per kind. Imposed as linear cuts on every one of the 216 cages (6 480 and 29 376 inequalities at L = 3), they leave the optimum at 26/3 exactly. So “case analysis inside a cage, then sum” is also dead.

What the LP does prove. Maximising and minimising each variable separately (h122 forced, L = 3) pins 32 non-types and 6 types. The 6 types are the hypothesis itself: the LP forces no new positive type anywhere. Of the 32 exclusions, 16 are the hypothesis’s one-hot companions (12) and law C (4). The other 16 are new: eight at B-sites, on the grids dx = ±1 and dx = ±5, and eight at A-sites, on dx = ±4 and on the antipodal grid dx = 6. Every one of them is extremal — the B-sites all have a transverse coordinate of magnitude 5, the largest a B-site can have at L = 3, and the A-sites are either on the antipodal x-grid or at transverse offset 6, the antipodal transverse plane. Not one is near the cage. They are part of the spread the orient report saw, and are already torus-global statements themselves; so the LP reproduces some of the light cone and cannot close it.

What integrality is needed (solver)

h124_milp.py re-solves the same programme with 0/1 imposed on a chosen subset of the indicators and everything else left continuous and non-negative.

Reading: one sixth of the integrality — a single (axis, sublattice) family — suffices, and no family restricted to a couple of grids does (the L = 3 entries that succeed on two grids fail at L = 4, so they are small-cell artefacts). The statement is uniform in which family is chosen, so the content is not “the x-field is special” but “one whole sublattice’s worth of a single indicator must be integral”.

This is the sheet theorem’s ingredient, not Lemma S1’s. Sheetcore’s proof of the sheet disjunction uses exactly this: f = F(i) + G(j) is a linear consequence, and the step that produces structure is “and f ∈ {0,1}, so F or G is constant”. The corresponding object here is available and proved: by the laws report’s Task 4, summing (P_A) round the x-torus telescopes, so the column counts N_B(i,j) = Σ_t f(t; i, j) satisfy N_B = F(i) + G(j) on the transverse lattice in every (T2) state, and 0 ≤ N_B ≤ L. A hand proof of (V) should be looked for as a statement about that separable integer function under the hypothesis.

Both circles (computed)

h100_spread.py on the torus, hypothesis assumed, (T2) only on hexagons inside the window |dx| ≤ RX, |dy| ≤ RT, |dz| ≤ RT, complete backbone inside the window:

One transverse plane short of the torus, the configuration is as free as a bare cage; with the plane restored, the whole backbone appears. So (V)’s globality is not the x-circle alone. The orient report’s “transverse light cone on slabs” is right as stated (its slabs had the full transverse torus) but should not be read as forcing that spreads outwards from the cage: there is no spread at all until every transverse plane is present.

Branching certificate (follow-up)

Verdict 5 says (V) follows from the laws, non-negativity, and 0/1 on one (axis, sublattice) family. That makes a finite case split possible in principle: a set S of that family’s variables such that every 0/1 assignment of S closes the LP (optimum 0, or infeasible). Call such an S a uniform certificate; it is a hand proof by case analysis on |S| bits, one Farkas certificate per branch.

How S is tested (proved). Fix any order on S and run a depth-first prefix search, pruning at a node whose LP already closes. Adding further fixed values to a closed LP keeps it closed (extra bounds can only lower an optimum, and an infeasible system stays infeasible), so if every leaf closes then every full assignment of S passes through a closed node; and an open leaf is an assignment of S that does not close. The verdict is therefore exact and does not depend on the order, and the variables the search actually branched on form a smaller uniform certificate. That is h127_grow.py.

Lemma U0 (proved; computed): four literals are the whole hypothesis

Lemma U0. Given one-hot and (T2), “v and v′ are type x, one lower bridgehead is type y and one upper bridgehead is type z” forces the other lower bridgehead to be type y and the other upper bridgehead to be type z.

Proof. Say β and γ are the named ones, and use the four hexagons of Lemma U1.

• H₁ = v (x) — β (y) — w_z^+ (z) — γ′ (x) — w_y^− (y) — β′ (z). Here v and β match, so the other four do not: in particular β′ is not type z, hence β′ ∈ {x, y}.
• H₃ = w_z^+ (z) — γ′ (y) — v′ (x) — γ (z) — w_y^+ (y) — β (x). Here v′ and γ match, so γ′ is not type y (hence γ′ ∈ {x, z}) and w_y^+ is not type y.
• H₂ = v (x) — β (z) — w_y^+ (y) — γ (x) — w_z^− (z) — β′ (y). v matches; β is type y so it does not; γ is type z so it does not; w_y^+ is not type y. So exactly one of [w_z^− z] and [β′ y] holds.
• H₄ = v′ (x) — γ (y) — w_z^− (z) — β′ (x) — w_y^− (y) — γ′ (z). v′ matches; γ is type z so it does not; w_y^− is not type y (from H₁). So exactly one of [w_z^− z], [β′ x], [γ′ z] holds.

If β′ were type x, then [β′ y] = 0, so H₂ gives [w_z^− z] = 1, and H₄ would carry two matches among its three free terms. So β′ is type y, [w_z^− z] = 0, and H₄ then gives γ′ is type z. ∎

Computed (h120_uhand.py closure, L = 3, 4, 5, all four choices of which lower and which upper bridgehead is named): the one-hexagon closure forces the other two in every case, and determines exactly the same ten sites as yy/zz does. So Theorem U′’s four literals and yy/zz are the same hypothesis in the type-only model, and every number below is unchanged by using either — h126_branch.py milp returns identical optima and identical node counts (7 at L = 3, 37 at L = 4) for yyzz, u4 and u4b.

Branching trees (solver)

h126_branch.py milp L family: scipy/HiGHS on the same programme with one family integral. Node counts (presolve and cuts on, so these are upper bounds on what branching alone needs):

The tree grows by roughly an order of magnitude per unit of L, and the two sublattices swap places between L = 3 and L = 4, so the L = 3 ranking is not meaningful.

A pure branch-and-bound of my own (no cuts, branch on the most fractional family variable, h126_branch.py bb) closes at L = 3 on the A x-family in 233 nodes, 117 closed leaves, depth 12 — but it branches on 65 distinct A-sites, so its tree is not a uniform certificate.

The uniform certificates (computed)

h127_grow.py growshrink grows S greedily — at each step it adds the family variable that minimises the worst remaining open branch, choosing from the ten or twelve most fractional candidates — and then deletes elements one at a time while the prefix tree still closes. (The --prune variant, which instead maximises the number of branches closed, was tried only for the L = 5 attempt and did not help.) Greedy gives an upper bound on the minimum |S|.

The L = 3 certificate, in coordinates relative to v (so that the cage’s own sites are the ones of the setting table):

S = { w_y^+ = (2,2,0), w_y^− = (2,−2,0), w_z^− = (2,0,−2), v + 4e_z = (0,0,4), v′ + 4e_z = (4,0,4), (−4,−2,2) }.

Three of the six are the cage’s own transverse methylenes; two are the 4e_z translates of the two rods; one is four grids away. The L = 4 certificate is

{ w_z^+ = (2,0,2), w_y^− = (2,−2,0), (0,4,0), (6,−6,0), (−4,0,4), (−6,−6,0), (−6,0,6), (−2,−6,0), (−6,−6,−4) },

with only two cage sites, and it touches six of the eight A-grids.

The structure of S (computed)

• It is not the x-line. Fixing the whole A x-line through v — the set the backbone makes monochromatic — leaves the worst branch at 8.67 (L = 3), 19.50 (L = 4), 33.00 (L = 5), that is, almost the unbranched LP optimum. The line is worth nothing.
• It is not a grid or a chain. The xB certificate at L = 3 meets all six B-grids (4, 2, 5, 4, 5, 2 sites) and its transverse positions run over the whole transverse torus.
• It is not translation-stable. The natural structured guess suggested by the L = 3 answer — the four transverse methylenes together with the 4e_z and 4e_y translates of the two rods, {(2,±2,0), (2,0,±2), (0,0,4), (4,0,4), (0,4,0), (4,4,0)} — is a uniform certificate at L = 3 (30 closed nodes) and is not at L = 4. So S is not one fixed local pattern repeated; the answer at each L is a different scattered set.
• It grows with L. 6 → 9 for the A x-family from L = 3 to L = 4 (both deletion-minimal under the greedy construction, so these are upper bounds on the true minimum). The greedy curve at L = 5 was still at 31.4 of 33.2 after four variables and did not finish in budget, so |S| there is certainly larger again.

The per-branch certificates (computed)

For the six-variable L = 3 certificate the prefix tree has 29 closed nodes: 18 close by LP infeasibility and 11 by an optimum of 0. Sizing them (h128_certduals.py, h129_extent.py):

The dual of a degenerate LP is not unique, so the first rows are only an upper bound on how big a certificate must be; the L1-minimised row is the honest one. It says that the sparsest combination is 25 hexagon laws for the easiest branch and around 113 for a typical one. The xB certificate is worse still: 113 of its 114 nodes close by infeasibility, and the one LP dual uses 316 of 432 (T2) rows across all 12 grids.

Verdict on the branching route

The case split is small — six bits and twenty-nine branches at L = 3 — and that is genuinely encouraging. What is not encouraging is what closes each branch: a combination of the order of a hundred (T2) laws spread over every grid of the torus, dense in the cage basis too. So the branching certificate does not by itself turn into a hand proof; it turns the problem into “describe, uniformly in L, the Farkas certificate of each of the branches”, which is the same globality that verdict 4 identified, now packaged 29 times over.

Two things from this are worth carrying forward. Lemma U0 is a real simplification of the hypothesis: only four literals are needed, and the proof is four hexagons. And the branch that closes with 25 laws is the natural place to start reading a certificate by hand; if its structure is recognisable, the others may follow the same shape.

Residual and next targets

What is proved: Lemma U1, Lemma U2, the two grid sums, and the equivalence “a counting proof exists iff the LP optimum is 0”. What is not: (V), and with it Theorem U.

The residual is now exact:

Residual (V′). Let τ be one-hot with (T2) on the torus, carrying the yy/zz cage at O. Suppose in addition that the indicator [· x] on A takes values in {0,1} — which it does — and that everything else is only known to be non-negative and to satisfy the laws. Show Σ_{b ∈ B-grid g+1} [b x] = 0.

That is a genuinely smaller problem than (V): the continuous relaxation of five sixths of the variables is already enough, so the argument has to look only at one sublattice’s x-field together with linear algebra. Three concrete next steps:

1. Find the certificate, case by case. For a fixed integral ξ on A, (V) is a pure Farkas question in the remaining variables. Compute, for the integral ξ patterns that survive the hypothesis, the certificate that the solver is implicitly using, and look for a uniform description. The x-line backbone fact (ξ ≡ 1 on v’s line) should be proved first in this form, since it is the same kind of statement one dimension smaller.
2. Use the separable column count. N_B(i,j) = F(i) + G(j) with 0 ≤ N_B ≤ L is the one integer-plus-linear object already proved and already global in all three circles. (V) says N_B ≡ 0. The hypothesis has to be turned into a bound on F or G.
3. Compute the deletion-minimal core of (V), still not done. Given verdict 6 it should be sought as a set of hexagons meeting every transverse plane, not as a slab.
4. Read one branch certificate. The branching section below gives a six-variable case split at L = 3 whose easiest branch closes with 25 (T2) laws after L1-minimisation. That is the smallest completely explicit object the problem has produced; if its shape is recognisable the other 28 branches may follow it.

A warning for whoever takes it up: the LP witnesses of h123 are the reason to stop looking for a weighted sum of laws. Any proposed proof that never uses an indicator’s integrality is refuted by those points, which satisfy every law and every non-negativity and have two thirds of the grid type x.

Computations run

All from scratch_h with the project .venv, PYTHONPATH=<repo>:<repo>/experiments/08_frozen_structure, TMPDIR=.tmp. SAT solves go through h32_cap (subprocess, SIGKILL at the cap); ps is blocked by the sandbox and was not used. The LP and MILP work is scipy/HiGHS in a single process, seconds to a few minutes each; the L = 5 MILP was the longest, several minutes.