diff --git a/research/subexponential-prime-dimension/PROOF.md b/research/subexponential-prime-dimension/PROOF.md new file mode 100644 index 0000000000..5310fde76f --- /dev/null +++ b/research/subexponential-prime-dimension/PROOF.md @@ -0,0 +1,153 @@ +# Prime supply with subexponential dimension + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and inherited reduction + +Let ell and d be integers satisfying + +```text +ell >= 2^18, 2 <= d <= 2^floor(sqrt(ell)/4), D=d-1. +``` + +For either t=2^ell or t=2^(ell-1), the half-open interval + +```text +I(t,d) = (t*(1-1/(3d)), t*(1-1/(4d))] +``` + +contains at least D primes. Thus the same two-scale caller can select D +distinct odd prime lengths in original axis order. Retain the separate +premise target_halo+2w <= 2^(ell-3) to obtain its period guard. The band +also retains the source-ratio guards and T/S<3/2 from ToikY's +[PR4029](https://github.com/CrocSwap/integer-mult-bounds/pull/4029). + +The new result is the displayed parameter domain. Source guards, ordering, +product accounting and the prime-selection algorithm retain their +predecessors' credit. No producer implementation or multiplication theorem +is proved here. + +All logarithms below are natural. Put y=log(t). We use the following +interval estimate from PR4029's PROOF.md, section "Imported analytic input +and effective cutoff", as a cited premise: + +```text +pi(b)-pi(a) >= t/(12*d*y) - 20*t*sqrt(y)*exp(-sqrt(y)/2). (1) +``` + +Its derivation requires only d>=2 and t>=4, before imposing the old +polynomial dimension restriction. Its analytic input is Fiori, Kadiri and +Swidinsky, [Corollary 22, arXiv:2206.12557v2](https://arxiv.org/pdf/2206.12557v2): + +```text +|pi(x)-Li(x)| <= 9.2211*x*sqrt(log(x))*exp(-.8476*sqrt(log(x))), x>=2. +``` + +Neither predecessor theorem is reverified by the finite checker. To make +the right side of (1) strictly larger than D, it suffices to prove + +```text +480*d*y^(3/2)*exp(-sqrt(y)/2) < 1, (2) +t > 24*d*D*y. (3) +``` + +Indeed, (2) makes the error strictly smaller than t/(24*d*y), leaving +strictly more than t/(24*d*y), which exceeds D by (3). + +## A dimension bound independent of a polynomial degree + +The elementary estimates 1/2=2 implies +(ell-1)*log(2) > (ell-1)/2 >= ell/4. Set z=sqrt(ell), so z>=512. +The left side of (2) is at most + +```text +480*z^3*exp(-3*z/40). +``` + +Let f(z)=log(480)+3*log(z)-3*z/40. At z=512, + +```text +f(512) < 7 + 3*9*(7/10) - 3*512/40 = -25/2 < 0. +f'(z) = 3/z - 3/40 <= f'(512) = -177/2560 < 0. +``` + +Here log(480)<7. These inequalities establish (2) on the entire domain, +without an enumeration over ell or d. + +For (3), D= z^2/4. +``` + +Use log(24)<5 and define g(z)=z^2/4-5-7*z/20-2*log(z). At z=512, + +```text +g(512) > 512^2/4 - 5 - 7*512/20 - 2*9*(7/10) + = 326696/5 > 0. +g'(512) = 512/2 - 7/20 - 2/512 = 327227/1280 > 0. +g''(z) = 1/2 + 2/z^2 > 0. +``` + +Therefore g stays positive for all z>=512, proving (3) and the theorem. + +The logarithm estimates use classical elementary inequalities. Integrating +1/t>1/2 on [1,2] proves log(2)>1/2. Positive exponential partial sums +of degrees three, six and three at 7/10, 7 and 5 exceed 2, 480 and 24, +respectively. The verifier checks these strict rational comparisons. + +## Strict enlargement of the original dimension region + +For every ell>=2^32, the new cap contains d<=ell^334 from PR4029. +It suffices to prove + +```text +334*log(ell) < (sqrt(ell)/4-1)*log(2), (4) +``` + +because floor(u)>u-1. With z=sqrt(ell)>=65536, the right side minus +the left side of (4) is strictly greater than + +```text +h(z) = z/8 - 7/10 - 668*log(z). +``` + +At z=65536, h(z)>8192-7/10-668*16*(7/10)=7097/10>0. +Its derivative 1/8-668/z is positive there and increases afterward. +This proves (4) for all ell>=2^32. + +The enlargement is strict. At ell=2^32, d=2^12000 exceeds +ell^334=2^10688 and is below the new cap 2^16384. Only exponent +comparisons are needed to certify this witness. The old improved +polynomial cutoff in PR5149 is a different domain comparison; no least +cutoff or optimal dimension constant is claimed. + +## Evidence boundary + +The standalone verifier computes the displayed rational endpoints and +derivative signs. It also checks the first error endpoint by the separate +integer inequality + +```text +8^38 > 480*512^3*3^38, +``` + +using e>8/3 and 3*512/40>38. A separate quota calculation compares +the exact exponents ell-1=262143 and 5+256+18=279, since +24*d*D*y < 2^5*2^256*2^18 at the first endpoint. These corroborate +the endpoint arithmetic; the derivatives above prove the unbounded range. + +The proof does not execute a giant prime search, materialize D lengths, +prove a practical cutoff, or implement an encoded caller. The imported +prime-counting theorem is mathematical input, not a finite certificate. +Native operations, physical costs, complete numerical recovery, compiler +closure, precision/tape and selected-supplier admission remain separate. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/subexponential-prime-dimension/README.md b/research/subexponential-prime-dimension/README.md new file mode 100644 index 0000000000..efca75331a --- /dev/null +++ b/research/subexponential-prime-dimension/README.md @@ -0,0 +1,111 @@ +# Subexponentially many axes in the fine prime band + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped mathematical proof with exact endpoint certificates. +The many-axis prime band from [ToikY's PR4029](https://github.com/CrocSwap/integer-mult-bounds/pull/4029) +contains at least D=d-1 primes at either retained target scale whenever + +```text +ell >= 2^18, 2 <= d <= 2^floor(sqrt(ell)/4). +``` + +This removes the polynomial dimension restriction in that analytic supply +argument. For every ell>=2^32 the new cap contains its entire old region +d<=ell^334. At ell=2^32 it also admits d=2^12000, while the old cap is +2^10688. The separate halo premise is retained. No new kappa is claimed. + +[PROOF.md](PROOF.md) gives the interval reduction, new endpoint and +monotonicity argument, and the strict enlargement proof. The predecessor's +interval estimate and the Fiori–Kadiri–Swidinsky prime-counting theorem are +cited inputs. The new result is the dimension region, rather than an +audit of either predecessor or a prime-producer implementation. + +## Reproduce + +From repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/subexponential-prime-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/subexponential-prime-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/subexponential-prime-dimension +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/subexponential-prime-dimension --check-source-history +``` + +Another CPython 3.12 installation may replace that interpreter path. The +direct verifier prints a generated JSON record binding all six package +files, followed by `PASS_SUBEXPONENTIAL_PRIME_DIMENSION`. It writes nothing +and needs no Git, network or predecessor runtime input. The package and +source-history checks separately validate the recorded historical pins. + +The checker uses exact fractions and integer powers. It checks the four +strict exponential partial sums, the stated endpoint and derivative +fractions, two alternative integer endpoint calculations, the polynomial +containment certificate and the strict enlarged-domain witness. It also +corroborates 24 dyadic endpoints and rejects nine invalid or unsupported +certificate parameters. Rejection of a smaller cutoff certificate does +not mean prime supply fails at that cutoff. The universal statement rests +on the written proof and imported analytic theorem. + +## Scope and credit + +The `uniform-transfer-audit` card changes to an analytic source-supply side +result connected to `analytic_recovery`. It discharges none of the five +selected assumptions in full. The selected PR6030 baseline returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; that is metadata orientation, +rather than a supplier replay. The working base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. + +Credit ToikY / PR4029, head `726c9a3a1dc58d2b1223dd681eb712255be407c1`, +for the exact band, caller binding, interval reduction and prior supply +domain. Credit Fiori, Kadiri and Swidinsky for their imported analytic +theorem; Jose Manuel / PR3935 for the tensor interface; Tekalign / PR4024 +for the CRT source premise; unpaidmoon / PR4142 for the separate guard; +Cinna Davis, Chafik Boukhalfa, Josie Elliston, the source08 contributors, +Harvey–van der Hoeven and Agarwal–Cooley for the retained selector and +source-construction lineage. Nick Petalas's PR5149 and PR5152 concern the +older polynomial cutoff and product envelope. Their results are credited +context, without being replayed here. Classical exponential estimates and +monotonicity arguments retain their mathematical credit; no global +literature-priority claim is made. + +Recent PR6444 improves a setup algorithm at the old abundance domain. +This result supplies a distinct analytic region and does not implement +its open encoded interface. No giant primes are computed. Encoded source +production, all-size physical tensor integration, numerical recovery, +stock, precision/tape, native and compiler obligations remain open or +inherited. No selected cold replay, Lean or Docker is run. Independent +human and formal proof-kernel review are unclaimed. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372253) +records the same target. Live PRs and recent handoffs, current main and +merged object/formula/general-region searches, recent account work and +local reservations were checked. Arbitrary historical diffs and unpublished +work remain outside coverage. [TASK.json](TASK.json) records overlap +freshness and the explicit scope change. [SOURCES.json](SOURCES.json) +pins historical provenance; no predecessor code is imported or modified. + +## Open next questions + +1. Can the original endpoint errors admit a larger coefficient of sqrt(ell) + in log(d), with an explicit cutoff? This would improve the analytic + capacity. Start with both unweakened endpoint errors. A uniform error + comparison and quota argument are still needed; no optimum is claimed. +2. Can a changed complete transform use the expanded dimension region to + lower its dominant paid bill? Start by deriving that caller's precision, + halo, source-loading and tensor cost laws. The present source-supply + theorem alone neither supplies that caller nor changes kappa. + +## Code inspection + +The verifier has no recursion, subprocesses, writes or dynamic code +generation. Every function is under 60 lines. All loops have fixed caps: +ten series terms, four logarithm certificates, 24 endpoint probes, nine +rejection controls, or six package files of at most 256 KiB. Explicit +exceptions remain active under `-O`. Scalar certificate parameters are +validated before arithmetic. CPython's integer and container allocation +is a managed-runtime deviation from fixed-storage execution; root exponents +are capped at 32, and the largest alternative power is 8^38. +These caps belong to finite corroboration, not to the theorem. Warning-strict +normal and optimized checks provide the local diagnostics. No static +analyzer or literal fixed-storage execution is claimed. diff --git a/research/subexponential-prime-dimension/SOURCES.json b/research/subexponential-prime-dimension/SOURCES.json new file mode 100644 index 0000000000..35863d2f2c --- /dev/null +++ b/research/subexponential-prime-dimension/SOURCES.json @@ -0,0 +1,52 @@ +{ + "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" + }, + { + "path": "research/many-axis-prime-supply/README.md", + "usage": "provenance", + "git_blob": "f3f736734a0d209a5fb383494b2253cc8f7702e4", + "sha256": "68ba22bcf761370c9370f770ed65de0de699feccb89c9011e470e00542ae72e9" + }, + { + "path": "research/many-axis-prime-supply/PROOF.md", + "usage": "provenance", + "git_blob": "1046c7493cf101e8cf1a43a7226a6d143e5190d1", + "sha256": "339213c572e0b1dae7028c16b371c0bdebc19e5ee5146ff9dd1e4c4570fa67e1" + }, + { + "path": "research/many-axis-prime-cutoff/README.md", + "usage": "provenance", + "git_blob": "7c79fab9a66e8d63602bbf0f65d3589e9f71e032", + "sha256": "786d4a5fbb1da3ba988f86d445c28e33000363e7e3cf962a536b61e4fdcc8e11" + }, + { + "path": "research/many-axis-prime-product-loss/README.md", + "usage": "provenance", + "git_blob": "e93107c8c3f7b2f0a07560d8547cd9759e1c5525", + "sha256": "e939dd08789a9a2a429ef8c7ca9883589fd5d4ca5bdff3da06178352c89eeb2a" + } + ], + "external_mathematical_input": { + "url": "https://arxiv.org/pdf/2206.12557v2", + "authors": [ + "Andrew Fiori", + "Habiba Kadiri", + "Joshua Swidinsky" + ], + "result": "Corollary 22", + "role": "Imported theorem; not executed, vendored or reverified." + } +} diff --git a/research/subexponential-prime-dimension/TASK.json b/research/subexponential-prime-dimension/TASK.json new file mode 100644 index 0000000000..01a58c16e1 --- /dev/null +++ b/research/subexponential-prime-dimension/TASK.json @@ -0,0 +1,128 @@ +{ + "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 sufficient two-scale prime-supply region ell>=2^18 and 2<=d<=2^floor(sqrt(ell)/4), with D=d-1.", + "scope_change_reason": "Original analytic side question extending ToikY PR4029 interval reduction beyond polynomial dimension. This does not audit a predecessor or discharge the full selected analytic_recovery assumption.", + "bottleneck_link": "Analytic source supply is one prerequisite of tensor/CRT assembly. The new region permits subexponential dimension, but a complete changed caller and paid bill remain absent.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified domain improvement, a written all-domain proof and exact endpoint certificates; do not optimize the coefficient or cutoff further.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal argument. verify.py computes exact logarithm and endpoint certificates, strict containment, 24 dyadic corroborations and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the original endpoint errors admit a larger coefficient of sqrt(ell) in log(d), at an explicit cutoff?", + "why_it_matters": "It would enlarge the analytic capacity beyond the conservative new region.", + "first_step": "Use both unweakened endpoint errors and derive one uniform rational monotonicity certificate.", + "blocked_by": "No optimized coefficient, least cutoff or complete endpoint comparison is supplied." + }, + { + "question": "Can a changed complete transform use the expanded dimension region to lower the dominant paid bill?", + "why_it_matters": "Prime supply alone does not improve kappa.", + "first_step": "Derive that caller's precision, halo, source-loading and full tensor cost laws.", + "blocked_by": "No changed complete caller or favorable full invoice is supplied." + } + ], + "claim_type": "scoped mathematical proof with exact endpoint certificates", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372253", + "predecessor": { + "pr": 4029, + "author": "ToikY", + "head": "726c9a3a1dc58d2b1223dd681eb712255be407c1", + "use": "Interval-count reduction and band/caller consequences, cited without scientific replay." + }, + "overlap": { + "checked_at_utc": "2026-11-03T11:10:02Z", + "sources": [ + "Live open PRs and account submissions", + "Latest 40 handoff comments and 12 active Discussions", + "Main README object, formula and general-dimension searches", + "Merged/all-state prime-supply, prime-dimension, subexponential searches", + "Local coordination reservations" + ], + "limitations": [ + "Overlap helper omitted 8788 sparse HEAD note paths; direct whole-main README searches supplement it.", + "Arbitrary historical diffs and unpublished work are not exhaustively searched." + ], + "nearby": [ + 4029, + 5149, + 5152, + 6444 + ], + "source_question": "original", + "relation_to_recent_account_work": "PR6444 concerns an algorithmic setup bound, rather than this analytic dimension region. No open encoded-interface question is taken.", + "remote_snapshot": { + "open_prs": 539, + "open_prs_fetched_at": "2026-11-03T11:05:07.442969+00:00", + "discussions": 6564, + "discussions_fetched_at": "2026-11-03T11:06:31.484347+00:00", + "complete_pagination": true + }, + "local_note_records": 129, + "local_note_inventory": 8917 + } +} diff --git a/research/subexponential-prime-dimension/VERIFY.json b/research/subexponential-prime-dimension/VERIFY.json new file mode 100644 index 0000000000..c3101d27d4 --- /dev/null +++ b/research/subexponential-prime-dimension/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact endpoint, derivative, logarithm and containment certificates, integer alternatives, 24 dyadic corroborations and nine rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same complete finite checks with assertions disabled; all checks use explicit exceptions." + } + ] +} diff --git a/research/subexponential-prime-dimension/verify.py b/research/subexponential-prime-dimension/verify.py new file mode 100644 index 0000000000..1e96920622 --- /dev/null +++ b/research/subexponential-prime-dimension/verify.py @@ -0,0 +1,135 @@ +#!/usr/bin/env python3 +"""Exact endpoint certificates for a written prime-supply domain proof.""" + +from fractions import Fraction as Q +from hashlib import sha256 +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def exponential_lower(value, degree): + require(isinstance(value, Q) and value > 0, "positive rational required") + require(type(degree) is int and 1 <= degree <= 10, "series degree outside cap") + term = Q(1) + total = term + for index in range(1, degree + 1): + term *= value / index + total += term + return total + + +def endpoint(root_bits, slope): + require(type(root_bits) is int and 1 <= root_bits <= 32, "root size outside cap") + require(isinstance(slope, Q) and slope > 0, "positive rational slope required") + root = 1 << root_bits + log_two_upper = Q(7, 10) + log_root_upper = root_bits * log_two_upper + decay = Q(1, 4) - slope * log_two_upper + error = 7 + 3 * log_root_upper - decay * root + error_derivative = Q(3, root) - decay + quota = Q(root * root, 4) - 5 - 2 * slope * log_two_upper * root + quota -= 2 * log_root_upper + quota_derivative = Q(root, 2) - 2 * slope * log_two_upper - Q(2, root) + require(decay > 0, "no positive error decay") + require(error < 0 and error_derivative < 0, "error endpoint or monotonicity fails") + require(quota > 0 and quota_derivative > 0, "quota endpoint or monotonicity fails") + return error, error_derivative, quota, quota_derivative + + +def containment(root_bits, polynomial_degree): + require(type(root_bits) is int and 1 <= root_bits <= 32, "root size outside cap") + require(type(polynomial_degree) is int and 1 <= polynomial_degree <= 1000, + "polynomial degree outside cap") + root = 1 << root_bits + margin = Q(root, 8) - Q(7, 10) - 2 * polynomial_degree * root_bits * Q(7, 10) + derivative = Q(1, 8) - Q(2 * polynomial_degree, root) + require(margin > 0 and derivative > 0, "polynomial containment certificate fails") + return margin, derivative + + +def check_logarithms(): + bounds = ((Q(7, 10), 3, 2), (Q(7), 6, 480), (Q(5), 3, 24), (Q(1), 4, Q(8, 3))) + values = [] + for argument, degree, target in bounds: + value = exponential_lower(argument, degree) + require(value > target, "strict exponential lower bound failed") + values.append(str(value)) + # log(2)>1/2 follows in PROOF.md by integrating 1/t>1/2 on [1,2]. + return values + + +def reject_controls(): + cases = (("small cutoff", 8, Q(1, 4)), + ("excessive dimension slope", 9, Q(1, 2)), + ("zero slope", 9, Q(0)), + ("Boolean root size", True, Q(1, 4)), + ("oversized root", 33, Q(1, 4)), + ("inexact slope", 9, 0.25)) + rejected = [] + for label, bits, slope in cases: + try: + endpoint(bits, slope) + except ValueError: + rejected.append(label) + else: + raise ValueError("accepted invalid certificate: " + label) + for bits, degree in ((15, 334), (16, 1000), (16, True)): + try: + containment(bits, degree) + except ValueError: + rejected.append("containment " + str((bits, degree))) + else: + raise ValueError("accepted unsupported containment certificate") + return rejected + + +def package_hashes(directory): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = directory / name + require(path.is_file() and not path.is_symlink(), "missing regular package file: " + name) + require(path.stat().st_size <= 262144, "package file exceeds read cap") + hashes[name] = sha256(path.read_bytes()).hexdigest() + return hashes + + +def verify(): + logs = check_logarithms() + primary = endpoint(9, Q(1, 4)) + require(primary == (Q(-25, 2), Q(-177, 2560), Q(326696, 5), Q(327227, 1280)), + "stated endpoint fractions disagree") + polynomial = containment(16, 334) + require(polynomial[0] == Q(7097, 10), "stated containment margin disagrees") + # Separate integer-power checks of the error and quota endpoints. + require(8 ** 38 > 480 * 512 ** 3 * 3 ** 38, "integer error endpoint failed") + require(3 * Q(512, 40) > 38, "integer error exponent rounding failed") + require((1 << 18) - 1 > 5 + 256 + 18, "integer quota endpoint failed") + # An enlarged-domain witness is encoded by exponents, without forming d or t. + require(334 * 32 < 12000 <= (1 << 16) // 4, "strict domain enlargement failed") + corroborated = 0 + for root_bits in range(9, 33): + endpoint(root_bits, Q(1, 4)) + corroborated += 1 + controls = reject_controls() + report = {"claim_type": "scoped mathematical proof with exact endpoint certificates", + "ell_min": 1 << 18, "dimension_cap": "2^floor(sqrt(ell)/4)", + "endpoint_fractions": [str(value) for value in primary], + "polynomial_containment": [str(value) for value in polynomial], + "logarithm_series_lower_values": logs, "dyadic_endpoints": corroborated, + "rejected_controls": controls, "new_kappa": False, + "package_sha256": package_hashes(Path(__file__).resolve().parent)} + print(json.dumps(report, indent=2, sort_keys=True)) + print("PASS_SUBEXPONENTIAL_PRIME_DIMENSION endpoints=" + str(corroborated) + + " controls=" + str(len(controls)) + " no_new_kappa") + + +if __name__ == "__main__": + require(len(sys.argv) == 1, "this read-only verifier accepts no arguments") + verify()