Numerical contracts for OCP MX element rounding

The bounded candidate search implements a mathematical nearest-even specification over all finite element encodings. The proofs do not assume uniform spacing, and therefore cover subnormals, binade boundaries, finite saturation, and the asymmetric two's-complement endpoint.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.mem_candidates {profile : Profile} {word : Element profile} {value : ℚ} : (word, value) ∈ candidates profile ↔ word.toRat? = some value

Candidate enumeration contains exactly the finite words with their decoded rational values.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.toRat?_zero (profile : Profile) : toRat? 0#profile.width = some 0

Every concrete profile contains positive zero.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.toRat?_int8 (word : Element Profile.int8) : word.toRat? = some (↑(BitVec.toInt word) / 64)

INT8 is the two's-complement integer divided by 64, rather than a sign-magnitude encoding.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.int8_bounds (word : Element Profile.int8) : -2 ≤ ↑(BitVec.toInt word) / 64 ∧ ↑(BitVec.toInt word) / 64 ≤ 127 / 64

The chosen INT8 profile uses the complete permitted asymmetric range.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.candidates_ne_nil (profile : Profile) : candidates profile ≠ []

There is always a finite candidate, so the executable fallback is unreachable.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.quantizeFinite_quantizes (profile : Profile) (input : Numerics.SignedRat) : Quantizes input (quantizeFinite profile input)

The executable finite element conversion satisfies the nearest-even numerical contract.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.Quantizes.error_le {profile : Profile} {input : Numerics.SignedRat} {word other : Element profile} {value otherValue : ℚ} (h : Quantizes input word) (hvalue : word.toRat? = some value) (hother : other.toRat? = some otherValue) : |value - input.value| ≤ |otherValue - input.value|

No finite element word has smaller absolute error than the rounded result.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.Quantizes.exact {profile : Profile} {input : Numerics.SignedRat} {word other : Element profile} {value : ℚ} (h : Quantizes input word) (hvalue : word.toRat? = some value) (hother : other.toRat? = some input.value) : value = input.value

A representable rational is reproduced exactly, including at finite endpoints.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.Quantizes.even_of_tie {profile : Profile} {input : Numerics.SignedRat} {word other : Element profile} {value otherValue : ℚ} (h : Quantizes input word) (hvalue : word.toRat? = some value) (hother : other.toRat? = some otherValue) (htie : |value - input.value| = |otherValue - input.value|) (heven : BitVec.toNat other % 2 = 0) : BitVec.toNat word % 2 = 0

An equally close even word prevents selection of an odd word.