Prove all-field negative correlation for corank-one pairs (no new κ)

research/corankone-pair-correlation/PROOF.md

@@ -0,0 +1,92 @@
+# Strict pair correlation over every finite field
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let K be a finite field of order q and m >= 2. Let U,V be rank-one
+idempotents on K^m with UV=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 rank 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.
+```
+
+In particular the two indicator variables have strictly negative covariance,
+with Cov(1_A,1_B) < -q^(-m) p^2. This is a scoped algebraic proof using
+the cited counting laws. It answers Open next question 1 of #4747. The
+binary and ternary strict-correlation results were already proved in #4261
+and #4273, respectively. The all-field conclusion is the new result.
+
+## Cited formulas and their normalization
+
+Use Nick Petalas's marginal theorem in #4227 and joint theorem in #4747,
+the latter pinned at f51dcebce79b8b8958427a9a9b7bc8feca352c9d. We use these
+as predecessor results, without auditing or replaying their counting proofs.
+Put n=m-1 >= 1 and
+
+```text
+s = q^2-q+1,  alpha=s^2,  beta=q^3-q+1,  gamma=q^3-q^2+1.
+
+p = (q-1) s^n / [q^n (q^(n+1)-1)],
+
+J = (q-1)^2 (alpha^n - 2 beta^n + gamma^n)
+    / [q^(2n) (q^(n+1)-1)(q^(n+1)-q)].
+```
+
+All denominators are positive, and p>0. Division gives
+
+```text
+J/p^2 = [(q^(n+1)-1)/(q^(n+1)-q)]
+        * [1 - (2 beta^n - gamma^n)/alpha^n].                 (1)
+```
+
+## The comparison
+
+For every real q >= 2, the following factorizations are positive:
+
+```text
+beta - gamma = q(q-1) > 0,
+q beta - alpha = (q-1)(2q^2-2q+1) > 0.
+```
+
+Also gamma=q^2(q-1)+1>0 and alpha>0. Since n is a positive integer,
+
+```text
+2 beta^n - gamma^n > beta^n > alpha^n/q^n.                  (2)
+```
+
+Insert (2) into (1), multiplying only by positive quantities:
+
+```text
+J/p^2 < [(q^(n+1)-1)/(q^(n+1)-q)] (1-q^(-n))
+      = (q^(n+1)-1)/q^(n+1)
+      = 1-q^(-m).
+```
+
+This proves the quantitative bound in every characteristic, including
+nonprime fields. No finite cutoff, estimate of a remainder, or untested
+interval is used. The algebraic comparison itself holds for every integer
+q >= 2, while its probability interpretation requires q to be a prime power.
+
+At q=2,m=2 the cited joint fraction is zero, which satisfies the strict
+bound because p>0. No positive-common-header assumption is needed.
+
+## Scope
+
+Uniform sampling from the complete GL group is essential. For example,
+over F_3 with m=2, take U=diag(1,0), V=diag(0,1), and the single header
+G=[[1,1],[1,2]]. Its inverse is [[2,2],[2,1]]. Both conjugated requests
+have first diagonal entry 2, so both pass. Restricting the domain to this
+one header gives J=p=1, violating the displayed bound. Thus this theorem
+cannot price an arbitrary restricted header catalogue.
+
+Nothing here supplies header selection, emission, dispatch, dirty
+restoration, stock, precision or a complete physical caller. Those costs
+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.

research/corankone-pair-correlation/README.md

@@ -0,0 +1,116 @@
+# Strict corank-one pair correlation over every finite field
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with finite corroboration. For two
+requests I-U,I-V with orthogonal rank-one kernels on F_q^m, m>=2, and
+uniformly weighted complete GL_m headers, let A,B be their full-leading-minor
+passing events. Then
+
+```text
+Pr(A and B) < (1-q^(-m)) Pr(A)Pr(B) < Pr(A)Pr(B).
+```
+
+[PROOF.md](PROOF.md) answers Open next question 1 of
+[#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747).
+It cites that predecessor's joint law and #4227's marginal law, then proves
+the new inequality by two positive polynomial factorizations. The binary
+and ternary strict-correlation cases retain #4261 and #4273's credit.
+There is no cutoff or unrun infinite tail in the written proof.
+
+## Reproduction and evidence
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-pair-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-pair-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-pair-correlation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-pair-correlation --check-source-history
+```
+
+The direct verifier emits `PASS_CORANKONE_PAIR_CORRELATION` in generated
+JSON with hashes of all six package files. It writes no receipt or other
+file. Its evidence covers:
+
+- Exact integer and rational comparisons for all 4,032 pairs
+  2<=q<=64, 2<=m<=65. Non-prime-power integers test the algebra only.
+  This checks the new comparison and normalization, not the predecessor
+  counting proofs.
+- An exact polynomial coefficient identity for
+  q beta-alpha=(q-1)(2q^2-2q+1), independent of evaluations at chosen q.
+- Nine controls covering independence, two correction-term mutations,
+  restricted header domains and five invalid replay inputs. A separate
+  reversed-polynomial-sign check also rejects its mutant.
+- Exact joint-to-product ratios 28/243 at q=2,m=3, 24/49 at q=3,m=2,
+  and 40/49 at q=5,m=2. These preserve the predecessor numerical values.
+
+The written proof quantifies over every finite field and dimension. The
+finite checks corroborate it; they are not formal proof-kernel acceptance.
+
+## Scope and remaining obligations
+
+This is an original consequence of cited formulas, not an independent audit
+of them. Pending #4747 is an explicit mathematical dependency, pinned in
+[SOURCES.json](SOURCES.json); no predecessor code or proof file is imported
+at runtime. The source manifest binds retained-main provenance through
+exact Git objects.
+Its separate external citation records the pending theorem by immutable URL
+and hash; the framework does not validate that bibliography entry.
+
+The result assumes two orthogonal rank-one kernels and the complete uniform
+header domain. Nonorthogonal kernels, restricted domains and three or more
+requests are outside scope. PROOF.md gives a singleton-domain counterexample
+to extending the inequality to restricted catalogues.
+
+No producer, selection/emission, dispatch, dirty restoration, stock,
+precision or complete physical invoice is supplied. These costs 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. Selected cold replay, Lean and Docker
+are unrun. Both registered package commands passed locally.
+
+The verifier has fixed finite loops, no recursion and functions below
+60 lines. CPython's required dynamic allocation is a deviation from fixed
+allocation. Its scope is this bounded, read-only finite replay, with at most
+one parameter pair active, six file hashes, three retained examples and
+polynomials of at most seven coefficients. The declared q,m limits bound
+integer sizes. Invalid-domain controls exercise exhaustion behavior.
+Warnings are errors in both registered modes. Ruff E/F/B/UP passes locally.
+Follow-up: retain these bounds if adding replay inputs; a larger search
+needs a fresh resource bound.
+
+## Related work and credit
+
+- Nick Petalas's [#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747),
+  head f51dcebce79b8b8958427a9a9b7bc8feca352c9d, supplies the all-field
+  joint law. At q=5,m=2, J=2/5 and p=7/10 give ratio 40/49, checked here.
+- Nick Petalas's #4227 supplies the marginal law. #4261 and #4273 supply
+  the binary and ternary pair laws and their strict negative correlation.
+  New here is the all-field inequality and its explicit relative gap.
+- #4599 and Ryanson Jonathan's #4607 prove binary four- and five-request
+  product inequalities. Ryanson Jonathan's #4606 independently checks the
+  four-event inequality. Their request counts differ from this two-event
+  theorem; no four- or five-event number is claimed here.
+- Ryanson Jonathan's #4605 recounts binary threshold headers. At its
+  overlapping k=2,m=3 case, J=1/84 and p=9/28 give ratio 28/243,
+  checked here; 168J=2 headers.
+- Nick Petalas's #4598 and Ryanson Jonathan's #4619 count and classify
+  five-request threshold decompositions. Their k=5 counts do not overlap
+  this two-request theorem.
+
+The earlier counting packages above are produced by Nick Petalas unless
+otherwise attributed. Cinna Davis supplies the BIT request context;
+source527, commdata2338 and Jose Manuel retain the normalizer lineage credit.
+The card's scope change and overlap coverage are recorded in TASK.json.
+
+## Open next questions
+
+1. Does negative association hold for disjoint groups in larger orthogonal
+   kernel families? First compare Pr(A1 A2 A3) with Pr(A1 A2)Pr(A3) using
+   #4275's binary three-request law. Pairwise negative correlation alone
+   does not imply this stronger property.
+2. Can an actual odd-field producer exploit a shared header with a complete
+   paid invoice? Pin its kernel lines and header domain before charging
+   selection, emission, dispatch, restoration and stock. No caller is
+   supplied here.

