Research: rank-8 rigidity passes to supersets — P105–P110 partial-frame punctures, P111 from #1212 alone (no new κ)

research/complex-rank8-rigidity-extension/PROOF.md

@@ -0,0 +1,100 @@
+# Rank-8 rigidity passes to supersets
+
+Notation and the system (E) are those of PR1212 (`research/complex-rank8-decoder-rigidity/PROOF.md` at head
+`57099cb5`, §0). For a set L of root lines, call L *rigid* if every L × L matrix K of rank at most 8 over a field
+of characteristic 0 that satisfies (E) on L equals `D (2 G_L) D⁻¹` for an invertible diagonal D. Finite facts
+marked **[X]** are recomputed by this package's `verify.py` (check id `X`).
+
+## Lemma 10 (extension)
+
+**Lemma 10.** Let L ⊂ L′ be sets of lines with L rigid and with the roots of L spanning R⁸. Suppose that for
+every i ∈ L′ \ L, the lines j ∈ L with G_ij = 0 span `r_i^⊥`. Then L′ is rigid.
+
+*Proof.* Let K′ have rank at most 8 and satisfy (E) on L′. Its principal submatrix K′[L,L] satisfies (E) on L
+and has rank at most 8. So K′[L,L] = D (2 G_L) D⁻¹ = 2 D R Rᵀ D⁻¹, where R is the L × 8 matrix of the roots
+r_j (Gram units). R has rank 8, so K′[L,L] has rank 8, and so does K′.
+
+Because rank K′ = rank K′[L,L] = 8, every row of K′ is a combination of the rows indexed by L. Write
+K′[i,:] = y_iᵀ K′[L,:]. On the columns L this reads K′[i,L] = y_iᵀ K′[L,L] = 2 u_iᵀ Rᵀ D⁻¹ with
+u_i = Rᵀ D y_i ∈ R⁸. That is, K′_ij = 2 ⟨u_i, r_j⟩ / d_j for j ∈ L.
+
+(E) gives K′_ij = 0 for every j ∈ L orthogonal to i. These r_j span `r_i^⊥`, so u_i = c_i r_i for some
+scalar c_i. The same argument on columns gives K′_ji = 2 d_j ⟨r_j, w_i⟩ with w_i = c′_i r_i.
+
+Next, compare entries between two new lines i, i′. Since K′[i,:] = y_iᵀ K′[L,:], we get
+K′_ii′ = y_iᵀ K′[L,i′] = 2 c′_i′ y_iᵀ D R r_i′, and y_iᵀ D R = u_iᵀ = c_i r_iᵀ by definition. So
+K′_ii′ = 2 c_i c′_i′ G_ii′ for all new i, i′. Taking i = i′, (E) gives
+K′_ii = 4 c_i c′_i = 4, so c′_i = 1/c_i. Set d_i = c_i for the new lines. Then K′_ab = 2 G_ab d_a / d_b
+for all a, b ∈ L′. ∎
+
+The proof uses the constraints of (E) only on new-versus-old orthogonal pairs and on the new diagonal. The
+constraints between two new lines hold automatically. It needs no zero exclusion, no pivot and no class
+structure.
+
+Both hypotheses matter:
+
+- **Rank.** A rank-one term supported on the odd entries of a new row satisfies (E). It gives a rank-9
+  solution that is not gauge **[control.rank9-escapes]**.
+- **Span.** If the orthogonal old lines span only a hyperplane of `r_i^⊥`, there is a rank-8 extension of a
+  gauge solution that satisfies (E) and is not gauge **[control.span-needed]**.
+
+## Theorem (bi-frame supersets)
+
+**Theorem.** Let F1, F2 be disjoint frames and S ⊆ F1 ∪ F2. Then the live set E8 \ S is rigid.
+
+*Proof.* W(E8) is transitive on the 2025 frames **[model.frame-transitivity]**, and its elements preserve
+(E) and the gauge form (PR1212 §0). So take F1 = FRAME0, which puts F2 inside P112.
+
+The unit L = E8 \ (FRAME0 ∪ F2) is rigid in each of the three FRAME0-stabiliser orbits of F2
+**[unit.frame-orbits]**:
+
+- type (2,2,2,2): PR1212, Theorem 1′;
+- type (4,4): PR1389;
+- type (1,…,1): PR1399.
+
+For every one of the 1260 units and every one of the 16 lines i ∈ FRAME0 ∪ F2, the live lines orthogonal to i
+span `r_i^⊥`. There are at least 52 of them in each case **[lemma10.span-condition]**. The roots of L span R⁸,
+because L also contains a line non-orthogonal to i: i has 56 such lines in E8, and at most 15 of them are
+removed. Lemma 10 then applies to L ⊂ E8 \ S. ∎
+
+**Corollary (floor).** On each of these live sets, every decoder with exactly eight costly terms in the E-graph
+model has cst ≥ 72 − |S| when |S| ≤ 15, and cst ≥ 56 when |S| = 16. The proof is PR1212 §8 verbatim with
+PR968's Theorem 4(b); see `research/complex-frame-pair-decoders/PROOF.md` §4. It inherits PR968's cited premise
+(F6).
+
+## Which intermediate punctures this reaches
+
+Now take S = FRAME0 ∪ X with X ⊂ P112. The question is when FRAME0 ∪ X lies in the union of two disjoint
+frames.
+
+- **Exactly when X lies in a frame inside P112.** Running over all pairs of disjoint frames whose union
+  contains FRAME0, the sets (F1 ∪ F2) \ FRAME0 are exactly the 1260 frames inside P112
+  **[census.biframe-covers]**.
+- **P111.** Every line of P112 lies in a type-(2,2,2,2) frame inside P112 **[census.p111-from-2222]**. So
+  P111 rigidity follows from PR1212's Theorem 1′ alone. This is a second proof of PR1389's P111 result. It
+  needs neither PR1389's three-row class argument nor P111's own zero-exclusion certificate.
+- **P110.** Every orthogonal pair in P112 lies in a type-(2,2,2,2) frame inside P112. So all 3304
+  orthogonal-pair P110 units are rigid, again from PR1212 alone **[census.table]**.
+- **P105–P109.** The covered X are counted below **[census.table]**. The "cheapest" column gives the
+  first rigid P104 type that contains X, in the order PR1212, then PR1399, then PR1389.
+
+| \|X\| | unit | all X | orthogonal X | covered X | cheapest: PR1212 / PR1399 / PR1389 |
+|---:|---|---:|---:|---:|---|
+| 1 | P111 | 112 | 112 | 112 | 112 / 0 / 0 |
+| 2 | P110 | 6216 | 3304 | 3304 | 3304 / 0 / 0 |
+| 3 | P109 | 227920 | 31024 | 29232 | 14784 / 14336 / 112 |
+| 4 | P108 | 6210820 | 94892 | 77868 | 22512 / 53760 / 1596 |
+| 5 | P107 | 134153712 | 82656 | 70560 | 18816 / 50176 / 1568 |
+| 6 | P106 | 2392407864 | 39088 | 35280 | 9408 / 25088 / 784 |
+| 7 | P105 | 36227890512 | 10592 | 10080 | 2688 / 7168 / 224 |
+
+**What is not reached.**
+
+- Any X containing an odd pair. No frame contains an odd pair, so Lemma 10 from a P104 unit cannot apply.
+  At P110 these are 2912 pairs in two stabiliser orbits, of sizes 224 and 2688. Write T_x for the four FRAME0
+  lines not orthogonal to x. In the 224-orbit T_x = T_y; in the 2688-orbit T_x and T_y share two lines
+  **[census.p110-odd-orbits]**.
+- Orthogonal sets X that do not extend to a frame inside P112, for example 1792 of the 31024 orthogonal
+  triples.
+
+For |X| ≥ 4 the covered X are a small fraction of all X, so most of P105–P108 is still open.

