Executable IEEE32Exec endpoint intervals

This module contains the executable interval definitions for IEEE32Exec endpoints.

It keeps the API small: the main goal is to have an executable interval type with endpoints in the same discrete grid as IEEE-754 binary32 (IEEE32Exec), using outward-rounded endpoint arithmetic (addDown/addUp/mulDown/mulUp).

Soundness theorems (enclosure proofs) are not bundled here; they are best stated relative to a chosen real/extended-real interpretation (see NN/Floats/IEEEExec/BridgeERealTotal.lean).

structure TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 : Type

An executable closed interval with IEEE-754 binary32 semantics (IEEE32Exec) as endpoints.

This type is intended for computation (endpoint arithmetic with outward rounding). Soundness theorems relating these intervals to real/extended-real interpretations are stated in separate bridge files (so theorems can choose the right notion of "real meaning" for the application).

• lo : IEEE32Exec

  lo.

• hi : IEEE32Exec

  hi.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprInterval32 : Repr Interval32

def TorchLean.Floats.IEEE754.IEEE32Exec.instReprInterval32.repr : Interval32 → ℕ → Std.Format

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.mem (I : Interval32) (x : IEEE32Exec) : Prop

Membership predicate: x lies between lo and hi using the IEEE32Exec order.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.instMembership : Membership IEEE32Exec Interval32

Enable x ∈ I notation for executable Interval32 intervals.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.mem_iff (I : Interval32) (x : IEEE32Exec) : x ∈ I ↔ I.lo.le x ∧ x.le I.hi

Unfold membership: x ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi.

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.Valid (I : Interval32) : Prop

Validity predicate for executable intervals.

We require both endpoints to be finite (not NaN/Inf) and ordered (lo ≤ hi).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.point (x : IEEE32Exec) : Interval32

Degenerate interval [x, x].

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.hull (A B : Interval32) : Interval32

Interval hull / union enclosure of two executable intervals.

This is the smallest interval (by endpoints) that contains both A and B, computed by taking the minimum of lower endpoints and maximum of upper endpoints.

Implementation note: we use IEEE-754 minimum/maximum so NaNs propagate.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.valid_point_iff_isFinite (x : IEEE32Exec) : (point x).Valid ↔ x.isFinite = true

point x is valid exactly when x is finite.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.add (A B : Interval32) : Interval32

Outward-rounded interval addition.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.neg (A : Interval32) : Interval32

Interval negation: -[lo, hi] = [-hi, -lo].

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.sub (A B : Interval32) : Interval32

Outward-rounded interval subtraction.

Helper combinators for interval multiplication.

mul needs the minimum/maximum of 4 corner products. We expose these helpers (instead of keeping them private) so downstream soundness proofs can unfold Interval32.mul in a stable way.

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.min4 (a b c d : IEEE32Exec) : IEEE32Exec

Minimum of 4 float values, using IEEE minimum (NaNs propagate).

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.max4 (a b c d : IEEE32Exec) : IEEE32Exec

Maximum of 4 float values, using IEEE maximum (NaNs propagate).

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.mul (A B : Interval32) : Interval32

Outward-rounded interval multiplication via the classical 4-corner rule.

We compute downward-rounded lower-corner products for the lower bound and upward-rounded products for the upper bound, then take the min/max across corners.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.whole : Interval32

The "whole" interval [-∞, +∞] (useful as a conservative fallback).

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.leB (x y : IEEE32Exec) : Bool

Executable Boolean x ≤ y using IEEE compare.

If compare is unordered (none, i.e. NaN involved), we return false.

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.containsZero (I : Interval32) : Bool

Returns true iff the real interval denoted by I contains 0.

We use this to conservative-handle division by an interval that straddles zero: a single interval cannot precisely represent the true quotient set (which is typically a union), so we return whole instead.

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.div (A B : Interval32) : Interval32

Interval division via the classical 4-corner rule when the denominator interval does not contain 0.

If 0 ∈ B, we conservatively return whole = [-∞,+∞].

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.inv (B : Interval32) : Interval32

Interval reciprocal 1/B, implemented as a special case of interval division.

If 0 ∈ B, we return whole.