Signed directed-rounding soundness.

The lemmas in this file handle sign-sensitive arithmetic cases for lower and upper IEEE32 rounding, connecting executable operations to real-valued enclosure statements.

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.