Directed executable IEEE32 operations.

This file provides lower and upper rounding variants for arithmetic operations, forming the runtime side of the interval-enclosure story.

def TorchLean.Floats.IEEE754.IEEE32Exec.shiftRightCeilPow2 (n shift : ℕ) : ℕ

ceil(n / 2^shift) for naturals, implemented via shifts (used for directed rounding).

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicPosDown (mant : ℕ) (exp : ℤ) : IEEE32Exec

Directed rounding down (toward -∞) for a positive dyadic mant * 2^exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicPosUp (mant : ℕ) (exp : ℤ) : IEEE32Exec

Directed rounding up (toward +∞) for a positive dyadic mant * 2^exp.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicDown (d : Dyadic) : IEEE32Exec

Directed rounding down (toward -∞) of an exact dyadic to float32.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicUp (d : Dyadic) : IEEE32Exec

Directed rounding up (toward +∞) of an exact dyadic to float32.

def TorchLean.Floats.IEEE754.IEEE32Exec.addDown (x y : IEEE32Exec) : IEEE32Exec

addDown x y is a float32 lower bound for the exact real sum (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.addUp (x y : IEEE32Exec) : IEEE32Exec

addUp x y is a float32 upper bound for the exact real sum (when finite).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.subDown (x y : IEEE32Exec) : IEEE32Exec

subDown x y is a float32 lower bound for the exact real difference (when finite).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.subUp (x y : IEEE32Exec) : IEEE32Exec

subUp x y is a float32 upper bound for the exact real difference (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.mulDown (x y : IEEE32Exec) : IEEE32Exec

mulDown x y is a float32 lower bound for the exact real product (when finite).

def TorchLean.Floats.IEEE754.IEEE32Exec.mulUp (x y : IEEE32Exec) : IEEE32Exec

mulUp x y is a float32 upper bound for the exact real product (when finite).

Directed rounding for exact rationals (division-friendly)

For divDown/divUp we need outward rounding of an exact rational num/den to the float32 grid. Our dyadic-directed rounders (roundDyadicDown/roundDyadicUp) already have a clean soundness proof, so we reduce rational rounding to dyadic rounding by building a dyadic enclosure of num/den:

• lower dyadic: ⌊(num/den) * 2^K⌋ * 2^{-K},
• upper dyadic: ⌈(num/den) * 2^K⌉ * 2^{-K}.

We then apply roundDyadicDown/roundDyadicUp to these dyadics.

This is sound (it produces outward-rounded endpoints), but it is not necessarily optimally tight; a larger ratApproxShift improves tightness at some computational cost.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratApproxShift : ℕ

Number of extra bits used when turning num/den into a dyadic enclosure.

def TorchLean.Floats.IEEE754.IEEE32Exec.quotCeil (num den : ℕ) : ℕ

ceil(num/den) for naturals, totalized (returns 0 when den = 0).

def TorchLean.Floats.IEEE754.IEEE32Exec.ratLowerMant (num den : ℕ) : ℕ

Lower dyadic mantissa for num/den at scale 2^ratApproxShift.

def TorchLean.Floats.IEEE754.IEEE32Exec.ratUpperMant (num den : ℕ) : ℕ

Upper dyadic mantissa for num/den at scale 2^ratApproxShift.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatDown (sign : Bool) (num den : ℕ) : IEEE32Exec

Directed rounding down (toward -∞) for a rational ±(num/den) with den > 0.

We do not attempt to be "correctly rounded" in the IEEE-754 sense; we only need a sound lower bound.

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatUp (sign : Bool) (num den : ℕ) : IEEE32Exec

Directed rounding up (toward +∞) for a rational ±(num/den) with den > 0.

def TorchLean.Floats.IEEE754.IEEE32Exec.divDown (x y : IEEE32Exec) : IEEE32Exec

divDown x y is a float32 lower bound for the exact real quotient (when finite and y ≠ 0).

def TorchLean.Floats.IEEE754.IEEE32Exec.divUp (x y : IEEE32Exec) : IEEE32Exec

divUp x y is a float32 upper bound for the exact real quotient (when finite and y ≠ 0).