From ef5136a007437627d140698bdd1fd052489d8692 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:01:52 +0100 Subject: [PATCH] feat(research): lower the many-axis prime cutoff to 2^30 --- research/many-axis-prime-cutoff/README.md | 169 +++++++++++++++++++ research/many-axis-prime-cutoff/SOURCES.json | 36 ++++ research/many-axis-prime-cutoff/TASK.json | 99 +++++++++++ research/many-axis-prime-cutoff/VERIFY.json | 32 ++++ research/many-axis-prime-cutoff/verify.py | 133 +++++++++++++++ 5 files changed, 469 insertions(+) create mode 100644 research/many-axis-prime-cutoff/README.md create mode 100644 research/many-axis-prime-cutoff/SOURCES.json create mode 100644 research/many-axis-prime-cutoff/TASK.json create mode 100644 research/many-axis-prime-cutoff/VERIFY.json create mode 100644 research/many-axis-prime-cutoff/verify.py diff --git a/research/many-axis-prime-cutoff/README.md b/research/many-axis-prime-cutoff/README.md new file mode 100644 index 0000000000..7c79fab9a6 --- /dev/null +++ b/research/many-axis-prime-cutoff/README.md @@ -0,0 +1,169 @@ +# Fourfold reduction of the many-axis prime-supply cutoff + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped mathematical proof with exact endpoint certificates.** +ToikY's [#4029](https://github.com/CrocSwap/integer-mult-bounds/pull/4029) +prime-supply theorem holds already for **`ell >= 2^30 = 1073741824`**, in +place of `ell >= 2^32`. The dimension range `2 <= d <= ell^334`, both target +scales, the prime band and separate halo premise stay the same. This is a new +endpoint argument using the predecessor's analytic reduction, not an audit. + +## Statement and proof + +Let `ell >= 2^30`, `D=d-1 >= 1` be integers and `d <= ell^334`. For either +`t=2^(ell-1)` or `t=2^ell`, the band + +```text +I(t,d) = (a,b] = (t*(1-1/(3d)), t*(1-1/(4d))] +``` + +contains at least `D` primes. Distinct selections for any `D` axes at these +scales satisfy the same source-ratio and product conclusions as #4029. +Retain its separate premise `target_halo+2w <= 2^(ell-3)` for the period guard. +The guard and separate oddness gate retain unpaidmoon's +[#4142](https://github.com/CrocSwap/integer-mult-bounds/pull/4142) credit. + +All logarithms are natural. The imported analytic theorem is Fiori, Kadiri +and Swidinsky's [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. +``` + +Put `y=log(t)`. We cite #4029's resulting interval estimate as the starting +point, preserving its constants and mathematical credit: + +```text +pi(b)-pi(a) >= t/(12*d*y) - 20*t*sqrt(y)*exp(-sqrt(y)/2). (1) +``` + +The two endpoint errors use `sqrt(t)<=a1/2`; the main term uses `Li(b)-Li(a)>=(b-a)/log(t)`. +We do not rerun the predecessor's source or analytic checks. To make (1) +greater 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) bounds the subtracted term by `t/(24*d*y)`, strictly, and (3) +then supplies the quota. For `ell>=2`, both scales obey `ell/4<=y<=ell`, +using `1/22`. It also gives `log(480)<7` and `log(24)<5`, +already from degrees six and three at seven and five respectively. +At `ell0=2^30`, `z0=2^15`, the logarithm of (4) is strictly less than + +```text +7 + 671*15*(7/10) - 2^13 = -2279/2 < 0. (5) +``` + +The derivative of `log(480)+671*log(z)-z/4` is `671/z-1/4`. +It is negative for every `z>=z0`, because `32768>4*671=2684`. +This proves (2) throughout the new domain, without finite extrapolation. + +For (3), `24*d*D*y<=24*ell^669` and `t>=exp(ell/4)`. At the new endpoint, + +```text +ell0/4 - log(24) - 669*log(ell0) + > 2^28 - 5 - 669*30*(7/10) = 268421402 > 0. (6) +``` + +The derivative of `ell/4-log(24)-669*log(ell)` is `1/4-669/ell`. +It is positive for every `ell>=ell0`, since `ell0>4*669=2676`. +Thus (3) holds everywhere in the new domain. Equations (1)-(3) prove the +prime quota. QED. + +The two bands are disjoint, so increasing prime lists can be interleaved in +original target order without repetition. Their lower endpoints exceed two, +so every selected prime is odd. The inherited band argument gives the strict +source guards and `S/T>(1-1/(3d))^D>2/3`, hence `T/S<3/2`. +The separate halo bound gives `s>(5/6)*2^(ell-1)>2*(target_halo+2w)`. +No new source program or setup-cost improvement is inferred. + +## Exact evidence and reproduction + +[verify.py](verify.py) checks (5), (6), both derivative signs and the +positive-series logarithm bounds by rational arithmetic. A second endpoint +calculation uses `e>8/3` and checks the integer inequality + +```text +8^8192 > 480 * 2^10065 * 3^8192. +``` + +The quota endpoint also follows from `e>2` and an exponent comparison, with +no giant target integer. These are two calculations of the new endpoint, +not independent proofs of the imported analytic theorem. Twelve rejecting +controls include an unsupported cutoff `2^28`, a false logarithm bound, +altered margins, missing derivative gaps and invalid replay parameters. +A rejected certificate at `2^28` does not prove prime supply fails there. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/many-axis-prime-cutoff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/many-axis-prime-cutoff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/many-axis-prime-cutoff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/many-axis-prime-cutoff --check-source-history +``` + +Replace that interpreter path with another CPython 3.12 installation when +needed. The marker is `PASS_MANY_AXIS_PRIME_CUTOFF`. The verifier emits +computed values and hashes of all five package files, writes nothing, and +needs no Git or network. No handwritten receipt is supplied. The last command +requires a publication commit and Git history. + +The verifier has bounded loops, no recursion and functions under 60 lines. +Its control helper has a fixed set of local indirect-call targets. Python's +dynamic allocation is a managed-runtime deviation, bounded by powers 2..32 +and series degree at most six. Integer-power operands stay below 50,000 bits. +Explicit checks remain active under optimization; both registered commands +make warnings errors. No external analyzer is required at replay. + +## Scope, provenance and credit + +The scientific base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority +revision 7. TASK.json records the changed `uniform-transfer-audit` scope. +SOURCES.json pins the predecessor statement, reduction and guard discussion +as historical provenance. No predecessor executable or live runtime input is +imported. Selected metadata orientation passed as +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it is not a supplier replay. +Live PRs/Discussions, merged searches, whole-main README searches and the +overlap helper found no matching cutoff reduction within their coverage. +Sparse local notes, arbitrary unseen diffs and unpublished work remain limits. + +Credit ToikY #4029 for the source-bound theorem, band, analytic reduction, +constructive algorithm and setup bill; unpaidmoon #4142 for the guard/oddness +separation and cutoff question; Fiori, Kadiri and Swidinsky for their theorem; +Jose Manuel #3935 for the tensor interface; Tekalign #4024 for CRT conversion; +Cinna Davis, Chafik Boukhalfa #1786 and Josie Elliston for prior selector work; +and Harvey and van der Hoeven, source08 and Agarwal and Cooley for the +retained number-theoretic, trial-division and CRT lineage. The new result +is only the smaller sufficient cutoff proved above. + +The cutoff remains enormous and is not claimed least. No giant prime search, +literal encoded producer, physical caller, native supplier, new kappa or +selected-frontier change is supplied. Halo/growth constants, numerical tensor +and recovery, precision/tape, stock and other supplier obligations remain. +Independent human and formal proof-kernel review are unclaimed. Selected cold +replay, predecessor scientific suites, Lean and Docker were not run. + +## Open next questions + +1. Can the original endpoint errors give a smaller sufficient cutoff than + the weakened bound (4)? This would enlarge the admitted parameter domain. + Start with rational bounds on both endpoint logarithms and a new + monotonicity certificate. No further reduction or least cutoff is proved. +2. Can an encoded prime producer meet the actual source-tape and head-return + contract? Start with #4142's loading/oddness boundary and #4029's written + trial-division algorithm. Literal arithmetic, complete execution and its + physical bill remain absent. The family decision is to stop at this + parameter improvement. diff --git a/research/many-axis-prime-cutoff/SOURCES.json b/research/many-axis-prime-cutoff/SOURCES.json new file mode 100644 index 0000000000..6bbdf9a75b --- /dev/null +++ b/research/many-axis-prime-cutoff/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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/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-encoded-axis-guard/README.md", + "usage": "provenance", + "git_blob": "1907b4f1815f056a9bad313ba316df3c6aa4a03e", + "sha256": "3d51a8dd86db6b95d8387b16f86d6ad3627a415583eea23dedd82ffc65bc57af" + } + ] +} diff --git a/research/many-axis-prime-cutoff/TASK.json b/research/many-axis-prime-cutoff/TASK.json new file mode 100644 index 0000000000..e3266f5401 --- /dev/null +++ b/research/many-axis-prime-cutoff/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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": "Lower the sufficient many-axis prime-supply cutoff from ell >= 2^32 to ell >= 2^30, retaining d <= ell^334 and the same band, target scales and halo premise.", + "scope_change_reason": "Original parameter improvement of ToikY PR4029, refining unpaidmoon PR4142 cutoff question. This is not a PR4100 audit or a replay of predecessors.", + "bottleneck_link": "An explicit smaller sufficient prime-supply domain enlarges one parameter regime available to the many-axis tensor/CRT caller. It supplies no encoded producer or complete paid caller.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved sufficient-cutoff reduction; package the new endpoint certificate without optimizing it further.", + "outcome": "completed", + "evidence": "README contains the dimension-uniform monotonicity proof. verify.py checks exact rational and integer endpoint certificates and twelve rejection controls. Imported prime-counting analysis and predecessor executables are not replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can original endpoint errors lower the sufficient cutoff further?", + "why_it_matters": "This would enlarge the sufficient prime-supply domain.", + "first_step": "Bound the two endpoint logarithms rationally and derive a new monotonicity certificate instead of weakening to (4).", + "blocked_by": "No further cutoff or least-cutoff proof is supplied." + }, + { + "question": "Can an encoded prime producer meet the actual source-tape and head-return contract?", + "why_it_matters": "Prime existence alone does not provide a complete physical caller.", + "first_step": "Use PR4142 loading/oddness contracts and PR4029 written trial-division construction.", + "blocked_by": "Literal encoded arithmetic, complete execution and its physical bill remain absent." + } + ], + "claim_type": "scoped mathematical proof with exact endpoint certificates", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144278", + "environment": { + "python": "3.12.15", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "platform": "macOS-27.0.1-arm64-arm-64bit" + }, + "orientation": { + "command": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_selected_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "scope": "Selected exact metadata/source orientation only, not a scientific replay." + }, + "overlap": { + "open_pr_snapshot_records": 305, + "discussion_snapshot_records": 4291, + "local_notes_searched": 162, + "local_head_notes": 6884, + "scope": "Live open lists, own-account work, recent handoffs and active Discussions, focused all-state/merged searches, whole-main README searches and targeted materialized predecessor reads. Sparse local search, arbitrary diffs and unpublished work are incomplete." + } +} diff --git a/research/many-axis-prime-cutoff/VERIFY.json b/research/many-axis-prime-cutoff/VERIFY.json new file mode 100644 index 0000000000..4f9d31b982 --- /dev/null +++ b/research/many-axis-prime-cutoff/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": 60, + "checks": "New rational and integer endpoint certificates, derivative signs and twelve rejection controls; read-only generated source-hash receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same exact checks under optimization, with explicit checks enabled." + } + ] +} diff --git a/research/many-axis-prime-cutoff/verify.py b/research/many-axis-prime-cutoff/verify.py new file mode 100644 index 0000000000..32e7ebae90 --- /dev/null +++ b/research/many-axis-prime-cutoff/verify.py @@ -0,0 +1,133 @@ +"""Exact endpoint certificates for the new many-axis prime-supply domain.""" + +from dataclasses import dataclass, replace +from fractions import Fraction +from hashlib import sha256 +import json +from math import factorial +from pathlib import Path + + +@dataclass(frozen=True) +class Certificate: + power: int + log2_upper: Fraction + error_margin: Fraction + quota_margin: Fraction + error_derivative_gap: int + quota_derivative_gap: int + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def exp_prefix(value: Fraction, degree: int) -> Fraction: + need(0 <= value <= 7, "exponential argument outside finite domain") + need(type(degree) is int and 0 <= degree <= 6, "invalid series degree") + return sum((value**k / factorial(k) for k in range(degree + 1)), Fraction()) + + +def endpoint(power: int, log2_upper: Fraction) -> Certificate: + need(type(power) is int and 2 <= power <= 32, "invalid cutoff power") + need(power % 2 == 0, "integer square-root certificate needs an even power") + need(isinstance(log2_upper, Fraction), "logarithm bound must be rational") + need(0 < log2_upper <= 1, "logarithm bound outside finite domain") + ell = 1 << power + z = 1 << (power // 2) + return Certificate( + power, + log2_upper, + Fraction(z, 4) - 7 - 671 * (power // 2) * log2_upper, + Fraction(ell, 4) - 5 - 669 * power * log2_upper, + z - 4 * 671, + ell - 4 * 669, + ) + + +def validate(certificate: Certificate) -> None: + expected = endpoint(certificate.power, certificate.log2_upper) + need(certificate == expected, "altered endpoint certificate") + need(exp_prefix(certificate.log2_upper, 3) > 2, "unproved log(2) bound") + need(exp_prefix(Fraction(7), 6) > 480, "unproved log(480) bound") + need(exp_prefix(Fraction(5), 3) > 24, "unproved log(24) bound") + need(certificate.error_margin > 0, "prime-count error bound not established") + need(certificate.quota_margin > 0, "prime quota bound not established") + need(certificate.error_derivative_gap > 0, "error monotonicity not established") + need(certificate.quota_derivative_gap > 0, "quota monotonicity not established") + + +def integer_endpoint(power: int) -> dict[str, int | bool]: + """A second endpoint calculation uses e > 8/3 and integer powers only.""" + need(type(power) is int and 2 <= power <= 32, "invalid integer cutoff") + need(power % 2 == 0, "invalid integer square root") + z_power = power // 2 + exponent = (1 << z_power) // 4 + need(exp_prefix(Fraction(1), 3) == Fraction(8, 3), "wrong e lower bound") + left = 8**exponent + right = 480 * (1 << (671 * z_power)) * 3**exponent + need(left > right, "integer error comparison failed") + # e > 2 and 24 < 2^5 avoid constructing an ell/4-bit integer. + need((1 << power) // 4 > 5 + 669 * power, "integer quota comparison failed") + return { + "power": power, + "exponential_power": exponent, + "left_bits": left.bit_length(), + "right_bits": right.bit_length(), + "strict_comparison": True, + } + + +def rejected(call, *args) -> None: + try: + call(*args) + except ValueError: + return + raise ValueError("negative control was accepted") + + +def controls(certificate: Certificate) -> int: + rejected(validate, endpoint(28, Fraction(7, 10))) + rejected(integer_endpoint, 28) + rejected(validate, endpoint(30, Fraction(2, 3))) + rejected(validate, replace(certificate, error_margin=Fraction(1))) + rejected(validate, replace(certificate, quota_margin=Fraction(1))) + rejected(validate, replace(certificate, error_derivative_gap=0)) + rejected(validate, replace(certificate, quota_derivative_gap=0)) + rejected(endpoint, True, Fraction(7, 10)) + rejected(endpoint, 29, Fraction(7, 10)) + rejected(endpoint, 34, Fraction(7, 10)) + rejected(endpoint, 30, 0.7) + rejected(exp_prefix, Fraction(8), 3) + return 12 + + +def main() -> None: + certificate = endpoint(30, Fraction(7, 10)) + validate(certificate) + integer_check = integer_endpoint(30) + control_count = controls(certificate) + 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} + payload = { + "status": "PASS_MANY_AXIS_PRIME_CUTOFF", + "claim_type": "scoped proof with exact endpoint certificates", + "old_cutoff": 1 << 32, + "new_cutoff": 1 << certificate.power, + "cutoff_reduction_factor": 4, + "log2_upper": str(certificate.log2_upper), + "error_log_upper": str(-certificate.error_margin), + "quota_log_margin_lower": str(certificate.quota_margin), + "error_derivative_gap": certificate.error_derivative_gap, + "quota_derivative_gap": certificate.quota_derivative_gap, + "integer_endpoint": integer_check, + "rejected_controls": control_count, + "package_sha256": hashes, + } + print(json.dumps(payload, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()