9.5 Worked audit chain: the Chebyshev \(\psi \) sweep

One N1 family illustrates the separation. The source theorem checkAll_1e7_sharp asks Lean to establish the closed equation

The exact manifest exposes both that proposition and the generated auxiliary axiom asserting that its Decidable.decide is true. The ordinary theorem psi_le_slope_mul_of_checkAll proves the checker’s semantic meaning: throughout the finite range it gives the real inequality \(\psi (x)\le 1.03883x\). The ordinary continuation theorem psi_le_sharp_of_finite_and_cor13 joins that finite input to the separately documented Chirre–Helfgott tail; the resulting reusable claim is node reuse:psi-sharp.

The generated Chebyshev family card supplies the exact manifest-family digest, source range, equation-ledger link, and fail-closed replay command. Its N1 label records a complete independent replay of all three production predicates. The checker-soundness and analytic continuation are Lean theorems, but the displayed finite equation is still native-trusted: the Python/GMP run corroborates rather than replaces the generated Lean axiom. Every family card below follows this same audit schema.