Prove all-field negative correlation for one-way full guards (no κ)

research/oneway-pair-correlation/PROOF.md

@@ -0,0 +1,107 @@
+# One-way coupled full guards have strictly negative correlation
+
+This scoped algebraic proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement and cited inputs
+
+Let K be a finite field of order q, let m>=2, and 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 G uniformly from the complete group GL_m(K). Let A and B be the
+events that every leading principal minor through order m-1 of GPG^-1
+and GQG^-1, respectively, is nonzero. Write p=Pr(A)=Pr(B) and
+J=Pr(A and B). Then
+
+```text
+J < (1-q^(-m)) p^2 < p^2.
+```
+
+Consequently Cov(1_A,1_B) < -q^(-m) p^2. This answers Open next question 1
+of [#4769](https://github.com/CrocSwap/integer-mult-bounds/pull/4769).
+It is a new inequality for the one-way coupling, using the counting laws
+as cited dependencies. The binary strict-correlation result is already in
+#4274; the all-field quantitative bound is new here. This is not a replay
+or audit of the predecessor proofs.
+
+Use Nick Petalas's marginal law in
+[#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227) and
+one-way joint law in #4769. Their exact retained proof blobs are pinned
+as historical provenance in SOURCES.json. Put
+
+```text
+n=m-1 >= 1,  t=q^m,  s=q^2-q+1,
+alpha=s^2,  beta=q^3-q+1,  gamma=q^3-q^2+1.
+```
+
+The cited formulas, with the latter's rational normalization cancelled, are
+
+```text
+p = (q-1)s^n / [q^n(t-1)],
+
+J = (q-1)[(q-1)alpha^n-(q-2)beta^n-gamma^n]
+    / [q^(2n)(t-1)(t-q)].                                  (1)
+```
+
+All denominators are positive and p>0. Dividing gives
+
+```text
+J/p^2 = (t-1)/(t-q) * (1-D),
+D = [(q-2)beta^n+gamma^n] / [(q-1)alpha^n].                  (2)
+```
+
+## The new comparison
+
+The following identities hold for every real q>=2:
+
+```text
+beta-gamma = q(q-1) > 0,
+q*gamma-alpha = (q-1)^3 > 0.                                (3)
+```
+
+Also gamma=q^2(q-1)+1>0 and alpha>0. The nonnegative weights q-2 and 1
+sum to q-1, so (3) and the positive integer n give
+
+```text
+D >= gamma^n/alpha^n > q^(-n).                              (4)
+```
+
+The first inequality is equality at q=2, but the second is always strict.
+Insert (4) into (2), multiplying only by positive quantities:
+
+```text
+J/p^2 < (t-1)/(t-q) * (1-q^(-n))
+      = (t-1)/t
+      = 1-q^(-m).
+```
+
+This proves the claim in every characteristic, including extension fields.
+There is no finite cutoff or untested tail. The polynomial comparison
+holds for every real q>=2; the header probability interpretation requires
+q to be a prime power.
+
+Nick Petalas's orthogonal-kernel comparison in
+[#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767)
+uses 2*beta^n-gamma^n and q*beta-alpha. Here the joint law has a different
+weighted correction, and its least base gamma suffices through the second
+identity in (3). That proof pattern is predecessor credit. Only the
+one-way correlation statement and its comparison are claimed here.
+
+## Complete-header hypothesis and limits
+
+A literal binary example shows why a restricted header catalogue does
+not inherit the inequality. Take
+
+```text
+U=[[1,1],[0,0]],  V=[[0,0],[0,1]],  G=[[1,0],[1,1]].
+```
+
+Here UV is nonzero, VU=0, and G^-1=G. Both conjugated requests have first
+diagonal entry 1, so both pass. If the header domain consists only of G,
+then J=p=1, which violates the displayed bound. Thus a physical caller's
+restricted catalogue needs a separate theorem.
+
+The argument supplies no header selection, emission, dispatch, dirty
+restoration, precision, stock or complete physical invoice. Those costs
+remain unknown. Two-way coupling and larger request families are outside
+the claim. No new kappa, supplier admission, selected-frontier change or
+complete multiplication theorem follows. Independent human and formal
+proof-kernel review are unclaimed.

research/oneway-pair-correlation/README.md

@@ -0,0 +1,104 @@
+# Strict one-way corank-one correlation over every finite field
+
+This scoped algebraic proof was produced by Nick Petalas. Apache-2.0.
+
+## Result and evidence
+
+Let U,V be rank-one idempotents over F_q^m with UV nonzero and VU=0.
+The two requests I-U,I-V use a complete, uniformly weighted GL_m(F_q)
+header. Each passes when every leading principal minor through order m-1
+is nonzero. For every finite field and every m>=2,
+
+```text
+Pr(A and B) < (1-q^(-m)) Pr(A)Pr(B) < Pr(A)Pr(B).
+```
+
+This settles Open next question 1 of
+[#4769](https://github.com/CrocSwap/integer-mult-bounds/pull/4769).
+The new step in [PROOF.md](PROOF.md) uses
+`q*gamma-alpha=(q-1)^3>0` to bound the one-way formula's weighted
+correction in every dimension. The marginal and joint counting laws are
+cited dependencies. Their proofs are not audited or rechecked here.
+The binary strict-correlation result is already in #4274; the new claim
+is the all-field quantitative bound. #4767 supplied the analogous
+orthogonal-kernel proof pattern and retains its credit.
+
+The verifier checks the polynomial identity by coefficient convolution
+and compares exact rational expressions at every integer
+2<=q<=64, 2<=m<=65, a total of 4,032 parameter pairs. Non-prime-power q
+check only the algebra. Five fixtures include q=4 and the one-way value
+J=53/351 with p=49/117 at q=3,m=3. Ten scenario controls cover independence,
+wrong or missing corrections, a literal singleton-header counterexample
+and six invalid finite-check inputs. A separate reversed-sign polynomial
+control also rejects. All checks remain active under optimized Python.
+The generated stdout receipt binds all six package files by SHA256.
+No receipt is handwritten or committed.
+
+This is an algebraic side result, with the explicit card scope change in
+[TASK.json](TASK.json). [SOURCES.json](SOURCES.json) pins the task catalogue,
+selected record and the three cited retained proofs as historical
+provenance at canonical main 624de9dc66858af0945e5f8a0942488d62280d43.
+There are no live external code inputs or third-party dependencies.
+
+## 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-pair-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-pair-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-pair-correlation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-pair-correlation --check-source-history
+```
+
+Use another CPython 3.12 installation in place of the local interpreter
+path elsewhere. Expected markers are `PASS_ONEWAY_PAIR_CORRELATION`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+The last command needs a publication commit and full Git history.
+The direct verifier writes nothing and works from a Git-free package copy.
+
+## Limits and implementation constraints
+
+The universal statement rests on the written proof and cited counting
+laws. Finite execution corroborates only the stated parameter domain.
+Exactly two fixed one-way coupled kernels and the complete uniform header
+domain are essential. The literal restricted-header example violates the
+bound when its domain has one element. Two-way coupling and larger request
+families remain open.
+
+Selection, emission, dispatch, dirty restoration, precision, stock and
+the complete physical caller bill remain unknown. No new kappa, supplier
+admission, selected-frontier change or complete multiplication theorem is
+claimed. Independent human and formal proof-kernel review are unclaimed.
+Lean, Docker and selected operator replay are unrun.
+
+The verifier has no recursion, subprocesses, dynamic code loading or
+external mutable state. Its parameter grid stops at q=64,m=65; polynomial
+inputs have at most four coefficients; fixtures and controls are fixed
+finite tuples. Six sequential file reads each have a 1 MiB capacity check.
+Every function is below 60 physical lines. Power of Ten rules 3 and 9
+have managed-runtime deviations for CPython allocation and standard
+iterator dispatch, confined to these bounded domains. Explicit contracts,
+normal and optimized warning-strict execution, and syntax diagnostics
+check the affected paths. Fixed-capacity native arithmetic would require
+a separately specified integer representation and is not supplied here.
+
+## Open next questions
+
+1. What correlation signs occur when both UV and VU are nonzero? This would
+   distinguish the remaining rank-one coupling types. First derive a joint
+   count for one named two-way pair and compare it with the cited marginal;
+   the one-way joint law does not apply to that pair.
+2. Can a named odd-field producer use a fully charged one-way shared-header
+   caller? Pin its kernel pair and actual header domain, then price selection,
+   emission, dispatch, restoration and stock. Unknown physical costs block
+   any supplier consequence. Structured first steps are in TASK.json.
+
+## Credit
+
+Nick Petalas's #4769/#4274 supplied the one-way joint law, #4227 supplied
+the corank-one marginal law, and #4767 supplied the orthogonal comparison
+and its proof pattern. The earlier binary strict-correlation proof remains
+#4274's credit. Cinna Davis supplied the BIT request context; source527,
+commdata2338 and Jose Manuel retain normalizer and recursive-closure
+lineage credit. No predecessor package is changed.

research/oneway-pair-correlation/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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/corankone-pair-correlation/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "fd2522be59e8c4d992688c4b5a229e88792e136b",
+      "sha256": "a3db8d9bfb191e7cbeb04dd3b2844692e0e5e3574f0f4d461a5e685f17f24716"
+    },
+    {
+      "path": "research/oneway-all-field-closed-form/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "6ccfc8cc732a238e9897d68549c228bce318fc73",
+      "sha256": "e30ea17fea8614a5fae3294e18ffb478cbd835d1b6c6aff4cadb2ad3757f79aa"
+    },
+    {
+      "path": "research/projector-header-density/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d",
+      "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262"
+    }
+  ]
+}

research/oneway-pair-correlation/TASK.json

@@ -0,0 +1,108 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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 strict negative correlation, with J < (1-q^(-m))Pr(A)Pr(B), for one-way coupled corank-one full guards over every finite field and m>=2.",
+  "scope_change_reason": "Take Open next question 1 of the merged one-way joint-law package #4769. This is a written algebraic side result, not a proof-assistant formalization or a predecessor audit.",
+  "bottleneck_link": "A quantified shared-header inequality resolves an open counting implication. It does not price a header producer or remove physical caller obligations, so it is not a supplier improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified dimension-uniform correlation bound and package it; leave other couplings and physical callers as open questions.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; exact coefficient-convolution identity; all 4,032 integer parameter pairs 2<=q<=64,2<=m<=65; five rational fixtures; ten scenario controls plus one polynomial sign control; generated file-bound stdout receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What correlation signs occur when both UV and VU are nonzero?",
+      "why_it_matters": "It distinguishes the remaining coupling types of two rank-one kernels.",
+      "first_step": "Pin one two-way pair, derive its joint full-guard count, and compare it with the existing marginal law.",
+      "blocked_by": "The one-way joint law requires VU=0 and does not cover this pair."
+    },
+    {
+      "question": "Can a named odd-field producer use a fully charged one-way shared-header caller?",
+      "why_it_matters": "A complete caller is needed before any header-density result can affect the supplier invoice.",
+      "first_step": "Pin the actual kernel pair and header domain, then price selection, emission, dispatch, dirty return and stock.",
+      "blocked_by": "No such physical producer or complete paid ledger is supplied."
+    }
+  ],
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131543",
+    "checked_at": "2026-10-22T19:46:02Z",
+    "upstream_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+    "coverage": "Complete cached pagination of 299 open PR bodies and 3,712 Discussion records; 105 local notes searched with 6,214 HEAD note paths omitted by sparse checkout. Main README and merged-PR searches for the formula, coupling and correlation were also run. Arbitrary diffs and unpublished work are outside coverage."
+  },
+  "claim_type": "scoped algebraic proof with finite corroboration"
+}

research/oneway-pair-correlation/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": "Exact polynomial comparison, 4,032 rational parameter pairs, five fixtures, ten scenario controls and a polynomial sign control."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same explicit mathematical checks and rejection controls with assertions disabled."
+    }
+  ]
+}