Exact values represented by binary models

Model.ExactValue records the complete interpretation of an executable bit pattern without introducing another floating-point carrier. Finite values retain their exact dyadic decoding, so positive and negative zero remain distinct when the format represents both. Infinities retain their sign, and NaNs retain their sign, signaling class, and fraction payload.

inductive FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue : Type

Complete exact interpretation of a Model bit pattern.

• finite (value : Numerics.Dyadic) : ExactValue

  A finite exact dyadic, including the sign of zero.

• infinity (sign : Bool) : ExactValue

  A signed infinity.

• nan (sign signaling : Bool) (payload : ℕ) : ExactValue

  A NaN with its sign, signaling class, and complete fraction field.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprExactValue : Repr ExactValue

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprExactValue.repr : ExactValue → ℕ → Std.Format

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqExactValue.decEq (x✝ x✝¹ : ExactValue) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqExactValue : DecidableEq ExactValue

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue {fmt : FloatFormat} (x : Model fmt) : ExactValue

Decode an executable bit pattern to its complete exact value.

This function is computational. It refines the real-valued numerical interpretation by retaining the distinctions that ℝ necessarily forgets.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_eq_finite_of_toDyadic?_eq_some {fmt : FloatFormat} {x : Model fmt} {value : Numerics.Dyadic} (hvalue : x.toDyadic? = some value) : x.exactValue = ExactValue.finite value

A successful dyadic decoding determines the exact finite value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactValue_eq_finite_iff {fmt : FloatFormat} {x : Model fmt} {value : Numerics.Dyadic} : x.exactValue = ExactValue.finite value ↔ x.toDyadic? = some value

Exact finiteness is equivalent to successful decoding with the indexed dyadic.