Proof-indexed binary-interchange values

Erased proof views refine one executable Model fmt by its encoded interpretation or numerical value. AtExact preserves the complete encoded interpretation, AtValue records the general numerical value, and At is the finite real specialization. These are refinement views, not additional runtime representations.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue (fmt : FloatFormat) (v : Numerics.NumericalValue ℝ) : Type

An executable float bundled with a proof of its complete numerical interpretation.

This is a refinement view, not a second floating-point representation.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.At (fmt : FloatFormat) (r : ℝ) : Type

An executable float bundled with a proof of its finite real interpretation.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.toNumericalValue (value : ExactValue) (encoding : FloatFormat.Encoding := FloatFormat.Encoding.ieee) : Numerics.NumericalValue ℝ

Forget encoding distinctions and retain the general numerical-system interpretation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNumericalValue_eq_exactValue_toNumericalValue {fmt : FloatFormat} (x : Model fmt) : x.toNumericalValue = x.exactValue.toNumericalValue fmt.encoding

Forgetting exact encoding distinctions agrees with the numerical-system interpretation.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.exactSemantics (fmt : FloatFormat) : Numerics.ExactSemantics (numericalSystem fmt)

The richer exact interpretation of Model and its coherent forgetting map.

Only proof APIs use it. Executable kernels call exactValue, field decoders, and arithmetic functions themselves.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact (fmt : FloatFormat) (v : ExactValue) : Type

An executable float bundled with a proof of its complete exact interpretation.

This is the generic exact proof view specialized to Model. It keeps signed zero and complete NaN metadata and carries one runtime Model fmt.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.OutcomeAt (fmt : FloatFormat) (v : ExactValue) (status : Numerics.IEEEStatus) : Type

An IEEE outcome bundled with proofs of both its complete value and its exception status.

The outcome is the runtime data. Only the two indexing equalities are erased.