Arb vs configured binary32 interval tutorial

This tutorial prints side-by-side enclosures for a few unary functions over a one-dimensional input interval:

• Arb (python-flint / Arb ball arithmetic): rigorous real enclosures at chosen precision.
• configured binary32: executable float32 evaluation on the endpoints (not a proved outward-rounded interval rule for transcendentals).
• Float32 baseline: ordinary runtime Float32 endpoint arithmetic, included to show why directed rounding matters.
• Rational baseline: exact Rat interval arithmetic for small polynomial/reference checks. NumPy / PyTorch analogue:

import numpy as np

lo, hi = np.float32(-0.5), np.float32(0.5)
endpoint_box = (np.tanh(lo), np.tanh(hi))   # common fast check, not a rigorous enclosure

TorchLean's lesson is more explicit: endpoint evaluation is useful for debugging, but rigorous transcendental enclosures need a trusted real enclosure source (here Arb) plus outward rounding back to the binary32 grid.

Implementation note: the reusable baseline interval helpers live in NN.Floats.Interval.Comparison; this file only chooses tutorial cases and prints their results.

Run:

lake exe torchlean floats_arb_ieee_compare

If Arb is not installed, the tutorial still prints the configured binary32 side and reports the Arb failure.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.polynomialExpr : Lean.Json

JSON expression for $x^2+0.1x-0.5$, in the safe Arb expression language.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.runOne (func : String) (lo hi : Float) (precBits digits : ℕ) : IO Unit

Run one tutorial comparison.

The output has four conceptual rows:

• Arb: rigorous real interval from the external oracle when available;
• ExecFloat.Binary 8 23: endpoint evaluation using FloatLib's configured binary32 arithmetic;
• Float32: ordinary runtime endpoint evaluation;
• configured binary32+Arb: Arb real enclosure rounded outward to binary32 endpoints.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.runAddTie : IO Unit

The classic round-to-nearest-even tie: 1 + 2^-24 in binary32.

The exact sum needs 25 significand bits, so it sits exactly halfway between 1 and the next float. Round-to-nearest-even therefore returns 1, not the next value up. Comparing the naive interval arithmetic against the directed addDown/addUp pair here is the point: only the directed version still encloses the exact rational sum.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.runSignedZeroDiv : IO Unit

Division by negative zero, which IEEE 754 defines as -∞ rather than an error.

The sign of zero is observable precisely through operations like this one, which is why the float32 model keeps +0 and -0 distinct instead of collapsing them.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.run : IO UInt32

Run a small fixed set of comparisons (unary funcs + a polynomial + some edge cases).

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.usage : String

Command-line help for the Arb-vs-IEEE32 interval tutorial.

def NN.Examples.DeepDives.Floats.ArbIEEEExecCompare.main (args : List String) : IO UInt32

Entrypoint: run the Arb-vs-ExecFloat.Binary 8 23 interval tutorial.