Arb-backed transcendentals for `IEEE32Exec.Interval32` #

NN/Floats/Interval/IEEEExec32.lean provides an executable endpoint-interval type IEEE32Exec.Interval32 with outward-rounded endpoint arithmetic for add/sub/mul:

endpoints live on the IEEE-754 binary32 grid (IEEE32Exec),
addDown/addUp/mulDown/mulUp are implemented via exact-dyadic arithmetic + directed rounding.

For transcendentals (exp/log/tanh/sqrt/...) the situation is different:

IEEE-754 does not specify correctly-rounded transcendentals (libm is out of scope),
NN/Floats/IEEEExec/Exec32.lean contains deterministic transcendental approximations, but they are not proved outward-rounded w.r.t. real semantics.

This file implements a pragmatic “sound route” for interval endpoints of transcendentals:

Call the Arb oracle (NN/Floats/Arb) to obtain a rigorous real enclosure [L,U] ⊇ f([a,b]).
Convert L,U : ℚ directly to float32 endpoints with the proved rational rounders:
- lower endpoint: roundRatDown,
- upper endpoint: roundRatUp.

Trust boundary:

The enclosure [L,U] is an oracle claim from Arb/python-flint; Arb is the external trusted producer for that real enclosure.
The exact-rational-to-float32 step is in Lean and its enclosure inequalities are proved in NN/Floats/IEEEExec/DirectedRoundingSoundness/Division.lean.

The result is useful when you want executable float32 endpoints and a clearly delineated source of transcendental soundness (Arb).

source

def Rat.toArbString (q : ℚ) :

String

Render a rational in a format that Arb's parser accepts (e.g. -3/2, 5).

Instances For

Proved outward rounding from `ℚ` to `IEEE32Exec` #

source

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatQDown (q : ℚ) :

IEEE32Exec

Proved outward rounding down of an exact rational to a binary32 endpoint.

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatQUp (q : ℚ) :

IEEE32Exec

Proved outward rounding up of an exact rational to a binary32 endpoint.

Instances For

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundRatQDown_le (q : ℚ) :

(roundRatQDown q).toEReal ≤ ↑↑q

The lower rational endpoint conversion is an EReal lower bound.

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundRatQUp_ge (q : ℚ) :

↑↑q ≤ (roundRatQUp q).toEReal

The upper rational endpoint conversion is an EReal upper bound.

Arb-backed interval endpoints for transcendentals #

source

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.ensureFinite (x : IEEE32Exec) (label : String) :

IO ℚ

Decode a float endpoint as an exact rational, failing if the value is NaN/Inf.

This is used to feed exact endpoint strings into the Arb oracle.

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.arbBounds (func : String) (X : Interval32) (precBits digits : ℕ := 200) :

IO (ℚ × ℚ)

Call Arb on the real interval [X.lo, X.hi] (interpreted exactly as rationals) and return the oracle-provided rational enclosure bounds (L,U).

This is the only step that crosses the trust boundary.

Instances For

source

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.arbUnary (func : String) (X : Interval32) (precBits digits : ℕ := 200) :

IO Interval32

Compute an IEEE32Exec.Interval32 enclosure for a transcendental unary func by:

getting a real enclosure [L,U] from Arb,
rounding endpoints outward to the binary32 grid.

The exact rational endpoints are passed directly to the proved directed-rational interface. Its internal fixed-point quotient enclosure may be conservative, but the wrapper inequalities above cover the complete conversion and there is no caller-selected approximation scale.

Instances For

source

@[inline]