Comparison helpers for executable interval examples

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

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

The important design point is separation: examples should print comparisons, not quietly define a second interval library. The primary TorchLean interval implementation is IEEE32Exec.Interval32; this module provides baselines that make examples and regression tests easier to read.

def TorchLean.Floats.Interval.Comparison.showInterval32 (I : IEEE754.IEEE32Exec.Interval32) : String

Pretty-print an executable IEEE32Exec.Interval32, including endpoint bits.

def TorchLean.Floats.Interval.Comparison.showFloat32 (x : Float32) : String

Pretty-print a runtime Float32, including its raw IEEE-754 bit pattern.

structure TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32 : Type

Closed interval with runtime Float32 endpoints.

This baseline uses ordinary runtime Float32 arithmetic and provides no outward-rounding guarantee. Examples compare it with the verified IEEE32Exec.Interval32 implementation.

• lo : Float32

  Lower endpoint.

• hi : Float32

  Upper endpoint.

def TorchLean.Floats.Interval.Comparison.Float32Interval.instReprIntervalF32.repr : IntervalF32 → ℕ → Std.Format

@[instance_reducible]

instance TorchLean.Floats.Interval.Comparison.Float32Interval.instReprIntervalF32 : Repr IntervalF32

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.point (x : Float32) : IntervalF32

Degenerate runtime-Float32 interval [x, x].

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.posZero : Float32

+0.0f by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.negZero : Float32

-0.0f by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.posInf : Float32

+∞ by IEEE-754 binary32 bits.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.negInf : Float32

-∞ by IEEE-754 binary32 bits.

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.minOfFour (a b c d : Float32) : Float32

Minimum of four runtime Float32 values using Lean's runtime order.

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.maxOfFour (a b c d : Float32) : Float32

Maximum of four runtime Float32 values using Lean's runtime order.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.add (A B : IntervalF32) : IntervalF32

Naive endpoint addition; no directed rounding.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.neg (A : IntervalF32) : IntervalF32

Naive interval negation: -[lo, hi] = [-hi, -lo].

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.sub (A B : IntervalF32) : IntervalF32

Naive endpoint subtraction; no directed rounding.

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.mul (A B : IntervalF32) : IntervalF32

Classical four-corner multiplication using runtime Float32; no directed rounding.

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.whole : IntervalF32

Conservative fallback interval [-∞, +∞].

@[inline]

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.leB (x y : Float32) : Bool

Boolean comparison wrapper; NaN comparisons evaluate to false.

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.containsZero (I : IntervalF32) : Bool

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

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.div (A B : IntervalF32) : IntervalF32

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

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

def TorchLean.Floats.Interval.Comparison.showIntervalF32 (I : Float32Interval.IntervalF32) : String

Pretty-print a naive runtime-Float32 interval.

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.interval32ToRat? (I : IEEE754.IEEE32Exec.Interval32) : Option FloatLib.Numerics.RationalInterval

Exact rational endpoint interval for a finite IEEE32Exec.Interval32; none for NaN/Inf.

def TorchLean.Floats.Interval.Comparison.float32ToRat? (x : Float32) : Option ℚ

Exact rational value of a finite runtime Float32; none for NaN/Inf.

def TorchLean.Floats.Interval.Comparison.intervalF32ToRat? (I : Float32Interval.IntervalF32) : Option FloatLib.Numerics.RationalInterval

Exact rational endpoint interval for a finite runtime-Float32 interval.

def TorchLean.Floats.Interval.Comparison.intervalUnaryEndpoints (f : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) intervalUnaryEndpoints._proof_1 intervalUnaryEndpoints._proof_2 intervalUnaryEndpoints._proof_3 intervalUnaryEndpoints._proof_4 → FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) intervalUnaryEndpoints._proof_1 intervalUnaryEndpoints._proof_2 intervalUnaryEndpoints._proof_3 intervalUnaryEndpoints._proof_4) (lo hi : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) intervalUnaryEndpoints._proof_1 intervalUnaryEndpoints._proof_2 intervalUnaryEndpoints._proof_3 intervalUnaryEndpoints._proof_4) : IEEE754.IEEE32Exec.Interval32

Endpoint-evaluate a unary function over an ExecFloat.Binary 8 23 interval.

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

def TorchLean.Floats.Interval.Comparison.intervalUnaryEndpointsF32 (f : Float32 → Float32) (lo hi : Float32) : Float32Interval.IntervalF32

Endpoint-evaluate a unary function over a runtime-Float32 interval.

This is the naive runtime baseline paired with intervalUnaryEndpoints.