Independent check of H ⇐ K_u + Lemma O + (R⁺) + (S≥1): confirmed with corrections (no gap; one mis-cited input, one unexercised case, two standing remarks)

Verdict: CONFIRMED WITH CORRECTIONS. Every proof in rphand §1–§4 and in the two borrowed theorems (Theorem D, w1prime §4; Theorem LC, wprime §2) is complete for the hypotheses it states. I found no gap. The corrections are to a citation and to how the inputs’ standing is worded; none changes the reduction.

Scripts (new, mine): scratch_h/h270_cage.py (cage check from the definitions, no geometry imported), h271_corpus.py (corpus audit; imports only Cell, eps_from_types, load_odd_corpus), h272_sat.py (solver attacks; own encoding of one-hot, (T2), bond rule, oddness, three types and the three laws as switchable constraints; every solve through h32_cap). No existing file was modified. Nothing was committed. Everything ran on this Mac, one solver process at a time.

1. Statement-by-statement audit

Specific points the brief asked about:

• (S) where only (S≥1) was assumed. (S) is used in the stripe theorem (PQ = 0) and in RP₁ step 2. In both places Lemma O is also assumed, and (S) = Lemma O at straight holes + (S≥1) is exact. No illegitimate use.
• Lemma O at holes whose orientation was not established. Every use is inside “odd, Lemma O” (all holes). Lemma E’s one-sided case uses none, which matters because Case 2 relies on it.
• Index sets. The two-product lemma is applied to (h ± s)/2 on the S k-lines, indexed by (x_i, x_j) ∈ (S-parity)²: a full product. Case 2 applies the zero-set argument to LC counts on the same index set.
• Sublattice and side bookkeeping for Theorem D. A B-plane F is carried to an A-plane by the inversion v ↦ (1,1,1) − v. The lower side is carried to the upper by a two-coordinate flip, for example (x,−y,−z) with y the normal: I checked that it maps A to A, B to B (since (1,1,1) ↦ (1,−1,−1) = d₁) and the bond set to itself. Both maps preserve types and (T2). The needed (E′) on the lower side is supplied by Lemma E, which gives both sides.
• “three types” and “odd” where D(iii) uses S1 and M′. Available in RP₁ and Theorem W by hypothesis. In the Corollary the two-type case is split off before Theorem W is invoked. The solver shows both hypotheses are genuinely needed (§3.3: D’s negation is SAT without either).

2. Corrections and remarks

2.1 Correction: the Corollary cites Lemma A for the absent-type case

rphand §4 says: “If a type is absent, Lemma A.” The synthesis (§1) lists “Lemma A (two-type states)” among the proved inputs. The Lemma A of record (docs/frozen-structure-2026-09-05.md, “a missing type forces a half-box period”) concludes a translation invariance, not an absent direction. The trails report’s Lemma A is unrelated. Repair: none is needed, because a missing type k is an empty axis k and both ±e_k are absent, so the case falls under the next sentence (“if some axis is one-way or empty”). Delete the Lemma A clause from the Corollary, and delete Lemma A from the synthesis’ list of inputs. (Lemma A is still needed for the periodicity conjecture from H, but not for H.)

2.2 Theorem W, Case 1: the cyclic argument

I re-derived it and checked it as written on the corpus (h271, “W1” rows):

• the S-stripe direction exists;
• 1. holds;
• (ii) holds: every plane along n, of either sublattice, has at most one label;
• the construction (a + S-plane c₁, the next non-empty S-plane a − plane c₂, c* the last + plane in [c₁, c₂), c** the first non-empty plane after it) always gives a − plane c** with c** ≥ c* + 2;
• F = c* + 1 is on the wall list.

Adjacency is excluded in each of the three possible parities of (c*, c**), by (i) or its mirror, so F is k-free. Its neighbours are c* (+) and c* + 2 (0 or −), as claimed. No correction.

2.3 Remark: Case 2 of Theorem W is vacuous in every tested setting

