Research: rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new kappa)

research/complex-rank8-rigidity-p104-admissible/PROOF.md

@@ -0,0 +1,95 @@
+# Rank-8 rigidity on the admissible P104 units
+
+Notation, equations (E), (1), (2), (E0), (E2), (E4) and Lemmas 2–8 are those of PR1212
+(`research/complex-rank8-decoder-rigidity/PROOF.md` at head `57099cb5`). Finite facts marked
+**[X]** are recomputed by this package's `verify.py` (check id `X`). Facts marked **[1212: X]** are
+PR1212's checks, which `verify.py --pr1212-dir` replays from blob-pinned files.
+
+**Theorem.** Let L be one of the 896 admissible P104 units: P112 minus a frame of type (1,…,1) relative to
+FRAME0. Let K be an L × L matrix over a field of characteristic 0 with rank K ≤ 8 that satisfies (E). Then
+K = D (2 G_L) D⁻¹ for an invertible diagonal D.
+
+**Corollary.** In the E-graph model, every decoder with exactly eight costly terms on an admissible P104 unit
+has cst ≥ 56. This is PR968's floor at p = 16, reached through PR1212's §8 verbatim. PR717's P104 decoders,
+which lie in this orbit **[1212: G.pr717-p104-orbit]**, attain it.
+
+By PR1212 §10 transport, the stabiliser of FRAME0 is transitive on the 896 admissible frames
+**[1212: G.frame-orbits]**. It therefore suffices to treat PR1212's representative, P112 minus the frame
+`DEAD` with pivot `PIVOT` (both listed as root vectors in `verify.py`) **[unit.live, unit.admissible-type,
+pr1212.unit-vectors]**.
+
+## Inputs that already hold
+
+Relative to this pivot there are 22 complete live classes, four classes with two live rows, and two empty
+classes **[unit.class-profile]**. PR1212 §10 records that three of its four finite inputs hold here:
+
+- **(I2)** zero exclusion (Lemma 8) **[1212: G.P104-11111111.zero-exclusion]**;
+- **(I3)** the Lemma 5 group witnesses for every complete class **[lemma5.group-witnesses;
+  1212: G.P104-11111111.class-witnesses]**;
+- **(I4)** every block carries a complete live class **[lemma6.blocks-and-gluing]**.
+
+Only (I1) fails: eight live lines lie in two-row classes, and there Lemma 5 leaves a one-parameter family
+**[control.in-class-not-forced]**.
+
+## Step 1: the complete classes
+
+Lemma 5 applies to each of the 22 complete classes. It needs only (I2), (I3) and the class's own
+equations. Lemma 6 applies to the set of complete classes. Its proof uses only complete classes:
+
+- the gluing equation (5) between complete classes C, C′ in distinct blocks through {k, k′};
+- for two classes in the same block, a complete class in one of the two other blocks through {k, k′};
+- the cocycle in the block of each triple.
+
+All three exist by (I4) **[lemma6.blocks-and-gluing]**. Lines outside the complete classes play no role. So there are nonzero
+g_f (f ∈ F) and d′_j such that for every line j in a complete class and f ∈ T_j:
+
+    a_jf = d′_j ε_jf g_f,      b_jf = 4 (d′_j g_f)⁻¹ ε_jf.                                  (6)
+
+## Step 2: Lemma 9 (propagation)
+
+**Lemma 9.** Let i be a live non-pivot line with support T = T_i. Call a pair {k, k′} ⊂ T *witnessed* if
+some line j of a complete class has G_ij = 0 and T_i ∩ T_j = {k, k′}. If the witnessed pairs connect T,
+then for a nonzero λ_i
+
+    a_if = λ_i ε_if g_f,      b_if = 4 (λ_i g_f)⁻¹ ε_if      (f ∈ T).
+
+*Proof.* Let j witness {k, k′}. Rule (3) with G_ij = 0 gives ε_ik ε_jk = −ε_ik′ ε_jk′
+**[lemma9.propagation-connected]**. Equation (E2) in the order a_i · b_j, with b_j from (6), reads
+
+    (4 / d′_j) (a_ik ε_jk / g_k + a_ik′ ε_jk′ / g_k′) = 0.
+
+Multiply by ε_ik ε_jk d′_j / 4 and use the sign identity:
+
+    a_ik ε_ik / g_k = a_ik′ ε_ik′ / g_k′.
+
+So a_if ε_if / g_f is constant along witnessed pairs, and hence on T. Call the constant λ_i. Then
+a_if = λ_i ε_if g_f, and λ_i ≠ 0 because (E0) needs a_i ≠ 0.
+
+In the order a_j · b_i, with a_j from (6), the same steps give b_ik ε_ik g_k = b_ik′ ε_ik′ g_k′. So
+b_if = μ_i ε_if / g_f. Finally (E0) gives 4 λ_i μ_i = 16. ∎
+
+The proof needs no zero exclusion for i, no in-class equation and no witness inside i's own class. Each
+witnessed pair costs one linear equation, so connectivity is exactly what is needed. With every witness at
+one column of T removed, a 2-dimensional family survives **[control.disconnected-not-forced]**. As an
+algebra cross-check, `verify.py` builds the witnessed equations (E2) from (6) for random rational g, d′. On
+both a_i|T and b_i|T they have rank 3, with kernels ε_i ∘ g and ε_i / g **[lemma9.solution-line]**.
+
+**Finite input.** On this unit all eight two-row lines have all six pairs of T witnessed, with 40 witnesses
+each **[lemma9.propagation-connected]**. The non-gauge two-row solution of the control satisfies every
+in-class condition. It fails 28 of the 40 witnessed equations for one of its rows
+**[control.cross-block-rejects]**.
+
+## Assembly
+
+Steps 1 and 2 put every live non-pivot line into PR1212 §7's form, with d′_i = λ_i for the two-row lines.
+PR1212 §7 then applies verbatim and gives K = D (2G) D⁻¹. An exact rational control checks the assembly on
+all 104 live lines **[assembly-control, control.perturbed-fails]**. ∎
+
+## Remarks
+
+- Lemma 9 is more general than the use made of it here. It needs only a set of lines already in form (6)
+  that witnesses a connected pair graph, whatever their classes. It can be iterated, since propagated lines
+  become witnesses. The work on another unit is in Step 1, which needs (6) on enough classes to fix g.
+- Lemma 9 is linear in a_i and b_i. The only field facts it uses are division by 4 and by the nonzero
+  g_f, d′_j. Step 1 inherits PR1212's argument, which holds over any field of characteristic 0
+  (PR1212 §9).

