Oriented loops: in every odd frozen state the moment signs orient the rod loops (one rod in, one out at every hole), and this fails in curl-free states; the unoriented hole is a type-only pattern (a straight cage with bridgeheads yy/zz), and Theorem U — one such cage forces the opposite sublattice x-free, hence the state curl-free — is solver-true at L = 3, 4, 5 in seconds. Also: the loops report’s wall picture withdrawn; corner counts; the sign field is always a function of the type field

Status tags as in the note: proved, computed, solver, conjecture. Scripts scratch_h/h80–h102 (main loop). Sequence date 2026-09-22 (wall clock 19 Sep). Builds on 2026-09-21-loops.md (rod loops), -laws.md (cage theorem), -sheetcore.md (M′), -sheetcurl.md ((B), Lemma S1).

1. Corrections and small facts

The wall picture of the loops report §2 is withdrawn (computed, h80_diamonds.py). Only the hole-centred half of the projected unit squares carries a cage law; the A-site-centred squares take every value in [−2, 2] on the odd corpus (516/537 at ±2 at L = 3). A mixed-difference constraint on a checkerboard of squares has a large kernel (an isolated 2 × 2 block at the right parity satisfies it), so there is no wall system and §5 item 2 of that report is void. The correction is written into the report itself.

Corner counts (computed, h80, h81, h82). On every odd state #corners_A = #corners_B = #odd hexagons / 2 (as the cage picture predicts: a corner cage has one A-odd and one B-odd hexagon). The minimum is 4L per sublattice (12 at L = 3, 16 at L = 4). The minimal states are two-type states: all A-corners in one z-layer of A-holes with x/y legs (two winding loops of six corners each), all B-corners in the adjacent layer; type z absent, so H’s hypothesis fails trivially. Two-axis states have corner counts that are multiples of 4L; three-axis states start at 22 and are irregular. Corners do not come in lines along the third axis (h81, ~40 %).

The sign field is a function of the type field (computed, h94_signcount.py). For every type field tested — odd, curl-free, and the counterexample below — the number of bond states with that type field (ice + frozen) is exactly 2 (global reversal). This is the Z₂ chain-sense system: one sense bit per x-chain, one equation per vertex, connected incidence graph; every sign statement below is therefore secretly type-only, and the solver’s add_sign_field is that system.

2. Lemma O: the loops are oriented — in odd states only

Orient each rod by its vertex’s moment (the in-pair). At a hole O with rods at O ± 2e_k, a rod points away from O iff its sign equals its side.

Computed (h83_orient.py, h93, h95). On the 132 sign-carrying corpus states (32 at L = 3, 100 at L = 4, all odd) every hole of both sublattices has exactly one rod pointing away: 0 exceptions in 58 112 holes. On diversified random frozen samples (random assumptions on 12 bond bits, two seeds, 77 samples): every odd sample (62) obeys it with 0 bad holes; every curl-free sample (14) violates it, with 48 or 72 bad holes at L = 3.

Solver. On the (3,3,3) torus (bond model, ice + non-flippable, h85, h91): “β = 0” and “β = 4” at one hole are SAT (β = number of radial cage bonds directed A→B; β = 2 is the oriented case, and β odd is UNSAT already on the cage by the ice count a = β/2). The model is a genuine frozen state (432 hexagons with two matches) and is curl-free, with 48 + 12 bad holes. With “some hexagon odd” added (h96), β = 0 and β = 4 are UNSAT (192 s, 261 s; control SAT). So:

Lemma O (solver, L = 3; computed on 194 odd states at L = 3, 4). In an odd frozen state every hole has one rod pointing toward it and one away; the rod loops of both sublattices are oriented closed curves. Consequences (proved from the lemma): each loop’s winding vector is canonical; Σ_loops w = M_S / L for each sublattice; and M_A = M_B in every ice state (proved directly: along any chain, sources and sinks alternate and lie on alternating sublattices).

