Research: masked rank-8 complex decoders are locally rigid on all P104 frame-pair punctures (no new kappa)

research/complex-p104-masked-local-rigidity/README.md

@@ -0,0 +1,133 @@
+# Masked rank-8 complex decoders are locally rigid on every frame-pair puncture (no new κ)
+
+**Status: scoped structural result (an exact infinitesimal certificate) plus a seeded finite sample.
+No κ claim and no new supplier.** The selected κ = 0.001672660197076918 and every existing file are
+unchanged.
+
+## Task card
+
+- **Card.** `complex-masked-decoder` (complex-mechanisms track), chooser nonce
+  `f98900d1d6bdb1d91a0247b80be5acee`, scope key `7acfe4d9cac04f7ba4cb`. Scope **refined**: before
+  synthesizing a masked decoder, test whether masking can deform the cheapest known decoders at all.
+- **Base and predecessors.** Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`.
+  https://github.com/CrocSwap/integer-mult-bounds/pull/717 (open, head `4a97676`) defines the masked
+  (E-graph) model; https://github.com/CrocSwap/integer-mult-bounds/pull/968 (merged,
+  `research/complex-frame-pair-decoders`) gives the frame-pair decoders and the all-pairs floor;
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1212 (open, head `072ae2f`) proves global rank-8
+  rigidity on P112 and P120 and lists P104 as numerical evidence only.
+- **Changed assumption.** The eight-term floor assumes exactness on all live pairs. Here only the
+  E-graph entries are fixed (diagonal and orthogonal pairs); odd entries are free, because cost-0 terms
+  can repair them.
+- **Object and question.** Real K on the live lines with K_ii = 4, K_ij = 0 for orthogonal live pairs and
+  rank K ≤ 8. Near K0 = 2G, is the solution set only the diagonal-torus orbit D K0 D⁻¹, on every
+  frame-pair puncture P104 = P120 − F0 − F1?
+- **Domain.** P120, P112 and all 1260 frames F1 disjoint from a fixed F0, plus 8 seeded random
+  punctures at each p = 24, 32, ..., 80. Budget 60 minutes; local only.
+- **Optimistic payoff.** A masked deformation with smaller supports would lower the copy charge below
+  the 7/13 ratio, about 2.8% of b per copy unit in the earlier knob calculus. The certificate shows that
+  no such deformation exists near the normal form, so the local payoff is zero.
+- **Claim.** https://github.com/CrocSwap/integer-mult-bounds/discussions/1275
+
+## Result
+
+**Local rigidity.** Let L be the live lines of P120, of P112, or of any P104 frame-pair puncture, and let
+V be the set of real L × L matrices K with rank K ≤ 8, K_ii = 4 and K_ij = 0 for orthogonal live pairs.
+Then the tangent space of V at K0 = 2G is the tangent space of the torus orbit {D K0 D⁻¹} (dimension
+v − 1). Because that orbit lies in V, V coincides with the orbit on a neighbourhood of K0. The
+statement holds over C as well, since every rank used below is a rank of a rational matrix.
+
+**Decoder consequence.** A live frame F has K[F, F] = 4I under the mask, so every K in V has rank exactly
+8. An eight-costly-term masked decoder whose costly part is close enough to 2G therefore equals
+D(2G)D⁻¹. Its rank-8 factorization has the all-pairs normal form supports of
+https://github.com/CrocSwap/integer-mult-bounds/pull/968, so that package's floor applies: cost at least
+56 on P104 and copy ratio at least 7/13 for punctures of at most 24 lines. Masking cannot locally move
+the frame-pair decoders.
+
+**Certificate (exact).** Rank-8 matrices near K0 = L Lᵀ/2 (doubled root coordinates) have tangent
+vectors Δ = L Mᵀ + N Lᵀ. For each live line i, the lines E(i) = {i} ∪ {live j orthogonal to i} span
+Q⁸, so the masked equations of row i determine N_i from M; what remains is a linear system in M alone,
+with 8v unknowns.
+
+- *Upper bound.* Over F_p with p = 2³¹ − 1 that system has rank 7v − 63. Rank over F_p never exceeds rank
+  over Q, so its rational kernel has dimension at most v + 63.
+- *Lower bound.* The gauge vectors M = L S (64) and torus vectors M = −T L/2 (one per line) satisfy the
+  equations (Δ = 0 and Δ = [T, K0] respectively, which vanish on the mask), and their span has rank
+  64 + v − 1 over F_p, hence over Q.
+- The two bounds meet. Removing the 64 gauge directions, which give Δ = 0, leaves exactly the v − 1 torus
+  directions.
+
+**Coverage of all 1260 frame pairs.** Breadth-first search with the 120 root reflections reaches all
+2025 frames, giving explicit words w_F with w_F(F0) = F. Schreier elements w_{sF}⁻¹ s w_F fix F0 and
+preserve |G|; 66 of them merge the 1260 frames disjoint from F0 into three classes of sizes 896, 336
+and 28. These are the three relative positions found in
+https://github.com/CrocSwap/integer-mult-bounds/pull/968. The masked system is invariant under such
+elements up to a sign conjugation, so one certified representative covers its class. For the three
+representatives every equation is inserted, and the rank is exactly 665 = 7 · 104 − 63.
+
+**Sample and control.**
+
+- 64 of 64 seeded random punctures with 24 to 80 lines pass the same exact certificate. This is a finite
+  sample, not a theorem about every puncture.
+- The decomposable live set D4 ⊕ D4 (24 lines in two mutually orthogonal blocks) is rejected, with rank
+  64 against a target of 105, and a known span of 86 because its torus splits into two components.
+- The equations of the known kernel are rechecked on random combinations for every certified set.
+- Corroboration: the P112 tangent rigidity recorded as checked in
+  https://github.com/CrocSwap/integer-mult-bounds/pull/717 (D1) is reproduced here by a separate exact
+  method.
+
+## Reproduce
+
+From the repository root, Python 3.10+ and the standard library (about 70 s):
+
+```sh
+python3 -I -B research/complex-p104-masked-local-rigidity/verify.py
+python3 scripts/research_package.py --package research/complex-p104-masked-local-rigidity --check-only
+```
+
+Expected final line:
+
+```text
+PASS_P104_MASKED_LOCAL_RIGIDITY: P120, P112 and all 1260 frame-pair punctures (3 classes) infinitesimally rigid at 2G; D4+D4 control rejected; seeded sample p=24..80 rigid 64/64; local only, no new kappa
+```
+
+## Scope and remaining obligations
+
+- **Local only.** Components of V away from the torus orbit are not excluded on P104. The global
+  statement is proved for P112 and P120 in https://github.com/CrocSwap/integer-mult-bounds/pull/1212,
+  not here.
+- **Not covered.** Nine or more costly terms (rank-9 costly parts); punctures other than the frame pairs
+  except the seeded sample; masked identities on other entry sets; physical copy trees, frames,
+  restoration and hosting.
+- **Inherited.** The decoder consequence uses the floor theorem and cited flat classification of
+  https://github.com/CrocSwap/integer-mult-bounds/pull/968. All all-size/compiler, realization, hosting,
+  precision/tape and analytic obligations of the selected record remain. Finite checks are not a formal
+  proof of integer multiplication, and the argument has not had independent human review.
+
+## Open next questions
+
+1. **Global rigidity on P104.** An off-orbit component could have smaller supports and beat 7/13. First
+   step: pivot on a live frame F (the mask forces K[F, F] = 4I, so K = K[:, F] K[F, :]/4) and solve the
+   bilinear system for each of the three classes. Blocked by a written case analysis comparable to the
+   P112/P120 proof of https://github.com/CrocSwap/integer-mult-bounds/pull/1212.
+2. **Nine masked costly terms on P104.** This is the mixed-β problem of
+   https://github.com/CrocSwap/integer-mult-bounds/pull/717 at the ratio-optimal puncture; rank-8
+   rigidity does not constrain rank-9 costly parts. First step: the same tangent computation at rank 9
+   for one fixed ninth support on one class. Blocked by the choice of a support alphabet.
+
+Structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+- DreamingOfClouds: the masked (E-graph) decoder model, cost-0 repair terms and the P112 tangent
+  rigidity in https://github.com/CrocSwap/integer-mult-bounds/pull/717.
+- themilkman216: frame-pair decoders, the 7/13 floor and the three relative positions in
+  https://github.com/CrocSwap/integer-mult-bounds/pull/968.
+- burntout76: global rank-8 rigidity on P112/P120 and the P104 question in
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1212.
+- Related masked P112 work: https://github.com/CrocSwap/integer-mult-bounds/pull/1213,
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1226,
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1236 and
+  https://github.com/CrocSwap/integer-mult-bounds/discussions/1267 concern a different puncture;
+  https://github.com/CrocSwap/integer-mult-bounds/pull/1071 bounds physical delivery for the frame-pair
+  centres, a separate obligation.
+- Prepared by Navinor with help from opencode. Apache-2.0.

research/complex-p104-masked-local-rigidity/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8",
+  "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-p104-masked-local-rigidity/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-masked-decoder",
+  "priority_revision": 2,
+  "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8",
+  "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": "Masked (E-graph) exactness with eight costly terms: real K on the live lines with K_ii = 4, K_ij = 0 on orthogonal live pairs, odd entries free, rank K <= 8. Exact infinitesimal rigidity of this solution set at K0 = 2G on P120, P112 and all 1260 frame-pair punctures P104 = P120 - F0 - F1 (three classes under explicit stabilizer elements), plus a seeded exact sample of 64 random punctures with 24 to 80 lines.",
+  "scope_change_reason": "Before synthesizing a masked decoder, test whether masking can deform the cheapest known decoders at all. The changed assumption is the all-pairs exactness of the eight-term bound (odd entries become free); the frame-pair punctures attain the 7/13 copy ratio, so they are where a masked deformation would matter first.",
+  "bottleneck_link": "The complex side binds. A masked deformation of the frame-pair decoder with smaller supports would lower the copy charge below the 7/13 ratio. Local rigidity shows that no such deformation exists near the all-pairs normal form, so any masked gain at P104 must come from a separate solution component.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the exact tangent certificate covers every frame-pair class, or after the first exact non-torus tangent direction (which would become the lead). No global solution-set search was attempted within the budget.",
+  "outcome": "negative-result",
+  "evidence": "verify.py: 9 exact checks. rank over F_p (p = 2^31 - 1) of the masked tangent system is 7v - 63 and the explicit gauge plus torus directions span 64 + v - 1, so the tangent space of the solution set equals the torus tangent (dimension v - 1) for P120, P112 and the three P104 classes (896, 336 and 28 frames); a decomposable D4 + D4 live set is rejected; 64 of 64 seeded deeper punctures pass.",
+  "author": "Navinor",
+  "ai_assistance": "Prepared with help from opencode (research, implementation and documentation).",
+  "open_questions": [
+    {
+      "question": "Is the masked rank-8 solution set on each P104 frame-pair puncture globally equal to the torus orbit of 2G?",
+      "why_it_matters": "An off-orbit component could have smaller term supports than the frame-pair decoder and beat the 7/13 copy ratio; local rigidity cannot exclude it.",
+      "first_step": "Pivot on a live frame F (the mask forces K[F,F] = 4I, so K = K[:,F] K[F,:] / 4) and solve the resulting bilinear system class by class for the three frame-pair classes.",
+      "blocked_by": "Needs a written case analysis comparable to the P112/P120 global proof in https://github.com/CrocSwap/integer-mult-bounds/pull/1212; not started here."
+    },
+    {
+      "question": "Do nine or more costly terms with masked exactness admit cheaper decoders on P104?",
+      "why_it_matters": "This is the mixed-beta problem of https://github.com/CrocSwap/integer-mult-bounds/pull/717 moved to the ratio-optimal puncture; rank-8 rigidity does not constrain rank-9 costly parts.",
+      "first_step": "Repeat the tangent computation at rank 9 for a fixed ninth support pattern on one P104 class.",
+      "blocked_by": "Needs a chosen support alphabet for the ninth term; no candidate is proposed here."
+    }
+  ]
+}

research/complex-p104-masked-local-rigidity/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Exact F_p rank and explicit kernel for the masked tangent system on P120, P112 and the three frame-pair classes (identity); seeded deeper punctures (positive sample); decomposable D4 + D4 live set must be rejected (failure control)."
+    }
+  ]
+}