Comparison helpers for executable interval examples

This module contains small, reusable baselines for numerical-audit examples:

• Interval Float32: a deliberately naive runtime-Float32 interval model;
• FloatLib's RationalInterval: exact rational endpoints for small reference checks;
• conversions from finite Binary 8 23 / runtime Float32 endpoints into rational intervals.

FloatLib supplies the interval arithmetic and its proofs. This module provides baselines that make examples and regression tests easier to read.

def TorchLean.Floats.Interval.Comparison.formatConfigured {fmt : FloatLib.Floats.Formats.BinaryInterchange.FloatFormat} {plan : FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [FloatLib.Floats.ExecFloat.ModelCodec plan (FloatLib.Floats.Formats.BinaryInterchange.Model fmt) code] (I : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family fmt code plan))) : String

Display configured endpoints through binary64, retaining their full original bit encodings.

def TorchLean.Floats.Interval.Comparison.formatValue {α β : Type} [ToString α] [ToString β] (bits : α → β) (x : α) : String

Pretty-print a scalar together with its raw encoding.

def TorchLean.Floats.Interval.Comparison.format {α : Type} (render : α → String) (I : FloatLib.Numerics.Interval α) : String

Pretty-print endpoints using a scalar renderer.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.posZero : Float32

+0.0f by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.negZero : Float32

-0.0f by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.posInf : Float32

+∞ by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.negInf : Float32

-∞ by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.add {α : Type} [Add α] (A B : FloatLib.Numerics.Interval α) : FloatLib.Numerics.Interval α

Naive endpoint addition; no directed rounding.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.sub {α : Type} [Sub α] (A B : FloatLib.Numerics.Interval α) : FloatLib.Numerics.Interval α

Naive endpoint subtraction; no directed rounding.

def TorchLean.Floats.Interval.Comparison.Naive.mul {α : Type} [Mul α] [Min α] [Max α] (A B : FloatLib.Numerics.Interval α) : FloatLib.Numerics.Interval α

Classical four-corner multiplication in the endpoint carrier; no directed rounding.

@[inline]

def TorchLean.Floats.Interval.Comparison.Naive.whole : FloatLib.Numerics.Interval Float32

Conservative fallback interval [-∞, +∞].

def TorchLean.Floats.Interval.Comparison.Naive.containsZero (I : FloatLib.Numerics.Interval Float32) : Bool

Return true iff the interval contains zero, including signed-zero endpoints.

def TorchLean.Floats.Interval.Comparison.Naive.div (A B : FloatLib.Numerics.Interval Float32) : FloatLib.Numerics.Interval Float32

Naive four-corner division when the denominator does not contain zero.

If the denominator straddles zero, return whole, mirroring the shape of Binary.Interval.div but without directed rounding.

def TorchLean.Floats.Interval.Comparison.Rational.mul (A B : FloatLib.Numerics.RationalInterval) : FloatLib.Numerics.RationalInterval

Classical four-corner multiplication over exact rationals.

def TorchLean.Floats.Interval.Comparison.Rational.contains (outer inner : FloatLib.Numerics.RationalInterval) : Bool

Boolean check that outer contains inner.

def TorchLean.Floats.Interval.Comparison.Rational.format (I : FloatLib.Numerics.RationalInterval) : String

Pretty-print an exact rational interval.

def TorchLean.Floats.Interval.Comparison.toRational? {α : Type} (decode : α → Option ℚ) (I : FloatLib.Numerics.Interval α) : Option FloatLib.Numerics.RationalInterval

Decode rational endpoints, preserving the decoder's special-value policy on failure.

def TorchLean.Floats.Interval.Comparison.endpoints {α : Type} [Min α] [Max α] (f : α → α) (lo hi : α) : FloatLib.Numerics.Interval α

Endpoint-evaluate a unary function, using the carrier's minimum and maximum.

This is not a sound transcendental interval rule in general; it is a comparison baseline for examples.