Exact decoding and destination quantization of standard MX blocks

Finite lane decoding is exact multiplication by the shared power of two. Saturating block quantization minimizes each lane's absolute error among all finite words at the selected scale. The result applies at subnormal and binade boundaries as well as outside the element range.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.Standard.scaleFinite_value (exponent : ℤ) (value : Numerics.SignedRat) : (scaleFinite exponent value).value = value.value * 2 ^ exponent

Exact rational meaning of scaling a finite lane.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.Standard.scaleFinite_negative (exponent : ℤ) (value : Numerics.SignedRat) : (scaleFinite exponent value).negative = value.negative

A positive power-of-two scale preserves the sign, including the sign of zero.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.ofArray?_eq_none_iff {profile : Profile} (scale : E8M0) (values : Array (Element profile)) : ofArray? scale values = none ↔ values.size ≠ 32

A zero-length or otherwise malformed array cannot become a standard block.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane_of_nan_scale {profile : Profile} (block : Block profile) (lane : Fin 32) (hscale : block.scale.exponent? = none) : block.decodeLane lane = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

A NaN shared scale overrides every element, including finite words and infinities.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane_finite {profile : Profile} (block : Block profile) (lane : Fin 32) {exponent : ℤ} {value : Numerics.SignedRat} (hscale : block.scale.exponent? = some exponent) (hvalue : block.values[↑lane].decode = Numerics.NumericalValue.finite value) : block.decodeLane lane = Numerics.NumericalValue.finite (scaleFinite exponent value)

Finite lane decoding is exact multiplication, without binary32 range truncation.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane_infinity {profile : Profile} (block : Block profile) (lane : Fin 32) {exponent : ℤ} {negative : Bool} (hscale : block.scale.exponent? = some exponent) (hvalue : block.values[↑lane].decode = Numerics.NumericalValue.infinity negative) : block.decodeLane lane = Numerics.NumericalValue.infinity negative

A finite shared scale preserves an element infinity and its sign.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane_exceptional {profile : Profile} (block : Block profile) (lane : Fin 32) {exponent : ℤ} {exceptional : Numerics.ExceptionalValue} (hscale : block.scale.exponent? = some exponent) (hvalue : block.values[↑lane].decode = Numerics.NumericalValue.exceptional exceptional) : block.decodeLane lane = Numerics.NumericalValue.exceptional exceptional

A finite shared scale preserves a lane-local NaN without changing adjacent lanes.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeFinite_of_decode {profile : Profile} (block : Block profile) (values : Vector Numerics.SignedRat 32) (h : block.decode = Vector.map Numerics.NumericalValue.finite values) : block.decodeFinite = Numerics.NumericalValue.finite values

The generic decoder retains every lane when the block has a finite vector observation.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Block.decodeLane_value {profile : Profile} (block : Block profile) (lane : Fin 32) {exponent : ℤ} {value : ℚ} (hscale : block.scale.exponent? = some exponent) (hvalue : block.values[↑lane].toRat? = some value) : Option.map Numerics.SignedRat.value (block.decodeLane lane).finite? = some (value * 2 ^ exponent)

Finite numerical element values remain exact after applying a shared scale.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.Element.quantize_quantizesWith (profile : Profile) (mode : OverflowMode) (input : Numerics.SignedRat) : QuantizesWith mode input (quantize profile mode (Numerics.NumericalValue.finite input))

Both explicit element overflow modes refine their numerical contract.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.quantizeFinite_quantizes (profile : Profile) (mode : OverflowMode) (input : Vector Numerics.SignedRat 32) : Quantizes profile mode input (quantizeFinite profile mode input)

Automatic shared-scale conversion satisfies the standard destination relation.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.quantizeFinite_error_le (profile : Profile) (input : Vector Numerics.SignedRat 32) (lane : Fin 32) {exponent : ℤ} (hscale : (selectScale profile input).exponent? = some exponent) : ∃ (value : ℚ), Option.map Numerics.SignedRat.value ((quantizeFinite profile OverflowMode.saturate input).decodeLane lane).finite? = some value ∧ ∀ (other : Element profile) (otherValue : ℚ), other.toRat? = some otherValue → |value - input[↑lane].value| ≤ |otherValue * 2 ^ exponent - input[↑lane].value|

At a finite selected scale, SAT minimizes the decoded absolute error of each lane among all finite element encodings.