Prove the joint full-guard law for an overlapping corank-one pair

research/corankone-pair-header-law/PROOF.md

@@ -0,0 +1,143 @@
+# Two overlapping corank-one requests
+
+## Contract and claim type
+
+This is a scoped counting proof. Let K be a finite field of order q, m >= 2,
+and let U,V be rank-one idempotents on K^m with UV = VU = 0. Put
+P = I-U and Q = I-V. A header G in GL_m(K) passes a request R when every
+leading principal minor of GRG^-1 of orders 1 through rank(R) is nonzero.
+We count headers passing both P and Q, with each complete header weighted
+equally. No restriction on the permitted header subset is implicit.
+
+P and Q commute. Their image intersection has dimension m-2, so for m > 2
+this is outside the orthogonal-request hypothesis of #4246. The theorem
+also differs from a nested rank-one/rank-r pair. At m=2, P and Q themselves
+are orthogonal rank-one requests, giving an overlap with #4239.
+
+## The general transfer law
+
+For a 2 by 2 matrix A over K, define
+
+```text
+w(A) = 2q^2-1  if A = 0,
+       q-1      if rank(A) = 1,
+       0        if rank(A) = 2.
+
+S = {A : A_11 != 1 and A_22 != 1}.
+f_0(A) = 1 if A = 0, otherwise 0.
+f_(j+1)(B) = sum_(A in S) f_j(A) w(B-A),  B in S.
+C(q,m) = sum_(A in S) f_(m-1)(A) w(I_2-A).
+D(q,m) = (q^m-1)(q^m-q) q^(2m-4).
+```
+
+**Theorem 1.** The joint passing fraction is C(q,m)/D(q,m). The recurrence
+has exactly q^2(q-1)^2 states and applies to every finite field, including
+nonprime fields. The number of passing headers is C(q,m)|GL_(m-2)(K)|,
+with |GL_0(K)| = 1.
+
+**Proof.** Orthogonality gives a direct decomposition
+K^m = im(U) + im(V) + (ker(U) intersect ker(V)). Choose nonzero vectors for the
+two one-dimensional images and a basis of the last summand. In this basis
+U = e_1 e_1^T and V = e_2 e_2^T. Changing this fixed basis permutes the
+complete header domain. It suffices to count this canonical pair.
+
+Write X = (u,v) for the first two columns of G, and Y = (a;b) for the first
+two rows of G^-1. Then YX = I_2 and the conjugated requests are I-ua and I-vb.
+Conversely every pair X,Y with YX = I_2 arises. The remaining columns of G
+can be any ordered basis of ker(Y), giving exactly |GL_(m-2)(K)| headers
+for every such pair. There are (q^m-1)(q^m-q) choices of X. Each row of Y
+solves two independent linear equations, giving q^(m-2) choices per row.
+Thus there are D(q,m) pairs, all with the same header fiber.
+
+The rank-one determinant identity gives
+
+```text
+det((I-ua)[1..j,1..j]) = 1 - sum_(i=1)^j a_i u_i.
+```
+
+The identity holds by multilinearity: choosing the rank-one part from two
+columns gives zero, leaving the identity term and j single-column terms.
+This is the corank-one guard reduction of #4227, with the proof included
+here to specify the exact interface.
+
+Let x_i = (u_i,v_i) be row i of X and y_i = (a_i,b_i)^T be column i of Y.
+The partial sums A_j = sum_(i=1)^j y_i x_i have their two diagonal entries
+equal to the prefix sums in the two determinant guards. Thus each A_j
+for 1 <= j < m must belong to S, and A_m = YX = I_2. There are no other
+guard conditions: both requests have rank m-1.
+
+For a fixed increment A, the number of ordered pairs y,x with yx=A is
+w(A). For zero, either x=0 or y=0, giving 2q^2-1 pairs. For a nonzero
+rank-one matrix, choose one factorization; all others rescale its factors
+by a nonzero scalar and its inverse, giving q-1 pairs. Rank two is
+impossible. The coordinate choices are independent before imposing their
+sum, so the recurrence counts every admissible X,Y once. The equal fibers
+then prove both formulas. S has q-1 choices for each diagonal entry and q
+for each off-diagonal entry. QED.
+
+## Binary closed form and correlation
+
+Put n=m-1. Define
+
+```text
+C(2,m) = (9^n - 2*7^n + 5^n)/4.
+```
+
+**Theorem 2.** This is the exact joint numerator in Theorem 1 for every
+m >= 2. Hence
+
+```text
+Pr(P and Q pass) = (9^(m-1) - 2*7^(m-1) + 5^(m-1))
+                  / (4(2^m-1)(2^m-2)2^(2m-4)).
+```
+
+It vanishes exactly at m=2 and is positive for every m>=3. For example,
+the fractions at m=3,4,5,6 are 1/84, 1/80, 149/14880 and 85/11904.
+
+**Proof.** In F_2, both diagonal entries of a safe state must be zero.
+The safe states are determined by their off-diagonal bits. A safe-state
+increment can only be zero, E_12 or E_21, with weights 7,1,1. The fourth
+zero-diagonal matrix has rank two and weight zero. The last increment
+I_2-A has both diagonal entries one, and has rank one exactly when both
+off-diagonal entries of A are one. Its weight is then one.
+
+We therefore need the number of length-n walks from (0,0) to (1,1), with
+seven stationary choices and one choice toggling each bit. The four
+characters of F_2^2 have eigenvalues 9,7,7,5. Character inversion at (1,1)
+gives (9^n-7^n-7^n+5^n)/4. Equivalently, expanding
+(7+x+y)^n modulo x^2=y^2=1 and extracting xy gives the same expression.
+
+For n=1 the count is zero. For n>=2, the word containing one E_12, one
+E_21 and n-2 zero increments gives a positive count. QED.
+
+**Corollary.** The two full-guard passing events are strictly negatively
+correlated over F_2 for every m>=2. Their joint fraction is asymptotic to
+(1/4)(9/16)^(m-1), and its ratio to the product of the marginal fractions
+tends to one from below.
+
+**Proof.** The single corank-one fraction, from #4227, is
+s_m = 3^n/((2^m-1)2^(m-1)). The binary guard reduction also proves it
+directly: the first n coordinate products are zero, giving three choices
+each, and the last product is one. A normalized rank-one factor pair has
+(2^m-1)2^(m-1) possibilities and equal header fibers. Therefore
+
+```text
+joint / s_m^2 = (2^m-1)/(2^m-2)
+               * (1 - 2(7/9)^n + (5/9)^n).
+```
+
+This is less than one because
+(2^(n+1)-1)(2*7^n-5^n) > 2^n 7^n > 9^n for n>=1. The stated limits
+follow by dividing the exact numerator and denominator by their leading
+powers. QED.
+
+## Scope
+
+The general transfer theorem covers all finite fields, but the replay
+implements q in {2,3,4,5,7}; F_4 uses x^2+x+1. Only q=2 has a closed form
+here. The proof is written mathematics, without a proof-kernel check.
+The binary case is outside the odd-prime preparation domain of the retained
+normalizer. Its algebraic count does not admit a binary physical caller.
+Even the odd-field recurrence supplies no request producer, header selection
+or emission, dispatch, dirty return, stock or complete cost invoice. Neither
+a supplier nor a complete multiplication theorem follows.

