From bd8ea82bb0a7e40427d6d4fc1477fda0ab40388b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:20:55 +0100 Subject: [PATCH] feat(research): count common-covector full-guard headers --- research/common-covector-header-law/PROOF.md | 139 ++++++++++++ research/common-covector-header-law/README.md | 104 +++++++++ .../common-covector-header-law/SOURCES.json | 42 ++++ research/common-covector-header-law/TASK.json | 117 ++++++++++ .../common-covector-header-law/VERIFY.json | 34 +++ research/common-covector-header-law/verify.py | 208 ++++++++++++++++++ 6 files changed, 644 insertions(+) create mode 100644 research/common-covector-header-law/PROOF.md create mode 100644 research/common-covector-header-law/README.md create mode 100644 research/common-covector-header-law/SOURCES.json create mode 100644 research/common-covector-header-law/TASK.json create mode 100644 research/common-covector-header-law/VERIFY.json create mode 100644 research/common-covector-header-law/verify.py diff --git a/research/common-covector-header-law/PROOF.md b/research/common-covector-header-law/PROOF.md new file mode 100644 index 0000000000..8c0baf7570 --- /dev/null +++ b/research/common-covector-header-law/PROOF.md @@ -0,0 +1,139 @@ +# A common-covector pair has a different dependence law + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K=F_q be any finite field, m>=2, and let a,c be independent columns +in K^m. Let b be a row with ba=bc=1. Put U=ab, V=cb, P=I-U, Q=I-V. +Thus U,V are distinct rank-one idempotents with UV=U and VU=V. Both +products are nonzero. Their complementary projectors P,Q have a common +image ker(b). This is outside the orthogonal and one-way coupling hypotheses. + +For a complete header G chosen uniformly from GL_m(K), let E_P mean that +every leading principal minor of GPG^-1 of orders 1 through m-1 is +nonzero. Define E_Q in the same way. Write n=m-1 and + +```text +alpha = q^2-q+1, +delta = q^2+(q-1)^3. +``` + +Then the exact joint passing probability is + +```text + (q-1)(delta^n-alpha^n) +J(q,m) = ----------------------------------------- . (1) + (q^m-1)(q^m-q) q^(m-2) +``` + +In particular, over F_2 the events are strictly positively correlated for +every m>=2. At m=2 the joint probability is 1/3 and each marginal is 1/2. +This refutes extension of the known negative-correlation statements to +arbitrary two-way coupled rank-one kernels. It does not contradict their +stated hypotheses. + +Claim type: scoped counting proof with finite corroboration. + +## Header orbit and the guard + +Conjugation takes the triple to (Ga,Gc,bG^-1). GL_m(K) acts transitively +on all triples (a,c,b) satisfying independence and ba=bc=1. To see this, +take a,c-a as the first two basis vectors. The second lies in ker(b). +Extend it to a basis of ker(b), and b has coordinates (1,0,...,0). +The same construction for any other triple gives the required change of +basis. Every triple therefore has the same number of complete-header +preimages, by the stabilizer coset bijection. + +There are (q^m-1)(q^m-q) ordered independent pairs a,c. For each pair, +the two independent linear equations ba=bc=1 have q^(m-2) solutions b. +Consequently the denominator in (1) is the number of triples in this orbit. + +The rank-one determinant identity gives + +```text +det(P[1:k,1:k]) = 1 - sum_(i=1)^k b_i a_i, +det(Q[1:k,1:k]) = 1 - sum_(i=1)^k b_i c_i. +``` + +This is the marginal guard identity of Nick Petalas #4227. We use its +partial-sum method, also used in #4261, and count the new common-covector +orbit directly. For every proper prefix, both partial sums must avoid 1; +at the final coordinate both sums equal 1. + +## Count first, subtract dependent pairs + +Temporarily allow all a,c, retaining ba=bc=1. At one coordinate the +increment is (b_i a_i,b_i c_i). A zero increment has q^2+q-1 preimages: +q^2 choices with b_i=0, and q-1 with b_i nonzero and a_i=c_i=0. +Every nonzero increment has q-1 preimages, one for each nonzero b_i. +Thus the increment weight is q^2 times the zero indicator plus the +constant q-1 on K^2. + +The safe state set S=(K minus {1})^2 has N=(q-1)^2 elements. Its weighted +transition matrix is q^2 I+(q-1)11^T. Every row sum is +q^2+(q-1)N=delta. Start at (0,0) in S. After n safe transitions the +total path weight is delta^n. The terminal state (1,1) is outside S, +so the last increment is nonzero from every safe state and has weight +q-1. The number of all passing triples before enforcing independence is +(q-1)delta^n. + +If a,c are dependent, the endpoint conditions force c=a. Indeed a is +nonzero, write c=t a, and 1=bc=t ba=t. Conversely every diagonal pair +c=a with ba=1 is a dependent triple. There are no other dependent cases. + +For these diagonal triples the scalar increment b_i a_i has 2q-1 +preimages at zero and q-1 at every nonzero element. On K minus {1}, +the safe transition matrix is q I+(q-1)11^T, with row sum +q+(q-1)^2=alpha. The last step again has weight q-1. Therefore exactly +(q-1)alpha^n of the passing triples have dependent columns. Subtracting +them gives the numerator of (1). Dividing by the independent-triple orbit +count proves (1), in every characteristic and every finite field. + +## Binary positive correlation in every dimension + +The cited single-request law #4227 gives + +```text +p(q,m) = (q-1)alpha^n / ((q^m-1)q^(m-1)). +``` + +At q=2, alpha=3 and delta=5, and direct cancellation yields + +```text +J(2,m) / p(2,m)^2 + = [2^(n+1)(2^(n+1)-1)/(2^(n+1)-2)] (5^n-3^n)/9^n. (2) +``` + +Since 5>9/2, replacing 5^n by (9/2)^n strictly decreases (2). The +resulting lower bound is + +```text +2(2^(n+1)-1)/(2^(n+1)-2) * (1-(2/3)^n). +``` + +This is at least 1 exactly when 3^n>=2^(n+1)-1. The latter inequality +holds for every n>=1. It is equality at n=1; if it holds at n then +3^(n+1)>=3*2^(n+1)-3>=2^(n+2)-1, since 2^(n+1)>=2. +The replacement of 5^n was strict even at n=1, so J(2,m)>p(2,m)^2 +for every m>=2. This is a written dimension-uniform proof, rather than +an inference from a finite census. + +## Credit and limits + +The two-way-coupling question is Open next question 1 of Nick Petalas +[#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778), following +#4769/#4274's one-way law. The marginal identity and probability are from +#4227; #4261 supplies the predecessor partial-sum/header counting method. +The common-covector orbit, its dependent-pair subtraction, formula (1), +and the binary positive-correlation proof are the new contribution here. +Cinna Davis supplied the BIT request context. source527, commdata2338 and +Jose Manuel retain the normalizer and recursive-closure lineage credit. + +Only this common-covector pair and complete uniformly weighted headers are +covered. The proof does not classify arbitrary two-way pairs, larger +families, restricted header catalogues, or odd-field correlation signs. +Selection, emission, dispatch, dirty restoration, stock, precision and the +physical caller bill remain unknown. No supplier admission, new kappa, +selected-frontier change or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/common-covector-header-law/README.md b/research/common-covector-header-law/README.md new file mode 100644 index 0000000000..08535a3694 --- /dev/null +++ b/research/common-covector-header-law/README.md @@ -0,0 +1,104 @@ +# Positive correlation for a common-covector full-guard pair + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped counting proof with finite corroboration. Over any finite +field F_q, let a,c be independent columns, b a row with ba=bc=1, and +P=I-ab, Q=I-cb on F_q^m, m>=2. For complete uniformly weighted GL_m(F_q) +headers, the joint full-guard passing fraction is exactly + +```text + (q-1)[(q^2+(q-1)^3)^(m-1) - (q^2-q+1)^(m-1)] +J(q,m) = ------------------------------------------------- . + (q^m-1)(q^m-q)q^(m-2) +``` + +Over F_2 these two guard events are strictly positively correlated in every +dimension m>=2. At m=2, J=1/3 exceeds the marginal product 1/4; at m=3, +J=4/21 and each marginal is 9/28. Thus negative correlation for the known +orthogonal and one-way cases does not extend to every two-way pair. + +[PROOF.md](PROOF.md) counts the common-covector header orbit by two partial +sums, subtracts exactly the equal-column paths, and proves the binary +comparison for all dimensions. This answers one case of Open next question 1 +in [#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778). That +question and #4769/#4274's contrasting one-way law retain Nick Petalas's +credit, as do #4227's marginal law and #4261's partial-sum/header method. +Cinna Davis supplied the BIT request context; source527, commdata2338 and +Jose Manuel retain the normalizer and recursive-closure lineage credit. +No predecessor implementation is imported or replayed. + +## Reproduction and evidence + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/common-covector-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/common-covector-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/common-covector-header-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/common-covector-header-law --check-source-history +``` + +Another CPython 3.12 installation may replace the local interpreter path. +The direct marker is `PASS_COMMON_COVECTOR_HEADER_LAW`. The verifier writes +no files. It prints a generated receipt with every domain's counts and +SHA256 hashes of all six package files. Both registered modes keep explicit +checks active, including optimized Python. + +The verifier enumerates all 34,290 complete headers in eight domains: +GL_2 over F_2,F_3,F_4,F_5,F_7, GL_3 over F_2,F_3, and GL_4 over F_2. +It inverts each header, conjugates both literal projectors and tests every +leading minor through rank m-1. Both marginals and the joint count agree. +F_4 is F_2[x]/(x^2+x+1), rather than integers modulo four. + +A separate vector enumeration counts all 26,070 independent orbit triples +in nine domains: q=2,m=2..5; q=3 or 4,m=2..3; q=5,m=2. Ten coordinate +transfers enumerate the actual increment factorizations for widths one and +two over F_2,F_3,F_4,F_5,F_7, at path lengths zero through eight. Their +difference agrees with the joint formula at m=2..9. Exact rational checks +corroborate binary positive correlation in all 255 dimensions m=2..256. +Fourteen fixture, mutation and invalid-input controls distinguish the +field arithmetic, independence, orthogonal substitution, omitted diagonal +subtraction, omitted row fiber and invalid finite-check parameters. + +## Scope and implementation limits + +The all-field and all-dimension claims rest on the written proof. Finite +execution corroborates the explicitly enumerated domains. Only two distinct +rank-one kernels with a common right covector and complete equally weighted +headers are covered. Other two-way pairs, larger families, restricted +headers and odd-field correlation signs are outside the proved claims. + +Header selection, emission, dispatch, dirty restoration, stock, precision, +producer compatibility and the complete paid physical caller remain unknown. +No new kappa, supplier admission, selected-frontier change or complete +multiplication theorem is claimed. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected operator replay are unrun. + +[TASK.json](TASK.json) records the change from the formal-interface card to +this algebraic side question. [SOURCES.json](SOURCES.json) binds predecessor +text, the catalogue and selected record as historical provenance on canonical +main. There are no runtime dependencies outside this package and no pending +Git-object dependency. Provenance/history checks require full Git history; +the direct verifier also runs from a standalone exported package. + +Power of Ten inspection finds no recursion or subprocesses in the verifier. +Every loop is bounded by fixed domains: at most 65,536 candidate matrices +of size four, 64 vectors per triple coordinate, 49 transfer states, nine +transfer rounds and 255 correlation dimensions. Functions fit within 60 +lines. Explicit require checks enforce input and mathematical contracts. +CPython allocates dynamically, a managed-runtime deviation from fixed +allocation; the stated domains bound live collections. Diagnostics use +warnings as errors. No shared implementation is changed. + +## Open next questions + +1. Determine the law for two-way pairs with independent covectors. Start + with one normalized pair whose two cross products are nonzero; its + partial-Gram orbit differs from the shared-covector model here. +2. Determine the correlation signs for this common-covector family over + odd fields. Compare the new joint formula with #4227's marginal squared, + starting with q*delta-alpha^2=q-1; a quantified sign proof is unclaimed. +3. Find a named physical producer and fully charged shared-header caller. + Pin its header domain before charging selection, emission, dispatch, + dirty restoration, precision and stock. Those costs are unknown. diff --git a/research/common-covector-header-law/SOURCES.json b/research/common-covector-header-law/SOURCES.json new file mode 100644 index 0000000000..bcb2098e53 --- /dev/null +++ b/research/common-covector-header-law/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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/projector-header-density/PROOF.md", + "usage": "provenance", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + }, + { + "path": "research/corankone-all-field-law/PROOF.md", + "usage": "provenance", + "git_blob": "ac0152e05a5c050bbd740ddbe6d0cbaaecbb6cd8", + "sha256": "ca7762bea269445f7b30c59c7b6161282483da5fd191faa668145f1ad6d8ade4" + }, + { + "path": "research/corankone-pair-header-law/README.md", + "usage": "provenance", + "git_blob": "743cf79ee8403d66cb651ac1111065cc650ad638", + "sha256": "ca362324cd8a041a25d6494f857e0f8bf7b2ef0d6f8c83ec5e8c08b0f92ca515" + }, + { + "path": "research/corankone-all-field-law/README.md", + "usage": "provenance", + "git_blob": "83a3e9e3de457d97743e6364a71cc493d0158fc1", + "sha256": "05422e3227c67f6a973282e01ac77031df58464184caf0f138d7b0c1af935c98" + } + ] +} diff --git a/research/common-covector-header-law/TASK.json b/research/common-covector-header-law/TASK.json new file mode 100644 index 0000000000..352eebd2fd --- /dev/null +++ b/research/common-covector-header-law/TASK.json @@ -0,0 +1,117 @@ +{ + "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": "Prove the all-field joint full-guard law for distinct rank-one kernels with a common right covector, and binary positive correlation in every dimension.", + "scope_change_reason": "The interface-formalization card is replaced by the explicitly open two-way-coupling counting question in PR4778, narrowed to common-covector kernels. This is a scoped written counting proof, not a proof-assistant formalization or predecessor audit.", + "bottleneck_link": "An algebraic side result delineating dependence of shared full guards. Complete-header counts do not supply a paid physical caller or improve the selected kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original formula and its binary correlation consequence. Leave other coupling classes and physical use as open next questions.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py enumerates eight complete-header domains, nine independent-triple domains, ten finite-field transfers and 255 binary dimensions. The verifier generates file-hash receipts on stdout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the joint law for two-way pairs whose rank-one covectors are independent?", + "why_it_matters": "The common-covector count and the one-way law do not exhaust two-way coupling.", + "first_step": "Fix ba=dc=1 with both cross products nonzero and independent rows b,d; derive the relevant orbit before counting its safe partial-Gram paths.", + "blocked_by": "The rank-one increment on two shared sums used here no longer describes that orbit." + }, + { + "question": "For this common-covector family, what are the correlation signs over odd fields?", + "why_it_matters": "The all-field joint formula permits an exact comparison, but the dimension-uniform sign proof here is binary.", + "first_step": "Compare equation (1) with the squared #4227 marginal using q*delta-alpha^2=q-1.", + "blocked_by": "A quantified all-q comparison remains to be proved." + }, + { + "question": "Can a physical request producer exploit this common-covector family with a favorable paid caller?", + "why_it_matters": "A complete-header density has no supplier consequence without an implementation and full invoice.", + "first_step": "Pin an actual producer and header domain, then charge selection, emission, dispatch, dirty return, precision and stock.", + "blocked_by": "All physical caller costs and producer compatibility remain unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132057", + "overlap_coverage": { + "canonical_base": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "open_pr_bodies": 326, + "discussion_records": 3748, + "local_notes": 109, + "head_notes": 6319, + "caveat": "Sparse notes, capped live searches and unpublished work are incomplete; no search certifies novelty. Main README searches and targeted merged PR searches found no same-question result." + } +} diff --git a/research/common-covector-header-law/VERIFY.json b/research/common-covector-header-law/VERIFY.json new file mode 100644 index 0000000000..625f86c6f8 --- /dev/null +++ b/research/common-covector-header-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": 120, + "checks": "Literal full GL headers, independent orbit triples, finite-field coordinate transfers, binary strict correlation and fourteen fixture/mutation/domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every scoped check with assertions disabled; explicit contract failures remain active." + } + ] +} diff --git a/research/common-covector-header-law/verify.py b/research/common-covector-header-law/verify.py new file mode 100644 index 0000000000..975c30835c --- /dev/null +++ b/research/common-covector-header-law/verify.py @@ -0,0 +1,208 @@ +"""Finite corroboration of the common-covector header law; no files written.""" + +import hashlib +import itertools +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path + + +def require(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 + result = 0 + for _ in range(2): + if b & 1: + result ^= a + b >>= 1 + a <<= 1 + if a & 4: + a ^= 7 + return result + + +def dot(a, b, q): + result = 0 + for x, y in zip(a, b, strict=True): + result = add(result, mul(x, y, q), q) + return result + + +def matrix_product(a, b, q): + return tuple(tuple(dot(row, col, q) for col in zip(*b, strict=True)) for row in a) + + +def inverse(a, q): + m = len(a) + rows = [list(row) + [int(i == j) for j in range(m)] for i, row in enumerate(a)] + for j in range(m): + pivot = next((i for i in range(j, m) if rows[i][j]), None) + if pivot is None: + return None + rows[j], rows[pivot] = rows[pivot], rows[j] + scale = next(x for x in range(1, q) if mul(rows[j][j], x, q) == 1) + rows[j] = [mul(x, scale, q) for x in rows[j]] + for i in range(m): + if i != j: + scale = neg(rows[i][j], q) + rows[i] = [add(x, mul(scale, y, q), q) + for x, y in zip(rows[i], rows[j], strict=True)] + return tuple(tuple(row[m:]) for row in rows) + + +def full_guard(a, q): + m = len(a) + for k in range(1, m): + block = tuple(tuple(a[i][j] for j in range(k)) for i in range(k)) + if inverse(block, q) is None: + return False + return True + + +def joint(q, m): + require(q in (2, 3, 4, 5, 7), "unsupported finite field") + require(isinstance(m, int) and 2 <= m <= 256, "dimension out of finite-check bounds") + n = m - 1 + alpha = q * q - q + 1 + delta = q * q + (q - 1) ** 3 + return Fraction((q - 1) * (delta**n - alpha**n), + (q**m - 1) * (q**m - q) * q ** (m - 2)) + + +def marginal(q, m): + return Fraction((q - 1) * (q * q - q + 1) ** (m - 1), + (q**m - 1) * q ** (m - 1)) + + +def enumerate_headers(q, m): + require((q, m) in ((2, 2), (3, 2), (4, 2), (5, 2), (7, 2), + (2, 3), (3, 3), (2, 4)), "header domain not registered") + p = tuple(tuple(int(i == j and i != 0) for j in range(m)) for i in range(m)) + v = tuple(tuple(add(p[i][j], neg(int(i == 1 and j == 0), q), q) + for j in range(m)) for i in range(m)) + total = left = right = both = 0 + for entries in itertools.product(range(q), repeat=m * m): + g = tuple(tuple(entries[i * m:(i + 1) * m]) for i in range(m)) + gi = inverse(g, q) + if gi is None: + continue + first = full_guard(matrix_product(matrix_product(g, p, q), gi, q), q) + second = full_guard(matrix_product(matrix_product(g, v, q), gi, q), q) + total += 1 + left += first + right += second + both += first and second + require(Fraction(both, total) == joint(q, m), f"header joint: {q},{m}") + require(Fraction(left, total) == Fraction(right, total) == marginal(q, m), + f"header marginals: {q},{m}") + return {"q": q, "m": m, "headers": total, "joint_pass": both, + "marginal_pass": left, "fraction": str(Fraction(both, total))} + + +def enumerate_triples(q, m): + require((q, m) in ((2, 2), (2, 3), (2, 4), (2, 5), + (3, 2), (3, 3), (4, 2), (4, 3), (5, 2)), + "triple domain not registered") + vectors = tuple(itertools.product(range(q), repeat=m)) + total = good = 0 + for a, c in itertools.product(vectors, repeat=2): + if not any(a) or any(c == tuple(mul(t, x, q) for x in a) for t in range(q)): + continue + for b in vectors: + if dot(b, a, q) != 1 or dot(b, c, q) != 1: + continue + total += 1 + passing = True + x = y = 0 + for i in range(m - 1): + x = add(x, mul(b[i], a[i], q), q) + y = add(y, mul(b[i], c[i], q), q) + if x == 1 or y == 1: + passing = False + good += passing + denominator = (q**m - 1) * (q**m - q) * q ** (m - 2) + require(total == denominator, f"triple orbit size: {q},{m}") + require(Fraction(good, total) == joint(q, m), f"triple joint: {q},{m}") + return {"q": q, "m": m, "triples": total, "joint_pass": good} + + +def transfer_counts(q, width): + require(q in (2, 3, 4, 5, 7) and width in (1, 2), "transfer bounds") + states = tuple(itertools.product(range(q), repeat=width)) + weights = Counter() + for values in itertools.product(range(q), repeat=width + 1): + weights[tuple(mul(x, values[-1], q) for x in values[:-1])] += 1 + safe = tuple(s for s in states if 1 not in s) + current = {s: int(not any(s)) for s in safe} + counts = [] + for _ in range(9): + counts.append(sum(value * weights[tuple(add(1, neg(x, q), q) for x in s)] + for s, value in current.items())) + current = {t: sum(value * weights[tuple(add(y, neg(x, q), q) + for x, y in zip(s, t, strict=True))] + for s, value in current.items()) for t in safe} + base = q + (q - 1) ** 2 if width == 1 else q * q + (q - 1) ** 3 + require(counts == [(q - 1) * base**n for n in range(9)], "transfer power law") + return counts + + +def controls(): + require(mul(2, 2, 4) == 3 and add(2, 2, 4) == 0, "F4 arithmetic") + require(joint(2, 2) == Fraction(1, 3), "binary base fixture") + require(joint(2, 3) == Fraction(4, 21), "binary next fixture") + require(joint(3, 2) == Fraction(5, 12), "odd-field fixture") + require(joint(4, 2) == Fraction(1, 2), "extension-field fixture") + require(joint(2, 2) != marginal(2, 2) ** 2, "independence mutant") + require(joint(2, 2) != 0, "orthogonal-pair substitution mutant") + require(Fraction(5, 6) != joint(2, 2), "missing dependent-pair subtraction") + require(Fraction(5**2 - 3**2, 7 * 6) != joint(2, 3), "missing row fiber") + for q, m in ((1, 2), (6, 2), (2, 1), (2, 257), (2, 2.5)): + try: + joint(q, m) + except ValueError: + continue + raise ValueError("invalid finite-check parameters accepted") + return 14 + + +def main(): + headers = [enumerate_headers(q, m) for q, m in + ((2, 2), (3, 2), (4, 2), (5, 2), (7, 2), (2, 3), (3, 3), (2, 4))] + triples = [enumerate_triples(q, m) for q, m in + ((2, 2), (2, 3), (2, 4), (2, 5), (3, 2), (3, 3), (4, 2), (4, 3), (5, 2))] + transfers = [] + for q in (2, 3, 4, 5, 7): + diagonal, raw = transfer_counts(q, 1), transfer_counts(q, 2) + for m in range(2, 10): + denominator = (q**m - 1) * (q**m - q) * q ** (m - 2) + require(Fraction(raw[m - 1] - diagonal[m - 1], denominator) == joint(q, m), + "independent transfer subtraction") + transfers.append({"q": q, "raw": raw, "diagonal": diagonal}) + for m in range(2, 257): + require(joint(2, m) > marginal(2, m) ** 2, "binary positive correlation") + require(3 ** (m - 1) >= 2**m - 1, "binary proof comparison") + package = Path(__file__).resolve().parent + files = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in files} + print(json.dumps({"status": "PASS_COMMON_COVECTOR_HEADER_LAW", "headers": headers, + "triples": triples, "transfers": transfers, + "binary_dimensions": [2, 256], "controls": controls(), + "sha256": hashes}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()