Strassen Polynomial-Matrix Product Correctness

Correctness proofs for the Strassen-style polynomial-matrix products in CompPoly.LinearAlgebra.PolynomialMatrix.Operations:

• rowGet_rowMulMatrixWith: entry semantics of the naive row-by-matrix product.
• mulBoundedWith_eq_mulWith: the degree-capped low-product reconstruction equals the naive product.
• mulStrassenWith_eq_mulWith and mulStrassenWithFuel_eq_mulWith: the Strassen recursion computes exactly the naive matrix product, as arrays.
• mulTruncColumnStrassenWith_eq_truncateColumns and mulTruncColumnStrassenWith_entry: the column-truncated Strassen recursion computes exactly the column-truncated naive product.

Generic array and fold helpers

theorem CompPoly.PolynomialMatrix.le_nextPowerOfTwoAtLeast (target : ℕ) : target ≤ nextPowerOfTwoAtLeast target

nextPowerOfTwoAtLeast is at least its target.

theorem CompPoly.PolynomialMatrix.natArraySlice_getD (values : Array ℕ) (start count j : ℕ) : (natArraySlice values start count).getD j 0 = if j < count then values.getD (start + j) 0 else 0

Entry access for natArraySlice.

theorem CompPoly.PolynomialMatrix.maxNatArrays_getD (a b : Array ℕ) (j : ℕ) : (maxNatArrays a b).getD j 0 = max (a.getD j 0) (b.getD j 0)

Entry access for maxNatArrays.

Row access helpers

theorem CompPoly.PolynomialMatrix.rowGet_of_size_le {F : Type u_1} [Zero F] {row : PolynomialRow F} {j : ℕ} (hj : Array.size row ≤ j) : rowGet row j = 0

Reading a row past its width yields zero.

truncateX algebra

