Raise the all-field plane-port decoder floor from 140 to 141 (no new κ)

research/plane-port-clique-floor-141/README.md

@@ -0,0 +1,110 @@
+# Every plane-port decoder costs at least 141, over every field
+
+**Exact finite certificate for a scoped lower bound. No new κ.**
+Take the strict 112-port mask with its 56 matched planes (PR1825, PR1889) and CubeJerry's
+additive full-plane COPY tariff (#4365). Every finite rank-one decoder of this mask, over any
+coefficient field, costs at least
+
+    36732955/262144 = 140.1251...,   hence  >= 141.
+
+This raises the all-field floor of Mark (Matarener)'s
+[PR #5560](https://github.com/CrocSwap/integer-mult-bounds/pull/5560)
+(`research/plane-port-global-rank-dual`) from 140 to 141. It answers that package's Open next
+question 2 ("Can a stronger functional beat the clique programme?") with a better point of the
+same programme. It does not reach the break-even value 164 or the 224 conjecture.
+
+## What is new
+
+The proof is #5560's, unchanged. Lemma 1 says a clique `Q` of pairwise non-orthogonal planes
+carries an identity block, so at least `2|Q|` terms touch it on both sides. Lemma 2 is weak
+duality, and Lemma 3 reduces condition (F) to ordered pairs of plane-generated subspaces. Any
+nonnegative clique weights that satisfy
+
+    sum over cliques Q with a plane inside A and a plane inside R of w_Q  <=  t(A, R)
+
+for every ordered pair `(A, R)` of the 39,087 generated subspaces therefore bound every decoder
+by `sum_Q 2|Q| w_Q`. See #5560's [PROOF.md](../plane-port-global-rank-dual/PROOF.md).
+
+The new part is the weight vector. #5560's 443 columns give 139.11. This
+[CERTIFICATE.json](CERTIFICATE.json) has 425 clique columns, of sizes 1 to 24, with integer
+weights over `2^20`. Their value is 140.1251. The columns came from fresh row-and-column
+generation. The pricing step is a local search over cliques, against duals of
+the active span-pair rows. Every round separated exhaustively over all 1,527,793,569 ordered pairs.
+
+## Evidence
+
+[verify.py](verify.py) was written separately from the generator. It checks, in exact arithmetic:
+
+- the 56 planes from the pinned archive and matching, each nondegenerate, with 109 orthogonal pairs;
+- an independent closure census by reduced echelon bases: 39,087 subspaces;
+- the tariff `dim A - dim(A meet R^perp)`, compared with Gaussian elimination of the pairing
+  matrix on 4,000 random pairs;
+- every column is a clique with a positive integer weight;
+- feasibility on **all** 39,087² ordered pairs. The minimum slack is 0. It is attained exactly
+  on the 1,732 pairs with tariff 0, which no clique can touch, and every positive-tariff pair
+  has positive slack;
+- the recorded bound 36732955/262144 > 140;
+- four rejecting controls: an overweight column, an orthogonal pair as a clique, a wrong
+  recorded bound, and #5560's own certificate, which passes feasibility but stays at 139.11 < 140.
+
+Load sums stay below 2^40 and census counts are at most 512, so the floating-point matrix
+products are exact. The full run takes about 30 seconds on a 2026 Apple laptop.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and numpy 2:
+
+```sh
+python3.12 -B research/plane-port-clique-floor-141/verify.py             # full check, prints PASS_PLANE_PORT_CLIQUE_FLOOR_141
+python3.12 -B research/plane-port-clique-floor-141/verify.py --sampled   # every 97th row only
+python3.12 -B scripts/research_package.py --package research/plane-port-clique-floor-141
+```
+
+Optional regeneration, which needs scipy and is not part of the proof:
+
+```sh
+PLANE_PORT_CACHE=/tmp/ppcf python3.12 -B research/plane-port-clique-floor-141/generate/colgen.py 1 40
+PLANE_PORT_CACHE=/tmp/ppcf python3.12 -B research/plane-port-clique-floor-141/generate/roundcert.py
+```
+
+`colgen.py` starts from #5560's columns and all singletons. It stops at the first point
+certified above 140. `roundcert.py` floors the weights onto the `2^20` grid and checks them
+exactly. It writes the certificate into the cache directory. The cache holds a 1.5 GB tariff
+matrix. On macOS with CPython 3.12.15, numpy 2.5.4 (Accelerate) and scipy 1.18.1, the generator
+stopped after 14 rounds, in about 6 minutes. It reproduced this CERTIFICATE.json byte for byte.
+Other BLAS or HiGHS builds may produce a different valid certificate, and verify.py checks
+whichever certificate is present.
+
+## Not covered
+
+- The optimum of the clique programme. #5560 reports a floating-point pricing estimate of
+  about 167. This run did not price exactly, so no upper bound is certified here.
+- The conjecture that 224 holds over every field. The interval [141, 224] stays open for
+  characteristic-0 coefficients with even denominators.
+- Native realization, hosting, routing, the coverage law and concave pricing. These are
+  #4365's and #5560's caveats. No supplier, κ or selected-frontier change follows.
+
+## Open next questions
+
+1. **What is the optimum of the clique programme, and is it above 164?** A certified value
+   above 164 would close the plane-port lever in #4365's contract for every field. *First step:*
+   raise `STOP` in `generate/colgen.py` and add an exact MILP pricer, which also certifies an
+   upper bound. *Blocked by:* local-search pricing found fewer than ten new columns per round
+   near 140.
+2. **Can non-clique columns do better?** #5560's estimate of about 167 leaves little room above
+   164. *First step:* add the sharp C5 covers of `c5-residual-weighted-cover` and the three- and
+   four-plane rank duals as columns, with the same exhaustive separation. *Blocked by:* nothing.
+   One separation pass takes about 15 seconds.
+3. **Does every decoder cost at least 224 over Q?** This is #5560's conjecture. *First step:*
+   #5560 THEORY.md E2, induction on the top 2-adic valuation. *Blocked by:* there is no known
+   bound for zero-mask binary layers.
+
+## Credit
+
+The clique programme, Lemmas 1-3 and the 140 certificate are Mark (Matarener)'s
+([#5560](https://github.com/CrocSwap/integer-mult-bounds/pull/5560)). That package's own credits
+also apply. The contract and two-plane theorem are CubeJerry's (#4365). The rank-dual
+functional is pinterbanget's (#4421). The 224 bound for 2-integral decoders is Philippe Van
+Velzen's (Discussion 1587, #2532). The plane-port budgets are josie's (#1808). The labels and
+matching come from PR1825/2126 (Cinna Davis). The new certificate, generator and verifier were
+produced by Nick Petalas. Apache-2.0.

research/plane-port-clique-floor-141/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "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"
+    },
+    {
+      "path": "research/plane-port-global-rank-dual/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "512297535886e717087af5cb0ade0a747a2bb400",
+      "sha256": "20ccaf90c909c602bacc101f3dc540848c844903506e8bce70eb06f28c1ec342"
+    }
+  ]
+}

research/plane-port-clique-floor-141/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Global all-field lower bound 36732955/262144 = 140.1251 (hence 141) on the additive full-plane COPY mass of every finite scalar decoder of the strict 112-port PR1825/PR1889 mask, under CubeJerry's #4365 tariff. It is a new 425-clique feasible point of PR5560's clique programme, checked exactly on all 39,087^2 ordered span pairs. PR5560's Lemmas 1-3 are reused unchanged.",
+  "scope_change_reason": "The card asks for a legal decoder or coframe change that improves the full signed moment. This package instead raises a lower bound on one decoder family's COPY mass: it answers Open next question 2 of PR5560 (research/plane-port-global-rank-dual), the stronger clique-programme certificate. It narrows the plane-port break-even window from [140, 164] to [141, 164].",
+  "bottleneck_link": "Side result for the plane-port coverage lever (plane-port-copy-budgets). A decoder must cost at most about 160-164 per call to break even with the incumbent word. The all-field floor rises from 140 to 141, which shrinks that window by one unit. No kappa change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exact certificate above 140 (floor 141); further column generation is left as an open question.",
+  "outcome": "completed",
+  "evidence": "verify.py: independent closure census of 39,087 generated subspaces, tariffs cross-checked by Gaussian elimination on 4,000 random pairs, 425 clique columns, exact feasibility on all 1,527,793,569 ordered pairs (minimum slack 0, attained exactly on the 1,732 zero-tariff pairs), bound 36732955/262144, and four rejecting controls including PR5560's own certificate (139.11 < 140). generate/ holds the row-and-column generation and rounding code (scipy HiGHS); it is not needed for the proof.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the optimum of the full clique programme, and does it exceed 164?",
+      "why_it_matters": "A certified value above 164 would close the plane-port lever for every coefficient field in #4365's contract without settling the 224 conjecture.",
+      "first_step": "Continue generate/colgen.py past the 140 stop (raise STOP), and replace the local-search pricing with an exact MILP pricer to obtain a certified upper bound on the programme.",
+      "blocked_by": "Local-search pricing slowed to fewer than ten new columns per round near 140; no exact pricing bound is available yet."
+    },
+    {
+      "question": "Can columns other than cliques (C5 covers, three- and four-plane rank duals) beat the clique programme's optimum?",
+      "why_it_matters": "PR5560 estimates the clique programme at about 167, which leaves little headroom above 164.",
+      "first_step": "Add the sharp C5 covers of c5-residual-weighted-cover as columns, with the same exhaustive span-pair separation used by verify.py.",
+      "blocked_by": "Nothing; the separation step takes about 15 seconds on one machine."
+    },
+    {
+      "question": "Does every decoder cost at least 224 over Q?",
+      "why_it_matters": "This is PR5560's conjecture, and it would close the lever for every field.",
+      "first_step": "PR5560 THEORY.md E2: induct on the top 2-adic valuation.",
+      "blocked_by": "No known lower bound for zero-mask binary layers."
+    }
+  ]
+}

research/plane-port-clique-floor-141/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [
+    "numpy==2.2.6"
+  ],
+  "inputs": [
+    "research/community-frontier1094-audit/selected-replay.tar.gz",
+    "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json",
+    "research/plane-port-global-rank-dual/CERTIFICATE.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 400,
+      "checks": "independent closure census (39,087 spans), tariff vs Gaussian elimination on 4,000 pairs, clique columns, exact feasibility on all 39,087^2 ordered pairs, bound 36732955/262144 > 140, four rejecting controls"
+    }
+  ]
+}