12 Source alignment and repairs

The formal proof follows Helfgott’s major-arc paper, minor-arc paper, and ternary-Goldbach monograph [ 9 , 8 , 10 ] , together with the finite verification of Helfgott and Platt [ 12 ] . It also uses explicit estimates such as those of Rosser–Schoenfeld [ 33 ] and named zero computations such as Platt–Trudgian [ 7 ] . The newer explicit prime-sum inputs are audited against Chirre–Helfgott [ 4 ] ; the Dirichlet-zero inputs distinguish Platt’s stronger primitive-character verification [ 20 ] from Trudgian’s multiplicity-counted zero-counting estimate [ 21 ] . The formal Trudgian contract is pinned to arXiv:1206.1844v4, whose constants are \(0.317\) and \(6.401\); the version of record has the non-identical pair \(0.315\) and \(6.455\).

The repository contains corrected and sometimes deliberately weakened consumer bounds. A weaker consumer is derived in Lean from the stronger source-shaped statement whenever possible. Repository-specific meshes, fixed-point scales, and repair allowances are identified as such rather than presented as verbatim paper equations. See the paper-error ledger, Helfgott errata notes, and the individual comparison cards for exact mappings.