Order theory for exact dyadics

The executable cmpDyadic comparison agrees with real order. The proof 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.