Certificate API Reference
This page is a legacy API map for existing certificate pages. It is not the conceptual starting point. Start with Proof Templates or Domain Libraries unless you already know the API family name.
LeanCert certificate APIs share the same basic pattern:
computable certificate data
+ a boolean or exact checker
+ a Golden Theorem
= a semantic theorem over real numbers
Use this page when you already know the family name and want the detailed API reference.
Families
| Certificate family | Use when you need |
|---|---|
| Chebyshev | finite-range bounds for the Chebyshev functions ψ and θ |
| ANT finite bridges | step sums, Abel transforms, Euler products, log products, Dirichlet truncations, prime-power extensionality, and explicit-PNT compiler schemas |
| ANT asymptotic envelopes | main-term plus error-term certificates for summatory functions, pointwise estimates, dyadic slab inequalities, and transforms |
| QProduct | exact finite q-product integrals and prime-limit sandwich certificates |
| ConstantFactory | exact and interval observer-generated q-product constants from perturbation sums and reusable moment kernels |
| Contour Shift | finite rectangle identities, horizontal-side vanishing, vertical-line limits, and residue-sum shift identities |
Imports
Most certificate families can be imported directly:
import LeanCert.ANT
import LeanCert.ANT.Asymp
import LeanCert.QProduct
import LeanCert.ConstantFactory
import LeanCert.ConstantFactory.IntervalBank
import LeanCert.Analysis.ContourShift
import LeanCert.Engine.ChebyshevPsi
import LeanCert.Engine.ChebyshevTheta
or through the aggregate API:
Choosing A Family
Use finite ANT certificates when your theorem is an exact finite statement: finite sums, products, truncations, and Abel transforms over explicit endpoints.
Use asymptotic envelope certificates when the theorem is naturally stated as a summatory main term plus an error term from some cutoff onward.
Use Chebyshev certificates for specialized ψ and θ finite-range bounds.
These can feed into ANT and asymptotic envelope arguments.
Use QProduct certificates for exact product-integral identities and finite prime-limit sandwich arguments.
Use ConstantFactory certificates when a q-product constant is best proved by holding a base kernel bank fixed and verifying finite observer perturbations around it.
Use contour-shift certificates when the analytic work has been decomposed into finite rectangle identities, horizontal decay, vertical-line convergence, and a stable finite residue sum. The current API centralizes the orientation and limit algebra; residue-theorem constructors can be layered on top.