Research: rank-8 masked decoders are gauge-rigid on every P109 unit — 19 new orbit certificates (no new κ)

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

@@ -0,0 +1,66 @@
+# Rank-8 rigidity on every P109 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 the "Step 1" argument are
+those of PR1399 (`research/complex-rank8-rigidity-p104-admissible/PROOF.md` at head `4e1ba3a1`). Lemma 10 and the
+coverage rule are those of PR1419 (`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 19 new units. Finite facts marked **[X]** are recomputed by this package's `verify.py` (check id `X`;
+`u` is one of `u01`, …, `u19`).
+
+**Theorem.** Let X be a 3-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 P109 unit has
+cst ≥ 61 = 72 − 11. This is PR968's Theorem 4(b) with p = 11, reached through PR1212 §8 verbatim.
+
+## Reduction to 19 units
+
+Let H be the group generated by `verify.py`'s 8 generators, each a reflection or a product of two reflections
+fixing FRAME0 **[model.generators]**. Its orbits split the 227920 triples of P112 into 24 classes, and whether
+a triple lies in a frame inside P112 is constant on each class **[census.triples]**:
+
+- **5 orbits, 29232 triples, inside a P112 frame.** PR1419's coverage rule applies, so these units are rigid by
+  PR1419's Theorem, which cites the P104 units of PR1212, PR1389 and PR1399.
+- **19 orbits, 198688 triples, not inside one.** 18 of them contain an odd pair; one, of 1792 triples, is
+  pairwise orthogonal **[census.open-orbits]**.
+
+Using a subgroup is sound. The orbits can only be finer than those of the full stabiliser, and PR1212 §10 transport
+needs only some Weyl element carrying one unit onto another. The 24 orbits match the full stabiliser's count,
+which an independent implementation found as well (see README). `UNITS.json` lists one representative per open
+orbit, the first triple of each in line order **[units.cover]**, with its pinned pivot frame F inside L.
+
+## Per-unit argument
+
+For each representative, the following facts are checked **[u.rigid]**:
+
+- PR1212 Lemma 2's D4 facts relative to F;
+- PR1212's (I3) on every complete class, with live witnesses;
+- PR1212's (I4): all 14 blocks carry a complete class, and complete classes glue through every shared pivot pair;
+- PR1399's Lemma 9 connectivity for every non-pivot live line outside a complete class, with the sign identity
+  for every witness;
+- **(I2) zero exclusion**: the zero-pattern CNF of PR1425 (families *two*, *four*, *diag*, *trans*), with the
+  clause "some pattern variable is true", is refuted by the DRUP proof in `PROOFS.json.gz`. That proof is
+  replayed by `verify.py`'s own two-watched-literal RUP checker and fails without that clause;
+- exact rational cross-checks of Lemma 9's rank-3 systems and of the §7 assembly on all 109 live lines;
+- the gauge pattern satisfies the CNF.
+
+Between 18 and 24 classes are complete, depending on the unit, and Lemma 9 carries the remaining 5–29 lines.
+
+The proof is then PR1425's verbatim:
+
+- **Step 1** (PR1399): Lemma 5 on each complete class and Lemma 6 on the set of complete classes give the gauge form
+  a_jf = d′_j ε_jf g_f and b_jf = 4 (d′_j g_f)⁻¹ ε_jf on those lines.
+- **Step 2:** Lemma 9 extends that form to every other non-pivot live line.
+- **Assembly:** PR1212 §7 gives K = D (2G) D⁻¹.
+
+Transport carries the result to every triple in the orbit. ∎
+
+## Counting
+
+| triples X of P112 | orbits | triples | rigid by |
+|---|---:|---:|---|
+| inside a P112 frame | 5 | 29232 | PR1419 (Lemma 10 from P104) |
+| not inside, pairwise orthogonal | 1 | 1792 | this package |
+| not inside, with an odd pair | 18 | 196896 | this package |
+| total | 24 | 227920 | |

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

@@ -0,0 +1,98 @@
+# Rank-8 masked decoders are gauge-rigid on every P109 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`) and PR1425 (`4b707c22`). It
+answers PR1425's open next question.
+
+PR1419's extension lemma makes P112 minus X rigid whenever X lies inside a frame of P112. For |X| = 3 that leaves
+198688 of the 227920 triples. Under the FRAME0 stabiliser they form 19 orbits: 18 contain an odd pair, and one
+(1792 triples) is pairwise orthogonal but extends to no P112 frame. This package proves rigidity on all 19 with
+PR1425's per-unit method ([PROOF.md](PROOF.md)):
+
+- a pivot frame passing PR1212's (I3) and (I4) with gluing;
+- PR1399's Lemma 9 connectivity for the lines outside complete classes;
+- a new DRUP refutation of the zero-pattern CNF for (I2) zero exclusion, with 1595 to 2945 lemmas per unit.
+
+**Consequence.** With PR1419, every P109 unit (P112 minus any three lines) is rigid. Every decoder with exactly
+eight costly terms in the E-graph model there has cst ≥ 61, which is PR968's 72 − p at p = 11.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 15 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p109/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P109: checks 25; all 19 open P109 orbits (198688 triples) rigid; with PR1419 every P109 unit is rigid; floor 61
+```
+
+`verify.py` is self-contained:
+
+- **Census.** It recomputes the orbit census of triples and the inside-a-frame split, and checks that the units
+  hit each open orbit once.
+- **Per unit.** It checks the pivot conditions, builds each CNF itself and replays the 19 proofs from
+  `PROOFS.json.gz` with its own RUP checker. It 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.
+
+`UNITS.json` and `PROOFS.json.gz` are regenerated in about 4 s by the command below, which needs python-sat
+(python-sat 1.9.dev15, Glucose 4.1, used here). Deletion lines are dropped, since the checker ignores them.
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p109/make_proof.py --out-dir /some/new/dir
+```
+
+Two one-time cross-checks were run but are not part of `verify.py`:
+
+- **PR1212's checker.** PR1212's `rup_check` at head `57099cb5` accepts all 19 proofs on this package's CNFs,
+  with the same lemma counts, and rejects every one without the zero clause.
+- **Independent census.** A separately written census matches the orbit table exactly: 24 orbits and every
+  (size, odd pairs, inside-a-frame) triple. It was written from a specification only, by OpenAI Codex, and
+  computed |H| = 344064 with 2025 frames.
+- **AI review.** A read-only adversarial review, also by OpenAI Codex, checked the CNF families, the lemma
+  hypotheses, subgroup coverage and the RUP checker, including 10000 random fuzz formulas. It found no soundness
+  gap. 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 29232 covered triples.
+
+  All of these PRs are open. PR968's premise (F6) is inherited through the floor. Attainment of 61 is not
+  checked.
+- **P108 and deeper.** The same method applies per orbit, but the open orbit count grows: 168 at |X| = 4 (see
+  below).
+- **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
+
+**P108: four-line punctures not inside a P112 frame.**
+
+- *Why it matters.* P109 is complete with this package. P108 is the next depth: 168 of 180 orbits, 6132952 of
+  6210820 quadruples. Both counts were found by this package's code and independently by the census above.
+- *A feasible first step.* A trial run of `make_proof.py`'s pivot rule and CNF on all 168 representatives found a
+  passing pivot and an unsatisfiable CNF for every one. That is 361027 lemmas, or about 5.9 MB gzipped. The run
+  was outside the package and is not certified here.
+- *The blocker.* Shipping per-orbit proofs at that size, plus a pure-Python census of 6.2 million quadruples, is
+  heavy. Deeper levels grow further, and the bottom level P105 alone has on the order of 10⁵ orbits. A
+  structural replacement for the DRUP step (I2) would remove that growth.
+
+## 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 (JosieElliston):** Lemma 9, the extension lemma with its 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, verifier and write-up. OpenAI Codex independently recomputed the orbit census and reviewed the package. Apache-2.0.

