Arb vs IEEE32Exec 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.
• IEEE32Exec: 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 quick 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 IEEE32Exec side and reports the Arb failure.

def TorchLean.Floats.Interval.ComparisonTutorial.polynomialExpr : Lean.Json

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

def TorchLean.Floats.Interval.ComparisonTutorial.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;
• IEEE32Exec: endpoint evaluation using TorchLean's deterministic binary32 executable model;
• Float32: ordinary runtime endpoint evaluation;
• IEEE32Exec+Arb: Arb real enclosure rounded outward to binary32 endpoints.

def TorchLean.Floats.Interval.ComparisonTutorial.runAddTie : IO Unit

def TorchLean.Floats.Interval.ComparisonTutorial.runSignedZeroDiv : IO Unit

def TorchLean.Floats.Interval.ComparisonTutorial.main (_args : List String) : IO UInt32

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

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

Entrypoint: run the Arb-vs-IEEE32Exec interval tutorial.