diff --git a/research/oneway-all-field-closed-form/PROOF.md b/research/oneway-all-field-closed-form/PROOF.md new file mode 100644 index 0000000000..6ccfc8cc73 --- /dev/null +++ b/research/oneway-all-field-closed-form/PROOF.md @@ -0,0 +1,116 @@ +# All-field closed form for one-way coupled full guards + +This scoped counting proof was produced by Nick Petalas. Apache-2.0. + +Let K be a finite field of order q, m>=2, and n=m-1. Let U,V be rank-one +idempotents on K^m with UV nonzero and VU=0. Set P=I-U and Q=I-V. +Choose a complete header G uniformly in GL_m(K). A request passes when +every leading principal minor of its conjugate, through order m-1, is +nonzero. Define + +```text +alpha=(q^2-q+1)^2, beta=q^3-q+1, gamma=q^3-q^2+1, +D=(q^m-1)(q^m-q)q^(2m-4). +``` + +The exact joint passing fraction is C(q,m)/D, where + +```text +C(q,m) = (q-1)/q^2 * [(q-1)alpha^n - (q-2)beta^n - gamma^n]. (1) +``` + +Thus the number of complete passing headers is C(q,m)|GL_(m-2)(K)|. +This replaces #4274's all-field transfer by a closed formula. Its binary +specialization was already proved there; the new claim is the all-field +expression. There is no new kappa or supplier claim. + +## Cited input and changed initial matrix + +Nick Petalas's [#4274 transfer theorem](https://github.com/CrocSwap/integer-mult-bounds/pull/4274), +retained in the main-branch source pinned by SOURCES.json, identifies +normalized pairs YX=L, with L=[[1,1],[0,1]], and equal header fibers. +The partial Gram sum A must have A_11,A_22 different from 1 until its +last increment. For any 2 by 2 matrix H let w(H) equal 2q^2-1 at zero, +q-1 at nonzero rank one, and zero at rank two. + +Make the substitution B=L-A. Its diagonal restriction is exactly that +both diagonal entries of B are nonzero. The initial state is B=L and +the terminal weight is h(B)=w(B). Negation preserves w. Consequently + +```text +C(q,m) = (T^n h)(L), +(Tf)(B) = sum_(C with nonzero diagonal) w(B-C)f(C). +``` + +The transfer and header-fiber theorem are predecessor credit, not new +results or independent audits in this contribution. + +## Solving the invariant coordinates + +Use the three-function identities proved in Nick Petalas's +[#4747, PROOF.md, Three invariant functions](https://github.com/petalas/integer-mult-bounds/blob/f51dcebce79b8b8958427a9a9b7bc8feca352c9d/research/corankone-all-field-law/PROOF.md). +This is an exact external theorem citation at commit +f51dcebce79b8b8958427a9a9b7bc8feca352c9d; no source code from that +pending package is imported or replayed. Put r=q-1 and +z(B)=1_(B_12=0)+1_(B_21=0). The cited identities are + +```text +T1 = alpha 1, +Tz = 2r^3 1 + beta z, +Th = r^2(q^2-3q+4)1 - r^2 z + gamma h. (2) +``` + +Write T^n h=a_n 1+b_n z+c_n h. This representation need not be unique +on small fields; the following coefficient solution still proves the +function identity. From (2), starting at (a_0,b_0,c_0)=(0,0,1), + +```text +a_(n+1) = alpha a_n + 2r^3 b_n + r^2(q^2-3q+4)c_n, +b_(n+1) = beta b_n - r^2 c_n, +c_(n+1) = gamma c_n. +``` + +Direct substitution gives, for every integer n>=0, + +```text +q^2 a_n = r^2 alpha^n + 2r beta^n - r(q+1)gamma^n, +q^2 b_n = -qr(beta^n-gamma^n), +c_n = gamma^n. (3) +``` + +For clarity, the polynomial identities needed in this substitution are + +```text +beta-gamma=qr, +alpha-beta=qr^3, +(q+1)(alpha-gamma)=q r[2r^2+q(q^2-3q+4)]. +``` + +The initial coefficients in (3) are 0,0,1. The last recurrence is +immediate; the first two follow from these identities. Induction proves +(3) without a characteristic restriction. All divisions here occur in +the rational counting coefficients, not in K, so characteristic two is +included. + +Finally, z(L)=1 and h(L)=0 because L has one zero off-diagonal entry +and is invertible. Hence C=a_n+b_n. Combining (3) yields (1). +The cited equal-fiber theorem supplies the probability denominator and +the complete-header count. This proves the stated all-field result. + +## Boundary examples and scope + +At m=2 the numerator simplifies to +(q-1)^2(q^2-3q+3). For q=2,3,4,5 the passing fractions are respectively +1/6, 1/4, 7/20, 13/30. At q=3,m=3 the fraction is 53/351, agreeing +with #4274's one-way transfer example. For q=5 the new formula is + +```text +C(5,m)=(4/25)[4*441^n-3*121^n-101^n]. +``` + +Only the closed form is new. No negative-correlation theorem for odd +fields, classification of two-way coupling, restricted header theorem, +or physical implementation is claimed. Selection, emission, dispatch, +dirty restoration, precision and stock costs are unknown. The proof +uses the cited all-field invariant identity as a predecessor theorem; +independent human and formal proof-kernel review are unclaimed. diff --git a/research/oneway-all-field-closed-form/README.md b/research/oneway-all-field-closed-form/README.md new file mode 100644 index 0000000000..400296d1a8 --- /dev/null +++ b/research/oneway-all-field-closed-form/README.md @@ -0,0 +1,103 @@ +# All-field closed form for one-way coupled full guards + +This scoped counting proof was produced by Nick Petalas. Apache-2.0. + +## Scope and evidence + +For rank-one idempotents U,V over F_q^m with UV nonzero and VU=0, the +two requests I-U,I-V use one complete, uniformly weighted GL_m header. +A request passes when every leading principal minor through its rank +is nonzero. Put n=m-1 and + +```text +alpha=(q^2-q+1)^2, beta=q^3-q+1, gamma=q^3-q^2+1. +``` + +The exact normalized passing-pair numerator is + +```text +C(q,m)=(q-1)/q^2 * [(q-1)alpha^n-(q-2)beta^n-gamma^n]. +``` + +Divide by `(q^m-1)(q^m-q)q^(2m-4)` for the probability, for every finite +field and every m>=2. At q=5 this is `(4/25)[4*441^n-3*121^n-101^n]`. +The m=2 passing fractions for q=2,3,4,5 are 1/6, 1/4, 7/20, 13/30. + +[#4274](https://github.com/CrocSwap/integer-mult-bounds/pull/4274) supplied +the all-field transfer and the binary closed form. The new step in +[PROOF.md](PROOF.md) changes the initial matrix in +[#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747)'s +three-function invariant system and solves its coefficient recurrence. +Both predecessor theorems are cited, not audited or claimed as new. + +The self-contained verifier checks 4,095 integer-parameter coefficient +comparisons at 2<=q<=64 and 0<=n<=64, and 36 raw partial-Gram transfer +cases over F2,F3,F4,F5 at 0<=n<=8. It explicitly visits 182,048 +source/target state pairs. It also enumerates every complete GL2 header +over F2,F3,F4,F5,F7,F8,F9, a total of 12,018 headers, including extension +fields. Six semantic controls and four input-bound rejections remain +active with assertions disabled. The generated stdout receipt binds all +six package files by SHA256; no handwritten receipt is stored. + +This algebraic side result changes the `formal-interface-lemma` card's +premise, as recorded in [TASK.json](TASK.json). [SOURCES.json](SOURCES.json) +pins the original catalogue, selected record and retained #4274 proof as +historical provenance. There are no live external code inputs or Python +dependencies. The exact external #4747 theorem citation is at commit +`f51dcebce79b8b8958427a9a9b7bc8feca352c9d`; no pending Git object is +needed to execute the package or its publication preflight. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/oneway-all-field-closed-form/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-all-field-closed-form/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-all-field-closed-form +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-all-field-closed-form --check-source-history +``` + +Replace the local interpreter path with another CPython 3.12 installation +elsewhere. Expected markers are `PASS_ONEWAY_ALL_FIELD_CLOSED_FORM`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The last command requires a publication commit and full Git history. +The direct verifier writes nothing and can run from a Git-free package copy. + +## Limits and implementation constraints + +The universal statement uses the written argument and the cited invariant +theorem. Finite execution corroborates its stated domains. Only two fixed +one-way coupled rank-one kernels and complete uniform headers are covered. +Physical selection, emission, dispatch, dirty restoration, precision and +stock costs remain unknown. No new kappa, supplier admission or complete +multiplication theorem follows. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and selected operator replay are unrun. + +The verifier has no recursion or dynamic code loading. Its largest state +matrix is 400 by 400, replay length is at most eight, field tables have at +most 81 entries, and coefficient checks stop at q=64,n=64. Functions stay +below 60 lines. CPython allocation and iterator dispatch are managed-runtime +deviations from Power of Ten rules 3 and 9, bounded by these fixed domains. +No plugin or callback registry is used. Normal and optimized warning-strict +commands exercise the same explicit checks. A fixed-capacity native replay +would require a separately specified integer capacity and is not supplied. + +## Open next questions + +1. Does the one-way joint law have strict negative correlation over every + finite field? Compare this formula with #4227's squared marginal after + checking live claims. The odd-field inequality is not proved here. +2. Can a named odd-field producer use a fully charged one-way shared-header + caller? Pin its kernel pair and header domain, then price selection, + emission, dispatch and dirty return. Unknown physical costs block any + supplier consequence. Structured first steps and blockers are in TASK.json. + +## Credit + +Nick Petalas's #4274/#4261 supplied the transfer and equal-header fibers; +#4747 supplied the all-field invariant identities; #4227 supplied the +corank-one guard and marginal context. The binary formula and small prime +examples are predecessor credit. Cinna Davis supplied the BIT request +context; source527, commdata2338 and Jose Manuel retain the normalizer and +recursive-closure lineage credit. No predecessor files are modified. diff --git a/research/oneway-all-field-closed-form/SOURCES.json b/research/oneway-all-field-closed-form/SOURCES.json new file mode 100644 index 0000000000..d237fd16f8 --- /dev/null +++ b/research/oneway-all-field-closed-form/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/oneway-corankone-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "5361c339bd172e13e0a2383ba734fa6e16f1082e", + "sha256": "1b13487af3fb2c0822f5cf417e017e507d74d85045c0df6a44997993eaa18a96" + } + ] +} diff --git a/research/oneway-all-field-closed-form/TASK.json b/research/oneway-all-field-closed-form/TASK.json new file mode 100644 index 0000000000..d28820b2dd --- /dev/null +++ b/research/oneway-all-field-closed-form/TASK.json @@ -0,0 +1,113 @@ +{ + "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": "An exact all-field closed form for two one-way coupled corank-one full-guard requests, for every finite field and m>=2.", + "scope_change_reason": "The assignment asks for original successor work. This algebraic side result extends the all-field transfer of PR4274 using the invariant identity of PR4747; it is not an audit or a selected-caller formalization.", + "bottleneck_link": "Exact joint header densities describe simultaneous request admission. A physical producer and complete caller cost are still required before a supplier consequence.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified closed formula, or at a documented obstruction within a 60-minute budget.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-field expression using cited transfer and invariant theorems. verify.py prints a file-bound receipt for 4095 coefficient comparisons, 36 raw-transfer cases and complete GL2 header counts over seven fields.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does one-way coupled full-guard admission have strict negative correlation over every finite field?", + "why_it_matters": "A joint density alone does not determine whether sharing a header is more favorable than multiplying marginals.", + "first_step": "Compare the new three-power formula with the corank-one marginal from PR4227, after checking active claims.", + "blocked_by": "No inequality for odd fields is supplied here." + }, + { + "question": "Can a named odd-field producer use a fully charged one-way shared-header caller?", + "why_it_matters": "A counting result removes no paid work until its producer and consumer are realized.", + "first_step": "Pin one actual kernel pair, its header domain and the complete selection/emission/dispatch/return ledger.", + "blocked_by": "Preparation, routing, dirty restoration, precision and stock costs remain unknown." + } + ], + "predecessor_theorems": [ + { + "pr": 4274, + "head": "497b8862d98ab57e33b262fa2631afc5a559257f", + "scope": "One-way transfer and equal header fibers; retained on base main." + }, + { + "pr": 4747, + "head": "f51dcebce79b8b8958427a9a9b7bc8feca352c9d", + "scope": "Three invariant function identities; exact external theorem citation, not a code or Git-object dependency." + } + ] +} diff --git a/research/oneway-all-field-closed-form/VERIFY.json b/research/oneway-all-field-closed-form/VERIFY.json new file mode 100644 index 0000000000..019d9818fe --- /dev/null +++ b/research/oneway-all-field-closed-form/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": "New formula versus the three-coordinate recurrence, raw transfer, complete GL2 headers over seven fields, semantic and boundary controls; generated SHA256 receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit checks and file-bound receipt with Python assertions disabled." + } + ] +} diff --git a/research/oneway-all-field-closed-form/verify.py b/research/oneway-all-field-closed-form/verify.py new file mode 100644 index 0000000000..d8c3a1fbd0 --- /dev/null +++ b/research/oneway-all-field-closed-form/verify.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the all-field one-way full-guard formula.""" + +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(q): + """Tables for seven explicitly bounded prime and extension fields.""" + specs = {2: (2, (0, 1)), 3: (3, (0, 1)), 4: (2, (1, 1, 1)), + 5: (5, (0, 1)), 7: (7, (0, 1)), 8: (2, (1, 1, 0, 1)), + 9: (3, (1, 0, 1))} + require(q in specs, "unsupported field order") + p, modulus = specs[q] + degree = len(modulus) - 1 + digits = tuple(tuple((a // p**i) % p for i in range(degree)) + for a in range(q)) + add, mul = [], [] + for a, b in product(digits, repeat=2): + add.append(sum(((a[i] + b[i]) % p) * p**i for i in range(degree))) + coeff = [0] * (2 * degree - 1) + for i, j in product(range(degree), repeat=2): + coeff[i + j] = (coeff[i + j] + a[i] * b[j]) % p + for k in range(2 * degree - 2, degree - 1, -1): + for j in range(degree): + coeff[k - degree + j] -= coeff[k] * modulus[j] + mul.append(sum((coeff[i] % p) * p**i for i in range(degree))) + neg = tuple(next(b for b in range(q) if add[a * q + b] == 0) + for a in range(q)) + require(all(any(mul[a * q + b] == 1 for b in range(q)) + for a in range(1, q)), "nonunit in field table") + return tuple(add), tuple(mul), neg + + +def subtract(a, b, q, add, neg): + return add[a * q + neg[b]] + + +def determinant(matrix, q, add, mul, neg): + a, b, c, d = matrix + return subtract(mul[a * q + d], mul[b * q + c], q, add, neg) + + +def closed(q, n): + require(2 <= q <= 128 and 0 <= n <= 128, "formula replay bounds") + alpha = (q * q - q + 1)**2 + beta, gamma = q**3 - q + 1, q**3 - q * q + 1 + numerator = (q - 1) * ((q - 1) * alpha**n + - (q - 2) * beta**n - gamma**n) + require(numerator % (q * q) == 0, "nonintegral numerator") + return numerator // (q * q) + + +def transfer_cases(q): + """Use the cited raw partial-Gram walk, with no invariant quotient.""" + add, mul, neg = field(q) + states = tuple(a for a in product(range(q), repeat=4) + if a[0] != 1 and a[3] != 1) + weights = [] + for a in product(range(q), repeat=4): + weights.append(2 * q * q - 1 if not any(a) else + q - 1 if determinant(a, q, add, mul, neg) == 0 else 0) + transitions, terminal = [], [] + for a in states: + row = [] + for b in states: + delta = tuple(subtract(x, y, q, add, neg) + for x, y in zip(a, b, strict=True)) + index = sum(x * q**(3 - i) for i, x in enumerate(delta)) + row.append(weights[index]) + transitions.append(tuple(row)) + delta = tuple(subtract(x, y, q, add, neg) + for x, y in zip((1, 1, 0, 1), a, strict=True)) + index = sum(x * q**(3 - i) for i, x in enumerate(delta)) + terminal.append(weights[index]) + counts = [int(a == (0, 0, 0, 0)) for a in states] + for n in range(9): + actual = sum(a * b for a, b in zip(counts, terminal, strict=True)) + require(actual == closed(q, n), f"raw transfer mismatch q={q}, n={n}") + if n < 8: + counts = [sum(w * c for w, c in zip(row, counts, strict=True)) + for row in transitions] + return 9, len(states)**2 + + +def complete_gl2(q): + """Literal first guards after conjugating U=e1(e1+e2)^T, V=e2e2^T.""" + add, mul, neg = field(q) + total = good = 0 + for a, b, c, d in product(range(q), repeat=4): + det = determinant((a, b, c, d), q, add, mul, neg) + if det == 0: + continue + total += 1 + # Clear the common nonzero determinant in each conjugated guard. + u11 = mul[a * q + subtract(d, c, q, add, neg)] + v11 = mul[b * q + neg[c]] + good += (subtract(det, u11, q, add, neg) != 0 + and subtract(det, v11, q, add, neg) != 0) + require(total == (q * q - 1) * (q * q - q), "GL2 size mismatch") + require(good == closed(q, 1), "literal GL2 header mismatch") + return {"q": q, "headers": total, "passing": good, + "fraction": str(Fraction(good, total))} + + +def coefficient_cases(): + """Check the new closed expression against its three-coordinate update.""" + cases = 0 + for q in range(2, 65): + r = q - 1 + alpha, beta, gamma = (q * q - q + 1)**2, q**3 - q + 1, q**3 - q*q + 1 + a, b, c = 0, 0, 1 + for n in range(65): + require(a + b == closed(q, n), "coefficient solution mismatch") + require(a + 2*b == Fraction(r*r, q*q) + * (alpha**n - 2*beta**n + gamma**n), "orthogonal boundary") + cases += 1 + a, b, c = (alpha*a + 2*r**3*b + r*r*(q*q-3*q+4)*c, + beta*b-r*r*c, gamma*c) + return cases + + +def controls(): + q, n = 3, 1 + alpha, beta, gamma = 49, 25, 19 + require(closed(q, n) != Fraction(2, 9)*(2*alpha-2*beta-gamma), + "beta coefficient mutation escaped") + require(closed(q, n) != Fraction(2, 9)*(2*alpha-beta+gamma), + "gamma sign mutation escaped") + require(closed(q, n) != Fraction(4, 9)*(2*alpha-beta-gamma), + "prefactor mutation escaped") + require(closed(2, 1) == 1, "one-way binary boundary") + require(Fraction(1, 6) != Fraction(1, 2)**2, "independence control") + add, _, _ = field(4) + require(add[1*4+1] == 0 and (1+1) % 4 != 0, "F4 confused with Z/4Z") + for q, n in ((1, 1), (129, 1), (2, -1), (2, 129)): + try: + closed(q, n) + except ValueError: + continue + raise ValueError("formula bound did not reject") + return 10 + + +def main(): + coefficient_count = coefficient_cases() + transfer_count = transitions = 0 + for q in (2, 3, 4, 5): + cases, pairs = transfer_cases(q) + transfer_count += cases + transitions += pairs + headers = [complete_gl2(q) for q in (2, 3, 4, 5, 7, 8, 9)] + require(Fraction(closed(3, 2), (27-1)*(27-3)*9) == Fraction(53, 351), + "cited one-way ternary boundary") + root = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py") + receipt = {"status": "PASS_ONEWAY_ALL_FIELD_CLOSED_FORM", + "coefficient_cases": coefficient_count, + "raw_transfer_cases": transfer_count, + "source_target_pairs": transitions, + "complete_gl2": headers, "controls": controls(), + "sha256": {name: sha256((root/name).read_bytes()).hexdigest() + for name in names}} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()