theorem CompPoly.PolynomialMatrix.truncateX_zero {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (order : ℕ) : truncateX order 0 = 0

Truncation of the zero polynomial.

theorem CompPoly.PolynomialMatrix.truncateX_add {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (order : ℕ) (p q : CPolynomial F) : truncateX order (p + q) = truncateX order p + truncateX order q

Truncation distributes over addition.

theorem CompPoly.PolynomialMatrix.truncateX_sub {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (order : ℕ) (p q : CPolynomial F) : truncateX order (p - q) = truncateX order p - truncateX order q

Truncation distributes over subtraction.

theorem CompPoly.PolynomialMatrix.truncateX_truncateX {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (o o' : ℕ) (p : CPolynomial F) : truncateX o (truncateX o' p) = truncateX (min o o') p

Nested truncations keep the smaller order.

theorem CompPoly.PolynomialMatrix.truncateX_sum {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (order n : ℕ) (f : ℕ → CPolynomial F) : truncateX order (∑ k ∈ Finset.range n, f k) = ∑ k ∈ Finset.range n, truncateX order (f k)

Truncation distributes over finite range sums.

theorem CompPoly.PolynomialMatrix.truncateX_mul_of_productCoeffCap_le {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] {p q : CPolynomial F} {order : ℕ} (h : productCoeffCap p q ≤ order) : truncateX order (p * q) = p * q

A product is unchanged by truncation past its coefficient cap.

ofFn access toolkit

theorem CompPoly.PolynomialMatrix.ofFn_size {F : Type u_1} [Zero F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) : Array.size (ofFn rows width entry) = rows

Row count of ofFn.

theorem CompPoly.PolynomialMatrix.getD_ofFn {F : Type u_1} [Zero F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) (i : ℕ) : Array.getD (ofFn rows width entry) i #[] = if i < rows then (List.map (entry i) (List.range width)).toArray else #[]

Row access for ofFn with zero defaults.

theorem CompPoly.PolynomialMatrix.rowGet_ofFn {F : Type u_1} [Zero F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) (i j : ℕ) : rowGet (Array.getD (ofFn rows width entry) i #[]) j = if i < rows ∧ j < width then entry i j else 0

Entry access for ofFn with zero defaults.

theorem CompPoly.PolynomialMatrix.MatrixWidth_ofFn {F : Type u_1} [Zero F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) : (ofFn rows width entry).MatrixWidth = if rows = 0 then 0 else width

Width of ofFn.

theorem CompPoly.PolynomialMatrix.MatrixWidth_ofFn_square {F : Type u_1} [Zero F] (n : ℕ) (entry : ℕ → ℕ → CPolynomial F) : (ofFn n n entry).MatrixWidth = n

Width of a square ofFn.

theorem CompPoly.PolynomialMatrix.ofFn_congr {F : Type u_1} [Zero F] {rows width : ℕ} {f g : ℕ → ℕ → CPolynomial F} (h : ∀ i < rows, ∀ j < width, f i j = g i j) : ofFn rows width f = ofFn rows width g

Two ofFn matrices with entrywise-equal in-range entries are equal.

Naive product semantics

theorem CompPoly.PolynomialMatrix.rowMulMatrixWith_size {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) : Array.size (rowMulMatrixWith mulCtx row M) = M.MatrixWidth

Width of a naive row-by-matrix product.

theorem CompPoly.PolynomialMatrix.rowGet_rowMulMatrixWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) {j : ℕ} (hj : j < M.MatrixWidth) : rowGet (rowMulMatrixWith mulCtx row M) j = ∑ k ∈ Finset.range (Array.size row), rowGet row k * rowGet (Array.getD M k #[]) j

Entry semantics of the naive row-by-matrix product.

theorem CompPoly.PolynomialMatrix.rowGet_rowMulMatrixWith_of_width_le {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) {j : ℕ} (hj : M.MatrixWidth ≤ j) : rowGet (rowMulMatrixWith mulCtx row M) j = 0

The naive row-by-matrix product is zero past the matrix width.

theorem CompPoly.PolynomialMatrix.mulWith_eq_ofFn {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (A B : PolynomialMatrix F) : mulWith mulCtx A B = ofFn (Array.size A) B.MatrixWidth fun (i j : ℕ) => ∑ k ∈ Finset.range (Array.size B), rowGet (Array.getD A i #[]) k * rowGet (Array.getD B k #[]) j

The naive matrix product as an ofFn matrix of convolution sums.

theorem CompPoly.PolynomialMatrix.mulWith_size {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (A B : PolynomialMatrix F) : Array.size (mulWith mulCtx A B) = Array.size A

Row count of the naive matrix product.

theorem CompPoly.PolynomialMatrix.mulWith_getD {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (A B : PolynomialMatrix F) {i : ℕ} (hi : i < Array.size A) : Array.getD (mulWith mulCtx A B) i #[] = rowMulMatrixWith mulCtx (Array.getD A i #[]) B

Rows of the naive matrix product.

theorem CompPoly.PolynomialMatrix.matrixRows_mulWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (A B : PolynomialMatrix F) : (mulWith mulCtx A B).MatrixRows = List.map (fun (row : PolynomialRow F) => rowMulMatrixWith mulCtx row B) A.MatrixRows

Row list of the naive matrix product.

Bounded product correctness

theorem CompPoly.PolynomialMatrix.rowMulMatrixBoundedWith_eq_rowMulMatrixWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (row : PolynomialRow F) (M : PolynomialMatrix F) : rowMulMatrixBoundedWith lowCtx row M = rowMulMatrixWith lowCtx.mulContext row M

The degree-capped row product equals the naive row product.

theorem CompPoly.PolynomialMatrix.mulBoundedWith_eq_mulWith {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (A B : PolynomialMatrix F) : mulBoundedWith lowCtx A B = mulWith lowCtx.mulContext A B

The degree-capped matrix product equals the naive matrix product.

Column-truncated naive product semantics

theorem CompPoly.PolynomialMatrix.rowGet_rowTruncateColumns {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (row : PolynomialRow F) (j : ℕ) : rowGet (rowTruncateColumns orders row) j = truncateX (orders.getD j 0) (rowGet row j)

Entry access for column truncation of a row.

theorem CompPoly.PolynomialMatrix.truncateColumns_size {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (M : PolynomialMatrix F) : Array.size (truncateColumns orders M) = Array.size M

Row count of a column-truncated matrix.

theorem CompPoly.PolynomialMatrix.truncateColumns_getD {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (M : PolynomialMatrix F) {i : ℕ} (hi : i < Array.size M) : Array.getD (truncateColumns orders M) i #[] = rowTruncateColumns orders (Array.getD M i #[])

Rows of a column-truncated matrix.

theorem CompPoly.PolynomialMatrix.rowMulMatrixTruncColumnWith_eq {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (orders : Array ℕ) (row : PolynomialRow F) (M : PolynomialMatrix F) : rowMulMatrixTruncColumnWith lowCtx orders row M = rowTruncateColumns orders (rowMulMatrixWith lowCtx.mulContext row M)

The truncated row product is the truncation of the naive row product.

theorem CompPoly.PolynomialMatrix.mulTruncColumnWith_eq {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (orders : Array ℕ) (A B : PolynomialMatrix F) : mulTruncColumnWith lowCtx orders A B = truncateColumns orders (mulWith lowCtx.mulContext A B)

The column-truncated product is the truncation of the naive product.

Structural ofFn rewrites for the block combinators

theorem CompPoly.PolynomialMatrix.add_ofFn {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (rows width : ℕ) (f g : ℕ → ℕ → CPolynomial F) : (ofFn rows width f).add (ofFn rows width g) = ofFn rows width fun (i j : ℕ) => f i j + g i j

Pointwise addition of equally shaped ofFn matrices.

theorem CompPoly.PolynomialMatrix.sub_ofFn {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (rows width : ℕ) (f g : ℕ → ℕ → CPolynomial F) : (ofFn rows width f).sub (ofFn rows width g) = ofFn rows width fun (i j : ℕ) => f i j - g i j

Pointwise subtraction of equally shaped ofFn matrices.

theorem CompPoly.PolynomialMatrix.mulWith_ofFn_ofFn {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (n : ℕ) (f g : ℕ → ℕ → CPolynomial F) : mulWith mulCtx (ofFn n n f) (ofFn n n g) = ofFn n n fun (i j : ℕ) => ∑ k ∈ Finset.range n, f i k * g k j

The naive product of square ofFn matrices.

theorem CompPoly.PolynomialMatrix.truncateColumns_ofFn {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] (orders : Array ℕ) (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) : truncateColumns orders (ofFn rows width entry) = ofFn rows width fun (i j : ℕ) => truncateX (orders.getD j 0) (entry i j)

Column truncation of an ofFn matrix.

Strassen seven-product sum identities

Padding step

Full Strassen correctness

theorem CompPoly.PolynomialMatrix.mulStrassenWithFuel_eq_mulWith {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff fuel : ℕ) (A B : PolynomialMatrix F) : mulStrassenWithFuel lowCtx leafCutoff fuel A B = mulWith lowCtx.mulContext A B

The fuel-bounded Strassen product equals the naive matrix product.

theorem CompPoly.PolynomialMatrix.mulStrassenWith_eq_mulWith {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (A B : PolynomialMatrix F) : mulStrassenWith lowCtx leafCutoff A B = mulWith lowCtx.mulContext A B

The Strassen product equals the naive matrix product.

theorem CompPoly.PolynomialMatrix.mulStrassenWith_size {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (A B : PolynomialMatrix F) : Array.size (mulStrassenWith lowCtx leafCutoff A B) = Array.size A

Row count of the Strassen product.

theorem CompPoly.PolynomialMatrix.mulStrassenWith_getD {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (A B : PolynomialMatrix F) {i : ℕ} (hi : i < Array.size A) : Array.getD (mulStrassenWith lowCtx leafCutoff A B) i #[] = rowMulMatrixWith lowCtx.mulContext (Array.getD A i #[]) B

Rows of the Strassen product are the naive row-by-matrix products.

theorem CompPoly.PolynomialMatrix.matrixRows_mulStrassenWith {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (A B : PolynomialMatrix F) : (mulStrassenWith lowCtx leafCutoff A B).MatrixRows = List.map (fun (row : PolynomialRow F) => rowMulMatrixWith lowCtx.mulContext row B) A.MatrixRows

Row list of the Strassen product.

Column-truncated Strassen correctness

theorem CompPoly.PolynomialMatrix.mulTruncColumnStrassenWithFuel_eq_truncateColumns {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff fuel : ℕ) (orders : Array ℕ) (A B : PolynomialMatrix F) : mulTruncColumnStrassenWithFuel lowCtx leafCutoff fuel orders A B = truncateColumns orders (mulWith lowCtx.mulContext A B)

The fuel-bounded column-truncated Strassen product equals the column-truncated naive matrix product.

theorem CompPoly.PolynomialMatrix.mulTruncColumnStrassenWith_eq_truncateColumns {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (orders : Array ℕ) (A B : PolynomialMatrix F) : mulTruncColumnStrassenWith lowCtx leafCutoff orders A B = truncateColumns orders (mulWith lowCtx.mulContext A B)

The column-truncated Strassen product equals the column-truncated naive matrix product.

theorem CompPoly.PolynomialMatrix.mulTruncColumnStrassenWith_size {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (orders : Array ℕ) (A B : PolynomialMatrix F) : Array.size (mulTruncColumnStrassenWith lowCtx leafCutoff orders A B) = Array.size A

Row count of the column-truncated Strassen product.

theorem CompPoly.PolynomialMatrix.mulTruncColumnStrassenWith_entry {F : Type u_1} [Ring F] [BEq F] [LawfulBEq F] (lowCtx : MulLowContext F) (leafCutoff : ℕ) (orders : Array ℕ) (A B : PolynomialMatrix F) {i : ℕ} (hi : i < Array.size A) (j : ℕ) : rowGet (Array.getD (mulTruncColumnStrassenWith lowCtx leafCutoff orders A B) i #[]) j = truncateX (orders.getD j 0) (rowGet (rowMulMatrixWith lowCtx.mulContext (Array.getD A i #[]) B) j)

Entries of the column-truncated Strassen product are the order-truncated naive product entries.