From ed13be75aaef2d8c33a1f70c40e13bc43dac10df Mon Sep 17 00:00:00 2001 From: Matarener Date: Wed, 21 Oct 2026 17:19:43 +0300 Subject: [PATCH] Audit #4100's fine-prime interval step at its caller (no new kappa) Checks vendor/FINE-PRIME.md section 1 at PROOF.md's epsilon = 1 - 10^-30: cited Trudgian Theorem 2, exact theta range, dominance and its explicit threshold, search cost, and small exact prime counts. The step holds as stated; #4029's d <= ell^334 domain does not cover this caller. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/fine-prime-trudgian-audit/README.md | 83 ++++++++++ .../fine-prime-trudgian-audit/SOURCES.json | 42 +++++ research/fine-prime-trudgian-audit/TASK.json | 74 +++++++++ .../fine-prime-trudgian-audit/VERIFY.json | 32 ++++ .../fine-prime-trudgian-audit/test_verify.py | 39 +++++ research/fine-prime-trudgian-audit/verify.py | 151 ++++++++++++++++++ 6 files changed, 421 insertions(+) create mode 100644 research/fine-prime-trudgian-audit/README.md create mode 100644 research/fine-prime-trudgian-audit/SOURCES.json create mode 100644 research/fine-prime-trudgian-audit/TASK.json create mode 100644 research/fine-prime-trudgian-audit/VERIFY.json create mode 100644 research/fine-prime-trudgian-audit/test_verify.py create mode 100644 research/fine-prime-trudgian-audit/verify.py diff --git a/research/fine-prime-trudgian-audit/README.md b/research/fine-prime-trudgian-audit/README.md new file mode 100644 index 0000000000..158a1abd8a --- /dev/null +++ b/research/fine-prime-trudgian-audit/README.md @@ -0,0 +1,83 @@ +# Fine-prime interval step of #4100 holds at its caller + +**Scoped audit; no new κ, no scientific acceptance of #4100.** Selected κ stays +0.001672660197076918 (#1094). + +## Proposition and caller + +[#4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) (Cinna Davis) selects the +source lengths in PROOF.md "Sizes, setup and elementary fallback". The caller has +`d=Theta(p^epsilon)`, `epsilon=1-10^-30`, targets `t=2^ell` or `2^(ell-1)` with +`ell=Theta(p^(1-epsilon))`, and distinct odd primes `s_i` with `theta_i=t_i/s_i-1` in +`[1/(4p^2),1/p^2]`. The supporting argument is `vendor/FINE-PRIME.md` §1, restated in +GAUSSIAN.md lines 13–19. With `eta=1/(4p^2)` it takes `s` in `((1-2eta)t,(1-eta)t]`. It then +applies Trudgian's Theorem 2 ([arXiv:1401.2689v2](https://arxiv.org/abs/1401.2689v2)): + + |pi(x)-li(x)| <= 0.2795 x (log x)^(-3/4) exp(-sqrt(log x/6.455)), x >= 229. + +The claim is that the interval eventually holds at least `t/(8p^2 log t)` primes. This is more +than `d`, and the trial-division search costs `2^o(p)`. + +The [#4311 coverage map](https://github.com/CrocSwap/integer-mult-bounds/pull/4311) listed +"the fine-prime interval at #4100's parameters" with no audit found. + +## Result + +The step holds as stated. No correction is needed. + +1. **Citation.** The statement, its constants and the range `x>=229` match Theorem 2 of the arXiv HTML v2. +2. **Theta range.** For `s` in the interval, `1/(4p^2) < theta < 1/(2p^2-1) <= 1/p^2`. The lower + end is attained at `s=(1-eta)t`. The open end corresponds to `s -> (1-2eta)t`. This is checked + exactly for `p=2..199`, and the algebra is uniform in `p`. Each `s_i/t_i > 1-1/(2p^2)`, so + `S/T > 1-d/(2p^2) > 1/2` whenever `d<=p`. +3. **Dominance.** `li((1-eta)t)-li((1-2eta)t) >= eta t/log t`. The function + `x(log x)^(-3/4)exp(-sqrt(log x/R))` increases for `x>=229`, so both endpoint errors are at most + its value at `t`. If `16 p^2 * 0.2795 * L^(1/4) * exp(-sqrt(L/6.455)) <= 1` with `L=log t`, the + count is at least `eta t/(2L) = t/(8p^2 log t)`. Here `L=Theta(p^(10^-30))`, which outgrows + `(2 log p)^2`, so the test holds for all large `p`. The count then exceeds `d`, because `t` is + exponential in `p^(10^-30)` while `d p^2 log t` is polynomial in `p`. +4. **Explicit threshold.** The required `ell` is about `6.455 (2 ln p)^2 / ln 2`. With the caller + constant taken as `ell ≈ p^(10^-30)/6`, the test first holds at `ln p ≈ 1.5·10^32`. Smaller + inputs use the elementary fallback that PROOF.md already specifies, which affects only finitely + many lengths. The value is legitimate but astronomical. It depends on the unspecified constant + in `d=Theta(p^epsilon)` and is reported for orientation, not as a claim. +5. **Search cost.** The interval has `eta t` candidates and each needs `O(sqrt t)` trial divisions, + so the total is `d 2^(1.5 ell) poly(p)`. Its logarithm is `O(p^(10^-30)+log p)=o(p)`, which + gives setup `2^o(p)=o(V)`. +6. **Small exact counts.** For `p` in {2,3,4,6,8,12} and `ell` in {24,28}, a segmented sieve finds + about twice `t/(8p^2 log t)` primes in the interval. Trudgian's test does not yet apply at these + sizes, so these counts are sanity checks only. + +**Relation to #4029.** [#4029](https://github.com/CrocSwap/integer-mult-bounds/pull/4029) (ToikY) +proves prime supply in `(t(1-1/(3d)), t(1-1/(4d))]` for `2<=d<=ell^334`. At `epsilon=1-10^-30`, +`log d/log ell ≈ 10^30`, so that domain does not reach #4100's caller. #4100 therefore needs its +own Trudgian argument, which is the one checked here. #1797 audited the older conditional +PR1786 interval with `theta>=1/(4d)`. + +## Reproduce + +```sh +python3.12 -B research/fine-prime-trudgian-audit/verify.py +python3.12 -B research/fine-prime-trudgian-audit/test_verify.py +python3.12 scripts/research_package.py --package research/fine-prime-trudgian-audit +``` + +Each run takes under a second. The rejecting controls are: + +- `log t=Theta(log p)` never passes dominance. +- The #4029 domain excludes the caller. +- `eta=0` gives no admissible `theta`. +- A direct sieve sanity count. + +## Open next questions + +- **FINE-PRIME §2 conditioning at the smaller theta.** Does + `||K^-1|| <= O(alpha^5 rho^2 theta^-2 exp(a rho/3))` stay polynomial at the GAUSSIAN.md caller + when `theta=1/(4p^2)`? The fine primes help only if it does. First step: compare it against + PR1758's explicit symbol bound. Nothing blocks it. See `open_questions` in [TASK.json](TASK.json). + +## Credit + +The construction and argument are by Cinna Davis (#4100). The cited prime theorem is due to Tim +Trudgian. The neighbouring prime-supply lemma is ToikY's #4029, and the coverage map is #4311. +This audit was prepared for Mark (Matarener) with substantial Claude Code assistance. Apache-2.0. diff --git a/research/fine-prime-trudgian-audit/SOURCES.json b/research/fine-prime-trudgian-audit/SOURCES.json new file mode 100644 index 0000000000..797ebdbaaa --- /dev/null +++ b/research/fine-prime-trudgian-audit/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/many-axis-prime-supply/README.md", + "usage": "input", + "git_blob": "f3f736734a0d209a5fb383494b2253cc8f7702e4", + "sha256": "68ba22bcf761370c9370f770ed65de0de699feccb89c9011e470e00542ae72e9" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + } + ] +} diff --git a/research/fine-prime-trudgian-audit/TASK.json b/research/fine-prime-trudgian-audit/TASK.json new file mode 100644 index 0000000000..5dff4ea554 --- /dev/null +++ b/research/fine-prime-trudgian-audit/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "refined", + "actual_scope": "One #4100 obligation: the fine-prime interval and search step (vendor/FINE-PRIME.md section 1, used by PROOF.md sizes/setup and GAUSSIAN.md) at the caller's parameters epsilon=1-10^-30, eta=1/(4p^2), t=2^ell.", + "scope_change_reason": "The card allows one precision/conditioning proposition with its caller; the #4311 coverage map lists this prime-interval step as unaudited, so this package narrows to it.", + "bottleneck_link": "Side result for the #4100 admission audit: confirms one all-size premise of the proposed unconditional exponent; it does not move the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the stated proposition is proved or refuted at the caller; do not extend to FINE-PRIME section 2 conditioning.", + "outcome": "completed", + "evidence": "Written check in README.md; verify.py binds sources, checks exact theta endpoints, the explicit Trudgian threshold (ln p ~ 1.5e32 at the caller) and small exact prime counts; test_verify.py has rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does FINE-PRIME section 2 (polynomial conditioning with theta as small as 1/(4p^2)) hold at the GAUSSIAN.md caller?", + "why_it_matters": "The fine primes are useful only if the Gaussian kernel inverse stays polynomial at the smaller theta.", + "first_step": "Check ||K^-1|| <= O(alpha^5 rho^2 theta^-2 exp(a rho/3)) against PR1758's explicit symbol bound with theta=1/(4p^2).", + "blocked_by": "none" + } + ] +} diff --git a/research/fine-prime-trudgian-audit/VERIFY.json b/research/fine-prime-trudgian-audit/VERIFY.json new file mode 100644 index 0000000000..a7e4d94f95 --- /dev/null +++ b/research/fine-prime-trudgian-audit/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/many-axis-prime-supply/README.md", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Bind the cited theorem, eta, epsilon and theta range to the #4100 sources; exact theta endpoints for p=2..199; Trudgian dominance threshold at the caller's epsilon; exact small prime counts." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "Rejecting controls: log t=Theta(log p) fails dominance; #4029's d<=ell^334 domain excludes epsilon=1-1e-30; eta=0 gives no admissible theta; sieve sanity." + } + ] +} diff --git a/research/fine-prime-trudgian-audit/test_verify.py b/research/fine-prime-trudgian-audit/test_verify.py new file mode 100644 index 0000000000..ed655e9ad4 --- /dev/null +++ b/research/fine-prime-trudgian-audit/test_verify.py @@ -0,0 +1,39 @@ +#!/usr/bin/env python3 +"""Rejecting controls for the fine-prime interval audit.""" +import math +import sys +from fractions import Fraction +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify # noqa: E402 + + +def main(): + # 1. If log t were only Theta(log p) (ell = 3 log2 p), the dominance test + # never passes: the p^2 factor beats exp(-sqrt(log t / R)). + for e in [2, 10, 100, 300]: + log_p = e * math.log(10) + assert not verify.dominance(log_p, 3 * log_p) + + # 2. #4029's prime supply needs d <= ell^334. At epsilon = 1 - 1e-30, + # log d / log ell = epsilon / (1 - epsilon) ~ 1e30, far outside it. + eps = Fraction(1) - Fraction(1, 10**30) + assert eps / (1 - eps) > 334 + + # 3. Without the -2eta shift the interval collapses: eta = 0 gives no theta >= 1/(4p^2). + p = 5 + assert 1 / (1 - Fraction(0)) - 1 < Fraction(1, 4 * p * p) + + # 4. Sieve sanity against a direct count. + assert verify.count_primes(100, 200) == sum( + 1 for n in range(101, 201) if all(n % q for q in range(2, math.isqrt(n) + 1))) + + # 5. The small-count rows are below the Trudgian threshold: they are sanity + # checks only, not evidence for the asymptotic step. + assert not verify.dominance(math.log(12), 28 * math.log(2)) + print("PASS_FINE_PRIME_AUDIT_CONTROLS") + + +if __name__ == "__main__": + main() diff --git a/research/fine-prime-trudgian-audit/verify.py b/research/fine-prime-trudgian-audit/verify.py new file mode 100644 index 0000000000..8c2c12e28c --- /dev/null +++ b/research/fine-prime-trudgian-audit/verify.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Audit the fine-prime interval step of the proposed #4100 construction. + +Proposition (vendor/FINE-PRIME.md section 1, used by PROOF.md "Sizes, setup and +elementary fallback" and GAUSSIAN.md lines 13-19): with eta = 1/(4p^2) and a +dyadic target t = 2^ell, ell = Theta(p^(1-epsilon)), epsilon = 1 - 10^-30, the +interval ((1-2eta)t, (1-eta)t] eventually holds at least t/(8 p^2 log t) +primes, more than d = Theta(p^epsilon), and every prime s there gives +theta = t/s - 1 in [1/(4p^2), 1/p^2]. + +Checks: +1. source binding: the cited theorem, eta, epsilon and theta range are read + from the pinned #4100 files; +2. exact theta endpoints for p = 2..199; +3. the sufficient Trudgian-dominance test and its explicit threshold at the + caller's epsilon (floating point, logarithmic domain; reported, not used + as a proof); +4. exact prime counts (segmented sieve) in small real intervals. +""" +import json +import math +from fractions import Fraction +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +SRC = ROOT / "research" / "unconditional-batched-crt" + +# Trudgian, arXiv:1401.2689v2, Theorem 2: for x >= 229, +# |pi(x) - li(x)| <= 0.2795 x (log x)^(-3/4) exp(-sqrt(log x / 6.455)). +A, R, X0 = 0.2795, 6.455, 229 + + +def check_sources(): + fine = (SRC / "vendor" / "FINE-PRIME.md").read_text(encoding="utf-8") + proof = (SRC / "PROOF.md").read_text(encoding="utf-8") + gauss = (SRC / "GAUSSIAN.md").read_text(encoding="utf-8") + for needle in ["eta_p = 1/(4p^2)", "(1-2 eta_p) t_i < s_i <= (1-eta_p) t_i", + "|pi(x)-li(x)| <= 0.2795 x (log x)^(-3/4)", + "exp(-sqrt(log x/6.455))", "for x>=229", + "x/(8p^2 log x)", "1/(4p^2) < theta_i <= 1/(2p^2-1) <= 1/p^2"]: + assert needle in fine, needle + assert "d=Theta(p^epsilon), epsilon=1-10^-30" in proof + assert "ell=Theta(p^(1-epsilon))" in proof + assert "theta_i in [1/(4p^2),1/p^2]" in proof + assert "log t=Theta(p^(1-epsilon))" in gauss + supply = (ROOT / "research" / "many-axis-prime-supply" / "README.md").read_text(encoding="utf-8") + assert "2≤d≤ell^334" in supply and "(t(1−1/(3d)), t(1−1/(4d))]" in supply + + +def check_theta(): + for p in range(2, 200): + eta = Fraction(1, 4 * p * p) + closed = 1 / (1 - eta) - 1 # s = (1-eta)t, attained + open_ = 1 / (1 - 2 * eta) - 1 # s -> (1-2eta)t, not attained + assert Fraction(1, 4 * p * p) < closed < open_ + assert open_ == Fraction(1, 2 * p * p - 1) <= Fraction(1, p * p) + # capacity: s/t > 1 - 2 eta for each axis, so S/T > 1 - d/(2p^2) > 1/2 for d <= p + assert 1 - Fraction(p, 2 * p * p) > Fraction(1, 2) + + +def dominance(log_p, L): + """True if 2*Trudgian error <= half of the main term eta*t/log t at log t = L. + + Equivalent to log(16) + 2 log p + log L + log(0.2795) - 0.75 log L + - sqrt(L/R) <= 0. Both endpoint errors are bounded by the value at t, + since x (log x)^(-3/4) exp(-sqrt(log x/R)) increases for x >= 229. + """ + return (math.log(16) + 2 * log_p + 0.25 * math.log(L) + math.log(A) + - math.sqrt(L / R)) <= 0 + + +def needed_L(log_p): + lo, hi = math.log(X0), 1e6 + while not dominance(log_p, hi): + hi *= 2 + for _ in range(200): + mid = (lo + hi) / 2 + lo, hi = (lo, mid) if dominance(log_p, mid) else (mid, hi) + return hi + + +def caller_threshold(delta=1e-30, const=6.0): + """Smallest ln p with ell = p^delta/const >= needed ell, by bisection on ln p.""" + def ok(u): + return delta * u - math.log(const) >= math.log(needed_L(u) / math.log(2)) + lo, hi = 1.0, 1e36 + assert not ok(lo) and ok(hi) + for _ in range(400): + mid = math.sqrt(lo * hi) + lo, hi = (lo, mid) if ok(mid) else (mid, hi) + return hi + + +def small_primes(n): + s = bytearray([1]) * (n + 1) + s[0:2] = b"\x00\x00" + for i in range(2, int(n ** 0.5) + 1): + if s[i]: + s[i * i::i] = bytearray(len(s[i * i::i])) + return [i for i in range(n + 1) if s[i]] + + +def count_primes(a, b): + """Number of primes in (a, b].""" + lo = a + 1 + seg = bytearray([1]) * (b - lo + 1) + for q in small_primes(math.isqrt(b)): + start = max(q * q, (lo + q - 1) // q * q) + seg[start - lo::q] = bytearray(len(seg[start - lo::q])) + return sum(seg) + + +def check_counts(): + rows = [] + for p in [2, 3, 4, 6, 8, 12]: + for ell in [24, 28]: + t = 2 ** ell + eta = Fraction(1, 4 * p * p) + a = math.floor((1 - 2 * eta) * t) + b = math.floor((1 - eta) * t) + if b - a > 3_000_000: + continue + cnt = count_primes(a, b) + claim = t / (8 * p * p * math.log(t)) + assert cnt > claim, (p, ell, cnt, claim) + rows.append({"p": p, "ell": ell, "primes": cnt, "claimed_min": round(claim, 1), + "trudgian_test_applies": dominance(math.log(p), math.log(t))}) + assert len(rows) == 9 and not any(r["trudgian_test_applies"] for r in rows) + return rows + + +def main(): + check_sources() + check_theta() + thresholds = {str(e): round(needed_L(e * math.log(10)) / math.log(2), 1) + for e in [1, 2, 3, 10, 100, 10**6, 10**30]} + # needed ell grows like (2 ln p)^2 * R / ln 2: polynomial in log p + ratio = needed_L(1e30 * math.log(10)) / (6.455 * (2 * 1e30 * math.log(10)) ** 2) + assert 0.99 < ratio < 1.01 + ln_p = caller_threshold() + assert 1e32 < ln_p < 2e32 + rows = check_counts() + out = {"needed_ell_by_log10_p": thresholds, "caller_threshold_ln_p": ln_p, + "small_counts": rows} + print(json.dumps(out, indent=1)) + print("PASS_FINE_PRIME_INTERVAL_STEP_AS_STATED") + + +if __name__ == "__main__": + main()