The shape of the proof of (V): its deletion-minimal cores are thin but global — they touch every x-grid and every transverse residue, no tube round the x-circle suffices, there is no bounded-x induction step (the next cage’s bridgehead pattern is not determined at all), and the statement survives both the affine and the LP relaxation, so no linear certificate exists. What is new and cheap: (V) needs only four literals — both rods type x, one lower bridgehead type y, one upper bridgehead type z — and Theorem U holds under that weakened hypothesis too

Status tags as in the note: proved, computed, solver, conjecture. New scripts are experiments/08_frozen_structure/scratch_h/h110_ucore.py … h119_minU.py. Every UNSAT below comes with a SAT control on the same clause set, and every solve runs in a subprocess.run child with a hard wall-clock cap (SIGKILL on expiry) — the h32_cap discipline, never an in-process solver. No existing script was modified and nothing was committed. Builds on 2026-09-22-orient.md (§3–4: the unoriented cage, Theorem U, lemma (V)), 2026-09-21-laws.md (the cage, C and Pᵏ) and 2026-09-21-sheetcore.md (M′, the plaquette laws).

1. Verdicts

1. (V) has no small core in any direction (solver, L = 3, 4, 5). The deletion-minimal hexagon cores are thin but global: 89 of 432 hexagons at L = 3, 260 of 1024 at L = 4, 591 of 2000 at L = 5 for the nearest target — a fifth to a third of the lattice — yet they occupy every one of the 4L x-grids and every residue of both transverse circles. The same holds for a far target and for the “not type y” form. There is no window lemma to find.
2. Not a tube (solver, L = 3, 4, 5). With the x-circle left completely closed and the transverse plane cut instead, every proper transverse box is SAT: at L = 5 (box 20) boxes of radius 4, 6, 8 and even 9 — 1280 of 2000 hexagons, one transverse residue removed in each of y and z — leave “a type-x B-site on grid g+1” satisfiable; only the full transverse torus is UNSAT. Cutting a single residue in y alone (1600 hexagons) still kills the whole-grid form, though it leaves the one-site form forced. So (V) needs the x-circle and both transverse circles.
3. The x-support is an arc, never a bounded slab (computed, L = 4, 5). Scanning all windows [−a, b] of x-grids: (V) is forced exactly when (a ≥ 3 ∧ b ≥ 9) ∨ (a ≥ 6 ∧ b ≥ 6) ∨ (a ≥ 9 ∧ b ≥ 3) at L = 4, and (a ≥ 3 ∧ b ≥ 11) ∨ (a ≥ 8 ∧ b ≥ 8) ∨ (a ≥ 11 ∧ b ≥ 3) at L = 5. The middle corner is h101’s symmetric threshold 2L − 2, reproduced exactly; the two outer corners are new, and they are cheaper: the smallest windows that prove (V) have 13 of 16 grids at L = 4 (640 of 1024 hexagons) and 15 of 20 at L = 5 (1200 of 2000). The support is the circle minus a short arc: 3 grids of 16 spared at L = 4, 5 of 20 at L = 5. Two points are not a trend, but the support is in neither case a bounded slab — it is at least three quarters of the circle.
4. There is no bounded-x step, and nothing to induct on (solver, L = 4, 5). Two separate negatives. First, the pattern does not propagate: with yy/zz at O, the cage at O + 4e_x is forced to be straight (both rods type x) but its bridgehead pattern is completely undetermined — all four transverse patterns yy/yy, yy/zz, zz/yy and zz/zz are SAT on the full torus (only the patterns with a type-x bridgehead are excluded, and those follow from B being x-free). An unoriented cage does not force the next cage to be unoriented, so the obvious induction does not exist. Second, even the weaker statement “the next rod is type x” is not a bounded-x step: at L = 5 no proper x-window forces it, and the L = 4 window that does is again the 2L − 2 slab. The five statements V_near, V_any, V_planey, rod +6 and rod −6 all flip from SAT to UNSAT at exactly the same window.
5. (V) is not a linear identity, and not even an LP consequence (computed, L = 3, 4). Relax the type field to X[v, a] ∈ ℚ with one-hot and (T2) as linear equations. With the cage pattern and the target “b is type x” adjoined, rank(A) = rank([A | b]) at both L = 3 (557) and L = 4 (1365): the affine system is feasible. So is the LP relaxation 0 ≤ X ≤ 1 (HiGHS, both L). Since laws Task 5 showed the cage laws C, Pˣ, Pʸ, Pᶻ span the whole linear calculus, no combination of cage laws can prove (V). A hand proof must use the 0/1 condition combinatorially, as sheetcore’s F(i) + G(j) ∈ {0, 1} step does.
6. The hypothesis is four literals (solver, L = 4, 5; new). (V) does not need the yy/zz pattern. It needs exactly: both rods type x, one lower bridgehead type y, one upper bridgehead type z. Every proper subset of those four literals is SAT: rods alone, rods with one bridgehead, one rod with both single bridgeheads, the two bridgeheads with no rod. (The oriented pattern rods + yy + yy is SAT too, but that is a different pattern, not a weakening.) Which lower and which upper bridgehead is chosen makes no difference.
7. Theorem U holds under the same four literals (solver, L = 3, 4, 5; new). “Both rods x, one lower bridgehead y, one upper bridgehead z, and some hexagon odd” is UNSAT in 0.3 s, 2.9 s, 14.9 s — the same cost as the eight-literal version — with each of the three one-literal-weaker controls SAT. This is a strictly stronger Theorem U, and a much better hand target.

