Arb-backed enclosures with FloatLib endpoint rounding #

Arb/python-flint supplies the external real-enclosure claim. Exact rational endpoints are then rounded outward by FloatLib's descriptor-generic software rounders. The theorems below are binary32 transport corollaries of FloatLib's directed-rational bounds. No native floating-point conversion or software transcendental approximation participates in this endpoint conversion.

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 `ExecFloat.Binary 8 23` #

source

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

(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQDown FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 q))).toEReal ≤ ↑↑q

The lower rational endpoint conversion is an EReal lower bound.

source

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

↑↑q ≤ (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundRatQUp FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 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 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toEReal_roundRatQDown_le._proof_1 toEReal_roundRatQDown_le._proof_2 toEReal_roundRatQDown_le._proof_3 toEReal_roundRatQDown_le._proof_4) (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. FloatLib's directed-rounding theorem covers the conversion, including overflow to infinite endpoints.

Instances For

source

@[inline]