[Matarener]

Requested by Mark

Change and mathematical scope

Audit with a positive scoped result; no new κ. The selected κ stays 0.001672660197076918.

This audits one all-size premise of #4100: the fine-prime interval and search step (vendor/FINE-PRIME.md §1). It is used by PROOF.md "Sizes, setup and elementary fallback" at epsilon = 1 - 10^-30 and by GAUSSIAN.md lines 13–19. The step holds as stated, and no correction is needed:

• Citation. Trudgian's Theorem 2 (arXiv:1401.2689v2) matches the statement used: constants 0.2795 and 6.455, valid for x >= 229.
• Theta range. For s in ((1-2eta)t, (1-eta)t] with eta = 1/(4p^2), 1/(4p^2) < theta < 1/(2p^2-1) <= 1/p^2. This is checked exactly for p = 2..199 and is uniform in p.
• Dominance. The main term is at least eta t/log t, and the two endpoint errors are bounded by their value at t. The interval therefore holds at least t/(8p^2 log t) primes, more than d, once 16 p^2 · 0.2795 · L^(1/4) · exp(-sqrt(L/6.455)) <= 1. This holds eventually because L = log t = Theta(p^(10^-30)).
• Threshold. The test needs about ell >= 6.455 (2 ln p)^2/ln 2. With caller constant ell ≈ p^(10^-30)/6, it first holds near ln p ≈ 1.5·10^32. Smaller inputs use the elementary fallback that PROOF.md already specifies. This is legitimate for the asymptotic theorem, though astronomical. The figure depends on the unspecified constant in d = Theta(p^epsilon).
• Search cost. The search costs d 2^(1.5 ell) poly(p) = 2^o(p).

Remaining obligations are unchanged. FINE-PRIME §2 (conditioning at the smaller theta) is not audited here.

Task and overlap

• Card. uniform-transfer-audit, priority revision 7. Scope is refined to this one proposition at its caller.
• Base and pins. Base 12fa8c5c844be21bfefb38a19503fbd867a11244. Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100 is pinned through the package sources.
• Overlap. The Map independent audit coverage of #4100's obligations (navigation; no new κ) #4311 coverage map lists "the fine-prime interval at Propose unconditional κ = 0.00173097911567079247276057 via batched CRT #4100's parameters" with no audit found, and a search for Trudgian or fine-prime PRs since 2026-10-19 found none.
• Prove source-bound prime supply for the many-axis tensor caller #4029 (ToikY) proves prime supply in (t(1-1/(3d)), t(1-1/(4d))] for d <= ell^334. At epsilon = 1 - 10^-30, log d/log ell ≈ 10^30, so that lemma does not cover this caller.
• Audit: PR1786 fine-prime transfer lemmas checked exactly; outer headroom 1.68e-10 on the PR1699 supplier (no new kappa) #1797 audited the older PR1786 interval.

Validation

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

All of these pass on CPython 3.12 (Windows), and scripts/check_research_commit.py passes. The verifier first binds every quoted statement to the pinned #4100 and #4029 bytes. It then checks:

• the exact theta endpoints;
• the dominance threshold, computed in the log domain in floating point and reported for orientation, not as a proof;
• exact segmented-sieve counts for p in {2,3,4,6,8,12} and ell in {24,28}, which give about twice the claimed minimum. These sizes are below the Trudgian threshold, so they are sanity checks only.

Rejecting controls:

• log t = Theta(log p) never passes dominance.
• Prove source-bound prime supply for the many-axis tensor caller #4029's domain excludes the caller.
• eta = 0 gives no admissible theta.
• The sieve is checked against a direct count.

The proof itself is the written argument in the README; the finite checks do not prove it.

Credit

The construction is by Cinna Davis (#4100) and the cited theorem by Tim Trudgian. The neighbouring lemma is ToikY's #4029, and the coverage map is #4311 (Ryanson Jonathan). Prepared for Mark (Matarener) with substantial Claude Code assistance. Apache-2.0.

Open next questions

FINE-PRIME §2: does ||K^-1|| <= O(alpha^5 rho^2 theta^-2 exp(a rho/3)) stay polynomial at theta = 1/(4p^2) at the GAUSSIAN.md caller? First step: compare it against PR1758's explicit symbol bound. See TASK.json.

🤖 Generated with Claude Code