Prove the all-field one-way corank-one header formula (no new κ)

research/oneway-all-field-closed-form/PROOF.md

@@ -0,0 +1,116 @@
+# All-field closed form for one-way coupled full guards
+
+This scoped counting proof was produced by Nick Petalas. Apache-2.0.
+
+Let K be a finite field of order q, m>=2, and n=m-1. Let U,V be rank-one
+idempotents on K^m with UV nonzero and VU=0. Set P=I-U and Q=I-V.
+Choose a complete header G uniformly in GL_m(K). A request passes when
+every leading principal minor of its conjugate, through order m-1, is
+nonzero. Define
+
+```text
+alpha=(q^2-q+1)^2, beta=q^3-q+1, gamma=q^3-q^2+1,
+D=(q^m-1)(q^m-q)q^(2m-4).
+```
+
+The exact joint passing fraction is C(q,m)/D, where
+
+```text
+C(q,m) = (q-1)/q^2 * [(q-1)alpha^n - (q-2)beta^n - gamma^n].       (1)
+```
+
+Thus the number of complete passing headers is C(q,m)|GL_(m-2)(K)|.
+This replaces #4274's all-field transfer by a closed formula. Its binary
+specialization was already proved there; the new claim is the all-field
+expression. There is no new kappa or supplier claim.
+
+## Cited input and changed initial matrix
+
+Nick Petalas's [#4274 transfer theorem](https://github.com/CrocSwap/integer-mult-bounds/pull/4274),
+retained in the main-branch source pinned by SOURCES.json, identifies
+normalized pairs YX=L, with L=[[1,1],[0,1]], and equal header fibers.
+The partial Gram sum A must have A_11,A_22 different from 1 until its
+last increment. For any 2 by 2 matrix H let w(H) equal 2q^2-1 at zero,
+q-1 at nonzero rank one, and zero at rank two.
+
+Make the substitution B=L-A. Its diagonal restriction is exactly that
+both diagonal entries of B are nonzero. The initial state is B=L and
+the terminal weight is h(B)=w(B). Negation preserves w. Consequently
+
+```text
+C(q,m) = (T^n h)(L),
+(Tf)(B) = sum_(C with nonzero diagonal) w(B-C)f(C).
+```
+
+The transfer and header-fiber theorem are predecessor credit, not new
+results or independent audits in this contribution.
+
+## Solving the invariant coordinates
+
+Use the three-function identities proved in Nick Petalas's
+[#4747, PROOF.md, Three invariant functions](https://github.com/petalas/integer-mult-bounds/blob/f51dcebce79b8b8958427a9a9b7bc8feca352c9d/research/corankone-all-field-law/PROOF.md).
+This is an exact external theorem citation at commit
+f51dcebce79b8b8958427a9a9b7bc8feca352c9d; no source code from that
+pending package is imported or replayed. Put r=q-1 and
+z(B)=1_(B_12=0)+1_(B_21=0). The cited identities are
+
+```text
+T1 = alpha 1,
+Tz = 2r^3 1 + beta z,
+Th = r^2(q^2-3q+4)1 - r^2 z + gamma h.                         (2)
+```
+
+Write T^n h=a_n 1+b_n z+c_n h. This representation need not be unique
+on small fields; the following coefficient solution still proves the
+function identity. From (2), starting at (a_0,b_0,c_0)=(0,0,1),
+
+```text
+a_(n+1) = alpha a_n + 2r^3 b_n + r^2(q^2-3q+4)c_n,
+b_(n+1) = beta b_n - r^2 c_n,
+c_(n+1) = gamma c_n.
+```
+
+Direct substitution gives, for every integer n>=0,
+
+```text
+q^2 a_n = r^2 alpha^n + 2r beta^n - r(q+1)gamma^n,
+q^2 b_n = -qr(beta^n-gamma^n),
+c_n = gamma^n.                                               (3)
+```
+
+For clarity, the polynomial identities needed in this substitution are
+
+```text
+beta-gamma=qr,
+alpha-beta=qr^3,
+(q+1)(alpha-gamma)=q r[2r^2+q(q^2-3q+4)].
+```
+
+The initial coefficients in (3) are 0,0,1. The last recurrence is
+immediate; the first two follow from these identities. Induction proves
+(3) without a characteristic restriction. All divisions here occur in
+the rational counting coefficients, not in K, so characteristic two is
+included.
+
+Finally, z(L)=1 and h(L)=0 because L has one zero off-diagonal entry
+and is invertible. Hence C=a_n+b_n. Combining (3) yields (1).
+The cited equal-fiber theorem supplies the probability denominator and
+the complete-header count. This proves the stated all-field result.
+
+## Boundary examples and scope
+
+At m=2 the numerator simplifies to
+(q-1)^2(q^2-3q+3). For q=2,3,4,5 the passing fractions are respectively
+1/6, 1/4, 7/20, 13/30. At q=3,m=3 the fraction is 53/351, agreeing
+with #4274's one-way transfer example. For q=5 the new formula is
+
+```text
+C(5,m)=(4/25)[4*441^n-3*121^n-101^n].
+```
+
+Only the closed form is new. No negative-correlation theorem for odd
+fields, classification of two-way coupling, restricted header theorem,
+or physical implementation is claimed. Selection, emission, dispatch,
+dirty restoration, precision and stock costs are unknown. The proof
+uses the cited all-field invariant identity as a predecessor theorem;
+independent human and formal proof-kernel review are unclaimed.

research/oneway-all-field-closed-form/README.md

@@ -0,0 +1,103 @@
+# All-field closed form for one-way coupled full guards
+
+This scoped counting proof was produced by Nick Petalas. Apache-2.0.
+
+## Scope and evidence
+
+For rank-one idempotents U,V over F_q^m with UV nonzero and VU=0, the
+two requests I-U,I-V use one complete, uniformly weighted GL_m header.
+A request passes when every leading principal minor through its rank
+is nonzero. Put n=m-1 and
+
+```text
+alpha=(q^2-q+1)^2, beta=q^3-q+1, gamma=q^3-q^2+1.
+```
+
+The exact normalized passing-pair numerator is
+
+```text
+C(q,m)=(q-1)/q^2 * [(q-1)alpha^n-(q-2)beta^n-gamma^n].
+```
+
+Divide by `(q^m-1)(q^m-q)q^(2m-4)` for the probability, for every finite
+field and every m>=2. At q=5 this is `(4/25)[4*441^n-3*121^n-101^n]`.
+The m=2 passing fractions for q=2,3,4,5 are 1/6, 1/4, 7/20, 13/30.
+
+[#4274](https://github.com/CrocSwap/integer-mult-bounds/pull/4274) supplied
+the all-field transfer and the binary closed form. The new step in
+[PROOF.md](PROOF.md) changes the initial matrix in
+[#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747)'s
+three-function invariant system and solves its coefficient recurrence.
+Both predecessor theorems are cited, not audited or claimed as new.
+
+The self-contained verifier checks 4,095 integer-parameter coefficient
+comparisons at 2<=q<=64 and 0<=n<=64, and 36 raw partial-Gram transfer
+cases over F2,F3,F4,F5 at 0<=n<=8. It explicitly visits 182,048
+source/target state pairs. It also enumerates every complete GL2 header
+over F2,F3,F4,F5,F7,F8,F9, a total of 12,018 headers, including extension
+fields. Six semantic controls and four input-bound rejections remain
+active with assertions disabled. The generated stdout receipt binds all
+six package files by SHA256; no handwritten receipt is stored.
+
+This algebraic side result changes the `formal-interface-lemma` card's
+premise, as recorded in [TASK.json](TASK.json). [SOURCES.json](SOURCES.json)
+pins the original catalogue, selected record and retained #4274 proof as
+historical provenance. There are no live external code inputs or Python
+dependencies. The exact external #4747 theorem citation is at commit
+`f51dcebce79b8b8958427a9a9b7bc8feca352c9d`; no pending Git object is
+needed to execute the package or its publication preflight.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/oneway-all-field-closed-form/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-all-field-closed-form/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-all-field-closed-form
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-all-field-closed-form --check-source-history
+```
+
+Replace the local interpreter path with another CPython 3.12 installation
+elsewhere. Expected markers are `PASS_ONEWAY_ALL_FIELD_CLOSED_FORM`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+The last command requires a publication commit and full Git history.
+The direct verifier writes nothing and can run from a Git-free package copy.
+
+## Limits and implementation constraints
+
+The universal statement uses the written argument and the cited invariant
+theorem. Finite execution corroborates its stated domains. Only two fixed
+one-way coupled rank-one kernels and complete uniform headers are covered.
+Physical selection, emission, dispatch, dirty restoration, precision and
+stock costs remain unknown. No new kappa, supplier admission or complete
+multiplication theorem follows. Independent human and formal proof-kernel
+review are unclaimed. Lean, Docker and selected operator replay are unrun.
+
+The verifier has no recursion or dynamic code loading. Its largest state
+matrix is 400 by 400, replay length is at most eight, field tables have at
+most 81 entries, and coefficient checks stop at q=64,n=64. Functions stay
+below 60 lines. CPython allocation and iterator dispatch are managed-runtime
+deviations from Power of Ten rules 3 and 9, bounded by these fixed domains.
+No plugin or callback registry is used. Normal and optimized warning-strict
+commands exercise the same explicit checks. A fixed-capacity native replay
+would require a separately specified integer capacity and is not supplied.
+
+## Open next questions
+
+1. Does the one-way joint law have strict negative correlation over every
+   finite field? Compare this formula with #4227's squared marginal after
+   checking live claims. The odd-field inequality is not proved here.
+2. Can a named odd-field producer use a fully charged one-way shared-header
+   caller? Pin its kernel pair and header domain, then price selection,
+   emission, dispatch and dirty return. Unknown physical costs block any
+   supplier consequence. Structured first steps and blockers are in TASK.json.
+
+## Credit
+
+Nick Petalas's #4274/#4261 supplied the transfer and equal-header fibers;
+#4747 supplied the all-field invariant identities; #4227 supplied the
+corank-one guard and marginal context. The binary formula and small prime
+examples are predecessor credit. Cinna Davis supplied the BIT request
+context; source527, commdata2338 and Jose Manuel retain the normalizer and
+recursive-closure lineage credit. No predecessor files are modified.

research/oneway-all-field-closed-form/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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/oneway-corankone-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5361c339bd172e13e0a2383ba734fa6e16f1082e",
+      "sha256": "1b13487af3fb2c0822f5cf417e017e507d74d85045c0df6a44997993eaa18a96"
+    }
+  ]
+}

research/oneway-all-field-closed-form/TASK.json

@@ -0,0 +1,113 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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": "An exact all-field closed form for two one-way coupled corank-one full-guard requests, for every finite field and m>=2.",
+  "scope_change_reason": "The assignment asks for original successor work. This algebraic side result extends the all-field transfer of PR4274 using the invariant identity of PR4747; it is not an audit or a selected-caller formalization.",
+  "bottleneck_link": "Exact joint header densities describe simultaneous request admission. A physical producer and complete caller cost are still required before a supplier consequence.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified closed formula, or at a documented obstruction within a 60-minute budget.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-field expression using cited transfer and invariant theorems. verify.py prints a file-bound receipt for 4095 coefficient comparisons, 36 raw-transfer cases and complete GL2 header counts over seven fields.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does one-way coupled full-guard admission have strict negative correlation over every finite field?",
+      "why_it_matters": "A joint density alone does not determine whether sharing a header is more favorable than multiplying marginals.",
+      "first_step": "Compare the new three-power formula with the corank-one marginal from PR4227, after checking active claims.",
+      "blocked_by": "No inequality for odd fields is supplied here."
+    },
+    {
+      "question": "Can a named odd-field producer use a fully charged one-way shared-header caller?",
+      "why_it_matters": "A counting result removes no paid work until its producer and consumer are realized.",
+      "first_step": "Pin one actual kernel pair, its header domain and the complete selection/emission/dispatch/return ledger.",
+      "blocked_by": "Preparation, routing, dirty restoration, precision and stock costs remain unknown."
+    }
+  ],
+  "predecessor_theorems": [
+    {
+      "pr": 4274,
+      "head": "497b8862d98ab57e33b262fa2631afc5a559257f",
+      "scope": "One-way transfer and equal header fibers; retained on base main."
+    },
+    {
+      "pr": 4747,
+      "head": "f51dcebce79b8b8958427a9a9b7bc8feca352c9d",
+      "scope": "Three invariant function identities; exact external theorem citation, not a code or Git-object dependency."
+    }
+  ]
+}

research/oneway-all-field-closed-form/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "New formula versus the three-coordinate recurrence, raw transfer, complete GL2 headers over seven fields, semantic and boundary controls; generated SHA256 receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same explicit checks and file-bound receipt with Python assertions disabled."
+    }
+  ]
+}