Research: rank-8 masked decoders are gauge-rigid on P111 and type-(4,4) P104 units (no new kappa)

research/complex-rank8-rigidity-p111-p104-44/PROOF.md

@@ -0,0 +1,104 @@
+# Rank-8 rigidity on P111 and the type-(4,4) 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 a P111 unit (P112 minus one line) or one of the 28 type-(4,4) P104 units, and 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 has cst ≥ 63 on P111 and
+cst ≥ 56 on the type-(4,4) units. This is PR968's floor at p = 9 and p = 16, reached through PR1212's §8
+verbatim. PR717's P111 decoders attain 63. Sharpness at 56 on the (4,4) units is not checked; PR968's
+frame-pair decoders do not exist on them.
+
+By PR1212 §10 transport, the stabiliser of FRAME0 is transitive on the 112 lines and on the 28 type-(4,4)
+frames **[1212: G.line-orbits, G.frame-orbits]**. It therefore suffices to treat one representative of each,
+with PR1212's pivot F **[pr1212.*.pivot-vectors]**. Zero exclusion (Lemma 8) holds on both
+representatives with these pivots **[1212: G.P111.zero-exclusion, G.P104-44.zero-exclusion]**.
+
+Call a class *usable* if it has at least three live rows.
+
+## Profiles
+
+- **P111:** 25 complete classes, one class C* with three live rows, and two empty classes
+  **[P111.class-profile]**. C*'s block contains no other usable class.
+- **Type (4,4):** 24 complete classes and four empty ones, so two complementary blocks carry nothing
+  **[P104-44.class-profile]**.
+
+In both units every live non-pivot line lies in a usable class **[\*.lines-in-usable-classes]**.
+
+## Lemma 5′ (three-row classes)
+
+Let C be a class with live rows 1, 2, 3 (row 4 dead) and support T = {a, b, c, d}. Then, for nonzero
+scalars δ_i and γ_f,
+
+    a_if = δ_i ε_if γ_f,      b_if = 4 δ_i⁻¹ ε_if γ_f⁻¹.
+
+*Proof.* By (E4) and (E0) the 3 × 4 class matrices satisfy A_C B_Cᵀ = 16 I₃, so both have rank 3.
+
+Each of the three row matchings of Lemma 2(d) has exactly one pair inside {1, 2, 3}, and the three pairs are
+distinct **[\*.three-row-lemma]**. So every column pair has one live group. Its Step-1 witness exists
+**[\*.group-witnesses]**. Step 1 of PR1212's Lemma 5 then applies to that group, and by the same argument
+with a and b exchanged, to b as well. This uses (E2) in the order a_j · b_i and zero exclusion of a_j.
+
+With the rows of u_if = a_if ε_if written as (1, x_i, y_i, z_i) and the columns labelled as in PR1212
+Step 3, the group relations are:
+
+- from {1,2}: x₁ = x₂ and y₁/z₁ = y₂/z₂;
+- from {1,3}: y₁ = y₃ and x₁/z₁ = x₃/z₃;
+- from {2,3}: z₂ = z₃ and x₂/y₂ = x₃/y₃.
+
+Put x = x₁ = x₂, y = y₁ = y₃, Z = z₂ = z₃, and let z = z₁, Y = y₂, X = x₃ be the remaining entries. Then
+Y = yZ/z and X = xZ/z, and the third ratio gives xy = XY = xyZ²/z², so Z = ±z.
+
+- Z = z gives equal rows: this is the stated form for a.
+- Z = −z gives the rows (1, x, y, z), (1, x, −y, −z), (1, −x, y, −z). The class's own sign rows, normalised
+  to a first row and column of +1, have the same group structure, so they equal this pattern. Then
+  A_C = diag(δ) D_r J D_c diag(γ) has rank 1, which contradicts rank 3 **[\*.three-row-lemma]**.
+
+The same holds for b, so b_if = δ′_i ε_if γ′_f.
+
+Within-class equations then require Σ_f ε_if ε_jf w_f = 0 for i ≠ j, where w_f = γ_f γ′_f. The three
+products ε_i ∘ ε_j of distinct live rows are independent and orthogonal to the all-ones vector
+**[\*.three-row-lemma]**, so they span its orthogonal complement and w = μ·1. Finally (E0) gives
+4 δ_i δ′_i μ = 16. ∎
+
+With two live rows this step fails: one product leaves w three free directions
+**[control.two-row-not-forced]**.
+
+## Lemma 6′ (gluing)
+
+Lemma 5 (complete classes) and Lemma 5′ give every usable class C a column scaling γ^C.
+
+**Relation (5) between classes.** For usable classes C ≠ C′ in distinct blocks through {k, k′}, any live
+orthogonal pair i ∈ C, j ∈ C′ whose supports meet in exactly {k, k′} yields relation (5), exactly as in
+PR1212.
+
+**Well-defined ratio.** For every pivot pair, the usable classes whose support contains it are nonempty and
+connected by such witnessed relations **[\*.gluing-connected]**. So ρ_kk′ := γ^C_k / γ^C_k′ is well
+defined.
+
+**Cocycle.** Inside one usable class, ρ_kk′ ρ_k′k″ = ρ_kk″. Fix a base point k₀ and set g_k := ρ_{k k₀}.
+For k, k′ ≠ k₀:
+
+- If the block of {k, k′, k₀} is usable, then ρ_kk′ = g_k / g_k′ directly.
+- Otherwise there is an m whose triples {k, k′, m}, {k, m, k₀} and {k′, m, k₀} all lie in usable blocks
+  **[\*.gluing-cocycle]** (every base point works on both units). Then
+  ρ_kk′ = ρ_km ρ_mk′ = (g_k / g_m)(g_m / g_k′).
+
+This is a multiplicative identity, so it holds over any field. The additive rank 21 = 28 − 7
+**[\*.cocycle-rank]** is a cross-check only.
+
+Hence γ^C = c_C g|_T for every usable class C. ∎
+
+The path condition is not vacuous. With four of the twelve usable (4,4) blocks removed, the relations drop
+to rank 17 and no base point passes **[control.path-condition-bites]**.
+
+## Assembly
+
+PR1212 §7 applies verbatim to all live non-pivot lines, which lie in usable classes. It gives
+K = D (2G) D⁻¹. An exact rational control checks the assembly on both units
+**[\*.assembly-control, control.perturbed-fails]**. ∎

