The alphabets and coefficient forms of Schönhage's tensor

Seven left variables, seven right variables, ten output variables and ten multiplication terms are represented explicitly. Indices start at zero. Linear forms are coefficient functions over integers; no arithmetic operation is treated as a native machine instruction.

Main definitions

• LeftVar, RightVar, OutVar, Term: the four finite alphabets.
• phi, psi, chi: the left, right and output coefficient forms.
• Term.Contributes: occurrence in an output form.

Main results

• card_leftVar, card_rightVar, card_term: alphabet sizes.
• Term.contributes_iff, chi_eq_ite: output incidence and its coefficient.

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.

inductive Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar : Type

Left input coordinates: three x coordinates and a two-by-two family of p coordinates.

• x (i : Fin 3) : LeftVar
• p (i j : Fin 2) : LeftVar

def Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqLeftVar.decEq (x✝ x✝¹ : LeftVar) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqLeftVar : DecidableEq LeftVar

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instFintypeLeftVar : Fintype LeftVar

inductive Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar : Type

Right input coordinates: three y coordinates and a two-by-two family of q coordinates.

• y (j : Fin 3) : RightVar
• q (i j : Fin 2) : RightVar

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqRightVar : DecidableEq RightVar

def Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqRightVar.decEq (x✝ x✝¹ : RightVar) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instFintypeRightVar : Fintype RightVar

inductive Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar : Type

Output coordinates comprise a three-by-three outer family and one distinguished inner coordinate.

• z (i j : Fin 3) : OutVar
• z0 : OutVar

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqOutVar : DecidableEq OutVar

def Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqOutVar.decEq (x✝ x✝¹ : OutVar) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instFintypeOutVar : Fintype OutVar

inductive Cslib.Algorithms.MatrixMultiplication.Schonhage.Term : Type

The multiplication labels consist of nine indexed labels P i j and the additional label P0.

• P (i j : Fin 3) : Term
• P0 : Term

def Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqTerm.decEq (x✝ x✝¹ : Term) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instDecidableEqTerm : DecidableEq Term

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.instFintypeTerm : Fintype Term

def Cslib.Algorithms.MatrixMultiplication.Schonhage.xForm (i : Fin 3) : LeftVar → ℤ

The linear form consisting of the single left variable x_i.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.pForm (i j : Fin 2) : LeftVar → ℤ

The linear form consisting of the single left variable p_ij.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.yForm (j : Fin 3) : RightVar → ℤ

The linear form consisting of the single right variable y_j.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.qForm (i j : Fin 2) : RightVar → ℤ

The linear form consisting of the single right variable q_ij.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.zForm (i j : Fin 3) : OutVar → ℤ

The linear form consisting of the single output variable z_ij.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.z0Form : OutVar → ℤ

The linear form consisting of the single output variable z₀.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.pHat : Matrix (Fin 3) (Fin 3) (LeftVar → ℤ)

Extend the two-by-two p family to three rows by cancelling each column sum; the third column is zero.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.qHat : Matrix (Fin 3) (Fin 3) (RightVar → ℤ)

Extend the two-by-two q family to three columns by cancelling each row sum; the third row is zero.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.phi : Term → LeftVar → ℤ

Left coefficients for each multiplication label. An indexed label adds its x coordinate to the corresponding pHat form; P0 negates the sum of the three x coordinates.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.psi : Term → RightVar → ℤ

Right coefficients for each multiplication label. Indexed labels use y plus qHat, whereas P0 uses the sum of the three y coordinates.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.chi : Term → OutVar → ℤ

Output coefficients: each indexed label occurs in its own outer coordinate and in z0; P0 occurs only in z0.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.IsInner : OutVar → Prop

Select the distinguished output coordinate, excluding the indexed outer coordinates.

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.instDecidablePredIsInner : DecidablePred IsInner

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.Contributes (lam : Term) (z : OutVar) : Prop

A label is relevant to an output coordinate when its output coefficient is nonzero.

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.instDecidableContributes (lam : Term) (z : OutVar) : Decidable (lam.Contributes z)

def Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.privateTerm : OutVar → Term

Choose the indexed label for an outer coordinate and P0 for the inner coordinate. Applying this choice coordinatewise defines a private leaf.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftStr (L : ℕ) : Type

A length-L tuple of left coordinates, indexed from zero.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.RightStr (L : ℕ) : Type

A length-L tuple with entries in RightVar.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.OutStr (L : ℕ) : Type

A length-L tuple with entries in OutVar.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.Vertex (k : ℕ) : Type

The sequence of multiplication labels identifying a depth-k recursion vertex.

@[reducible, inline]

abbrev Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf (L : ℕ) : Type

A terminal vertex, whose label sequence has the full recursion depth.

The alphabets

def Cslib.Algorithms.MatrixMultiplication.Schonhage.LeftVar.equiv : LeftVar ≃ Fin 3 ⊕ Fin 2 × Fin 2

The left variables, listed: x i is .inl i, and p i j is .inr (i, j).

def Cslib.Algorithms.MatrixMultiplication.Schonhage.RightVar.equiv : RightVar ≃ Fin 3 ⊕ Fin 2 × Fin 2

The right variables, listed: y j is .inl j, and q i j is .inr (i, j).

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.equiv : Term ≃ Option (Fin 3 × Fin 3)

The terms, listed: P i j is some (i, j), and P0 is none.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leftVar : Fintype.card LeftVar = 7

The left alphabet has cardinality seven.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_rightVar : Fintype.card RightVar = 7

The right alphabet has cardinality seven.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_term : Fintype.card Term = 10

There are ten multiplication labels.

Which terms contribute to which output variables

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.contributes_z0 (lam : Term) : lam.Contributes OutVar.z0

The inner coordinate receives a contribution from every multiplication label.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.contributes_z_iff (lam : Term) (i j : Fin 3) : lam.Contributes (OutVar.z i j) ↔ lam = P i j

For an outer coordinate, relevance determines both indices of the multiplication label.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.contributes_iff (lam : Term) (z : OutVar) : lam.Contributes z ↔ z.IsInner ∨ lam = z.privateTerm

Relevance has two possibilities: the output is inner, or the label is the private label selected by that output.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Term.sum_contributes {A : Type u_1} [AddCommMonoid A] (c : Term → A) (z : OutVar) : ∑ lam : Term with lam.Contributes z, c lam = match z with | OutVar.z i j => c (P i j) | OutVar.z0 => ∑ lam : Term, c lam

Separate decoding into its two cases: an outer output selects one summand; the inner output sums the whole label family.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.chi_eq_ite (lam : Term) (z : OutVar) : chi lam z = if lam.Contributes z then 1 else 0

Each output coefficient is the zero-or-one indicator of Term.Contributes.