Exact policy-aware numerical systems

The adapter interprets every finite FP8, FP6, FP4, FNUZ, or IEEE code as an exact dyadic. It uses the complete FloatFormat, so an all-ones exponent can mean infinity, a finite value, or part of a NaN encoding according to the selected representation policy. A NaN is denoted by its fraction field, the same payload convention as ExactValue.nan and the real-valued numericalSystem.

def FloatLib.Floats.Formats.BinaryInterchange.Model.exactNumericalSystem (fmt : FloatFormat) : Numerics.NumericalSystem

Exact numerical-system semantics for a policy-aware binary format.

Finite codes denote their exact dyadic value, infinities carry their sign, and a NaN carries its fraction field as payload.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.ExactAtFinite (fmt : FloatFormat) (value : Numerics.Dyadic) : Type

A policy-aware binary word with an erased proof of its exact finite dyadic value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactNumericalSystem_represents_iff {fmt : FloatFormat} (x : Model fmt) (value : Numerics.Dyadic) : (exactNumericalSystem fmt).Represents x value ↔ x.toDyadic? = some value

Exact decoding is precisely finite representation in the general interface.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toDyadic?_eq_some_of_exactRepresents {fmt : FloatFormat} {x : Model fmt} {value : Numerics.Dyadic} (hvalue : (exactNumericalSystem fmt).Represents x value) : x.toDyadic? = some value

A represented finite value is exactly the result of decoding its code.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactRepresents_of_toDyadic?_eq_some {fmt : FloatFormat} {x : Model fmt} {value : Numerics.Dyadic} (hdecode : x.toDyadic? = some value) : (exactNumericalSystem fmt).Represents x value

Successful finite decoding establishes representation in the general interface.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exactNumericalSystem_ne_infinity_of_nonIEEE {fmt : FloatFormat} (hfmt : fmt.encoding ≠ FloatFormat.Encoding.ieee) (x : Model fmt) (sign : Bool) : (exactNumericalSystem fmt).denote x ≠ Numerics.NumericalValue.infinity sign

Non-IEEE binary encodings never denote infinity in the general interface.