Theorem H is not proved, and (V) is not proved. §10 says what the proof shape now is.

2. Setting

Notation as in 2026-09-22-orient.md §3. On the (L, L, L) torus, box (4L)³ in a/4 units, fix an A-cage at O = a₀ + (2, 0, 0). Relative x-coordinates dx are measured from O. The cage’s rods (x-methylenes) are v = O − 2e_x at dx = −2 and v′ = O + 2e_x at dx = +2; the two lower bridgeheads are at dx = −1 (grid g+1 in the orient report’s labelling, g being v’s grid) and the two upper bridgeheads at dx = +1 (grid g+3). The unoriented pattern yy/zz is: both rods type x, both lower bridgeheads type y, both upper bridgeheads type z.

Lemma (V) is “under yy/zz, no B-site of grid g+1 is type x”, equivalently “grid g+1 is a complete type-y plane”. With the grid-count identity and the sublattice mirror of M′ it gives Theorem U. Targets below: near = the B-site of grid g+1 at relative position (−1, −3, 1), the closest non-bridgehead site of that grid; far = the transversally antipodal one.

The model throughout is the type-only model a4_typemodel.TypeModel: one-hot at every vertex and (T2) on a chosen set of hexagons. No bonds, no ice rule, no sign field.

3. Deletion-minimal cores (solver)

h110_ucore.py puts a selector s_h on each hexagon’s (T2) clauses, asserts the pattern and the target, takes CaDiCaL’s assumption core over the selectors, and then runs one destructive deletion pass with core refinement at every step (the h50_window.py pattern, inside one capped child). Minimality is verified afterwards: each single deletion is SAT.

“wraps” means every residue of that circle carries a core vertex, so the core has no transverse gap at all. The cores are not concentrated near the cage: at L = 4 the near-target core has between 6 and 24 vertices on each of the sixteen grids, thinning only slightly at the antipode (6, 8, 11 vertices on dx = −8, −7, −6 against 22–24 near the cage). These are deletion-minimal, not minimum, so the true minimum may be smaller — but it cannot be transversally smaller than §4 allows, and it cannot be longitudinally smaller than §5 allows, and both of those are global. The L = 5 profile is the same shape: 10 to 15 core vertices on the three grids nearest the antipode (dx = −8, −9, −10) against 40 to 44 on the grids nearest the cage, with every one of the twenty grids occupied.

4. No tube round the x-circle (solver)

h111_tube.py closes the x-circle completely (no x restriction on the hexagons) and cuts the transverse plane instead: (T2) only on hexagons all of whose vertices satisfy |dy| ≤ RTy, |dz| ≤ RTz. If (V) were a tube statement — a bounded cross-section carried round the circle — some bounded RT would be UNSAT.