Proved by hand: the corner case. At a corner cage the two rods lie in one hexagon, which is odd with both matches on the rods; a hexagon’s two flow reversals are one source and one sink, so one rod points toward O and one away. The whole content of Lemma O is therefore the straight case: consecutive kinks v, v + 4e_k on a k-line have equal moment sign (a straight x-cage is oriented iff m(v) = m(v′), by the radial count).

Stronger, with gaps (computed, h89). On all 132 corpus states every k-line’s type-k sites share one moment sign, gaps included (0 mixed lines among 10 000+ with ≥ 2 kinks at L = 4); on the curl-free samples 24 or 36 lines per state are mixed, each with exactly two sign changes. Bonded-kink adjacency does not explain it (h90: the kinks of a line lie in one component of the bonded-kink graph in only 84 % of lines).

3. The unoriented hole is a type-only pattern (proved, computed)

Bit calculus (proved): bit(e) = 1 iff bond e is directed A→B; along a path, at a vertex u entered by e and left by e′, bit(e′) = bit(e) ⊕ [τ(u) ≠ axis(e, e′)] (the two hexagon bonds of a match carry equal bits). For the straight x-cage with rods v = w_x^−, v′ = w_x^+, lower bridgeheads β, β′ (grid g+1, v’s row-neighbours) and upper γ, γ′ (grid g+3, v′’s column-neighbours), a path v–b–w–b′–v′ gives m(v) = m(v′) iff q = [τ(b) = axis_b] + [τ(w) = axis_w] + [τ(b′) = axis_b′] is even.

Computed (h97_cage_orient.py, all 3⁸ assignments of the cage under (T2) on its four hexagons, 144 patterns; the four paths agree on every one). The straight x-cage is unoriented iff its bridgehead pattern is yy/zz or zz/yy: both lower bridgeheads of one transverse type and both upper of the other. Every other (T2) pattern (xx/xx, yy/yy, zz/zz, xy/yx, yx/xy, xz/xz, zx/zx) is oriented. A hand-built yy/zz cage satisfies ice + (T2) on its four hexagons, and the solver keeps it SAT on balls of radius 6 (h84, h87): the lemma is not cage-local.

4. Theorem U (solver, L = 3, 4, 5): an unoriented cage forces curl-free

Type-only model (one-hot + (T2)), the cage at O fixed, h98_unoriented.py:

Theorem U (solver). A frozen state containing a straight cage with an unoriented bridgehead pattern is curl-free. With §3 and the corner case, Lemma O for odd states follows: odd ⇒ no unoriented cage ⇒ every hole oriented.

What the pattern forces (computed, backbone h99, enumeration h102). Under yy/zz at one A-cage on the (3,3,3) and (4,4,4) tori: the whole A x-line through v is type x; the entire B-grid g+1 is type y and the entire B-grid g+3 is type z; every B-site of the torus is non-x; nothing else on A is forced. The full family at L = 3 has 1008 type fields: in every one all six B-grids are monochromatic (y or z), B is x-free, A is x plus one of y, z, and there are no corners — the n_B = 0 curl-free world. So U factors as

yy/zz ⇒ (V) B-grid g+1 is x-free ⇒ (grid-count identity) B has no type x ⇒ (sublattice mirror of M′, with the A-kink v; proved) curl-free,

and the new content is (V), equivalently “yy/zz ⇒ B-grid g+1 is a complete type-y plane” (Lemma S1 then gives B x-free directly).

