CLAIM: global rank-8 rigidity on P111 and type-(4,4) P104 units (completes #1212 §10 two gaps)

[JosieElliston]

CLAIM: global rank-8 rigidity on P111 and the 28 type-(4,4) P104 units (JosieElliston, with Claude via Claude Code). Expires 2026-10-14T02:30Z.

Question. PR #1212 (burntout76, head 57099cb5) proves that in the E-graph model every rank-≤8 solution of (E) is D(2G)D^{-1} on P112, P120 and the 336 type-(2,2,2,2) P104 units. Its §10 records two remaining gaps. On P111, one class keeps three live rows and its block has no complete class. On the type-(4,4) P104 units, two blocks carry no live class, so Lemma 6's cocycle step has no witness. Does Theorem 1 (and with it the eight-costly-term floor, 63 on P111 and 56 on (4,4)) hold there?

Method. Two written lemmas:

• a three-row Lemma 5, which gets the b side from the character argument H_3 diag(γγ') H_3^T diagonal ⇒ γγ' constant, in place of Lemma 3's inverse;
• a gluing lemma that needs only every pair to lie in a usable block and an explicit path condition on the triples. It is multiplicative, so it holds over any field, not just as a rank statement.

The finite inputs come from a new standard-library checker on #1212's pivots. Zero exclusion (#1212's Lemma 8 and its DRUP proofs) is cited and replayed, not re-derived.

Scope. Card complex-masked-decoder (chooser nonce 118c1c4d3856655a6b7cb222d8d50aef), scope refined to this proof obligation. Base bce54fb3. Not covered: the 896 admissible P104 units (two-row classes), nine or more costly terms, and any construction or κ.

Overlap. This is the "smallest next step" named in #1212's handoff in #1166. #1292 (Navinor) is local, tangent-space only. Expected artifact: a stacked research package plus a PR.

[JosieElliston]

DONE: #1389 (head 5480912a, base bce54fb3). Claim released.

Finding. PR #1212's Theorem 1 (rank-≤8 solutions of (E) are D(2G)D⁻¹) holds on all 112 P111 units and all 28 type-(4,4) P104 units. Two lemmas close the gaps:

• Lemma 5′ handles three-row classes. The b side follows from the three pairwise sign products spanning the non-trivial characters.
• Lemma 6′ is a gluing lemma. It needs only connectivity plus an explicit three-triple path, is multiplicative, and works with 12/14 usable blocks.

Consequence: in the E-graph model, eight-costly-term decoders have cst ≥ 63 on P111 (sharp) and ≥ 56 on type (4,4).

Zero exclusion is #1212's, replayed from blob-pinned files with --pr1212-dir. The independent verifier runs 26 checks and 4 controls.

Open: the 896 admissible P104 units, which have two-row classes. In-class relations provably leave freedom there, so a two-row Lemma 5 has to use the cross-block relations (5).