Example: a proof-carrying PDE residual
This is the capability nothing else in the ML toolchain offers: take a trained surrogate and produce a certificate that bounds its PDE residual over an entire input box — not just at sampled points.
Step 1 — enclose the residual over a box
from omnibias.core.verified import TaylorModelMV
from omnibias.verify import enclose_pde_residual
# Propagate a Taylor model of the residual over a box of inputs.
enclosure = enclose_pde_residual(
field=trained_field,
equation="heat",
box={"x": (0.2, 0.4), "t": (0.0, 0.1)},
order=4,
)
print(enclosure.bound) # |u_t - κ·u_xx| ≤ this, everywhere in the box
Step 2 — seal a certificate
from omnibias.core.proof.certificate import make_certificate, verify_certificate_digest
cert = make_certificate(enclosure, claim="residual_bounded", epsilon=1e-3)
assert verify_certificate_digest(cert) # tamper-evident hash
cert.save("heat_residual.cert.json")
Step 3 — kernel-check the obligation (optional)
from omnibias.core.proof.lean_check import check_certificate
verdict = check_certificate(cert)
print(verdict.theorem_prover_verified) # True only on a genuine Lean pass
What this proves - and what it doesn't
The certificate bounds the residual of this trained surrogate over the box, to outward-rounded floating-point rigor. It does not prove existence, uniqueness, or regularity of the true PDE solution, and it does not certify points outside the box. This is proof-preparation infrastructure — read Exactness & scope before quoting a result.