Binary exponent bounds for positive rational numbers

The executable rational rounder locates a positive quotient between consecutive powers of two using Numerics.RationalBinary.floorLog2. This module proves that format-independent characterization, including the asymmetric numerator and denominator cases that make quotient normalization easy to get wrong.

The result is shared by arbitrary exponent widths and both directed rounding modes. Division and conversion proofs can therefore reuse one rational lemma instead of duplicating leading-bit arguments for each concrete format.

Executable power-of-two comparisons

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.lessThanPowerOfTwo_eq_true_iff (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : Numerics.RationalBinary.lessThanPowerOfTwo numerator denominator exponent = true ↔ ↑numerator / ↑denominator < bpow exponent

Numerics.RationalBinary.lessThanPowerOfTwo exactly tests whether a natural quotient is below a binary power.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.atLeastPowerOfTwo_eq_true_iff (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : Numerics.RationalBinary.atLeastPowerOfTwo numerator denominator exponent = true ↔ bpow exponent ≤ ↑numerator / ↑denominator

Numerics.RationalBinary.atLeastPowerOfTwo exactly tests whether a binary power is at most the real quotient of two natural numbers with nonzero denominator.

Coarse logarithm bounds

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_log2_sub_log2_sub_one (numeratorLog denominatorLog : ℕ) : bpow (Int.ofNat numeratorLog - Int.ofNat denominatorLog - 1) = 2 ^ numeratorLog / 2 ^ denominatorLog.succ

Closed form for the lower coarse exponent candidate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_log2_sub_log2_add_one (numeratorLog denominatorLog : ℕ) : bpow (Int.ofNat numeratorLog - Int.ofNat denominatorLog + 1) = 2 ^ numeratorLog.succ / 2 ^ denominatorLog

Closed form for the upper coarse exponent candidate.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.log2_sub_log2_bounds (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have exponent := Int.ofNat numerator.log2 - Int.ofNat denominator.log2; bpow (exponent - 1) ≤ ↑numerator / ↑denominator ∧ ↑numerator / ↑denominator < bpow (exponent + 1)

The difference of the numerator and denominator leading-bit positions locates a positive quotient within one binary exponent.

Exact floor-logarithm characterization

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.bpow_interval_exponent_unique (value : ℝ) (left right : ℤ) (hleftLower : bpow left ≤ value) (hleftUpper : value < bpow (left + 1)) (hrightLower : bpow right ≤ value) (hrightUpper : value < bpow (right + 1)) : left = right

Two intervals of the form [2^e, 2^(e+1)) containing the same value have equal exponents.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_bounds (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have exponent := Numerics.RationalBinary.floorLog2 numerator denominator; bpow exponent ≤ ↑numerator / ↑denominator ∧ ↑numerator / ↑denominator < bpow (exponent + 1)

Numerics.RationalBinary.floorLog2 places a positive quotient between consecutive powers of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_eq_int_log (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : Numerics.RationalBinary.floorLog2 numerator denominator = Int.log 2 (↑numerator / ↑denominator)

The shift-based rational logarithm agrees with Mathlib's integer logarithm on positive inputs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_den_one (n : ℕ) (hn : n ≠ 0) : Numerics.RationalBinary.floorLog2 n 1 = ↑n.log2

Viewing a positive natural number as a quotient by one preserves its floor binary logarithm.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_eq_of_bounds (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hlower : bpow exponent ≤ ↑numerator / ↑denominator) (hupper : ↑numerator / ↑denominator < bpow (exponent + 1)) : Numerics.RationalBinary.floorLog2 numerator denominator = exponent

A binary interval characterization determines Numerics.RationalBinary.floorLog2.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floorLog2_scaleByPowerOfTwo (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : Numerics.RationalBinary.floorLog2 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).1 (Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent).2 = Numerics.RationalBinary.floorLog2 numerator denominator + exponent

Exact binary scaling adds its exponent to the rational floor logarithm.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaledRatToReal_floorLog2_bounds (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : bpow (Numerics.RationalBinary.floorLog2 numerator denominator + exponent) ≤ scaledRatToReal numerator denominator exponent ∧ scaledRatToReal numerator denominator exponent < bpow (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1)

The leading exponent of a scaled positive rational bounds its exact real value between consecutive binary powers.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.scaleByPowerOfTwo_floorLog2_bounds (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : have scaled := Numerics.RationalBinary.scaleByPowerOfTwo numerator denominator exponent; bpow (Numerics.RationalBinary.floorLog2 numerator denominator + exponent) ≤ ↑scaled.1 / ↑scaled.2 ∧ ↑scaled.1 / ↑scaled.2 < bpow (Numerics.RationalBinary.floorLog2 numerator denominator + exponent + 1)

After moving an external binary exponent into a positive rational, its quotient remains between the binary powers determined by the original leading exponent plus that scale.

Comparison with a positive dyadic

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compareDyadicScaled?_false_eq_compare (numerator denominator : ℕ) (exponent : ℤ) (value : Numerics.Dyadic) (hdenominator : denominator ≠ 0) (hvalueSign : value.negative = false) (hvalue : value.significand ≠ 0) : Numerics.RationalBinary.compareDyadicScaled? false numerator denominator exponent value = some (compare (scaledRatToReal numerator denominator exponent) value.toReal)

The optimized comparison of a nonnegative scaled rational with a positive dyadic returns exactly their real-number ordering.

The comparison first uses the leading exponent of the ratio to the dyadic. Only when that exponent is zero does it compare the scaled numerator and denominator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compareDyadicScaled?_false_eq_lt_iff (numerator denominator : ℕ) (exponent : ℤ) (value : Numerics.Dyadic) (hdenominator : denominator ≠ 0) (hvalueSign : value.negative = false) (hvalue : value.significand ≠ 0) : Numerics.RationalBinary.compareDyadicScaled? false numerator denominator exponent value = some Ordering.lt ↔ scaledRatToReal numerator denominator exponent < value.toReal

Nonnegative scaled-rational comparison returns .lt exactly for strict real order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compareDyadicScaled?_false_eq_eq_iff (numerator denominator : ℕ) (exponent : ℤ) (value : Numerics.Dyadic) (hdenominator : denominator ≠ 0) (hvalueSign : value.negative = false) (hvalue : value.significand ≠ 0) : Numerics.RationalBinary.compareDyadicScaled? false numerator denominator exponent value = some Ordering.eq ↔ scaledRatToReal numerator denominator exponent = value.toReal

Nonnegative scaled-rational comparison returns .eq exactly for real equality.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.compareDyadicScaled?_false_eq_gt_iff (numerator denominator : ℕ) (exponent : ℤ) (value : Numerics.Dyadic) (hdenominator : denominator ≠ 0) (hvalueSign : value.negative = false) (hvalue : value.significand ≠ 0) : Numerics.RationalBinary.compareDyadicScaled? false numerator denominator exponent value = some Ordering.gt ↔ value.toReal < scaledRatToReal numerator denominator exponent

Nonnegative scaled-rational comparison returns .gt exactly for reverse strict real order.