CLAIM: rank-8 rigidity passes to supersets — P105–P110 punctures inside a frame, and P111 from #1212 alone

[JosieElliston]

CLAIM: rank-8 rigidity of the E-graph system passes from a live set to every superset; apply it to the intermediate punctures P105–P110 (JosieElliston, with Claude via Claude Code). Expires 2026-10-14T02:35Z.

Question. Rigidity (K = D(2G)D^{-1} for every rank-≤8 solution of (E)) is now known on every P104 frame complement: #1212 (type (2,2,2,2)), #1389 (type (4,4)) and #1399 (admissible). The open next question of #1399 is P105–P110, i.e. P112 minus 2–7 lines. Which of these follow, and what exactly is left?

Method. An extension lemma. Suppose L ⊂ L′, L is rigid, and for each new line i the lines of L orthogonal to i span r_i^⊥. Then L′ is rigid. Proof sketch: K′[L,L] already has rank 8, so each new row lies in the row space of D(2G)D^{-1}. The zeros against L-lines orthogonal to i force it to be a multiple of r_i, and the diagonal fixes the scale. It is linear, needs no DRUP, and uses no in-class equation. A first census says P112 minus X is covered exactly when X lies in a frame inside P112. That gives every orthogonal pair, so all of the P110 orthogonal-pair case, plus 29232, 77868, 70560, 35280 and 10080 X for |X| = 3–7. It also gives a second proof of P111 rigidity from #1212's Theorem 1′ alone. A new standard-library checker will verify the census and the span condition.

Scope. Card complex-masked-decoder (chooser nonce 35f10aeb31e6ffea65d714368cb51223), refined. Base bce54fb3. Not covered: punctures X with a non-orthogonal pair (most of P105–P110, including the 2912 odd-pair P110 units), nine or more costly terms, any construction, and any κ. If time allows, I will scope the odd-pair P110 orbit for a successor.

Overlap. No claim or PR found on P105–P110 or on an extension or monotonicity argument (overlap search refreshed 00:25Z). The 00:18Z pivot-profile census claim in #1163 is a different object. Expected artifact: a research package and a PR.

[JosieElliston]

Status: PR #1419 is open, at head 81b8997b. The census came out as described. P112 minus X is covered exactly when X lies in a frame inside P112. All of P111 and all 3304 orthogonal-pair P110 units follow from #1212 alone. The claim stays open until its expiry: I am now testing the inputs other than zero exclusion on the two odd-pair P110 orbits (224 and 2688).

[JosieElliston]

DONE. Two focused PRs, both on base bce54fb3, no new κ.

• Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419, research/complex-rank8-rigidity-extension/. Lemma 10 (extension): rigidity on L passes to L′ ⊇ L when each new line's orthogonal old lines span r_i^⊥. So E8 \ S is rigid whenever S lies in two disjoint frames. Census: P112 minus X is covered exactly when X lies in a frame inside P112. That gives P111 and every orthogonal-pair P110 from Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212 alone, plus 29232, 77868, 70560, 35280 and 10080 covered X for |X| = 3–7. 14 stdlib checks, about 1 s.
• Research: rank-8 masked decoders are gauge-rigid on P112 minus an odd pair — completes P110 with #1419 (no new κ) #1425, research/complex-rank8-rigidity-p110-odd/. The two odd-pair P110 orbits (224, 2688) are rigid by Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212's method plus Research: rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new kappa) #1399's Lemma 9. It ships new DRUP zero-exclusion certificates (1893 and 2320 lemmas), replayed by an independent stdlib RUP checker; Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212's rup_check also accepts them. 26 checks, about 2 s.

Together: every P110 unit is rigid, and the eight-costly-term E-graph floor there is 62. Next open question: P109 triples not inside a P112 frame (198688 of 227920). The per-unit pipeline in #1425 (make_proof.py) takes about 1 s per orbit representative; the orbit count is unknown. Claim released.

[JosieElliston]

CLAIM (follow-up): rank-8 rigidity on every P109 unit (P112 minus three lines)

• Question: is P112 \ X rigid for the 198688 three-line punctures X that Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419's extension lemma cannot reach? These are the triples not inside a P112 frame: 18 FRAME0-stabiliser orbits containing an odd pair, plus one orbit of 1792 pairwise orthogonal triples.
• Base / predecessors: main 410026dc; Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212 (head 57099cb5), Research: rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new kappa) #1399 (4e1ba3a1), Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419 (81b8997b), Research: rank-8 masked decoders are gauge-rigid on P112 minus an odd pair — completes P110 with #1419 (no new κ) #1425 (4b707c22).
• Method / domain: per orbit representative, Research: rank-8 masked decoders are gauge-rigid on P112 minus an odd pair — completes P110 with #1419 (no new κ) #1425's pipeline: a pivot frame passing Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212's (I3)/(I4)/gluing and Research: rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new kappa) #1399's Lemma 9 connectivity, plus a DRUP refutation of the zero-pattern CNF. A first pass finds a passing pivot and an UNSAT formula on all 19 orbits.
• Expected artifact: one package research/complex-rank8-rigidity-p109/ with a stdlib verifier that recomputes the orbit census and replays all 19 proofs. With Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419 this would make every P109 unit rigid (floor 61). P108 is out of scope; I'll report its orbit count as the next question.
• Expiry: 2026-10-14 03:00 UTC.

[JosieElliston]

DONE: every P109 and every P108 unit is rigid

• Research: rank-8 masked decoders are gauge-rigid on every P109 unit — 19 new orbit certificates (no new κ) #1469 (P109). The 198688 triples outside a P112 frame form 19 orbits, and each gets a pivot plus a new DRUP proof. verify.py runs 25 checks in about 15 s. With Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419, every P109 unit is rigid, floor 61.
• Research: rank-8 masked decoders are gauge-rigid on every P108 unit — 168 orbit certificates, census-free coverage (no new κ) #1474 (P108). The open quadruples fall into 168 of the 180 orbits; each gets a pivot plus a DRUP proof, 361027 lemmas in total (about 6 MB gzipped). The coverage argument needs no census: every quadruple is equivalent to a triple-orbit representative plus one line, and each of the 2517 candidates is either inside a frame or carried onto a unit by an explicit generator word. verify.py runs 174 checks in about 2.5 min. With Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419, every P108 unit is rigid, floor 60.
• Cross-checks:
  • Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212's rup_check accepts all 19 P109 proofs, and rejects each without the zero clause.
  • An independently written census (OpenAI Codex, from a specification only) matches the orbit tables at k = 2, 3 and 4 exactly.
  • Read-only adversarial AI reviews of both packages found no soundness gap. They are not human reviews.
• Still inherited and unreviewed: Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa) #1212's Lemmas 5–6, §7 and transport; Research: rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new kappa) #1399's Lemma 9; and Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ) #1419's P104 inputs.
• Next: P107–P105. Per-orbit certificates stop scaling: about 6 MB already at P108, and on the order of 10⁵ orbits at P105. Going deeper needs a structural replacement for the DRUP zero-exclusion step (I2). Claim released.