diff --git a/research/corankone-pair-header-law/PROOF.md b/research/corankone-pair-header-law/PROOF.md new file mode 100644 index 0000000000..2493784dba --- /dev/null +++ b/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. diff --git a/research/corankone-pair-header-law/README.md b/research/corankone-pair-header-law/README.md new file mode 100644 index 0000000000..743cf79ee8 --- /dev/null +++ b/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. diff --git a/research/corankone-pair-header-law/SOURCES.json b/research/corankone-pair-header-law/SOURCES.json new file mode 100644 index 0000000000..2f77740924 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/corankone-pair-header-law/TASK.json b/research/corankone-pair-header-law/TASK.json new file mode 100644 index 0000000000..5d12aab7cd --- /dev/null +++ b/research/corankone-pair-header-law/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact simultaneous full-leading-minor header density for commuting corank-one P=I-U,Q=I-V with orthogonal rank-one kernels over finite fields. General finite-state transfer law and a binary all-dimension closed form with strict negative correlation.", + "scope_change_reason": "This is original counting work answering a concrete subcase of the nonorthogonal full-guard question in PR4240 and PR4246, rather than an independent audit of PR4100. It changes the card premise and is a side result, not supplier admission.", + "bottleneck_link": "Shared-header pricing needs joint guard laws, not products of marginal probabilities. The exact count specifies one overlapping-image case; physical caller costs and a real producer remain unknown, so kappa is unchanged.", + "budget_minutes": 60, + "stop_rule": "Prove the transfer reduction and binary formula, compare both with complete small header and normalized-pair censuses, then stop without expanding into a physical caller.", + "outcome": "completed", + "evidence": "PROOF.md gives the general transfer theorem and binary closed form. verify.py enumerates all normalized pairs in 12 finite domains and all complete GL headers in seven domains, with independent literal no-pivot elimination, 99 transfer cases and four controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the transfer law be reduced to a closed form or a smaller invariant state space for odd q?", + "why_it_matters": "Odd fields lie in the retained executable normalizer domain, and a compact formula would expose the exact dependence there.", + "first_step": "Diagonalize or quotient the q=3 transfer matrix while preserving both diagonal guard values and the rank of I-A.", + "blocked_by": "No invariant-state lumping is proved here." + }, + { + "question": "What is the joint full-guard law for more than two corank-one requests with pairwise orthogonal rank-one kernels?", + "why_it_matters": "It would determine whether a shared header can serve a larger overlapping family.", + "first_step": "Replace the 2 by 2 partial Gram matrix by a 3 by 3 matrix for q=2 and m=3,4.", + "blocked_by": "The binary four-state simplification no longer applies." + }, + { + "question": "Does an actual odd-field request producer admit a fully charged shared-header caller?", + "why_it_matters": "A joint density is not a physical saving.", + "first_step": "Pin a producer with orthogonal kernel lines and charge header selection, emission, dispatch, dirty return and stock.", + "blocked_by": "No producer or complete physical invoice is supplied." + } + ] +} diff --git a/research/corankone-pair-header-law/VERIFY.json b/research/corankone-pair-header-law/VERIFY.json new file mode 100644 index 0000000000..ac4f853223 --- /dev/null +++ b/research/corankone-pair-header-law/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/BIT.md", + "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact transfer law, complete normalized-pair and GL-header censuses, full pivot guards, boundary specializations, controls and source hashes; read-only." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under optimized Python, using explicit need() checks." + } + ] +} diff --git a/research/corankone-pair-header-law/verify.py b/research/corankone-pair-header-law/verify.py new file mode 100644 index 0000000000..8127de43fc --- /dev/null +++ b/research/corankone-pair-header-law/verify.py @@ -0,0 +1,353 @@ +"""Exact overlapping corank-one header counts; standard library, read-only.""" + +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b, q): + return a ^ b if q == 4 else (a + b) % q + + +def neg(a, q): + return a if q == 4 else -a % q + + +def mul(a, b, q): + if q != 4: + return a * b % q + value = 0 + for _ in range(2): + if b & 1: + value ^= a + b >>= 1 + a <<= 1 + if a & 4: + a ^= 7 + return value + + +def dot(a, b, q): + value = 0 + for x, y in zip(a, b, strict=True): + value = add(value, mul(x, y, q), q) + return value + + +def binary_count(m): + need(2 <= m <= 64, "binary dimension outside bounded replay domain") + n = m - 1 + numerator = 9**n - 2 * 7**n + 5**n + need(numerator >= 0 and numerator % 4 == 0, "integral nonnegative count") + return numerator // 4 + + +def pair_total(q, m): + return (q**m - 1) * (q**m - q) * q ** (2 * m - 4) + + +def rank_weight(a, q): + if not any(a): + return 2 * q * q - 1 + determinant = add(mul(a[0], a[3], q), neg(mul(a[1], a[2], q), q), q) + return 0 if determinant else q - 1 + + +def transfer_counts(q, maximum): + need(q in (2, 3, 4, 5, 7) and 2 <= maximum <= 64, "transfer domain") + states = [ + a for a in itertools.product(range(q), repeat=4) if a[0] != 1 and a[3] != 1 + ] + increments = [ + (a, rank_weight(a, q)) + for a in itertools.product(range(q), repeat=4) + if rank_weight(a, q) + ] + index = {a: i for i, a in enumerate(states)} + transitions = [[] for _ in states] + for i, a in enumerate(states): + for b, weight in increments: + target = tuple(add(x, y, q) for x, y in zip(a, b, strict=True)) + if target in index: + transitions[i].append((index[target], weight)) + final = [ + rank_weight( + ( + add(1, neg(a[0], q), q), + neg(a[1], q), + neg(a[2], q), + add(1, neg(a[3], q), q), + ), + q, + ) + for a in states + ] + current = [0] * len(states) + current[index[(0, 0, 0, 0)]] = 1 + result = {} + for length in range(1, maximum): + following = [0] * len(states) + for i, count in enumerate(current): + for target, weight in transitions[i]: + following[target] += count * weight + current = following + result[length + 1] = sum(x * y for x, y in zip(current, final, strict=True)) + return result + + +def vector_guard(u, a, q): + prefix = 0 + for x, y in zip(u[:-1], a[:-1], strict=True): + prefix = add(prefix, mul(x, y, q), q) + if prefix == 1: + return False + return True + + +def enumerate_pairs(q, m): + """Enumerate X=(u,v), Y=(a;b) directly, imposing YX=I_2.""" + need( + (q, m) + in ( + (2, 2), + (2, 3), + (2, 4), + (2, 5), + (2, 6), + (3, 2), + (3, 3), + (3, 4), + (4, 2), + (4, 3), + (5, 2), + (5, 3), + ), + "pair census domain", + ) + vectors = list(itertools.product(range(q), repeat=m)) + total = good = single = 0 + for u in vectors[1:]: + multiples = {tuple(mul(c, x, q) for x in u) for c in range(q)} + for v in vectors: + if v in multiples: + continue + left = [] + right = [] + for a in vectors: + values = (dot(a, u, q), dot(a, v, q)) + if values == (1, 0): + left.append(vector_guard(u, a, q)) + elif values == (0, 1): + right.append(vector_guard(v, a, q)) + need(len(left) == len(right) == q ** (m - 2), "left inverse fibers") + # Every combination is explicitly visited, including failed pairs. + for first in left: + for second in right: + total += 1 + single += first + good += first and second + need(total == pair_total(q, m), "complete normalized-pair count") + return total, good, single + + +def inverse(a, q): + n = len(a) + rows = [list(row) + [int(i == j) for j in range(n)] for i, row in enumerate(a)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i][j]), None) + if pivot is None: + return None + rows[j], rows[pivot] = rows[pivot], rows[j] + unit = next(c for c in range(1, q) if mul(rows[j][j], c, q) == 1) + rows[j] = [mul(unit, x, q) for x in rows[j]] + for i in range(n): + if i != j: + factor = neg(rows[i][j], q) + rows[i] = [ + add(x, mul(factor, y, q), q) + for x, y in zip(rows[i], rows[j], strict=True) + ] + need( + all(rows[i][j] == int(i == j) for i in range(n) for j in range(n)), + "inverse endpoint", + ) + return [row[n:] for row in rows] + + +def full_guard(a, q): + """Literal no-pivot Gaussian guard test through rank m-1.""" + rows = [list(row) for row in a] + n = len(rows) + for j in range(n - 1): + pivot = rows[j][j] + if not pivot: + return False + unit = next(c for c in range(1, q) if mul(pivot, c, q) == 1) + for i in range(j + 1, n): + factor = neg(mul(rows[i][j], unit, q), q) + for k in range(j, n): + rows[i][k] = add(rows[i][k], mul(factor, rows[j][k], q), q) + return True + + +def conjugate_complement(g, gi, axis, q): + return [ + [ + add(int(i == j), neg(mul(g[i][axis], gi[axis][j], q), q), q) + for j in range(len(g)) + ] + for i in range(len(g)) + ] + + +def enumerate_headers(q, m): + need( + (q, m) in ((2, 2), (2, 3), (2, 4), (3, 2), (3, 3), (4, 2), (5, 2)), + "header census domain", + ) + total = good = single = first_only = 0 + fibers = {} + for entries in itertools.product(range(q), repeat=m * m): + g = [entries[i * m : (i + 1) * m] for i in range(m)] + gi = inverse(g, q) + if gi is None: + continue + total += 1 + p = conjugate_complement(g, gi, 0, q) + r = conjugate_complement(g, gi, 1, q) + first, second = full_guard(p, q), full_guard(r, q) + good += first and second + single += first + first_only += bool(p[0][0] and r[0][0]) + for axis, matrix in enumerate((p, r)): + u = [row[axis] for row in g] + need( + full_guard(matrix, q) == vector_guard(u, gi[axis], q), + "literal elimination versus scalar prefix guards", + ) + key = tuple(row[k] for row in g for k in (0, 1)) + tuple(gi[0] + gi[1]) + fibers[key] = fibers.get(key, 0) + 1 + gl = 1 + for i in range(m): + gl *= q**m - q**i + need(total == gl, "complete GL domain") + need(len(fibers) == pair_total(q, m), "all normalized pairs reached") + need(set(fibers.values()) == {gl // pair_total(q, m)}, "equal conjugation fibers") + return total, good, single, first_only + + +def check_formula_and_controls(tables): + for m, count in tables[2].items(): + need(count == binary_count(m), "binary closed form versus transfer") + joint = Fraction(count, pair_total(2, m)) + single = Fraction(3 ** (m - 1), (2**m - 1) * 2 ** (m - 1)) + need(joint < single * single, "strict negative correlation") + need((count > 0) == (m >= 3), "exact binary existence threshold") + # Directly enumerate local factorizations, independent of rank weights. + for q in tables: + counts = {} + for a, b, c, d in itertools.product(range(q), repeat=4): + matrix = (mul(a, c, q), mul(a, d, q), mul(b, c, q), mul(b, d, q)) + counts[matrix] = counts.get(matrix, 0) + 1 + for matrix in itertools.product(range(q), repeat=4): + need( + counts.get(matrix, 0) == rank_weight(matrix, q), "local factor weights" + ) + controls = [ + ( + Fraction(binary_count(3), pair_total(2, 3)) != Fraction(9, 28) ** 2, + "independence product", + ), + (binary_count(4) != (8**3 - 2 * 6**3 + 4**3) // 4, "lost zero factor"), + (binary_count(3) != (9**2 + 2 * 7**2 + 5**2) // 4, "even parity target"), + ] + for condition, label in controls: + need(condition, "failed control: " + label) + return len(controls) + + +def check_sources(package, root): + sources = json.loads((package / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + actual = hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() + need(actual == row["sha256"], "source hash mismatch: " + row["path"]) + + +def emit_receipt(package, root, result): + manifest = json.loads((package / "VERIFY.json").read_text()) + paths = sorted([p for p in package.iterdir() if p.is_file()]) + paths += [root / name for name in manifest["inputs"]] + result["sha256"] = { + str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in paths + } + print("PASS_CORANKONE_PAIR_HEADER_LAW " + json.dumps(result, sort_keys=True)) + + +def main(): + package = Path(__file__).resolve().parent + root = package.parent.parent + check_sources(package, root) + tables = {q: transfer_counts(q, 64 if q == 2 else 10) for q in (2, 3, 4, 5, 7)} + pair_cases = ( + (2, 2), + (2, 3), + (2, 4), + (2, 5), + (2, 6), + (3, 2), + (3, 3), + (3, 4), + (4, 2), + (4, 3), + (5, 2), + (5, 3), + ) + header_cases = ((2, 2), (2, 3), (2, 4), (3, 2), (3, 3), (4, 2), (5, 2)) + pair_results = {} + for q, m in pair_cases: + total, good, single = enumerate_pairs(q, m) + need(good == tables[q][m], "direct pair census versus transfer") + marginal = Fraction( + (q * q - q + 1) ** (m - 1) * (q - 1), q ** (m - 1) * (q**m - 1) + ) + need(Fraction(single, total) == marginal, "single-request specialization") + pair_results[f"{q},{m}"] = [total, good, single] + header_results = {} + for q, m in header_cases: + total, good, single, first_only = enumerate_headers(q, m) + need( + Fraction(good, total) == Fraction(tables[q][m], pair_total(q, m)), + "literal header census versus transfer", + ) + header_results[f"{q},{m}"] = [total, good, single, first_only] + need( + header_results["2,3"][1] != header_results["2,3"][3], + "first-pivot-only control must differ", + ) + controls = check_formula_and_controls(tables) + 1 + for q, table in tables.items(): + need( + Fraction(table[2], pair_total(q, 2)) + == Fraction((q - 1) * (q - 2), q * (q + 1)), + "rank-one pair boundary", + ) + result = { + "pairs": pair_results, + "headers": header_results, + "transfer_cases": sum(len(t) for t in tables.values()), + "controls": controls, + } + emit_receipt(package, root, result) + + +if __name__ == "__main__": + main()