certivl

Exact rational and certified interval arithmetic. Every quantity is a Fraction or an Ivl — a closed interval with exact rational endpoints guaranteed to contain the true value — and every operation rounds outward, so containment survives composition.

That is the whole point: if x.hi < 0 then the true value is negative. Not probably, not to within tolerance. A computed inequality becomes a proof.

pip install certivl

from certivl import Ivl, pi_ivl, sqrt_ivl

p = pi_ivl()
print(float(p.hi - p.lo))          # 2e-80

x = Ivl(3, 3) * sqrt_ivl(2) - p    # 3*sqrt(2) - pi
assert x.lo > Ivl(11, 10).lo       # proved > 1.1, not estimated

What is in it

Ivl with the arithmetic operators, and validated enclosures for sqrt, sin, cos, tan, sec, asin, atan, pi, sqrt2, sqrt3, deg, abs, integer isqrt, plus isolate_root for certified root bracketing of an integer polynomial by bisection with exact sign evaluation.

The algebraic half runs on the standard library alone — Ivl arithmetic, sqrt, isqrt, sqrt2, sqrt3, abs, isolate_root. The transcendental enclosures — pi, sin, cos, tan, sec, asin, atan, deg — are built from mpmath's validated interval type, widened outward, so mpmath is a dependency rather than an extra.

Why not mpmath, Arb, or python-flint

Those are faster and more general, and if you want validated numerics at scale you should use them. This exists for a narrower job: plane geometry where the answer has to be a proof and the constants are algebraic. Exact Fraction endpoints throughout, no binary float anywhere on the path, and denominators sized so the final interval widths are irrelevant to the conclusion rather than tuned to it.

Where it came from

This is the kernel underneath four deposited papers on certified computation for classical plane-covering problems — the Lebesgue universal covering ladder, opaque sets for the unit disc, and Fejes Tóth's point-goalie problem. It certified Pál, Sprague and Hansen's published areas to the digits their authors quoted, and adjudicated a disagreement between a published table and its author's own write-up.

The bug that explains the design

An earlier version converted mpf values by re-creating them in the ambient mpmath context before reading their tuple. mp.prec in a fresh process is 53, so the first conversions of a run were silently rounded to double precision — a one-sided error near 1e-17, inside intervals padded to 1e-80.

Nothing caught it for weeks. It surfaced through a cross-check between two independently computed results that should have summed to zero and instead missed by 8.1e-19 — a discrepancy only visible because everything around it was exact. The conversion now reads the raw (sign, man, exp, bc) tuple, which cannot round.

That is the argument for exact endpoints in one paragraph: a rounding error inside a tolerance is invisible, and a rounding error inside a proof is fatal.

Tests

python tests/test_exact.py

Constants are checked against published decimal expansions quoted from elsewhere, never generated by this code — a kernel checked against itself is checked against nothing. The suite finishes by confirming a value known to lie outside its interval is rejected, because a test that has never failed is not evidence.

Note what is being tested: containment, not accuracy. A wide interval is useless and honest; an interval that excludes the true value is a broken proof. Ivl(-2, 3) ** 2 returns [-6, 9] rather than [0, 9] — loose, and correct.

Licence

MIT.