Directed rounding soundness for IEEE32Exec

NN/Floats/IEEEExec/Exec32.lean defines executable directed rounding on the IEEE-754 binary32 grid:

• roundDyadicDown / roundDyadicUp round an exact dyadic toward -∞ / +∞.
• addDown/addUp, mulDown/mulUp lift this to outward-rounded arithmetic for interval endpoints.

This file proves (one core piece of) the enclosure direction (“golden theorem” style): the directed rounding down kernel for positive dyadics is a sound lower bound for the exact real value.

Scope (what is proved here):

• roundDyadicPosDown / roundDyadicPosUp soundness (in EReal, to handle overflow to ±∞).
• Full dyadic rounding soundness: roundDyadicDown is a lower bound and roundDyadicUp is an upper bound for the exact dyadic real semantics.
• Interval-endpoint soundness for addDown/addUp/mulDown/mulUp on finite inputs, as inequalities in EReal between the executable endpoint operation and the exact real operation.

Outside this file's scope:

• Correctly-rounded/outward-rounded transcendental functions w.r.t. a standard libm. IEEE-754 does not specify libm results; for rigorous transcendentals, prefer the Arb oracle backend.
• Division/sqrt interval primitives (substantially larger; requires separate algorithms + proofs).

References:

• IEEE 754-2019 (floating-point arithmetic): doi:10.1109/IEEESTD.2019.8766229
• Goldberg (1991), “What Every Computer Scientist Should Know About Floating-Point Arithmetic”: doi:10.1145/103162.103163

Basic helpers

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.IEEE754.IEEE32Exec.bpow (e : ℤ) : ℝ

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_pos (e : ℤ) : 0 < bpow e

bpow e = 2^e is strictly positive.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_nonneg (e : ℤ) : 0 ≤ bpow e

bpow e = 2^e is nonnegative.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_add (e1 e2 : ℤ) : bpow (e1 + e2) = bpow e1 * bpow e2

Exponent law for bpow: bpow (e₁+e₂) = bpow e₁ * bpow e₂.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_le_pow2_succ (k : ℕ) : pow2 k ≤ pow2 (k + 1)

pow2 is monotone in the exponent, in the simple form pow2 k ≤ pow2 (k+1).

We use this for small exponent-range arguments (e.g. 2^23 ≤ 2^24) without importing broader monotonicity machinery.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_lt_pow2_succ (k : ℕ) : pow2 k < pow2 (k + 1)

Strict growth of pow2: pow2 k < pow2 (k+1).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_add (a b : ℕ) : pow2 (a + b) = pow2 a * pow2 b

theorem TorchLean.Floats.IEEE754.IEEE32Exec.pow2_mul (a b : ℕ) : pow2 a * pow2 b = pow2 (a + b)

Commuted form of pow2_add: pow2 a * pow2 b = pow2 (a + b).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_ofNat (n : ℕ) : bpow (Int.ofNat n) = ↑(pow2 n)

Interpret bpow at a natural exponent in terms of pow2.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_negSucc (n : ℕ) : bpow (Int.negSucc n) = (↑(pow2 (n + 1)))⁻¹

Interpret bpow at a negative successor exponent as an inverse power of two.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_pos (mant : ℕ) (exp : ℤ) : dyadicToReal { sign := false, mant := mant, exp := exp } = ↑mant * bpow exp

Real semantics of a nonnegative dyadic (mant, exp) (sign bit false).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_signTrue (mant : ℕ) (exp : ℤ) : dyadicToReal { sign := true, mant := mant, exp := exp } = -(↑mant * bpow exp)

Real semantics of a negative dyadic (mant, exp) (sign bit true).

A few float32 constants as reals

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.directed_toEReal_posZero : posZero.toEReal = 0

toEReal maps +0 to 0.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.directed_toEReal_negZero : negZero.toEReal = 0

toEReal maps -0 to 0.

Shift helpers (floor/ceil division by powers of two)

shiftRightCeilPow2 is also controlled from above by the corresponding floor quotient: ceil-division can overshoot by at most 1.

Soundness: directed rounding on positive dyadics

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundDyadicPosDown_le (mant : ℕ) (exp : ℤ) (hm : mant ≠ 0) : (roundDyadicPosDown mant exp).toReal ≤ ↑mant * bpow exp

roundDyadicPosDown is a real lower bound for a positive dyadic.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicPosUp_ge (mant : ℕ) (exp : ℤ) (hm : mant ≠ 0) : ↑↑mant * ↑(bpow exp) ≤ (roundDyadicPosUp mant exp).toEReal

roundDyadicPosUp mant exp is an EReal upper bound for the positive dyadic (mant : ℝ) * 2^exp.

This is the “ceil” counterpart to toReal_roundDyadicPosDown_le.