diff --git a/research/corankone-all-field-law/PROOF.md b/research/corankone-all-field-law/PROOF.md new file mode 100644 index 0000000000..ac0152e05a --- /dev/null +++ b/research/corankone-all-field-law/PROOF.md @@ -0,0 +1,178 @@ +# The all-field two-request law + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and predecessor + +Let K be any finite field of order q, let m >= 2, and let U,V be rank-one +idempotents on K^m with UV=VU=0. Set P=I-U and Q=I-V. A complete header +G in GL_m(K) passes R if every leading principal minor of GRG^-1 of orders +1 through rank(R) is nonzero. Weight all complete headers equally. + +Write n=m-1 and + +```text +alpha = (q^2-q+1)^2, +beta = q^3-q+1, +gamma = q^3-q^2+1. +``` + +The exact joint passing fraction is + +```text + (q-1)^2 [alpha^n - 2 beta^n + gamma^n] +J = ------------------------------------------------- . + q^2 (q^m-1)(q^m-q) q^(2m-4) +``` + +This is a scoped counting proof, with finite corroboration. It supplies the +all-field closed form left open by Nick Petalas's #4261 and extends the +binary and ternary closed forms in #4261 and #4273. Those results are cited +as predecessors, not re-audited. The retained request context is due to +Cinna Davis; source527, commdata2338 and Jose Manuel retain the normalizer +lineage credit. + +## The cited transfer, in complementary coordinates + +Use #4261's normalized-pair and equal-header-fiber theorem. In its partial +Gram coordinates A, safe states have A_11,A_22 != 1, the initial state is +A=0, and the terminal weight is w(I-A). Substitute B=I-A. Let S consist +of the 2 by 2 matrices B with both diagonal entries nonzero. Define + +```text +w(H) = 2q^2-1 if H=0; q-1 if rank(H)=1; 0 otherwise, +(Tf)(B) = sum_(C in S) w(B-C) f(C), +h(B) = w(B) = (q-1) 1_(det B=0). +``` + +Negation preserves w, so this substitution preserves the transfer. The +passing-pair numerator is c_n=(T^n h)(I). The total normalized-pair count +is D=(q^m-1)(q^m-q)q^(2m-4), so J=c_n/D. Every pair has exactly +|GL_(m-2)(K)| header completions. This package's new proof concerns c_n. + +## Three invariant functions + +Put z(B)=1_(B_12=0)+1_(B_21=0) and a=(q-1)^2(q^2-3q+4). Then + +```text +T 1 = alpha 1, +T z = 2(q-1)^3 1 + beta z, +T h = a 1 - (q-1)^2 z + gamma h. (1) +``` + +These identities hold over every finite field, without a prime-field +assumption. They reduce the transfer from q^2(q-1)^2 states to three +functions. + +For T1, enumerate the rank-one increment yx. Its two diagonal restrictions +are y_i x_i != B_ii. For each nonzero B_ii there are q^2-(q-1)=q^2-q+1 +choices of (y_i,x_i). The two coordinates are independent. Thus T1=alpha. +This also accounts for all 2q^2-1 factorizations of the zero increment. + +For the first off-diagonal zero indicator, impose y_1 x_2=B_12. If +B_12 != 0, there are q-1 choices of (y_1,x_2), and each of x_1,y_2 +has q-1 choices after its diagonal exclusion. The total is (q-1)^3. +If B_12=0, inclusion-exclusion on y_1=0 or x_2=0 gives + +```text +2q(q^2-q+1)-q^2 = (q-1)^3 + beta. +``` + +Apply the same argument to B_21 and add. This proves Tz. + +For Th, sum over singular C in S. Diagonal row and column scalings +preserve S, rank differences, off-diagonal zeros and singularity. They +normalize B's diagonal to (1,1). Transposition and residual scaling reduce +its off-diagonal pattern to one of the following. In the last row, t is +any field element other than 0,1. + +| Type | B | (Th)(B) | +|---|---|---| +| Z | [[1,0],[0,1]] | (q-2)(q-1)^3 | +| L | [[1,1],[0,1]] | (q-1)^2(q^2-3q+3) | +| R | [[1,1],[1,1]] | (q-1)(2q^2-1)+(q-1)^2((q-1)(2q-3)-1) | +| N | [[1,1],[t,1]] | (q-1)^2(q^2-3q+4) | + +Here is a direct count of each row, rather than extrapolation from a +finite collection of fields. Write C=[[r,s],[u,v]], with r,v != 0 and +su=rv. In particular s,u != 0. + +For Z, det(B-C)=0 says r+v=1. There are q-2 choices of r and q-1 +choices of s, giving (q-2)(q-1) targets. Multiply by (q-1)^2 for the +transition weight and h(C). + +For L, det(B-C)=0 says u=r+v-1. Among the (q-1)^2 choices of r,v, +exactly q-2 have r+v=1. Each remaining choice determines nonzero u +and s=rv/u. This gives q^2-3q+3 targets. + +For R, det(B-C)=0 says s+u=r+v. Together with su=rv, this means +{s,u}={r,v}, with multiplicity one if r=v and two otherwise. There are +(q-1)(2q-3) targets. One is C=B, whose transition weight is 2q^2-1; +the others have transition weight q-1. This proves the displayed R row. + +For N, eliminate u from the two determinant conditions to get + +```text +(r-s)(v-s) = (1-t)s(s-1). +``` + +When s=1, there are 2q-3 choices of nonzero r,v. For each s != 0,1, +the right side is nonzero. There are q-1 choices of nonzero r-s before +excluding r=0 and v=0. Those exclusions coincide precisely when +s=1-1/t, a unique permitted s. Thus the total number of targets is + +```text +(2q-3) + (q-2)(q-3) + 1 = q^2-3q+4. +``` + +The N case is absent for q=2. No division by 2 or characteristic-specific +step was used. Substituting z=2,1,0,0 and h=0,0,q-1,0 respectively in +these four rows proves the third identity in (1). + +## Closing the scalar recurrence + +Equation (1) implies + +```text +(T-alpha)(T-beta)(T-gamma) h = 0. +``` + +Therefore c_n satisfies the cubic recurrence with characteristic +polynomial (X-alpha)(X-beta)(X-gamma). Its initial values are + +```text +c_0 = 0, +c_1 = (q-1)^3(q-2), +c_2 = a alpha - (q-1)^2[2(q-1)^3+2 beta] + gamma c_1. +``` + +The candidate d_n=((q-1)^2/q^2)(alpha^n-2 beta^n+gamma^n) satisfies +the same recurrence. Direct polynomial expansion gives d_0=0, +d_1=c_1 and d_2=c_2. Induction proves c_n=d_n for every n>=0, hence +the stated formula for every m>=2. This is an all-field written proof. + +For example q=5 gives + +```text +c_n = (16/25)(441^n - 2*121^n + 101^n), +c_1 = 192, c_2 = 112256, J_(m=2) = 2/5. +``` + +At q=2 and q=3 the three bases specialize to (9,7,5) and (49,25,19), +respectively, and the coefficients to 1/4 and 4/9, exactly the cited +predecessor formulas. No new result is claimed for those specializations. + +## Evidence and limits + +The self-contained verifier enumerates literal rank-one factorizations, +checks (1) by exact field arithmetic, and compares the new formula to a +separately implemented full-state transfer. Its generated receipt states +every finite domain and binds the six package files by SHA256. These checks +corroborate the proof; they do not replace its quantified argument. + +Only two fixed orthogonal rank-one kernels and complete uniform headers +are covered. Nonorthogonal kernels, restricted header sets and k>=3 remain +outside this formula. Header selection, emission, dispatch, restoration, +stock and physical costs remain unpriced. 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/corankone-all-field-law/README.md b/research/corankone-all-field-law/README.md new file mode 100644 index 0000000000..83a3e9e3de --- /dev/null +++ b/research/corankone-all-field-law/README.md @@ -0,0 +1,92 @@ +# A three-power header law over every finite field + +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, and let P=I-U,Q=I-V. +A complete header passes a request when every leading principal minor +through its rank is nonzero. For uniformly weighted complete GL_m(F_q) +headers, the exact probability of passing both requests is + +```text +(q-1)^2 [((q^2-q+1)^2)^n - 2(q^3-q+1)^n + (q^3-q^2+1)^n] +----------------------------------------------------------------, n=m-1. + q^2 (q^m-1)(q^m-q) q^(2m-4) +``` + +[PROOF.md](PROOF.md) reduces the full partial-Gram transfer to the invariant +span of three functions. The proof works in arbitrary characteristic and +in nonprime fields. For q=5 the numerator before division by the normalized +pair count is `(16/25)(441^n-2*121^n+101^n)`, with first values 192 and +112256. The joint fraction at m=2 is 2/5. + +This answers the all-field closed-form question left open by +[#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261) and +[#4273](https://github.com/CrocSwap/integer-mult-bounds/pull/4273), both +produced by Nick Petalas. Their partial-Gram transfer and binary/ternary +special cases are cited steps. The new result is the all-field invariant +space and closed form. Cinna Davis supplied the BIT request context; +source527, commdata2338 and Jose Manuel retain the normalizer lineage +credit. No predecessor implementation is imported or replayed. + +## Reproduction and evidence + +From the repository root, use CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-all-field-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-all-field-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-all-field-law --check-source-history +``` + +The marker is `PASS_CORANKONE_ALL_FIELD_LAW`. The verifier prints a generated +receipt with finite domains, counts and SHA256 hashes of all six package +files. It writes no artifacts. Registered replay runs both normal and +optimized modes, with warnings as errors and explicit checks active under -O. + +It checks all source states over F_2,F_3,F_4,F_5 and every normalized orbit +representative over F_7,F_8,F_9. F_4 and F_8 use irreducible binary +polynomials; F_9 uses x^2+1 over F_3. Every target state is included in +each identity sum. Literal factor enumeration checks the zero and rank-one +weights separately. Every complete GL_2 header over these seven fields is +inverted and both conjugated full guards are checked. Independent full-state +evolution over F_2,F_3,F_4,F_5 checks n=0..8. Eleven exact integer evaluations certify the two displayed +initial-value polynomial identities of degree at most ten. Seven controls +distinguish boundary cases, wrong eigenvalues/coefficient, independence, +and confusing F_4 with Z/4Z. + +## Scope and obligations + +This is a complete-domain counting theorem for the stated two requests. +It makes no statement about arbitrary restricted header families, nonorthogonal +kernels or three or more kernels. A producer and the costs of selection, +emission, dispatch, dirty restoration, stock, precision and the full physical +caller remain unknown. No new kappa, supplier admission or selected-frontier +change is claimed. Independent human and formal proof-kernel review are +unclaimed. Lean, Docker and the selected construction's cold replay are unrun. + +The card's scope is changed from proof-assistant interface work to this +explicitly open algebraic side question. TASK.json records that change. +SOURCES.json pins predecessor proof text as historical provenance; there +are no external runtime inputs. + +The verifier uses bounded loops, no recursion and functions below 60 lines. +The largest full transfer has 400 states and 160,000 stored weights. +The largest identity domain has 5,184 targets and ten source representatives. +CPython's dynamic allocation is a managed-runtime deviation from fixed +allocation, bounded by these fixed domains. Warnings are errors in both +registered commands. Ruff E/F/B/UP and AST function-size inspection pass +locally. The executable result is finite corroboration, not a +formal proof-kernel check of the written theorem. + +## Open next questions + +1. Does the exact two-event formula imply strict negative correlation over + every finite field? Start by comparing it with #4227's marginal squared; + no all-field correlation theorem is claimed here. +2. Can three requests admit a similarly small all-field invariant space? + Start with rank-one increments on 3 by 3 matrices; this proof uses the + specific 2 by 2 determinant structure. +3. Can a real odd-field request producer use the count with a fully paid + shared-header caller? Pin its header domain before charging selection, + emission, dispatch, restoration and stock. Those costs remain unknown. diff --git a/research/corankone-all-field-law/SOURCES.json b/research/corankone-all-field-law/SOURCES.json new file mode 100644 index 0000000000..2389a8c4a0 --- /dev/null +++ b/research/corankone-all-field-law/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/corankone-pair-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548", + "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0" + }, + { + "path": "research/ternary-corankone-pair-law/PROOF.md", + "usage": "provenance", + "git_blob": "c91f551dcf370de1c5d2860d3c75e74bc1d88d6e", + "sha256": "096b3acfd46f905553f3145f5714d57a7f0141028c50fad04eea0ec4b252564f" + } + ] +} diff --git a/research/corankone-all-field-law/TASK.json b/research/corankone-all-field-law/TASK.json new file mode 100644 index 0000000000..be7e789d31 --- /dev/null +++ b/research/corankone-all-field-law/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "A written all-finite-field closed form for the simultaneous full-guard header fraction of two corank-one requests with orthogonal rank-one kernels, via a three-function invariant space.", + "scope_change_reason": "Takes the explicit all-field closed-form question left open by PR4261 and PR4273 as an algebraic side result; does not claim a formalized interface or audit predecessor results.", + "bottleneck_link": "A precise shared-header count can guide future producer selection, but no physical implementation costs or supplier admission follow.", + "budget_minutes": 60, + "stop_rule": "Stop after proving and checking the first all-field closed form; leave correlation and higher-request extensions open.", + "outcome": "completed", + "evidence": "PROOF.md and the self-contained verifier with literal factor counts, all-state invariant identities, full-state transfers and polynomial checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the product inequality hold over every finite field?", + "why_it_matters": "Would quantify shared-header dependence.", + "first_step": "Compare the new formula to the squared marginal of PR4227.", + "blocked_by": "A uniform inequality is not proved here." + }, + { + "question": "Can three requests have a small all-field invariant space?", + "why_it_matters": "Would extend beyond pair counts.", + "first_step": "Study rank-one increments on 3 by 3 states.", + "blocked_by": "The 2 by 2 determinant argument does not directly extend." + }, + { + "question": "Can an actual producer use a fully charged shared-header caller?", + "why_it_matters": "Counting alone does not improve a supplier.", + "first_step": "Pin the producer and header domain, then charge the complete caller.", + "blocked_by": "Selection, emission, dispatch, restoration and stock costs remain unknown." + } + ] +} diff --git a/research/corankone-all-field-law/VERIFY.json b/research/corankone-all-field-law/VERIFY.json new file mode 100644 index 0000000000..35f2237953 --- /dev/null +++ b/research/corankone-all-field-law/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All-field invariant identities, independent finite transfer, literal factor weights, degree-bounded polynomial identities and seven controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All-field invariant identities, independent finite transfer, literal factor weights, degree-bounded polynomial identities and seven controls." + } + ] +} diff --git a/research/corankone-all-field-law/verify.py b/research/corankone-all-field-law/verify.py new file mode 100644 index 0000000000..891ca0ea2d --- /dev/null +++ b/research/corankone-all-field-law/verify.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Exact finite checks for the all-field pair law. Produced by Nick Petalas.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field(p, modulus): + """Tables for the fixed fields, with polynomial-basis extension arithmetic.""" + degree = len(modulus) - 1 + q = p**degree + require(q in (2, 3, 4, 5, 7, 8, 9), "unsupported field size") + digits = [tuple((i // p**j) % p for j in range(degree)) for i in range(q)] + addition, multiplication = [], [] + for a, b in product(digits, repeat=2): + addition.append(sum((a[i] + b[i]) % p * p**i for i in range(degree))) + coefficients = [0] * (2 * degree - 1) + for i, j in product(range(degree), repeat=2): + coefficients[i + j] = (coefficients[i + j] + a[i] * b[j]) % p + for k in range(2 * degree - 2, degree - 1, -1): + for j in range(degree): + coefficients[k - degree + j] -= coefficients[k] * modulus[j] + multiplication.append(sum(coefficients[i] % p * p**i for i in range(degree))) + add = tuple(tuple(addition[a * q : (a + 1) * q]) for a in range(q)) + mul = tuple(tuple(multiplication[a * q : (a + 1) * q]) for a in range(q)) + neg = tuple(next(b for b in range(q) if add[a][b] == 0) for a in range(q)) + sub = tuple(tuple(add[a][neg[b]] for b in range(q)) for a in range(q)) + for a in range(1, q): + require(sum(mul[a][b] == 1 for b in range(q)) == 1, "missing inverse") + for a, b, c in product(range(q), repeat=3): + require(mul[a][add[b][c]] == add[mul[a][b]][mul[a][c]], "distributivity") + return q, sub, mul + + +def invariants(matrix, mul): + a, b, c, d = matrix + zeros = int(b == 0) + int(c == 0) + singular = int(mul[a][d] == mul[b][c]) + return zeros, singular + + +def transition(source, target, q, sub, mul): + a, b, c, d = (sub[x][y] for x, y in zip(source, target, strict=True)) + if a == b == c == d == 0: + return 2 * q * q - 1 + return q - 1 if mul[a][d] == mul[b][c] else 0 + + +def parameters(q): + return (q * q - q + 1) ** 2, q**3 - q + 1, q**3 - q * q + 1 + + +def numerator(q, n): + alpha, beta, gamma = parameters(q) + value = Fraction((q - 1) ** 2, q * q) * (alpha**n - 2 * beta**n + gamma**n) + require(value.denominator == 1 and value >= 0, "nonintegral count") + return value.numerator + + +def check_identities(q, states, samples, sub, mul): + alpha, beta, gamma = parameters(q) + constant = (q - 1) ** 2 * (q * q - 3 * q + 4) + target_values = [invariants(b, mul) for b in states] + for source in samples: + total, zero_sum, terminal = 0, 0, 0 + for target, (zeros, singular) in zip(states, target_values, strict=True): + weight = transition(source, target, q, sub, mul) + total += weight + zero_sum += weight * zeros + terminal += weight * singular * (q - 1) + zeros, singular = invariants(source, mul) + require(total == alpha, "T1 identity") + require(zero_sum == 2 * (q - 1) ** 3 + beta * zeros, "Tz identity") + require( + terminal == constant - (q - 1) ** 2 * zeros + gamma * (q - 1) * singular, + "Th identity", + ) + return len(samples) * len(states) + + +def check_transfer(q, states, sub, mul): + """Independent full-state evolution, without the invariant quotient.""" + rows = [tuple(transition(a, b, q, sub, mul) for b in states) for a in states] + terminal = [(q - 1) * invariants(b, mul)[1] for b in states] + start = states.index((1, 0, 0, 1)) + for n in range(9): + require(terminal[start] == numerator(q, n), "closed form versus transfer") + if n < 8: + terminal = [ + sum(w * v for w, v in zip(row, terminal, strict=True)) for row in rows + ] + return [numerator(q, n) for n in range(1, 5)] + + +def factor_count_controls(q, sub, mul): + """Enumerate literal outer products, independently of determinant weights.""" + counts = {} + for u, v, x, y in product(range(q), repeat=4): + matrix = (mul[u][x], mul[u][y], mul[v][x], mul[v][y]) + counts[matrix] = counts.get(matrix, 0) + 1 + zero = (0, 0, 0, 0) + for matrix in product(range(q), repeat=4): + require( + counts.get(matrix, 0) == transition(matrix, zero, q, sub, mul), + "literal factor multiplicity", + ) + require(counts[zero] != 2 * q * q, "zero multiplicity mutant survived") + return q**4 + + +def check_headers(q, sub, mul): + """Literal complete GL2 headers and both conjugated one-pivot requests.""" + invertible, passing = 0, 0 + for a, b, c, d in product(range(q), repeat=4): + determinant = sub[mul[a][d]][mul[b][c]] + if determinant == 0: + continue + invertible += 1 + inverse_det = next(x for x in range(1, q) if mul[determinant][x] == 1) + inverse_00 = mul[d][inverse_det] + inverse_10 = mul[sub[0][c]][inverse_det] + # G diag(1,0) G^-1 and G diag(0,1) G^-1, at their only pivot. + passing += int(mul[a][inverse_00] != 0 and mul[b][inverse_10] != 0) + require(invertible == (q * q - 1) * (q * q - q), "complete GL2 domain") + require(passing == numerator(q, 1), "literal full-guard header count") + return {"total": invertible, "passing": passing} + + +def check_polynomials(): + """A degree-at-most-10 identity is fixed by 11 distinct integer evaluations.""" + for q in range(2, 13): + alpha, beta, gamma = parameters(q) + constant = (q - 1) ** 2 * (q * q - 3 * q + 4) + c1 = (q - 1) ** 3 * (q - 2) + c2 = ( + constant * alpha - (q - 1) ** 2 * (2 * (q - 1) ** 3 + 2 * beta) + gamma * c1 + ) + require((q - 1) ** 2 * (alpha - 2 * beta + gamma) == q * q * c1, "initial c1") + require( + (q - 1) ** 2 * (alpha**2 - 2 * beta**2 + gamma**2) == q * q * c2, + "initial c2", + ) + return 11 + + +def controls(): + require(numerator(2, 1) == 0 and numerator(2, 2) == 2, "binary boundary") + require(numerator(3, 1) == 8 and numerator(3, 2) == 672, "ternary boundary") + require(numerator(5, 1) == 192 and numerator(5, 2) == 112256, "quinary fixture") + alpha, beta, gamma = parameters(5) + require( + Fraction(16, 25) * (alpha - 2 * beta + gamma + 1) != 192, + "wrong last eigenvalue mutant survived", + ) + require( + Fraction(16, 25) * (alpha - beta + gamma) != 192, + "missing negative coefficient mutant survived", + ) + joint = Fraction(numerator(5, 1), (25 - 1) * (25 - 5)) + marginal = Fraction(4 * 21, (25 - 1) * 5) + require(joint == Fraction(2, 5) and joint != marginal**2, "independence control") + _, _, mul = field(2, (1, 1, 1)) + require(mul[2][2] == 3 and (2 * 2) % 4 == 0, "F4 must not be Z/4Z") + return 7 + + +def main(): + specifications = ( + (2, (0, 1)), + (3, (0, 1)), + (2, (1, 1, 1)), + (5, (0, 1)), + (7, (0, 1)), + (2, (1, 1, 0, 1)), + (3, (1, 0, 1)), + ) + domains, transitions, factors = [], 0, 0 + for p, modulus in specifications: + q, sub, mul = field(p, modulus) + states = [ + (a, b, c, d) + for a, b, c, d in product(range(q), repeat=4) + if a != 0 and d != 0 + ] + samples = ( + states + if q <= 5 + else [(1, 0, 0, 1), (1, 1, 0, 1)] + [(1, 1, t, 1) for t in range(1, q)] + ) + transitions += check_identities(q, states, samples, sub, mul) + factors += factor_count_controls(q, sub, mul) + row = { + "q": q, + "states": len(states), + "sources": len(samples), + "GL2_headers": check_headers(q, sub, mul), + } + if q <= 5: + row["numerators_n1_to_n4"] = check_transfer(q, states, sub, mul) + domains.append(row) + root = Path(__file__).resolve().parent + names = ( + "README.md", + "PROOF.md", + "TASK.json", + "SOURCES.json", + "VERIFY.json", + "verify.py", + ) + receipt = { + "domains": domains, + "identity_transition_pairs": transitions, + "literal_factor_tuples": factors, + "polynomial_evaluations": check_polynomials(), + "controls": controls(), + "sha256": { + name: sha256((root / name).read_bytes()).hexdigest() for name in names + }, + } + print("PASS_CORANKONE_ALL_FIELD_LAW " + json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()