research/corankone-pair-header-law/README.md

@@ -0,0 +1,144 @@
+# Exact full-guard law for an overlapping corank-one pair
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped counting proof with finite corroboration.** Let U,V
+be orthogonal rank-one idempotents on F_q^m, m>=2. The requests P=I-U and
+Q=I-V commute and have an image intersection of dimension m-2. A complete
+header G passes a request when all leading principal minors through its
+rank are nonzero. Both requests use the same G.
+
+[PROOF.md](PROOF.md) gives an exact transfer recurrence over every finite
+field, with q^2(q-1)^2 states, and this binary closed form for every m>=2:
+
+```text
+Pr(P and Q pass) = (9^(m-1) - 2*7^(m-1) + 5^(m-1))
+                  / (4(2^m-1)(2^m-2)2^(2m-4)).
+```
+
+The binary passing events are strictly negatively correlated. A shared
+passing header exists exactly when m>=3. At m=3 the fraction is 1/84,
+while the product of the two marginals is (9/28)^2. At m=4 it is 1/80.
+The joint fraction is asymptotic to (1/4)(9/16)^(m-1), and its ratio to
+the product of the marginals tends to one from below.
+
+This answers one subcase of the nonorthogonal full-guard question in
+[#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240) and
+[#4246](https://github.com/CrocSwap/integer-mult-bounds/pull/4246). The new
+part is the joint full-chain count for overlapping images. The rank-one
+determinant identity and marginal density are credited to
+[#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227).
+
+## Reproduction and evidence
+
+From the repository root, with any CPython 3.12 replacing this local path:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-pair-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-pair-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-pair-header-law
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-pair-header-law --check-source-history
+```
+
+The scientific marker is `PASS_CORANKONE_PAIR_HEADER_LAW`. Its generated
+JSON contains each census denominator, joint count and single count, plus
+SHA-256 hashes of every package file and both declared source inputs.
+The verifier checks the source pins before enumeration and writes no files.
+There is no handwritten or stored result receipt.
+
+The finite corroboration is:
+
+- **32,274 complete GL headers**, over F_2 at m=2,3,4; F_3 at m=2,3;
+  and F_4,F_5 at m=2. Each header is inverted and both conjugated requests
+  undergo literal no-pivot elimination. Every normalized-pair fiber is
+  enumerated and checked for equal size.
+- **2,007,234 normalized pairs X,Y with YX=I_2**, over F_2 at m=2..6;
+  F_3 at m=2..4; and F_4,F_5 at m=2,3. These are enumerated separately
+  from the matrix headers and transfer recurrence. Every joint and marginal
+  fraction is checked. F_4 is F_2[x]/(x^2+x+1), not Z/4Z.
+- **99 transfer cases**, over F_2 at m=2..64 and F_3,F_4,F_5,F_7 at
+  m=2..10. Every binary case agrees with the closed form. Local rank-one
+  factor weights are separately enumerated over all five fields.
+- Four controls distinguish the independence product, omitted zero-factor
+  multiplicity, the wrong parity target and first-pivot-only admission.
+  At q=2,m=3 the last control distinguishes 2 full-guard headers from 54
+  headers passing only the first guards, out of 168.
+
+The entire small census is registered in both normal and optimized Python.
+The explicit checks remain active under `-O`. Executed checks corroborate
+the written universal proof; they do not replace it.
+
+## Scope and remaining obligations
+
+The transfer theorem is for every finite field; the implemented fields and
+dimensions are listed above. Only the binary law is simplified to a closed
+form. The assumptions are fixed idempotents with orthogonal rank-one kernels
+and a complete, equally weighted GL header domain. No density is asserted
+for arbitrary restricted header subsets.
+
+The binary case extends the guard algebra outside the retained normalizer's
+odd-prime executable domain. Even over odd fields, no real request producer,
+header selection/emission, dispatch, dirty return, stock, precision or full
+physical invoice is supplied. These costs remain unknown, rather than zero.
+No new kappa, selected-frontier change, supplier admission or complete
+multiplication theorem is claimed. Independent human and formal proof-kernel
+review are unclaimed. Selected cold replay, Lean and Docker were not run.
+
+The verifier uses bounded loops without recursion. The largest transfer has
+1,764 states and at most 679,140 stored transitions. Matrix dimensions are
+at most six in the direct pair census and four in the header census.
+CPython dynamically allocates integers, lists and tuples; this is a managed
+runtime deviation from fixed allocation, bounded here by the declared finite
+domains. Functions stay below 60 lines. Diagnostics use warnings as errors
+in both registered modes; Ruff E/F/B/UP is a local static check.
+
+## Related open work and credit
+
+- [#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227), head
+  `3d793eade8de2ba49ec08f8d004c1b2f566a78e6`, supplies the corank-one
+  determinant identity and marginal count. All 12 marginal fractions in this
+  pair census agree numerically with its formula. New here is the joint law.
+- [#4228](https://github.com/CrocSwap/integer-mult-bounds/pull/4228), head
+  `bb25dcedb5bbbacd3c35359eb6b5488b087bcde6`, gives all-rank single-request
+  densities. Its corank-one specialization is the same marginal formula,
+  numerically checked here in the same 12 cases. Its intermediate-rank
+  recurrence is not used or recounted.
+- [#4239](https://github.com/CrocSwap/integer-mult-bounds/pull/4239), head
+  `5e24dfb5463d540721687d92c369609da5589523`, gives the orthogonal rank-one
+  joint law. At m=2 this theorem becomes its two-request case. The five
+  transfer fractions q=2,3,4,5,7 agree numerically with
+  (q-1)(q-2)/(q(q+1)); for q=3 the value is 1/6.
+- [#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240), head
+  `9f9c89ed75e9fdae6b6762925b080fb308824858`, counts nonorthogonal rank-one
+  first guards. This answers a higher-rank full-guard subcase of its first
+  open question. Only the m=2 orthogonal boundary overlaps numerically,
+  agreeing on the same five values above.
+- [#4246](https://github.com/CrocSwap/integer-mult-bounds/pull/4246), head
+  `a2d99d73bf21b39fbb0a9a88917424ff26c2e63c`, counts full chains for
+  orthogonal requests. P,Q here overlap when m>2, so its stage product
+  does not apply. The m=2 rank-(1,1) boundary agrees numerically on the
+  same five values. The laminar-family claim in the
+  [handoff thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166)
+  concerns nested or orthogonal requests. This pair is neither when m>2;
+  no overlapping count beyond the orthogonal m=2 case is asserted.
+
+All five preceding counting packages were produced by Nick Petalas.
+The retained normalizer and recursive-closure lineage is due to source527,
+commdata2338 and Jose Manuel. Cinna Davis supplied the #4100 BIT.md
+per-request accounting context. Chris R / Clear1nsight's #3950 is earlier
+deterministic header-counting context. No predecessor credit is changed.
+The written proofs here are self-contained; no unmerged predecessor code
+or unavailable Git-history object is imported. SOURCES.json pins the two
+retained main-branch contract files, base and original task card.
+
+## Open next questions
+
+1. Can the odd-q transfer be reduced to a closed form or a smaller invariant
+   state space? Start by quotienting the q=3 transfer while preserving both
+   diagonal guard values and rank(I-A). Such a quotient is not proved here.
+2. What is the full-guard law for three or more corank-one requests with
+   orthogonal rank-one kernels? Start with a 3 by 3 partial Gram matrix at
+   q=2,m=3,4. The four-state simplification no longer applies.
+3. Can a real odd-field producer use a fully charged shared-header caller?
+   Pin its kernel lines and charge selection, emission, dispatch, dirty
+   return and stock. A producer and its physical invoice are still missing.

research/corankone-pair-header-law/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/BIT.md",
+      "usage": "input",
+      "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa",
+      "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da"
+    },
+    {
+      "path": "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py",
+      "usage": "input",
+      "git_blob": "3e8a72e7ce705c51ff24e9015ccf6463204ff193",
+      "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77"
+    }
+  ]
+}