Citation: Harald Andrés Helfgott, The ternary Goldbach problem, Snapshots of Modern Mathematics from Oberwolfach 2014-03
Audited version: 2014 English snapshot, DOI 10.14760/SNAP-2014-003-EN
Audit status: historical background reference
Inspection scope: The 1742 Goldbach–Euler correspondence, the historical wording of the conjecture, and a short account of the ternary problem
Bibliography entry: REFERENCES.md#helfgott-snapshot-2014
Primary locators: https://doi.org/10.14760/SNAP-2014-003-EN; https://publications.mfo.de/handle/mfo/429. No claim node. This expository snapshot supplies historical context for the README. It is not a named trust atom or a claim-level dependency of the formal proof.

Citation: G. H. Hardy and J. E. Littlewood, Some problems of Partitio numerorum; III: On the expression of a number as a sum of primes, Acta Math. 44, 1–70
Audited version: version of record
Audit status: historical background reference
Inspection scope: Historical statement of the Hardy–Littlewood ternary-prime heuristic and asymptotic program
Bibliography entry: REFERENCES.md#hardy-littlewood-1923
Primary locators: https://doi.org/10.1007/BF02403921; https://archive.ymsc.tsinghua.edu.cn/pacm_paperurl/20170108203038474495327. No claim node. This paper supplies historical context for the README. It is not a named trust atom or a claim-level dependency of the formal proof.

Citation: I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akademii Nauk SSSR 15, 291–294
Audited version: original 1937 Russian publication
Audit status: historical background reference
Inspection scope: The original unconditional theorem that every sufficiently large odd integer is a sum of three primes
Bibliography entry: REFERENCES.md#vinogradov-1937
Primary locators: https://www.mathnet.ru/eng/person26537#bib65. No claim node. This paper supplies historical context for the README. It is not a named trust atom or a claim-level dependency of the formal proof.

Citation: Andrés Chirre and Harald Andrés Helfgott, Optimal bounds for sums of non-negative arithmetic functions
Audited version: arXiv:2512.15709v1
Audit status: claim-level primary-source audit
Inspection scope: Corollary 1.3 and its proof; Proposition 7.7; Lemmas 8.5, 9.2, A.6, and A.7, including the displayed ranges and finite-computation prose
Bibliography entry: REFERENCES.md#chirre-helfgott-2025
Primary locators: https://arxiv.org/abs/2512.15709v1. Mapped claims:

• reuse:psi-sharp: derived, Corollary 1.3, p. 4; proof p. 36. The Lean continuation packages the paper estimate with separately exposed finite and analytic inputs.

• reuse:chirre-helfgott-a6: adapted, Lemma A.6, p. 42, and Lemma 8.5, pp. 30–31. This is a continuation theorem using a certified Lemma-8.5 anchor, not a literal formalization of Lemma A.6 alone.

• cite:ch25-lemma-9-2-psi: source-shaped, Lemma 9.2, pp. 35–36. The atom retains the paper’s normalized quotient, real range, and inequality.

• cite:ch25-proposition-7-7-platt-head-2e4: adapted, Proposition 7.7, pp. 25–27. The paper prints the factor-two reciprocal aggregate and credits Platt’s zero list; the live atom is an adapted multiplicity-preserving enumeration handoff, while the local Lean certificate derives the aggregate.

• cite:ch25-lemma-a7-arb-boundary: source-shaped, Lemma A.7, pp. 42–43. The comparison card expands the regularized function and boundary convention.

• cite:ch25-proposition-7-7-platt-head-2e4: derived, Lemma A.7, pp. 42–43. The stated absence of low nontrivial zeros is now a Lean theorem derived from this shared multiplicity-preserving Proposition-7.7 zero enumeration.

Citation: LMFDB Collaboration, Riemann zeta zero data: source, completeness, and rigor statements
Audited version: public knowledge pages accessed 2026-07-19
Audit status: verification-artifact provenance audit
Inspection scope: Source attribution to David Platt, absolute ordinate precision, and rigorous completeness of the published Riemann-zeta zero data
Bibliography entry: REFERENCES.md#lmfdb-zeta-zero-data
Primary locators: https://www.lmfdb.org/knowledge/show/rcs.source.zeros.zeta; https://www.lmfdb.org/knowledge/show/rcs.cande.zeros.zeta; https://www.lmfdb.org/knowledge/show/rcs.rigor.zeros.zeta. Mapped claims:

• cite:ch25-proposition-7-7-platt-head-2e4: local-reproduction, source, completeness, and rigor knowledge pages. The independent repository fold uses LMFDB’s Platt data and preserves the published precision and completeness provenance; the live atom remains the multiplicity-preserving enumeration handoff documented by its card.

