Metadata-Version: 2.4
Name: certivl
Version: 0.1.0
Summary: Exact rational and certified interval arithmetic: enclosures that turn a computed inequality into a proof.
Author-email: Vincent Gonzalez <vincegonzalez@me.com>
License: MIT
Project-URL: Homepage, https://github.com/vince-gonzalez/certivl
Project-URL: Source, https://github.com/vince-gonzalez/certivl
Keywords: interval arithmetic,certified computation,computer-assisted proof,exact arithmetic,rational arithmetic,validated numerics,rigorous numerics
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: mpmath>=1.3
Dynamic: license-file

# 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
```

```python
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.
