diff --git a/research/oneway-corankone-header-law/PROOF.md b/research/oneway-corankone-header-law/PROOF.md new file mode 100644 index 000000000..5361c339b --- /dev/null +++ b/research/oneway-corankone-header-law/PROOF.md @@ -0,0 +1,127 @@ +# One-way coupled corank-one requests + +## Contract + +Let K be a finite field of order q and m>=2. Let U,V be rank-one +idempotents on K^m with UV nonzero and VU=0. Put P=I-U and Q=I-V. +A header G in GL_m(K) passes R when every leading principal minor of +GRG^-1 of orders 1 through rank(R) is nonzero. Headers have equal weight. +Both requests have rank m-1 and use the same complete header. + +The claim is a scoped counting proof. It extends the partial-Gram method +of Nick Petalas's #4261 from orthogonal kernels to one-way coupled kernels. +The noncommuting requests are outside its hypotheses and outside #4259's +laminar-family theorem. No physical implementation or new kappa follows. + +## All-field transfer theorem + +Write B=[[1,1],[0,1]]. Define, for 2 by 2 matrices A, + +```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)(A) = sum_(T in S) f_j(T) w(A-T), for A in S. +C(q,m) = sum_(A in S) f_(m-1)(A) w(B-A). +D(q,m) = (q^m-1)(q^m-q) q^(2m-4). +``` + +**Theorem.** The joint passing fraction is C(q,m)/D(q,m). There are +C(q,m)|GL_(m-2)(K)| passing headers, with |GL_0(K)|=1. The transfer has +q^2(q-1)^2 states and applies to every finite field. + +**Proof.** Write U=u a and V=v b with a(u)=b(v)=1. The assumptions give +b(u)=0 and a(v)!=0. Rescale v and b inversely so that a(v)=1. Then +X_0=(u,v) and Y_0=(a;b) satisfy Y_0 X_0=B. Both have rank two since B +is invertible. Choose an ordered basis of ker(Y_0) after u,v. In this +basis U=e_1(e_1^T+e_2^T), V=e_2 e_2^T and Y_0=[B 0]. This change of +fixed basis permutes the header domain, preserving the fraction. + +For a header G, put X=G X_0 and Y=Y_0 G^-1. Then YX=B and the +conjugated kernels are the first column of X times the first row of Y, +and the second column times the second row. Conversely, given X,Y with +YX=B, choose the remaining columns of G as any ordered basis of ker(Y). +This gives an invertible G and YG=[B 0]=Y_0. The fiber has exactly +|GL_(m-2)(K)| elements. There are (q^m-1)(q^m-q) full-rank X, and each +of the two rows of Y has q^(m-2) solutions to its two equations. Thus +there are D(q,m) pairs, with equal fibers. + +For a column x and row y, multilinearity of the determinant gives + +```text +det((I-xy)[1..j,1..j]) = 1 - sum_(i=1)^j y_i x_i. +``` + +Terms choosing the rank-one part from two columns vanish. This is the +corank-one guard reduction of #4227. If x_i is row i of X and y_i is +column i of Y, the two diagonal entries of A_j=sum_(i<=j) y_i x_i are +exactly the two guard prefix sums. Hence A_j must lie in S for 1<=j=2, + +```text +C(2,m) = (9^n - 5^n)/4, +Pr(P and Q pass) = (9^(m-1)-5^(m-1)) + / [4(2^m-1)(2^m-2)2^(2m-4)]. +``` + +**Proof.** Safe states over F2 have zero diagonal and are indexed by their +two off-diagonal bits. Safe increments are zero with weight seven, E_12 +with weight one and E_21 with weight one. The final increment B-A has +both diagonal entries one. Its determinant vanishes exactly when +(1+A_12)A_21=1, so only A_12=0,A_21=1 contributes, with weight one. + +The length-n walk on F2^2 therefore ends at (0,1). The four character +eigenvalues of its transition operator are 9,7,7,5. Character inversion +at (0,1) gives (9^n+7^n-7^n-5^n)/4. This proves the formula, including +integrality. A walk with one E_21 and n-1 zero increments proves positivity +for every m>=2. For m=2,3,4,5,6 the fractions are respectively +1/6, 1/12, 151/3360, 371/14880 and 451/32256. + +## Comparison and correlation + +The orthogonal-kernel count in #4261 is +C_orth=(9^n-2*7^n+5^n)/4. The new one-way count exceeds it by +(7^n-5^n)/2>0 for every m>=2, with the same denominator D(2,m). +Thus one-way coupling creates passing headers even at m=2, where the +orthogonal pair has none. This is a count improvement, without a priced +caller or a primitive-saving claim. + +The two passing events remain strictly negatively correlated. The marginal +law from #4227 is s_m=3^n/[(2^m-1)2^n]. Directly, each of the first n +coordinate products must be zero, with three choices each; the last must +be one. The normalized rank-one denominator is (2^m-1)2^n. Therefore + +```text +joint / s_m^2 = (2^(n+1)-1)/(2^(n+1)-2) * [1-(5/9)^n] < 1. +``` + +The inequality is equivalent to (2^(n+1)-1)5^n>9^n. It holds at n=1; +the left-to-right ratio increases at each step since +5(2^(n+2)-1)>9(2^(n+1)-1). The joint density is asymptotic to +(1/4)(9/16)^n and its ratio to s_m^2 tends to one from below. These +conclusions use the complete equally weighted header domain. + +## Scope + +The theorem covers one-way coupled rank-one kernels over finite fields. +Pairs with both UV and VU nonzero, coincident images or covectors, restricted +header subsets, and finite local rings are outside scope. The all-field +result is a recurrence; only F2 has a closed form here. Written mathematics +is the universal evidence. The executable census covers only its declared +finite domains. Binary guards extend beyond the retained normalizer's +odd-prime executable domain. Even for odd fields, a request producer, +header selection/emission, dispatch, dirty return, stock and full physical +invoice remain unknown. No multiplication theorem or supplier is admitted. diff --git a/research/oneway-corankone-header-law/README.md b/research/oneway-corankone-header-law/README.md new file mode 100644 index 000000000..7f04085df --- /dev/null +++ b/research/oneway-corankone-header-law/README.md @@ -0,0 +1,154 @@ +# Exact full-guard law for a one-way coupled pair + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: **scoped counting proof with finite corroboration**. Let U,V +be rank-one idempotents over F_q^m with UV nonzero and VU=0. Both +corank-one requests P=I-U and Q=I-V use one equally weighted complete +GL_m header. A request passes when every leading principal minor through +its rank is nonzero. These requests do not commute. + +[PROOF.md](PROOF.md) proves an exact all-field transfer with +q^2(q-1)^2 states. Over F2, for every m>=2, its closed form is + +```text +Pr(P and Q pass) = (9^(m-1)-5^(m-1)) + / [4(2^m-1)(2^m-2)2^(2m-4)]. +``` + +The fractions at m=2,3,4 are 1/6, 1/12 and 151/3360. This strictly +exceeds the orthogonal-kernel density of +[#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261) in every +dimension, by (7^(m-1)-5^(m-1))/(2D), with +D=(2^m-1)(2^m-2)2^(2m-4). Both passing events are still strictly +negatively correlated. Their joint fraction is asymptotic to +(1/4)(9/16)^(m-1); its ratio to the product of marginals tends to one. + +The changed premise is one-way coupling of the kernel projectors. This +answers a higher-rank subcase of the nonorthogonal full-guard question in +[#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240). +The new step normalizes the partial-Gram endpoint to [[1,1],[0,1]] and +extracts the changed binary walk endpoint. It is original counting work, +not an audit of the cited packages. No new kappa or supplier admission. + +## 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/oneway-corankone-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-corankone-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-corankone-header-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-corankone-header-law --check-source-history +``` + +The scientific marker is `PASS_ONEWAY_CORANKONE_HEADER_LAW`. Its generated +stdout JSON records each exact count and SHA256 bindings for every package +file and both live inputs. No stored or handwritten receipt is used. The +verifier authenticates inputs before enumeration and writes no files. + +The complete bounded replay checks: + +- **32,094 complete GL headers** over F2 at m=2,3,4; F3 at m=2,3; + and F5 at m=2. Generic matrix conjugation and literal no-pivot + elimination test both full guard chains. Every normalized-pair fiber + is counted and checked to have the same size. +- **1,946,574 normalized pairs X,Y with YX=[[1,1],[0,1]]**, separately + enumerated over F2 at m=2..6, F3 at m=2..4 and F5 at m=2,3. Every + joint fraction matches the transfer and every marginal matches the + cited #4227/#4228 corank-one formula. +- **84 transfer cases**, over F2 at m=2..64 and F3,F5,F7 at m=2..8. + All 63 binary counts match the closed form and strict gain/correlation + identities. Rank-one factor multiplicities are independently enumerated + over all four fields. +- Five controls distinguish the orthogonal endpoint, wrong binary parity, + a lost zero-factor multiplicity, independent marginals and first-pivot-only + admission. At q=2,m=3, first-only admission accepts 66 headers while + full admission accepts 14, out of 168. + +Both normal and optimized Python execute explicit checks, so `-O` does not +remove them. The finite counts corroborate the written all-parameter proof. + +## Scope and remaining obligations + +The transfer applies to every finite field. Executed arithmetic uses only +F2,F3,F5,F7; extension-field execution is unrun. Only F2 has a closed form +here. The theorem requires fixed one-way coupled kernels and complete, +equally weighted headers. It says nothing about arbitrary restricted covers, +local rings, coincident image/kernel types or pairs with both products nonzero. + +Binary guards extend beyond the retained normalizer's odd-prime executable +domain. Even in odd characteristic, no real producer, header selection or +emission, dispatch, dirty return, stock, precision or complete physical invoice +is supplied. Those costs are unknown. No selected cold replay, GL64 scan, +Lean or Docker run was performed. No complete multiplication theorem is +claimed. Independent human and formal proof-kernel review are unclaimed. + +The executable loops have bounded domains, with no recursion. The largest +transfer has 1,764 states and at most 679,140 candidate transitions; each +normalized census uses at most 125 vectors, at most 125^2 candidate X +choices and at most 125 candidate rows per X. Accepted row-fiber pairs +have at most 16^2 combinations. Direct GL censuses visit at most 65,536 +candidate matrices, of dimension at most four; factor vectors have length +at most six. +CPython's dynamic integers and containers are a managed-runtime deviation +from fixed allocation, constrained here by these explicit finite domains. +All functions stay below 60 lines. Registered diagnostics use warnings as +errors in normal and optimized modes. No standalone Ruff executable was +available; local AST inspection checks syntax and function sizes. + +## Related open work and credit + +- [#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261), head + `4728fc766b3084f3ab2f5c8543a5e74e4a12b126`, supplies the orthogonal-kernel + partial-Gram method. The new numerator is strictly larger in all 63 binary + replay dimensions. Its m=3 density 1/84 differs from the new 1/12, as the + changed premise predicts; no same-type joint number is shared. +- [#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240), head + `9f9c89ed75e9fdae6b6762925b080fb308824858`, supplies the one-sided + rank-one classification. At m=2 our requests have that type. Its joint + fractions for q=2,3,5,7 agree numerically with this transfer, respectively + 1/6, 1/4, 13/30 and 31/56. This adds the full chain at m>2. +- [#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227), head + `3d793eade8de2ba49ec08f8d004c1b2f566a78e6`, supplies the determinant + reduction and marginal law. All ten marginal census fractions agree + numerically; the joint one-way law is new. +- [#4228](https://github.com/CrocSwap/integer-mult-bounds/pull/4228), head + `bb25dcedb5bbbacd3c35359eb6b5488b087bcde6`, supplies all-rank marginal + densities. Its corank-one specialization agrees on those same ten cases; + no intermediate-rank recurrence is imported. +- [#4239](https://github.com/CrocSwap/integer-mult-bounds/pull/4239), head + `5e24dfb5463d540721687d92c369609da5589523`, counts orthogonal rank-one + requests. The one-way requests here share no joint type with that theorem, + including at m=2, so no overlapping joint number is asserted. +- [#4246](https://github.com/CrocSwap/integer-mult-bounds/pull/4246), head + `a2d99d73bf21b39fbb0a9a88917424ff26c2e63c`, counts orthogonal full chains. + Our noncommuting pair is outside that hypothesis; no joint number is shared. +- [#4259](https://github.com/CrocSwap/integer-mult-bounds/pull/4259), head + `2a582d8f66d1900b22ee2cd0062ee5dca94e8f85`, counts laminar full chains. + Our pair is neither contained nor orthogonal; no joint number is shared. +- [#4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) supplies + the BIT request and complete-header context. Its actual caller costs and + multiplication claim are outside this package; no recursive bill is compared. + +All the preceding counting packages were produced by Nick Petalas. Source527, +commdata2338 and Jose Manuel retain the normalizer and recursive-closure +credit. Cinna Davis supplies BIT.md. Chris R / Clear1nsight's #3950 is earlier +deterministic counting context. The proof and enumerators are self-contained; +no unmerged source code or unavailable Git-history object is imported. +SOURCES.json pins the two retained main-branch contract files, base and card. + +## Open next questions + +1. What is the full-guard law when both UV and VU are nonzero? Start with + endpoint [[1,a],[b,1]], separating invertible endpoints from ab=1. + The singular endpoint needs extra image/covector-rank filters to identify + the intended simultaneous-conjugacy orbit. +2. Can an actual odd-field producer use a fully charged one-way shared-header + caller? Pin its kernel lines and charge selection, emission, dispatch, + dirty restoration and stock. No producer or complete invoice is supplied. + +The active ternary orthogonal-pair and three-orthogonal-kernel claims in the +[handoff thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166) +change the field or number of orthogonal kernels. They are separate from this +changed-coupling question. [TASK.json](TASK.json) records scope and provenance. diff --git a/research/oneway-corankone-header-law/SOURCES.json b/research/oneway-corankone-header-law/SOURCES.json new file mode 100644 index 000000000..ffff228e4 --- /dev/null +++ b/research/oneway-corankone-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/selected-bit-recursive-closure/vendor/controlled_normalizer.py", + "usage": "input", + "git_blob": "3e8a72e7ce705c51ff24e9015ccf6463204ff193", + "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77" + }, + { + "path": "research/unconditional-batched-crt/BIT.md", + "usage": "input", + "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa", + "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da" + } + ] +} diff --git a/research/oneway-corankone-header-law/TASK.json b/research/oneway-corankone-header-law/TASK.json new file mode 100644 index 000000000..0f0b53779 --- /dev/null +++ b/research/oneway-corankone-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 full-leading-minor shared-header density for P=I-U,Q=I-V with rank-one idempotents UV nonzero and VU=0 over finite fields. All-field partial-Gram transfer and binary all-dimension closed form.", + "scope_change_reason": "Original counting continuation of PR4240 open question 1, changing the orthogonal-kernel premise of PR4261. This is a side result rather than an audit of PR4100; no predecessor result is reverified as a deliverable.", + "bottleneck_link": "Shared-header rates require a joint full-guard law, rather than products of marginal rates. One-way coupling increases this exact algebraic rate, but no physical producer or paid caller is supplied, so no kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved formula agrees with complete small GL headers and normalized-pair counts; package without extending the family.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-field transfer, binary formula, strict count gain and negative correlation. verify.py checks 32094 headers, 1946574 normalized pairs, 84 transfer cases and five controls, generating a SHA256-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the full-guard law when both UV and VU are nonzero?", + "why_it_matters": "The one-way case changes an orthogonality premise but leaves the other noncommuting types open.", + "first_step": "Fix a 2 by 2 Gram endpoint [[1,a],[b,1]] and distinguish invertible endpoints from the singular ab=1 case.", + "blocked_by": "A singular endpoint does not force X and Y to have rank two; an unfiltered transfer need not count one simultaneous-conjugacy orbit." + }, + { + "question": "Can one actual odd-field request producer use a fully charged one-way shared-header caller?", + "why_it_matters": "The increased algebraic passing fraction is not a physical primitive saving.", + "first_step": "Pin a producer and its two kernel lines; charge selection, emission, dispatch, dirty restoration and stock.", + "blocked_by": "No producer or complete cost invoice is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19085445", + "base_checked": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "coverage": "381 open PR bodies and 3159 Discussion records in the first paginated overlap snapshot; targeted merged-title and main-README searches; no complete historical code-diff search." + } +} diff --git a/research/oneway-corankone-header-law/VERIFY.json b/research/oneway-corankone-header-law/VERIFY.json new file mode 100644 index 000000000..29ea768dc --- /dev/null +++ b/research/oneway-corankone-header-law/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py", + "research/unconditional-batched-crt/BIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete literal GL and normalized-pair censuses, transfer law, binary closed form, correlation, source hashes and five controls; read-only." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same mathematical and source checks under optimized Python, with explicit need() checks." + } + ] +} diff --git a/research/oneway-corankone-header-law/verify.py b/research/oneway-corankone-header-law/verify.py new file mode 100644 index 000000000..7735924e7 --- /dev/null +++ b/research/oneway-corankone-header-law/verify.py @@ -0,0 +1,282 @@ +"""One-way coupled corank-one full guards; bounded, read-only exact checks.""" + +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + + +FIELDS = (2, 3, 5, 7) +PAIR_DOMAINS = ((2, 2), (2, 3), (2, 4), (2, 5), (2, 6), + (3, 2), (3, 3), (3, 4), (5, 2), (5, 3)) +HEADER_DOMAINS = ((2, 2), (2, 3), (2, 4), (3, 2), (3, 3), (5, 2)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def denominator(q, m): + return (q**m - 1) * (q**m - q) * q ** (2 * m - 4) + + +def binary_count(m): + need(2 <= m <= 64, "binary replay dimension") + value = 9 ** (m - 1) - 5 ** (m - 1) + need(value > 0 and value % 4 == 0, "positive integral binary count") + return value // 4 + + +def factor_weight(a, q): + if not any(a): + return 2 * q * q - 1 + return 0 if (a[0] * a[3] - a[1] * a[2]) % q else q - 1 + + +def transfer(q, maximum, endpoint=(1, 1, 0, 1)): + need(q in FIELDS and 2 <= maximum <= 64, "transfer replay domain") + states = [a for a in itertools.product(range(q), repeat=4) + if a[0] != 1 and a[3] != 1] + increments = [(a, factor_weight(a, q)) + for a in itertools.product(range(q), repeat=4) + if factor_weight(a, q)] + index = {a: i for i, a in enumerate(states)} + edges = [[] for _ in states] + for i, a in enumerate(states): + for delta, weight in increments: + b = tuple((x + y) % q for x, y in zip(a, delta, strict=True)) + if b in index: + edges[i].append((index[b], weight)) + final = [factor_weight(tuple((x - y) % q + for x, y in zip(endpoint, a, strict=True)), q) + for a in states] + current = [0] * len(states) + current[index[(0, 0, 0, 0)]] = 1 + counts = {} + for length in range(1, maximum): + following = [0] * len(states) + for i, count in enumerate(current): + for j, weight in edges[i]: + following[j] += count * weight + current = following + counts[length + 1] = sum(x * y for x, y in zip(current, final, strict=True)) + need(len(states) == q * q * (q - 1)**2, "safe-state cardinality") + return counts + + +def local_weights(q): + vectors = list(itertools.product(range(q), repeat=2)) + observed = Counter() + for y in vectors: + for x in vectors: + observed[tuple(a * b % q for a in y for b in x)] += 1 + for a in itertools.product(range(q), repeat=4): + need(observed[a] == factor_weight(a, q), "rank-one factor multiplicity") + return len(vectors)**2 + + +def dot(u, v, q): + return sum(x * y for x, y in zip(u, v, strict=True)) % q + + +def scalar_guard(u, a, q): + total = 0 + for i in range(len(u) - 1): + total = (total + u[i] * a[i]) % q + if total == 1: + return False + return True + + +def enumerate_pairs(q, m): + need((q, m) in PAIR_DOMAINS, "pair census domain") + vectors = list(itertools.product(range(q), repeat=m)) + total = good = single = 0 + for u in vectors[1:]: + multiples = {tuple(c * x % q for x in u) for c in range(q)} + for v in vectors: + if v in multiples: + continue + left, right = [], [] + for row in vectors: + values = (dot(row, u, q), dot(row, v, q)) + if values == (1, 1): + left.append(scalar_guard(u, row, q)) + elif values == (0, 1): + right.append(scalar_guard(v, row, q)) + need(len(left) == len(right) == q ** (m - 2), "YX=B row fibers") + for first in left: + for second in right: + total += 1 + single += first + good += first and second + need(total == denominator(q, m), "exhaustive pair count") + return {"total": total, "joint": good, "single": single} + + +def inverse(matrix, q): + n = len(matrix) + rows = [list(row) + [int(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + 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 = pow(rows[j][j], -1, q) + rows[j] = [unit * x % q for x in rows[j]] + for i in range(n): + if i != j: + c = rows[i][j] + rows[i] = [(x - c * y) % 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 multiply(a, b, q): + n = len(a) + return [[sum(a[i][k] * b[k][j] for k in range(n)) % q + for j in range(n)] for i in range(n)] + + +def full_guard(matrix, q): + """Literal no-pivot elimination, independent of the scalar-prefix test.""" + rows = [list(row) for row in matrix] + n = len(rows) + for j in range(n - 1): + if not rows[j][j]: + return False + unit = pow(rows[j][j], -1, q) + for i in range(j + 1, n): + c = rows[i][j] * unit % q + for k in range(j, n): + rows[i][k] = (rows[i][k] - c * rows[j][k]) % q + return True + + +def canonical_requests(m, q): + identity = [[int(i == j) for j in range(m)] for i in range(m)] + u = [[int(i == 0 and j in (0, 1)) for j in range(m)] for i in range(m)] + v = [[int(i == j == 1) for j in range(m)] for i in range(m)] + need(multiply(u, u, q) == u and multiply(v, v, q) == v, "idempotents") + need(not any(x for row in multiply(v, u, q) for x in row), "VU=0") + need(any(x for row in multiply(u, v, q) for x in row), "UV nonzero") + return [[[(identity[i][j] - kernel[i][j]) % q for j in range(m)] + for i in range(m)] for kernel in (u, v)] + + +def gl_size(q, m): + value = 1 + for i in range(m): + value *= q**m - q**i + return value + + +def enumerate_headers(q, m): + need((q, m) in HEADER_DOMAINS, "header census domain") + requests = canonical_requests(m, q) + fibers = Counter() + total = good = single = first_only = 0 + for flat in itertools.product(range(q), repeat=m * m): + g = [flat[i * m:(i + 1) * m] for i in range(m)] + gi = inverse(g, q) + if gi is None: + continue + transformed = [multiply(multiply(g, r, q), gi, q) for r in requests] + flags = [full_guard(r, q) for r in transformed] + total += 1 + good += all(flags) + single += flags[0] + first_only += all(r[0][0] != 0 for r in transformed) + x = tuple(g[i][j] for i in range(m) for j in range(2)) + y = tuple((gi[0][i] + gi[1][i]) % q for i in range(m)) + tuple(gi[1]) + fibers[x + y] += 1 + need(total == gl_size(q, m), "complete GL domain") + need(len(fibers) == denominator(q, m), "all normalized-pair fibers") + need(set(fibers.values()) == {gl_size(q, m - 2)}, "equal header fibers") + return {"total": total, "joint": good, "single": single, + "first_only": first_only, "fibers": len(fibers)} + + +def check_binary(counts): + for m, count in counts.items(): + n = m - 1 + need(count == binary_count(m), "binary closed form") + orthogonal = (9**n - 2 * 7**n + 5**n) // 4 + need(count - orthogonal == (7**n - 5**n) // 2 > 0, "strict coupling gain") + joint = Fraction(count, denominator(2, m)) + marginal = Fraction(3**n, (2**m - 1) * 2**n) + ratio = Fraction(2**m - 1, 2**m - 2) * (1 - Fraction(5, 9)**n) + need(joint / marginal**2 == ratio < 1, "negative correlation") + return len(counts) + + +def controls(transfers, headers): + good = transfers[2][3] + wrong_orthogonal = (9**2 - 2 * 7**2 + 5**2) // 4 + wrong_parity = (9**2 + 2 * 7**2 + 5**2) // 4 + wrong_zero_weight = (3**2 - (-1)**2) // 4 + need(good not in (wrong_orthogonal, wrong_parity, wrong_zero_weight), + "coupling, parity and zero-weight controls") + marginal = Fraction(9, 28) + need(Fraction(good, denominator(2, 3)) != marginal**2, "independence control") + need(headers['2,3']['first_only'] > headers['2,3']['joint'], + "first-only admission control") + need(Fraction(transfers[2][2], denominator(2, 2)) == Fraction(1, 6), + "one-way m=2 boundary") + return 5 + + +def bindings(package): + root = package.parents[1] + sources = json.loads((package / 'SOURCES.json').read_text()) + result = {} + for row in sources['files']: + if row['usage'] == 'input': + digest = hashlib.sha256((root / row['path']).read_bytes()).hexdigest() + need(digest == row['sha256'], 'source binding: ' + row['path']) + result[row['path']] = digest + for path in sorted(package.iterdir()): + if path.is_file(): + result[str(path.relative_to(root))] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + package = Path(__file__).resolve().parent + hashes = bindings(package) + transfers = {q: transfer(q, 64 if q == 2 else 8) for q in FIELDS} + weights = {q: local_weights(q) for q in FIELDS} + pairs, headers = {}, {} + for q, m in PAIR_DOMAINS: + row = enumerate_pairs(q, m) + need(row['joint'] == transfers[q][m], "pair census vs transfer") + marginal = Fraction((q*q - q + 1)**(m - 1) * (q - 1), + (q**m - 1) * q**(m - 1)) + need(Fraction(row['single'], row['total']) == marginal, "PR4227 marginal") + pairs[f'{q},{m}'] = row + for q, m in HEADER_DOMAINS: + row = enumerate_headers(q, m) + pair = pairs[f'{q},{m}'] + need(Fraction(row['joint'], row['total']) == + Fraction(pair['joint'], pair['total']), "literal matrix guard census") + need(Fraction(row['single'], row['total']) == + Fraction(pair['single'], pair['total']), "literal marginal census") + headers[f'{q},{m}'] = row + for q in FIELDS: + value = Fraction(transfers[q][2], denominator(q, 2)) + need(value == Fraction((q - 1)**3 + 1, q*q*(q + 1)), "PR4240 one-sided boundary") + result = {"pairs": pairs, "headers": headers, "local_factorizations": weights, + "transfer_cases": sum(len(x) for x in transfers.values()), + "binary_cases": check_binary(transfers[2]), + "controls": controls(transfers, headers), "sha256": hashes} + print('PASS_ONEWAY_CORANKONE_HEADER_LAW ' + json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()