Counts of nonempty calls in the finite pruned recursion

Main results

• Pruned.calls_irrel: the call trace depends only on the requests, not the encoded values.
• Pruned.card_calls_le_totalSize_add_one: requested-set cardinalities pay for every call, with one extra root for the empty-query boundary.

These are combinatorial facts about the existing finite trace. They do not assign an instruction cost to the recursion. Native execution bounds must separately charge their actual instructions.

References

The trace is from [AlmanWilliams2026, Section 2.4.2] and Anthropic's formal-math revision 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, pinned source.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.childSet_empty {n : ℕ} (lam : Term) : childSet ∅ lam = ∅

An empty request set has no child requests.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.calls_irrel {n : ℕ} (a b a' b' : Leaf n → ℤ) (S : Finset (OutStr n)) : calls n a b S = calls n a' b' S

Values of the two encoded arrays do not affect which calls are made.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.card_calls_succ {n : ℕ} (a b : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) : (calls (n + 1) a b S).card = 1 + ∑ lam : Term, if (childSet S lam).Nonempty then (calls n (sliceAt a lam) (sliceAt b lam) (childSet S lam)).card else 0

One root call and all nonempty child traces, counted with their multiplicities.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.totalSize_succ {n : ℕ} (a b : Leaf (n + 1) → ℤ) (S : Finset (OutStr (n + 1))) : totalSize a b S = S.card + ∑ lam : Term, if (childSet S lam).Nonempty then totalSize (sliceAt a lam) (sliceAt b lam) (childSet S lam) else 0

The passed-set total is the root size plus the totals of its nonempty children.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.card_calls_le_totalSize {n : ℕ} (a b : Leaf n → ℤ) (S : Finset (OutStr n)) (hS : S.Nonempty) : (calls n a b S).card ≤ totalSize a b S

A nonempty call carries at least one query, so the passed-set total pays for every call.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.card_calls_empty {n : ℕ} (a b : Leaf n → ℤ) : (calls n a b ∅).card = 1

Empty requests make only the root call, including at zero depth.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.card_calls_le_totalSize_add_one {n : ℕ} (a b : Leaf n → ℤ) (S : Finset (OutStr n)) : (calls n a b S).card ≤ totalSize a b S + 1

Every call is paid for by a requested-set element, except possibly an empty root.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.totalSize_irrel {n : ℕ} (a b a' b' : Leaf n → ℤ) (S : Finset (OutStr n)) : totalSize a b S = totalSize a' b' S

Encoded values do not affect the total size of the request sets.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Pruned.card_calls_add_one_le {n : ℕ} (a b : Leaf n → ℤ) (S : Finset (OutStr n)) : (calls n a b S).card + 1 ≤ 2 * 10 ^ n

Even without pruning, a ten-way depth-n tree has fewer than twice 10^n nodes. This ordinary count supplies a word-size bound for native timestamp generations.