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 is intentionally independent of any arithmetic operation. Addition, multiplication, FMA, conversion, and directed rounding can all share the same exact domain and 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.cmpDyadic (a b : Numerics.Dyadic) : Ordering

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

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

@[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; no fixed-width constants are used.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.ieeeToDyadicImpl? {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.toDyadic_eq_toDyadicImpl : @ieeeToDyadic? = @ieeeToDyadicImpl?

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