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.

Non-goals (not proved here yet):

• 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 heavier 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

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.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_neg_of_toDyadic?_some (x : IEEE32Exec) {d : Dyadic} (hx : x.toDyadic? = some d) : x.neg.toEReal = -x.toEReal

toEReal respects negation on the finite/dyadic branch.

We phrase this lemma using the dyadic decode witness toDyadic? x = some d, which guarantees:

• x is finite (hence toEReal agrees with toReal), and
• toReal (neg x) = -toReal x (via toReal_neg_eq_neg).

Negation / sign-bit flip helpers

Negation preserves “not NaN”

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_neg_eq_false_of_isNaN_eq_false (x : IEEE32Exec) (hnan : x.isNaN = false) : x.neg.isNaN = false

If x is not a NaN then neg x is not a NaN.

We only state the direction we actually need in the directed-rounding development: negative directed rounding is implemented as neg of a positive kernel, so we need to know this cannot introduce a NaN when starting from a non-NaN value.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_neg_of_isNaN_eq_false (x : IEEE32Exec) (hnan : x.isNaN = false) : x.neg.toEReal = -x.toEReal

toEReal commutes with neg as long as we are not in the NaN case.

This is a small but important glue lemma: it lets us lift the positive rounding kernels to the signed directed-rounding functions (roundDyadicDown / roundDyadicUp) without introducing new floating-point corner cases.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_roundDyadicPosUp_eq_false (mant : ℕ) (exp : ℤ) (hm : mant ≠ 0) : (roundDyadicPosUp mant exp).isNaN = false

Soundness of roundDyadicDown: the result is ≤ the exact dyadic real value (in EReal).

This is the key lemma needed to justify addDown/mulDown as interval lower endpoints.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_roundDyadicPosDown_some (mant : ℕ) (exp : ℤ) : ∃ (d : Dyadic), (roundDyadicPosDown mant exp).toDyadic? = some d

roundDyadicPosDown (directed rounding toward -∞ for positive dyadics) never produces a NaN/Inf value.

We package this as an existence statement: the output always has a dyadic decode. This is the bridge we use later to turn toEReal into toReal (as an EReal) without unfolding all bit-level definitions at call sites.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicDown_le (d : Dyadic) : (roundDyadicDown d).toEReal ≤ ↑(dyadicToReal d)

Soundness of roundDyadicDown: it produces an EReal lower bound for the exact dyadic value.

Informal: rounding down is monotone towards -∞, so the rounded result is always ≤ the exact real meaning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicUp_ge (d : Dyadic) : ↑(dyadicToReal d) ≤ (roundDyadicUp d).toEReal

Soundness of roundDyadicUp: the result is ≥ the exact dyadic real value (in EReal).

This is the key lemma needed to justify addUp/mulUp as interval upper endpoints.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addDown_le (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.addDown y).toEReal ≤ ↑(x.toReal + y.toReal)

Lower-endpoint soundness for addDown on finite inputs: the result is ≤ the exact real sum (in EReal), even in overflow-to--∞ scenarios.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_addUp_ge (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : ↑(x.toReal + y.toReal) ≤ (x.addUp y).toEReal

Upper-endpoint soundness for addUp on finite inputs: the exact real sum is ≤ the result (in EReal), with overflow rounding to +∞.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_mulDown_le (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.mulDown y).toEReal ≤ ↑(x.toReal * y.toReal)

Lower-endpoint soundness for mulDown on finite inputs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_mulUp_ge (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : ↑(x.toReal * y.toReal) ≤ (x.mulUp y).toEReal

Upper-endpoint soundness for mulUp on finite inputs.