8.1 Primary-source-linked analytic extensions
The following nodes make the source relationship explicit even when the Lean result is independently proved, restricted to a safe domain, or conditional on a certificate that the source does not itself provide. The opposite-sign Theorem 3.1 node is a proof-corrected external source atom retained by the extension library; it is dormant in the public theorem’s dependency cone.
Trust tier: DEF. For a primitive nonprincipal character modulo \(q\) and \(T\ge 1\), the multiplicity-counted number of nontrivial zeros differs from \(T\pi ^{-1}\log (qT/(2\pi e))\) by at most \(0.317\log (qT)+6.401\). This is the exact arXiv-v4 source contract; it deliberately excludes the principal character and supplies no proof of the finite or analytic input. The version of record instead prints \(0.315\log (qT)+6.455\) and is not silently substituted here.
Trust tier: BT-C. Trudgian’s primitive-nonprincipal contract together with a separate multiplicity-counted \(q=1\) zeta contract implies Helfgott’s combined \(0.5\log (qT)+17.7\) Riemann–von Mangoldt envelope. The principal branch is kept explicit and no zero-simplicity assumption is introduced.
Source: trudgian-2015, arXiv:1206.1844v4, Theorem 1 and equation (1.1), p. 1; multiplicity via Section 2 argument-principle identity, p. 2 [derived] Source: helfgott-major-2013, Lemma 4.3, equations (4.25)–(4.26), pp. 37–38 [derived]
Split on whether the primitive character is principal. Primitivity forces a principal character to have modulus one, where the separate zeta premise applies; on the nonprincipal branch, weaken Trudgian’s sharper \(0.317/6.401\) constants by elementary logarithmic monotonicity.
Trust tier: BT-U. Under the explicit holomorphy, nonvanishing, boundary, and growth hypotheses, the polynomial Phragmén–Lindelöf bound holds at the strip midpoint.
Choose compatible logarithm branches for the multipliers, apply the strip maximum principle to the normalized function, and remove the auxiliary exponential damping.
Trust tier: BT-U. The midpoint estimate iterates over dyadic strip points and extends by continuity to the full closed strip.
Source: fiori-2025, Theorem 1, pp. 2–4, and Lemma 5 [adapted]
Induct on dyadic subdivisions using the midpoint theorem, then pass to arbitrary closed-strip points through the proved continuity closure.
Trust tier: BT-U. For \(\Re (a){\gt}-1/2\) and arbitrary complex \(z\), the repository’s raw parabolic-cylinder \(U(a,z)\) is given by the right-hand side of DLMF 12.5.1.
Unfold the local raw-\(U\) definition. This establishes the exact integral formula on its domain but does not independently identify a globally normalized analytic continuation.
Trust tier: BT-U. The raw integral definition of \(U(a,z)\) satisfies Weber’s differential equation when \(\Re (a){\gt}-1/2\) and \(\Re (z){\gt}0\).
Source: dlmf-chapter-12, equations 12.2.2 and 12.5.1 [adapted]
Differentiate the DLMF 12.5.1 integral twice and use the proved integration-by-parts identity. Both domain restrictions remain visible rather than assuming global analytic continuation.
Trust tier: BT-U. For positive real part of \(s\), the twisted-Gaussian Mellin transform is \(\Gamma (s)e^{-\pi ^2\delta ^2}U(s-1/2,-2\pi i\delta )\).
Source: helfgott-major-2013, Section 3.2, equation 3.8, p. 12 [derived] Source: dlmf-chapter-12, equation 12.5.1 [derived]
Substitute \(a=s-1/2\) and \(z=-2\pi i\delta \) in the integral representation and simplify its Gamma and exponential factors.
Trust tier: EA-U. For \(\sigma \ge 0\), nonzero \(\tau \) and \(\delta \), and \(\delta \tau {\lt}0\), the recurrence-continued twisted-Gaussian Mellin transform satisfies the three-term bound in Helfgott equations (3.1)–(3.2). The \(C_2\) term uses the full falling-product form of \(P_\sigma \) displayed by the paper’s repeated-integration-by-parts proof.
This declaration is a named external analytic source atom, not a Lean proof. It is dormant: the production theorem uses the independently proved live-cone estimate, so this atom is absent from the public axiom closure.
Trust tier: BT-U. For every positive \(\sigma \), \(|\tau |\ge 2\), and matching signs, the twisted-Gaussian Mellin transform satisfies the second bound in Helfgott equation (3.3).
Rotate to the ray \(\pi /4-\frac12\arcsin (2/|\tau |)\), control the two vanishing arcs, evaluate the resulting Gaussian moment, and use the conjugation symmetry for negative \(\tau \).
Trust tier: BT-U. For \(0\le \sigma \le 1\), \(|\tau |\ge 2\), and matching signs, Helfgott’s continued twisted-Gaussian Mellin transform satisfies the first bound in equation (3.3), including the boundary \(\sigma =0\).
Use the integration-by-parts recurrence at the boundary, bound the shifted transforms at real parts one and two by the proved rotated-ray estimate, and use conjugation for negative \(\tau \).
Trust tier: BT-U. The raw Mathlib Mellin transform satisfies the first equation-(3.3) envelope for \(0\le \sigma \le 1\). The positive-\(\sigma \) proof follows the paper; at \(\sigma =0\) Mathlib’s totalized integral is zero, unlike the paper’s continued transform.
Derive the positive-\(\sigma \) range from the continued source theorem using agreement with the convergent Mellin integral. Close the raw-Mellin boundary separately from Mathlib’s nonintegrable-integral convention.
Trust tier: BT-U. The coprime partial sum of \(\mu (n)/n\) has absolute value at most one.
Formalize the Davenport counting and fractional-part argument at an integer endpoint, then pass from real \(x\) to \(\lfloor x\rfloor \) and specialize the positive modulus to a natural.
Trust tier: BT-U. The squarefree coprime \(G_d\) sum satisfies the explicit equation-12.12 asymptotic with the stronger corrected constant \(6.11\).
Source: ramare-snirelman-1995, Lemma 3.4 and equations 3.5–3.9 [adapted]
Re-evaluate the Euler-product contribution omitted by the printed numerical estimate and prove the corrected uniform bound.
Trust tier: EF-U. The explicit \(G(z)\le \log z+1.4709\) estimate holds in the production range after its compact head is certified.
Source: ramare-snirelman-1995, Lemma 3.5 part 1 and equation 3.13 [derived]
Join exact finite folds to the analytic tail. The source locator is Lemma 3.5, not the distinct \(G_d\) asymptotic in Lemma 3.4.
Trust tier: BT-U. The analytic Ramaré estimate used by the Section-2.4 Möbius route is proved with the corrected Euler–Maclaurin identity.
Source: ramare-2015, Theorem 1.4, p. 1361 [derived] Source: ramare-corrigendum-2019, corrected Lemma 3.2, pp. 2384–2385 [erratum]
Establish the signed Euler–Maclaurin identity, retain its cancellation, and use the corrigendum’s coefficients and signs.
Trust tier: EF+PF-U. The compact Liouville scan and the proved analytic continuation yield the explicit coprime little-sum tail bound.
Combine the repository-native compact sweep with the formal reindexing and continuation estimates. This does not trust the paper’s separate computation through \(1.1\cdot 10^{10}\).
Trust tier: EF-U. The required equation-2.14 Chebyshev bound follows from a repository finite window joined to the later analytic range.
Source: ramare-rumely-1996, Section 5.2, Theorem 5.2.1, and Table 2, pp. 421–424 [background]
Directly certify the \(2\)–\(4\) million window, then join it to Chirre–Helfgott Lemma 9.2 and Corollary 1.3. The Ramaré–Rumely tag is historical comparison, not a dependency of this Lean proof.
Trust tier: BT-U. The multiplicity-weighted reciprocal-square zeta-zero tail above \(3\cdot 10^{12}\) is at most \(2.96\cdot 10^{-12}\).
Specialize the two-sided ordinate formula at \(m=1\), pass from ordinates to zero moduli, and discharge its Riemann–von Mangoldt input through the repository’s ordinary-kernel Backlund proof.