(V) is x-global (computed, h100, h101). On transverse boxes of radius up to 9 with x-extent up to ±6, yy/zz forces nothing beyond the cage’s own six methylene exclusions. On x-slabs with the full transverse torus, “some B-site on grid g+1 is type x” (and “not y”, and the g+3 mirror) is SAT up to |dx| ≤ 2L−3 and UNSAT from |dx| ≤ 2L−2 at both L = 4 and L = 5: the slab must contain all hexagons except those meeting a three-grid gap at the antipode. (The “light cone” seen in h100 at RX = 5, RT = 10 on L = 5 is a closed-transverse-torus effect — RT = 10 is the whole plane there; agent uhand shows nothing at all is forced until every transverse plane is present, and agent ucore that (V) needs the closed three-torus: no window, no tube, no bounded-x step, and no linear certificate. See 2026-09-22-ucore.md, -uhand.md.)

5. What this does for Theorem H

Not a proof. What changes:

• H ⟺ [odd ⇒ some direction missing]. By U (solver) and the hand corner case, every odd state has oriented loops, so the missing step is: oriented loops + a corner ⇒ some direction missing, i.e. some axis k on which every k-rod of both sublattices points the same way. On the fair samples every odd state does miss a direction, three-axis states miss at most one sign per axis; every curl-free sample has all six directions and unoriented holes. (An earlier version of this sentence claimed the absent set is the same on A and B; on the full corpus it differs in 38/637 and 32/720 odd states — agent extremal — so that claim is withdrawn.)
• In an odd state the winding vector of each loop is an invariant, and the line-sign law (§2) says each k-line carries one sign. H’s contrapositive is then: some axis has all its lines of one sign. That is a statement about the type→sign function, which the linear calculus does not see; it is the global object the loops report asked for.
• Theorem U is a rigidity theorem of M′’s kind (one local pattern ⇒ a sheet), solver-true in seconds where H takes hours, so it is the natural next hand target: a proof of (V) on the x-circle would be the first hand proof of an x-global statement in this project.

5a. Later the same session: the sign half of H is type-only in odd states (computed)

• α_k ⟺ one-way (computed, h104_alpha.py, 132 odd sign states, 0 exceptions). Say axis k satisfies α_k when on every k-chain consecutive kinks (type-k sites with no type-k site between them along the chain) lie on opposite sublattices. One-way ⇒ α_k is proved (an A-kink is +k iff it is a source of its chain, a B-kink +k iff a sink, and sources and sinks alternate). On every odd state the converse holds too: α_k with type k present ⟺ every k-rod has one sign. On a curl-free state it fails (one case). On the type corpus every odd state with all three types present has an α axis (396 + 116 of 637 at L = 3; the 125 without are two-type states).
• So, modulo “α ⇒ one-way in odd states”, H ⟺ H_α: all three types present ∧ every axis has a chain with two consecutive same-sublattice kinks ⇒ curl-free — a type-only statement. Solver (h105_halpha.py, type-only, L = 3): the negation did not finish in 600 s; H_α is H-hard, as it must be, so this is a reformulation, not a cheaper target.
• Adjacent uniform chains agree (computed, h106_chainpairs.py). In odd states, two kinked chains of one family joined by a bond (rows in slabs g and g+2 sharing a column bond), each uniformly signed, always agree: 0 exceptions in 2 968 + 15 922 pairs. Another coherence law of Lemma O’s kind, and the mechanism behind α ⇒ one-way.
• Negative (computed, h103, h107, h108). One-way is not bond-connectivity of the type-k set (one-way axes with up to 21 components; two-way with 2). One-way is not “no loop turns back in k”: two-way axes with no turn-back loop exist (12 / 40 cases), so the disagreement lives across loops. The relative sign of a two-way axis’s kink against a one-way axis’s direction is not a radius-1 local function of the types (85–90 % of kinks in sign-determining neighbour patterns, the rest mixed).

Reading. In odd states every sign relation examined (adjacent kinks on a line, a whole line, adjacent chains, α ⇒ one-way) is coherent, and every one fails in curl-free states. Theorem U is the first of these turned into a type-only rigidity theorem. H’s sign half is the same phenomenon at the scale of a whole axis: for some k the coherence covers every k-kink.

6. 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 child (SIGKILL at the cap).