Ball arithmetic

Unified evaluation (experimental)

alkahest.experimental.evaluate provides one result contract for exact rational, f64, and rigorous interval evaluation. It returns an EvaluationResult; mathematically unsupported inputs return status == "unsupported" and a stable E-EVAL-* reason code rather than raising. Invalid API input, such as an invalid mode or zero precision, still raises ValueError.

from fractions import Fraction
import alkahest as ak
from alkahest.experimental import evaluate

p = ak.ExprPool()
x = p.symbol("x")
result = evaluate(x + p.rational(1, 3), {x: Fraction(1, 6)})
assert result.value == Fraction(1, 2)
assert result.backend == "exact_rational"

Use mode="f64" for ordinary floating-point evaluation and mode="interval" with ArbBall bindings for an enclosure. In interval mode, result.value and result.enclosure are the same ArbBall; its lo and hi bound the true result. mode="auto" selects intervals for ArbBall bindings (or an explicit precision), exact rationals when possible, and otherwise falls back to f64.

Ball arithmetic provides rigorous enclosures: every operation produces an interval guaranteed to contain the true result. Alkahest uses FLINT’s Arb library as the backend.

ArbBall

An ArbBall represents the real interval [midpoint ± radius]:

from alkahest import ArbBall

a = ArbBall(2.0, 0.5)    # [1.5, 2.5]
b = ArbBall(3.0, 0.0)    # exactly 3.0

print(a.mid)   # 2.0
print(a.rad)   # 0.5
print(a.lo)    # 1.5
print(a.hi)    # 2.5

An ArbBall can also carry a precision (in bits) for the midpoint:

a = ArbBall(2.0, 1e-30, prec=128)  # 128-bit midpoint

Ball arithmetic operations

All arithmetic on ArbBall values produces a guaranteed enclosure. The radius grows to account for rounding and operation error:

a = ArbBall(2.0, 0.1)
b = ArbBall(3.0, 0.1)

print(a + b)    # [4.8, 5.2]  — radius grows by sum of input radii
print(a * b)    # guaranteed enclosure of [1.9, 2.1] * [2.9, 3.1]
print(a ** 2)   # [3.24, 4.41]  (squares the interval)

interval_eval

interval_eval evaluates a symbolic expression with ArbBall inputs:

from alkahest import ExprPool, ArbBall, interval_eval, sin, exp

pool = ExprPool()
x = pool.symbol("x")

# sin(1 ± 1e-10) — guaranteed enclosure
result = interval_eval(sin(x), {x: ArbBall(1.0, 1e-10)})
print(result.lo, result.hi)

# Multivariate
y = pool.symbol("y")
expr = sin(x) * exp(y)
result = interval_eval(expr, {
    x: ArbBall(1.0, 0.01),
    y: ArbBall(0.0, 0.01),
})

interval_eval guarantees that the output ball contains the true value for any input in the given input balls, accounting for all rounding in the intermediate computation.

The indeterminate ball

Some expressions have no finite enclosure over the ball you asked about — 1/x where the ball straddles 0, or an intermediate result whose enclosure lost so much to the dependency problem that a later reciprocal became unbounded. The answer in that case is [-inf, inf]: the whole real line, which is true and carries no information.

r = interval_eval(pool.integer(1) / x, {x: ArbBall(0.0, 1.0)})
r.lo, r.hi        # (-inf, inf)
r.contains(5.0)   # True — it contains everything

Two consequences worth knowing:

• Check lo/hi for finiteness before believing a bound. An infinite endpoint is the API saying “I could not bound this”, and it is the only way it says so — interval_eval does not raise for it.
• contains is True for an indeterminate ball, never False. This is the direction that matters: contains is what a caller uses to cross-check a symbolic identity, and a False there is read as a refutation. “No information” must never be reported as “that value is outside the enclosure”, so no ball ever has NaN endpoints — a NaN produced by an indeterminate operand (0 · ∞ in the radius of a product, ∞ − ∞ in the midpoint of a sum) widens to the whole line instead of escaping.

Boxes containing a singularity

The guarantee is about the whole input box, not only its endpoints, so a box a function is unbounded on cannot get a finite answer. Such a box widens to [-inf, inf] — an honest, if useless, enclosure — rather than reporting the hull of the values at the two ends:

import math
# [0.1, 0.1 + pi] contains pi/2, where tan has a pole
b = ArbBall((0.1 + 0.1 + math.pi) / 2, math.pi / 2)
interval_eval(tan(x), {x: b})                    # ArbBall(0.000000 ± inf)

# x**-2 over a box containing 0
interval_eval(x**-2.0, {x: ArbBall(1.0, 2.0)})   # ArbBall(0.000000 ± inf)

A box on which the function is bounded but not monotone still gets a finite enclosure — x**2.0 over [-1, 3] covers x = 0, and bessel_j0 over [-1, 1] covers the peak at x = 0 — it is only the unbounded case that degenerates.

AcbBall

Complex ball arithmetic for expressions over ℂ:

from alkahest import AcbBall

z = AcbBall(1.0, 0.0, 1.0, 0.0)  # 1 + i, exact

Use cases

Certified numerical evaluation. Compute a value and prove it lies within a tight bound without symbolic proof:

# Prove sin(1) ∈ [0.841, 0.842]
r = interval_eval(sin(x), {x: ArbBall(1.0, 0.0)})
assert r.lo > 0.841 and r.hi < 0.842

Numerical verification of symbolic results. After deriving a symbolic simplification, verify it numerically with rigorous bounds:

# Verify sin²(x) + cos²(x) = 1 at x = 1
lhs = sin(x)**pool.integer(2) + cos(x)**pool.integer(2)
r = interval_eval(lhs, {x: ArbBall(1.0, 0.0)})
assert 1.0 in r  # ball contains 1

Sensitivity analysis. Pass an input ball representing parameter uncertainty and observe how the output uncertainty grows:

# x = 1 ± 0.1 (10% uncertainty)
r = interval_eval(x**pool.integer(3), {x: ArbBall(1.0, 0.1)})
print(r)  # output uncertainty

Relationship to Lean certificates

Ball arithmetic and Lean certificate export are complementary:

• Ball arithmetic gives numerical certainty within floating-point computation.
• Lean certificates give symbolic/logical certainty for the rewrite steps applied.

Combining them: certify(interval(differentiate(f))) gives a derivative, evaluated with rigorous interval bounds, with a machine-checkable proof of the symbolic differentiation step.