No two-way axis in the corpus is in Case 2 (807 / 807 and 1007 / 1007 two-way axes are Case 1). With my encoding, “z two-way, A’s type-z vertices all +, B’s all −” is UNSAT under the three laws as constraints (L = 3: 0.15 s; L = 4: 0.89 s), and also under odd + three types alone (0.14 s; 0.30 s). The written argument for Case 2 is correct, so this is not a gap. It does mean the case has no data behind it. It is probably provably empty (from (R⁺) and Theorem Ω, say), which would shorten the proof. I have not proved that.

2.4 Standing of the inputs (task 5)

• Lemma O in odd states ⇐ Theorem U + corner case + cage enumeration: confirmed. My independent cage enumeration (h270, sign form) gives:
  • 1104 of the 1200 (T2) patterns of a cage are oriented;
  • the 96 unoriented ones are all straight;
  • for rod axis r they are exactly the patterns whose two bridgeheads on one r-side have one transverse type and the two on the other side have the other type (16 per ordered pair, for each of the three axes);
  • no corner cage is unoriented, so the corner case also holds cage-locally.
  This is orient §3’s statement, with the side grouping made explicit. The straight case then needs Theorem U, whose standing is solver-only at L = 3, 4, 5 with hand residue (V). My own sign-form query (“adjacent type-z vertices on one line with opposite signs”) is SAT without oddness and UNSAT with it: L = 3 in 0.07 s, L = 4 in 1.62 s.
• (S) = Lemma O (straight holes) + (S≥1): confirmed (§1).
• (R⁺) and (S≥1) hold without oddness at L = 3, 4: confirmed with my own encoding (§3.3).
• Wording to reconcile. rphand §0 says Lemma R gives “the first two members” of (R⁺). rphand §9 and the synthesis say it gives “k-separation ≤ 3”. One of the two should be corrected; I did not audit Lemma R.
• K_u’s scope. rphand calls K_u simply “certified”. The attack proposal records it as certified modulo Lemma L and the scope of the window certificates (a ≥ 3 and b, c ≥ 4, with the small cells by torus verdicts). The Corollary’s “H” inherits that scope. I did not audit K_u, as instructed.

3. Independent computations

3.1 Cage check of Lemma sP (h270_cage.py, 0.38 s)

• Model: the ten cage vertices, the four hexagons found by searching all (A-hole, σ) whose six vertices lie in the cage, the twelve bonds, and (T2) as “exactly two of [τ(a_k) = k], [τ(b_k) = k]”. The bond rule is solved by propagation.
• Results, identical for A- and B-cages:
  • 1200 (T2) patterns;
  • law C 1200/1200;
  • P^k 3600/3600;
  • bond rule consistent in all 1200;
  • 1104 oriented patterns, 0 sP violations;
  • 96 unoriented patterns, exactly 3 violations each (288).

3.2 Corpus (h271_corpus.py; L = 3: 637 states, 2.8 s; L = 4: 720 states, 6.8 s)

A chain is the component of a vertex in the 2-regular bond graph between two adjacent planes, computed directly rather than from Lemma 1’s formula. Every chain had 4L vertices. The two-type failure counts reproduce rphand §6’s 14 244 and 31 344 exactly.

3.3 Solver (h272_sat.py, CaDiCaL via h32_cap)

A three-type state is required only where marked “three”. “Laws” means Lemma O at every hole, faithful (S≥1) (no type-k vertex between, at least one vertex between) and (R⁺), all imposed as clauses, with no oddness.

Reading:

• No intermediate statement could be broken. Every counterexample query that the reduction predicts to be UNSAT came back UNSAT, each with a satisfiable control, except the L = 4 wall query, which is undecided at the 540 s cap. At L = 3 that query is UNSAT with the laws as constraints and no oddness. The existence of the wall therefore rests on the laws alone, as the proof says, not on oddness.
• Lemma E needs orientation exactly in its two-sided case.
• Theorem D needs both oddness and three types, as §6 of rphand says.
• A side observation: at L = 3, Lemma O alone (as a constraint) already forces the wall. This does not bear on the proof.

Not run: the L = 5, 6 samples of rphand §7, and the L = 4 wall query beyond 540 s, which would need more than the 10-minute foreground budget.