Citation: FLINT developers, acb_dirichlet Riemann-zeta zero-counting and isolation routines
Audited version: FLINT 3.6.0
Audit status: verification-tool provenance audit
Inspection scope: Certified Riemann-zeta zero counting, isolation, and interval arithmetic used by the independent Proposition 7.7 recomputation
Bibliography entry: REFERENCES.md#flint-acb-dirichlet-3-6
Primary locators: https://flintlib.org/doc/acb_dirichlet.html#riemann-zeta-function-zeros; https://github.com/flintlib/flint/tree/v3.6.0/src/acb_dirichlet. Mapped claims:

• cite:ch25-proposition-7-7-platt-head-2e4: local-reproduction, Riemann zeta function zeros documentation and FLINT 3.6.0 acb_dirichlet source. The repository’s independent external certificate invokes these Arb/FLINT routines; this software provenance is separate from the Chirre–Helfgott paper statement and from the Lean kernel.

Citation: Dave Platt and Tim Trudgian, The Riemann hypothesis is true up to 3 times 10 to the 12th power, BLMS 53, 792–797
Audited version: arXiv:2004.09765v1 and version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorem 1, including the exact verified height and multiplicity formulation
Bibliography entry: REFERENCES.md#platt-trudgian-2021
Primary locators: https://arxiv.org/abs/2004.09765v1; https://doi.org/10.1112/blms.12460. Mapped claims:

• cite:platt-trudgian-rh-zeta-3e12: exact, Theorem 1, p. 2. The exact source height is 3,000,175,332,800; downstream lower-height uses are derived.

Citation: Harald Andrés Helfgott, Minor arcs for Goldbach’s problem
Audited version: arXiv:1205.5252v4
Audit status: claim-level primary-source audit
Inspection scope: Main theorem and equations 1.2–1.4; Section 2.4 and equations 2.8–2.11, 2.17, 2.19; Sections 3–5 and Appendix A, especially Lemma A.5 and equation A.5
Bibliography entry: REFERENCES.md#helfgott-minor-2013
Primary locators: https://arxiv.org/abs/1205.5252v4. Mapped claims:

• cite:platt_stronger_range: source-shaped, sentence following equation 2.11, p. 8. The stronger finite interval is retained verbatim as a separate atom.

• reuse:phi-gain-large-sieve: method, Section 4.2, Lemma 4.3 and equations 4.38–4.40, p. 45. The formal phi-gain inequality is proved in Lean from the reusable large-sieve infrastructure.

• reuse:phi-gain-at-r: derived, Section 4.2, Lemma 4.3 and equations 4.38–4.40, p. 45. This is the single-point specialization of the formal phi-gain theorem.

Citation: Harald Andrés Helfgott, Major arcs for Goldbach’s problem
Audited version: arXiv:1305.2897v4
Audit status: claim-level primary-source audit
Inspection scope: Theorems 1.4 and 3.1, equations 3.1–3.3 and 3.8; Lemmas 4.1–4.3, equations 4.24–4.28, Proposition 4.8, Corollary 4.9, and Section 4.6
Bibliography entry: REFERENCES.md#helfgott-major-2013
Primary locators: https://arxiv.org/abs/1305.2897v4. Mapped claims:

• cite:helfgott-major-4-6-platt-dirichlet: derived, Section 4.6, pp. 56–59. The card derives Helfgott’s three restricted ranges as a theorem from the stronger source-shaped Platt atom.

• reuse:helfgott-thm31-opp: erratum, Theorem 3.1, equations 3.1–3.2, pp. 9–10; repeated-integration-by-parts display, pp. 25–26. The dormant Lean atom retains sigma >= 0, nonzero tau, opposite signs, and the recurrence-defined continuation; delta != 0 is retained explicitly although implied by delta*tau < 0. Its P_sigma uses the falling-product coefficients shown by the proof, correcting the abbreviated final coefficient printed in equation (3.2). It is not in ternary_goldbach’s current axiom closure.

• reuse:helfgott-thm31-same-arb: local-reproduction, Theorem 3.1, equation 3.3 second alternative, pp. 9–10; proof equation 3.66, p. 26. The Lean rotated-ray proof covers the paper’s full positive-sigma range and uses the raw Mellin integral only where it is absolutely convergent.

• reuse:helfgott-thm31-same-low: local-reproduction, Theorem 3.1, equation 3.3 first alternative, pp. 9–10; proof equations 3.66–3.67, pp. 26–27. The Lean theorem uses Helfgott’s one-step recurrence to cover the continued value at sigma zero, shifted rotated-ray bounds at real parts one and two, and conjugation for negative ordinates.

• reuse:helfgott-thm31-same-low-raw: adapted, Theorem 3.1, equation 3.3 first alternative, pp. 9–10; proof equations 3.66–3.67, pp. 26–27. For positive sigma this is the rotated-ray proof; at sigma zero the Lean theorem uses Mathlib’s totalized raw Mellin value zero rather than Helfgott’s continued transform.

• reuse:parabolic-mellin: derived, Section 3.2, equation 3.8, p. 12. The exact Mellin identity is proved from the DLMF integral representation.