research/complex-rank8-rigidity-p104-admissible/README.md

@@ -0,0 +1,94 @@
+# Rank-8 masked decoders are gauge-rigid on the 896 admissible P104 units (no new κ)
+
+**Status: scoped structural result. No κ claim, no construction.** It extends PR1212 (burntout76,
+`research/complex-rank8-decoder-rigidity/`, open, head `57099cb5`) and depends on that PR's zero-exclusion
+lemma. It is independent of PR1389, the type-(4,4) and P111 cases.
+
+PR1212 proves the following in PR717's E-graph (masked) model. Every rank-≤8 solution K of
+`K_ii = 4, K_ij = 0` on orthogonal live pairs, with odd entries free, is `D(2G)D⁻¹`. As a result, decoders
+with exactly eight costly terms keep PR968's floor. Its PROOF.md §10 leaves the **896 admissible P104 units**
+open (PR717's P104 among them). On its pivot there, four classes keep only two live rows, and Lemma 5 then
+leaves a one-parameter family inside each.
+
+This package closes that gap ([PROOF.md](PROOF.md)) with one new lemma:
+
+- **Lemma 9 (propagation).** Lemmas 5–6 already fix the global scaling `g` on the 22 complete classes, since
+  all 14 blocks carry one. A two-row line `i` then needs no in-class argument. Each witness `j` in a complete
+  class with `T_i ∩ T_j = {k, k′}` turns (E2) into `a_ik ε_ik / g_k = a_ik′ ε_ik′ / g_k′`, and the reverse
+  order gives the same for `b`. If the witnessed pairs connect `T_i`, then `a_i ∝ ε_i ∘ g` and `b_i ∝ ε_i / g`,
+  and (E0) fixes the product. On this unit every two-row line has all six pairs witnessed, with 40 witnesses
+  per line.
+
+**Consequence.** In the E-graph model, every decoder with exactly eight costly terms has `cst ≥ 56` on every
+admissible P104 unit. PR717's P104 decoders attain it.
+
+Together with PR1212 (336 type-(2,2,2,2) units) and PR1389 (28 type-(4,4) units), this covers all 1260 P104
+frame complements. That combination is conditional on PR1389, which is unmerged and unreviewed.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 0.1 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p104-admissible/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P104_ADMISSIBLE: checks 15; classes 22 complete + 4 two-row; 8 two-row lines propagated; floor 56; zero exclusion cited from PR1212
+```
+
+To also replay PR1212's zero exclusion for this unit (about 15 s), first make a checkout of PR1212's head.
+The verifier checks the git blobs of its `verify.py` and `proof-P104-11111111.drup`. It then runs PR1212's
+verifier and matches the unit and pivot by root vectors:
+
+```sh
+git fetch origin pull/1212/head && git worktree add --detach /tmp/pr1212 57099cb5
+python3 -I -B research/complex-rank8-rigidity-p104-admissible/verify.py --pr1212-dir /tmp/pr1212
+```
+
+The last line then ends `... replayed from PR1212` with 22 checks. The replay covers
+`G.P104-11111111.zero-exclusion`, `G.P104-11111111.class-witnesses`, `G.frame-orbits` and
+`G.pr717-p104-orbit`.
+
+The verifier is independent of PR1212's code: it has its own E8 model, classes, witnesses, gluing and
+propagation. It recomputes the orbit type of the punctured frame. It cross-checks Lemma 9's algebra on
+the actual (E2) equations (rank 3, with the gauge vector as kernel). The four controls show that:
+
+- the in-class conditions admit a non-gauge two-row solution;
+- witnessed cross-block equations reject that solution (28 of 40 fail);
+- removing the witnesses at one column leaves a 2-dimensional family;
+- a perturbed entry breaks (2).
+
+## Not covered
+
+- **Nine or more costly terms**, including PR717's mixed-β problem. Rank-8 rigidity says nothing about
+  rank-≥9 solutions of (E).
+- **The intermediate punctures P105–P110.**
+- **Zero exclusion** is PR1212's DRUP result, replayed but not re-derived. The flat classification premise
+  (F6) inherited through PR968 is unchanged.
+- 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
+
+**Intermediate punctures P105–P110.** This matters because, with this package, PR1212 and PR1389, rigidity
+holds on P120, P112, P111 and every P104 frame complement. The units in between are the remaining
+eight-term gap in the masked model. A feasible first step: enumerate the FRAME0-stabiliser orbits of 2–7
+line punctures of P112. For each orbit, pick a pivot and test (I3) and (I4) on the complete classes, then
+Lemma 9 connectivity for the other live lines. Lemma 9 needs no in-class equations, so incomplete classes
+cost nothing once `g` is fixed. The blocker: zero exclusion is a separate DRUP certificate per unit
+(PR1212's CNF builder plus python-sat), and the orbit count is not yet known. See [TASK.json](TASK.json).
+
+## Credit
+
+- **burntout76 / Brett Halligan (PR1212):** the theorem, the proof skeleton and every lemma reused here,
+  zero exclusion and its DRUP certificate for this unit, the transport, the pivot, and the §10 record of
+  this gap.
+- **themilkman216 (PR968):** the eight-term floor.
+- **DreamingOfClouds (PR717):** the E-graph model and the P104 decoders.
+- **Navinor (PR1292):** local rigidity on all P104 units.
+
+Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code,
+covering the proof, verifier and write-up. Apache-2.0.

research/complex-rank8-rigidity-p104-admissible/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-p104-admissible/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: does every rank-<=8 solution of PR1212's system (E) on the 896 admissible (type (1,...,1)) P104 units equal D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 56 there?",
+  "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212 answered it for exactly eight costly terms on P112, P120 and the type-(2,2,2,2) units, and PR1389 on P111 and type (4,4); both list the admissible P104 units as open (PR1212 PROOF.md section 10, PR1389 open question). This closes that gap; it does not construct a decoder.",
+  "bottleneck_link": "Side result on the binding complex supplier: the admissible units are where PR968's 7/13 ratio is attained (PR717's P104/56). This rules out masked eight-costly-term decoders below the floor there, so the remaining masked escape routes are nine or more costly terms or deeper/other punctures.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the admissible P104 orbit; nine or more costly terms and P105-P110 punctures are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 11 exact checks plus 4 controls (about 0.1 s); --pr1212-dir replays PR1212's zero-exclusion DRUP proof for this unit, its class witnesses and the orbit transport from blob-pinned files (7 more checks).",
+  "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), and with it the eight-costly-term floor, hold on the intermediate punctures P105-P110 (P112 minus 2-7 lines)?",
+      "why_it_matters": "With this package, PR1212 and PR1389, rigidity holds on P120, P112, P111 and every P104 frame complement. The intermediate punctures are the remaining eight-term gap in the masked model between those depths.",
+      "first_step": "Enumerate the FRAME0-stabiliser orbits of 2-7 line punctures of P112, pick a pivot per orbit, and test (I3), (I4) on the complete classes plus Lemma 9 witness connectivity for every other live line. Lemma 9 uses no in-class equations, so incomplete classes cost nothing once g is fixed.",
+      "blocked_by": "Zero exclusion is a separate DRUP certificate per unit (PR1212's CNF builder and python-sat), and the number of orbits is not yet known."
+    }
+  ]
+}

research/complex-rank8-rigidity-p104-admissible/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": "11 exact structural checks on PR1212's admissible P104 representative (unit and orbit type, D4 blocks, class profile, Lemma 5 group witnesses, Lemma 6 blocks and gluing, Lemma 9 propagation connectivity and solution line, assembly) and 4 negative controls. PR1212 zero exclusion is cited; replay it with --pr1212-dir."
+    }
+  ]
+}