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.

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

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.toNumericalValue : ExactValue → 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

Forgetting exact encoding distinctions agrees with the existing 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.

This capability is used only by proof-facing APIs. Executable kernels continue to call exactValue, field decoders, and arithmetic functions directly.

@[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 preserves signed zero and complete NaN metadata while retaining exactly one runtime Model fmt.

@[reducible, inline]

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

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

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