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:

1. Call the Arb oracle (NN/Floats/Arb) to obtain a rigorous real enclosure [L,U] ⊇ f([a,b]).
2. Convert L,U : ℚ to float32 endpoints by rounding outward to the IEEE32Exec grid:
   • lower endpoint: round toward -∞ (using roundDyadicDown),
   • upper endpoint: round toward +∞ (using roundDyadicUp).

Trust boundary:

• The enclosure [L,U] is an oracle claim from Arb/python-flint; this module does not prove the Arb computation inside Lean.
• The rounding-to-float32 step is in-Lean and (for dyadic rounding) proved sound in NN/Floats/IEEEExec/DirectedRoundingSoundness.lean.

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

def Rat.toArbString (q : ℚ) : String

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

Exact rational view of float32 values

def TorchLean.Floats.IEEE754.IEEE32Exec.Dyadic.toRat (d : Dyadic) : ℚ

Convert an exact dyadic (-1)^sign * mant * 2^exp into an exact rational (ℚ).

def TorchLean.Floats.IEEE754.IEEE32Exec.toRat? (x : IEEE32Exec) : Option ℚ

Exact rational value of a finite IEEE32Exec float.

Returns none for NaN/Inf.

Outward rounding from ℚ to IEEE32Exec

def TorchLean.Floats.IEEE754.IEEE32Exec.pow2Rat (k : ℕ) : ℚ

A rational view of 2^k.

This is a small helper used to implement ratToDyadicDown/ratToDyadicUp.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratToDyadicDown (q : ℚ) (k : ℕ) : Dyadic

Approximate a rational q from below by a dyadic with denominator 2^k:

d = floor(q * 2^k) * 2^{-k}.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratToDyadicUp (q : ℚ) (k : ℕ) : Dyadic

Approximate a rational q from above by a dyadic with denominator 2^k:

d = ceil(q * 2^k) * 2^{-k}.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatQDown (q : ℚ) (k : ℕ := 200) : IEEE32Exec

Outward rounding down of a rational to the float32 grid (via a dyadic approximation).

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatQUp (q : ℚ) (k : ℕ := 200) : IEEE32Exec

Outward rounding up of a rational to the float32 grid (via a dyadic approximation).

Arb-backed interval endpoints for transcendentals

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.

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.

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.arbUnary (func : String) (X : Interval32) (precBits digits dyadicBits : ℕ := 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.

dyadicBits controls the internal dyadic approximation used when rounding rationals to float32; it can be increased if you want the outward rounding to be closer to the Arb bounds.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.tanhArb (X : Interval32) (precBits digits dyadicBits : ℕ := 200) : IO Interval32

Arb-backed tanh enclosure for Interval32 (oracle + outward rounding to float32 endpoints).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.expArb (X : Interval32) (precBits digits dyadicBits : ℕ := 200) : IO Interval32

Arb-backed exp enclosure for Interval32 (oracle + outward rounding to float32 endpoints).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.logArb (X : Interval32) (precBits digits dyadicBits : ℕ := 200) : IO Interval32

Arb-backed log enclosure for Interval32 (oracle + outward rounding to float32 endpoints).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.sqrtArb (X : Interval32) (precBits digits dyadicBits : ℕ := 200) : IO Interval32

Arb-backed sqrt enclosure for Interval32 (oracle + outward rounding to float32 endpoints).