Verdict. No proper transverse box works for the whole-grid statement. The one-site statement survives a one-residue cut in a single transverse direction (the 1600-hexagon rows) but not a one-residue cut in both, and not a two-residue cut in one. So (V) is a statement on the closed three-torus, not a tube round x. This also rules out proving (V) on an infinite slab or a transversally infinite cylinder and then specialising.

5. The shape of the x-support (computed)

h115_shape.py scans every window [XLO, XHI] of x-grids, with x measured forward from O so a window may run round the circle, and asks whether the hexagons inside already force (V). Write a = −XLO (grids below O) and b = XHI (above). U = UNSAT (the window proves it), S = SAT, . = the window is the whole torus. The matrices for the one-site and whole-grid queries are identical, so only one is shown.

L = 4 (box 16), query “some non-bridgehead B-site of grid g+1 is type x”:

  a\b   0   1   2   3   4   5   6   7   8   9  10  11  12  13  14
    0   S   S   S   S   S   S   S   S   S   S   S   S   S   S   S
    1   S   S   S   S   S   S   S   S   S   S   S   S   S   S   U
    2   S   S   S   S   S   S   S   S   S   S   S   S   S   U   .
    3   S   S   S   S   S   S   S   S   S   U   U   U   U   .   .
    4   S   S   S   S   S   S   S   S   S   U   U   U   .   .   .
    5   S   S   S   S   S   S   S   S   S   U   U   .   .   .   .
    6   S   S   S   S   S   S   U   U   U   U   .   .   .   .   .
    7   S   S   S   S   S   S   U   U   U   .   .   .   .   .   .
    8   S   S   S   S   S   S   U   U   .   .   .   .   .   .   .
    9   S   S   S   U   U   U   U   .   .   .   .   .   .   .   .
   10   S   S   S   U   U   U   .   .   .   .   .   .   .   .   .
   11   S   S   S   U   U   .   .   .   .   .   .   .   .   .   .
   12   S   S   S   U   .   .   .   .   .   .   .   .   .   .   .

L = 5 (box 20) has the same shape with corners (3, 11), (8, 8), (11, 3).

Three thresholds, not one. The middle corner a = b = 2L − 2 is exactly h101’s symmetric slab threshold, reproduced independently. The two outer corners — (3, 9) and (9, 3) at L = 4, (3, 11) and (11, 3) at L = 5 — are new: a window that reaches only three grids below the cage but far round the other way also proves (V). Two values of L are too few to fit a formula to the outer corners; what is clear is that they are strictly cheaper than the symmetric slab at L = 5 and equal to it at L = 4. The smallest windows that prove (V) are therefore 13 of 16 grids (L = 4) and 15 of 20 (L = 5), not 2(2L − 2) + 1 = 13 and 17. In particular the minimum shrinks below the symmetric slab at L = 5, and the arc that can be spared is 3 grids at L = 4 and 5 at L = 5 — it grows, but far slower than the circle.

Reading. The forcing is not a wave that leaves the cage in both directions and meets at the antipode: a window that reaches 9 grids one way and 3 the other proves (V) at L = 4, while the symmetric 5-and-5 window does not. What matters is the total arc and a minimum reach of 3 on the short side — i.e. enough room to pass the cage’s own five grids [−2, 2] and one grid beyond the lower bridgehead.

6. No one-step statement (solver)

h112_step.py takes x-slabs of 2, 3 and 4 cages and the full torus, assumes yy/zz at O, and reports the backbone over the ten sites of each cage (rods, four transverse methylenes, four bridgeheads) together with a scan of the nine straight patterns for the cage at O + 4e_x.

(The 3-cage slab is 13 of 16 grids, i.e. the 2L − 2 threshold again — see §5 — so its extra forcing is not a bounded step. On the slabs a cage may still have type-x bridgeheads; only the closed torus excludes xx/xx, and that is just B being x-free.)

The bridgehead pattern of the next cage is not determined — at all. On the full torus the cage at O + 4e_x may be unoriented (yy/zz, zz/yy) or oriented (yy/yy, zz/zz). There is therefore no invariant of the form “cage j is unoriented ⇒ cage j+1 is unoriented” to induct on. This is consistent with Theorem U rather than in tension with it: U concludes curl-free, and curl-free states are full of oriented cages.