• reuse:trudgian-rvm-bridge: derived, Lemma 4.3, equations (4.25)–(4.26), pp. 37–38. The Lean bridge keeps the primitive-nonprincipal Trudgian branch and the separate q=1 zeta branch explicit before recovering Helfgott’s combined envelope.

Citation: Harald Andrés Helfgott, The ternary Goldbach problem
Audited version: arXiv:1501.05438v2
Audit status: claim-level primary-source audit
Inspection scope: Proposition 10.4.1; Lemma 11.2.2; Propositions 11.2.3 and 12.2.4; equations 13.14–13.17, 14.2, 14.7–14.14, 14.27, and 14.49–14.51; Appendices A and C
Bibliography entry: REFERENCES.md#helfgott-ternary-2015
Primary locators: https://arxiv.org/abs/1501.05438v2. Mapped claims:

• cite:helfgott_prop_12_2_4: source-shaped, Proposition 12.2.4, pp. 236–242. The card maps equations 12.24 and 12.30–12.33 and records the surrounding small-R issue.

• tg:major-14-2: adapted, equation 14.2, p. 260. The production theorem specializes the paper envelope at the explicit threshold.

• tg:major-14-7-upper: adapted, equation 14.7, p. 261. The upper estimate is assembled from source-shaped analytic and finite inputs.

• tg:major-14-7-lower: adapted, equation 14.7, p. 261. The lower block includes repository-certified smoothing and Mertens bounds.

• tg:major-prop-10-4-1: adapted, Proposition 10.4.1, pp. 213–215. The Lean consumer uses an explicit weighted-threshold specialization.

• tg:major-14-14: derived, equations 14.10–14.14, pp. 261–263. The explicit lower constant is proved by exact rational enclosures.

• tg:major-14-9: adapted, equations 14.8–14.9, p. 261. The source-shaped odd singular factor is discharged by a finite product and Euler-tail proof.

• tg:major-14-27: weakened, equation 14.27, p. 267. The repository keeps a conservative outward-rounded major coefficient.

• tg:minor-13-14-low: adapted, equation 13.14, pp. 249–250. This low-denominator branch includes an explicit ten-percent repair term absent from the printed equation.

• tg:minor-13-14-medium: adapted, equation 13.14, pp. 249–250. The denominator range and repair allowance are repository refinements.

• tg:minor-13-14-small-q: adapted, equation 13.14, pp. 249–250. The compressed crossover is a repository interval decomposition.

• tg:minor-13-14-uniform: derived, equation 13.14, pp. 249–250. The conditional theorem combines the separately visible regional caps.

• tg:minor-13-15-cap: adapted, equation 13.15, p. 250. The fixed cap includes conservative repair costs.

• tg:minor-13-15-uniform: derived, equation 13.15, p. 250. The uniform theorem is derived from the explicit cap.

• tg:minor-13-16-high-q: adapted, equation 13.16, p. 250. The high-denominator case is closed with formal large-sieve and finite inputs.

• tg:minor-13-17-sup: derived, equation 13.17, p. 250. This conditional supremum packages the three formal denominator cases.

• tg:minor-14-49: weakened, equation 14.49, p. 275. The repository proves the intentionally larger conservative coefficient 1.048 over 49 through a repaired derivation; it does not claim that the printed 1.00948 over 49 is an erratum.

• tg:prime-power-tail: adapted, equations 14.50–14.51, pp. 275–276. A sharper explicit mixed prime-power tail is certified in Lean.

• tg:closed-large-endpoint: adapted, Chapter 14, pp. 260–276. The closed endpoint combines corrected major, minor, and tail components.

Citation: Harald Andrés Helfgott, The ternary Goldbach conjecture is true
Audited version: arXiv:1312.7748v2
Audit status: background provenance audit
Inspection scope: Sections 1–7 and appendices; contents and numbered structure checked against the distinct monograph
Bibliography entry: REFERENCES.md#helfgott-ternary-article-2013
Primary locators: https://arxiv.org/abs/1312.7748v2. No claim node. This shorter article is not an alternate source for Chapters 8–14 of arXiv:1501.05438v2. The live chapter-numbered claims use the monograph, so no claim-level Blueprint edge is asserted here.

Citation: Harald Andrés Helfgott and David J. Platt, Numerical verification of the ternary Goldbach conjecture up to 8.875 times 10 to the 30th power
Audited version: arXiv:1305.3062v2
Audit status: claim-level primary-source audit
Inspection scope: Theorem 4.1 and Sections 3–4 describing the computation and loss of per-range data files
Bibliography entry: REFERENCES.md#helfgott-platt-2013
Primary locators: https://arxiv.org/abs/1305.3062v2. Mapped claims:

• cite:helfgott_platt_theorem_4_1: exact, Theorem 4.1. Oddness, inclusive endpoints, threshold digits, primality, and allowance of repeated primes match exactly.

• tg:finite-provider: derived, Theorem 4.1. The production finite provider is the direct theorem-level adapter from the source-shaped atom.

