2 Witnesses and the conditional theorem
Trust tier: BT-U. For every natural number \(n\), a value of ‘PrimeTripleFor n‘ exists if and only if \(n\) is a sum of three primes.
Unpack the three stored primes and their sum equation in one direction; package witnesses for ‘IsThreePrimeSum‘ in the other.
Trust tier: BT-U. The finite ternary representation count \(r_3(n)\) is positive exactly when \(n\) is a sum of three primes.
Rewrite cardinal positivity as nonemptiness of the finite set of prime triples, then unpack or package the three primes and their sum.
Trust tier: DEF. Definition of the input proposition asserting that every odd \(n\) above the Helfgott–Platt threshold satisfies the signed smoothed major/minor/tail endpoint. This node defines a contract; it does not supply a proof of the contract.
Trust tier: DEF. Definition of the input proposition asserting that every odd \(n\) from \(7\) through the Helfgott–Platt threshold has an explicit three-prime witness. This node defines a contract; it does not prove it.
Trust tier: BT-C. The large-odd analytic contract and the finite prime-triple contract imply ternary Goldbach for every odd \(n\ge 7\).
Split on whether \(n\) is at most the published finite threshold. Use the finite witness below it and extract three primes from the signed smoothed endpoint above it.