Blueprint for the Ternary Goldbach Formalization

9.4 Mitigations in this repository

The current controls reduce those risks without relabeling the result as kernel-only.

  • The toolchain and all Lake dependencies are pinned. Release review uses a clean environment and a fresh source build of the live consumer.

  • A fresh #print axioms is compared with a separate environment traversal. The inspector also reads each dependency’s ConstantInfo, validates the full closed Decidable.decide P = true shape, and rejects unknown source wrappers, sorryAx, or deprecated native-trust primitives.

  • The exact manifest stores every expanded axiom type, the separately expanded proposition \(P\), declaration range, module, type and payload digests, family membership, and source witness. Family-member digests make additions or substitutions fail closed. These checks corroborate provenance; they are not a cryptographic attestation of the compiler run.

  • The external replay facade independently pins all proposition and payload transport fields and hashes each checker’s transitive repository-local Lean source closure, following ordinary, public, and private imports and including the Lean/Lake dependency files. A checker body or dependency change therefore fails before replay. The fresh inspector remains stronger because it reconstructs the manifest from the live Lean environment.

  • The equation ledger states the finite equation, arithmetic model, range, paper comparison, and known replay limitation. Ordinary Lean keeps the checker-soundness bridge separate, and derives weakened consumer statements from stronger source-shaped statements.

  • The computations use explicit integer, rational, fixed-point, or outward interval arithmetic. This removes an undocumented floating-point tolerance from the propositions, but it does not remove the native compiler from the trusted base.

  • The independent Python/GMP facade is fail-closed. Complete replay exits zero; partial or absent exact replay exits nonzero unless a reviewer explicitly asks for an incomplete audit. The generated cards report the exact numerator as well as the N1/N2/N3 label.

  • The strict completion gate scripts/tg_native_trust_surface.py –require-zero-native fails while any generated native atom remains. This is the criterion for a future claim that the native trust boundary has been eliminated.