Citation: Henri Cohen, François Dress, and Mohamed El Marraki, Explicit estimates for summatory functions linked to the Möbius mu-function, FACM 37.1, 51–63
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Lemma 1; Theorems 3 and 3 bis; the F/G table; Lemma 4; Theorems 5 and 5 bis
Bibliography entry: REFERENCES.md#cohen-dress-el-marraki-2007
Primary locators: https://doi.org/10.7169/facm/1229618741; https://www.math.u-bordeaux.fr/~hecohen/artdm4.dvi. Mapped claims:

• cite:cdem-squarefree-verifier-output: local-reproduction, Lemma 1, p. 55, and Theorems 3 and 3 bis. The bounded B1/B2 contracts are repository-selected computations using the paper’s bootstrap, not printed theorem statements.

• cite:cdem-reproducible-table-verifier-output: local-reproduction, Lemma 4, p. 59, and Theorem 5 bis, p. 62. The K=199330, N=5e9 table is repository-designed and differs from the paper’s 63,951-term table.

• reuse:squarefree-asymptotic: method, Lemma 1, p. 55. The formal theorem exposes a conditional squarefree-density bootstrap inspired by the source.

Citation: Greg Hurst, Computations of the Mertens function and improved bounds on the Mertens conjecture, Math. Comp. 87, 1013–1028
Audited version: arXiv:1610.08551v2 and version of record
Audit status: claim-level primary-source audit
Inspection scope: Section 6.1, pp. 1020–1022, including the computation through 10 to the 16th power, extrema, runtime, and independent checks
Bibliography entry: REFERENCES.md#hurst-2018
Primary locators: https://arxiv.org/abs/1610.08551v2; https://doi.org/10.1090/mcom/3275. Mapped claims:

• cite:hurst-mertens-sqrt: background, Section 6.1, pp. 1020–1022. Hurst supplies the underlying computation but does not itself state the exact rational 0.571 square-root theorem.

Citation: Ethan Simpson Lee and Nicol Leong, New explicit bounds for Mertens function and the reciprocal of the Riemann zeta-function
Audited version: arXiv:2208.06141v4
Audit status: claim-level primary-source audit
Inspection scope: Corollary 1.3 equation 4, pp. 2–3, and its proof in Section 5.3, p. 23
Bibliography entry: REFERENCES.md#lee-leong-2024
Primary locators: https://arxiv.org/abs/2208.06141v4. Mapped claims:

• cite:hurst-mertens-sqrt: source-shaped, Corollary 1.3, equation 4; Section 5.3. This is the exact 0.571 square-root piece on 33 through 10 to the 16th power, with endpoint handling documented in the card.

Citation: Olivier Ramaré, Explicit estimates on several summatory functions involving the Moebius function, Math. Comp. 84, 1359–1387
Audited version: version of record, read together with the 2019 corrigendum
Audit status: claim-level primary-source audit
Inspection scope: Theorems 1.1, 1.4, 1.5, and 1.12; Lemma 1.9, Corollary 1.10, Lemmas 2.1, 3.2, 7.1, 7.4, and 10.2; equation 7.1
Bibliography entry: REFERENCES.md#ramare-2015
Primary locators: https://doi.org/10.1090/S0025-5718-2014-02914-1; https://ramare-olivier.github.io/Maths/mcom2914.pdf. Mapped claims:

• reuse:ramare-mstar-continuation: adapted, Section 7, equation 7.1 and Lemma 7.1, p. 1375; Lemma 7.4 and equations 7.2–7.3, pp. 1376–1377. The source supplies the m-star architecture, 33-million table, and continuation estimates and comparisons; the repository extends the table to 140 million, uses log(N+1), and joins it to a separately exposed little-Mertens tail.

• reuse:ramare-thm-1-4: derived, Theorem 1.4, p. 1361. The source-shaped analytic estimate is assembled in Lean; superseded Theorem-1.5 constants are not used as corrected values.

Citation: Olivier Ramaré, Corrigendum to Explicit estimates on several summatory functions involving the Moebius function, Math. Comp. 88, 2383–2388
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Corrected Lemma 3.2, pp. 2384–2385; the distinct corrected Theorem 1.5 was checked but is not an input to this target
Bibliography entry: REFERENCES.md#ramare-corrigendum-2019
Primary locators: https://doi.org/10.1090/mcom/3449. Mapped claims:

• reuse:ramare-thm-1-4: erratum, corrected Lemma 3.2, pp. 2384–2385. The formal Euler–Maclaurin route uses the corrected coefficients and signs in Lemma 3.2. The corrigendum’s corrected Theorem 1.5 constants are a separate result and are not attributed to this target.

Citation: Olivier Ramaré, From explicit estimates for primes to explicit estimates for the Möbius function, Acta Arith. 157.4, 365–379
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorem 1.1; Corollary 1.4 and its following sentence; Lemmas 4.5, 6.2, and 6.3; Section 7
Bibliography entry: REFERENCES.md#ramare-2013
Primary locators: https://doi.org/10.4064/aa157-4-4. Mapped claims:

