Research: Eisenstein E8 decoder copy floor 23 via submatrix-minrank certificates (past the clique-method limit; no κ claim)

research/eisenstein-submatrix-copy-floor/AUTOMORPHISMS.json

@@ -0,0 +1 @@
+{"base_pair": [0, 1], "generators": [[0, 2, 1, 3, 4, 6, 5, 10, 9, 8, 7, 11, 20, 21, 23, 22, 27, 26, 25, 24, 12, 13, 15, 14, 19, 18, 17, 16, 29, 28, 30, 31, 34, 35, 32, 33, 37, 36, 38, 39], [0, 3, 13, 1, 20, 5, 18, 9, 16, 7, 14, 21, 12, 2, 10, 23, 8, 27, 6, 25, 4, 11, 26, 15, 24, 19, 22, 17, 28, 29, 37, 33, 38, 31, 36, 35, 34, 30, 32, 39], [0, 4, 12, 1, 21, 8, 15, 6, 19, 10, 17, 20, 13, 2, 5, 24, 9, 22, 7, 26, 3, 11, 23, 16, 27, 14, 25, 18, 29, 28, 36, 34, 37, 32, 38, 30, 31, 33, 35, 39], [0, 5, 15, 1, 22, 10, 13, 4, 16, 7, 19, 23, 14, 2, 3, 26, 8, 20, 9, 25, 6, 11, 21, 18, 24, 12, 27, 17, 30, 31, 37, 33, 36, 34, 39, 28, 29, 35, 32, 38], [1, 2, 0, 3, 4, 5, 6, 7, 8, 9, 10, 11, 29, 28, 31, 30, 33, 32, 35, 34, 13, 12, 15, 14, 17, 16, 19, 18, 20, 21, 22, 23, 24, 25, 26, 27, 36, 37, 38, 39]]}

research/eisenstein-submatrix-copy-floor/README.md