What is forced everywhere is weaker and already known: the whole A x-line through v is type x, every B-site is non-x, and each cage’s four transverse methylenes are non-y / non-z (the six methylene exclusions, which are law C applied to a straight cage and are provable by hand).

And the surviving candidate for a step — “the far rod of the next cage is type x” — is itself x-global. h113_prop.py at L = 5 tried the windows [−2, 6] … [−6, 10] for six starting patterns (yy/zz, zz/yy, yy/yy, zz/zz, rods only, one rod only): every one is SAT until the window becomes the whole torus. h114_thresh.py then measured five consequences of yy/zz on one scale:

They flip together. The continuation of the x-line is exactly as global as (V) itself, so “propagate along the line, then close up” is not available as a proof strategy: the propagation step is the theorem.

7. (V) survives the affine and LP relaxations (computed)

h116_linear.py relaxes the type field: variables X[v, a] ∈ ℚ, one equation Σ_a X[v, a] = 1 per vertex and one equation Σ_{v ∈ h} X[v, α_h(v)] = 2 per hexagon — (T2) verbatim as a linear equation. Ranks are computed exactly by Gaussian elimination modulo 2³¹ − 1; the LP is HiGHS.

Consequence for a hand proof. laws Task 5 established that C and Pˣ, Pʸ, Pᶻ on every cage of both kinds span the whole linear calculus of the type field, and that integrality adds no linear relation. Adding the target raises the rank by exactly one and keeps the system consistent, so the negation of (V) is linearly consistent with all of them. No rational combination of cage laws is a certificate for (V). Any hand proof must at some point use 0/1 or one-hot as an inequality or a case split — the way sheetcore’s sheet theorem uses f(i, j) = F(i) + G(j) ∈ {0, 1} to force F or G constant. This is the single most useful negative result here: it rules out the linear-algebra-round-the-torus route that §5 of the orient report suggested.

8. The near-miss (computed)

h117_defect.py takes a window one grid short of the threshold (L = 4, [−6, 5], 576 of 1024 hexagons), asserts yy/zz and a type-x B-site on grid g+1, and describes a model. This is what a hand proof has to exclude.

• Every constrained grid carries exactly 8 type-x sites out of 32 — both sublattices, all twelve grids of the window. The unconstrained grids (dx = +6 … +9, beyond the window) are uniformly type z: the structure simply stops at the gap.
• The A x-line through v is x at dx = −2 and +2 and breaks at both ends of the window: type z at dx = +6 (inside the gap) and type y at dx = −6 (the window’s lowest grid, which almost no complete hexagon reaches).
• On each B-grid the type-x sites lie mostly on one diagonal line y + z = const — 4 to 6 of the 8 — and that constant drifts by +2 per B-grid: −5 → 10, −3 → 12, −1 → 14, +1 → 0, +3 → 2, +5 → 4. The counterexample is a tilted kink sheet spiralling along x.
• 192 of the 576 constrained hexagons are odd: the near-miss is not a curl-free state with a blemish, it is a thoroughly odd window state.

So the obstruction (V) expresses is the closure of a tilted sheet round the closed three-torus. In a window the sheet can enter, drift, and terminate in the gap; on the closed torus it must come back to itself, and the cage at O pins the phase it would have to return to. Because the sheet is tilted, closing it needs the transverse circles as well as the x-circle — which is exactly what §4 measures. That is a genuinely global, genuinely integral statement, matching §4, §5 and §7.

9. The minimal hypothesis, and a stronger Theorem U (solver)

h118_weaken.py runs every sub-pattern of yy/zz on the full torus. Results are identical at L = 4 and L = 5.

Lemma (V′) (solver, L = 4, 5). Let v and v′ = v + 4e_x both be type x. Let b be a B-neighbour of v one grid above v (dx = −1 relative to the cage centre) with τ(b) = y, and b′ a B-neighbour of v′ one grid below v′ (dx = +1) with τ(b′) = z. Then no B-site of b’s grid is type x, and b’s grid is a complete type-y plane.