• reuse:ramare-mstar-continuation: adapted, Corollary 1.4 and the following sentence, p. 366. This source supplies only the 0.03/log little-Mertens tail used by the continuation. The m-star architecture and finite table come from Ramaré 2015 Section 7.

• reuse:ramare-corrected-finite: adapted, Lemmas 4.5, 6.2, and 6.3. This adapter exposes repository-corrected finite seams rather than attributing them verbatim to the paper.

Citation: Olivier Ramaré and Sebastián Zúñiga-Alterman, From explicit estimates for the primes to explicit estimates for the Möbius function – II
Audited version: arXiv:2408.05969v2 and version of record
Audit status: claim-level primary-source audit
Inspection scope: Equation 19, Lemma 6.2 p. 10, and Lemma 7.1 pp. 10–11 with its numerical table
Bibliography entry: REFERENCES.md#ramare-zuniga-alterman-2024
Primary locators: https://arxiv.org/abs/2408.05969v2; https://doi.org/10.7169/facm/250121-19-5. Mapped claims:

• cite:ramare-zuniga-2024-lemma-6-2: exact, equation 19 and Lemma 6.2, p. 10. The real interval, coefficient, floor convention, and normalized sum match the source.

Citation: David J. Platt, Numerical computations concerning the GRH
Audited version: arXiv:1305.3087v1
Audit status: claim-level primary-source audit
Inspection scope: Theorem 7.1, p. 14, including conductor and height ranges
Bibliography entry: REFERENCES.md#platt-2013
Primary locators: https://arxiv.org/abs/1305.3087v1. Mapped claims:

• cite:helfgott-major-4-6-platt-dirichlet: exact, Theorem 7.1, p. 14. The trust atom retains Platt’s two parity branches at conductor at most 400000; the Helfgott Section-4.6 consumer is a derived theorem.

Citation: Timothy S. Trudgian, An improved upper bound for the error in the zero-counting formulae for Dirichlet L-functions and Dedekind zeta-functions, Math. Comp. 84, 1439–1450
Audited version: arXiv:1206.1844v4 for the mapped 0.317/6.401 claim; version of record separately checked and non-identical
Audit status: claim-level primary-source audit with revision distinction
Inspection scope: arXiv v4 Theorem 1 and equation (1.1), including its primitive nonprincipal restriction; the definition of N(T,chi) and Cauchy argument-principle identity in Section 2; comparison with the non-identical version-of-record constants 0.315 and 6.455
Bibliography entry: REFERENCES.md#trudgian-2015
Primary locators: https://arxiv.org/abs/1206.1844v4; https://doi.org/10.1090/S0025-5718-2014-02898-6. Mapped claims:

• reuse:trudgian-rvm-source: exact, arXiv:1206.1844v4, Theorem 1 and equation (1.1), p. 1; multiplicity via Section 2 argument-principle identity, p. 2. The named Lean proposition preserves the primitive, nonprincipal, T >= 1, multiplicity-counted hypotheses and the arXiv-v4 error 0.317 log(qT) + 6.401 exactly. The version of record instead prints 0.315 log(qT) + 6.455; those two envelopes cross, so the published pair is documented but is not used as an interchangeable source for this definition.

• reuse:trudgian-rvm-bridge: derived, arXiv:1206.1844v4, Theorem 1 and equation (1.1), p. 1; multiplicity via Section 2 argument-principle identity, p. 2. The bridge weakens the arXiv-v4 constants on the nonprincipal branch and requires a visibly separate q=1 zeta premise; it does not attribute the principal branch to Trudgian or silently substitute the non-identical version-of-record constants.

Citation: Andrew Fiori, A Note on the Phragmén–Lindelöf Theorem
Audited version: arXiv:2502.13282v3
Audit status: claim-level primary-source audit
Inspection scope: Theorem 1, Corollary 3, Remark 4, Lemma 5, Theorem 7, and Remark 8
Bibliography entry: REFERENCES.md#fiori-2025
Primary locators: https://arxiv.org/abs/2502.13282v3. Mapped claims:

• reuse:fiori-midpoint: adapted, Lemma 5, pp. 3–4. The logarithm branches and multiplier regularity are explicit in Lean.

• reuse:fiori-dyadic: adapted, Theorem 1, pp. 2–4, and Lemma 5. The closed non-strict strip form is derived by the dyadic midpoint argument plus a formal continuity closure.

Citation: H. L. Montgomery and R. C. Vaughan, Hilbert’s inequality, JLMS 8, 73–82
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorems 1–2, Corollary 1, Lemmas 1–5, and equations 1.2–1.7 and 3.6–3.7
Bibliography entry: REFERENCES.md#montgomery-vaughan-hilbert-1974
Primary locators: https://doi.org/10.1112/jlms/s2-8.1.73. Mapped claims:

• reuse:classical-large-sieve: adapted, Theorem 1 and Corollary 1, pp. 73–74. The foundations-only Lean proof follows the Hilbert-inequality route but is not a trust dependency on the paper.

