Prove the sharp P112 exceptional-hull two-call COPY floor

research/p112-exceptional-hull-floor/PROOF.md

@@ -0,0 +1,132 @@
+# Exceptional-hull cross forms keep the P112 two-call floor
+
+## Statement and inherited model
+
+Use the arbitrary directed cross-form model of Sagar Thakrar's PR2294,
+with the support theorem and incidence count stated in commdata2338's
+[PR2395 proof](../p112-cross-form-rank-tradeoff/PROOF.md). These results are
+premises, not new results of this package.
+
+The reader and source label spaces are both F2^9, with the ordinary dot
+product as the within-call pairing. Every nonzero P112 root-code coefficient
+vector has label span F2^9 or one of eight coordinate-support hyperplanes.
+Write the reader hyperplanes as U_a = r_a^perp and the source hyperplanes
+as V_b = s_b^perp. Their pairings have rank eight. Equivalently,
+
+    r_a dot s_b = 1 for every a,b in {0,...,7}.                 (1)
+
+Let S = span_F2{s_0,...,s_7}. Take any nonzero binary vector v, any
+i in {0,...,7}, and independent directed cross forms
+
+    beta01 = r_i v^T,
+    beta10 = C, with every row of C in S.                      (2)
+
+**Theorem.** Every exact two-call root-code factorization in this model
+has total union COPY-rank price at least 128. The minimum is exactly 128.
+There is no restriction on the number of terms or their complex scalars.
+The reverse form C may have rank greater than one.
+
+## New transfer step
+
+Take any double term, meaning that both reader blocks and both source
+blocks are nonzero. Restrict its four support spans to coordinate
+hyperplanes U_a,V_b,U_c,V_d. This is possible by the inherited support
+theorem. Restricting a matrix cannot increase its rank.
+
+The within-call pairing on U_a x V_b is nonsingular. The vector in V_b
+representing the functional x -> x dot r_i on U_a is
+
+    z = r_i + (r_i dot s_b) r_a = r_i + r_a.                   (3)
+
+Indeed, z dot s_b = 1+1 = 0, so z is in V_b. Also x dot z = x dot r_i
+for x in U_a. Nonsingularity gives uniqueness.
+
+Every exceptional source normal kills z, since
+
+    s_j dot z = s_j dot r_i + s_j dot r_a = 1+1 = 0.           (4)
+
+By linearity, every vector of S kills z. The row-space hypothesis on C
+therefore implies C z = 0.
+
+Write the restricted double pairing in block form as [A B; E D], with
+A and D nonsingular eight-by-eight matrices. For a source vector y in
+V_d, the vector representing B's functional on U_a is z (v dot y).
+Equation (4) gives E A^-1 B = 0. Block elimination now gives
+
+    rank_F2 [A B; E D] = 8 + rank_F2(D - E A^-1 B) = 16.       (5)
+
+Thus every double term has price at least 16. This is the new step.
+In particular, it applies when C is a sum of independent exceptional
+source functionals, rather than one rank-one cross form.
+
+## From term prices to the sharp floor
+
+The inherited coefficient identity is sum_j a_j c_j^T = I_16 over C,
+with ordinary transpose. Discard terms having a zero entire factor.
+Call a term pure if it has a reader in one call and a source only in the
+other. Let n count all non-pure terms and d count the double terms.
+
+Each diagonal identity block has complex rank eight and therefore needs
+at least eight diagonal-contributing terms. A double contributes to both
+blocks; every other non-pure term contributes to exactly one. Hence
+
+    n + d >= 16.                                              (6)
+
+Every non-pure term has price at least eight from its within-call block.
+Equation (5) raises the double-term charge to sixteen. Pure prices are
+nonnegative, so the complete separate-total COPY price is at least
+
+    8(n-d) + 16d = 8(n+d) >= 128.                             (7)
+
+The sixteen separate coordinate terms give I_16 and cost 16*8 = 128,
+independently of the cross forms. This proves attainment.
+
+## An explicit case outside the prior sufficient test
+
+Use the actual retained geometry. Its annihilators, as nine-bit integers,
+are
+
+    r = [129,65,209,17,197,5,149,85],
+    s = [33,289,297,41,267,11,3,259].
+
+Let e = 1, the first binary coordinate vector, and set
+
+    beta01 = r_0 e^T,
+    beta10 = r_1 s_0^T + e s_1^T.
+
+Their row arrays are respectively
+
+    [1,0,0,0,0,0,0,1,0],
+    [256,0,0,0,0,0,33,0,0].
+
+The global ranks are (1,2), while both minimum coordinate-support cross
+ranks are zero. The forward restriction vanishes on U_0. The reverse
+restriction vanishes on U_1 x V_1. Its two left vectors and two right
+vectors are independent, so its global rank is two. PR2395's sufficient
+test c01+c10 >= min(8,r01,r10) reads 0 >= 1 and abstains here. The theorem
+above proves the exact minimum 128 for this example and its whole family.
+
+This does not settle the entire rank-(1,2) class. It excludes this
+exceptional-hull way of exploiting the zero pure prices.
+
+## Evidence boundary and credit
+
+The arbitrary-complex-factorization theorem is a written scoped proof.
+The verifier derives the eight normals from the pinned geometry, checks
+8,192 transfer instances and all 6,561 choices of the fixture's four
+support spans, including full spans. It checks the fixture's ranks and
+zero minima, the coordinate attainer, and two actual price-15 doubles
+after removing the respective geometric hypotheses. It does not rerun
+the inherited complete support census or enumerate complex decoders.
+
+JoyboyBrian's adjacent PR5141, head
+`b75399c455aa24f21ec9c78c337c3c277efd177d`, proves the full rank-(1,1)
+floor. Its mixed-orientation argument covers a rank-one reverse form
+with one exceptional source functional. Equations (3)-(5) extend that
+argument to a reverse row space in their linear span, giving new
+higher-rank cases. No PR5141 code or theorem is a runtime dependency.
+
+The inherited model and support/count lemmas retain Sagar Thakrar,
+commdata2338, alephnan, Mihir Srivastava and Adam Gall's credit. The new
+exceptional-hull extension and package were produced by Nick Petalas.
+Apache-2.0. Independent human and formal proof-kernel review are unclaimed.