research/complex-rank8-rigidity-p109/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-p109/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 the 198688 triples X not inside a P112 frame (the part of P109 that PR1419's extension lemma cannot reach), equal to D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor 61 on every P109 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, and PR1425 for the rest of P110; PR1425's open next question is P109. 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 P109 unit, so the remaining masked escape routes are nine or more costly terms or punctures of depth four or more not inside a frame.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at P109 with one PR; P108 (168 open orbits, trial run only) and deeper punctures, and nine or more costly terms, are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 25 exact checks in about 15 s (generators; triple orbit census with the inside-a-frame split; one unit per open orbit; per unit 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). PR1212's rup_check independently accepts all 19 proofs, and an independently written census (OpenAI Codex, from a specification) matches the orbit table (both recorded, not run by verify.py); 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, verifier, CNF/RUP reimplementation 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 P108 units P112 minus X, |X| = 4, where X is not inside a frame of P112 (168 of 180 orbits, 6132952 of 6210820 quadruples)?",
+      "why_it_matters": "With this package and PR1419 every P109 unit is rigid; P108 is the next depth of the eight-term gap in the masked model.",
+      "first_step": "A trial run of make_proof.py's pivot rule and CNF on all 168 representatives found a passing pivot and an UNSAT CNF for each (361027 lemmas, about 5.9 MB gzipped); package it with a census of 4-subsets.",
+      "blocked_by": "Proof volume and a pure-Python census of 6.2 million quadruples; orbit counts keep growing toward P105 (order 1e5 orbits), so a structural replacement for the DRUP zero-exclusion step is needed to go deep."
+    }
+  ]
+}