From 35486fd99b32842d7d5537b38fdec1f4ac80270e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 6 Nov 2026 13:07:56 +0000 Subject: [PATCH] feat(research): reduce the effective interval onset --- .../smaller-interval-onset/CODE-SAFETY.md | 44 +++++ research/smaller-interval-onset/PROOF.md | 165 ++++++++++++++++++ research/smaller-interval-onset/README.md | 68 ++++++++ research/smaller-interval-onset/SOURCES.json | 29 +++ research/smaller-interval-onset/TASK.json | 113 ++++++++++++ research/smaller-interval-onset/VERIFY.json | 34 ++++ research/smaller-interval-onset/verify.py | 117 +++++++++++++ 7 files changed, 570 insertions(+) create mode 100644 research/smaller-interval-onset/CODE-SAFETY.md create mode 100644 research/smaller-interval-onset/PROOF.md create mode 100644 research/smaller-interval-onset/README.md create mode 100644 research/smaller-interval-onset/SOURCES.json create mode 100644 research/smaller-interval-onset/TASK.json create mode 100644 research/smaller-interval-onset/VERIFY.json create mode 100644 research/smaller-interval-onset/verify.py diff --git a/research/smaller-interval-onset/CODE-SAFETY.md b/research/smaller-interval-onset/CODE-SAFETY.md new file mode 100644 index 0000000000..3972747358 --- /dev/null +++ b/research/smaller-interval-onset/CODE-SAFETY.md @@ -0,0 +1,44 @@ +# Verifier bounds and inspection + +The verifier only checks the new rational gates and hashes its own package. +It does not implement, import, fetch or replay the cited probability law. + +- Control flow has no recursion. Failed gates raise `ValueError`; file errors + propagate after the context manager closes the file. +- The Taylor sum has five terms. The gate loop has thirteen entries, the + rejecting-control loop has two inputs, and the file loop has seven paths. + There are no unbounded searches, queues, subprocesses or network calls. +- The exponent is bounded by `10^12` and is never used as a power exponent. + Computed powers have exponents at most 80. The supplied rational numerators + and denominators stay below 256 bits. Every file read is capped at 65537 + bytes and rejects lengths above 65536. Files close before the next read. +- Every function is below 60 physical lines. `require` calls enforce the + arithmetic conditions in both ordinary and optimized execution. All mutable + collections are local, and returned gate results and file bytes are used. +- No dynamic code, decorators, registration or callback chain is introduced. + `sum`, the context manager and JSON encoding use normal Python dispatch. + Imported calls have explicit standard-library targets. +- Registered checks enable warnings as errors. Development mode is also run + locally. The repository's existing package workflow runs both registered + normal and optimized commands. No shared workflow or analyzer is changed. + +## Managed-runtime deviation + +Rule: 3, fix memory capacity before steady operation. + +Location: `verify.py`, rational arithmetic, dictionaries and JSON output. + +Reason: CPython and `Fraction` allocate objects during arithmetic; they do not +provide an allocation-free execution mode. + +Scope: one bounded verifier invocation, including seven bounded file reads. + +Compensating control: fixed loop sizes, bounded exact integers, a 64 KiB cap +per file and sequential file lifetimes. No retained probability distribution +or enormous onset integer is allocated. + +Verification: the two registered commands, the local development-mode run, +and static inspection of the bounded domains above. + +Follow-up: reassess these bounds before adding inputs, adjustable numerical +domains or another package file to the receipt inventory. diff --git a/research/smaller-interval-onset/PROOF.md b/research/smaller-interval-onset/PROOF.md new file mode 100644 index 0000000000..e8342ec633 --- /dev/null +++ b/research/smaller-interval-onset/PROOF.md @@ -0,0 +1,165 @@ +# A smaller effective interval onset + +This scoped proof is produced by Nick Petalas. It uses alephnan's +[PR #6713](https://github.com/CrocSwap/integer-mult-bounds/pull/6713), +`LOCAL_LIMIT.md` at `cd666f05c4e9006025b634687cc493911c8371c8`, +as a mathematical premise. No predecessor verifier or convolution is replayed. + +## Premise and conclusion + +Use the notation of that source. The centered sum is `Z_n`, the centered +Gaussian `G_n` has variance `nv`, and `c_sigma = sqrt(2*pi*v)`. +For every integer `n >= 1296`, every real `x`, and every interval `I` with +endpoints `x,x+b`, the source proves + +\[ +\begin{aligned} + \sqrt n\,|\Pr(Z_n\in I)-\Pr(G_n\in I)|&\le A_n+bB_n,\\ + \left|\sqrt n\,\Pr(Z_n\in I) + -\frac{b e^{-x^2/(2nv)}}{c_\sigma}\right| + &\le A_n+bB_n+\frac{b^2}{4\sqrt n}, +\end{aligned} +\] + +where + +\[ + B_n=3/\sqrt n+\sqrt n\log n\,e^{-\sqrt n/320}, + \qquad A_n=(1+4B_n)/\log n. +\] + +These are its equations (1) and (2). They include every endpoint convention, +singletons when `b=0`, and the empty interval. Their six hypotheses H, +including `2 <= v <= 3`, and their classical analytic dependencies remain +premises here. In particular `c_sigma < 5` follows from `v <= 3, pi < 4`. + +**New conclusion.** Put `K = 751000000`. For every integer `n >= 2^K`, +every real `x`, and `0 <= b <= 5000`, both + +\[ + c_\sigma\sqrt n\,|\Pr(Z_n\in I)-\Pr(G_n\in I)| <10^{-8} +\] + +and + +\[ + \left|c_\sigma\sqrt n\,\Pr(Z_n\in I) + -b e^{-x^2/(2nv)}\right|<10^{-8} +\] + +hold with the same endpoint conventions. The source used `n >= 2^(10^12)` +for these guarantees. Only this local onset is improved. The proof below +also yields the sharper intermediate remainder coefficient `1025/1024` +in place of the source's simplification to `2`. + +## Uniform remainder bound + +Write `w = log n`, and first suppose `w >= 60`. The larger source bound is + +\[ + E(n,b)=\frac1w+ + (b+4/w)\left(3e^{-w/2}+w e^{w/2}e^{-e^{w/2}/320}\right) + +\frac{b^2}4e^{-w/2}. +\] + +For `0 <= b <= 5000`, we have `b+4/w < 5001` and + +\[ + 3\cdot5001+5000^2/4=6265003<2^{23}. +\] + +Consequently + +\[ + E(n,b)<\frac1w+2^{23}e^{-w/2} + +5001w e^{w/2}e^{-e^{w/2}/320}. \tag{A} +\] + +Multiply the two remainder terms by `w`. The first, +`R_1(w)=2^23 w e^(-w/2)`, decreases on `[60,infinity)` because its +logarithmic derivative is `1/w-1/2 < 0`. +The positive Taylor terms through degree four give + +\[ + e^3>1+3+9/2+27/6+81/24=131/8>16, +\] + +so `e^30 > 2^40`. Therefore + +\[ + R_1(w)\le R_1(60)<60/2^{17}<1/2048. \tag{B} +\] + +The second is `R_2(w)=5001w^2 e^(w/2) exp(-e^(w/2)/320)`. +Its logarithmic derivative is + +\[ + 2/w+1/2-e^{w/2}/640 + \le 2/60+1/2-2^{40}/640<0. +\] + +Thus `R_2` also decreases. The function `u exp(-u/320)` decreases for +`u>320`. Since `e^30>2^40>320`, + +\[ + \begin{aligned} + R_2(w)&\le R_2(60) + <5001\cdot60^2\cdot2^{40} e^{-2^{40}/320}\\ + &<2^{65}e^{-2^{31}} + <2^{65-2^{31}}<1/2048. \tag{C} + \end{aligned} +\] + +Here `5001*60^2 < 2^25`, `2^40/320 > 2^31`, and `e>2` +justify the successive strict inequalities. All of these are small exact +integer or rational comparisons. Combining (A), (B), and (C) proves + +\[ + \boxed{E(n,b)<\frac{1025}{1024\log n}} + \quad(w\ge60,\ 0\le b\le5000). \tag{D} +\] + +The smaller Gaussian-integral error obeys the same bound. No atomic-mass +estimate or change of endpoint convention is introduced. + +## The new onset + +The positive series +`log 2 = 2 sum_(j>=0) (1/3)^(2j+1)/(2j+1)` gives `log 2 > 2/3`. +For `n >= 2^K`, therefore, `w > 2K/3 > 60` and `n > 1296`. +Multiplying (D) by `c_sigma < 5` yields + +\[ + c_\sigma E(n,b) + <\frac{5\cdot1025}{1024w} + <\frac{15375}{2048K} + <\frac1{10^8}, +\] + +because, exactly, + +\[ + 2048\cdot751000000-15375\cdot10^8=548000000>0. +\] + +This proves both stated conclusions. The old and new onset exponents obey +`10^12 > 1331*K`; this compares exponents of symbolic integers, not runtime +or measured practical performance. No power with either enormous exponent +is constructed. + +## Scope and credit + +Alephnan retains credit for the effective interval inequalities, their +Fourier argument and application to the complete historical flow. CubeJerry +retains the fixed-height exponent result in PR #6329. The raw-p7 law and +analytic lineage retain the credit recorded there, including zxv, +Ryanson Jonathan / pinterbanget, DLamdata, Cinna Davis / 1337isnot1337, +Jacob Alan Sussman, and Nick Petalas's earlier leaf results. Beurling, +Selberg, Vaaler and Shou retain the classical approximation credit. + +The new contribution is the strict rational remainder budget and its smaller +sufficient local onset. The original hypotheses and interval inequalities +are cited, not independently proved or certified here. This written proof +has not been checked by a proof kernel. It does not substitute the new onset +into the full mixed-layer flow proof, improve its exponent, price a physical +implementation, or discharge any selected framework assumption. diff --git a/research/smaller-interval-onset/README.md b/research/smaller-interval-onset/README.md new file mode 100644 index 0000000000..805722b671 --- /dev/null +++ b/research/smaller-interval-onset/README.md @@ -0,0 +1,68 @@ +# A smaller effective interval-local-limit onset + +Scoped proof produced by Nick Petalas. Assuming the interval error inequalities +of alephnan's [PR #6713](https://github.com/CrocSwap/integer-mult-bounds/pull/6713) +at `cd666f05c4e9006025b634687cc493911c8371c8`, the same uniform `10^-8` +local-limit guarantee holds for + +```text +n >= 2^751000000 instead of n >= 2^(10^12). +``` + +This covers every interval of length at most 5000, every real location and +every endpoint convention, for both the exact Gaussian integral and the +left-endpoint Gaussian approximation. The exponents decrease by a factor +greater than 1331. Neither enormous integer is materialized. + +[PROOF.md](PROOF.md) proves the new intermediate bound +`E(n,b) < 1025/(1024 log n)` whenever `log n >= 60` and `0 <= b <= 5000`. +The improvement comes from retaining a smaller bound for the two decaying +remainders. It uses the predecessor's analytic inequalities as premises; +no predecessor program, certificate or probability convolution executes. +The source and exact hash are in [SOURCES.json](SOURCES.json). + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/smaller-interval-onset/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/smaller-interval-onset/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/smaller-interval-onset +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/smaller-interval-onset --check-source-history +``` + +Other hosts may substitute their CPython 3.12 executable. The verifier checks +the exact rational gates in the new proof, rejects two insufficient onset +certificates, and emits a generated receipt bound to every package file. +Those rejecting controls concern this sufficient estimate; they are not +counterexamples to the local-limit theorem at smaller depths. The universal +conclusion rests on the written monotonicity argument and cited premises. + +## Limitations + +The onset remains impractical. This is a historical analytic side result, +not a new kappa or a complete multiplication theorem. The six H hypotheses, +source interval inequalities and classical analytic approximation remain +mathematical inputs. No predecessor replay or independent audit is claimed. +The complete flow majorant has not been rederived with this onset. No +physical supplier, compiler, precision, ownership, tape or recovery obligation +is discharged. The selected record and all five assumptions remain unchanged. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Propagate this smaller local onset through the complete fixed-height flow + proof. Begin by identifying every use of its original local-limit cutoff; + retain all mixed layers, boundary exits and terminal leaves. +- Improve the error rate or remainder constant using the actual characteristic + function. A sharper spectral estimate could reduce the still enormous + sufficient onset much further. + +## Credit + +The new remainder estimate and onset are produced by Nick Petalas. +Alephnan retains the effective interval-bound credit in PR #6713, and +CubeJerry retains the fixed-height exponent theorem in PR #6329. The law, +flow and analytic lineage, and the classical approximation credit, are +listed in [PROOF.md](PROOF.md). Apache-2.0. diff --git a/research/smaller-interval-onset/SOURCES.json b/research/smaller-interval-onset/SOURCES.json new file mode 100644 index 0000000000..acb5e9ea54 --- /dev/null +++ b/research/smaller-interval-onset/SOURCES.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ], + "external_mathematical_dependencies": [ + { + "author": "alephnan", + "pr": 6713, + "commit": "cd666f05c4e9006025b634687cc493911c8371c8", + "path": "research/effective-direct-flow/LOCAL_LIMIT.md", + "url": "https://github.com/alephnan/integer-mult-bounds/blob/cd666f05c4e9006025b634687cc493911c8371c8/research/effective-direct-flow/LOCAL_LIMIT.md", + "sha256": "07702eabadefa4e2c435d6ea7e60c781aaa786fa875cab773a5962d8d2a2efe3", + "used": "Equations (1) and (2), the six H hypotheses and c_sigma < 5. These are cited premises. The verifier does not fetch, import or authenticate the external source; the hash identifies the inspected bytes. No foreign Git-history availability is asserted." + } + ] +} diff --git a/research/smaller-interval-onset/TASK.json b/research/smaller-interval-onset/TASK.json new file mode 100644 index 0000000000..14325c2203 --- /dev/null +++ b/research/smaller-interval-onset/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a smaller sufficient onset for the cited historical interval-local-limit inequalities, retaining the uniform 10^-8 guarantee for intervals of length at most 5000.", + "scope_change_reason": "This is an original quantitative extension of alephnan PR6713 open question 1, not an audit or discharge of a selected all-size assumption.", + "bottleneck_link": "Historical analytic side result. A smaller interval onset can reduce the explicit full-flow threshold after a separate propagation argument; it does not change the selected invoice or exponent.", + "budget_minutes": 60, + "stop_rule": "Ship the first strict onset improvement; do not optimize further or rederive the complete flow majorant.", + "outcome": "completed", + "evidence": "PROOF.md gives the new universal analytic implication. verify.py checks exact rational arithmetic gates and rejecting sufficient-certificate controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the smaller local onset reduce the complete fixed-height recurrence majorant?", + "why_it_matters": "The published global threshold depends on the old local onset.", + "first_step": "Locate every use of the cutoff in PR6713 PROOF.md and carry all layer and tail terms.", + "blocked_by": "A new complete propagation argument is outside this local result." + }, + { + "question": "Can a sharper characteristic-function estimate reduce the onset further?", + "why_it_matters": "The new sufficient depth remains impractical.", + "first_step": "Bound the actual characteristic function on a compact noncentral frequency band.", + "blocked_by": "A stronger spectral estimate is not supplied here." + } + ], + "predecessor": { + "pr": 6713, + "author": "alephnan", + "commit": "cd666f05c4e9006025b634687cc493911c8371c8", + "source_question": "README.md Open next questions, first item", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19440644" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + }, + "overlap": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at_utc": "2026-11-06T13:03:41Z", + "helper_open_pr_records": 734, + "helper_discussion_records": 6841, + "helper_remote_pagination_complete": true, + "local_materialized_records": 135, + "local_head_records": 8917, + "local_complete": false, + "targeted_checks": "All-state direct-flow/local-limit/onset searches, merged key-formula searches, origin/main README grep, latest 30 handoff comments and local target locks. PR6713 first open question is the source. PR6723/6728/6729 and PR6741/6742 are related coverage, not this new onset.", + "limits": "Searches and claims are non-atomic. Sparse helper coverage is incomplete. No literature-wide novelty or coverage of unpublished work is claimed." + } +} diff --git a/research/smaller-interval-onset/VERIFY.json b/research/smaller-interval-onset/VERIFY.json new file mode 100644 index 0000000000..e9c9c9d41b --- /dev/null +++ b/research/smaller-interval-onset/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact rational remainder and onset gates; two insufficient-certificate controls; generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same exact arithmetic gates with assertions disabled; no predecessor computation." + } + ] +} diff --git a/research/smaller-interval-onset/verify.py b/research/smaller-interval-onset/verify.py new file mode 100644 index 0000000000..c15d103556 --- /dev/null +++ b/research/smaller-interval-onset/verify.py @@ -0,0 +1,117 @@ +"""Check the new rational onset certificate, without a predecessor replay.""" + +from fractions import Fraction +from hashlib import sha256 +import json +from math import factorial +from pathlib import Path +import sys + + +ONSET_EXPONENT = 751_000_000 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py", "CODE-SAFETY.md", +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def remainder_gates() -> dict[str, str]: + """Certify endpoint and derivative bounds used on the whole w >= 60 ray.""" + w0 = 60 + width = 5000 + majorant_width = 5001 + u0 = 2**40 + taylor = sum(Fraction(3**j, factorial(j)) for j in range(5)) + gates = { + "window coefficient": Fraction(width) + Fraction(4, w0) + < majorant_width, + "inverse square-root coefficient": 3 * majorant_width + + Fraction(width**2, 4) < 2**23, + "positive Taylor lower bound": taylor == Fraction(131, 8) + and taylor > 16, + "first logarithmic derivative": Fraction(1, w0) - Fraction(1, 2) < 0, + "first endpoint": Fraction(w0, 2**17) < Fraction(1, 2048), + "second logarithmic derivative": Fraction(2, w0) + Fraction(1, 2) + - Fraction(u0, 640) < 0, + "auxiliary decreasing function": u0 > 320, + "second endpoint coefficient": majorant_width * w0**2 < 2**25, + "second exponential power": Fraction(u0, 320) > 2**31, + "second endpoint tail": 65 - 2**31 < -11, + "combined remainder": 2 * Fraction(1, 2048) == Fraction(1, 1024), + "Gaussian normalizer": 2 * 4 * 3 < 5**2, + "source domain on ray": 2**80 > 1296, + } + for name, passed in gates.items(): + require(passed, name) + return { + "taylor_lower": str(taylor), + "first_endpoint_upper": str(Fraction(w0, 2**17)), + "scaled_error_coefficient": str(Fraction(1025, 1024)), + "rational_gates": str(len(gates)), + } + + +def onset_gate(exponent: int) -> Fraction: + """Apply the proved sufficient bound; failure is not a theorem counterexample.""" + require(type(exponent) is int and 100 <= exponent <= 10**12, + "onset exponent outside the certificate domain") + log_lower = Fraction(2 * exponent, 3) + require(log_lower >= 60, "remainder ray is unavailable") + error_upper = Fraction(5 * 1025, 1024) / log_lower + require(error_upper < Fraction(1, 10**8), + "coarse sufficient error estimate exceeds the target") + return error_upper + + +def rejecting_controls() -> int: + for exponent in (99, 750_000_000): + rejected = False + try: + onset_gate(exponent) + except ValueError: + rejected = True + require(rejected, "insufficient onset certificate accepted") + return 2 + + +def package_hashes() -> dict[str, str]: + """Bound input reads and report hashes of the actual reviewed artifact.""" + here = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + with (here / name).open("rb") as source: + content = source.read(65537) + require(len(content) <= 65536, "package file exceeds 64 KiB") + hashes[name] = sha256(content).hexdigest() + return hashes + + +def main() -> None: + require(len(sys.argv) == 1, "this verifier takes no arguments") + gates = remainder_gates() + error = onset_gate(ONSET_EXPONENT) + slack = 2048 * ONSET_EXPONENT - 15375 * 10**8 + require(slack == 548_000_000 and slack > 0, "onset cross-product slack") + require(10**12 > 1331 * ONSET_EXPONENT, "exponent comparison") + receipt = { + "status": "PASS_SMALLER_INTERVAL_ONSET", + "claim_type": "scoped analytic implication from cited inequalities", + "onset_encoding": f"2^{ONSET_EXPONENT}", + "normalized_error_upper": str(error), + "target": "1/100000000", + "onset_cross_product_slack": slack, + "remainder": gates, + "rejecting_sufficient_certificate_controls": rejecting_controls(), + "external_premises_replayed": False, + "package_sha256": package_hashes(), + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()