research/complex-rank8-rigidity-extension/README.md

@@ -0,0 +1,99 @@
+# Rank-8 rigidity passes to supersets: P105–P110 partial-frame punctures, and P111 from PR1212 alone (no new κ)
+
+**Status: scoped structural result. No κ claim, no construction.** It builds on the rank-8 rigidity line of PR1212
+(burntout76, `research/complex-rank8-decoder-rigidity/`, open, head `57099cb5`), PR1389 and PR1399. It answers
+PR1399's open next question, the intermediate punctures P105–P110, as far as a linear argument reaches.
+
+In PR717's E-graph (masked) model, a live set L is *rigid* if every rank-≤8 solution K of PR1212's system (E)
+(`K_ii = 4`, `K_ij = 0` on orthogonal live pairs, odd entries free) is `D(2G)D⁻¹`. Rigidity is what turns
+PR968's eight-term floor into a floor for masked decoders with exactly eight costly terms (PR1212 §8).
+
+**Lemma 10 (extension).** Suppose L ⊂ L′, L is rigid, and the roots of L span R⁸. Suppose also that for each new
+line i, the lines of L orthogonal to i span `r_i^⊥`. Then L′ is rigid.
+
+The proof ([PROOF.md](PROOF.md)) is a few lines of linear algebra. K′[L,L] already has rank 8, so each new row
+is `2uᵀRᵀD⁻¹` on L. The zeros against the orthogonal old lines force `u ∝ r_i`, and the diagonal fixes the
+scale. There is no zero exclusion, no DRUP certificate and no class argument.
+
+**Theorem.** E8 \ S is rigid whenever S lies in the union of two disjoint frames. The P104 units are rigid by
+PR1212, PR1389 and PR1399. The span condition holds on all 1260 units for all 16 new lines, with at least 52
+orthogonal live lines each.
+
+**What it reaches.** For P112 minus X:
+
+- **Coverage rule.** FRAME0 ∪ X lies in a union of two disjoint frames exactly when X lies in a frame inside
+  P112.
+- **P111.** Every line lies in a type-(2,2,2,2) frame, so P111 rigidity follows from PR1212 alone. This is a
+  second proof of PR1389's P111 result.
+- **P110.** All 3304 orthogonal-pair units are rigid, again from PR1212 alone.
+- **P105–P109.** 29232, 77868, 70560, 35280 and 10080 covered X for |X| = 3, …, 7. The PROOF.md table splits
+  them by which predecessor they need.
+
+The eight-costly-term floor on each covered unit is then cst ≥ 72 − p with p = 8 + |X|, by PR968
+Theorem 4(b) via PR1212 §8.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 1 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-extension/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_EXTENSION: checks 14; Lemma 10 on all 1260 bi-frame units; 226324 punctures P105-P110 covered (all 3304 orthogonal-pair P110); P111 from PR1212 alone; P104 rigidity cited from PR1212/PR1389/PR1399
+```
+
+The verifier has its own E8 model and recomputes everything it uses:
+
+- the 2025 frames and W(E8) transitivity on them;
+- the three FRAME0-stabiliser orbits of the 1260 frames in P112, matched to the three types;
+- the span condition;
+- the cover census, the P111 cover, the P105–P110 table and the odd-pair P110 orbits.
+
+It also runs exact rational checks of the lemma's mechanism and three controls:
+
+- a rank-9 solution escapes;
+- without the span condition there is a rank-8 non-gauge extension;
+- a perturbed orthogonal entry is rejected.
+
+## Not covered
+
+- **Punctures containing an odd pair.** No frame contains an odd pair, so Lemma 10 from a P104 unit cannot
+  reach them. This is most of P105–P110. At P110 it is 2912 pairs in two stabiliser orbits, of sizes 224
+  and 2688.
+- Orthogonal X that do not extend to a frame inside P112, for example 1792 of the 31024 orthogonal triples.
+- **Inherited P104 rigidity** is cited, not recomputed. The type-(2,2,2,2) units come from PR1212 Theorem 1′,
+  which is open and so is the whole chain. The other two types come from PR1389 and PR1399, both unmerged and
+  unreviewed. P111 and all of P110's covered units need only PR1212.
+- **Nine or more costly terms.** Rank-8 rigidity says nothing about rank ≥ 9; see control.rank9-escapes.
+- PR968's flat-classification premise (F6) is inherited through the floor. Attainment of 72 − p on these
+  particular units is not checked.
+- The written proof has had no independent human review. There is no construction and no κ change, and every
+  condition of the selected record is unchanged.
+
+## Open next questions
+
+**Odd-pair P110.** Is P112 minus an odd pair {x, y} rigid? These are the two stabiliser orbits of sizes 224 and
+2688 (see [TASK.json](TASK.json)).
+
+- *Why it matters.* They are the whole remaining eight-term gap at P110, and the extension lemma cannot reach
+  them.
+- *A feasible first step.* Per orbit, pick a pivot frame inside the unit. Test PR1212's (I3) and (I4) on the
+  complete classes, then PR1399's Lemma 9 witness connectivity for the lines of incomplete classes. Build the
+  zero-exclusion CNF with PR1212's `make_proof.py`.
+- *The blocker.* Zero exclusion passes up to supersets, but these units contain no smaller unit with a known
+  certificate. Each orbit therefore needs its own DRUP proof.
+
+## Credit
+
+- **burntout76 / Brett Halligan (PR1212):** the rigidity theorem, (E), the type-(2,2,2,2) units, the transport
+  and §8's floor argument.
+- **themilkman216 (PR968):** the eight-term floor 72 − p and its puncture theorem.
+- **DreamingOfClouds (PR717):** the E-graph model.
+- **PR1389, PR1399 (JosieElliston):** the type-(4,4) and admissible P104 units.
+
+Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code,
+covering the lemma, verifier and write-up. Apache-2.0.

research/complex-rank8-rigidity-extension/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    }
+  ]
+}

research/complex-rank8-rigidity-extension/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-masked-decoder",
+  "priority_revision": 2,
+  "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "original_card": {
+    "id": "complex-masked-decoder",
+    "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?",
+    "starting_points": [
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md"
+    ],
+    "methods": [
+      "Synthesize a decoder with exact coefficients and fully priced helper endpoints.",
+      "Bound the best possible budget for a fixed support alphabet before synthesis."
+    ],
+    "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-decoder-field-extension-seed44/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44",
+      "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.",
+    "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.",
+    "allowed_variations": [
+      "Select a specific masked or overcomplete family with exact labels and supports."
+    ],
+    "scope_change_triggers": [
+      "Repeating the exact eight-term all-pairs search inside its proved scope."
+    ],
+    "overlap_terms": [
+      "masked decoder",
+      "overcomplete",
+      "eight-term"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Proof obligation inside the masked (E-graph) model: on which intermediate punctures P112 minus X (|X| = 2..7, i.e. P105-P110) does every rank-<=8 solution of PR1212's system (E) equal D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 72 - p? Answered by an extension lemma from the P104 frame complements, with an exact census of the punctures it reaches and of what is left.",
+  "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212, PR1389 and PR1399 answered it for exactly eight costly terms on P120, P112, P111 and every P104 frame complement, and PR1399 lists P105-P110 as its open next question. This settles the punctures that lie inside a frame and gives a second proof of P111 from PR1212 alone; it does not construct a decoder.",
+  "bottleneck_link": "Side result on the binding complex supplier: it rules out masked eight-costly-term decoders below PR968's floor on every partial-frame puncture between P112 and P104, so the remaining masked escape routes are nine or more costly terms or punctures containing an odd pair.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at what the extension lemma reaches; punctures with an odd pair (starting with the two P110 orbits) and nine or more costly terms are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 9 exact checks (E8 model, 2025 frames and W(E8) transitivity, stabiliser orbits of the 1260 frames in P112, the span condition on all 1260 x 16 new lines, the bi-frame cover census, the P111 cover, the P105-P110 table, the odd-pair P110 orbits) plus 5 algebraic checks and controls, about 1 s. Rigidity of the P104 units is cited from PR1212, PR1389 and PR1399, not recomputed.",
+  "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)",
+  "ai_assistance": "Claude Opus 5.5 via Claude Code: proof, verifier and write-up. Submitted by the account holder.",
+  "open_questions": [
+    {
+      "question": "Does rank-8 rigidity of (E) hold on P112 minus an odd pair {x, y} (G_xy = +-1), the two FRAME0-stabiliser orbits of sizes 224 and 2688 that make up the rest of P110?",
+      "why_it_matters": "With this package every orthogonal-pair P110 unit is rigid; the odd pairs are the whole remaining eight-term gap at P110, and the extension lemma cannot reach them because no frame contains an odd pair.",
+      "first_step": "For each orbit representative pick a pivot frame inside P112 minus {x, y}, test PR1212's inputs (I3), (I4) on the complete classes and PR1399's Lemma 9 witness connectivity for the lines of incomplete classes, then build the zero-exclusion CNF with PR1212's make_proof.py.",
+      "blocked_by": "Zero exclusion is not inherited: P112 minus an odd pair contains no unit with a known certificate, so each orbit needs its own DRUP proof (python-sat), which no submitted package has."
+    }
+  ]
+}

research/complex-rank8-rigidity-extension/VERIFY.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "9 exact census and structure checks (E8 model, frames, W(E8) transitivity, stabiliser orbits, Lemma 10 span condition on all 1260 bi-frame units, bi-frame cover census, P111 cover, P105-P110 table, odd-pair P110 orbits) and 5 algebraic checks/controls. P104 rigidity is cited from PR1212/PR1389/PR1399."
+    }
+  ]
+}