@@ -0,0 +1,138 @@
+# Eisenstein E8 decoder copy floor: 23, past the clique-method limit
+
+**Research note; no new supplier, no κ change, selected record untouched.**
+In the abstract Eisenstein E8 scalar binary decoder model of
+[`research/eisenstein-clique-copy-bound`](../eisenstein-clique-copy-bound/PROOF.md)
+(Jonathan Lam, PR798), every fitting decomposition costs **at least 23**
+Eisenstein pairing-rank units. PR798 proved 22 and showed that *no* weighting
+of cliques can prove more. This package adds the ingredient that its PROOF.md
+says is needed: rank bounds on non-clique principal submatrices.
+
+```sh
+python3 -B research/eisenstein-submatrix-copy-floor/verify.py
+```
+
+Expected (about 35 s, standard library only, any CPython 3.10+):
+
+```text
+PASS_EISENSTEIN_SUBMATRIX_COPY_FLOOR: C >= 23; objective 30200/1367; 296321 flat pairs; 540 S_uw sets minrank 10; 5 controls; no new kappa
+```
+
+The geometry (40 K-lines, orthogonality, all 772 flats, pairing ranks, all
+cliques) is imported unchanged from PR798's pinned `geometry.py`.
+
+## Model (PR798, unchanged)
+
+`B` is a 40×40 matrix over F2 with `B_tt = 1` and `B_ts = 0` for distinct
+nonorthogonal lines; entries on orthogonal pairs are free in both directions.
+A decomposition `B = Σ_j 1_Rj 1_Aj^T` costs `C = Σ_j c(R_j, A_j)`, with
+`c(R,A) = rank_Q(V_R V_A^T)/2`. `N[x]` is `x` plus its 27 nonorthogonal lines.
+
+## Proof
+
+**Lemma 1 (zero-cost totals can be dropped).** If `c(R,A) = 0` then
+`X_R ⊥ X_A`, so every `(t,s) ∈ R×A` is an orthogonal pair of distinct lines
+(the form is positive definite): a free entry. Deleting all zero-cost totals
+leaves a fitting matrix `B'` and the same cost.
+
+**Lemma 2 (submatrix rank).** For a line set `S` let `m(S)` be the least F2
+rank of `B[S,S]` over all fitting `B`. For `B'` from Lemma 1,
+`m(S) ≤ rank B'[S,S] ≤ #{j : c_j ≥ 1, R_j meets S, A_j meets S}`. Hence any
+weights `λ_S ≥ 0` with
+
+    Σ_S λ_S [F meets S][G meets S] ≤ c(F,G)   for all flats F, G with c(F,G) ≥ 1   (★)
+
+prove `C ≥ Σ_S λ_S m(S)`. Closure keeps `c` and can only add hits, so flats
+suffice, exactly as in PR798. Cliques (`m(Q) = |Q|`) are PR798's method.
+Asymmetric row/column sets add nothing. Define `m(P,Q)` as the least rank
+of `B[P,Q]` over fitting `B`. Every entry of `B[P,Q]` outside `(P∩Q)²` is off
+the diagonal, so it is zero or free; setting the free ones to zero gives
+`m(P,Q) = m(P∩Q)`, while the hit count for `(P,Q)` is at least that for `P∩Q`.
+
+**The new sets.** For distinct nonorthogonal `u, w`, let `S_uw = N[u] ∩ N[w]`
+(20 lines; 540 sets). `u` and `w` are nonorthogonal to every line of `S_uw`, so
+`B[S_uw,S_uw] = I_2 ⊕ B[core]` with an 18-line core, and `m(S_uw) = 2 + m(core)`.
+
+**Lemma 3 (m(core) = 8).** The core's largest clique `Q` has 5 lines. Any
+factorization `B = U V^T` with 7 columns can be normalized to
+`U[Q] = V[Q] = [I_5 | 0]` (since `U[Q] V[Q]^T = I_5`, transform by an invertible
+`M` with `U[Q] M = [I_5|0]`, then by `[[I,0],[W^T,I]]` to clear the rest of
+`V[Q]`). Then each other line `v` has `U[v] = (B[v,Q], s_v)`,
+`V[v] = (B[Q,v]^T, t_v)` with `s_v, t_v ∈ F2²`, and every remaining entry is
+`B[v,Q]·B[Q,w] + s_v·t_w`. The verifier enumerates all fixed-entry-respecting
+choices by exhaustive backtracking and finds none: no fitting completion of
+rank ≤ 7. A rank-8 completion exists and is rebuilt and rank-checked. So
+`m(S_uw) = 10`. The greedy clique bound gives only 5 + 2 = 7, and the
+chromatic (orthogonal-frame) bound gives 10: F2 cancellation does not help here.
+
+**Symmetry.** Five pinned permutations (`AUTOMORPHISMS.json`) preserve the
+nonorthogonality graph and generate a group transitive on all 540
+nonorthogonal pairs (checked by orbit closure). An automorphism maps the fitting
+pattern to itself and `S_uw` to `S_(gu)(gw)`, so the exhaustive search runs once.
+
+**Certificate.** Weights `184/6835` on each singleton, `13/13670` on each of
+the 2,880 seven-cliques and `7/20505` on each `S_uw` satisfy (★) on all
+296,321 flat pairs with positive cost (601 tight), checked in exact
+arithmetic. The objective is
+
+    40·184/6835 + 2880·7·13/13670 + 540·10·7/20505 = 30200/1367 ≈ 22.0922.
+
+Costs are integers, so **C ≥ 23**.
+
+## Why this works, and how far it goes
+
+Under PR798's optimal clique dual (1/24 on the 240 pairs of twelve-line flats
+with `c = 2`, 1/2 on full/full), a set `S` is "priced" at
+`1/2 + e/24`, where `e` counts orthogonal pairs `(x,y)` with `S` meeting both
+`x^⊥` and `y^⊥`. A set can lift the bound only if `m(S)` exceeds its price.
+`S_uw` is priced at 9.5 and has `m = 10`; the whole pattern is priced at 10.5
+with minrank 10.
+
+Exploration (not part of the replay): we enumerated the 858,299 sets
+`S = ⋂_{a∈A} N[a]` that are maximal for their hit pattern (every set has the
+same price as such a set and at most its minrank), grouped them into 78
+classes by (|A|, |S|, price), computed one minrank per class by SAT with the
+Lemma 3 normalization, and solved the class-uniform LP. Only the `S_uw` class
+violates the clique dual, and the LP optimum is again 30200/1367. If those
+classes are orbits of the graph's automorphism group (not checked), then
+30200/1367 would be the exact optimum of the whole principal-submatrix method,
+and pushing past 23 would need yet another ingredient. This is conditional.
+
+## Consequences and scope
+
+- The abstract optimum moves from [22,40] to **[23,40]**. PR1794's necessary
+  window for a beating Eisenstein supplier (C ≤ 31, ≤ 29 at the best window)
+  shrinks to 23..31. PR798's conditional Dfc three-stage window (C = 22..26)
+  becomes 23..26. Neither route is closed.
+- Same model and premises as PR798: whole K-lines, scalar binary totals, the
+  stated fitting pattern, and PR446's pairing-rank premise for any physical
+  reading. Nonlinear messages (the separate `eisenstein-message-copy-bound`
+  package) and sub-line operations are not covered.
+- This is a written proof with exhaustive finite premises, checked by a stdlib
+  replay; no proof assistant and no independent human review.
+
+## Open next questions
+
+1. **Is 30200/1367 the exact limit of principal-submatrix certificates?**
+   Why: it tells the next prover whether more set families can help. First
+   step: verify that the 78 classes are automorphism orbits (or give per-class
+   rank witnesses) and exhibit the dual. Blocker: none; about one session.
+2. **A cost-aware ingredient.** The Gaussian planar theorem
+   (`gaussian-e8-asymmetric-copy`) charges a total by how its support's rank
+   deficit relates to support size. Adapting that idea to the 12-line Eisenstein
+   hyperplanes (the tight dual pairs here) might lift the bound further. First step:
+   restrict to decompositions whose totals have K-rank-≤3 joint support.
+   Blocker: the Eisenstein planes have up to four lines, so the matching
+   argument changes.
+3. **Upper side.** No decoder cheaper than 40 is known. A SAT/ILP search over
+   non-clean supports at cost ≤ 31 would test PR1794's remaining window directly.
+
+## Credit
+
+Model, geometry, clique certificate and the method-limit theorem: Jonathan Lam
+(@jonathanlam), PR798, with PR620's archived geometry (Joel Pulikkan /
+GamingPuzzled). Weighted-clique method: Douglas R. Colkitt (PR703) and Sagar
+Thakrar (PR738). Window and prize screen: Maximooch (PR1794). The pointer to
+this target: DreamingOfClouds' note in discussion 1167. New material: Josie
+Elliston, prepared with Claude Opus 5.5 (Anthropic) via Claude Code, which did
+the search, proof and verifier. Apache-2.0.

