8 Reusable formal infrastructure
These are significant ordinary-Lean or conditional interfaces developed or exposed alongside the production proof. Some occur in the final theorem’s current cone; the large-sieve and squarefree-density nodes are intentionally shown as reusable side results rather than claimed production dependencies.
Trust tier: BT-U. The classical additive large-sieve inequality holds for arbitrary complex coefficients in the repository’s separated-point formulation.
Source: montgomery-vaughan-hilbert-1974, Theorem 1 and Corollary 1, pp. 73–74 [adapted] Source: yangjit-2022, equations 1.2–1.4 and Lemmas 2.1–2.2 [method] Source: iwaniec-kowalski-2004, Theorem 7.7 [method]
Apply the unconditional cosecant Hilbert norm bound to the off-diagonal Gram matrix and add the diagonal contribution.
Trust tier: BT-U. Averaging over squarefree dilations yields the Montgomery \(\sum \mu ^2(r)/\varphi (r)\) amplification of the large sieve.
Source: helfgott-minor-2013, Section 4.2, Lemma 4.3 and equations 4.38–4.40, p. 45 [method] Source: iwaniec-kowalski-2004, Lemma 7.15 [adapted]
Apply Montgomery’s prime-support estimate at each squarefree dilation, sum and identify the resulting fan energy, then apply the classical large sieve once to the full well-spaced fan.
Trust tier: BT-U. The amplified inequality implies the single-point \((\varphi (q)/q)\log R\) large-sieve gain.
Source: helfgott-minor-2013, Section 4.2, Lemma 4.3 and equations 4.38–4.40, p. 45 [derived]
Lower-bound the squarefree amplification sum by its explicit totient/logarithm estimate and rearrange.
Trust tier: BT-U. The squarefree count satisfies \(|Q(x)-(6/\pi ^2)x|\le 3\sqrt{x}+2\).
Source: cohen-dress-el-marraki-2007, Lemma 1, p. 55 [method]
Expand \(\mu ^2\) by square divisors, isolate the main zeta value, and bound the floor and tail errors explicitly.
Trust tier: BT-C. The finite \(m^\star \) table through \(1.4\cdot 10^8\) and the explicit little-Mertens tail imply \(m^\star (N)\log (N+1)\le 4/5\).
Source: ramare-2015, Section 7, equation 7.1 and Lemma 7.1, p. 1375; Lemma 7.4 and equations 7.2–7.3, pp. 1376–1377 [adapted] Source: ramare-2013, Corollary 1.4 and the following sentence, p. 366 [adapted]
Split at successive fourth roots until the argument enters the finite table, and use the analytic tail bound on every continuation step.
Trust tier: BT-C. A first-Mertens table through \(10^8\) and the four Lemma-7.1 rows imply the readable corrected finite certificate bundle.
Normalize the checker contracts to the paper variables and project the required endpoint and coefficient inequalities.
Trust tier: BT-C. The displayed finite forms of equations (4.10) and (8.9) imply the Rosser–Schoenfeld Mertens-product upper bound for \(x\ge 286\).
Split into the seed, finite ladder, and analytic tail ranges; in each range substitute the corresponding explicit input and match at the shared endpoints.
Trust tier: BT-C. The literal finite integer-mirror inequality through \(2{,}560{,}000\) implies the singular-series C.17 tail-count estimate.
Prove soundness of the scaled integer accumulator, convert its finite bound to the real count inequality, and attach the analytic tail.
Trust tier: BT-C. The finite interval through \(10^7\) and Chirre–Helfgott Corollary 1.3 imply \(\psi (x)\le 1.03883x\) for all \(x\ge 0\).
Source: chirre-helfgott-2025, Corollary 1.3, p. 4; proof p. 36 [derived] Source: rosser-schoenfeld-1962, Theorem 12, equation 3.35 [source-shaped]
Use the checked step-function interval below the cutoff and the analytic corollary above it, verifying the overlap constants exactly.
Trust tier: BT-C. The finite interval through \(10^6\) and the sharp psi input imply \(\psi (x)-\vartheta (x)\le 1.4262\sqrt{x}\).
Source: rosser-schoenfeld-1962, Theorem 13, equation 3.36 [source-shaped]
Split the prime powers by exponent, control the square term with the psi input, and fold the higher powers into an explicit polynomial envelope.
Trust tier: BT-C. Middle-interval nonnegativity and the von-Mangoldt prefix contract imply \(t g(t)\ge -2.9702\) on the full required domain.
Source: chirre-helfgott-2025, Lemma A.6, p. 42, and Lemma 8.5, pp. 30–31 [adapted]
Cover the compact middle interval by the first contract, express the endpoint ray through the prefix sum, and use monotonicity to join the ranges.
Trust tier: BT-U. The Backlund remainder satisfies \(|f_3(\tau )|\le 0.06\) for \(1\le \tau \le 12\).
Source: titchmarsh-1986, Sections 9.3–9.4, Theorems 9.3–9.4 [method]
Replay a 277-cell ordinary-kernel interval transcript. Each stopped cell uses rational Taylor bounds and the cells cover the whole interval without gaps.