Skip to main content

Provenance & certificates

A number is only as trustworthy as its provenance. omnibias can attach a certificate to an enclosed quantity: a canonical, hash-sealed JSON record of what was bounded, how tightly, and whether a theorem prover checked it.

Certificate format v1​

The format (omnibias.core.proof.certificate) serializes Interval and TaylorModel enclosures into canonical JSON and seals it with a digest.

{
  "certificate_schema_version": "1",
  "claim": "spectral_gap_positive",
  "enclosure": { "type": "Interval", "lo": "0.731...", "hi": "0.734..." },
  "method": "lehmann-maehly-goerisch",
  "digest": "sha256:…",
  "theorem_prover_verified": false
}

Two independent guarantees​

  1. Tamper-evidence (always): verify_certificate_digest recomputes the hash. If a single field changed, verification fails. This protects the record.
  2. Theorem-prover verification (when earned): theorem_prover_verified is set only by a genuine Lean kernel pass on the extracted obligation. The certificate cannot forge it; asserting the claim without a pass blocks the verdict.
The flag is earned, never asserted

theorem_prover_verified = true means a Mathlib-free Lean 4 kernel checked the finite, rational obligation. With no Lean toolchain present, the bridge degrades gracefully and the flag stays false. A false flag is honest, not a failure.

What goes into provenance​

  • the claim (what is being bounded and its sign/threshold),
  • the enclosure (interval or Taylor model, outward-rounded),
  • the method that produced it,
  • the schema version and digest,
  • the verification status.

Using it in practice​

from omnibias.core.proof.certificate import (
    make_certificate, verify_certificate_digest,
)

cert = make_certificate(enclosure, claim="residual_bounded", epsilon=1e-3)
cert.save("artifact.cert.json")

# Anyone, later:
assert verify_certificate_digest(cert)     # the record is intact

See also​

Last updated on