Both b and b′ lie strictly between the two rods. Four literals, and every proper subset of the four is satisfiable — so this is the minimal hypothesis in the strongest sense the solver can certify. In sheetcore’s plaquette language it reads: a plaquette of an A-grid whose two A-middles m, M are both type x, with one column-edge B-vertex of type y and one row-edge B-vertex of type z, forces the column-edge grid (g − 1) to be x-free.

h119_minU.py checks that Theorem U itself holds under the same four literals:

Theorem U′ (solver, L = 3, 4, 5). A frozen state containing an A-vertex pair v, v + 4e_x both of type x, with a type-y B-neighbour of v above it and a type-z B-neighbour of v + 4e_x below it, is curl-free.

This costs the solver exactly what the eight-literal version cost, so nothing was lost by weakening, and it is a strictly better hand target: the hypothesis is now four sites in one plaquette rather than a whole cage pattern.

10. What the proof shape is, and what remains

What (V) is not. It is not a window lemma (§3), not a tube round the x-circle (§4), not a bounded-x induction with a closure contradiction (§6 — the induction hypothesis does not exist, because the next cage’s bridgehead pattern is free), and not a linear consequence of the cage laws (§7). All four of the natural routes are closed by computation; the orient report §4 left the core uncomputed and named the first three as the obvious things to try.

What it is (conjecture, from §8). The mechanism looks like the closure of a tilted kink sheet round the closed three-torus. The near-miss configuration at L = 4 is a (T2)-consistent sheet of 8 type-x sites per grid whose transverse phase drifts by a fixed amount per grid; the hypothesis (V′) pins the phase at one plaquette; and the contradiction would be that the drift cannot return the sheet to that phase after 4L grids. That last step is a conjecture — the drift was measured in one model at one L — not a computed fact. But it is the same kind of argument as sheetcore’s sheet theorem — a conserved local quantity, integrated round a circle, with an integrality step that splits a two-variable function into F(i) + G(j) — but it must run round the x-circle as well as the transverse ones, which no lemma in the project does yet.

The hand proof therefore needs, in order:

1. A phase invariant for the kink sheet along x. Sheetcore’s plaquette law already says the mixed second difference of the B-kink indicator on the transverse lattice equals [m type x] − [M type x], with m, M the A-middles two grids away. Under (V′) both middles of the plaquette at O are type x, so that source vanishes there. The missing object is the quantity that is conserved as one steps from B-grid to B-grid in x, and whose value the drift in §8 measures. It should be an F(i) + G(j) decomposition carried along x, not within a single grid.
2. The integrality step. Whatever that invariant is, §7 guarantees it cannot be derived by summing cage laws with rational coefficients. The 0/1 condition must enter, as it does in sheetcore §3, where F(i) + G(j) ∈ {0, 1} forces one of F, G constant.
3. The closure contradiction. The invariant must fail to close after 4L grids, given the phase (V′) pins. §5’s asymmetric thresholds say how much room the closure needs, and it is less than h101’s symmetric slab: 13 of 16 grids at L = 4 and 15 of 20 at L = 5, in windows reaching only 3 grids below the cage.

Two concrete next computations, if the route is pursued:

• Identify the drift invariant numerically. Take the near-miss models of §8 at several window sizes and several L, and fit the per-grid transverse phase of the type-x set; then test whether the fitted invariant is forced on the full torus by a backbone query. If the drift is always ±2 per B-grid, that is a two-line hand lemma waiting to be found.
• Check whether (V′) has a sign-free counterpart with the ice rule restored. Everything here is type-only; if the bond-level model makes the invariant visible as a flux, the closure argument may be easier there.

What this does for Theorem H. Nothing directly — H still reduces, via U′ and the hand corner case, to “oriented loops + a corner ⇒ some direction missing”. But Theorem U′ is now a four-literal hypothesis with a fifteen-second solver proof at L = 5, and the obstruction to a hand proof is isolated to one missing object: a conserved transverse phase for the kink sheet along x. That is a narrower target than the orient report left.

11. Computations run

All from scratch_h with the project .venv, PYTHONPATH=<repo>:<repo>/experiments/08_frozen_structure, TMPDIR=.tmp; every solve in an h32_cap-style child with a hard SIGKILL cap. Wall-clock is the whole invocation unless noted.