Blueprint for the Ternary Goldbach Formalization

6 Tail removal and large-odd closure

The major/minor coefficient gap is

\[ \frac{1.058259-1.048}{49}X^2 = \frac{0.010259}{49}X^2. \]

The sharp mixed prime-power tail is at most twenty times the explicit square-root-log envelope. The threshold computation proves this is strictly smaller than the displayed gap.

Theorem 6.1 Sharp mixed prime-power tail

Trust tier: BT-U. The contribution in which at least one von-Mangoldt argument is a proper prime power is bounded by the explicit sharp tail envelope.

Source: helfgott-ternary-2015, equations 14.50–14.51, pp. 275–276 [adapted]

Proof

Union-bound the three bad coordinates, use the proved prime-power counting bound, and retain the smoothing norms in the resulting square-root-log envelope.

Theorem 6.2 Major-minus-minor gap dominates the tail

Trust tier: BT-U. Above the finite threshold, the coefficient gap \((1.058259-1.048)X^2/49\) strictly dominates twenty times the sharp square-root-log prime-power tail.

Proof

Reduce monotonicity to the published threshold, enclose the remaining logarithmic and power terms, and verify the endpoint inequality with exact certificates.

Trust tier: EF-C. An odd target above the finite threshold satisfying the uniform (13.17) supremum satisfies the signed smoothed analytic endpoint.

Proof

Use (14.27) for the major lower bound, (14.49) for the minor upper bound, the sharp prime-power estimate for \(T\), and the numerical gap theorem for \(T{\lt}c_1-c_2\).

Trust tier: HEAVY+EF+PF-C. The explicit low, medium, and compact small-\(q\) inputs imply the exact signed endpoint for every odd target above the finite threshold.

Proof

Build the (13.14), (13.15), and (13.16) cases, deduce the (13.17) supremum, and invoke the endpoint-from-supremum theorem.

Trust tier: HEAVY+EF+PF-U. Every odd target above the Helfgott–Platt threshold satisfies the signed smoothed analytic endpoint.

Source: helfgott-ternary-2015, Chapter 14, pp. 260–276 [adapted]

Proof

Supply the regional endpoint theorem with the proved low and medium fixed-prefix caps and the proved compact small-\(q\) crossover aggregation.