Exact rational scaling by powers of two

Binary formats repeatedly need the same small collection of exact operations: locate a positive rational between consecutive powers of two, move a binary exponent into a numerator or denominator, and compare a signed rational with a dyadic without constructing an enormous shifted integer.

These operations belong to the exact numerical layer rather than to any one floating-point format. IEEE interchange, P3109, posits, and application-defined binary quantizers may therefore share them without importing one another's encoding or exceptional-value policy.

@[inline]

def FloatLib.Numerics.RationalBinary.lessThanPowerOfTwo (numerator denominator : ℕ) (exponent : ℤ) : Bool

Test numerator / denominator < 2^exponent for a positive denominator, using integers.

@[simp]

theorem FloatLib.Numerics.RationalBinary.lessThanPowerOfTwo_ofNat (numerator denominator shift : ℕ) : lessThanPowerOfTwo numerator denominator (Int.ofNat shift) = decide (numerator < denominator.shiftLeft shift)

Nonnegative exponents shift the denominator in the strict comparison.

@[simp]

theorem FloatLib.Numerics.RationalBinary.lessThanPowerOfTwo_natCast (numerator denominator shift : ℕ) : lessThanPowerOfTwo numerator denominator ↑shift = decide (numerator < denominator.shiftLeft shift)

A natural exponent shifts the denominator in the strict comparison.

@[simp]

theorem FloatLib.Numerics.RationalBinary.lessThanPowerOfTwo_negSucc (numerator denominator shift : ℕ) : lessThanPowerOfTwo numerator denominator (Int.negSucc shift) = decide (numerator.shiftLeft (shift + 1) < denominator)

Negative exponents shift the numerator in the strict comparison.

@[inline]

def FloatLib.Numerics.RationalBinary.atLeastPowerOfTwo (numerator denominator : ℕ) (exponent : ℤ) : Bool

Test numerator / denominator ≥ 2^exponent for a positive denominator, using integers.

@[simp]

theorem FloatLib.Numerics.RationalBinary.atLeastPowerOfTwo_ofNat (numerator denominator shift : ℕ) : atLeastPowerOfTwo numerator denominator (Int.ofNat shift) = decide (numerator ≥ denominator.shiftLeft shift)

Nonnegative exponents shift the denominator in the non-strict comparison.

@[simp]

theorem FloatLib.Numerics.RationalBinary.atLeastPowerOfTwo_natCast (numerator denominator shift : ℕ) : atLeastPowerOfTwo numerator denominator ↑shift = decide (numerator ≥ denominator.shiftLeft shift)

A natural exponent shifts the denominator in the non-strict comparison.

@[simp]

theorem FloatLib.Numerics.RationalBinary.atLeastPowerOfTwo_negSucc (numerator denominator shift : ℕ) : atLeastPowerOfTwo numerator denominator (Int.negSucc shift) = decide (numerator.shiftLeft (shift + 1) ≥ denominator)

Negative exponents shift the numerator in the non-strict comparison.

@[inline]

def FloatLib.Numerics.RationalBinary.floorLog2 (numerator denominator : ℕ) : ℤ

Compute ⌊log₂(numerator / denominator)⌋.

The intended mathematical preconditions are positive numerator and denominator. Keeping the kernel total makes it convenient inside executable quantizers; proofs establish the preconditions where logarithmic bounds are used.

@[inline]

def FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo (numerator denominator : ℕ) : ℤ → ℕ × ℕ

Represent (numerator / denominator) * 2^exponent as a ratio of natural numbers.

Positive exponents shift the numerator and negative exponents shift the denominator. No division or approximation occurs.

@[simp]

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_ofNat (numerator denominator shift : ℕ) : scaleByPowerOfTwo numerator denominator (Int.ofNat shift) = (numerator.shiftLeft shift, denominator)

Scaling by a nonnegative exponent shifts only the numerator.

@[simp]

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_natCast (numerator denominator shift : ℕ) : scaleByPowerOfTwo numerator denominator ↑shift = (numerator.shiftLeft shift, denominator)

Scaling by a natural exponent shifts only the numerator.

@[simp]

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_zero (numerator denominator : ℕ) : scaleByPowerOfTwo numerator denominator 0 = (numerator, denominator)

Scaling by 2^0 leaves both sides of the exact quotient unchanged.

@[simp]

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_negSucc (numerator denominator shift : ℕ) : scaleByPowerOfTwo numerator denominator (Int.negSucc shift) = (numerator, denominator.shiftLeft (shift + 1))

Scaling by a negative exponent shifts only the denominator.

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_fst_ne_zero (numerator denominator : ℕ) (exponent : ℤ) (hnumerator : numerator ≠ 0) : (scaleByPowerOfTwo numerator denominator exponent).1 ≠ 0

A nonzero numerator remains nonzero after exact binary scaling.

theorem FloatLib.Numerics.RationalBinary.scaleByPowerOfTwo_snd_ne_zero (numerator denominator : ℕ) (exponent : ℤ) (hdenominator : denominator ≠ 0) : (scaleByPowerOfTwo numerator denominator exponent).2 ≠ 0

A nonzero denominator remains nonzero after exact binary scaling.

def FloatLib.Numerics.RationalBinary.compareDyadicScaled? (negative : Bool) (numerator denominator : ℕ) (exponent : ℤ) (value : Dyadic) : Option Ordering

Compare (numerator / denominator) * 2^exponent, with the supplied sign, against a dyadic.

A zero denominator returns none. After multiplying the denominator by the dyadic significand, a leading-position test often decides the result. Only equal leading positions require exponent alignment; that shift is then bounded by the integer operand widths.

def FloatLib.Numerics.RationalBinary.compareDyadic? (negative : Bool) (numerator denominator : ℕ) (value : Dyadic) : Option Ordering

Compare an exact signed rational with a dyadic.