Citation: Wijit Yangjit, On the Montgomery–Vaughan weighted generalization of Hilbert’s inequality
Audited version: arXiv:2203.14950v1
Audit status: claim-level primary-source audit
Inspection scope: Equations 1.2–1.4, Theorems 1.1–1.5, and Lemmas 2.1–2.2
Bibliography entry: REFERENCES.md#yangjit-2022
Primary locators: https://arxiv.org/abs/2203.14950v1. Mapped claims:

• reuse:classical-large-sieve: method, equations 1.2–1.4 and Lemmas 2.1–2.2. This supplies comparison context for weighted Hilbert constants; the Lean theorem is independently proved.

Citation: H. L. Montgomery and R. C. Vaughan, The large sieve, Mathematika 20.2, 119–134
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorem 1 and equations 1.4 and 1.6; Lemma 7 equation 4.3; Lemma 8
Bibliography entry: REFERENCES.md#montgomery-vaughan-large-sieve-1973
Primary locators: https://doi.org/10.1112/S0025579300004708; https://personal.science.psu.edu/rcv4/personal/Publications/large_sieve.pdf. No claim node. All claim mappings for this source are retired from the current trust boundary.

Citation: Olivier Ramaré, Explicit estimates on the summatory functions of the Möbius function with coprimality restrictions, Acta Arith. 165.1, 1–10
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorem 1.1, equation 1.2, and Lemmas 2.1, 2.3–2.5, and 3.1–3.2
Bibliography entry: REFERENCES.md#ramare-coprime-2014
Primary locators: https://doi.org/10.4064/aa165-1-1. Mapped claims:

• reuse:ramare-coprime-liouville: derived, Lemma 2.4, pp. 5–6. The final 0.099 over log estimate is assembled from the native compact sweep and ordinary Lean continuation.

Citation: Olivier Ramaré, Some elementary explicit bounds for two mollifications of the Möbius function, FACM 49.2, 229–240
Audited version: version of record and author offprint
Audit status: background provenance audit
Inspection scope: Lemma 3.7 and its recalled divisor-remainder estimate
Bibliography entry: REFERENCES.md#ramare-mollifications-2013
Primary locators: https://doi.org/10.7169/facm/2013.49.2.3; https://ramare-olivier.github.io/Maths/MuLog-4.pdf. No claim node. Lemma 3.7 concerns a weighted divisor-sum asymptotic and is not an input to the repository’s fourth-root m-star continuation. The earlier source edge was removed after checking the formula against the live Lean declaration.

Citation: Olivier Ramaré, On Šnirel’man’s constant, Annali SNS Pisa 22.4, 645–706
Audited version: version of record scan
Audit status: claim-level primary-source audit
Inspection scope: Lemma 3.4 and equations 3.5–3.9; Lemma 3.5 part 1 and equation 3.13
Bibliography entry: REFERENCES.md#ramare-snirelman-1995
Primary locators: https://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/. Mapped claims:

• reuse:ramare-g-asymptotic: adapted, Lemma 3.4 and equations 3.5–3.9. Lean proves a stronger corrected constant 6.11 and records the under-evaluated printed product.

• reuse:ramare-g-upper: derived, Lemma 3.5 part 1 and equation 3.13. The source’s 1.4709 upper bound is routed through formal and finite components.

Citation: Andrew Granville and Olivier Ramaré, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients, Mathematika 43.1, 73–107
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Lemma 10.2 and its Davenport counting/fractional-part proof
Bibliography entry: REFERENCES.md#granville-ramare-1996
Primary locators: https://doi.org/10.1112/S0025579300011608; https://ramare-olivier.github.io/Maths/granvilleramare.pdf. Mapped claims:

• reuse:granville-ramare: derived, Lemma 10.2. The source is stated for an integer endpoint N >= 1 and integer modulus d. The Lean theorem extends it to real x >= 1 by N = floor(x) and specializes the modulus to a positive natural q.

Citation: Olivier Ramaré and Robert Rumely, Primes in arithmetic progressions, Math. Comp. 65.213, 397–425
Audited version: version of record and author-hosted scan
Audit status: claim-level primary-source audit
Inspection scope: Section 5.2, Theorem 5.2.1, Table 2, and the rigorous fixed-point sieve description, pp. 421–424
Bibliography entry: REFERENCES.md#ramare-rumely-1996
Primary locators: https://doi.org/10.1090/S0025-5718-96-00669-2; https://ramare-olivier.github.io/Maths/rumely.pdf. Mapped claims:

• reuse:rr-2-14: background, Section 5.2, Theorem 5.2.1, and Table 2, pp. 421–424. The live formal proof does not invoke this source: it joins a repository-native 2m–4m psi certificate to Chirre–Helfgott Lemma 9.2 and Corollary 1.3. Table 2 is retained only as historical comparison; its k=1 square-root bound reaches slope 1.0004 only on the upper part of the window.

