Research: rank-8 masked decoders are gauge-rigid on P112 minus an odd pair — completes P110 with #1419 (no new κ)

research/complex-rank8-rigidity-p110-odd/PROOF.md

@@ -0,0 +1,72 @@
+# Rank-8 rigidity on P112 minus an odd pair
+
+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`). Finite facts
+marked **[X]** are recomputed by this package's `verify.py` (check id `X`, with `u` one of `meet4` and `meet2`).
+
+**Theorem.** Let x, y ∈ P112 with G_xy = ±1, and let L = P112 \ {x, y}. 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 such a unit has
+cst ≥ 62 = 72 − 10. This is PR968's Theorem 4(b) with p = 10, reached through PR1212 §8 verbatim. With
+PR1419, which covers the orthogonal pairs, this holds on every P110 unit, i.e. P112 minus any two lines.
+
+## Reduction to two units
+
+The FRAME0 stabiliser permutes the 2912 odd pairs of P112 in two orbits, of sizes 224 and 2688. They are
+distinguished by how many FRAME0 lines are odd to both x and y: 4 or 2 **[orbits.odd-pairs]**. By PR1212 §10
+transport, it suffices to treat one representative per orbit. Each has a pinned pivot frame F inside L, listed
+as root vectors in `verify.py` **[u.unit]**. Relative to F the D4 facts of PR1212 Lemma 2 hold
+**[u.d4-structure]**.
+
+The class profiles (live rows per class) are **[u.class-profile]**:
+
+- `meet4`: 24 complete classes, 2 with three live rows, and 2 empty (FRAME0 itself);
+- `meet2`: 22 complete classes, 2 with three live rows, and 4 with two.
+
+## Inputs
+
+Write I for the lines of complete classes and J for the other non-pivot live lines (6 for `meet4`, 14 for
+`meet2`).
+
+- **(I2) Zero exclusion.** No entry of a_i = K[i,F] or b_i = K[F,i] vanishes on T_i, for any rank-8
+  solution and any non-pivot live line i **[u.zero-exclusion]**. Rank K = 8 because K[F,F] = 4I, so
+  K = K[:,F] K[F,:] / 4, and a_i, b_i are supported on T_i by (E). Each clause family of the CNF is then a
+  necessary condition on the zero pattern:
+  - *two*: for orthogonal i, j with T_i ∩ T_j = {k, k′}, the sum a_ik b_jk + a_ik′ b_jk′ = 0, so one
+    product vanishes exactly when the other does;
+  - *four*: for orthogonal i, j with T_i = T_j, a sum of four products is 0, so exactly one of them cannot
+    be nonzero;
+  - *diag*: a_i · b_i = 16;
+  - *trans*: for a complete class C, A_C B_Cᵀ = 16 I because the class's rows are pairwise orthogonal
+    **[u.d4-structure]**, so A_C and B_C are nonsingular and have a nonzero transversal (PR1212 Lemma 3).
+
+  With the clause "some pattern variable is true" added, the CNF is refuted by a shipped DRUP proof. It is
+  replayed by `verify.py`'s own two-watched-literal RUP checker, and the proof's SHA256 and the CNF's digest
+  are pinned. Three controls back this up:
+  - the gauge pattern satisfies the CNF without that clause **[u.cnf-consistent]**;
+  - the same proof fails without that clause **[u.control-needs-zero-clause]**;
+  - unit propagation alone does not refute the formula **[u.control-bogus-proof]**.
+
+  PR1212's independent `rup_check` also accepts both proofs, with the same lemma counts. That was run once and
+  is recorded in the README; `verify.py` does not depend on it.
+- **(I3)** Every live group of every complete class has a live witness **[u.lemma5-witnesses]**.
+- **(I4)** All 14 blocks carry a complete class, and complete classes in distinct blocks glue through every
+  shared pivot pair **[u.lemma6-blocks-gluing]**.
+- **Lemma 9 input.** For each line of J, the column pairs of T_i witnessed by lines of I connect T_i. In
+  fact all six pairs are witnessed for every line, and the sign identity holds for every witness
+  **[u.lemma9-propagation]**.
+
+## Proof
+
+**Step 1** is PR1399's Step 1 verbatim. PR1212's Lemma 5 applies to each complete class, using (I2), (I3) and
+the class's own equations. Lemma 6 applies to the set of complete classes, using (I4). Together they give
+nonzero g_f and d′_j with a_jf = d′_j ε_jf g_f and b_jf = 4 (d′_j g_f)⁻¹ ε_jf for j ∈ I.
+
+**Step 2.** PR1399's Lemma 9 applies to each line of J, three-row and two-row alike. It needs only Step 1's
+form on I and the witness connectivity, so a_i = λ_i ε_i ∘ g and b_i = 4/λ_i · ε_i / g. The witnessed (E2)
+equations have rank 3 on a_i|T and on b_i|T, with these kernels **[u.lemma9-solution-line]**.
+
+**Assembly.** Every non-pivot live line is now in PR1212 §7's form, and §7 gives K = D (2G) D⁻¹. An exact
+rational control checks the assembly on all 110 live lines **[u.assembly-control]**. ∎

research/complex-rank8-rigidity-p110-odd/README.md

@@ -0,0 +1,83 @@
+# Rank-8 masked decoders are gauge-rigid on P112 minus an odd pair, which completes P110 (no new κ)
+
+**Status: scoped structural result. No κ claim, no construction.** It extends the rank-8 rigidity line of PR1212
+(burntout76, open, head `57099cb5`) and PR1399 (open, head `4e1ba3a1`). It answers PR1419's open next question.
+
+PR1419 shows that rank-8 rigidity of PR1212's system (E) passes to supersets. That makes P112 minus any
+orthogonal pair rigid, but it cannot reach an **odd pair**, because no frame contains one. The 2912 odd pairs
+form two FRAME0-stabiliser orbits, of sizes 224 and 2688. This package proves rigidity on both, by PR1212's
+method plus PR1399's Lemma 9 ([PROOF.md](PROOF.md)). Each orbit representative has a pivot frame with:
+
+- **(I2) zero exclusion**: a new DRUP refutation per orbit, 1893 and 2320 lemmas;
+- **(I3) and (I4)**, plus gluing, on the complete classes;
+- **Lemma 9 witness connectivity** for every line of an incomplete class, with all six column pairs
+  witnessed.
+
+**Consequence.** With PR1419, every P110 unit (P112 minus any two lines) is rigid. Every decoder with exactly
+eight costly terms in the E-graph model there has cst ≥ 62, which is PR968's 72 − p at p = 10.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 2 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p110-odd/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P110_ODD: checks 26; both odd-pair orbits (224 + 2688) rigid; with PR1419 every P110 unit is rigid; floor 62
+```
+
+`verify.py` is independent of PR1212's code. It has its own E8 model, stabiliser orbits, classes, witnesses,
+gluing, Lemma 9 checks, zero-pattern CNF and two-watched-literal RUP checker. It replays the shipped
+`proof-meet4.drup` and `proof-meet2.drup` against CNFs it builds itself, and pins the SHA256 of both the proofs
+and the CNFs. Its controls:
+
+- the gauge zero pattern satisfies the CNF without the "some entry vanishes" clause;
+- the proofs fail without that clause;
+- a bare empty-clause proof is rejected.
+
+To regenerate the proofs, which needs python-sat (python-sat 1.9.dev15, Glucose 4.1, used here):
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p110-odd/make_proof.py --out-dir /some/new/dir
+```
+
+As a one-time cross-check, not part of `verify.py`, PR1212's `rup_check` (head `57099cb5`) accepts both proofs
+on this package's CNFs, with the same lemma counts, and rejects them without the zero clause.
+
+## Not covered
+
+- **P105–P109 punctures containing an odd pair**, and orthogonal punctures outside a frame (see PR1419's
+  census). The method here applies per orbit, but the orbit counts grow quickly with |X|.
+- **Inherited steps.** PR1212's Lemmas 5–6, §7 assembly and §10 transport, and PR1399's Lemma 9, are cited,
+  not re-derived. Both PRs are open. PR968's premise (F6) is inherited through the floor. Attainment of 62 on
+  these units is not checked.
+- **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
+
+**P109: three-line punctures with an odd pair.**
+
+- *Why it matters.* With this package P110 is complete. P109 is the next depth, and PR1419's census leaves
+  198688 of its 227920 punctures uncovered.
+- *A feasible first step.* Enumerate the FRAME0-stabiliser orbits of 3-subsets of P112 that are not inside a
+  P112 frame. Then run `make_proof.py`'s pivot rule and CNF per orbit, which is about 1 s per unit here.
+  Lemma 10 of PR1419 reduces the work: any rigid sub-unit settles every superset.
+- *The blocker.* The number of orbits is not yet known. Each orbit needs its own certificate, unless a
+  rigid sub-unit is found first.
+
+## 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 (JosieElliston):** Lemma 9 and the extension lemma with its census.
+
+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-p110-odd/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-p110-odd/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: is every rank-<=8 solution of PR1212's system (E) on P112 minus an odd pair (the part of P110 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 62?",
+  "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, and PR1419 for punctures inside a frame; PR1419's open next question is the two odd-pair P110 orbits. This closes them, completing P110; 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 P110 unit, so the remaining masked escape routes are nine or more costly terms or deeper punctures with odd pairs.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at P110; P109 and deeper punctures with an odd pair, and nine or more costly terms, are left as handoffs.",
+  "outcome": "completed",
+  "evidence": "verify.py: 26 exact checks in about 2 s (orbits of odd pairs; per orbit representative the unit, D4 structure, class profile, (I3), (I4) and gluing, Lemma 9 connectivity and algebra, assembly, CNF consistency, DRUP replay of zero exclusion with its own RUP checker, and two proof controls). PR1212's rup_check independently accepts both proofs (recorded, not run by verify.py).",
+  "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. Submitted by the account holder.",
+  "open_questions": [
+    {
+      "question": "Does rank-8 rigidity of (E) hold on P109 units P112 minus X, |X| = 3, where X is not inside a frame of P112 (198688 of 227920 triples)?",
+      "why_it_matters": "With this package and PR1419 every P110 unit is rigid; P109 is the next depth of the eight-term gap in the masked model.",
+      "first_step": "Enumerate the FRAME0-stabiliser orbits of the uncovered triples and run make_proof.py's pivot rule and CNF on one representative per orbit (about 1 s per unit at P110); use PR1419's Lemma 10 whenever a rigid sub-unit exists.",
+      "blocked_by": "The orbit count is not yet known, and each orbit needs its own zero-exclusion certificate unless a rigid sub-unit is found."
+    }
+  ]
+}

research/complex-rank8-rigidity-p110-odd/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": "26 exact checks: odd-pair orbits; per representative unit, D4 structure, class profile, (I3), (I4)/gluing, Lemma 9 connectivity and algebra, assembly, CNF consistency, DRUP zero-exclusion replay with the package's own RUP checker, and two proof controls."
+    }
+  ]
+}

research/complex-rank8-rigidity-p110-odd/make_proof.py

@@ -0,0 +1,68 @@
+#!/usr/bin/env python3
+"""Choose the two orbit representatives and pivots, and regenerate the DRUP refutations that verify.py
+replays (needs python-sat; verify.py itself does not).
+
+    python3 -I -B research/complex-rank8-rigidity-p110-odd/make_proof.py --out-dir /new/dir
+
+Representatives: the lexicographically first odd pair (in verify.py's line order) with each FRAME0 meet.
+Pivot: the first frame inside the live set, in line order, that passes (I3), (I4), gluing and Lemma 9
+connectivity. Any DRUP-producing solver may be substituted; verify.py checks the proof, not the solver.
+"""
+import argparse
+import hashlib
+import itertools
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+import verify as V  # noqa: E402
+
+
+def frames_in(live):
+    live = sorted(live)
+    out = []
+
+    def grow(cur, cand):
+        if len(cur) == 8:
+            out.append(cur)
+            return
+        for n, j in enumerate(cand):
+            grow(cur + [j], [k for k in cand[n + 1:] if V.G[j][k] == 0])
+
+    grow([], live)
+    return out
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument('--out-dir', required=True)
+    ap.add_argument('--solver', default='g4')
+    args = ap.parse_args()
+    from pysat.solvers import Solver
+    out = Path(args.out_dir)
+    for m in (4, 2):
+        pair = next(p for p in itertools.combinations(V.P112, 2)
+                    if V.G[p[0]][p[1]] != 0 and V.meet(frozenset(p)) == m)
+        live = [i for i in V.P112 if i not in pair]
+        F = next(F for F in frames_in(live) if V.passes(V.inputs(live, F)))
+        cnf, zvars = V.build_cnf(live, F)
+        with Solver(name=args.solver, bootstrap_with=cnf.clauses + [zvars], with_proof=True) as s:
+            if s.solve():
+                print(f'meet{m}: UNEXPECTED satisfiable')
+                return 1
+            proof = s.get_proof()
+        path = out / f'proof-meet{m}.drup'
+        if path.exists():
+            print(f'refusing to overwrite {path}')
+            return 2
+        text = '\n'.join(proof) + '\n'
+        path.write_text(text)
+        print(f"meet{m}: pair {[V.LINES[i] for i in pair]}")
+        print(f"meet{m}: pivot {[V.LINES[i] for i in F]}")
+        print(f"meet{m}: {len(proof)} proof lines, sha256 {hashlib.sha256(text.encode()).hexdigest()}, "
+              f"cnf {V.cnf_digest(cnf.clauses + [zvars])}")
+    return 0
+
+
+if __name__ == '__main__':
+    sys.exit(main())