Exact dyadic decoding primitives

Finite binary interchange values decode exactly to a sign, natural significand, and integral power-of-two exponent. This module defines that bridge and the exact comparison used by arithmetic, conversions, and rounding.

The decoding layer depends on no arithmetic operation, so addition, multiplication, FMA, conversion, and directed rounding share the same exact domain and each prove their own final packing step.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.negDyadic (fmt : FloatFormat) (value : Numerics.Dyadic) : Numerics.Dyadic

Exact negation with the zero convention selected by the destination format.

def FloatLib.Floats.Formats.BinaryInterchange.Model.unpackedToDyadic? : Float.Model.UnpackedFloat → Option Numerics.Dyadic

Exact dyadic value represented by a finite value in Lean's logical float model.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.pow2 (k : ℕ) : ℕ

2^k as a Nat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.pow2_eq_two_pow (k : ℕ) : pow2 k = 2 ^ k

The executable shift definition of a power of two agrees with natural exponentiation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadicAligned (a b : Numerics.Dyadic) : Ordering

Exact comparison of two dyadics by aligning their exponents and comparing signed mantissas.

The alignment shift is the full exponent difference, so this form is only cheap when the exponents are close. cmpDyadic decides every other case first and uses this form only when the leading bit positions coincide.

def FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic (a b : Numerics.Dyadic) : Ordering

Exact comparison of two dyadics.

Zero operands and opposite signs are decided directly. For nonzero operands of one sign, the leading bit positions log2 significand + exponent decide the magnitude order unless they coincide, and only then are the significands aligned. The alignment shift is therefore bounded by the significand widths, not by the distance between the exponents.

This lives with the decoding primitives because finite-value comparison does not depend on any rounding operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_eq_cmpDyadicAligned (a b : Numerics.Dyadic) : cmpDyadic a b = cmpDyadicAligned a b

The leading-position comparison agrees with exponent alignment for every operand pair.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cmpDyadic_swap (a b : Numerics.Dyadic) : (cmpDyadic a b).swap = cmpDyadic b a

Exchanging the operands of the exact comparison reverses its result.

Both operands are aligned to the same smaller exponent whichever comes first, so the aligned form reduces this to Int.compare_swap.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadic? {fmt : FloatFormat} (x : Model fmt) : Option Numerics.Dyadic

Decode an IEEE bit pattern into an exact dyadic.

• NaN / Inf → none
• ±0 → mant = 0, exp = 0 (sign preserved)
• subnormal → mant = frac, exp = ieeeMinSubnormalExponent fmt
• normal → mant = 2^fracWidth + frac, exp = e_biased - (bias + fracWidth)

Every threshold is derived from fmt, and no fixed-width constants are used.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Internal.ieeeToDyadic? {fmt : FloatFormat} (x : Model fmt) : Option Numerics.Dyadic

Compiled IEEE finite decoder.

The storage word is converted to Nat once, then all three fields are extracted from that shared value. The exponent field alone determines whether an IEEE encoding is exceptional, so the decoder also avoids the repeated masks and shifts performed by IEEE.isNaN and IEEE.isInf.

@[csimp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadic_eq_internal : @ieeeToDyadic? = @Internal.ieeeToDyadic?

The compiler uses the single-pass field decoder while proofs keep ieeeToDyadic?.