NN.Floats.IEEEExec.DirectedRoundingSoundness.SignedOps

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.

source

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” #

source

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.

source

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.

source

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

(roundDyadicPosUp mant exp).isNaN = false

Soundness of roundDyadicDown: $\operatorname{toEReal}(\operatorname{roundDyadicDown}(d)) \leq\operatorname{dyadicToReal}(d)$.

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

source

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.

source

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.

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toEReal_roundDyadicUp_ge (d : Dyadic) :

↑(dyadicToReal d) ≤ (roundDyadicUp d).toEReal

Soundness of roundDyadicUp: $\operatorname{dyadicToReal}(d) \leq\operatorname{toEReal}(\operatorname{roundDyadicUp}(d))$.

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

source

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: $\operatorname{toEReal}(\operatorname{addDown}(x,y)) \leq\operatorname{toReal}(x)+\operatorname{toReal}(y)$, even when the result overflows to $-\infty$.

source

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: $\operatorname{toReal}(x)+\operatorname{toReal}(y) \leq\operatorname{toEReal}(\operatorname{addUp}(x,y))$, with overflow rounding to $+\infty$.

source