Provenance and certificates

A certificate records a supported claim and its evidence. Its meaning comes from the schema and checker for that claim, not from a filename, digest, or self-reported flag.

Keep three checks separate

Check	What it establishes	What it does not establish
Payload digest	The payload matches the recorded digest	The mathematical statement is true
Numerical replay	A supported replay procedure reproduces the claim	An unrestricted theorem beyond the replay contract
Formal check	The emitted supported obligation passed its check	Every assumption in the surrounding application

The public APIs live in certificate, replay, and lean_check. Use their actual schema and return types. The earlier illustrative make_certificate(...).save(...) workflow is not a current supported API.

Record enough to reproduce the result

Preserve the source revision, distribution versions, input representation, domain, bounds, arithmetic assumptions, method settings, and full checker result. If the formal toolchain is unavailable or the obligation unsupported, report that outcome directly. A Boolean field supplied inside an untrusted payload is not independently earned verification.

Report the bound

For an enclosure, report both endpoints and the domain on which they apply. Do not replace the interval with its midpoint while retaining the enclosure claim. For a relaxation, report its relationship to the original problem and any certified gap. For a sampled test, report the sample set and tolerance rather than calling it a global guarantee.

Read verified arithmetic, the formal bridge, and reproducibility together when producing an evidence artifact.