Prove a global all-field COPY floor 140 for the 56-plane port decoder (no new κ)

research/plane-port-global-rank-dual/EVIDENCE.md

@@ -0,0 +1,50 @@
+# Search evidence for the 224 conjecture
+
+**Heuristic numerical search, not a proof.** Script: [search/real_escape.py](search/real_escape.py).
+Raw result lines: [search/results/](search/results/).
+
+## Method
+
+For a group `D` of planes, every term slot has fixed plane supports `(A, R)` with `A, R` subsets of
+`D` (for 5-7 planes only sides of 1-2 planes, the whole group and all-but-one). The objective is
+the mask residual on fixed cells plus `lam * sum_k t(A_k, R_k) |u_k| |v_k|`, minimised by L-BFGS
+with `lam` raised in steps. Survivors are pruned by weight and refitted exactly by least squares.
+Whenever the refit is exact (max residual below `1e-9`), the run records the **true** cost: the
+sum of tariffs of the actual nonzero supports. The mask is the strict one: free entries between
+orthogonal planes. A decomposition of the identity endpoint is also a strict-mask decoder, so
+"no escape" here also covers the identity endpoint used by the three- and four-plane rank duals.
+
+Real solutions include every rational one, so a real minimum of `4|D|` excludes all denominators on
+that group. The search is local optimisation from random starts and can miss a cheaper decoder.
+Where it stops above the baseline, it did not even reach the known decoder, so that line is
+weak evidence.
+
+## Results
+
+No run found an exact decoder below `4|D|`.
+
+| Groups | Starts | Reached baseline | Above baseline | Below baseline |
+|---|---:|---:|---:|---:|
+| 6 open triple classes of `three-plane-rank-dual` | 40 | 6 | 0 | 0 |
+| 40 random open quadruples of `four-plane-rank-dual` | 30 | 30 | 10 | 0 |
+| 60 most degenerate quadruples (3 of them open) | 30 | 44 | 16 | 0 |
+| 23 induced C5s | 15 | 6 | 17 | 0 |
+| C5 + 1 most degenerate plane (23) | 15 | 5 | 18 | 0 |
+| C5 + 2 most degenerate planes (23) | 15 | 3 | 20 | 0 |
+
+The baselines are 12, 16, 20, 24 and 28. On quadruples the solver usually reaches 16. On 5-7 plane
+groups it often stops 2-10 above, so those rows say little beyond "nothing cheap was found".
+
+The open quadruples were sampled with `random.Random(2026).sample` from the 5,584 index-zero
+quadruples of `four-plane-rank-dual/CERT-INDEX.bin.gz`. The open triple classes are the six classes
+of `three-plane-rank-dual/CERTIFICATES.json` that carry an `f2_minimum_mass` field; one example
+triple per class is searched.
+
+## Provenance
+
+The 60 degenerate quadruples and the C5 groups ran on Kaggle with the same search core from the
+fork branch `Matarener/integer-mult-bounds:v4-plane-lb`. The C5 run stopped after 49 of 69
+groups on an `SVD did not converge` error inside a refit; the refit now skips such a prefix, and the
+remaining 20 groups ran separately. The `quads-degenerate` and `c5` modes of `real_escape.py`
+reproduce the same group lists. The open-quadruple run used `real_escape.py` from this package on
+Kaggle; the open-triple run used it locally.

research/plane-port-global-rank-dual/FULL-CHECK.json

@@ -0,0 +1,14 @@
+{
+ "schema": "plane-port-global-rank-dual/verify/1",
+ "planes": 56,
+ "generated_subspaces": 39087,
+ "ordered_pairs_checked": 1527793569,
+ "complete": true,
+ "columns": 443,
+ "scale": 1048576,
+ "min_slack": 0,
+ "tight_pairs": 1732,
+ "lower_bound": "18233853/131072",
+ "lower_bound_float": 139.1132583618164,
+ "new_kappa_claimed": false
+}

research/plane-port-global-rank-dual/PROOF.md

