Batch correctness of the tensor product

Main results

• bilinearProduct_arrays_eq_mul: exact integer matrix multiplication at selected strings.
• batch_product_spec: arbitrary output strings with m inner levels.

The batch arrays vanish on strings with the wrong number of inner positions. The coefficient rules select equal inner indices and the specified outer row and column, yielding the usual product of integer matrices.

References

Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. These are finite mathematical counts and identities; they give no native program or instruction-cost certificate.

Cardinalities of index types

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_outerStr (L m : ℕ) : Fintype.card (OuterStr L m) = N0 L m

The outer-index type has N0 L m elements.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_innerStr (m : ℕ) : Fintype.card (InnerStr m) = D m

The inner-index type has D m elements.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_subsets_eq_K (L m : ℕ) : {Q : Finset (Fin L) | Q.card = m}.card = K L m

There are K L m subsets of Fin L with cardinality m.

The input arrays

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.arrayL_leftStrOf {L m : ℕ} (X : Finset (Fin L) → LeftMat L m) (Q : Finset (Fin L)) (hQ : Q.card = m) (r : OuterStr L m) (π : InnerStr m) : arrayL m X (leftStrOf Q hQ r π) = X Q r π

The entry of the left input array at the string with inner set Q, outer part r and inner part π is X_Q[r, π].

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.arrayR_rightStrOf {L m : ℕ} (Y : Finset (Fin L) → RightMat L m) (Q : Finset (Fin L)) (hQ : Q.card = m) (π : InnerStr m) (c : OuterStr L m) : arrayR m Y (rightStrOf Q hQ π c) = Y Q π c

The entry of the right input array at the string with inner set Q, inner part π and outer part c is Y_Q[π, c].

Coefficients and batch correctness

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.coefficient_z0 (s : LeftVar) (t : RightVar) : coefficient s t OutVar.z0 = if ∃ (i : Fin 2) (j : Fin 2), s = LeftVar.p i j ∧ t = RightVar.q i j then 1 else 0

The inner-output coefficient selects equal inner index pairs (Section 2.3.3). Checked directly on coefficient; no polynomial coefficient bridge is assumed.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.coefficient_x_y_z (i' j' i j : Fin 3) : coefficient (LeftVar.x i') (RightVar.y j') (OutVar.z i j) = if i' = i ∧ j' = j then 1 else 0

With two outer inputs, the outer-output coefficient selects exactly the matching row and column (Section 2.3.3).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bilinearProduct_arrays_eq_mul {L m : ℕ} (X : Finset (Fin L) → LeftMat L m) (Y : Finset (Fin L) → RightMat L m) (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) : bilinearProduct (arrayL m X) (arrayR m Y) (outStrOf Q hQ r c) = (X Q * Y Q) r c

At the output string for a size-m set Q and indices r, c, the bilinear product of the batch arrays equals (X Q * Y Q) r c. The matrices have arbitrary integer entries (cf. [AlmanWilliams2026, Lemma 9]).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.batch_product_spec {L m : ℕ} (X : Finset (Fin L) → LeftMat L m) (Y : Finset (Fin L) → RightMat L m) (w : OutStr L) (h : (innerSetO w).card = m) : bilinearProduct (arrayL m X) (arrayR m Y) w = (X (innerSetO w) * Y (innerSetO w)) (rowO w h) (colO w h)

An output string with exactly m inner levels selects the product of the two matrices indexed by its inner set, at its extracted row and column. This is an equality of integer values for the arrays arrayL m X and arrayR m Y (cf. [AlmanWilliams2026, Lemma 9]).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.arrays_eq_mul {L m : ℕ} (X : Finset (Fin L) → LeftMat L m) (Y : Finset (Fin L) → RightMat L m) (Q : Finset (Fin L)) (hQ : Q.card = m) (r c : OuterStr L m) : result L (arrayL m X) (arrayR m Y) (outStrOf Q hQ r c) = (X Q * Y Q) r c

Full.result on the batch arrays agrees with the matrix product for every size-m set Q and every row and column index.