Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Primary-source audit 11.9Helfgott major arcs

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.

LaTeX

Primary-source audit 11.10Helfgott ternary Goldbach monograph

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.

LaTeX