Pruned tensor evaluation and the calls it makes

The recursion skips children with no requested output strings, reading only precomputed leaf encodings. Its values agree with the full recursion on the requested set and vanish elsewhere. A call trace records finite recursive calls and passed sets; it is not a machine execution or an instruction counter.

The root is always called. At depth zero with an empty request set it is itself a visited leaf, although the set of contributing leaves is empty. The leaf characterization therefore requires positive depth or a nonempty request set. The value and total-set-size statements hold without that qualification.

Main definitions

• Pruned.run, Pruned.result, Pruned.calls: pruned evaluation and its call trace.
• Pruned.Visits, Pruned.totalSize: visited leaves and total size of passed sets.
• computeEncoding: recursive computation of either input encoding.

Main results

• Pruned.result_eq_piecewise_full: agreement on requested strings and zero elsewhere.
• Pruned.visits_iff_mem_leaves: exact visited-leaf characterization with the root exception.
• Pruned.totalSize_le: passed-set total bounded by depth plus one times leaf count.
• pruned_spec: all three properties together for the two input encodings.

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.sliceSet {n : ℕ} (S : Finset (OutStr (n + 1))) (z : OutVar) : Finset (OutStr n)

Retain the tails of requested tuples whose first coordinate equals z.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.childSet {n : ℕ} (S : Finset (OutStr (n + 1))) (lam : Term) : Finset (OutStr n)

The requests for a child label are the union of slices for output coordinates to which that label contributes.

structure Cslib.Algorithms.MatrixMultiplication.Schonhage.PrunedCall : Type

One mathematical call record, pairing its label-sequence position with the request set supplied there. The dependent pairs retain the two tuple lengths.

• vertex : (k : ℕ) × Vertex k

  The call depth and the terms identifying its vertex.

• passed : (n : ℕ) × Finset (OutStr n)

  The remaining string length and requested output strings.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.PrunedCall.under (lam : Term) (c : PrunedCall) : PrunedCall

Embed a child call into its parent by prepending the child label to its recorded vertex.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.run (n : ℕ) : (Leaf n → ℤ) → (Leaf n → ℤ) → Finset (OutStr n) → (OutStr n → ℤ) × Multiset PrunedCall

Evaluate requested outputs from the two supplied leaf-encoding arrays. For each term, form its child request set and recurse only when that set is nonempty. Decode the child values and set unrequested outputs to zero. The second component records recursive calls and their requested sets as a multiset. Each child receives the corresponding slices of the encoding arrays. The root call is always recorded, including at depth zero with an empty request set. These are mathematical values and call records, without a native execution cost.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result (n : ℕ) (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) : OutStr n → ℤ

Project the output values from the pruned recursion and discard the call multiset.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.calls (n : ℕ) (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) : Multiset PrunedCall

Project the multiset of call records, retaining repetitions and the root record.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.Visits {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Leaf L) : Prop

A leaf is visited when some recorded call has that full-depth vertex.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.totalSize {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) : ℕ

Add the cardinalities of the request sets carried by all call records, with multiplicity.

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

Choose the private label at every output coordinate. The resulting leaf is relevant to that output tuple and distinguishes it from every other output tuple.

Section 2.4.1: the encodings

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

Recursively apply the coefficient family c along a term string. Each level replaces the input array by a weighted sum of its first-letter slices; depth zero returns its unique entry. Choosing phi or psi computes the corresponding shared input encoding.

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

Recursive encoding agrees with the closed coefficient-product formula encodeWith.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.computeEncoding_phi {L : ℕ} (a : LeftStr L → ℤ) : computeEncoding phi L a = encodingL a

Specializing recursive encoding to phi gives the existing left-encoding array.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.computeEncoding_psi {L : ℕ} (b : RightStr L → ℤ) : computeEncoding psi L b = encodingR b

Specializing recursive encoding to psi gives the existing right-encoding array.

