Full tensor recursion and shared encodings

The recursion works on mathematical arrays indexed by finite strings. Its multiplication record identifies the two encoded integers at each leaf. The returned array equals the bilinear tensor expansion. These recursive values and combinatorial counts carry no native instruction-cost interpretation.

Main definitions

• Full.run, Full.result, Full.multipliedAt: full evaluation and leaf operands.
• encodeLeft, encodeRight, encodingL, encodingR: shared leaf encodings.
• bilinearProduct, coefficient, leaves: the tensor expansion and contributing leaves.

Main results

• full_spec: full evaluation returns the bilinear product and uses the stated encodings.
• tensor_expansion: expansion into products of the one-level tensor coefficients.
• abs_phi_le_one, abs_psi_le_one: bounded encoding coefficients.

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.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.sliceAt {α β : Type} {L : ℕ} (a : (Fin (L + 1) → α) → β) (s : α) : (Fin L → α) → β

Fix the first coordinate of a tuple-indexed array and retain the shorter tuple as its argument. The construction works for any coordinate alphabet and value type.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeStepL {L : ℕ} (lam : Term) (a : LeftStr (L + 1) → ℤ) : LeftStr L → ℤ

Apply the left coefficient form for lam to all first-coordinate slices of the input array.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeStepR {L : ℕ} (lam : Term) (b : RightStr (L + 1) → ℤ) : RightStr L → ℤ

Apply the right coefficient form for lam to all first-coordinate slices of the input array.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.run (L : ℕ) : (LeftStr L → ℤ) → (RightStr L → ℤ) → (OutStr L → ℤ) × (Leaf L → ℤ × ℤ)

