From ffd229598f3a1a87437e02c74a459498f257f6d5 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 22:17:59 +0100 Subject: [PATCH] feat(research): prove exact binomial parity suffix norms --- .../README.md | 204 ++++++++++++++++++ .../SOURCES.json | 36 ++++ .../TASK.json | 79 +++++++ .../VERIFY.json | 32 +++ .../verify.py | 191 ++++++++++++++++ 5 files changed, 542 insertions(+) create mode 100644 research/triangular-parity-binomial-suffix/README.md create mode 100644 research/triangular-parity-binomial-suffix/SOURCES.json create mode 100644 research/triangular-parity-binomial-suffix/TASK.json create mode 100644 research/triangular-parity-binomial-suffix/VERIFY.json create mode 100644 research/triangular-parity-binomial-suffix/verify.py diff --git a/research/triangular-parity-binomial-suffix/README.md b/research/triangular-parity-binomial-suffix/README.md new file mode 100644 index 0000000000..40be9dc4c7 --- /dev/null +++ b/research/triangular-parity-binomial-suffix/README.md @@ -0,0 +1,204 @@ +# Exact binomial forward-suffix norms in the parity compiler + +This package proves a scoped all-depth formula. For the exact triangular +Toeplitz parity compiler on `f(z)=1+c z`, at dyadic dimension `N=2^h`, +the largest infinity norm of a forward suffix is + +```text +B_h(|c|) = 1 + sum_{j=0}^{h-1} |c|^(2^j). +``` + +The maximum ranges over every complete-shear cut and every legal interleaving +of the disjoint children. The empty sum at `h=0` gives 1. The statement holds +for every real or complex `c`, without a small-tail assumption. If `c!=0` and +`h>=2`, a proper, nontrivial cut attains it. + +In particular, at `|c|=1` the exact maximum is `1+log_2 N`. The completed +operator has infinity norm 2 when `N>=2`. Brian's complementary +[#4737 forward-prefix theorem](https://github.com/CrocSwap/integer-mult-bounds/pull/4737) +bounds every forward prefix by 2 here. Thus a bounded endpoint and bounded +forward prefixes do not provide a dimension-independent forward-suffix bound +at the unit-tail boundary. This is a precision-interface obstruction for this +specific compiler, not a supplier or multiplication theorem. No new kappa is +claimed. + +## Model and predecessor boundary + +Use the exact parity factorization in Vlado Vojdanovski's +[#1673](https://github.com/CrocSwap/integer-mult-bounds/pull/1673), retained in +[`SHALLOW-TOEPLITZ.md`, section 3](../unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md). +For a unit symbol, write `f(z)=e(z^2)+z o(z^2)` and, modulo `z^(N/2)`, set + +```text +k=o/e, s=e-z o^2/e, +T = L diag(E,S) U, +U = [ I ZK ; 0 I ], L = [ I 0 ; K I ], +E=T(e), S=T(s), K=T(k). +``` + +These blocks use even/odd coordinate order. The circuit applies `U`, then the +two child programs in any order-preserving interleaving, then `L`. A macro is +a whole completed shear. Restored logical coordinates or physical coordinate +permutations have the same infinity norm. Include both endpoint cuts. If `P` +has executed and `Q` remains, the convention is `T=QP`. + +Brian's [#4731](https://github.com/CrocSwap/integer-mult-bounds/pull/4731), +head `3fcaa4d4c0568ce474c593d0882296ff43d3705a`, proves the common bound +`1/(1-eta)` for the four macro-cut operators at tail `eta<1`, with a +four-wire binomial suffix of norm `7/4` at `c=1/2`. Its sharpness witness uses +inverse operators and does not give an exact all-depth forward-suffix law. +The new contribution is that law and its unit-tail logarithmic obstruction. +The predecessor results are cited inputs, not re-verification deliverables. + +## Proof + +Let `M_h(c)` be the maximum forward-suffix infinity norm over the stated cuts +and schedules. The leaf gives `M_0(c)=1`. For a binomial parent, + +```text +e=1, o=c, k=c, s=1-c^2 z. +``` + +The entire even-child program is the identity. Indeed, splitting the identity +symbol gives `k=0` and two identity children at every level. Thus interleaving +its macros never changes a matrix. The sole nonidentity child is the odd child, +which is itself the binomial program with coefficient `-c^2`. + +At a cut during the child phase, the remaining operator is exactly + +```text +Q = L diag(I,Q_s) = [ I 0 ; c I Q_s ], +``` + +where `Q_s` is any legal odd-child suffix. The even and odd column blocks +are disjoint. Therefore each bottom block row has absolute sum `|c|` plus +the corresponding row sum of `Q_s`. Every `Q_s` has unit diagonal, hence +norm at least one. It follows that + +```text +||Q||_infinity = |c| + ||Q_s||_infinity. +``` + +The remaining cuts are before `U`, with suffix `T_N(1+c z)` of norm +`1+|c|`, and after `L`, with suffix identity. Both are at most the child-phase +maximum, because `M_(h-1)(-c^2)>=1`. Conversely an attaining child cut is a +legal parent cut after `U`; finishing an identity child is always possible. +Thus, for every `h>=1`, + +```text +M_h(c) = |c| + M_(h-1)(-c^2). +``` + +Iteration gives the asserted formula for all complex `c`. This argument +covers every legal interleaving, rather than assuming a serial schedule. + +An explicit attaining cut runs all right shears along the all-odd descendant +chain before running any left shear on that chain. Its suffix's last row, in +zero-based original coordinates, has diagonal entry 1 and entries + +```text +column N-1-2^j: c_j, 0<=j=1`, `c_j=-c^(2^j)`, so its row sum is +exactly `B_h(|c|)`. At `h>=2` and `c!=0`, the already executed root `U` is +nonidentity. The unexecuted root `L` is also nonidentity; since it occupies the +opposite off-diagonal block, the prefix has not reached the endpoint. Hence +this is a proper, nontrivial cut. At `h=1` the root `U` is identity, which is +why the nontrivial-cut assertion excludes that case. + +For fixed `0<=rho<1`, the finite sums converge and satisfy +`B_h(rho)<=1+rho/(1-rho)`. At `rho=1`, the exact value is `1+h`. +For `rho>1` and `h>=1`, the last summand gives +`B_h(rho)>=rho^(N/2)`, while the completed norm stays `1+rho`. These are +direct consequences of the same formula, not claims about other symbols or +other implementations. + +## Exact finite evidence and reproduction + +The standard-library checker constructs literal parity matrices independently +of the formula and enumerates all reachable `(P,Q)` matrix pairs bottom-up. +At each node every pair of child cuts occurs in some legal interleaving, so +the Cartesian product covers all schedules without listing equivalent ones. +It verifies `QP=T` at each constructed cut and compares the maximum suffix +norm and an attaining last row with the closed form. It imports no predecessor +executable code. + +The fixed domain is `c` in `{0,1,-1,2,-2,1/2,-1/2,3/2}` and `h=0,...,5`. +These 48 rational fixtures enumerate 223 distinct cut pairs, counted separately +for each fixture. Eight controls cover a wrong Schur sign, a missing left +shear, reversed factor order, an endpoint-only bound, extending the binomial +formula to different support, and three invalid-domain inputs. Explicit +checks remain active under `-O`. The script emits a generated receipt binding +the five package files by SHA256. No receipt is hand-written or committed. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/triangular-parity-binomial-suffix +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/triangular-parity-binomial-suffix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/triangular-parity-binomial-suffix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/triangular-parity-binomial-suffix --check-source-history +``` + +Expected direct marker: `PASS_BINOMIAL_SUFFIX fixtures=48 controls=8`. +For `c=1/2`, dimensions 4, 8, 16 and 32 give exact maxima `7/4`, `29/16`, +`465/256` and `119041/65536`. At `c=1`, the corresponding maxima are 3, 4, 5 +and 6. The written induction supplies the all-depth complex statement; +finite rational checks do not establish it by themselves. + +## Limits and code constraints + +No cuts inside a shear, rounded arithmetic, Gaussian gauge conversion, +fixed-tape costs, compiler admission, full selected replay or formal proof +kernel are covered. This theorem does not contradict the retained strict +`eta<1` stability assumptions. No universal suffix optimum over all symbols +with a specified tail budget is asserted. + +The verifier has no recursion, dynamic imports, network calls or subprocesses. +Functions fit within 60 lines. Fixed fixtures enforce `N<=32`; the bottom-up +tree has at most 63 entries and each node permits at most 256 cut pairs. +Python's managed allocations and exact-rational temporaries are a documented +deviation from fixed-allocation operation. This finite checker has bounded +collection capacities and no exposed input interface. If the finite fixture +domain grows, its matrix, cut-count and rational bit-size bounds need review +before changing these limits. Warning-as-error and optimized replay provide +the available standard-library diagnostics; no additional linter is installed +or run here. + +## Open next questions + +What is the sharp forward-suffix envelope over *all* symbols with tail l1 at +most `eta<1`? The binomial lower envelope here and #4731's common upper +envelope leave a gap. It matters for a one-sided precision ledger. A feasible +first step is an exact four-wire optimization with independent even/odd +coefficients, followed by a row invariant that preserves their correlation. +The blocker is that the simple scalar recurrence here uses the identity even +child and does not apply to a general symbol. No further search is included. + +## Sources, overlap and credit + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision +7. [SOURCES.json](SOURCES.json) pins historical catalogue/selected provenance, +the retained factorization, and Brian's two predecessor notes. None is an +executable input to this self-contained checker. The original card's historical +baseline schema is stale; the current selected source-binding orientation +passed, without running a native or operator replay. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132795) +followed live open/own PR lists, recent handoffs and active discussions, +distinctive-term searches of every tracked main-branch package README, merged +PR searches and a local reservation. The card overlap report explicitly has +sparse local omissions; the separate Git-object README searches cover that +textual gap for the target terms. These searches do not prove novelty outside +their coverage. Concurrent signed finite-prefix, superunit forward-prefix, +and internal FFT-cut claims study different questions. + +This result was produced by Nick Petalas. Credit Vlado Vojdanovski for the +retained parity compiler, Cinna Davis for its later Gaussian caller, Brian for +the four-cut envelope and forward-prefix theorem, James Reed for the +one-level tail accounting and finite-prefix examples, and the predecessor +lineage retained in their packages. Their files and credits are unchanged. +New work is Apache-2.0. Independent human and formal proof-kernel review are +unclaimed. diff --git a/research/triangular-parity-binomial-suffix/SOURCES.json b/research/triangular-parity-binomial-suffix/SOURCES.json new file mode 100644 index 0000000000..c3a9173bf0 --- /dev/null +++ b/research/triangular-parity-binomial-suffix/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md", + "usage": "provenance", + "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be", + "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310" + }, + { + "path": "research/triangular-parity-uniform-prefix/README.md", + "usage": "provenance", + "git_blob": "6e64fb48fbd33b9742f0ba81de77bfb661b80403", + "sha256": "dd0259414df08b5b462cec450df5a0618c30ba112ddf87b2acbb2e39a1c69414" + }, + { + "path": "research/triangular-parity-forward-bound/README.md", + "usage": "provenance", + "git_blob": "d008710585a897b9b568e74c7b867d8c784e4aa8", + "sha256": "745c2105fc614e6ba453327a37e483b808425a40ce3e2b44e2643b0ea1db3781" + } + ] +} diff --git a/research/triangular-parity-binomial-suffix/TASK.json b/research/triangular-parity-binomial-suffix/TASK.json new file mode 100644 index 0000000000..58e9b1299b --- /dev/null +++ b/research/triangular-parity-binomial-suffix/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "Prove the exact all-depth maximum forward-suffix infinity norm for f(z)=1+c z under the retained parity macro compiler, over all child interleavings.", + "scope_change_reason": "Replace predecessor re-verification with a new closed-form precision-interface theorem and the critical unit-tail logarithmic obstruction.", + "bottleneck_link": "A sharp suffix envelope constrains one-sided precision accounting for the triangular compiler used by the Gaussian caller. This is a scoped side result, not supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original formula and package it; do not expand the coefficient search.", + "outcome": "completed", + "evidence": "Written recurrence proof and 48 exact rational fixtures, 223 enumerated cut pairs and eight failure/domain controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the sharp forward-suffix envelope over all unit symbols with tail l1 at most eta<1?", + "why_it_matters": "It could tighten the one-sided macro precision ledger beyond the common four-cut bound.", + "first_step": "Optimize the four-wire even/odd coefficient split exactly and derive a correlation-preserving row invariant.", + "blocked_by": "The binomial recurrence requires an identity even child; a general symbol has two nontrivial children." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132795", + "related_claims": "Signed n=8 finite-prefix, superunit forward-prefix and internal FFT-cut claims have distinct domains or operators.", + "coverage_limit": "Sparse local notes are incomplete; separate git grep searches read all tracked main README blobs for distinctive target terms." + } +} diff --git a/research/triangular-parity-binomial-suffix/VERIFY.json b/research/triangular-parity-binomial-suffix/VERIFY.json new file mode 100644 index 0000000000..382510e9be --- /dev/null +++ b/research/triangular-parity-binomial-suffix/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": "Exact binomial suffix maxima, all cut pairs, attaining rows, endpoint identities and eight controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite domain and controls with assertions disabled." + } + ] +} diff --git a/research/triangular-parity-binomial-suffix/verify.py b/research/triangular-parity-binomial-suffix/verify.py new file mode 100644 index 0000000000..640ad5fc53 --- /dev/null +++ b/research/triangular-parity-binomial-suffix/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the binomial suffix theorem. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction as F +from hashlib import sha256 +import json +from pathlib import Path + +MAX_N = 32 +MAX_STATES = 256 + + +def require(ok, message): + if not ok: + raise AssertionError(message) + + +def identity(n): + return tuple(tuple(F(i == j) for j in range(n)) for i in range(n)) + + +def multiply(a, b): + n = len(a) + rows = [] + for row in a: + active = tuple((k, value) for k, value in enumerate(row) if value) + rows.append(tuple(sum((v * b[k][j] for k, v in active), F(0)) + for j in range(n))) + return tuple(rows) + + +def norm(a): + return max(sum(map(abs, row)) for row in a) + + +def toeplitz(f): + return tuple(tuple(f[i - j] if i >= j else F(0) + for j in range(len(f))) for i in range(len(f))) + + +def diagonal(a, b): + m = len(a) + return tuple(tuple(a[i][j] if i < m and j < m else + b[i - m][j - m] if i >= m and j >= m else F(0) + for j in range(2 * m)) for i in range(2 * m)) + + +def logical_order(a): + n = len(a) + position = tuple(i // 2 + (n // 2 if i % 2 else 0) for i in range(n)) + return tuple(tuple(a[i][j] for j in position) for i in position) + + +def split(f, wrong_sign=False): + m = len(f) // 2 + e, o = f[::2], f[1::2] + k = [F(0)] * m + for i in range(m): + k[i] = o[i] - sum((e[j] * k[i - j] for j in range(1, i + 1)), F(0)) + s = list(e) + for i in range(1, m): + correction = sum((o[j] * k[i - 1 - j] for j in range(i)), F(0)) + s[i] += correction if wrong_sign else -correction + left, right = [list(r) for r in identity(2 * m)], [list(r) for r in identity(2 * m)] + for i in range(m): + for j in range(i + 1): + left[m + i][j] = k[i - j] + if i > j: + right[i][m + j] = k[i - j - 1] + return e, tuple(s), tuple(map(tuple, left)), tuple(map(tuple, right)) + + +def all_cuts(f): + """Bottom-up exact (prefix, suffix) pairs for all child interleavings.""" + n = len(f) + if not (1 <= n <= MAX_N and n & (n - 1) == 0 and f[0] == 1): + raise ValueError("expected a bounded unit dyadic symbol") + symbols = [f] + for index in range(2 * n - 1): + node = symbols[index] + if len(node) > 1: + e, s, _, _ = split(node) + symbols.extend((e, s)) + require(len(symbols) == 2 * n - 1, "full binary tree capacity") + states = {} + for node in reversed(symbols): + size = len(node) + unit, target = identity(size), toeplitz(node) + if size == 1: + states[node] = {(unit, unit)} + continue + e, s, left, right = split(node) + endpoint = logical_order(multiply(left, multiply(diagonal(toeplitz(e), toeplitz(s)), right))) + require(endpoint == target, "literal parity endpoint") + pairs = {(unit, target), (target, unit)} + require(len(states[e]) * len(states[s]) + 2 <= MAX_STATES, "cut capacity") + for pe, qe in states[e]: + for ps, qs in states[s]: + p = logical_order(multiply(diagonal(pe, ps), right)) + q = logical_order(multiply(left, diagonal(qe, qs))) + require(multiply(q, p) == target, "suffix times prefix") + pairs.add((p, q)) + states[node] = pairs + return states[f] + + +def prediction(c, depth): + return F(1) + sum((abs(c) ** (2 ** j) for j in range(depth)), F(0)) + + +def witness_row(c, depth): + n = 2 ** depth + row = [F(0)] * n + row[-1] = F(1) + coefficient = c + for j in range(depth): + row[n - 1 - 2 ** j] = coefficient + coefficient = -coefficient ** 2 + return tuple(row) + + +def check_fixture(c, depth): + n = 2 ** depth + f = (F(1),) if n == 1 else (F(1), c, *([F(0)] * (n - 2))) + pairs = all_cuts(f) + bound = prediction(c, depth) + maximum = max(norm(q) for _, q in pairs) + require(maximum == bound, "exact binomial forward-suffix maximum") + witnesses = [(p, q) for p, q in pairs if q[-1] == witness_row(c, depth)] + require(bool(witnesses), "literal attaining last row") + if depth >= 2 and c: + require(any(p != identity(n) and p != toeplitz(f) for p, _ in witnesses), + "attaining proper nontrivial cut") + require(norm(toeplitz(f)) == (F(1) if depth == 0 else F(1) + abs(c)), + "completed endpoint norm") + if abs(c) == 1: + require(maximum == 1 + depth, "critical logarithmic law") + return {"c": str(c), "depth": depth, "n": n, "cut_pairs": len(pairs), + "maximum_suffix_norm": str(maximum)} + + +def controls(): + passed = [] + f = (F(1), F(1, 2), F(0), F(0)) + e, s, left, right = split(f, wrong_sign=True) + require(logical_order(multiply(left, multiply(diagonal(toeplitz(e), toeplitz(s)), right))) + != toeplitz(f), "wrong Schur sign rejection") + passed.append("wrong Schur sign") + e, s, left, right = split(f) + middle = diagonal(toeplitz(e), toeplitz(s)) + require(logical_order(multiply(middle, right)) != toeplitz(f), "missing left shear rejection") + passed.append("missing left shear") + require(logical_order(multiply(right, multiply(middle, left))) != toeplitz(f), + "reversed order rejection") + passed.append("reversed order") + require(max(norm(q) for _, q in all_cuts(f)) > norm(toeplitz(f)), + "endpoint is not a suffix bound") + passed.append("endpoint-only bound") + shifted = (F(1), F(0), F(1, 2), F(0)) + require(max(norm(q) for _, q in all_cuts(shifted)) != prediction(F(0), 2), + "binomial support hypothesis is necessary") + passed.append("non-binomial support") + for bad in ((F(1),) * 3, (F(2), F(0)), (F(1),) * 64): + try: + all_cuts(bad) + except ValueError: + passed.append(f"invalid domain of length {len(bad)}") + continue + raise AssertionError("invalid symbol accepted") + return passed + + +def main(): + coefficients = tuple(map(F, (0, 1, -1, 2, -2))) + (F(1, 2), F(-1, 2), F(3, 2)) + records = [check_fixture(c, depth) for c in coefficients for depth in range(6)] + passed_controls = controls() + pair_count = sum(record["cut_pairs"] for record in records) + root = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"claim_type": "scoped proof with finite corroboration", + "fixtures": records, "cut_pairs": pair_count, "controls": passed_controls, + "source_sha256": hashes}, indent=2)) + print(f"PASS_BINOMIAL_SUFFIX fixtures={len(records)} controls={len(passed_controls)}") + + +if __name__ == "__main__": + main()