IEEE32Exec and FP32: Comparisons and Min/Max

Comparisons and min/max (finite refinement)

Comparisons are subtle in IEEE-754 because of NaNs and signed zeros. Since FP32 is a finite-only model, we only bridge the finite behavior here: comparisons/min/max agree with the corresponding real comparisons once NaNs/Infs are ruled out.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_eq_signedMant_shiftLeft_toExp (d : Dyadic) (e : ℤ) (he : e ≤ d.exp) : dyadicToReal d = ↑(signedMant d.sign (d.mant.shiftLeft (d.exp - e).toNat)) * neuralBpow binaryRadix e

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_lt_iff (a b : Dyadic) : cmpDyadic a b = Ordering.lt ↔ dyadicToReal a < dyadicToReal b

Dyadic comparison correctness (lt case).

cmpDyadic compares two decoded dyadics by aligning exponents and comparing signed integers. This theorem states that the .lt result agrees with the real-ordering of dyadicToReal.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_eq_iff (a b : Dyadic) : cmpDyadic a b = Ordering.eq ↔ dyadicToReal a = dyadicToReal b

Dyadic comparison correctness (eq case).

This is the equality variant of cmpDyadic_lt_iff.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.cmpDyadic_gt_iff (a b : Dyadic) : cmpDyadic a b = Ordering.gt ↔ dyadicToReal b < dyadicToReal a

Dyadic comparison correctness (gt case).

This is the greater-than variant of cmpDyadic_lt_iff, phrased as dyadicToReal b < dyadicToReal a.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_cmpDyadic_of_toDyadic? (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some (cmpDyadic dx dy)

Bridge for IEEE32Exec.compare on finite values.

When both operands decode to dyadics (toDyadic? = some), compare returns a result and it is exactly cmpDyadic of those dyadics.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_lt_iff_toReal_lt (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.lt ↔ x.toReal < y.toReal

compare x y = .lt if and only if toReal x < toReal y (finite path).

This is the user-facing ordering theorem that lets downstream reasoning switch between IEEE32Exec.compare and < on reals.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_eq_iff_toReal_eq (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.eq ↔ x.toReal = y.toReal

compare x y = .eq if and only if toReal x = toReal y (finite path).

Note: this equality is on the decoded real values; it ignores NaN payloads and signed-zero distinctions (those are handled explicitly elsewhere).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.compare_eq_some_gt_iff_toReal_gt (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : x.compare y = some Ordering.gt ↔ y.toReal < x.toReal

compare x y = .gt if and only if toReal y < toReal x (finite path).

This is the greater-than companion to compare_eq_some_lt_iff_toReal_lt.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_eq_zero_of_isZero (x : IEEE32Exec) {d : Dyadic} (hx : x.toDyadic? = some d) (hz : x.isZero = true) : x.toReal = 0

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_minimum_eq_min (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.minimum y).toReal = min x.toReal y.toReal

Bridge for IEEE32Exec.minimum on finite values: its real meaning is min (toReal x) (toReal y).

This proof follows IEEE-754 style rules (including NaN propagation and signed-zero handling), but the statement is on toReal, which erases the sign of zero.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_maximum_eq_max (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) : (x.maximum y).toReal = max x.toReal y.toReal

Bridge for IEEE32Exec.maximum on finite values: its real meaning is max (toReal x) (toReal y).

This is the companion of toReal_minimum_eq_min. As above, the conclusion is phrased in terms of toReal, so signed zeros are identified.