Numerical correctness of exact MX dot products

The executable list reductions are related to finite sums of decoded rational products and to the factored shared-scale formula of OCP MX 1.0 §6.1. For finite input lanes and a finite binary32 result, the result is one nearest-even rounding of the exact real dot across any number of blocks. Its error is at most half an ULP, including gradual underflow; there is no accumulation error.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.sum_finite (values : List ℚ) : sum (List.map Numerics.NumericalValue.finite values) = Numerics.NumericalValue.finite values.sum

Exact finite reduction agrees with the algebraic sum, independently of cancellation.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.sum_ofFn_finite {n : ℕ} (values : Fin n → ℚ) : sum (List.ofFn fun (i : Fin n) => Numerics.NumericalValue.finite (values i)) = Numerics.NumericalValue.finite (∑ i : Fin n, values i)

An indexed finite reduction agrees with the mathematical finite sum.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.sum_eq_infinity (values : List (Numerics.NumericalValue ℚ)) (sign : Bool) (h : ∀ value ∈ values, (∃ (q : ℚ), value = Numerics.NumericalValue.finite q) ∨ value = Numerics.NumericalValue.infinity sign) (hmem : Numerics.NumericalValue.infinity sign ∈ values) : sum values = Numerics.NumericalValue.infinity sign

An infinity survives a reduction whose other terms are finite or infinities of the same sign. The hypothesis excludes both invalid products and opposite-infinity cancellation.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.toReal_roundFloat32_finite (value : ℚ) (hfinite : (roundFloat32 (Numerics.NumericalValue.finite value)).isFinite = true) : (roundFloat32 (Numerics.NumericalValue.finite value)).toReal = BinaryInterchange.Model.roundAt BinaryInterchange.FloatFormat.binary32 ↑value

The existing binary rational packer realizes the independent nearest-even real projection. Finiteness excludes overflow, where a real-valued error is not defined.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.DotProduct.sum_eq_nan_of_mem (values : List (Numerics.NumericalValue ℚ)) (h : Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan ∈ values) : sum values = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