research/complex-rank8-rigidity-p111-p104-44/README.md

@@ -0,0 +1,88 @@
+# Rank-8 masked decoders are gauge-rigid on P111 and the type-(4,4) 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.
+
+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⁻¹`. It proves this on
+P112, P120 and the 336 type-(2,2,2,2) P104 units. As a result, decoders with exactly eight costly terms
+keep PR968's floor there. Its PROOF.md §10 names two remaining gaps:
+
+- **P111** (112 units): one class keeps three live rows, and its block has no complete class.
+- **Type-(4,4) P104** (28 units): two blocks carry no live class, so Lemma 6's cocycle step has no witness.
+
+This package closes both gaps ([PROOF.md](PROOF.md)):
+
+- **Lemma 5′.** A class with three live rows has the same Lemma-5 form. PR1212 notes that the group
+  relations again force two cases, and that case (ii) has rank 1 < 3. What is new here is the `b` side:
+  without a square class matrix, the in-class equations force `γ_f γ′_f` to be constant, because the three
+  pairwise sign products span the non-trivial characters.
+- **Lemma 6′.** The gluing works whenever the usable classes through each pivot pair are connected and an
+  explicit three-triple path exists. This holds on both units with 14/14 and 12/14 usable blocks. The
+  argument is multiplicative and is valid over any field of characteristic 0.
+
+**Consequence.** In the E-graph model, every decoder with exactly eight costly terms has `cst ≥ 63` on every
+P111 unit (attained by PR717's P111 hits) and `cst ≥ 56` on every type-(4,4) P104 unit. Sharpness of 56 on
+these units is not checked.
+
+## Reproduce
+
+From the repository root, Python 3.10+, standard library only, about 1 s:
+
+```sh
+python3 -I -B research/complex-rank8-rigidity-p111-p104-44/verify.py
+```
+
+Expected final line:
+
+```text
+PASS_COMPLEX_RANK8_RIGIDITY_P111_P104_44: checks 26; P111 three-row 1, blocks 14/14; P104-44 blocks 12/14 path-glued; floors 63/56; zero exclusion cited from PR1212
+```
+
+To also replay PR1212's zero-exclusion DRUP refutations and orbit transport (about 15 s), first make a
+checkout of PR1212's head. The verifier checks the git blobs of its `verify.py` and two `.drup` files, then
+runs it:
+
+```sh
+git fetch origin pull/1212/head && git worktree add --detach /tmp/pr1212 57099cb5
+python3 -I -B research/complex-rank8-rigidity-p111-p104-44/verify.py --pr1212-dir /tmp/pr1212
+```
+
+The verifier is an independent implementation, with its own E8 model, classes, witnesses, gluing and
+assembly. It imports nothing from PR1212. It checks units and pivots given as root vectors and confirms that
+these match PR1212's pivot indices. The controls show four things:
+
+- two-row classes are not forced;
+- P111 needs Lemma 5′;
+- the path condition rejects a rank-deficient block set;
+- a perturbed entry breaks (2).
+
+## Not covered
+
+- **The 896 admissible P104 units** (PR717's P104 among them). Four classes keep only two live rows, and
+  Lemma 5′ fails there. PR1292 (Navinor) proves local rigidity only.
+- **Nine or more costly terms**, including PR717's mixed-β problem.
+- **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
+
+**Rigidity on the admissible P104 units.** This matters because PR968's 7/13 ratio is attained there, so an
+off-orbit masked solution there would be the cheapest escape from the floor. The first step is a two-row
+variant of Lemma 5 that uses the cross-block relations (5) with the neighbouring four-row classes to fix the
+one-parameter in-class family. This is blocked on writing that argument. The in-class relations alone
+provably do not suffice (`control.two-row-not-forced`).
+
+## Credit
+
+- **burntout76 / Brett Halligan (PR1212):** the theorem, the proof skeleton and every lemma reused here,
+  zero exclusion, the transport, and the handoff naming this step.
+- **themilkman216 (PR968):** the eight-term floor.
+- **DreamingOfClouds (PR717):** the E-graph model and the P111 decoders.
+- **Navinor (PR1292):** local P104 rigidity.
+
+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-p111-p104-44/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-p111-p104-44/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 P111 and on the 28 type-(4,4) P104 units equal D(2G)D^-1, so that decoders with exactly eight costly terms keep PR968's floor (63 on P111, 56 on (4,4))?",
+  "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/type-(2,2,2,2) and listed P111 and type (4,4) as open (its PROOF.md section 10). This closes those two gaps; 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 two more puncture families, narrowing where a cheaper masked decoder could exist (nine or more costly terms, or the 896 admissible P104 units).",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at P111 and type (4,4); the two-row classes of the admissible P104 units need a different argument and are left as a handoff.",
+  "outcome": "completed",
+  "evidence": "verify.py: 26 exact checks plus 4 controls; --pr1212-dir replays PR1212's zero-exclusion DRUP proofs and orbit transport from blob-pinned files.",
+  "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 hold on the 896 admissible P104 units (PR717's P104 among them), where four classes keep only two live rows?",
+      "why_it_matters": "These are the units where PR968's 7/13 ratio is attained; an off-orbit masked solution there would be the cheapest escape from the floor.",
+      "first_step": "For a two-row class, Lemma 5 leaves a one-parameter family; test whether the cross-block relations (5) with the neighbouring four-row classes fix it, on PR1212's pivot.",
+      "blocked_by": "Needs a two-row variant of Lemma 5 that uses gluing equations, not only in-class relations; PR1292 gives local rigidity only."
+    }
+  ]
+}

research/complex-rank8-rigidity-p111-p104-44/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 structural checks on the P111 and type-(4,4) units (pivot, D4 blocks, class profile, group witnesses, three-row lemma, gluing connectivity and path condition, assembly) and 4 negative controls. PR1212 zero exclusion is cited; replay it with --pr1212-dir."
+    }
+  ]
+}