research/p112-exceptional-hull-floor/README.md

@@ -0,0 +1,105 @@
+# A sharp P112 floor for exceptional-hull cross forms
+
+The new [scoped proof](PROOF.md) gives exact two-call COPY cost **128** when
+`beta01 = r_i v^T` and the reverse form's row space lies in the binary span
+of the eight exceptional source annihilators. The reverse form may have
+rank greater than one. Every double term then costs at least 16, because
+its Schur feedback vanishes.
+
+The explicit rank-(1,2) fixture has minimum pure cross prices `(0,0)`.
+Thus commdata2338's [PR2395](https://github.com/CrocSwap/integer-mult-bounds/pull/2395)
+sufficient test abstains, while this theorem proves the sharp floor.
+The new result excludes this exceptional-hull subfamily of PR2395's open
+rank-(1,2) cases. It does not settle that entire rank pair.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Reproduction and evidence
+
+From the repository root, use CPython 3.12, standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/p112-exceptional-hull-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p112-exceptional-hull-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/p112-exceptional-hull-floor --check-source-history
+```
+
+The portable interpreter spelling is `python3.12 -W error -B`. Run the
+publication preflight after committing. The registered normal and optimized
+commands print a generated JSON receipt bound to the package and live-source
+hashes, followed by
+
+```text
+PASS_P112_EXCEPTIONAL_HULL transfer=8192 doubles=6561 floor=128 controls=2
+```
+
+Local replay used CPython 3.12.15 on macOS arm64. Both registered commands
+passed. Hosted CI is recorded in the PR body when available.
+
+The 8,192 transfer checks cover all eight forward exceptional choices,
+eight reader restrictions, eight source restrictions and sixteen elements
+of the source-normal span. The 6,561 double cases cover all nine possible
+support spans in each of four positions for the explicit fixture. They
+have minimum price 16. The sixteen coordinate terms attain 128.
+
+Two hypothesis-removal controls exhibit actual price-15 doubles. They
+show why the new double-price argument needs its geometric hypotheses;
+they do not exhibit a sub-128 exact decoder. The written proof supplies
+the universal implication for arbitrary complex factors. No solver, Lean,
+native operator replay or multiplier replay is required or claimed.
+
+## Sources and related work
+
+The base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7.
+[SOURCES.json](SOURCES.json) pins the actual geometry and PR2395 proof.
+PR2395, head `361de309e5fc05f83862f0b6c611210eda9837a1`, supplies the support
+classification, within-call floor and coefficient incidence count. Sagar
+Thakrar's [PR2294](https://github.com/CrocSwap/integer-mult-bounds/pull/2294)
+supplies the arbitrary directed cross-form model, following alephnan's
+PR1714 and the support work of Mihir Srivastava and Adam Gall.
+
+JoyboyBrian's [PR5141](https://github.com/CrocSwap/integer-mult-bounds/pull/5141),
+head `b75399c455aa24f21ec9c78c337c3c277efd177d`, settles rank-(1,1). Its
+mixed-orientation calculation is the adjacent rank-one predecessor. The
+new step closes the reverse functional under linear span and thereby
+allows higher reverse rank. Its proof and verifier are not imported.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144293)
+is the canonical investigation record. The catalogue card
+`formal-interface-lemma` is changed to this written interface proof, with
+no claim of proof-assistant formalization.
+
+## Limitations
+
+The inherited support theorem is a cited premise. This package computes
+only the geometry needed for the new transfer and fixture, rather than
+rechecking that theorem. The union rank price is the separate-total
+two-call root-code model. Physical chart realization, dirty restoration,
+hosting, precision, rank-power costs, recursive admission and integer
+multiplication remain outside scope. The selected frontier is unchanged.
+
+## Open next questions
+
+1. Settle the rank-(1,2) cases outside this exceptional-hull family. First
+   classify which coordinate restrictions give nonzero Schur feedback;
+   then couple those discounts to the paid pure terms. Arbitrary complex
+   coefficient cancellation remains the obstacle.
+2. Can a legal physical cross-form interface realize any surviving
+   discounted pairing? Start with one explicit form and charge its chart
+   conversions and cleanup. A binary form alone supplies no implementation.
+
+## Verifier bounds
+
+The verifier uses structured control flow, fixed finite domains and no
+recursion or code generation. Every function is shorter than 60 lines.
+Checks use explicit exceptions and remain active under optimization.
+The diagnostics command is Python's warning-strict replay in both modes.
+
+Power-of-ten rule 3 has a CPython runtime deviation in `verify.py`.
+Integers, JSON parsing and lists allocate dynamically. Input files are capped
+at 2 MiB; the root table is 112-by-8, and the largest pairing is 18-by-18
+binary. The 6,561-case enumeration retains one pairing at a time. The
+normal and optimized replays exercise this bound. A fixed-memory port
+would be needed only if this finite offline verifier becomes an embedded
+runtime requirement. No shared library or predecessor file is changed.

research/p112-exceptional-hull-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/p112-cross-form-rank-tradeoff/PROOF.md",
+      "usage": "input",
+      "git_blob": "f29d1c7c189e2c1addb81001b7266a80a828db47",
+      "sha256": "91c7e68d2b93354a5a041e62408ec592e73167c7176816e7e53f6ae27c3b9bfb"
+    },
+    {
+      "path": "research/p112-single-lift/reference-geometry.json",
+      "usage": "input",
+      "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640",
+      "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080"
+    }
+  ]
+}

research/p112-exceptional-hull-floor/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove a sharp 128 COPY-rank floor for two-call P112 cross forms beta01=r_i v^T and rowspace(beta10) contained in the exceptional source-normal span, including an undecided rank-(1,2) fixture.",
+  "scope_change_reason": "The card asks for formalization. This contribution instead proves a new scoped binary transfer implication left open by PR2395, with a written proof and exact finite evidence. No kernel formalization is claimed.",
+  "bottleneck_link": "The new double-term price rules out an exceptional-hull route to sub-128 two-call COPY, directing residual searches toward cross forms outside this family.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved higher-rank case and package it; do not extend to arbitrary residual rank pairs.",
+  "outcome": "completed",
+  "evidence": "Written Schur-feedback proof; 8192 transfer instances; 6561 support-span double matrices for a rank-(1,2), minimum-(0,0) fixture; sharp 128 coordinate attainer; two price-15 hypothesis-removal controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can rank-(1,2) cross forms outside the exceptional-hull family beat total COPY price 128?",
+      "why_it_matters": "The new theorem excludes a subfamily but leaves the full residual pair open.",
+      "first_step": "Classify nonzero Schur feedback at coordinate restrictions, then couple double discounts to pure coefficient ranks.",
+      "blocked_by": "Arbitrary complex coefficient cancellation and support-price coupling."
+    },
+    {
+      "question": "Can a surviving discounted cross form be realized by a legal paid physical interface?",
+      "why_it_matters": "Binary rank prices alone do not give a supplier or kappa improvement.",
+      "first_step": "Name one explicit cross form and charge chart conversions and dirty cleanup.",
+      "blocked_by": "A physical realization and complete producer/consumer bill are absent."
+    }
+  ]
+}