Blueprint for the Ternary Goldbach Formalization

4 Major arcs

The live Chapter-14 major route lower-bounds the mixed major contribution by

\[ \frac{1.058259}{49}X^2. \]

It combines the primitive-character error envelope (14.2), the two sides of the (14.7) \(L^2\) estimate, Proposition 10.4.1, the smoothing main-term lower bound (14.10)–(14.14), and the odd singular-series lower bound (14.9).

Theorem 4.1 Primitive-character error envelope (14.2)

Trust tier: EF-U. Above the Helfgott–Platt threshold, the primitive-character error term satisfies the explicit envelope used in equation (14.2).

Source: helfgott-ternary-2015, equation 14.2, p. 260 [adapted]

Proof

Specialize the proved explicit-formula and zero-sum bounds at the Chapter-14 scale. The external zero computations and finite interval certificates are exposed separately in the trust-boundary appendix.

Theorem 4.2 Major-arc L2 upper estimate (14.7)

Trust tier: EF-U. The quadratic major-arc error has the explicit upper bound required by equation (14.7) at the honest threshold.

Source: helfgott-ternary-2015, equation 14.7, p. 261 [adapted]

Proof

Insert the primitive error envelope into the character and denominator decomposition, then sum the certified per-modulus bounds.

Theorem 4.3 Major-arc L2 lower estimate (14.7)

Trust tier: EF-U. The main major-arc block has the complementary explicit lower estimate used in equation (14.7).

Source: helfgott-ternary-2015, equation 14.7, p. 261 [adapted]

Proof

Combine the per-denominator lower blocks, the disjoint-arc integral splitting, and the certified odd Mertens and smoothing-mass bounds.

Theorem 4.4 Major-arc error envelope

Trust tier: EF-U. The \(L^2\) estimates imply the explicit Proposition 10.4.1 error budget for the mixed major integral.

Source: helfgott-ternary-2015, Proposition 10.4.1, pp. 213–215 [adapted]

Proof

Apply Cauchy–Schwarz to the main/error decomposition and substitute the upper and lower \(L^2\) envelopes.

Theorem 4.5 Positive main-term constant (14.10–14.14)

Trust tier: BT-U. The smoothing main term in equations (14.10)–(14.14) has the required explicit positive lower bound.

Source: helfgott-ternary-2015, equations 14.10–14.14, pp. 261–263 [derived]

Proof

Evaluate the windowed smoothing integral and certify the remaining compact numerical inequalities by exact rational enclosures.

Theorem 4.6 Odd singular-series lower bound (14.9)

Trust tier: EF-U. For odd \(n\), the singular-series factor has the explicit lower bound used in equation (14.9).

Source: helfgott-ternary-2015, equations 14.8–14.9, p. 261 [adapted]

Proof

Isolate the factors at \(2\) and \(3\), check the finite prime deficit product, and bound the remaining Euler tail.

Theorem 4.7 Positive mixed major contribution (14.27)

Trust tier: EF-U. For odd \(n\) above the finite threshold, the real part of the mixed major integral is at least \((1.058259/49)X^2\).

Source: helfgott-ternary-2015, equation 14.27, p. 267 [weakened]

Proof

Combine the (14.7) error envelope, Proposition 10.4.1, the positive main-term bound from (14.10)–(14.14), and the odd singular-series lower bound (14.9).