Citation: Olivier Ramaré and Yannick Saouter, Short effective intervals containing primes, JNT 98.1, 10–33
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Lemma 2, p. 14, including the two-sided ordinate tail with its error term
Bibliography entry: REFERENCES.md#ramare-saouter-2003
Primary locators: https://doi.org/10.1016/S0022-314X(02)00029-X; https://ramare-olivier.github.io/Maths/gap.pdf. Mapped claims:

• reuse:rs03-zero-tail: weakened, Lemma 2, p. 14. The Lean endpoint specializes m=1, replaces ordinates by zero moduli, rounds to 2.96e-12, and reproves the needed Riemann–von Mangoldt input.

Citation: J. Barkley Rosser, Explicit bounds for some functions of prime numbers, AJM 63.1, 211–232
Audited version: version of record
Audit status: background provenance audit
Inspection scope: Theorem 19, p. 223, including |N(T)-F(T)| < 0.137 log T + 0.443 log log T + 1.588 for T >= 2; Lemma 17, p. 225, including the multiplicity-counted reciprocal ordinate sums 0.0463, 0.00167, and 0.0000744
Bibliography entry: REFERENCES.md#rosser-1941
Primary locators: https://doi.org/10.2307/2371291; https://archive.org/details/sim_american-journal-of-mathematics_1941-01_63_1. No claim node. The production proof reaches the relevant prime-function estimates through later Rosser–Schoenfeld results and checked fork theorems, so no claim-level Blueprint edge to Rosser 1941 is asserted. Theorem 19 and Lemma 17 were nevertheless checked in the version-of-record issue scan for historical provenance.

Citation: J. Barkley Rosser and Lowell Schoenfeld, Approximate formulas for some functions of prime numbers, Illinois J. Math. 6.1, 64–94
Audited version: version of record
Audit status: claim-level primary-source audit
Inspection scope: Theorems 4, 8, 12, 13, 15, 19, and 23; equations 3.14, 3.29, 3.35–3.36, 3.41–3.42, 4.6, 4.10, and Lemma 13 equation 8.9
Bibliography entry: REFERENCES.md#rosser-schoenfeld-1962
Primary locators: https://doi.org/10.1215/ijm/1255631807. Mapped claims:

• reuse:rs62-mertens: derived, Theorem 8, equation 3.29; using Theorem 23, equation 4.10, and Lemma 13, equation 8.9. The target concludes the Mertens-product inequality printed as Theorem 8 (3.29); its conditional proof assembles the two explicitly named range inputs (4.10) and (8.9).

• reuse:psi-sharp: source-shaped, Theorem 12, equation 3.35. Theorem 12 supplies the source-shaped comparison. The live Lean proof instead joins a native finite head to the later Chirre–Helfgott continuation; it does not invoke the RS62 analytic range.

• reuse:psi-minus-theta: source-shaped, Theorem 13, equation 3.36. This is a source-shaped comparison for the independently reproved inequality; the Lean continuation keeps its native bounded head and sharp-psi premise explicit.

Citation: J. Barkley Rosser and Lowell Schoenfeld, Sharper bounds for the Chebyshev functions theta and psi, Math. Comp. 29, 243–269
Audited version: version of record
Audit status: background provenance audit
Inspection scope: Theorem 6 equation (5.1) and Corollary 2 equations (5.6)–(5.7); Helfgott equation (2.19) is derived from Corollary 2, while Rosser–Schoenfeld’s own equation (2.19) is unrelated
Bibliography entry: REFERENCES.md#rosser-schoenfeld-1975
Primary locators: https://doi.org/10.1090/S0025-5718-1975-0457373-7. No claim node. The former equation-(5.1) theta route and Corollary-2 finite use were replaced by a weaker Rosser–Schoenfeld 1962 psi route and repository-native heads; the equation-(2.19) label belongs to Helfgott’s derivation, not this paper.

Citation: N. M. Temme, DLMF Chapter 12: Parabolic Cylinder Functions
Audited version: DLMF Version 1.2.7, released 2026-06-15; numbered equations accessed 2026-07-19
Audit status: claim-level primary-source audit
Inspection scope: Equations 12.2.2, 12.2.6, 12.2.8, 12.2.10–12.2.11, 12.2.15–12.2.16, 12.5.1, 12.5.4, 12.5.6, 12.7.1–12.7.2, 12.7.14, and 12.9.1–12.9.3
Bibliography entry: REFERENCES.md#dlmf-chapter-12
Primary locators: https://dlmf.nist.gov/12; https://dlmf.nist.gov/12.2.E2; https://dlmf.nist.gov/12.2.E11; https://dlmf.nist.gov/12.2.E16; https://dlmf.nist.gov/12.5.E1; https://dlmf.nist.gov/12.5.E6; https://dlmf.nist.gov/12.9.E1; https://dlmf.nist.gov/12.9.E2; https://dlmf.nist.gov/12.9.E3. Mapped claims:

