From 884f96d112e0002c24000b3d89b82fca142e0fc9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 22:50:51 +0100 Subject: [PATCH] feat(research): prove the full CRT arena batch threshold --- research/crt-arena-batch-threshold/PROOF.md | 133 ++++++++++++++++ research/crt-arena-batch-threshold/README.md | 80 ++++++++++ .../crt-arena-batch-threshold/RESULT.json | 55 +++++++ .../crt-arena-batch-threshold/SOURCES.json | 24 +++ research/crt-arena-batch-threshold/TASK.json | 80 ++++++++++ .../crt-arena-batch-threshold/VERIFY.json | 36 +++++ research/crt-arena-batch-threshold/verify.py | 149 ++++++++++++++++++ 7 files changed, 557 insertions(+) create mode 100644 research/crt-arena-batch-threshold/PROOF.md create mode 100644 research/crt-arena-batch-threshold/README.md create mode 100644 research/crt-arena-batch-threshold/RESULT.json create mode 100644 research/crt-arena-batch-threshold/SOURCES.json create mode 100644 research/crt-arena-batch-threshold/TASK.json create mode 100644 research/crt-arena-batch-threshold/VERIFY.json create mode 100644 research/crt-arena-batch-threshold/verify.py diff --git a/research/crt-arena-batch-threshold/PROOF.md b/research/crt-arena-batch-threshold/PROOF.md new file mode 100644 index 0000000000..f4aba80664 --- /dev/null +++ b/research/crt-arena-batch-threshold/PROOF.md @@ -0,0 +1,133 @@ +# Full shared-arena batch threshold + +This is a scoped counting theorem about the explicit bill in unpaidmoon's +[PR4650 proof](../crt-arena-root-axis/PROOF.md), at canonical main +`624de9dc66858af0945e5f8a0942488d62280d43`. Its tariffs and arena census are +premises here. The new result classifies the full batch without changing that +bill. No predecessor executable is replayed. + +## Statement + +Let `p >= 2` and `1 <= h <= ell <= p` be integers. Put + +``` +q = p+2, N = 2^h, w = 4q, +A = N^2 + 2Nh^2 + 24Nh + 3N, +J = N(h^2+3h+1), +T = A(26wJ+25w) + 30wJ + 3Nh + 6(2h-1)N + 3, +U = 65536q^3 + 1024q ell^3 + 1024q^2 + + 4[9(ell+2)^2 N + (1+8w^2)T], +B = 8q U, E = 2^(4ell) q^16. +``` + +Thus `B` repeats the complete one-axis charge, including its CRT work and +four networks, on the maximum `8q` axes. In particular every tape action +still pays the optional schoolbook product of two `w`-bit words. + +Then `B < E` except at exactly `(p,ell,h) = (2,1,1)` and `(2,2,2)`. +The least real constant `C` satisfying `B <= C E` throughout this domain is + +``` +C* = 9702312163 / 8589934592. +``` + +It is attained at `(2,2,2)`. These are comparisons of the stated majorant. +An excess of that majorant is not a lower bound on an actual machine. + +## Proof for p >= 3 + +First take `ell = h`, so `q >= max(5,h+2)`. PR4650's explicit-bill lemmas +give, for `h >= 2`, + +``` +U <= 17472q^4 + 36q^2 N + 6109440q^3 N^3 h^2. +``` + +Multiplication by the full batch size gives + +``` +B <= 139776q^5 + 288q^3 N + 48875520q^4 N^3 h^2. +``` + +Each summand is strictly below `E/3`. For the first this is equivalent to +`419328 < N^4 q^11`, which holds already at `N=4,q=5` and is preserved by +increasing either variable. For the second it is +`864 < N^3 q^13`, with the same smallest pair. + +The third comparison is + +``` +146626560 h^2 < 2^h q^12. +``` + +At `h=2,3`, use `q >= 5` and the respective exact comparisons + +``` +586506240 < 976562500, +1319639040 < 1953125000. +``` + +At `h=4`, `q >= 6` gives `2346024960 < 34828517376`. +For `h >= 4`, set `r(h) = 2^h(h+2)^12/h^2`. Then + +``` +r(h+1)/r(h) = 2 ((h+3)/(h+2))^12 (h/(h+1))^2 + >= 2 (4/5)^2 = 32/25 > 1. +``` + +Consequently the `h=4` inequality propagates to every larger `h` using +`q >= h+2`. This proves `B < E` at `ell=h>=2`. + +For `ell=h=1`, PR4650's height-one expansion gives + +``` +U <= 37169148q^3, +B <= 297353184q^4 < 16q^16 = E, +``` + +since `297353184 < 16*5^12` and `q >= 5`. + +Now fix `q,h` and increase `ell`. The only `ell`-dependent terms in `U` +are `1024q ell^3` and `36N(ell+2)^2`. For integer `ell>=1`, + +``` +(ell+1)^3 - 16ell^3 = -15ell^3+3ell^2+3ell+1 <= -8ell^3 < 0, +(ell+3)^2 - 16(ell+2)^2 = -15ell^2-58ell-55 < 0. +``` + +The omitted part of `U` is positive and independent of `ell`, so +`U(ell+1)<16U(ell)`. Multiplication by the fixed `8q` preserves this strict +inequality, while `E(ell+1)=16E(ell)`. The result at `ell=h` therefore +extends to every `ell>=h`, in particular the required `ell<=p`. + +## Exhaustion of p = 2 and sharp constant + +There are exactly three admissible pairs `(ell,h)` when `p=2`. +Substitution into the displayed integers gives + +``` +(ell,h) B E B/E +(1,1) 75548846976 68719476736 590225367/536870912 +(2,1) 75549780608 1099511627776 590232661/8589934592 +(2,2) 1241895956864 1099511627776 9702312163/8589934592 +``` + +The middle ratio is below one. The first exceeds one, and its numerator +when written over `8589934592` is `9443605872 < 9702312163`. All `p>=3` +ratios are below one by the proof above. Hence the last row is the global +maximum and gives the stated least constant. This completes the proof. + +## Consequence and limits + +For every `p>=3`, changing the scalar inventory is unnecessary to fit the +entire batch under this particular allowance. Over the full domain `p>=2`, +the sharp majorant constant is `C*`, and the coarse integer constant two +also suffices. This closes the large-parameter part of PR4650's batch +question with its existing schedule; it does not supply the tighter +word-operation inventory requested there. + +The arena tariff, CRT reconstruction premise and maximum batch size remain +inherited. Reservoir placement, actual arena execution, repair, native lifting, +all-size caller composition and the outer multiplication theorem are separate +obligations. The selected frontier is unchanged. The quantified conclusion is +proved by the inequalities above; finite checker output is corroboration. diff --git a/research/crt-arena-batch-threshold/README.md b/research/crt-arena-batch-threshold/README.md new file mode 100644 index 0000000000..9aff5a3b2c --- /dev/null +++ b/research/crt-arena-batch-threshold/README.md @@ -0,0 +1,80 @@ +# The full shared-arena CRT batch fits from p = 3 + +Scoped counting proof, with exact finite corroboration. No new kappa. + +For the explicit one-axis bill `U` in unpaidmoon's PR4650, repeat its complete +CRT and four-network charge on all `8(p+2)` axes. Retain its schoolbook product +beside every tape action. [PROOF.md](PROOF.md) proves that this full batch is +strictly below `E = 2^(4ell)(p+2)^16` for all integers `p>=3` and +`1<=h<=ell<=p`. The three admissible `p=2` cases are exhausted explicitly. +Exactly `(p,ell,h)=(2,1,1)` and `(2,2,2)` exceed `E`. + +The least uniform constant in `8(p+2)U <= C E` is +`C = 9702312163/8589934592`, attained at `(2,2,2)`. A majorant exceeding an +allowance does not prove an actual machine lower bound. The new conclusion is +that no scalar-inventory change is needed for the large-parameter batch under +this particular allowance, despite the previously displayed small failure. + +## Evidence and reproduction + +The quantified result comes from the written proof. [verify.py](verify.py) +independently forms the full batch, compares a second polynomial expansion, +and checks all 45,759 triples with `2<=p<=64`. The generated, hash-bound +[RESULT.json](RESULT.json) records the exact exceptions, the sharp witness, +63 height inequalities, 64 extension steps and eight rejection controls. +No predecessor executable is run. The verifier authenticates its one live +proof input by SHA256 and Git blob identity. [SOURCES.json](SOURCES.json) +pins the canonical base, catalogue, selected record and inherited bill. + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/crt-arena-batch-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/crt-arena-batch-threshold/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/crt-arena-batch-threshold +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/crt-arena-batch-threshold --check-source-history +``` + +The direct verifier prints `PASS_CRT_ARENA_BATCH_THRESHOLD`. Its checker has +an explicit finite domain; the proof has no `p<=64` restriction. Normal and +optimized checks retain all checks through explicit exceptions. Default replay +does not rewrite the receipt; `--write-result` generates it deliberately. + +## Scope and credit + +Base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [TASK.json](TASK.json) changes `uniform-transfer-audit` into an +original analytic extension of another contributor's open batch question. +The [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133323) +states the proposed threshold and the first-result stopping rule. + +This contribution was produced by Nick Petalas. Credit unpaidmoon for +[PR4650](https://github.com/CrocSwap/integer-mult-bounds/pull/4650)'s one-axis +bill, its majorant lemmas and the batch question, and +[PR4377](https://github.com/CrocSwap/integer-mult-bounds/pull/4377)'s CRT and +rotation tariffs. Credit ToikY for +[PR4192](https://github.com/CrocSwap/integer-mult-bounds/pull/4192)'s arena +census and Cinna Davis for +[PR4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100)'s CRT +construction. Their claims are cited premises, not new verification deliverables. +Predecessor files and attribution are unchanged. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The arena and reconstruction tariffs remain inherited. This does not execute +an arena, implement a tighter scalar inventory, compose reservoir placement or +exceptional repair, admit a supplier, or prove the multiplication theorem. +No Lean, Docker, native replay or full historical suite is required or run. +The selected frontier is unchanged. Python's managed allocation is bounded by +the fixed 64-parameter checker domain; no recursion or unbounded search is used. + +## Open next questions + +1. Can the actual word-level scalar inventory fit constant one at the two + excluded `p=2` corners? Start with the per-record comparisons in PR4192 + section 2. The present majorant excess does not settle that question. +2. Can this full-batch allowance be composed with reservoir placement and the + actual paid repair-key service of PR4795? Begin with one complete entry, + call and exit program, retaining all source-state queries and restoration + charges. Physical movement and all-size caller premises remain external. + +The [structured questions](TASK.json) record relevance, first steps and blockers. diff --git a/research/crt-arena-batch-threshold/RESULT.json b/research/crt-arena-batch-threshold/RESULT.json new file mode 100644 index 0000000000..b2e427ba73 --- /dev/null +++ b/research/crt-arena-batch-threshold/RESULT.json @@ -0,0 +1,55 @@ +{ + "status": "PASS_CRT_ARENA_BATCH_THRESHOLD", + "claim_type": "scoped proof with finite corroboration", + "grid_p_max": 64, + "grid_triples": 45759, + "exceptions": [ + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "sharp_constant": "9702312163/8589934592", + "height_checks": 63, + "extension_checks": 64, + "rejection_controls": 8, + "p2_exhaustion": [ + { + "p": 2, + "ell": 1, + "h": 1, + "batch": 75548846976, + "allowance": 68719476736, + "ratio": "590225367/536870912" + }, + { + "p": 2, + "ell": 2, + "h": 1, + "batch": 75549780608, + "allowance": 1099511627776, + "ratio": "590232661/8589934592" + }, + { + "p": 2, + "ell": 2, + "h": 2, + "batch": 1241895956864, + "allowance": 1099511627776, + "ratio": "9702312163/8589934592" + } + ], + "source_sha256": { + "PROOF.md": "8c9dbbd057811cfbca421234bc9b1f43f71d367a374508231d344c072ed779bb", + "verify.py": "7a484329cd3ac65b1f382193f64335cf4aa472b73066ffb392cecb0866ef7703", + "SOURCES.json": "0e27c0b68888e41ed0670aafab366b4627da9e8c28101647dc81e4b8d4b78689", + "TASK.json": "d9e6430ff9f76e537968719f8828d04cfb5429835bb7cc8c08199ad2e64ee148", + "VERIFY.json": "9b4a6efc1fd154209366b306fee5092dffe4f45e04f76f3d2e17ee3c91a95c30" + } +} diff --git a/research/crt-arena-batch-threshold/SOURCES.json b/research/crt-arena-batch-threshold/SOURCES.json new file mode 100644 index 0000000000..ffe8f58984 --- /dev/null +++ b/research/crt-arena-batch-threshold/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/crt-arena-root-axis/PROOF.md", + "usage": "input", + "git_blob": "e2f7a81d5302aa3e5fdd8051da53def50525c130", + "sha256": "dc6871e84b882210ad9a96300bc22944530d783ca78b3badd5a174bf628d45aa" + } + ] +} diff --git a/research/crt-arena-batch-threshold/TASK.json b/research/crt-arena-batch-threshold/TASK.json new file mode 100644 index 0000000000..9ad686814d --- /dev/null +++ b/research/crt-arena-batch-threshold/TASK.json @@ -0,0 +1,80 @@ +{ + "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 full shared-arena CRT batch threshold and its least uniform majorant constant.", + "scope_change_reason": "Original analytic extension of PR4650, rather than an audit of its one-axis theorem. The explicit full-batch counterexample leaves the unbounded p>=3 domain and sharp uniform constant unsettled.", + "bottleneck_link": "Closes the large-parameter arena-batch allowance under the inherited schoolbook tariff, without changing the scalar inventory or treating other CRT costs as zero.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified full-batch theorem; defer physical execution and new inventory to open questions.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified argument; RESULT.json is generated by the exact bounded verifier.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the actual word-level scalar inventory fit constant one at the two excluded p=2 corners?", + "why_it_matters": "The present excess is a majorant excess and does not exclude a cheaper physical implementation.", + "first_step": "Replace one schoolbook product per tape action by the actual per-record comparisons in PR4192 section 2 and price the two finite cases.", + "blocked_by": "A tighter physical inventory is outside this theorem." + }, + { + "question": "Can this full-batch allowance be composed with reservoir placement and the actual exceptional-repair evaluator?", + "why_it_matters": "The full batch theorem discharges only an arithmetic allowance, not total CRT cost.", + "first_step": "Bind one complete entry/call/exit program to the paid key service in PR4795, retaining every source-state query and restoration charge.", + "blocked_by": "Matched physical movement, ownership and all-size caller premises remain external." + } + ] +} diff --git a/research/crt-arena-batch-threshold/VERIFY.json b/research/crt-arena-batch-threshold/VERIFY.json new file mode 100644 index 0000000000..78414b62a3 --- /dev/null +++ b/research/crt-arena-batch-threshold/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/crt-arena-root-axis/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact full-batch grid, independent polynomial bill expansion, proof-inequality controls, sharp witness, domain rejection and hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with Python assertions disabled." + } + ] +} diff --git a/research/crt-arena-batch-threshold/verify.py b/research/crt-arena-batch-threshold/verify.py new file mode 100644 index 0000000000..65477a4013 --- /dev/null +++ b/research/crt-arena-batch-threshold/verify.py @@ -0,0 +1,149 @@ +"""Exact corroboration of the new full-batch threshold; standard library only.""" + +import argparse +import hashlib +import json +from fractions import Fraction +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +LIMIT = 64 +SHARP = Fraction(9702312163, 8589934592) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def bill(p, ell, h): + if not (type(p) is type(ell) is type(h) is int): + raise ValueError("integer parameters required") + if not (2 <= p <= LIMIT and 1 <= h <= ell <= p): + raise ValueError("fixture outside bounded checker domain") + q, n, w = p + 2, 2**h, 4 * (p + 2) + accesses = n*n + 2*n*h*h + 24*n*h + 3*n + records = n * (h*h + 3*h + 1) + tape = accesses * (26*w*records + 25*w) + 30*w*records + tape += 3*n*h + 6*(2*h-1)*n + 3 + crt = 65536*q**3 + 1024*q*ell**3 + 1024*q*q + axis = crt + 4*(9*(ell+2)**2*n + (1+8*w*w)*tape) + return 8*q*axis, 2**(4*ell)*q**16 + + +def expanded_batch(p, ell, h): + """A separate q-polynomial expansion of the full batch numerator.""" + q, n = p+2, 2**h + a = n*(n + 2*h*h + 24*h + 3) + j = n*(h*h + 3*h + 1) + linear = 4*(a*(26*j+25)+30*j) + constant = n*(15*h-6)+3 + return ((524288+4096*linear)*q**4 + (8192+4096*constant)*q**3 + + (32*linear+8192*ell**3)*q**2 + + (32*constant+288*(ell+2)**2*n)*q) + + +def sources(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + digest = hashlib.sha256(data).hexdigest() + require(digest == row["sha256"], "source SHA256 mismatch") + header = f"blob {len(data)}\0".encode() + blob = hashlib.sha1(header+data).hexdigest() + require(blob == row["git_blob"], "source Git blob mismatch") + + +def proof_checks(): + checks = 0 + for h in range(2, LIMIT+1): + q, n = max(5, h+2), 2**h + require(419328 < n**4*q**11, "first third") + require(864 < n**3*q**13, "second third") + require(146626560*h*h < n*q**12, "third third") + if h >= 4: + require(2*h*h*25 >= 32*(h+1)**2, "induction multiplier") + checks += 1 + require(297353184 < 16*5**12, "height-one base") + for ell in range(1, LIMIT+1): + require((ell+1)**3-16*ell**3 <= -8*ell**3, "cubic step") + require((ell+3)**2 < 16*(ell+2)**2, "quadratic step") + return checks, LIMIT + + +def grid(): + failures, total, maximum = [], 0, Fraction(0) + for p in range(2, LIMIT+1): + for ell in range(1, p+1): + for h in range(1, ell+1): + batch, allowance = bill(p, ell, h) + require(batch == expanded_batch(p, ell, h), "expanded bill") + ratio = Fraction(batch, allowance) + require(ratio <= SHARP, "sharp uniform bound") + if batch >= allowance: + failures.append([p, ell, h]) + maximum = max(maximum, ratio) + total += 1 + require(failures == [[2, 1, 1], [2, 2, 2]], "exception classification") + require(maximum == SHARP, "attained constant") + return total, failures + + +def controls(): + invalid = [(True, 1, 1), (2, 0, 1), (2, 1, 2), (1, 1, 1), + (2, 3, 1), (LIMIT+1, 1, 1)] + for args in invalid: + try: + bill(*args) + except ValueError: + continue + raise ValueError("invalid fixture accepted") + batch, allowance = bill(2, 2, 2) + require(batch > allowance, "constant-one overclaim must reject") + require(batch*SHARP.denominator == allowance*SHARP.numerator, + "any strictly smaller constant must reject at the witness") + return len(invalid)+2 + + +def result(): + sources() + proof = proof_checks() + total, failures = grid() + rejection_count = controls() + names = ["PROOF.md", "verify.py", "SOURCES.json", "TASK.json", "VERIFY.json"] + hashes = {name: hashlib.sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in names} + witnesses = [] + for ell, h in [(1, 1), (2, 1), (2, 2)]: + batch, allowance = bill(2, ell, h) + witnesses.append({"p": 2, "ell": ell, "h": h, "batch": batch, + "allowance": allowance, + "ratio": str(Fraction(batch, allowance))}) + return {"status": "PASS_CRT_ARENA_BATCH_THRESHOLD", + "claim_type": "scoped proof with finite corroboration", + "grid_p_max": LIMIT, "grid_triples": total, + "exceptions": failures, "sharp_constant": str(SHARP), + "height_checks": proof[0], "extension_checks": proof[1], + "rejection_controls": rejection_count, + "p2_exhaustion": witnesses, "source_sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + actual = result() + path = PACKAGE / "RESULT.json" + if args.write_result: + path.write_text(json.dumps(actual, indent=2)+"\n") + expected = json.loads(path.read_text()) + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + "receipt differs from exact replay") + print(json.dumps(actual, indent=2)) + + +if __name__ == "__main__": + main()