Count shared Schur-product rank pairs without matrix enumeration (no κ)

research/schur-rank-pair-law/PROOF.md

@@ -0,0 +1,178 @@
+# Joint nullities of a matrix and its identity shift
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+The subspace inclusion-exclusion method and Gaussian coefficients are classical.
+The contribution here is an explicit joint law, with all lifting factors retained,
+and its substitution into ssafwann's binary sharp Schur-header count from #4678.
+No priority claim about finite-field enumeration outside this repository is made.
+
+## Statement
+
+Let q be a prime power and d a nonnegative integer. Let C_d(a,b;q) count matrices
+H in M_d(F_q) with nullity H=a and nullity(I-H)=b. Write
+
+\[
+{n\brack k}_q=\prod_{r=0}^{k-1}\frac{q^n-q^r}{q^k-q^r},\qquad
+\mu(k)=(-1)^kq^{k(k-1)/2}.
+\]
+
+The Gaussian coefficient is zero for k outside 0..n. For 0<=a,b<=d with a+b>d,
+C_d(a,b;q)=0. Otherwise, put t=d-a-b. Then
+
+\[
+\boxed{\begin{aligned}
+C_d(a,b;q)
+={d\brack a}_q{d-a\brack b}_q q^{ab}
+\sum_{i=0}^{t}\sum_{j=0}^{t-i}
+&\mu(i)\mu(j){t\brack i}_q{t-i\brack j}_q\\[-2pt]
+&\cdot q^{ij+bi+aj+d(t-i-j)}.
+\end{aligned}} \tag{1}
+\]
+
+This is an exact integer formula. For each nullity pair it has
+(t+1)(t+2)/2 summands, so the entire distribution has O(d^4) explicit summands.
+This counts arithmetic summands, not bit operations or measured runtime.
+Gaussian coefficients and powers can be precomputed. The small standalone
+implementation instead evaluates their bounded products directly.
+
+## Proof
+
+The zero and one eigenspaces of H are disjoint. Indeed, Hv=0 and Hv=v imply
+v=0. This proves the a+b>d exclusion.
+
+There are
+
+\[
+B_d(a,b)={d\brack a}_q{d-a\brack b}_q q^{ab} \tag{2}
+\]
+
+ordered pairs of disjoint subspaces A,B of dimensions a,b. Choose A, choose
+the b-dimensional projection of B in V/A, and choose a lift of that projected
+subspace. Relative to a fixed complement, the lift is the graph of an arbitrary
+map into A, with q^(ab) choices. This proves (2).
+
+Fix one such pair, write W=A+B, and let t=dim(V/W). We count H for which
+ker H=A and ker(I-H)=B. Prescribing H to be zero on A and the identity on B
+leaves d*t free matrix entries, hence q^(dt) extensions before excluding
+larger eigenspaces.
+
+For a vector space L of dimension m, the elementary subspace identity is
+
+\[
+\sum_{U\le L}\mu(\dim U)
+=\sum_{k=0}^m {m\brack k}_q(-1)^kq^{k(k-1)/2}
+=\begin{cases}1&m=0,\\0&m>0.\end{cases} \tag{3}
+\]
+
+For completeness, the finite q-binomial expansion of
+`product_(r=0)^(m-1)(1-q^r z)` has coefficient
+`(-1)^k q^(k(k-1)/2) [m choose k]_q` at z^k. Induction on m, multiplying by
+the last linear factor and using the Gaussian recurrence, proves this
+expansion. Setting z=1 gives (3).
+
+For any H extending the prescription on A+B, apply (3) to ker H/A and
+ker(I-H)/B. The product of the two subspace sums is one exactly when both
+kernels equal their prescribed subspaces, and is zero otherwise. Summing over
+H and exchanging these finite sums gives a signed sum over super-subspaces
+A'>=A and B'>=B, of respective dimension increments i,j. A pair with nonzero
+intersection has no compatible H, since its intersection would have to be
+both fixed and killed.
+
+It remains to count the disjoint super-subspace pairs. Their projections into
+V/W are disjoint subspaces I,J of dimensions i,j. To see disjointness, suppose
+x in A' and y in B' have the same nonzero image in V/W. Write x-y=a+b with
+a in A,b in B. Then x-a=y+b is a nonzero vector in A' intersect B', which is
+impossible. The same argument shows A' intersect W=A and B' intersect W=B.
+
+Choose I and J disjoint in V/W. Equation (2) in dimension t gives
+
+\[
+{t\brack i}_q{t-i\brack j}_q q^{ij}
+\]
+
+choices. For fixed I,J and a fixed section V/W -> V, the possibilities for
+A'/A are graphs of maps I -> W/A, giving q^(bi) lifts. Similarly B'/B has
+q^(aj) lifts. Each pair of lifts is disjoint because I,J are disjoint, and
+every allowed A',B' occurs once. Thus the required number is
+
+\[
+{t\brack i}_q{t-i\brack j}_q q^{ij+bi+aj}. \tag{4}
+\]
+
+For each such pair, H is prescribed on A'+B', of dimension a+b+i+j, and
+is arbitrary on a complement. There are q^(d(t-i-j)) extensions. Multiplying
+by the inclusion-exclusion weights mu(i)mu(j), summing over i+j<=t, and then
+multiplying by (2) proves (1).
+
+## Substitution into the binary Schur-header law
+
+This part uses the one-block counting theorem of **ssafwann, #4678**, head
+`af9cf805c501e4e9e947c98c0b97b2281b6b6e97`. It does not reprove or audit that
+theorem. Its archived README is pinned as provenance in SOURCES.json.
+
+Fix commuting binary idempotents P,Q in dimension n. Let their joint-sector
+dimensions, ordered as 00,10,01,11, be r00,r10,r01,r11. A complete header is
+an ordered basis M in GL_n(F2). Its split pair consists of the first d columns
+of M and first d rows of M^-1. Let N count complete headers with both leading
+blocks I_d and Schur-commutator rank 2d, and let Z count complete headers with
+both leading blocks I_d. These are one-block events, not full-guard chains.
+
+Use ssafwann's factor counts, restated for clarity. Put
+
+\[
+I(s,k)=\prod_{j=0}^{k-1}(2^s-2^j),\quad G(s)=I(s,s),
+\]
+
+with I(s,k)=0 unless 0<=k<=s. Define
+
+\[
+U(r,d,\rho)=\sum_{k=\rho}^{\min(d,r)}
+ {d-\rho\brack d-k}_2 I(r,k)2^{d(r-k)},
+\]
+
+\[
+A(r,d,\rho)=I(r,d)2^{\rho(r-d)}I(r-d,d-\rho)
+\]
+
+when r>=d, and zero otherwise. U counts arbitrary factorizations XY=T of a
+fixed rank-rho d-by-d matrix through a dimension-r space. A also requires X
+surjective and Y injective. These formulas and the G(n-d) completion
+multiplicity are credited inputs from #4678.
+
+For each (a,b) put h=d-a and w=d-b. Grouping that theorem's sum over actual
+H by the exact nullity pair gives
+
+\[
+\boxed{\begin{aligned}
+N=G(n-d)\sum_{a=0}^d\sum_{b=0}^{d-a}
+ C_d(a,b;2)\,&U(r_{00},d,w)A(r_{10},d,w)\\
+ &\cdot A(r_{01},d,w)A(r_{11},d,h),\\
+Z=G(n-d)\sum_{a=0}^d\sum_{b=0}^{d-a}
+ C_d(a,b;2)\,&U(r_{00},d,w)U(r_{10},d,w)\\
+ &\cdot U(r_{01},d,w)U(r_{11},d,h).
+\end{aligned}} \tag{5}
+\]
+
+This substitution is the improvement. There is no enumeration of 2^(d*d)
+compressed products, and no independence approximation. The predecessor's
+complete-header density remains N/G(n) and its conditional density remains
+N/Z when Z>0. Split-pair counts are N/G(n-d) and Z/G(n-d).
+
+For four equal dimension-d sectors, all three A factors require h=w=d.
+The U factor then also equals G(d). Consequently
+
+\[
+N/G(3d)=C_d(0,0;2)G(d)^4. \tag{6}
+\]
+
+At d=4, C_4(0,0;2)=5824. The sharp and identity-pivot split-pair counts from
+(5) are respectively
+
+```text
+962018618785136640000
+8291457123053721102581760
+```
+
+Each becomes a complete-header count after multiplication by G(12).
+These are formula evaluations, not a literal census of GL_16(F2).

