From 7fceedc146a3f4dc53e99a304c9e03461af36342 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:19:31 +0100 Subject: [PATCH] feat(research): count shared Schur-product rank pairs exactly --- research/schur-rank-pair-law/PROOF.md | 178 ++++++++++++++++ research/schur-rank-pair-law/README.md | 136 ++++++++++++ research/schur-rank-pair-law/SOURCES.json | 24 +++ research/schur-rank-pair-law/TASK.json | 129 ++++++++++++ research/schur-rank-pair-law/VERIFY.json | 34 +++ research/schur-rank-pair-law/verify.py | 239 ++++++++++++++++++++++ 6 files changed, 740 insertions(+) create mode 100644 research/schur-rank-pair-law/PROOF.md create mode 100644 research/schur-rank-pair-law/README.md create mode 100644 research/schur-rank-pair-law/SOURCES.json create mode 100644 research/schur-rank-pair-law/TASK.json create mode 100644 research/schur-rank-pair-law/VERIFY.json create mode 100644 research/schur-rank-pair-law/verify.py diff --git a/research/schur-rank-pair-law/PROOF.md b/research/schur-rank-pair-law/PROOF.md new file mode 100644 index 0000000000..9673ed6369 --- /dev/null +++ b/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). diff --git a/research/schur-rank-pair-law/README.md b/research/schur-rank-pair-law/README.md new file mode 100644 index 0000000000..f81da1f15c --- /dev/null +++ b/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. diff --git a/research/schur-rank-pair-law/SOURCES.json b/research/schur-rank-pair-law/SOURCES.json new file mode 100644 index 0000000000..9383132f9e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/schur-rank-pair-law/TASK.json b/research/schur-rank-pair-law/TASK.json new file mode 100644 index 0000000000..cf9238b792 --- /dev/null +++ b/research/schur-rank-pair-law/TASK.json @@ -0,0 +1,129 @@ +{ + "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": "An exact finite-field joint-nullity distribution for H and I-H, replacing the exponential compressed-product sum in the cited binary sharp Schur-header theorem by polynomially many explicit summands.", + "scope_change_reason": "The explicit evaluation gap in ssafwann PR4678 motivates a scoped algebraic counting side result, rather than a formalization or predecessor audit.", + "bottleneck_link": "Retains the shared-product rank dependence when evaluating exact one-block header frequencies. Physical implementation and supplier costs remain unknown; no new kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified joint-count formula and its binary substitution; do not extend to more affine shifts or physical header covers.", + "outcome": "completed", + "evidence": "PROOF.md derives the joint law and weighted substitution. verify.py checks 86727 matrices in 15 contexts, 15 weighted sums, 63 distribution consistency contexts, a new d=4 balanced evaluation and 11 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can joint nullities at three distinct affine shifts be counted without matrix enumeration?", + "why_it_matters": "Nonbinary equal-scalar Schur pivots can involve more than two shifted ranks.", + "first_step": "Count prescribed three eigenspaces and their disjoint super-subspace lifts.", + "blocked_by": "A multiple-shift dependency formula; the two-eigenspace law does not supply it." + }, + { + "question": "Can a named physical producer turn these counts into a smaller paid header cover?", + "why_it_matters": "Uniform complete-header density does not imply a physical saving.", + "first_step": "Specify the actual producer ensemble and selection/emission contract.", + "blocked_by": "Physical reads, restoration, stock, dispatch and the complete consumer bill." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132030", + "main_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "overlap": { + "open_prs": 325, + "discussion_records": 3742, + "complete_remote_pagination": true, + "local_notes": 72, + "tracked_notes": 6319 + }, + "limits": "Sparse local inventory; targeted all-main README and merged PR searches supplement it. Arbitrary diffs, unpublished work and a complete closed-body census are not covered.", + "submission_overlap": { + "main_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "open_prs": 326, + "discussion_records": 3754, + "complete_remote_pagination": true, + "local_notes": 76, + "tracked_notes": 6319, + "discussion_refreshed_at": "2026-10-22T20:18:18.963407+00:00", + "limits": "Sparse local notes; all-main distinctive README searches and live merged/open body searches supplement this snapshot. No exhaustive arbitrary-diff or unpublished coverage." + } + }, + "family_decision": { + "decision": "narrow", + "proved": "Joint-nullity formula and polynomial-summand substitution into the credited one-block binary law.", + "unknown": "Production header cover, selection/emission, reads, dirty restoration, stock, dispatch, precision and the complete consumer bill.", + "stop": "No new parameter search or construction expansion." + } +} diff --git a/research/schur-rank-pair-law/VERIFY.json b/research/schur-rank-pair-law/VERIFY.json new file mode 100644 index 0000000000..792729ae12 --- /dev/null +++ b/research/schur-rank-pair-law/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Joint-nullity matrix census, binary weighted substitution, formula consistency, balanced d4 count and eleven controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Identical checks and generated file-bound receipt with optimization enabled." + } + ] +} diff --git a/research/schur-rank-pair-law/verify.py b/research/schur-rank-pair-law/verify.py new file mode 100644 index 0000000000..8af1b3c435 --- /dev/null +++ b/research/schur-rank-pair-law/verify.py @@ -0,0 +1,239 @@ +#!/usr/bin/env python3 +"""Exact joint eigenspace counts and the credited binary Schur-header sum.""" + +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from math import prod +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def validate(n: int, q: int) -> None: + require(type(n) is int and 0 <= n <= 32, "dimension outside 0..32") + require(type(q) is int and 2 <= q <= 64, "field order outside 2..64") + powers = {p**k for p in (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, + 31, 37, 41, 43, 47, 53, 59, 61) + for k in range(1, 7) if p**k <= 64} + require(q in powers, "field order is not a prime power") + + +def gaussian(n: int, k: int, q: int) -> int: + if not 0 <= k <= n: + return 0 + numerator = prod(q**n - q**j for j in range(k)) + denominator = prod(q**k - q**j for j in range(k)) + require(numerator % denominator == 0, "nonintegral Gaussian coefficient") + return numerator // denominator + + +def injections(n: int, k: int, q: int) -> int: + return prod(q**n - q**j for j in range(k)) if 0 <= k <= n else 0 + + +def joint_count(n: int, a: int, b: int, q: int) -> int: + """Count H with nullity H=a and nullity(I-H)=b.""" + validate(n, q) + require(type(a) is int and type(b) is int and 0 <= a <= n + and 0 <= b <= n, "invalid nullities") + t = n - a - b + if t < 0: + return 0 + total = 0 + for i in range(t + 1): + for j in range(t - i + 1): + exponent = (i * (i - 1) // 2 + j * (j - 1) // 2 + + i * j + b * i + a * j + n * (t - i - j)) + total += ((-1)**(i + j) * q**exponent + * gaussian(t, i, q) * gaussian(t - i, j, q)) + count = gaussian(n, a, q) * gaussian(n - a, b, q) * q**(a * b) * total + require(count >= 0, "negative joint count") + return count + + +def distribution(n: int, q: int) -> dict[tuple[int, int], int]: + validate(n, q) + counts = {(a, b): joint_count(n, a, b, q) + for a in range(n + 1) for b in range(n + 1)} + require(sum(counts.values()) == q**(n * n), "wrong total matrix count") + require(all(counts[a, b] == counts[b, a] for a, b in counts), + "H -> I-H symmetry failed") + return counts + + +def add(x: int, y: int, q: int) -> int: + return x ^ y if q == 4 else (x + y) % q + + +def multiply(x: int, y: int, q: int) -> int: + if q != 4: + return x * y % q + value = (x if y & 1 else 0) ^ (x << 1 if y & 2 else 0) + return value ^ 7 if value & 4 else value + + +def rank(entries: tuple[int, ...], n: int, q: int) -> int: + rows = [list(entries[n * i:n * (i + 1)]) for i in range(n)] + r = 0 + for col in range(n): + pivot = next((i for i in range(r, n) if rows[i][col]), None) + if pivot is None: + continue + rows[r], rows[pivot] = rows[pivot], rows[r] + inverse = next(x for x in range(1, q) + if multiply(rows[r][col], x, q) == 1) + rows[r] = [multiply(x, inverse, q) for x in rows[r]] + for i in range(r + 1, n): + coefficient = rows[i][col] + for j in range(col, n): + value = multiply(coefficient, rows[r][j], q) + negative = value if q == 4 else -value + rows[i][j] = add(rows[i][j], negative, q) + r += 1 + return r + + +def enumerate_matrices(n: int, q: int) -> Counter: + require(q in (2, 3, 4, 5) and 0 <= n <= 4 + and q**(n * n) <= 65536, "literal census exceeds capacity") + counts = Counter() + for entries in product(range(q), repeat=n * n): + shifted = tuple(add(int(i == j), entries[n * i + j] + if q in (2, 4) else -entries[n * i + j], q) + for i in range(n) for j in range(n)) + counts[n - rank(entries, n, q), n - rank(shifted, n, q)] += 1 + require(sum(counts.values()) == q**(n * n), "incomplete literal census") + return counts + + +def factor_count(r: int, d: int, rho: int, full: bool) -> int: + """U/A from ssafwann #4678, equations (1)-(2), at q=2.""" + if full: + if r < d: + return 0 + return (injections(r, d, 2) * 2**(rho * (r - d)) + * injections(r - d, d - rho, 2)) + return sum(gaussian(d - rho, d - k, 2) * injections(r, k, 2) + * 2**(d * (r - k)) for k in range(rho, min(d, r) + 1)) + + +def header_split_counts(sectors: tuple[int, ...], d: int) -> tuple[int, int]: + require(len(sectors) == 4 and all(type(r) is int and 0 <= r <= 64 + for r in sectors), "invalid sectors") + require(type(d) is int and 1 <= d <= 32 and d <= sum(sectors), + "invalid block dimension") + sharp, admitted = 0, 0 + for (a, b), multiplicity in distribution(d, 2).items(): + h, w = d - a, d - b + ranks = (w, w, w, h) + sharp += multiplicity * prod(factor_count(r, d, rho, j != 0) + for j, (r, rho) in enumerate(zip(sectors, ranks, strict=True))) + admitted += multiplicity * prod(factor_count(r, d, rho, False) + for r, rho in zip(sectors, ranks, strict=True)) + require(0 <= sharp <= admitted, "header counts are inconsistent") + return sharp, admitted + + +def literal_header_sum(sectors: tuple[int, ...], d: int) -> tuple[int, int]: + require(1 <= d <= 3, "literal compressed-product sum exceeds capacity") + sharp, admitted = 0, 0 + for entries in product(range(2), repeat=d * d): + shifted = tuple(entries[d * i + j] ^ int(i == j) + for i in range(d) for j in range(d)) + h, w = rank(entries, d, 2), rank(shifted, d, 2) + ranks = (w, w, w, h) + sharp += prod(factor_count(r, d, rho, j != 0) + for j, (r, rho) in enumerate(zip(sectors, ranks, strict=True))) + admitted += prod(factor_count(r, d, rho, False) + for r, rho in zip(sectors, ranks, strict=True)) + return sharp, admitted + + +def check_censuses() -> tuple[int, int]: + cases, contexts = 0, 0 + for q, maximum in ((2, 4), (3, 3), (4, 2), (5, 2)): + for n in range(maximum + 1): + literal = enumerate_matrices(n, q) + exact = distribution(n, q) + require(all(literal[key] == value for key, value in exact.items()), + f"joint law disagrees with matrices at {(q, n)}") + cases += sum(literal.values()) + contexts += 1 + return cases, contexts + + +def check_headers() -> int: + contexts = 0 + for d in (1, 2, 3): + for sectors in ((d, d, d, d), (0, d, d, 2 * d), + (d, d + 1, d, d + 1), (1, 1, 1, 2), (0, 2, 2, 1)): + require(header_split_counts(sectors, d) == literal_header_sum(sectors, d), + "grouped and literal weighted sums disagree") + contexts += 1 + require(header_split_counts((1, 1, 1, 2), 1) == (3, 172), "first credited example") + require(header_split_counts((0, 2, 2, 1), 1) == (9, 100), "second credited example") + require(header_split_counts((2, 2, 2, 2), 2) == (2592, 1932288), + "third credited example") + return contexts + + +def check_controls() -> int: + table = distribution(2, 2) + require(table[1, 1] == 6 and table[0, 0] == 2, "binary base fixture") + # Missing q^(ab) and missing super-space lift factors are separate errors. + require(table[1, 1] != gaussian(2, 1, 2), "disjointness control ineffective") + wrong_fixed = sum((-1)**j * 2**(2 * (1 - j)) + * gaussian(1, j, 2) for j in range(2)) + require(table[1, 0] != gaussian(2, 1, 2) * wrong_fixed, + "lift-factor control ineffective") + left = sum(v for (a, _), v in table.items() if a == 0) + require(table[0, 0] * 16 != left * left, "independence control ineffective") + require(joint_count(2, 2, 1, 2) == 0, "disjoint eigenspace boundary failed") + rejected = 0 + for n, a, b, q in ((-1, 0, 0, 2), (33, 0, 0, 2), (2, -1, 0, 2), + (2, 0, 3, 2), (2, 0, 0, 6), (2, 0, 0, 1)): + try: + joint_count(n, a, b, q) + except ValueError: + rejected += 1 + require(rejected == 6, "an invalid input was accepted") + try: + enumerate_matrices(4, 3) + except ValueError: + return 11 + raise ValueError("literal capacity guard did not reject") + + +def main() -> None: + cases, contexts = check_censuses() + headers = check_headers() + controls = check_controls() + larger = 0 + for q in (2, 3, 4, 5, 7, 8, 9): + for n in range(9): + _ = distribution(n, q) # Check invariants; discard the bounded histogram. + larger += 1 + sharp, admitted = header_split_counts((4, 4, 4, 4), 4) + derangements = joint_count(4, 0, 0, 2) + require(derangements == 5824, "binary dimension-four derangement count") + require(sharp == 5824 * injections(4, 4, 2)**4, "balanced-sector identity") + package = Path(__file__).resolve().parent + files = ("README.md", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + receipt = {"matrix_cases": cases, "matrix_contexts": contexts, + "weighted_header_contexts": headers, "controls": controls, + "larger_distribution_contexts": larger, + "balanced_d4_sharp_split_pairs": sharp, + "balanced_d4_identity_split_pairs": admitted, + "source_sha256": {name: sha256((package / name).read_bytes()).hexdigest() + for name in files}} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_SCHUR_RANK_PAIR_LAW no_new_kappa") + + +if __name__ == "__main__": + main()