Proof Templates
Proof templates are reusable certificate strategies. Use them when your theorem is not just one interval inequality, but has a repeatable proof shape: generated rows, main/error envelopes, perturbations of a base object, product-integral identities, or contour-shift bookkeeping.
A proof template usually has this form:
structured certificate data
+ a checker or reusable soundness theorem
+ project-specific side conditions
= semantic theorem in Lean
Unlike direct tactics, proof templates do not always close a theorem from a raw expression. Some have executable checkers; others organize proof obligations that must be supplied by project-specific mathematics.
| Template | Use when you have... |
|---|---|
| Checker-to-theorem | a boolean checker and a theorem explaining what success means |
| Table certificates | many generated finite rows with one row checker |
| Asymptotic envelopes | a summatory function, main term, and nonnegative error term |
| Pointwise envelopes | a real-variable approximation and an error radius |
| ConstantFactory | a base object with reusable moments and finite perturbations |
| QProduct finite integrals | exact finite product-integral identities |
| Contour-shift certificates | rectangle identities, horizontal vanishing, vertical limits, and residue data |
| Directed-limit certificates | a limit object enclosed by computable truncations with a computable tail majorant |
| Wall quotients | a 0/0 removable singularity whose enclosure must come from derivative data |