@@ -0,0 +1,94 @@
+# Proof of the global bound
+
+## Object
+
+The 112 selected ports carry binary labels `q_p` in `F_2^9`. The retained PR1825 matching
+(`research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json`) pairs them into 56 planes
+`E_i = span(q_a, q_b)`. Every plane is nondegenerate: its 2 x 2 Gram matrix over `F_2` has rank 2.
+Two planes are *orthogonal* when every vector of one is orthogonal to every vector of the other;
+109 of the 1,540 plane pairs are orthogonal.
+
+A **decoder** over a field `F` is a finite family of rank-one terms `u_k v_k^T` with
+`u_k, v_k in F^112` and `M = sum_k u_k v_k^T`, satisfying the strict scalar mask of PR1889:
+
+- `M_pp = 1` for every port;
+- `M_pq = 0` when `p != q` and the planes of `p` and `q` are equal or non-orthogonal;
+- `M_pq` is free when the planes of `p` and `q` are orthogonal.
+
+`F` is arbitrary: `Q` with any denominators (in particular even ones), `R`, `C`, or a finite field.
+
+**Tariff** (the contract of #4365, unchanged). Let `A_k` and `R_k` be the sets of planes that contain a
+port where `u_k`, respectively `v_k`, is nonzero, and `W(X) = span(E_i : i in X)`. The term costs
+
+    t_k = rank over F_2 of the dot-product pairing between W(A_k) and W(R_k)
+        = dim W(A_k) - dim(W(A_k) meet W(R_k)^perp).
+
+It depends only on the plane supports. Charges add: the decoder costs `sum_k t_k`.
+
+## Theorem
+
+For every field `F` and every decoder,
+
+    sum_k t_k  >=  18233853 / 131072  =  139.1132...,
+
+hence `sum_k t_k >= 140`, because the cost is an integer.
+
+## Proof
+
+A **clique** is a set `Q` of pairwise non-orthogonal planes. Write `P(Q)` for its `2|Q|` ports.
+
+**Lemma 1 (identity block).** For every clique `Q`, at least `2|Q|` terms touch `Q` on both sides,
+that is, have `A_k` meeting `Q` and `R_k` meeting `Q`.
+
+*Proof.* Every pair of distinct ports in `P(Q)` lies in one plane or in two non-orthogonal planes, so
+the mask fixes `M` restricted to `P(Q)` to the identity `I_{2|Q|}`. A term that misses `P(Q)` on
+one side restricts to zero there. Hence `I_{2|Q|}` is a sum of the restrictions of the touching
+terms, each of rank at most one, and their number is at least `2|Q|`. This holds over every field.
+Lean: `V4.identity_block_needs_terms` in [lean/V4Duality.lean](lean/V4Duality.lean). Its hypothesis
+is the identity block on a port set `S`; its conclusion counts the terms nonzero on `S` on both
+sides.
+
+**Lemma 2 (weak duality).** Let `w_Q >= 0` be weights on cliques such that every term satisfies
+
+    sum over cliques Q touched by term k on both sides of w_Q  <=  t_k.            (F)
+
+Then `sum_Q w_Q * 2|Q| <= sum_k t_k`.
+
+*Proof.* Swap the order of summation and use Lemma 1. Lean: `V4.weak_duality`.
+
+**Lemma 3 (finite check).** Condition (F) holds for every possible term if, for every ordered pair
+`(A, R)` of subspaces generated by nonempty plane sets,
+
+    sum over cliques Q with  in(A) meets Q  and  in(R) meets Q  of w_Q  <=  t(A, R),       (F')
+
+where `in(A)` is the set of planes contained in `A`.
+
+*Proof.* For a term with nonempty supports put `A = W(A_k)`, `R = W(R_k)`. Then `A_k` is contained in
+`in(A)`, so every clique touched by the term is counted in (F'), and `t_k = t(A, R)`. A term with an
+empty side costs 0 and touches no clique.
+
+**The certificate.** [CERTIFICATE.json](CERTIFICATE.json) lists 443 cliques, of sizes up to 24,
+with integer weights `w_Q / 2^20`. [verify.py](verify.py) recomputes the planes from the pinned
+archive and matching, enumerates all 39,087 subspaces generated by plane sets, computes their
+tariffs, checks that every column is a clique and checks (F') on all `39,087^2 = 1,527,793,569`
+ordered pairs in exact integer arithmetic. The minimum slack is 0, attained on 1,732 pairs. The
+bound is `sum_Q w_Q 2|Q| / 2^20 = 18233853/131072`.
+
+Lemmas 1-3 and the certificate give the theorem.
+
+## Where the certificate came from
+
+The weights are a rounded-down optimal dual of a clique linear programme solved by column
+generation (separation over all ordered span pairs, on Kaggle). Only the rounded certificate
+matters for the proof. We do not know the optimum of the full clique programme. A floating-point
+pricing estimate from the same run suggests it is at most about 167; that estimate is not
+certified here.
+
+## What the proof does not use
+
+- No coefficient restriction: no integrality, no parity, no bound on denominators or term counts.
+- No symmetry `u_k = v_k` and no positivity.
+- Free mask entries are never used; only identity blocks on cliques.
+
+It also leaves out everything outside the #4365 contract: native realization, hosting, routing and
+any non-additive or concave pricing.

research/plane-port-global-rank-dual/README.md

@@ -0,0 +1,120 @@
+# Every plane-port decoder costs at least 140, over every field
+
+**Scoped proof with an exact finite certificate and two Lean-checked lemmas. No new κ.**
+For the selected 112 ports matched into 56 planes (PR1825) and the strict scalar mask (PR1889),
+every finite rank-one decoder, over **any** coefficient field, has additive full-plane COPY mass
+
+    sum of tariffs  >=  18233853/131072 = 139.113...,   hence  >= 140.
+
+This is the first global bound for the whole 56-plane decoder that holds for arbitrary rational
+coefficients, in particular with even denominators. Before it, the only all-field global bound was
+the fitting rank 49. The value 224 is proved only for 2-integral coefficients and characteristic 2
+(Philippe Van Velzen), and for decoders split into disjoint plane pairs (#4365).
+
+The package also states the **conjecture that 224 holds over every field**, gives the structural
+conditions an escape below 224 would have to meet, and reports a numerical search over real
+coefficients on the open local cases left by the three- and four-plane rank duals. That search
+found no escape. It is evidence, not proof.
+
+## Contract
+
+Unchanged from CubeJerry's #4365, as used by `three-plane-rank-dual` and `four-plane-rank-dual`:
+a term `u vᵀ` costs the binary pairing rank between the spans of the complete planes touched by
+`u` and by `v`; charges add; coefficients lie in any field. The endpoint here is the full strict
+112-port mask: unit diagonal, zeros inside planes and between non-orthogonal planes, free entries
+between orthogonal planes. [PROOF.md](PROOF.md) states it precisely.
+
+## Why it matters
+
+`plane-port-copy-budgets` (josie) prices the plane-port lever: a decoder must cost at most about
+160-164 per call just to match the incumbent word, and the lever map in Discussion 2278 needs about
+128 for doubling κ. The bound 140 excludes the doubling target for every coefficient field inside
+this contract. The break-even window `[140, 164]` stays open, and only for characteristic-0
+coefficients with essential even denominators ([THEORY.md](THEORY.md), E1).
+
+## Proof in one paragraph
+
+On a clique `Q` of pairwise non-orthogonal planes the mask is the identity on `2|Q|` ports, so at
+least `2|Q|` terms touch `Q` on both sides, over every field. Weights `w_Q >= 0` with
+`sum_{Q touched by a term} w_Q <= tariff` for every possible term then give
+`total tariff >= sum_Q 2|Q| w_Q` by weak duality. Tariffs depend only on the generated spans, so
+the feasibility condition is a finite check over all 39,087² ordered pairs of plane-generated
+subspaces. [CERTIFICATE.json](CERTIFICATE.json) gives 443 cliques with integer weights `/2^20`.
+The two abstract lemmas are kernel-checked in Lean ([lean/](lean/)); the finite check is
+[verify.py](verify.py).
+
+## Evidence for the conjecture
+
+[EVIDENCE.md](EVIDENCE.md) has the tables. In short, a sparse real-coefficient search with exact
+refits found no local decoder below 4 per plane on:
+
+- all 6 open triple classes of `three-plane-rank-dual` (the classes with no all-field certificate);
+- 40 random open quadruples of `four-plane-rank-dual`, plus 3 more open ones met by chance;
+- the 60 most degenerate quadruples;
+- 69 groups built from the 23 induced 5-cycles and their 6- and 7-plane extensions.
+
+A real solution space contains every rational one, so a real minimum of `4|S|` excludes every
+denominator. The search is local optimization from random starts, and on 5-7 plane groups it often
+stops above the baseline, so these runs are weak evidence there.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and numpy 2:
+
+```sh
+python3 -B research/plane-port-global-rank-dual/verify.py          # bounded: every 97th row, ~1 min
+python3 -B research/plane-port-global-rank-dual/verify.py --full   # all 1.53e9 pairs, ~7 min
+bash research/plane-port-global-rank-dual/lean/check.sh            # Lean v4.21.0 + Mathlib cache
+```
+
+The bounded run checks the census, 20,000 tariffs against Gaussian elimination, every clique and
+weight, the bound, three rejecting controls, and feasibility on 403 of 39,087 rows. The full run
+writes [FULL-CHECK.json](FULL-CHECK.json): all 1,527,793,569 ordered pairs, minimum slack 0 on
+1,732 tight pairs. The searches need scipy:
+
+```sh
+python3 research/plane-port-global-rank-dual/search/real_escape.py triples-open 40
+python3 research/plane-port-global-rank-dual/search/real_escape.py quads-open 40 30 2026
+python3 research/plane-port-global-rank-dual/search/real_escape.py quads-degenerate 60 30
+python3 research/plane-port-global-rank-dual/search/real_escape.py c5 15
+```
+
+## Not covered
+
+- The conjecture itself: no bound between 140 and 224 is proved for characteristic 0.
+- The optimum of the full clique programme. A floating-point column-generation estimate suggests it
+  is at most about 167, so this method alone may not reach 164; that estimate is not certified.
+- Native realization, hosting, routing and the coverage law, which are #4365's caveats.
+- Non-additive or concave pricing.
+
+## Open next questions
+
+1. **Does every decoder cost at least 224 over Q?**
+   - *Why it matters:* it would close the plane-port lever for every coefficient field.
+   - *First step:* turn the 2-adic layering of THEORY.md E2 into an induction on the top valuation,
+     bounding what a zero-mask binary layer can save on the integral layer.
+   - *Blocked by:* no known lower bound for zero-mask layers.
+2. **Can a stronger functional beat the clique programme?**
+   - *Why it matters:* `[140, 164]` is the break-even window; a certified value above 164 would close
+     the lever in this contract without settling the conjecture.
+   - *First step:* add the sharp C5 covers of `c5-residual-weighted-cover` and the four-plane
+     certificates as columns, with the same exhaustive span-pair separation.
+   - *Blocked by:* nothing; the column-generation code is in the fork branch named in TASK.json.
+3. **Is there an exact rational escape on an open four-plane class?**
+   - *Why it matters:* a cost-15 decoder would be the first mixing gain under #4365's contract.
+   - *First step:* exact search with forced half coefficients (THEORY.md E1) on the lowest LP class
+     of `four-plane-rank-dual`.
+   - *Blocked by:* nothing.
+
+## Credit
+
+The contract and the two-plane theorem are CubeJerry's (#4365). The rank-dual functional
+`sum_X w_X rank(M_XX)` is pinterbanget's (Ryanson Jonathan: #4421 and the four-plane extension);
+this package applies it to cliques of the whole 112-port mask. The 224 bound for 2-integral decoders is
+Philippe Van Velzen's (Discussion 1587, #2532). The fitting rank 49 is from PR2471 (ywz65) and
+PR2484 (Sagar Thakrar). The C5 results are Tekalign's, Sagar Thakrar's and Nick Petalas's.
+The plane-port budgets are josie's. Labels and matching come from PR1825/2126 (Cinna Davis).
+
+Prepared by Mark (Matarener) with substantial Claude Code assistance in derivation, code, Lean and
+writing. The verifier was written separately from the code that generated the certificate, in the
+same AI-assisted project. No independent human review is claimed. Apache-2.0.

research/plane-port-global-rank-dual/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/community-frontier1094-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f",
+      "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6"
+    },
+    {
+      "path": "research/four-plane-rank-dual/CERT-INDEX.bin.gz",
+      "usage": "input",
+      "git_blob": "7c525e1ed8af5069c8bb28cac9fefe40406a9261",
+      "sha256": "b66ba05b1b37a1be42c85ce855eca387a822df9d0b5d93a2d46d8c46d84ad7b1"
+    },
+    {
+      "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6",
+      "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1"
+    },
+    {
+      "path": "research/three-plane-rank-dual/CERTIFICATES.json",
+      "usage": "input",
+      "git_blob": "43087b96986d9e770807d090f2286a6e2135df4a",
+      "sha256": "f343036b3788969a690c87e6cdded90b2351d90caa5340c8b813e2240ffb0438"
+    }
+  ]
+}