Directed rounding soundness for division (IEEE32Exec)

NN/Floats/IEEEExec/Exec32.lean defines executable outward-rounded division endpoints:

• roundRatDown / roundRatUp: enclose an exact rational ±(num/den) by a dyadic at scale $2^{\mathtt{ratApproxShift}}$ and then apply roundDyadicDown / roundDyadicUp.
• divDown / divUp: lift this to IEEE32 floats (handling NaN/Inf/±0 cases explicitly).

This file proves the enclosure direction that is needed for interval arithmetic soundness:

• $\operatorname{toEReal}(\operatorname{roundRatDown}(\ldots))\le\text{exact}$,
• $\text{exact}\le\operatorname{toEReal}(\operatorname{roundRatUp}(\ldots))$,
• $\operatorname{toEReal}(\operatorname{divDown}(x,y))\le \operatorname{toReal}(x)/\operatorname{toReal}(y)$ and $\operatorname{toReal}(x)/\operatorname{toReal}(y)\le \operatorname{toEReal}(\operatorname{divUp}(x,y))$ in the finite, nonzero-divisor regime.

We work in EReal so that overflow of the computed endpoints to ±∞ remains a sound enclosure.

References (interval arithmetic background):

• IEEE 754-2019 (floating-point arithmetic): doi:10.1109/IEEESTD.2019.8766229
• Goldberg (1991): doi:10.1145/103162.103163
• Moore–Kearfott–Cloud (2009), Introduction to Interval Analysis.

Local helpers

Natural ceil helper used by roundRatUp

Dyadic enclosure of num/den at scale 2^ratApproxShift

Soundness of roundRatDown / roundRatUp

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundRatDown_le (sign : Bool) (num den : ℕ) (hden : den ≠ 0) : (roundRatDown sign num den).toEReal ≤ if sign = true then -(↑↑num / ↑↑den) else ↑↑num / ↑↑den

Soundness of roundRatDown: the computed lower endpoint is below (or equal to) the exact rational.

This is the enclosure direction interval arithmetic needs: roundRatDown sign num den is a lower bound on the exact signed quotient ±(num/den).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundRatUp_ge (sign : Bool) (num den : ℕ) (hden : den ≠ 0) : (if sign = true then -(↑↑num / ↑↑den) else ↑↑num / ↑↑den) ≤ (roundRatUp sign num den).toEReal

Soundness of roundRatUp: the exact rational is below (or equal to) the computed upper endpoint.

Together with toEReal_roundRatDown_le, this yields an EReal enclosure for ±(num/den).

Expressing dyadic division as the same signed rational used by divDown/divUp

We reuse shared helper lemmas from RatScaling: scaleRat_ofNat, scaleRat_negSucc, neural_bpow_div, dyadicToReal_div_eq_signedRat.

Soundness of divDown / divUp in the finite, nonzero-divisor regime

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_divDown_le (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) : (x.divDown y).toEReal ≤ ↑(x.toReal / y.toReal)

Soundness of divDown: a lower enclosure for real division in EReal.

In the finite, nonzero-divisor regime this shows: toEReal (divDown x y) <= (toReal x / toReal y). We use EReal so that overflow of the computed endpoint to ±∞ remains a sound enclosure.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_divUp_ge (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) : ↑(x.toReal / y.toReal) ≤ (x.divUp y).toEReal

Soundness of divUp: an upper enclosure for real division in EReal.

In the finite, nonzero-divisor regime this shows: (toReal x / toReal y) <= toEReal (divUp x y).