• reuse:parabolic-integral: adapted, equation 12.5.1. The repository raw U is defined by the right-hand side for Re(a) > -1/2 and arbitrary complex z; this is not an independent global normalization theorem.

• reuse:parabolic-weber: adapted, equations 12.2.2 and 12.5.1. The integral representation retains arbitrary complex z, while the current differentiated-integral proof of Weber’s equation assumes both Re(a) > -1/2 and Re(z) > 0; no global analytic continuation is claimed.

• reuse:parabolic-mellin: derived, equation 12.5.1. Direct substitution yields Gamma(s) exp(-pi squared delta squared) U(s-1/2,-2 pi i delta).

Citation: F. W. J. Olver, Asymptotics and Special Functions, 1997 reprint of the 1974 edition
Audited version: AKP Classics 1997 reprint; pagination checked against the scanned edition
Audit status: background provenance audit
Inspection scope: Chapter 6, Section 6, equations (6.01) and (6.03)–(6.06), pp. 206–208; Chapter 7, Section 10, Exercise 10.4, p. 259, checked but branch-sensitive and not used as a global identity; Chapter 13, Section 15, Exercise 15.1, p. 516
Bibliography entry: REFERENCES.md#olver-1997
Primary locators: https://www.routledge.com/Asymptotics-and-Special-Functions-1st-Edition/Olver/p/book/9780429064616. No claim node. The checked Chapter 6 material treats large positive order with real scaled argument, not the repository’s former fixed-parameter, large-complex-argument contracts. Those public Blueprint nodes were removed after the contracts were found unsatisfiable; a corrected API must bound the right parameter regime, including the Gamma-weighted product needed by the Mellin application.

Citation: Harold Davenport, Multiplicative Number Theory, 3rd ed., revised by Hugh L. Montgomery, GTM 74
Audited version: Springer third edition, 2000
Audit status: methodology/background audit
Inspection scope: Printed Sections 12–17 and 24; especially Section 12 equations (6)–(8) and (17), Section 13 equations (1)–(5), Sections 15–17, and Section 24 equations (1)–(6)
Bibliography entry: REFERENCES.md#davenport-2000
Primary locators: https://link.springer.com/book/9780387950976. No claim node. The book supplies standard proof architecture for Perron, zeta, and Vaughan Type-I/II modules; no theorem from it is a named final trust atom or a single claim-level Blueprint dependency.

Citation: Henryk Iwaniec and Emmanuel Kowalski, Analytic Number Theory, AMS Colloquium Publications 53
Audited version: AMS 2004 edition
Audit status: methodology/background audit
Inspection scope: Lemma 3.1 and equation 3.9; equations 4.105–4.106 (Mellin transform and inversion, not an L2 isometry); Theorems 5.4, 5.6, 5.8, 5.12, 7.7, and 7.13; Lemma 7.15; Lemmas 13.7–13.8
Bibliography entry: REFERENCES.md#iwaniec-kowalski-2004
Primary locators: https://bookstore.ams.org/coll-53. Mapped claims:

• reuse:classical-large-sieve: method, Theorem 7.7. The Lean result is independently proved through the Montgomery–Vaughan Hilbert inequality.

• reuse:phi-gain-large-sieve: adapted, Lemma 7.15. The formal amplifier makes the phi gain and all hypotheses explicit.

Citation: Hugh L. Montgomery and Robert C. Vaughan, Multiplicative Number Theory I: Classical Theory, CSAM 97
Audited version: Cambridge first edition, first published in print 2006
Audit status: methodology/background audit
Inspection scope: Theorem 2.7; Sections 5.1–5.2; Lemma 6.3, pp. 170–171; Lemma 7.13, p. 221; Section 7.4, pp. 228ff.; Theorem 9.12; Section 10.2; Lemma 12.2, p. 398. Section 7.4 concerns almost-primes, not the large sieve
Bibliography entry: REFERENCES.md#montgomery-vaughan-book-2006
Primary locators: https://doi.org/10.1017/CBO9780511618314. No claim node. No named public-theorem atom is sourced to the book; claim-level large-sieve edges use Iwaniec–Kowalski Sections 7.4–7.5, the original Montgomery–Vaughan papers, or independently proved Lean interfaces.

Citation: E. C. Titchmarsh, revised by D. R. Heath-Brown, The Theory of the Riemann Zeta-Function, 2nd ed.
Audited version: Oxford second edition, 1986
Audit status: methodology/background audit
Inspection scope: Sections 9.3–9.4, especially Theorems 9.3–9.4, for the Riemann–von Mangoldt and Backlund methodology used in the repository’s independently formalized zero-counting chain
Bibliography entry: REFERENCES.md#titchmarsh-1986
Primary locators: https://global.oup.com/academic/product/the-theory-of-the-riemann-zeta-function-9780198533696. Mapped claims:

• reuse:backlund-f3: method, Sections 9.3–9.4, Theorems 9.3–9.4. The finite interval certificate is repository-owned and proved; the book supplies historical analytic context. Its qualitative O(log T) remainder alone does not certify N(3)=0.