Order theory for exact dyadics

The executable cmpDyadic comparison agrees with real order. The proof reduces it to cmpDyadicAligned, aligns both integer significands at the smaller exponent, and then cancels their common positive power-of-two scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_eq_signedSignificand_shiftLeft (d : Numerics.Dyadic) (exponent : ℤ) (hexponent : exponent ≤ d.exponent) : d.toReal = ↑{ negative := d.negative, significand := d.significand.shiftLeft (d.exponent - exponent).toNat, exponent := 0 }.signedSignificand * Flocq.bpow Numerics.binaryRadix exponent

Real semantics after moving a dyadic significand to any smaller exponent.

The aligned integer is the exact signed significand at scale 2^exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_lt_iff (a b : Numerics.Dyadic) : cmpDyadic a b = Ordering.lt ↔ a.toReal < b.toReal

Executable dyadic comparison returns .lt exactly when the real values are ordered.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_eq_iff (a b : Numerics.Dyadic) : cmpDyadic a b = Ordering.eq ↔ a.toReal = b.toReal

Executable dyadic comparison returns .eq exactly when the real values are equal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_gt_iff (a b : Numerics.Dyadic) : cmpDyadic a b = Ordering.gt ↔ b.toReal < a.toReal

Executable dyadic comparison returns .gt exactly when the real values are reversed.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_eq_compare (a b : Numerics.Dyadic) : cmpDyadic a b = compare a.toReal b.toReal

Executable dyadic comparison is the comparison of the real values.