1 Scope and trust semantics

This Blueprint is a human-scale map from the informal argument to the live Lean declarations. It follows the public production theorem, not the faster axiomatized development profile. The authoritative trust boundary is always a fresh #print axioms Math.Problems.TernaryGoldbach.ternary_goldbach.

Formal-to-formal arrows are inferred by LeanArchitect from the Lean terms. The production-provider nodes also have curated arrows to the native-family and citation appendices. Those appendix arrows summarize the audited transitive trust boundary; they are not kernel proofs of the prose or of the completeness of an informal explanation.

LeanArchitect writes \leanok whenever it finds no sorryAx. That marker does not distinguish an ordinary kernel proof from a theorem using native evaluation or a named external axiom; it can also appear on a definition whose proposition has not been proved. The badge printed in each node supplies that distinction:

• BT-U: unconditional modulo propext, Classical.choice, and Quot.sound;

• BT-C: a base-trio implication whose inputs remain visible;

• DEF: a definition or contract, not a proof that the contract is inhabited;

• NATIVE: compiler/native evaluation of a closed finite predicate;

• EF: a named external finite computation with a comparison card;

• EA: a named external analytic source statement; and

• a plus sign records combined boundaries.

The public proof uses two clean mathematical contracts. The finite contract provides prime triples up to the published cutoff, and the large contract provides an analytic endpoint above it. Their derivation is separated from the base-trio threshold split.