research/corankone-pair-correlation/SOURCES.json

@@ -0,0 +1,50 @@
+{
+  "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/projector-header-density/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/projector-header-density/PROOF.md",
+      "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d",
+      "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262"
+    },
+    {
+      "path": "research/corankone-pair-header-law/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/corankone-pair-header-law/PROOF.md",
+      "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548",
+      "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0"
+    },
+    {
+      "path": "research/ternary-corankone-pair-law/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/ternary-corankone-pair-law/PROOF.md",
+      "git_blob": "c91f551dcf370de1c5d2860d3c75e74bc1d88d6e",
+      "sha256": "096b3acfd46f905553f3145f5714d57a7f0141028c50fad04eea0ec4b252564f"
+    }
+  ],
+  "external_citations": [
+    {
+      "description": "Cited joint-law theorem, not imported code or machine-validated provenance. The source-history gate applies to files only.",
+      "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4747",
+      "commit": "f51dcebce79b8b8958427a9a9b7bc8feca352c9d",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f51dcebce79b8b8958427a9a9b7bc8feca352c9d/research/corankone-all-field-law/PROOF.md",
+      "path": "research/corankone-all-field-law/PROOF.md",
+      "git_blob": "ac0152e05a5c050bbd740ddbe6d0cbaaecbb6cd8",
+      "sha256": "ca7762bea269445f7b30c59c7b6161282483da5fd191faa668145f1ad6d8ade4"
+    }
+  ]
+}