Evaluate the two arrays and retain the operands used at each leaf. At depth zero, multiply their unique entries. At positive depth, apply each term’s left and right coefficient forms, recurse, and decode the child results into an output array. The second component maps each term string to its pair of encoded input values. This is a finite integer recursion, with no instruction counter.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.result (L : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : OutStr L → ℤ

Project the output array from full evaluation, discarding its record of leaf operands.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.multipliedAt (L : ℕ) (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (τ : Leaf L) : ℤ × ℤ

Read the ordered pair of leaf operands recorded by Full.run.

2.3.2 Unraveling the recursion computation

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeLeft {L : ℕ} (τ : Leaf L) (a : LeftStr L → ℤ) : ℤ

Evaluate the left encoding at one leaf by weighting each input entry with the product of its coordinate coefficients.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeRight {L : ℕ} (τ : Leaf L) (b : RightStr L → ℤ) : ℤ

Evaluate the right encoding at one leaf using the corresponding products of right coefficients.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf.Contributes {L : ℕ} (τ : Leaf L) (w : OutStr L) : Prop

A leaf is relevant to an output tuple when its labels are relevant at every coordinate.

@[instance_reducible]

instance Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf.instDecidableContributes {L : ℕ} (τ : Leaf L) (w : OutStr L) : Decidable (τ.Contributes w)

def Cslib.Algorithms.MatrixMultiplication.Schonhage.bilinearProduct {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : OutStr L → ℤ

For each output tuple, sum the products of left and right encodings over its relevant leaves.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.coefficient (s : LeftVar) (t : RightVar) (z : OutVar) : ℤ

The coefficient linking one left, right and output coordinate, obtained by summing products of the relevant label coefficients.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodingL {L : ℕ} (a : LeftStr L → ℤ) : Leaf L → ℤ

Package all left-encoding values into an array indexed by leaves.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodingR {L : ℕ} (b : RightStr L → ℤ) : Leaf L → ℤ

Package all right-encoding values into an array indexed by leaves.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.leaves {L : ℕ} (U : Finset (OutStr L)) : Finset (Leaf L)

Take the union of the relevant-leaf sets of all requested output tuples.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leftStr (L : ℕ) : Fintype.card (LeftStr L) = 7 ^ L

Counting length-L left tuples gives 7^L.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_rightStr (L : ℕ) : Fintype.card (RightStr L) = 7 ^ L

Counting length-L right tuples gives 7^L.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_vertex (k : ℕ) : Fintype.card (Vertex k) = 10 ^ k

A depth-k label sequence has ten independent choices at each position.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_phi_le_one (lam : Term) (s : LeftVar) : |phi lam s| ≤ 1

Every left coefficient has absolute value at most one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.abs_psi_le_one (lam : Term) (t : RightVar) : |psi lam t| ≤ 1

Every right coefficient has absolute value at most one.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_support_phi_le (lam : Term) : {s : LeftVar | phi lam s ≠ 0}.card ≤ 3

The support of any left coefficient form has cardinality at most three.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_support_psi_le (lam : Term) : {t : RightVar | psi lam t ≠ 0}.card ≤ 3

The support of any right coefficient form has cardinality at most three.

Which leaves contribute to an output string

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf.contributes_succ {L : ℕ} {τ : Leaf (L + 1)} {w : OutStr (L + 1)} : τ.Contributes w ↔ (τ 0).Contributes (w 0) ∧ Contributes (Fin.tail τ) (Fin.tail w)

Split coordinatewise leaf relevance into the first label and the remaining label tuple.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf.sum_contributes_succ {L : ℕ} (w : OutStr (L + 1)) (f : Leaf (L + 1) → ℤ) : ∑ τ : Leaf (L + 1) with τ.Contributes w, f τ = ∑ lam : Term with lam.Contributes (w 0), ∑ τ' : Leaf L with τ'.Contributes (Fin.tail w), f (Fin.cons lam τ')

A sum over the leaves contributing to w, split by the first term of the leaf.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Leaf.filter_contributes_eq_piFinset {L : ℕ} (w : OutStr L) : {τ : Leaf L | τ.Contributes w} = Fintype.piFinset fun (ℓ : Fin L) => {lam : Term | lam.Contributes (w ℓ)}

The relevant-leaf filter is a product of the allowed label sets at individual coordinates.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_leaves {L : ℕ} {U : Finset (OutStr L)} {τ : Leaf L} : τ ∈ leaves U ↔ ∃ w ∈ U, τ.Contributes w

Membership in leaves(U).

The two encodings at once

def Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeWith {α : Type} [Fintype α] (c : Term → α → ℤ) {L : ℕ} (τ : Leaf L) (a : (Fin L → α) → ℤ) : ℤ

Encoding for an arbitrary coefficient family: weight each array entry by the product of coefficients selected by the leaf. This specializes to both input encodings.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeWith_zero {α : Type} [Fintype α] (c : Term → α → ℤ) (τ : Leaf 0) (a : (Fin 0 → α) → ℤ) : encodeWith c τ a = a Fin.elim0

With no coordinates, the encoding evaluates the array at its unique empty argument.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeWith_cons {α : Type} [Fintype α] (c : Term → α → ℤ) {L : ℕ} (lam : Term) (τ' : Leaf L) (a : (Fin (L + 1) → α) → ℤ) : encodeWith c (Fin.cons lam τ') a = encodeWith c τ' fun (u' : Fin L → α) => ∑ s : α, c lam s * sliceAt a s u'

Process the first label of an encoding by combining the first-coordinate slices, then encode the resulting shorter array.

Lemma 7

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeLeft_cons {L : ℕ} (lam : Term) (τ' : Leaf L) (a : LeftStr (L + 1) → ℤ) : encodeLeft (Fin.cons lam τ') a = encodeLeft τ' (encodeStepL lam a)

The left encoding at a cons leaf is the tail encoding of the array produced by encodeStepL.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.encodeRight_cons {L : ℕ} (lam : Term) (τ' : Leaf L) (b : RightStr (L + 1) → ℤ) : encodeRight (Fin.cons lam τ') b = encodeRight τ' (encodeStepR lam b)

The right encoding at a cons leaf is the tail encoding of the array produced by encodeStepR.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.multipliedAt_eq_encoding {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (τ : Leaf L) : multipliedAt L a b τ = (encodeLeft τ a, encodeRight τ b)

The operand record of full evaluation agrees with encodeLeft and encodeRight at every leaf.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.result_succ {L : ℕ} (a : LeftStr (L + 1) → ℤ) (b : RightStr (L + 1) → ℤ) (w : OutStr (L + 1)) : result (L + 1) a b w = ∑ lam : Term with lam.Contributes (w 0), result L (encodeStepL lam a) (encodeStepR lam b) (Fin.tail w)

Unfold full evaluation once and express decoding as a sum over labels relevant to the leading output coordinate.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.bilinearProduct_succ {L : ℕ} (a : LeftStr (L + 1) → ℤ) (b : RightStr (L + 1) → ℤ) (w : OutStr (L + 1)) : bilinearProduct a b w = ∑ lam : Term with lam.Contributes (w 0), bilinearProduct (encodeStepL lam a) (encodeStepR lam b) (Fin.tail w)

The bilinear product obeys the same first-coordinate decoding recurrence as full evaluation.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Full.result_eq_bilinearProduct {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : result L a b = bilinearProduct a b

Full evaluation computes the bilinear tensor expansion bilinearProduct.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.full_spec {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) : (∀ (τ : Leaf L), Full.multipliedAt L a b τ = (encodeLeft τ a, encodeRight τ b)) ∧ Full.result L a b = bilinearProduct a b

The complete value specification of full evaluation: its result is bilinearProduct, and each leaf’s operands are the corresponding left and right encodings.

Lemma 8

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.prod_gamma_eq_sum_contributes {L : ℕ} (u : LeftStr L) (v : RightStr L) (w : OutStr L) : ∏ ℓ : Fin L, coefficient (u ℓ) (v ℓ) (w ℓ) = ∑ τ : Leaf L with τ.Contributes w, (∏ ℓ : Fin L, phi (τ ℓ) (u ℓ)) * ∏ ℓ : Fin L, psi (τ ℓ) (v ℓ)

Expand the product of one-coordinate coefficients as a sum of coefficient products indexed by relevant leaves.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.tensor_expansion {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (w : OutStr L) : bilinearProduct a b w = ∑ u : LeftStr L, ∑ v : RightStr L, (∏ ℓ : Fin L, coefficient (u ℓ) (v ℓ) (w ℓ)) * a u * b v

Expand bilinearProduct as a double sum of input-entry products. The coefficient of each pair is the product, over string positions, of the one-level coefficients.