The certified register

The rigorous register (omnibias.core.verified) computes enclosures that provably contain the true value, instead of unverified floats. It is pure Python and imports no backend.

The arithmetic

Tool	What it provides
Interval	outward-rounded interval arithmetic
affine	affine (zonotope) arithmetic with dependency cancellation
TaylorModel / TaylorModelMV	a polynomial plus a rigorous remainder interval
sequence_space	geometric-decay tail bounds for series
kantorovich	radii-polynomial existence proofs
lohner	QR-Lohner / Taylor-model validated ODE flow
eig_operator	Lehmann–Maehly–Goerisch eigenvalue lower bounds

from omnibias.core.verified import Interval

x = Interval(0.5, 0.5)
y = x.sin()          # provably contains sin(0.5)
print(y.lo, y.hi)

The validation discipline

Every enclosure is tested two ways

An enclosure must contain both a dense deterministic grid and a random sample of true values. An interval that is merely "usually right" is a bug — the test suite rejects it.

Affine arithmetic cancels dependency

Naive interval arithmetic over-estimates when a variable appears multiple times (the "dependency problem"). Affine arithmetic tracks shared noise symbols so correlated terms cancel:

Certificate format v1

Results are sealed into a canonical, hash-stamped JSON certificate (omnibias.core.proof.certificate):

• It is tamper-evident: an edited payload fails verify_certificate_digest.
• A Verdict carries certificate_schema_version and the kernel-earned theorem_prover_verified flag.
• An independent replay twin regenerates the result with a different algorithm, so a forged number fails replay.

from omnibias.core.proof.certificate import verify_certificate_digest
assert verify_certificate_digest(cert)   # tamper check

What you can certify

• Robustness / Lipschitz / monotonicity / reachable-set certificates for trained networks (see verify).
• Residual enclosures for a neural PDE surrogate (see Proof-carrying PDE).
• Periodic-orbit existence and certified Lyapunov bounds for dynamical systems (see dynamics).

The next step: a formal gate

A certificate's finite, rational obligation can be re-checked by a Lean 4 kernel. That is the formal loop.

Enclosures are guarantees, not point values

A certified result is an interval [lo, hi] that contains the truth — it is a different and often stronger statement than a single float. Quote the interval, not a midpoint, when the guarantee matters.