Shape and entry refinement for mixed-precision matrix multiplication

Successful matmul execution produces exactly one row per left input row and one entry per right input column. Every output entry is the corresponding executable dotSequential. For IEEE encodings with finite inputs, intermediate values, and results, dotSequential_abs_error_le_budget supplies its numerical error bound.

def FloatLib.Floats.Formats.BinaryInterchange.Model.MatmulRefines (p : SitePolicy) (A B : Matrix p.storage) (C : Matrix p.output) : Prop

Shape and entry contract for a successful mixed-precision matrix product.

The entry equation preserves the implementation's left-to-right dot-product order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.matmul_refines (p : SitePolicy) (A B : Matrix p.storage) (C : Matrix p.output) (hresult : matmul p A B = Except.ok C) : MatmulRefines p A B C

Every successful mixed-precision matrix multiplication satisfies its shape and entry contract.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.matmul_entry_abs_error_le_budget (p : SitePolicy) (A B : Matrix p.storage) (C : Matrix p.output) (hmatmul : matmul p A B = Except.ok C) (i : ℕ) (hi : i < Array.size A) (j : ℕ) (hj : j < ncols B) (hstorage : p.storage.isIEEE = true) (hproduct : p.product.isIEEE = true) (haccumulator : p.accumulator.isIEEE = true) (houtput : p.output.isIEEE = true) (hfinite : ∀ k < A[i]!.size, MulAccFinite p A[i]![k]! (column B j)[k]! (sequentialAccumulator p A[i]! (column B j) k)) (haccFinite : (sequentialAccumulator p A[i]! (column B j) A[i]!.size).isFinite = true) (hresultFinite : C[i]![j]!.isFinite = true) : |C[i]![j]!.toReal - sequentialDotReal p A[i]! (column B j) A[i]!.size| ≤ epsilonAt p.output (sequentialAccumulator p A[i]! (column B j) A[i]!.size).toReal + sequentialErrorBudget p A[i]! (column B j) A[i]!.size

The sequential-dot budget bounds a selected entry of a successful matrix product, under the dot theorem's IEEE-encoding and local finiteness hypotheses.