Audit #4100's fine-prime interval step: Trudgian bound holds at epsilon = 1 - 1e-30 (no new κ)

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.

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"
+    }
+  ]
+}

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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()