Section 2.4.2: the sets S_λ of step (2)

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_sliceSet {n : ℕ} (S : Finset (OutStr (n + 1))) (z : OutVar) (w' : OutStr n) : w' ∈ sliceSet S z ↔ Fin.cons z w' ∈ S

Membership in a slice of a set of output strings.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.childSet_P {n : ℕ} (S : Finset (OutStr (n + 1))) (i j : Fin 3) : childSet S (Term.P i j) = sliceSet S (OutVar.z i j) ∪ sliceSet S OutVar.z0

An indexed child combines the matching outer slice with the inner slice of the request set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.childSet_P0 {n : ℕ} (S : Finset (OutStr (n + 1))) : childSet S Term.P0 = sliceSet S OutVar.z0

The distinguished child needs only the inner slice of the request set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sliceSet_subset_childSet {n : ℕ} (S : Finset (OutStr (n + 1))) {lam : Term} {z : OutVar} (h : lam.Contributes z) : sliceSet S z ⊆ childSet S lam

Every requested suffix in a relevant output slice belongs to the corresponding child request set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_childSet {n : ℕ} {S : Finset (OutStr (n + 1))} {lam : Term} {w' : OutStr n} : w' ∈ childSet S lam ↔ ∃ w ∈ S, lam.Contributes (w 0) ∧ Fin.tail w = w'

A suffix belongs to a child request set precisely when it comes from a requested parent tuple whose leading coordinate is relevant to that child label.

Lemma 10, first claim: the values

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.childResult {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) (lam : Term) : OutStr n → ℤ

Evaluate a child on its requested suffixes, using the zero array when that child has no requests.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result_succ {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) : result (n + 1) encA encB S = S.piecewise (fun (w : OutStr (n + 1)) => match w 0 with | OutVar.z i j => childResult encA encB S (Term.P i j) (Fin.tail w) | OutVar.z0 => ∑ lam : Term, childResult encA encB S lam (Fin.tail w)) 0

Unfold the pruned values once, exposing the child arrays used for decoding.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result_succ_apply {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) (w : OutStr (n + 1)) : result (n + 1) encA encB S w = if w ∈ S then ∑ lam : Term with lam.Contributes (w 0), childResult encA encB S lam (Fin.tail w) else 0

At a requested tuple, decoding sums child values at its tail over labels relevant to its leading coordinate; every unrequested tuple has value zero.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result_eq_piecewise_sum {n : ℕ} (encA encB : Leaf n → ℤ) (S : Finset (OutStr n)) : result n encA encB S = S.piecewise (fun (w : OutStr n) => ∑ τ : Leaf n with τ.Contributes w, encA τ * encB τ) 0

For arbitrary supplied leaf arrays, the pruned result is zero off the request set and is a sum of relevant leaf products on that set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result_eq_piecewise_bilinearProduct {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (U : Finset (OutStr L)) : result L (encodingL a) (encodingR b) U = U.piecewise (bilinearProduct a b) 0

Pruning the two input encodings yields bilinearProduct on the requested strings and zero elsewhere.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.result_eq_piecewise_full {n : ℕ} (a : LeftStr n → ℤ) (b : RightStr n → ℤ) (S : Finset (OutStr n)) : result n (encodingL a) (encodingR b) S = S.piecewise (Full.result n a b) 0

Pruning precomputed input encodings agrees with full evaluation at every requested string and is zero elsewhere.

Lemma 10, second claim: the calls that are made and the sets passed to them

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

Test relevance for an initial label sequence against the matching prefix of an output tuple. Longer label sequences fail the depth condition.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Vertex.contributes_iff_leaf {L : ℕ} (τ : Leaf L) (w : OutStr L) : Contributes τ w ↔ τ.Contributes w

At full depth, vertex relevance coincides with the existing leaf-relevance predicate.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Vertex.contributes_cons {k L : ℕ} {lam : Term} {τ : Vertex k} {w : OutStr (L + 1)} : Contributes (Fin.cons lam τ) w ↔ lam.Contributes (w 0) ∧ τ.Contributes (Fin.tail w)

Decompose relevance of a nonempty vertex into relevance of its head and relevance of its tail.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.childCalls {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) (lam : Term) : Multiset PrunedCall

Obtain a child call multiset from its recursion, or the empty multiset when its request set is empty.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.calls_succ {n : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) : calls (n + 1) encA encB S = { vertex := ⟨0, Fin.elim0⟩, passed := ⟨n + 1, S⟩ } ::ₘ Finset.univ.val.bind fun (lam : Term) => Multiset.map (PrunedCall.under lam) (childCalls encA encB S lam)

Unfold call recording into the parent record and the embedded records from nonempty children.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.mem_calls_succ {n : ℕ} {encA encB : Leaf (n + 1) → ℤ} {S : Finset (OutStr (n + 1))} {c : PrunedCall} : c ∈ calls (n + 1) encA encB S ↔ c = { vertex := ⟨0, Fin.elim0⟩, passed := ⟨n + 1, S⟩ } ∨ ∃ (lam : Term), (childSet S lam).Nonempty ∧ ∃ c' ∈ calls n (sliceAt encA lam) (sliceAt encB lam) (childSet S lam), c = PrunedCall.under lam c'

Membership in the positive-depth call multiset means being the root record or an embedded call of some nonempty child.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.Called {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Vertex k) : Prop

A vertex is called when its depth and label tuple occur in the recorded call multiset.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.called_root {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Vertex 0) : Called encA encB U τ

The root is called.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.called_succ {n k : ℕ} (encA encB : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) (τ : Vertex (k + 1)) : Called encA encB S τ ↔ (childSet S (τ 0)).Nonempty ∧ Called (sliceAt encA (τ 0)) (sliceAt encB (τ 0)) (childSet S (τ 0)) (Fin.tail τ)

A non-root vertex is called exactly when its leading child has requests and the tail vertex is called within that child.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.called_iff_root_or {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (hkL : k ≤ L) (τ : Vertex k) : Called encA encB U τ ↔ k = 0 ∨ ∃ w ∈ U, τ.Contributes w

For vertices within the recursion depth, being called is equivalent to being the root or being relevant to at least one requested tuple.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.called_iff {L k : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (hk : 1 ≤ k ∨ U.Nonempty) (hkL : k ≤ L) (τ : Vertex k) : Called encA encB U τ ↔ ∃ w ∈ U, τ.Contributes w

Away from the empty-request root exception, a vertex within the recursion depth is called exactly when some requested tuple is relevant to it. The hypothesis hk admits every positive-depth vertex and also admits the root when requests are nonempty.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.depth_add_length {L : ℕ} {encA encB : Leaf L → ℤ} {U : Finset (OutStr L)} {c : PrunedCall} (hc : c ∈ calls L encA encB U) : c.vertex.fst + c.passed.fst = L

A call at depth k is passed strings of length L - k.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.IsSuffixFrom {n L : ℕ} (k : ℕ) (w' : OutStr n) (w : OutStr L) : Prop

w' is the suffix of w that is left when the first k variables are removed.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.mem_passed_iff {L : ℕ} {encA encB : Leaf L → ℤ} {U : Finset (OutStr L)} {c : PrunedCall} (hc : c ∈ calls L encA encB U) (w' : OutStr c.passed.fst) : w' ∈ c.passed.snd ↔ ∃ w ∈ U, c.vertex.snd.Contributes w ∧ IsSuffixFrom c.vertex.fst w' w

A recorded call receives exactly the suffixes of original requests relevant to its vertex. Its recorded remaining length and depth identify the suffix position.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.visits_iff_root_or_mem_leaves {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (τ : Leaf L) : Visits encA encB U τ ↔ L = 0 ∨ τ ∈ leaves U

A leaf is visited exactly when it is the zero-depth root or contributes to a request. This includes the empty request set without an exceptional hypothesis.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.visits_iff_mem_leaves {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (h : 0 < L ∨ U.Nonempty) (τ : Leaf L) : Visits encA encB U τ ↔ τ ∈ leaves U

With positive depth or nonempty requests, the visited-leaf set is exactly leaves U. The unconditional root case is given separately by Pruned.visits_iff_root_or_mem_leaves.

Lemma 10, third claim: the total size of the sets passed

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_leaves_succ {n : ℕ} {S : Finset (OutStr (n + 1))} {τ : Leaf (n + 1)} : τ ∈ leaves S ↔ Fin.tail τ ∈ leaves (childSet S (τ 0))

Membership in a positive-depth relevant-leaf set reduces to membership of the tail in the child relevant-leaf set.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leaves_succ {n : ℕ} (S : Finset (OutStr (n + 1))) : (leaves S).card = ∑ lam : Term, (leaves (childSet S lam)).card

Count relevant leaves by summing the relevant-leaf counts of all children; distinct leading labels keep these families disjoint.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.privateLeaf_injective {L : ℕ} : Function.Injective privateLeaf

Different output strings have different private leaves.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_le_card_leaves {n : ℕ} (S : Finset (OutStr n)) : S.card ≤ (leaves S).card

The private-leaf injection bounds the number of requested tuples by the number of their relevant leaves.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.sum_card_passed_le {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) (k : ℕ) : (Multiset.map (fun (c : PrunedCall) => c.passed.snd.card) (Multiset.filter (fun (c : PrunedCall) => c.vertex.fst = k) (calls L encA encB U))).sum ≤ (leaves U).card

At any fixed depth, the sum of all passed request-set cardinalities is bounded by the root request set's relevant-leaf count.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.totalSize_le {L : ℕ} (encA encB : Leaf L → ℤ) (U : Finset (OutStr L)) : totalSize encA encB U ≤ (L + 1) * (leaves U).card

The sum of the cardinalities of all passed request sets is at most (L + 1) * (leaves U).card.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.pruned_spec {L : ℕ} (a : LeftStr L → ℤ) (b : RightStr L → ℤ) (U : Finset (OutStr L)) : Pruned.result L (encodingL a) (encodingR b) U = U.piecewise (bilinearProduct a b) 0 ∧ (0 < L ∨ U.Nonempty → ∀ (τ : Leaf L), Pruned.Visits (encodingL a) (encodingR b) U τ ↔ τ ∈ leaves U) ∧ Pruned.totalSize (encodingL a) (encodingR b) U ≤ (L + 1) * (leaves U).card

Combine value correctness, the visited-leaf characterization and the passed-set cardinality bound for the two input encodings. Values and the set-size bound apply at every depth and request set. The leaf equivalence excludes the empty zero-depth root; Pruned.visits_iff_root_or_mem_leaves gives the unconditional alternative for that case.