Rational semantics of exact-dyadic order

Dyadic stores a signed natural significand and an integral power of two. Its executable comparison routines avoid constructing rationals: they align powers of two, compare natural magnitudes, and account for signs. This module proves that those decisions are exactly the ordering decisions made by Dyadic.toRat.

The correctness arguments are separate from execution. Field-level comparisons avoid temporary Dyadic records, while format proofs can use rational inequalities. The later lemmas show that the leading-position comparator agrees with full exponent alignment.

Basic rational denotations

@[simp]

theorem FloatLib.Numerics.Dyadic.zero_toRat : zero.toRat = 0

Canonical exact zero denotes rational zero.

@[simp]

theorem FloatLib.Numerics.Dyadic.ofScaledInt_toRat (coefficient exponent : ℤ) : (ofScaledInt coefficient exponent).toRat = Rat.ofInt coefficient * 2 ^ exponent

The scaled-integer constructor has exactly its expected rational denotation.

theorem FloatLib.Numerics.Dyadic.toRat_pos_of_significand_ne_zero (value : Dyadic) (hsignificand : value.significand ≠ 0) (hnegative : value.negative = false) : 0 < value.toRat

A nonzero dyadic whose sign field is clear has a strictly positive rational denotation.

Format-specific exact rounders share this fact when they reduce signed inputs to positive magnitudes. Keeping it on the common carrier avoids duplicating sign-and-scale arguments in every radix-two format.

@[simp]

theorem FloatLib.Numerics.Dyadic.toRat_eq_zero_iff (value : Dyadic) : value.toRat = 0 ↔ value.significand = 0

A dyadic has zero rational value exactly when its integer significand is zero.

theorem FloatLib.Numerics.Dyadic.neg_toRat (value : Dyadic) : value.neg.toRat = -value.toRat

Exact dyadic negation commutes with rational denotation.

theorem FloatLib.Numerics.Dyadic.mul_toRat (left right : Dyadic) : (left.mul right).toRat = left.toRat * right.toRat

Exact dyadic multiplication commutes with rational denotation.

Exponent alignment and comparison

theorem FloatLib.Numerics.Dyadic.compare_eq_compare_toRat (left right : Dyadic) : left.compare right = Ord.compare left.toRat right.toRat

The executable comparator is the ordinary linear-order comparator on rational denotations.

This is the proof boundary that lets format-specific rounders use aligned integers while their specifications remain stated in mathlib's ordered rational field. Proving the three-way result once also keeps the strict and equality corollaries below from repeating exponent alignment.

theorem FloatLib.Numerics.Dyadic.compare_eq_lt_iff (left right : Dyadic) : left.compare right = Ordering.lt ↔ left.toRat < right.toRat

The integer comparator reports lt exactly when rational denotation is smaller.

theorem FloatLib.Numerics.Dyadic.compare_eq_gt_iff (left right : Dyadic) : left.compare right = Ordering.gt ↔ right.toRat < left.toRat

The integer comparator reports gt exactly when rational denotation is greater.

Keeping both strict directions at the comparator boundary lets nearest-even rounders inspect one three-way comparison instead of evaluating two independently aligned dyadic comparisons.

theorem FloatLib.Numerics.Dyadic.compare_eq_eq_iff (left right : Dyadic) : left.compare right = Ordering.eq ↔ left.toRat = right.toRat

The integer comparator reports eq exactly for equal rational denotations.

Field-level scalable comparison

Optimized rounders often hold the sign, significand, and exponent in local variables rather than in a constructed Dyadic. These lemmas connect that execution path to the same rational order without requiring runtime record construction.

theorem FloatLib.Numerics.Dyadic.Internal.compareNonzeroMagnitudes_eq_compareNonnegativeFields (leftSignificand rightSignificand : ℕ) (leftExponent rightExponent : ℤ) (hleft : leftSignificand ≠ 0) (hright : rightSignificand ≠ 0) : compareNonzeroMagnitudes leftSignificand leftExponent rightSignificand rightExponent = compareNonnegativeFields leftSignificand leftExponent rightSignificand rightExponent

Leading-position magnitude comparison equals ordinary exact nonnegative comparison.

The optimized branch avoids exponent-gap allocation; this theorem keeps the existing exact dyadic comparator as its mathematical specification.

theorem FloatLib.Numerics.Dyadic.Internal.compareScalableFields_eq_compareFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : compareScalableFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = compareFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent

Exponent-scalable field comparison has exactly the ordinary exact-dyadic result.

Kernels can use this equality to justify comparisons over large exponent ranges without materializing an integer whose width is the exponent gap.

theorem FloatLib.Numerics.Dyadic.Internal.compareScalable_eq_compare (left right : Dyadic) : compareScalable left right = left.compare right

Record-based scalable comparison equals ordinary exact-dyadic comparison.

Boolean comparison API

theorem FloatLib.Numerics.Dyadic.isLess_eq_decide (left right : Dyadic) : left.isLess right = decide (left.toRat < right.toRat)

Boolean strict comparison agrees with rational order.

theorem FloatLib.Numerics.Dyadic.isLessOrEqual_eq_decide (left right : Dyadic) : left.isLessOrEqual right = decide (left.toRat ≤ right.toRat)

Boolean non-strict comparison agrees with rational order.

theorem FloatLib.Numerics.Dyadic.isEqual_eq_decide (left right : Dyadic) : left.isEqual right = decide (left.toRat = right.toRat)

Boolean numerical equality agrees with equality of exact rational denotations.

theorem FloatLib.Numerics.Dyadic.isEqual_comm (left right : Dyadic) : left.isEqual right = right.isEqual left

Numerical equality is symmetric even when dyadic records are not normalized.