research/schur-rank-pair-law/README.md

@@ -0,0 +1,136 @@
+# Exact rank-pair multiplicities for Schur-header counting
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped counting proof with exact finite corroboration. For every
+finite field F_q, [PROOF.md](PROOF.md) gives a double-sum formula for the number
+of d-by-d matrices H with prescribed nullities of H and I-H. It preserves their
+dependence and replaces the 2^(d*d)-matrix sum in **ssafwann's #4678** binary
+sharp Schur-header law with polynomially many explicit arithmetic summands.
+The inclusion-exclusion method is classical. No historical novelty claim is
+made for finite-field enumeration beyond this repository.
+
+The new formula is proved by counting two disjoint eigenspaces and their
+super-subspaces, including the graph-lift factors q^(ab) and q^(bi+aj).
+For a fixed nullity pair it has at most (d+1)(d+2)/2 summands. The entire joint
+distribution has O(d^4) summands. This is an algebraic evaluation improvement,
+not a measured runtime speedup. Binary header counting remains conditional
+on the cited predecessor theorem and concerns one deletion only.
+
+At d=4 with four equal dimension-four sectors, the sharp split-pair count is
+**962018618785136640000** and the identity-pivot split-pair count is
+**8291457123053721102581760**. Multiply either by |GL_12(F2)| for its complete
+ordered-header count. These are formula evaluations, not exhaustive counts
+of the GL_16(F2) header space. No new kappa or supplier admission is claimed.
+
+## Evidence and reproduction
+
+From the repository root, use CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/schur-rank-pair-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/schur-rank-pair-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/schur-rank-pair-law
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/schur-rank-pair-law --check-source-history
+```
+
+Any CPython 3.12 interpreter may replace the local path. The standalone verifier
+has no imports from another package and writes no files. Its output includes
+`PASS_SCHUR_RANK_PAIR_LAW` and a generated receipt bound to all six package
+files. The publication check requires full Git history. The verifier also runs
+from a Git-free export containing these six files.
+
+The direct matrix implementation uses ordinary Gaussian elimination, separately
+from the subspace counting formula. Its literal censuses cover all dimensions
+0 through 4 over F2, 0 through 3 over F3, and 0 through 2 over F4 and F5.
+There are **86,727 matrix/context cases in 15 contexts**. F4 is represented by
+F2[t]/(t^2+t+1), so the nonprime-field check uses field operations, not arithmetic
+modulo four. The empty matrix and impossible a+b>d pairs are included.
+
+Fifteen weighted binary header contexts compare the new grouped formula to
+the literal sum over every compressed product at d=1,2,3. They include the
+three numerical examples credited to #4678, with sharp/identity split-pair
+counts (3,172), (9,100) and (2592,1932288). The weighted comparisons share the
+credited U/A factors; they check the new regrouping, not those factor formulas
+or the predecessor's Schur criterion. No predecessor verifier is replayed.
+
+There are also 63 formula-only distribution checks through dimension eight
+over q=2,3,4,5,7,8,9, checking nonnegativity, total mass and shift symmetry.
+These are consistency checks rather than new exhaustive censuses. Eleven
+controls cover omitted disjointness/lift factors, independent marginals,
+the impossible-eigenspace boundary, six malformed inputs and the literal
+census capacity limit. Explicit exceptions keep every check active under -O.
+
+## Scope, sources and obligations
+
+Base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority
+revision 7. The `formal-interface-lemma` card is changed to this algebraic
+side result answering the evaluation gap explicitly stated in #4678. The
+current-priorities selected source-binding command passes; it is metadata
+orientation only. The original card's historical balanced baseline is not the
+selected construction, so the current source-bound first step is used.
+
+Advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132030)
+was posted after a local question reservation, live PR/body and Discussion
+checks, and distinctive main/merged searches. The overlap helper covered 325
+open PRs and 3,742 Discussion records with complete pagination. Its sparse
+local inventory searched 72 of 6,319 tracked notes; relevant source notes were
+then materialized and all-main README searches were performed. Arbitrary code
+diffs, unpublished work and a complete closed-PR body census are outside that
+coverage. No absence-of-matches claim proves novelty.
+
+The proof of the joint distribution is self-contained. The binary header
+application cites ssafwann's #4678 at
+`af9cf805c501e4e9e947c98c0b97b2281b6b6e97`, including its U/A factors and
+complete-header completion multiplicity. Its unchanged archived README and
+the catalogue/selected record are source-hashed provenance, not runtime inputs.
+The new implementation transcribes the credited displayed U/A formulas; no
+predecessor source code is copied. Exact Git blobs and hashes are in SOURCES.json.
+
+Credit ssafwann #4678/#4671/#4657 for the header theorem, six-map method and
+sector construction, Nick Petalas #4597/#4278 and the earlier header lineage
+for Schur factorizations, Ryanson Jonathan #4609/#4617 and lee-phys #4634 for
+sharpness/dimension context, and Cinna Davis for the BIT setting. source527,
+commdata2338 and Jose Manuel retain the normalizer lineage credit. All existing
+predecessor notices remain unchanged.
+
+The universal claims rest on the written proof. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and the selected scientific
+cold replay were not run. Later full guards and noncommuting residual states
+are outside this result. Restricted production covers, selection/emission,
+physical reads, dirty compensation/restoration, dispatch, precision, stock and
+the complete consumer bill remain unknown. Unknown costs are not zero.
+
+## Code bounds and diagnostics
+
+Only the new verifier is executed. It has no recursion, subprocesses, network,
+mutation of shared state, dynamic code or callback registration. Formula entry
+points enforce d<=32 and prime-power q<=64; sectors have size at most 64.
+The direct census enforces q^(d*d)<=65536. Each matrix is processed once and
+discarded; the histogram has at most 25 entries. The larger formula histogram
+has at most 1,089 entries. All calls are direct and returned values are consumed.
+Functions stay below 60 physical lines. Warnings are errors in both registered
+commands; repository metadata and publication-byte checks also run. No external
+static analyzer is installed or claimed.
+
+Power of Ten rule 3 deviation: CPython allocates integers, tuples and dictionaries
+during arithmetic and elimination. Fixed preallocation cannot prevent those
+runtime allocations. Live memory is bounded by the enforced dimensions, one
+current matrix, one histogram and bounded-size integer sums. No matrix list or
+unbounded cache is retained. Ordinary and optimized full replays exercise these
+bounds. A larger executable domain would require a new capacity review; this
+deviation does not weaken the all-d mathematical formula.
+
+## Open next questions
+
+Can joint nullities at three distinct affine shifts be counted without matrix
+enumeration? Equal-scalar nonbinary Schur pivots can require more than two
+different shifted ranks, so the present two-eigenspace law is insufficient.
+Begin by counting prescribed three eigenspaces and their super-subspace lifts.
+The blocker is an exact multiple-shift dependency formula, not extra binary
+samples. This question is unclaimed here.
+
+Can a named producer use these exact counts to supply a smaller paid header
+cover? Begin with its actual request ensemble and selection/emission contract.
+The complete physical bill remains the blocker; a positive density alone does
+not remove paid work.

research/schur-rank-pair-law/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/schur-header-count/README.md",
+      "usage": "provenance",
+      "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2",
+      "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e"
+    }
+  ]
+}