Blueprint for the Ternary Goldbach Formalization

7 Production providers and final threshold split

Proof

Apply the closed large-odd endpoint pointwise. The explicit trust-family edges are an audit summary of the fresh transitive axiom closure; exact atoms and equations are linked in the appendices.

Theorem 7.2 Production finite provider

Trust tier: EF-U. Helfgott–Platt Theorem 4.1 supplies ‘FiniteOddGoldbachInput‘.

Source: helfgott-platt-2013, Theorem 4.1 [derived]

Proof

The source-shaped external theorem already returns the exact ‘PrimeTripleFor‘ witness required by the finite contract.

Theorem 7.3 Ternary Goldbach

Trust tier: HEAVY+EF+PF-U. Every odd natural number \(n\ge 7\) is a sum of three primes.

Proof

Instantiate the base-trio conditional threshold split with the production large-odd and finite providers.

The finite provider is precisely Helfgott–Platt Theorem 4.1. The large provider is the closed major/minor/tail construction above. The final proof term merely supplies those providers to the conditional threshold split.