One exceptional lane product poisons an exact reduction, regardless of its position.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_eq_nan_of_left_lane {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (lane : Fin 32) (exceptional : Numerics.ExceptionalValue) (h : left.decodeLane lane = Numerics.NumericalValue.exceptional exceptional) : dotExact left right = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

A lane-local NaN on the left propagates through multiplication and the full block sum.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_eq_nan_of_right_lane {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (lane : Fin 32) (exceptional : Numerics.ExceptionalValue) (h : right.decodeLane lane = Numerics.NumericalValue.exceptional exceptional) : dotExact left right = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

A lane-local NaN on the right also poisons the full dot.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_eq_nan_of_scale {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (h : left.scale.exponent? = none ∨ right.scale.exponent? = none) : dotExact left right = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

A NaN shared scale on either operand poisons the dot independently of element bits.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_eq_nan_of_zero_infinity {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (lane : Fin 32) (zero : Numerics.SignedRat) (sign : Bool) (hzero : zero.value = 0) (hleft : left.decodeLane lane = Numerics.NumericalValue.finite zero) (hright : right.decodeLane lane = Numerics.NumericalValue.infinity sign) : dotExact left right = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan

A zero lane multiplied by infinity is invalid even when every other product is finite.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotGeneral_eq_nan_of_block {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) (block : Fin n) (h : dotExact left[↑block] right[↑block] = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.nan) : dotGeneral left right = BinaryInterchange.Model.canonicalNaN BinaryInterchange.FloatFormat.binary32

An invalid block dot propagates to the final binary32 NaN across any number of blocks.

@[simp]

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotGeneral_empty {leftProfile rightProfile : Profile} (left : Vector (Block leftProfile) 0) (right : Vector (Block rightProfile) 0) : dotGeneral left right = BinaryInterchange.Model.posZero BinaryInterchange.FloatFormat.binary32

With no blocks there are no exceptional operands, and the result is positive zero.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_finite {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (a b : Fin 32 → Numerics.SignedRat) (ha : ∀ (i : Fin 32), left.decodeLane i = Numerics.NumericalValue.finite (a i)) (hb : ∀ (i : Fin 32), right.decodeLane i = Numerics.NumericalValue.finite (b i)) : dotExact left right = Numerics.NumericalValue.finite (∑ i : Fin 32, (a i).value * (b i).value)

Finite decoded lanes are multiplied and accumulated exactly, even when they cancel.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.toReal_dot_eq_roundAt {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (a b : Fin 32 → Numerics.SignedRat) (ha : ∀ (i : Fin 32), left.decodeLane i = Numerics.NumericalValue.finite (a i)) (hb : ∀ (i : Fin 32), right.decodeLane i = Numerics.NumericalValue.finite (b i)) (hfinite : (dot left right).isFinite = true) : (dot left right).toReal = BinaryInterchange.Model.roundAt BinaryInterchange.FloatFormat.binary32 (∑ i : Fin 32, ↑(a i).value * ↑(b i).value)

A finite one-block result is one nearest-even rounding of its exact real dot.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.abs_toReal_dot_sub_le {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (a b : Fin 32 → Numerics.SignedRat) (ha : ∀ (i : Fin 32), left.decodeLane i = Numerics.NumericalValue.finite (a i)) (hb : ∀ (i : Fin 32), right.decodeLane i = Numerics.NumericalValue.finite (b i)) (hfinite : (dot left right).isFinite = true) : |(dot left right).toReal - ∑ i : Fin 32, ↑(a i).value * ↑(b i).value| ≤ BinaryInterchange.Model.epsilonAt BinaryInterchange.FloatFormat.binary32 (∑ i : Fin 32, ↑(a i).value * ↑(b i).value)

The one-block dot also incurs only the final half-ULP rounding error.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotExact_eq_scaled_sum {leftProfile rightProfile : Profile} (left : Block leftProfile) (right : Block rightProfile) (a b : Fin 32 → Numerics.SignedRat) (leftExponent rightExponent : ℤ) (hleft : left.scale.exponent? = some leftExponent) (hright : right.scale.exponent? = some rightExponent) (ha : ∀ (i : Fin 32), left.values[↑i].decode = Numerics.NumericalValue.finite (a i)) (hb : ∀ (i : Fin 32), right.values[↑i].decode = Numerics.NumericalValue.finite (b i)) : dotExact left right = Numerics.NumericalValue.finite (2 ^ leftExponent * 2 ^ rightExponent * ∑ i : Fin 32, (a i).value * (b i).value)

The exact block reduction equals the specification's factored shared-scale expression.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.dotGeneralExact_finite {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) (a b : Fin n → Fin 32 → Numerics.SignedRat) (ha : ∀ (j : Fin n) (i : Fin 32), left[↑j].decodeLane i = Numerics.NumericalValue.finite (a j i)) (hb : ∀ (j : Fin n) (i : Fin 32), right[↑j].decodeLane i = Numerics.NumericalValue.finite (b j i)) : dotGeneralExact left right = Numerics.NumericalValue.finite (∑ j : Fin n, ∑ i : Fin 32, (a j i).value * (b j i).value)

General accumulation sums every exact lane product without intermediate rounding.

noncomputable def FloatLib.Floats.Formats.OCP.MX.Standard.realDot {n : ℕ} (a b : Fin n → Fin 32 → Numerics.SignedRat) : ℝ

Real exact dot of decoded lanes, without an intermediate representability restriction.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.toReal_dotGeneral_eq_roundAt {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) (a b : Fin n → Fin 32 → Numerics.SignedRat) (ha : ∀ (j : Fin n) (i : Fin 32), left[↑j].decodeLane i = Numerics.NumericalValue.finite (a j i)) (hb : ∀ (j : Fin n) (i : Fin 32), right[↑j].decodeLane i = Numerics.NumericalValue.finite (b j i)) (hfinite : (dotGeneral left right).isFinite = true) : (dotGeneral left right).toReal = BinaryInterchange.Model.roundAt BinaryInterchange.FloatFormat.binary32 (realDot a b)

The final finite binary32 result is one nearest-even rounding of the exact real dot.

theorem FloatLib.Floats.Formats.OCP.MX.Standard.abs_toReal_dotGeneral_sub_le {leftProfile rightProfile : Profile} {n : ℕ} (left : Vector (Block leftProfile) n) (right : Vector (Block rightProfile) n) (a b : Fin n → Fin 32 → Numerics.SignedRat) (ha : ∀ (j : Fin n) (i : Fin 32), left[↑j].decodeLane i = Numerics.NumericalValue.finite (a j i)) (hb : ∀ (j : Fin n) (i : Fin 32), right[↑j].decodeLane i = Numerics.NumericalValue.finite (b j i)) (hfinite : (dotGeneral left right).isFinite = true) : |(dotGeneral left right).toReal - realDot a b| ≤ BinaryInterchange.Model.epsilonAt BinaryInterchange.FloatFormat.binary32 (realDot a b)

Finite-result absolute error is at most half an ULP of the exact dot. This includes subnormal results and cancellation; there is no error from the number or order of finite summands.