research/eisenstein-submatrix-copy-floor/RESULT.json

@@ -0,0 +1,10 @@
+{
+  "cliques7": 2880,
+  "controls": 5,
+  "copy_floor": 23,
+  "core_rank8_witness_rank": 8,
+  "flat_pairs_with_positive_cost": 296321,
+  "objective": "30200/1367",
+  "s20_sets": 540,
+  "tight": 601
+}

research/eisenstein-submatrix-copy-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "research/eisenstein-clique-copy-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "5c5fd2f87ce3c4e61ed782ceaa623edd80811349",
+      "sha256": "b75539c196ed45f23cf238413da9684dcba503f6630ad68a9648ecacf6aada3f"
+    },
+    {
+      "path": "research/eisenstein-clique-copy-bound/geometry.py",
+      "usage": "input",
+      "git_blob": "a92c16295d6fcf2a7ffeb7d38444613f939db6cb",
+      "sha256": "248df3fb820b5165ca485ad4d43f0271043498c45a59ac1edc310a124073644c"
+    }
+  ]
+}

research/eisenstein-submatrix-copy-floor/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 3,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "In the abstract Eisenstein E8 scalar binary decoder model of research/eisenstein-clique-copy-bound (PR798; optimum known in [22,40], clique certificates provably stop at 22), do rank bounds on non-clique principal submatrices of the fitting pattern lift the copy floor above 22?",
+  "scope_change_reason": "The card's diagonal-batch line is closed by PR679 and the diagonal-child-contract audit, and its live variants are claimed by other contributors. This decoder floor is the copy-cost side of the same card ('a scoped lower bound for one alphabet'): PR1794 shows an Eisenstein supplier beats the selected record only if C <= 31, and DreamingOfClouds' discussion-1167 note names it one of the sharper open decoder targets.",
+  "bottleneck_link": "Side result on an alternative complex unit: narrows PR1794's necessary window for an Eisenstein supplier from C in 22..31 to 23..31. No supplier, kappa or selected-record change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after an exact certificate for the first integer above 22, plus a class-level exploration of whether principal-submatrix sets can go further; no decoder construction.",
+  "outcome": "completed",
+  "evidence": "verify.py (stdlib, exact): imports PR798's pinned geometry; exhaustive normalized search shows the 18-line core of S_uw = N[u] & N[w] has no fitting completion of rank <= 7 (rank-8 witness rebuilt), so minrank(S_uw) = 10 vs clique-dual price 9.5; five pinned automorphisms are transitive on the 540 nonorthogonal pairs; weights 184/6835, 13/13670, 7/20505 satisfy all 296,321 positive-cost flat-pair inequalities (601 tight); objective 30200/1367 > 22 so C >= 23; 5 rejection controls; RESULT.json pinned. Exploration (not replayed): class-uniform LP over 78 classes of hit-maximal sets also gives 30200/1367.",
+  "author": "Josie Elliston",
+  "ai_assistance": "Claude Code (Claude Opus 5.5) did the search, proof and verifier under the author's direction; one OpenAI Codex read-only review. Exploration used python-sat, networkx and scipy in a private venv; the replay is stdlib only.",
+  "open_questions": [
+    {
+      "question": "Is 30200/1367 the exact limit of principal-submatrix certificates?",
+      "why_it_matters": "Tells the next prover whether more set families can help or a new ingredient is required.",
+      "first_step": "Check that the 78 hit-maximal classes are automorphism orbits (or give per-class rank witnesses) and exhibit the matching dual.",
+      "blocked_by": "Nothing; about one session."
+    },
+    {
+      "question": "Can a cost-aware argument (like the Gaussian planar theorem) lift the bound past 23 on the 12-line Eisenstein hyperplanes?",
+      "why_it_matters": "The tight dual pairs are twelve-line hyperplane pairs; a bound >= 32 would close PR1794's window.",
+      "first_step": "Restrict to totals whose joint support has K-rank <= 3 and adapt the planar matching argument.",
+      "blocked_by": "Eisenstein planes hold up to four lines, so the matching step changes."
+    },
+    {
+      "question": "Is there any fitting decoder cheaper than 40 (non-clean supports, C <= 31)?",
+      "why_it_matters": "Tests PR1794's remaining window from the upper side.",
+      "first_step": "SAT/ILP over flat-pair rectangles with parity constraints at cost <= 31.",
+      "blocked_by": "Parity constraints make LP relaxations weak; needs a good encoding."
+    }
+  ]
+}

research/eisenstein-submatrix-copy-floor/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/eisenstein-clique-copy-bound/PROOF.md",
+    "research/eisenstein-clique-copy-bound/geometry.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "exact C >= 23 certificate: minrank(S_uw)=10 by exhaustive normalized search plus rank-8 witness; automorphism transitivity on 540 pairs; 296,321 flat-pair inequalities; objective 30200/1367; 5 rejection controls; RESULT.json equality"
+    }
+  ]
+}