Schönhage's ten-term polynomial identity

The ten products of linear forms equal the wanted inner/outer product polynomial plus an explicit error polynomial. This is an identity over integers in 24 formal variables. The error term is retained; it cannot be discarded for unrestricted inputs.

Main definitions

• TriPoly, formL, formR, formO: the polynomial interpretation of the forms.
• G, E: the wanted polynomial and the error polynomial.

Main results

• identity: the complete ten-term polynomial identity, including its error.

References

Part of [AlmanWilliams2026, Section 2]. Direct mathematical adaptation of Anthropic's pinned formal source. Definitions are selectively extracted from that pin's PaperStatements.lean; no machine semantics or running-time statement is imported. The docstrings below explain the local declarations in our own words.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.Var : Type

All 24 variables of the identity: the left, the right and the output variables.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.TriPoly : Type

The polynomials in which Schönhage's identity is an identity.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.polyL (s : LeftVar) : TriPoly

A left variable, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.polyR (t : RightVar) : TriPoly

A right variable, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.polyO (z : OutVar) : TriPoly

An output variable, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.formL (f : LeftVar → ℤ) : TriPoly

A linear form in the left variables, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.formR (f : RightVar → ℤ) : TriPoly

A linear form in the right variables, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.formO (f : OutVar → ℤ) : TriPoly

A linear form in the output variables, as a polynomial.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.G : TriPoly

The target polynomial combines the nine outer x-y products with the four p-q products attached to the inner coordinate.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.E : TriPoly

The error polynomial collects the additional outer-coordinate terms involving pHat or qHat. It has no inner-coordinate summand.

Linear forms as polynomials

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formL_eq_linearCombination (f : LeftVar → ℤ) : formL f = (Fintype.linearCombination ℤ polyL) f

formL is the linear map that sends the form consisting of the single variable s to the polynomial s.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formR_eq_linearCombination (f : RightVar → ℤ) : formR f = (Fintype.linearCombination ℤ polyR) f

formR is the linear map that sends the form consisting of the single variable t to the polynomial t.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formO_eq_linearCombination (f : OutVar → ℤ) : formO f = (Fintype.linearCombination ℤ polyO) f

formO is the linear map that sends the form consisting of the single variable z to the polynomial z.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formL_single (s : LeftVar) : formL (Pi.single s 1) = polyL s

The form consisting of a single left variable is that variable.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formR_single (t : RightVar) : formR (Pi.single t 1) = polyR t

The form consisting of a single right variable is that variable.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formO_single (z : OutVar) : formO (Pi.single z 1) = polyO z

The form consisting of a single output variable is that variable.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formL_phi_P (i j : Fin 3) : formL (phi (Term.P i j)) = polyL (LeftVar.x i) + formL (pHat i j)

Interpret an indexed left coefficient form as the sum of its x variable and its extended p form.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formR_psi_P (i j : Fin 3) : formR (psi (Term.P i j)) = polyR (RightVar.y j) + formR (qHat i j)

Interpret an indexed right coefficient form as the sum of its y variable and its extended q form.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formO_chi_P (i j : Fin 3) : formO (chi (Term.P i j)) = polyO (OutVar.z i j) + polyO OutVar.z0

Interpret an indexed output form as the sum of the corresponding outer variable and the inner variable.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formL_phi_P0 : formL (phi Term.P0) = -(polyL (LeftVar.x 0) + polyL (LeftVar.x 1) + polyL (LeftVar.x 2))

The distinguished left form is the negative sum of the three x polynomials.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formR_psi_P0 : formR (psi Term.P0) = polyR (RightVar.y 0) + polyR (RightVar.y 1) + polyR (RightVar.y 2)

The distinguished right form is the sum of the three y polynomials.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.formO_chi_P0 : formO (chi Term.P0) = polyO OutVar.z0

The distinguished output form denotes the inner polynomial variable alone.

Lemma 6

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.pHat_column_sum (j : Fin 3) : ∑ i : Fin 3, pHat i j = 0

Summing pHat over the row index gives the zero coefficient function.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.qHat_row_sum (i : Fin 3) : ∑ j : Fin 3, qHat i j = 0

Summing qHat over the column index gives the zero coefficient function.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_pHat_mul_qHat : ∑ i : Fin 3, ∑ j : Fin 3, formL (pHat i j) * formR (qHat i j) = ∑ i : Fin 2, ∑ j : Fin 2, polyL (LeftVar.p i j) * polyR (RightVar.q i j)

The product sum for the extended arrays reduces to the four products from their original two-by-two arrays.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.identity : ∑ lam : Term, formL (phi lam) * formR (psi lam) * formO (chi lam) = G + E

The ten products of the coefficient forms equal the wanted polynomial G plus the explicit error polynomial E.