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/Bridge/ERealTotal.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.

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

@[implicit_reducible]

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

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\in 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\in I\iff I.\mathtt{lo}\le x\land x\le I.\mathtt{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 ($\mathtt{lo}\le\mathtt{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: $-[\mathtt{lo},\mathtt{hi}]=[-\mathtt{hi},-\mathtt{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.minOfFour (a b c d : IEEE32Exec) : IEEE32Exec

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

def TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.maxOfFour (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 $[-\infty,+\infty]$ (useful as a conservative fallback).

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

Executable Boolean $x\le 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 four-corner rule when the denominator interval does not contain $0$.

If $0\in B$, we conservatively return $\mathtt{whole}=[-\infty,+\infty]$.

@[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\in B$, we return whole.

Pointwise activation ranges

@[inline]

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

Image enclosure for ReLU. Because ReLU is monotone, applying max(x,0) to both endpoints is both sound and sharp on the binary32 endpoint grid.

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

Image enclosure for absolute value.

Intervals entirely on one side of zero are preserved or negated. An interval crossing zero maps to [0, max(-lo, hi)].

@[inline]

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

Outward-rounded square-root image of a nonnegative interval.

The operation itself is total because IEEE32Exec.sqrtDown and sqrtUp implement IEEE special values. Callers that want a real enclosure must separately establish that both endpoints are finite and nonnegative; the graph numerical checker enforces that domain before constructing this range.