Comparison helpers for executable interval demos

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

• Float32Interval.IntervalF32: a deliberately naive runtime-Float32 interval model;
• RealInterval.IntervalRat: exact rational interval arithmetic for small reference checks;
• conversions from finite IEEE32Exec / 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 only 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 is a baseline, not the verified interval implementation. Operations use ordinary runtime Float32 arithmetic and therefore do not provide outward-rounding guarantees. It is useful in demos because it shows exactly why IEEE32Exec.Interval32 exists.

• lo : Float32

  Lower endpoint.

• hi : Float32

  Upper endpoint.

@[implicit_reducible]

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

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

@[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.min4 (a b c d : Float32) : Float32

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

def TorchLean.Floats.Interval.Comparison.Float32Interval.IntervalF32.max4 (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.

structure TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat : Type

Closed interval with exact rational endpoints.

This is a compact reference domain for examples. It is intentionally small: enough for corner-rule checks and containment comparisons, not a replacement for a full real-analysis interval library.

• lo : ℚ

  Lower endpoint.

• hi : ℚ

  Upper endpoint.

@[implicit_reducible]

instance TorchLean.Floats.Interval.Comparison.RealInterval.instReprIntervalRat : Repr IntervalRat

def TorchLean.Floats.Interval.Comparison.RealInterval.instReprIntervalRat.repr : IntervalRat → ℕ → Std.Format

@[inline]

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.point (x : ℚ) : IntervalRat

Degenerate rational interval [x, x].

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.min4 (a b c d : ℚ) : ℚ

Minimum of four rationals.

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.max4 (a b c d : ℚ) : ℚ

Maximum of four rationals.

@[inline]

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.add (A B : IntervalRat) : IntervalRat

Exact interval addition over rationals.

@[inline]

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.neg (A : IntervalRat) : IntervalRat

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

@[inline]

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.sub (A B : IntervalRat) : IntervalRat

Exact interval subtraction over rationals.

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.mul (A B : IntervalRat) : IntervalRat

Classical four-corner multiplication over exact rationals.

def TorchLean.Floats.Interval.Comparison.RealInterval.IntervalRat.contains (outer inner : IntervalRat) : Bool

Boolean check that outer contains inner.

def TorchLean.Floats.Interval.Comparison.RealInterval.showIntervalRat (I : IntervalRat) : String

Pretty-print an exact rational interval.

def TorchLean.Floats.Interval.Comparison.interval32ToRat? (I : IEEE754.IEEE32Exec.Interval32) : Option RealInterval.IntervalRat

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 RealInterval.IntervalRat

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

def TorchLean.Floats.Interval.Comparison.intervalUnaryEndpoints (f : IEEE754.IEEE32Exec → IEEE754.IEEE32Exec) (lo hi : IEEE754.IEEE32Exec) : IEEE754.IEEE32Exec.Interval32

Endpoint-evaluate a unary function over an IEEE32Exec interval.

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

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.