Certificate API Reference

This page maps the detailed certificate APIs. For a conceptual starting point, use 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.Chebyshev.Psi
import LeanCert.Engine.Chebyshev.Theta

or through the aggregate API:

import LeanCert

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.