Extend the rank dual to four planes: COPY floor 16 over every field on 361,706 of 367,290 plane quadruples; 5,584 open (no new κ)

research/four-plane-rank-dual/README.md

@@ -0,0 +1,103 @@
+# Four-plane COPY floor: exact certificates for 98.5% of plane quadruples
+
+**Claim type:** exact lower-bound certificates, checked by a standard-library verifier, plus a
+documented open remainder. **No new κ.** This extends CubeJerry's
+[#4365](https://github.com/CrocSwap/integer-mult-bounds/pull/4365), which closed two-plane
+mixing, and my [#4421](https://github.com/CrocSwap/integer-mult-bounds/pull/4421), which closed
+three-plane mixing on all 27,720 triples, to four planes. The contract is #4365's unchanged:
+
+- whole-plane closures;
+- `F₂`-rank tariffs `t(S, T)`;
+- additive charges;
+- payload in any field.
+
+## Result
+
+For **361,706 of the 367,290 plane quadruples (98.48%)**, every decomposition of `I₈` costs at
+least **16 = Σ p_i²**, over every field. This is exactly the cost of separate coordinate messages,
+so on those quadruples four-plane mixing cannot lower the COPY mass. **5,584 quadruples, in 3,650
+tariff classes, remain open.**
+
+## Certificates
+
+The functionals are those of #4421, extended to four planes:
+
+    L(M) = Σ_{(Z, X)} w · rank(Φ_Z(M)_XX).
+
+- `X` ranges over the 15 plane unions.
+- `Φ_Z` zeroes a set `Z` of the 12 off-diagonal plane blocks. `Z = ∅` gives #4365's block-rank
+  functional.
+- **Subadditivity.** `rank` of a linear image is subadditive.
+- **Atom bound.** `Φ_Z(u vᵀ)_XX` is a sum over touched row planes of `u_P(Σ_allowed v_Q)ᵀ`. So its
+  rank is at most the number of distinct allowed column (or row) plane sets, a combinatorial bound
+  valid over every field.
+- **The test.** If `Σ w·bound(S, T, X, Z) ≤ t(S, T)` for all 225 closure pairs, every decomposition
+  costs at least `L(I₈) = Σ w·2|X|`. This holds because `Φ_Z` never touches the diagonal blocks.
+
+Coverage:
+
+| Certificate | Classes | Quadruples |
+| --- | --- | --- |
+| block-rank (`Z = ∅`) | 195,523 | the bulk |
+| zeroed-block and mixed (several `Z`) | 24,732 | |
+| **total certified** | **220,255 of 223,905** | **361,706 of 367,290** |
+
+All certificates have value exactly 16, and there are 9,330 distinct ones. `verify.py`
+recomputes all 367,290 quadruples' tariffs from the pinned selected archive and matching
+certificate, the same pins as #4365 and #4421. It reads one certificate index per quadruple from
+`CERT-INDEX.bin.gz` and checks every certificate exactly, with integer-scaled weights against an
+exact bound table that it builds itself.
+
+## The open remainder
+
+On the 3,650 open classes, the best LP value over all `4096 × 15` zero-set and union pairs ranges
+from 12.571 to just under 16. Most values are 15.33, 15.5, 15.0 or 15.6. These classes typically
+combine two kinds of cheap atom:
+
+- one free plane pair: binary cross rank 0, so messages between the two planes cost 0;
+- a cheap full closure: joint Gram rank 5–7 instead of 8, so a message touching all four planes
+  costs less than 8.
+
+The LP's fractional covering leans on the free cross atoms. As in the three-plane case, a real
+decomposition must cancel them, and these functionals cannot see the cancellation. For the
+triples, one more family (mixed `Z`) closed the gap. For quadruples, the families here, including
+off-principal blocks `rank(Φ_Z(M)_{X,Y})` tested on three open classes, do not. These quadruples
+are **undecided**, not counterexamples. Two direct tests on one of them were also inconclusive:
+
+- an exact `F₂` ILP over 65,025 binary atoms for mass ≤ 15 hit its 900 s limit;
+- a short real-coefficient search found nothing.
+
+## Not covered
+
+- The ℚ/ℂ minimum on the 5,584 open quadruples.
+- Decoders over five or more planes.
+- Native realization, coverage and hosting, which are #4365's caveats.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/four-plane-rank-dual --check-only
+python3.12 -B scripts/research_package.py --package research/four-plane-rank-dual
+```
+
+The verifier prints `PASS_FOUR_PLANE_RANK_DUAL` in about 4.5 minutes, using only the standard
+library. `generation/` holds the scipy scripts that produced the certificates; verification does
+not need them.
+
+## Open next questions
+
+1. **Is the four-plane mass below 16 over ℂ on the open classes?**
+   - *Why it matters:* a mass below 16 would be the first mixing gain under #4365's contract.
+   - *First step:* a cancellation-aware functional for a free plane pair combined with a cheap full
+     closure. Alternatively, an exact `F₃` or `F₂` search on the lowest class (LP 12.571).
+   - *Blocked by:* nothing.
+
+## Credit
+
+- The contract and the two-plane theorem are CubeJerry's (#4365).
+- The labels and matching come from PR1825/2126 (Cinna Davis) and the retained matching
+  certificate.
+- Gonzalo Mier's PR3990/3997 are predecessors.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/four-plane-rank-dual/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/community-frontier1094-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f",
+      "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6"
+    },
+    {
+      "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6",
+      "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1"
+    }
+  ]
+}

research/four-plane-rank-dual/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 7,
+  "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/heterogeneous-owner-assembly/README.md",
+      "certificates/selected-result.json",
+      "research/selected-k8-unrestricted-ends/README.md"
+    ],
+    "methods": [
+      "Propose a changed helper inventory and derive an optimistic exact moment.",
+      "Design a small completed instance and independently verify its endpoint and rank bill."
+    ],
+    "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "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.",
+    "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.",
+    "allowed_variations": [
+      "Narrow to one changed boundary or helper type with explicit counts.",
+      "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": [
+      "Mixing only providers already inside the pinned catalogue.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "helper inventory",
+      "heterogeneous-owner",
+      "mutable leaver"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Extend #4365/#4421's rank dual to plane quadruples: exact all-field certificates of the four-plane COPY floor 16.",
+  "scope_change_reason": "#4421 closed three-plane mixing; its open question 1 is four planes.",
+  "bottleneck_link": "Local decoders that mix planes could only help if they lower COPY mass below separate messages.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop at the zero-set certificate families; report the remainder as open.",
+  "outcome": "completed",
+  "evidence": "verify.py: 361,706 of 367,290 quadruples (220,255 of 223,905 tariff classes) certified at floor 16 over every field with 9,330 exact certificates; 5,584 quadruples open with LP values 12.571..15.9.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Is the four-plane COPY mass below 16 over C on the 3,650 open classes?",
+      "why_it_matters": "It would be the first mixing gain under #4365's contract.",
+      "first_step": "A cancellation-aware functional for free pairs with cheap full closures, or an exact F3/F2 search on the lowest class.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/four-plane-rank-dual/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/community-frontier1094-audit/selected-replay.tar.gz",
+    "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Pinned archive and matching; tariffs of all 367,290 plane quadruples recomputed; 9,330 distinct certificates of value 16 checked exactly (integer-scaled weights, self-built zeroed-block bound table) on every referenced class; 361,706 quadruples certified, 5,584 reported open."
+    }
+  ]
+}

research/four-plane-rank-dual/diagnostics/LOWEST-CLASS.md

@@ -0,0 +1,50 @@
+# Diagnostic: the lowest open quadruple class (LP 12.571)
+
+This is local, exploratory evidence. It is not part of the registered verifier and is not a theorem.
+
+## The class
+
+The example quadruple is planes `(7, 8, 15, 52)`. Its single-plane cross tariffs are
+
+- `A–B` and `C–D`: 0, so messages between those planes are free;
+- every other cross pair: 2, with each such plane pair's joint Gram of rank 2 ("aligned").
+
+The full closure costs 8. The best zeroed-block LP value is 88/7 = 12.571.
+
+## Why the zeroed-block family stops short here
+
+Take `Z = {AB, BA, CD, DC}`. The candidate `L(M) = 2·rank(Φ_Z(M))` has `L(I) = 16` and satisfies 221 of
+the 225 atom inequalities. It fails only on `(ABC, ABD)`, `(ABD, ABC)`, `(ACD, BCD)` and
+`(BCD, ACD)`, which each cost 4. On `(ABC, ABD)` the image `Φ_Z(u vᵀ)` has row vectors
+
+    w_A = (v_A, 0, v_D),   w_B = (0, v_B, v_D),   w_C = (v_A, v_B, 0),
+
+with `w_A + w_B − w_C = (0, 0, 2v_D)`. This is rank 2 in characteristic 2, where the functional
+would give `L ≤ 4`, but generically rank 3 in characteristic 0, where `L = 6 > 4`. So the obstruction
+to certifying 16 is characteristic-dependent. The combinatorial atom bound cannot see that
+difference.
+
+## A border decomposition at mass 14 over ℝ
+
+The LP's fractional covering suggested the patterns. `lowreal.py` searches small multisets of those
+patterns plus free atoms with alternating least squares. The best mass-14 multiset is
+`AC×AC, AD×AD, 2·BD×BD, BCD×ACD, AB×CD` plus two of each free atom. `border.py` tracks it:
+
+| ALS iteration | `‖Σ u vᵀ − I‖` | `max ‖u‖‖v‖` |
+| --- | --- | --- |
+| 100 | 2.44e-1 | 2.5e3 |
+| 1,000 | 7.41e-2 | 2.9e5 |
+| 3,000 | 4.26e-2 | 2.7e6 |
+| 10,000 | 2.33e-2 | 3.0e7 |
+| 20,000 | 1.65e-2 | 1.2e8 |
+
+The residual tends to 0 only as the coefficients diverge. That is the signature of a border
+decomposition (border rank), not an exact one. No exact decomposition below 16 was found. An exact
+`F₂` ILP, over 65,025 atoms with mass at most 15, timed out at 1,500 s.
+
+## Reading
+
+Over ℝ and ℂ, mass 14 is approached but apparently not attained. A finite-precision decoder cannot
+use diverging coefficients, so this is consistent with the open floor being 16, and it explains why
+the zeroed-block LP falls below 16. Proving 16 needs a characteristic-0 argument that uses
+cancellation, for example the closedness of the set of exact mass-14 decompositions.

research/four-plane-rank-dual/diagnostics/border.py

@@ -0,0 +1,26 @@
+import numpy as np
+exec(open('lowreal.py').read().split("cap=int(sys.argv[1])")[0])
+mult=(1, 0, 1, 2, 0, 0, 1, 1, 0, 0)
+pats=[p for p,k in zip(paid,mult) for _ in range(k)]+[f for f in free for _ in range(2)]
+n=len(pats); I=np.eye(8); rng=np.random.default_rng(11)
+bestrun=None
+for rs in range(60):
+    Uv=[np.zeros(8) for _ in pats]; Vv=[np.zeros(8) for _ in pats]
+    for j,(S,Tt) in enumerate(pats):
+        Uv[j][coords(S)]=rng.standard_normal(len(coords(S))); Vv[j][coords(Tt)]=rng.standard_normal(len(coords(Tt)))
+    hist=[]
+    for it in range(20000):
+        for side in (0,1):
+            src=Vv if side==0 else Uv; dst=Uv if side==0 else Vv
+            for r in range(8):
+                js=[j for j,(S,Tt) in enumerate(pats) if r in coords(S if side==0 else Tt)]
+                M=np.array([src[j] for j in js]).T
+                x,*_=np.linalg.lstsq(M, I[r,:] if side==0 else I[:,r], rcond=None)
+                for j,xx in zip(js,x): dst[j][r]=xx
+        if it in (100,1000,3000,10000,19999):
+            res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I)
+            mx=max(np.linalg.norm(Uv[j])*np.linalg.norm(Vv[j]) for j in range(n))
+            hist.append((it,res,mx))
+    if bestrun is None or hist[-1][1]<bestrun[-1][1]: bestrun=hist
+    if hist[-1][1]<1e-9: break
+for h in bestrun: print('iter %6d residual %.3e max|u||v| %.3e'%h)

research/four-plane-rank-dual/diagnostics/lowreal.py

@@ -0,0 +1,46 @@
+import itertools, numpy as np, pickle, sys, time
+A,B,C,D=1,2,4,8
+paid=[((A|C),(A|C)),((B|C),(B|C)),((A|D),(A|D)),((B|D),(B|D)),((C|D),(A|B)),((A|B|D),(A|B|C)),((B|C|D),(A|C|D)),((A|B),(C|D)),((A|B|C),(A|B|D)),((A|C|D),(B|C|D))]
+cost=[2,2,2,2,2,4,4,2,4,4]
+free=[(A,B),(B,A),(C,D),(D,C)]
+coords=lambda S:[2*k+i for k in range(4) if S>>k&1 for i in range(2)]
+rng=np.random.default_rng(3)
+def als(pats,restarts=30,iters=600):
+    n=len(pats); I=np.eye(8); best=9
+    for _ in range(restarts):
+        Uv=[np.zeros(8) for _ in pats]; Vv=[np.zeros(8) for _ in pats]
+        for j,(S,Tt) in enumerate(pats):
+            Uv[j][coords(S)]=rng.standard_normal(len(coords(S))); Vv[j][coords(Tt)]=rng.standard_normal(len(coords(Tt)))
+        for it in range(iters):
+            for side in (0,1):
+                src=Vv if side==0 else Uv; dst=Uv if side==0 else Vv
+                for r in range(8):
+                    js=[j for j,(S,Tt) in enumerate(pats) if r in coords(S if side==0 else Tt)]
+                    if not js: continue
+                    M=np.array([src[j] for j in js]).T
+                    x,*_=np.linalg.lstsq(M, I[r,:] if side==0 else I[:,r], rcond=None)
+                    for j,xx in zip(js,x): dst[j][r]=xx
+            if it%50==49:
+                res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I)
+                if res<1e-10: return res,(Uv,Vv)
+        res=np.linalg.norm(sum(np.outer(Uv[j],Vv[j]) for j in range(n))-I); best=min(best,res)
+    return best,None
+cap=int(sys.argv[1]); t=time.time(); tried=0; best=9
+for mult in itertools.product(range(3),repeat=len(paid)):
+    m=sum(c*k for c,k in zip(cost,mult))
+    if m>cap or sum(mult)<4: continue
+    pats=[p for p,k in zip(paid,mult) for _ in range(k)]+[f for f in free for _ in range(2)]
+    # necessary: every diagonal plane block reachable by >=2 paid terms (free atoms never touch diagonal blocks)
+    if any(sum(1 for S,Tt in pats[:sum(mult)] if S&P and Tt&P)<2 for P in (A,B,C,D)): continue
+    tried+=1
+    r,sol=als(pats,restarts=6,iters=300)
+    if r<best: best=r; bestmult=mult
+    if r<1e-8:
+        print('FOUND mass',m,'mult',mult,flush=True); pickle.dump((pats,sol),open('lowreal_found.pkl','wb')); break
+    if tried%20==0: print('tried',tried,'best',round(best,5),round(time.time()-t),flush=True)
+print('end tried',tried,'best',best,flush=True)
+print('bestmult',bestmult,flush=True)
+pats=[p for p,k in zip(paid,bestmult) for _ in range(k)]+[f for f in free for _ in range(2)]
+r,sol=als(pats,restarts=200,iters=3000)
+print('hard re-solve residual',r,flush=True)
+if sol: pickle.dump((pats,sol),open('lowreal_found.pkl','wb'))

research/four-plane-rank-dual/generation/NOTES.md

@@ -0,0 +1,16 @@
+# Generation scripts (not needed for verification)
+
+These scripts produced `CERTIFICATES.json.gz` and `CERT-INDEX.bin.gz`. They need numpy 1.26 and
+scipy 1.13, and were run from a scratch directory containing a repository checkout at `imb/`.
+
+1. `quad.py` computes the tariff classes of all quadruples (`quad_classes.pkl`). It then screens
+   them with the block-rank LP and writes `quad_weak.pkl`.
+2. `phitable.py` builds the zeroed-block bound table, `phitab4.npy`.
+3. `quad3.py <chunk> 12` solves the zeroed-block and mixed LPs for the weak classes, first over
+   subsets of the cheap cross pairs and then over all 4096 zero sets.
+4. `fastcheck.py` holds the exact checker shared with `verify.py`.
+5. `gen_quad.py` rationalizes every certificate, checks it exactly, deduplicates, and writes the
+   two artifacts.
+
+`verify.py` re-derives the tariffs and the bound table itself, and trusts nothing produced here
+beyond the certificate data, which it checks exactly.