Research: rank-8 masked decoders are gauge-rigid on every P108 unit — 168 orbit certificates, census-free coverage (no new κ)

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

@@ -0,0 +1,59 @@
+# Rank-8 rigidity on every P108 unit
+
+Notation, (E), equations (2), (E0), (E2), and Lemmas 2–8 are those of PR1212
+(`research/complex-rank8-decoder-rigidity/PROOF.md` at head `57099cb5`). Lemma 9 and "Step 1" are PR1399's
+(`research/complex-rank8-rigidity-p104-admissible/PROOF.md` at head `4e1ba3a1`). Lemma 10 and the coverage rule
+are PR1419's (`research/complex-rank8-rigidity-extension/PROOF.md` at head `81b8997b`). The per-unit argument is
+PR1425's (`research/complex-rank8-rigidity-p110-odd/PROOF.md` at head `4b707c22`), applied to 168 new units.
+Finite facts marked **[X]** are recomputed by this package's `verify.py` (check id `X`; `u` is one of `u001`, …,
+`u168`).
+
+**Theorem.** Let X be a 4-subset of P112 and L = P112 \ X. 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 a P108 unit has
+cst ≥ 60 = 72 − 12. This is PR968's Theorem 4(b) with p = 12, reached through PR1212 §8 verbatim.
+
+## Reduction to 168 units, without a census of quadruples
+
+Let H be the group generated by `verify.py`'s 8 generators. Each is a reflection or a product of two reflections
+fixing FRAME0 **[model.generators]**, so H maps frames inside P112 to frames inside P112. H splits the 227920
+triples of P112 into 24 orbits **[census.triples]**. Let t_1, …, t_24 be their first members.
+
+**Candidate lemma.** Every 4-subset Y of P112 is H-equivalent to a *candidate* t_k ∪ {x} with x ∉ t_k.
+*Proof.* Pick a triple s ⊂ Y. Its orbit contains some t_k, so h(s) = t_k for some h ∈ H, and h(Y) = t_k ∪ {h(y)}
+where y is the fourth line. ∎
+
+There are 2517 distinct candidates **[census.cover]**:
+
+- **49 lie inside a P112 frame.** Since H preserves that property, so does every Y equivalent to one. These units
+  are rigid by PR1419's Theorem, which cites the P104 units of PR1212, PR1389 and PR1399.
+- **The other 2468 are covered by the units.** `COVER.json` gives each one a unit and a word in the generators,
+  of length at most 10. `verify.py` applies the word to the unit's quadruple and checks that the result is the
+  candidate. None of the 168 units lies inside a P112 frame. That they lie in distinct orbits, one per open
+  orbit, comes from `make_proof.py`'s grouping and the independent census. `verify.py` does not check it, and the
+  argument does not need it, since a redundant unit would only add work.
+
+So every 4-subset of P112 is either inside a P112 frame or transported from one of the 168 units. PR1212 §10
+transport needs only some Weyl element carrying one unit onto another. The orbits were grouped with numpy in
+`make_proof.py`, which is not trusted. The full quadruple census, 180 orbits with 12 inside a frame and 168 open,
+is consistent with an independently written count (see README) but is not needed by the argument.
+
+## Per-unit argument
+
+For each unit **[u.rigid]** checks the same conditions as PR1425 and the P109 package:
+
+- PR1212 Lemma 2's D4 facts relative to the pinned pivot F ⊂ L;
+- (I3) with live witnesses on every complete class;
+- (I4), all 14 blocks, and gluing through every shared pivot pair;
+- Lemma 9 connectivity and its sign identity for every other non-pivot live line;
+- (I2) zero exclusion: the zero-pattern CNF plus "some pattern variable is true" is refuted by the DRUP proof
+  in `PROOFS.json.gz`, which is replayed by `verify.py`'s own RUP checker and fails without that clause;
+- exact rational checks of Lemma 9's rank-3 systems and of the §7 assembly on all 108 live lines;
+- the gauge pattern satisfies the CNF.
+
+The proof is then PR1425's:
+
+- **Step 1** (PR1399): Lemmas 5–6 on the complete classes;
+- **Step 2:** Lemma 9 on the rest;
+- **Assembly:** PR1212 §7, then transport. ∎

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

