Orders and counts of contributing leaves

Main definitions

• order, alpha, beta: leaf order and its two counting distributions.

Main results

• card_contributing_of_order, card_filter_order_eq, card_outStr_of_leaf: exact counts.
• two_pow_mul_beta_le: geometric decay when L = 19m.

References

Adapted selectively from [AlmanWilliams2026, Section 2] and Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. These are finite mathematical counts and identities; they give no native program or instruction-cost certificate.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.P0Levels {L : ℕ} (τ : Leaf L) : Finset (Fin L)

The set of levels at which a leaf chooses P₀.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.order {L : ℕ} (m : ℕ) (τ : Leaf L) : ℤ

The integer difference between m and the number of P0 positions of a leaf. It can be negative for arbitrary leaves; nonnegativity is proved for leaves contributing to an output with m inner positions.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.alpha (m d : ℕ) : ℕ

The quantity m.choose d * 9 ^ d, counting order-d leaves contributing to one output with m inner positions.

def Cslib.Algorithms.MatrixMultiplication.Schonhage.beta (L m d : ℕ) : ℕ

The quantity L.choose (m - d) * 9 ^ (L - m + d), using natural-number subtraction. Its interpretation as the number of order-d leaves requires d ≤ m ≤ L.

One level: which terms contribute to which variables

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.OutVar.privateTerm_eq_P0_iff (z : OutVar) : z.privateTerm = Term.P0 ↔ z.IsInner

The private term of z is P₀ exactly if z = z₀.

The order of a leaf

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_P0Levels {L : ℕ} {τ : Leaf L} {ℓ : Fin L} : ℓ ∈ P0Levels τ ↔ τ ℓ = Term.P0

Membership in the set of levels at which a leaf chooses P₀.

@[simp]

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.mem_innerSetO {L : ℕ} {η : OutStr L} {ℓ : Fin L} : ℓ ∈ innerSetO η ↔ (η ℓ).IsInner

Membership in the inner set of an output string.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.P0Levels_subset {L : ℕ} {τ : Leaf L} {w : OutStr L} (h : τ.Contributes w) : P0Levels τ ⊆ innerSetO w

A contributing leaf can use P0 only at an inner position of the output string.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.order_nonneg {L m : ℕ} {w : OutStr L} (hw : (innerSetO w).card = m) {τ : Leaf L} (h : τ.Contributes w) : 0 ≤ order m τ

A leaf contributing to a string with exactly m inner positions has nonnegative order relative to m.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.order_le {L : ℕ} (m : ℕ) (τ : Leaf L) : order m τ ≤ ↑m

The order relative to m of any leaf is at most m, regardless of which outputs it contributes to.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.order_eq_iff {L : ℕ} (m d : ℕ) (τ : Leaf L) : order m τ = ↑d ↔ (P0Levels τ).card + d = m

A leaf has order d exactly if it chooses P₀ at m - d levels.

The counts

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_filter_contributes {L m : ℕ} (w : OutStr L) (hw : (innerSetO w).card = m) : {τ : Leaf L | τ.Contributes w}.card = 10 ^ m

Exactly 10 ^ m leaves contribute to an output string with m inner positions.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_contributing_of_order {L m : ℕ} (w : OutStr L) (hw : (innerSetO w).card = m) (d : ℕ) : {τ : Leaf L | τ.Contributes w ∧ order m τ = ↑d}.card = alpha m d

For a string with m inner positions, alpha m d leaves of order d contribute to it. The natural parameter d is unrestricted; for d > m both sides are zero.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_filter_order_eq {L m : ℕ} (hmL : m ≤ L) (d : ℕ) (hd : d ≤ m) : {τ : Leaf L | order m τ = ↑d}.card = beta L m d

If d ≤ m ≤ L, the full leaf index type contains exactly beta L m d leaves of order d.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.beta_zero (L m : ℕ) : beta L m 0 = L.choose m * 9 ^ (L - m)

Evaluate beta at order zero.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.beta_zero_eq_M (L m : ℕ) : beta L m 0 = M L m

The order-zero count formula equals M L m.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_outStr_of_leaf {L m : ℕ} (hmL : m ≤ L) (d : ℕ) (τ : Leaf L) (hτ : order m τ = ↑d) : {w : OutStr L | (innerSetO w).card = m ∧ τ.Contributes w}.card = (L - m + d).choose d

Assuming m ≤ L, a leaf of natural order d contributes to exactly (L - m + d).choose d output strings with m inner positions. The order hypothesis forces d ≤ m.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.beta_pos {L m : ℕ} (hmL : m ≤ L) (d : ℕ) : 0 < beta L m d

β_d is positive when m ≤ L.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.Equation5.ratio_nat {L m : ℕ} (hmL : m ≤ L) (d : ℕ) (hd1 : 1 ≤ d) (hd : d ≤ m) : beta L m d * (L - m + d) = 9 * (m - d + 1) * beta L m (d - 1)

For 1 ≤ d ≤ m ≤ L, consecutive values of beta satisfy the displayed multiplication identity, without division (cf. [AlmanWilliams2026, equation (5)]).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.beta_ratio {L m : ℕ} (hmL : m ≤ L) (d : ℕ) (hd1 : 1 ≤ d) (hd : d ≤ m) : ↑(beta L m d) / ↑(beta L m (d - 1)) = 9 * (↑m - ↑d + 1) / (↑L - ↑m + ↑d)

For 1 ≤ d ≤ m ≤ L, the ratio of consecutive beta values is 9 * (m - d + 1) / (L - m + d), with the ratio and subtractions interpreted in ℚ. This extends the parameter ranges used in [AlmanWilliams2026, equations (5) and (7)].

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.beta_ratio_lt_half (m d : ℕ) (hd1 : 1 ≤ d) (hd : d ≤ m) : ↑(beta (19 * m) m d) / ↑(beta (19 * m) m (d - 1)) ≤ 9 * ↑m / (18 * ↑m + 1) ∧ 9 * ↑m / (18 * ↑m + 1) < 1 / 2

At L = 19 * m and 1 ≤ d ≤ m, the ratio of consecutive beta values is bounded above by 9 * m / (18 * m + 1), which is strictly below 1 / 2. All divisions here are in ℚ.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.two_pow_mul_beta_le (m d : ℕ) (hd : d ≤ m) : 2 ^ d * beta (19 * m) m d ≤ M (19 * m) m

For d ≤ m and L = 19 * m, the order count satisfies 2 ^ d * beta L m d ≤ M L m. This is the division-free geometric bound from [AlmanWilliams2026, equation (5)].