@@ -0,0 +1,104 @@
+# Rank-8 masked decoders are gauge-rigid on every P108 unit (no new κ)
+
+**Status: scoped structural result. No κ claim, no construction.** It continues the rank-8 rigidity line of
+PR1212 (burntout76, open, head `57099cb5`), PR1399 (`4e1ba3a1`), PR1419 (`81b8997b`), PR1425 (`4b707c22`) and
+the P109 package (PR1469). It answers PR1469's open next question.
+
+PR1419's extension lemma makes P112 minus X rigid whenever X lies inside a frame of P112. For |X| = 4 that leaves
+168 of the 180 FRAME0-stabiliser orbits of quadruples, 6132952 of 6210820. This package proves rigidity on all
+168 with PR1425's per-unit method ([PROOF.md](PROOF.md)). Each representative has:
+
+- a pivot frame passing PR1212's (I3), (I4) and gluing;
+- PR1399's Lemma 9 connectivity for the remaining lines;
+- a new DRUP refutation for (I2) zero exclusion, 361027 lemmas in total.
+
+**Coverage without a census.** The verifier does not enumerate the 6.2 million quadruples. Every quadruple
+contains a triple, and the 24 triple orbits are cheap to compute. So every quadruple is equivalent to a
+*candidate*: a triple-orbit representative plus one line. There are 2517 candidates:
+
+- 49 lie inside a P112 frame, which is the PR1419 case;
+- for each of the other 2468, `COVER.json` gives a word in the generators that carries a unit's quadruple onto
+  it, and `verify.py` replays every word.
+
+That the 168 units lie in distinct orbits comes from the census and is not needed by the argument.
+
+**Consequence.** With PR1419, every P108 unit (P112 minus any four lines) is rigid. Every decoder with exactly
+eight costly terms in the E-graph model there has cst ≥ 60, which is PR968's 72 − p at p = 12.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 2.5 minutes:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p108/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P108: checks 174; 168 rigid units cover every P108 quadruple outside a P112 frame; with PR1419 every P108 unit is rigid; floor 60
+```
+
+What `verify.py` does:
+
+- **Builds everything itself.** It has its own E8 model, triple orbits, cover-word replay, pivot conditions,
+  CNF builder and two-watched-literal RUP checker. It replays all 168 proofs from `PROOFS.json.gz` (about
+  6 MB) and pins the SHA256 of each decompressed proof and each CNF.
+- **Controls.** The gauge pattern satisfies each CNF. Each proof fails without the "some entry vanishes"
+  clause. An empty-clause-only proof is rejected.
+
+To regenerate `UNITS.json`, `COVER.json` and `PROOFS.json.gz` (about 40 s, 8 processes), run the command below.
+It needs python-sat (1.9.dev15, Glucose 4.1, used here), numpy and scipy. numpy only proposes the orbit grouping;
+the verifier checks every word.
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p108/make_proof.py --out-dir /some/new/dir
+```
+
+**One-time cross-check, not part of `verify.py`.** OpenAI Codex wrote a census independently, from a
+specification only. It finds the same 180 quadruple orbits, with 12 inside a P112 frame (77868 quadruples,
+matching PR1419's count) and 168 open. The argument above does not need that census.
+
+**AI review.** A read-only adversarial review, also by Codex, checked the coverage argument. It confirmed that
+every triple orbit's representative is used, that frame containment is invariant, and that every cover word
+replays. It also checked the P108 edge cases, such as classes with a single live row. It found no soundness gap,
+and its wording point on orbit distinctness is applied above. This is not a human review.
+
+## Not covered
+
+- **Inherited steps.** These are cited, not re-derived:
+  - PR1212's Lemmas 5–6, §7 assembly and §10 transport;
+  - PR1399's Lemma 9;
+  - PR1419's Lemma 10 with its P104 inputs, for the frame-contained quadruples.
+
+  All of these PRs are open, as is PR1469, which is the P109 package. This package does not depend on it, since
+  Lemma 10 is not used between depths here. PR968's premise (F6) is inherited through the floor. Attainment of
+  60 is not checked.
+- **P107 and deeper**, and **nine or more costly terms**.
+- 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
+
+**P107 to P105, and a structural zero-exclusion lemma.**
+
+- *Why it matters.* PR968's floor goes to p = 15, which is P105. With PR1419's Lemma 10, rigidity of every P105
+  unit would give every intermediate depth at once.
+- *A feasible first step.* Run the same pipeline on the P107 candidates, each a P108 orbit representative plus
+  one line, to measure the proof volume. In parallel, look for a pivot-local argument that excludes zeros from
+  the *trans* and *diag* families alone.
+- *The blocker.* The per-orbit certificates already take about 6 MB at P108, and P105 has on the order of 10⁵
+  orbits. No structural replacement for the DRUP step (I2) is known.
+
+## Credit
+
+- **burntout76 / Brett Halligan (PR1212):** the theorem, (E), the CNF families of Lemmas 4 and 8 (reimplemented
+  here), the pivot reduction, Lemmas 5–6, §7 and the transport.
+- **themilkman216 (PR968):** the floor 72 − p.
+- **DreamingOfClouds (PR717):** the E-graph model.
+- **PR1399, PR1419, PR1425, PR1469 (JosieElliston):** Lemma 9, the extension lemma and coverage rule, and the
+  per-unit pipeline.
+
+Prepared by JosieElliston with substantial assistance from Claude Opus 5.5 (Anthropic) via Claude Code, covering
+the proof, coverage argument, verifier and write-up. OpenAI Codex independently recomputed the orbit census and
+reviewed the package. Apache-2.0.

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

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983",
+  "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-p108/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-masked-decoder",
+  "priority_revision": 2,
+  "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983",
+  "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: is every rank-<=8 solution of PR1212's system (E) on P112 minus X, for every 4-subset X not inside a P112 frame (the part of P108 that PR1419's extension lemma cannot reach; 168 orbits), equal to D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 60 on every P108 unit?",
+  "scope_change_reason": "The card asks whether a masked decoder can beat the floor. PR1212/PR1389/PR1399 answered it for exactly eight costly terms on P120, P112, P111 and every P104 frame complement, PR1419 for punctures inside a frame, PR1425 for the rest of P110 and the P109 package (PR1469) for the rest of P109, whose open next question is P108. This closes it; it does not construct a decoder.",
+  "bottleneck_link": "Side result on the binding complex supplier: masked eight-costly-term decoders cannot beat PR968's floor on any P108 unit, so the remaining masked escape routes are nine or more costly terms or punctures of depth five or more not inside a frame.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at P108 with one PR; P107 and deeper (orbit counts growing toward order 1e5 at P105), and nine or more costly terms, are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 174 exact checks in about 2.5 minutes (generators; triple orbits; a candidate-lemma coverage argument with explicit generator words for all 2468 open candidates; per unit (168) the pivot's D4 structure, (I3), (I4) and gluing, Lemma 9 connectivity and algebra, assembly, CNF consistency, DRUP replay of zero exclusion with its own RUP checker and the needs-zero-clause control; one bogus-proof control). The 180-orbit quadruple census (168 open) matches an independently written census by OpenAI Codex (recorded, not needed by the argument); a read-only adversarial review by OpenAI Codex found no soundness gap (not a human review).",
+  "author": "JosieElliston (with Claude Opus 5.5 via Claude Code)",
+  "ai_assistance": "Claude Opus 5.5 via Claude Code: proof, coverage argument, verifier and write-up. OpenAI Codex: independent orbit census from a specification and a read-only adversarial review. Submitted by the account holder.",
+  "open_questions": [
+    {
+      "question": "Does rank-8 rigidity of (E) hold on P107-P105 units (P112 minus 5-7 lines not inside a P112 frame), and can the per-orbit DRUP step (I2) be replaced by a structural zero-exclusion lemma?",
+      "why_it_matters": "PR968's floor covers punctures up to p = 15 (P105); with PR1419's Lemma 10, rigidity of every P105 unit would give every intermediate depth at once. Per-orbit certificates already cost about 6 MB at P108 and P105 has on the order of 1e5 orbits.",
+      "first_step": "Run make_proof.py's pivot rule and CNF on P107 candidates (P108 orbit representative + one line) to measure proof volume; separately, look for a pivot-local argument that excludes zeros using only the trans and diag families, which carry most refutations.",
+      "blocked_by": "Proof volume grows with the orbit count; no structural replacement for (I2) is known."
+    }
+  ]
+}