Sparse query bounds

Main definitions

• saving: the factor D^(-1/18) for D = 4^m.

Main results

• card_leaves_le_sum_min: sum the two order-wise bounds.
• card_leaves_le_saving: explicit sparse leaf bound, with no assumed sparse solver.

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.

Specialization to L = 19 * m

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.N0_nineteen_mul (m : ℕ) : N0 (19 * m) m = 3 ^ (18 * m)

At L = 19 * m, the outer dimension is 3 ^ (18 * m).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.M_pos {L m : ℕ} (hmL : m ≤ L) : 0 < M L m

M is positive when m ≤ L.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.two_pow_eq_sqrt_D (m : ℕ) : 2 ^ m = √↑(D m)

The real square root of D m is 2 ^ m.

noncomputable def Cslib.Algorithms.MatrixMultiplication.Schonhage.saving (m : ℕ) : ℝ

The positive real factor 2 ^ (-m / 9), used in the finite leaf and encoding count bounds.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.saving_pos (m : ℕ) : 0 < saving m

2^{-m/9} is positive.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.saving_le_one (m : ℕ) : saving m ≤ 1

2^{-m/9} ≤ 1.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.saving_mul_two_rpow (m : ℕ) : saving m * 2 ^ (↑m / 9) = 1

2^{-m/9} · 2^{m/9} = 1.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.saving_eq_D_rpow (m : ℕ) : saving m = ↑(D m) ^ (-(1 / 18))

Express saving m as the real power D^(-1/18) for D = D m.

The first inequality

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leaves_filter_order_le {L m : ℕ} (U : Finset (OutStr L)) (hU : ∀ w ∈ U, (innerSetO w).card = m) (d : ℕ) : {τ ∈ leaves U | order m τ = ↑d}.card ≤ min (U.card * alpha m d) (beta L m d)

If every string in U has m inner positions, its contributing leaves of natural order d are bounded both by U.card * alpha m d and by beta L m d. The minimum combines these bounds without counting a shared leaf more than once.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leaves_le_sum_min {L m : ℕ} (U : Finset (OutStr L)) (hU : ∀ w ∈ U, (innerSetO w).card = m) : (leaves U).card ≤ ∑ d ∈ Finset.range (m + 1), min (U.card * alpha m d) (beta L m d)

Bound the cardinality of leaves U by summing the smaller of the per-output bound and the full leaf count over natural orders 0 through m. Every string in U must have exactly m inner positions; the empty set is permitted (cf. [AlmanWilliams2026, Lemma 11]).

The second inequality

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_beta_large_orders_lt (m : ℕ) : ↑(∑ d ∈ Finset.range (m + 1) with m < 9 * d, beta (19 * m) m d) < 2 * saving m * ↑(M (19 * m) m)

At L = 19 * m, the sum of beta L m d over 0 ≤ d ≤ m with m < 9 * d is strictly below 2 * saving m * M L m. This includes m = 0, when the sum is empty.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sum_alpha_small_orders_lt (m : ℕ) (hm : 1 ≤ m) : ↑(∑ d ∈ Finset.range (m + 1) with 9 * d ≤ m, alpha m d) < 2 ^ m * saving m

For m ≥ 1, the sum of alpha m d over 0 ≤ d ≤ m with 9 * d ≤ m is strictly below 2 ^ m * saving m. For m = 0, the two quantities are equal, so the strict inequality needs the stated positivity hypothesis.

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.card_leaves_le_saving {m : ℕ} (U : Finset (OutStr (19 * m))) (hU : ∀ w ∈ U, (innerSetO w).card = m) : ↑(leaves U).card ≤ saving m * (2 ^ m * ↑U.card + 2 * ↑(M (19 * m) m))

For strings of length 19 * m, each with m inner positions, the contributing leaf set has cardinality at most saving m * (2 ^ m * U.card + 2 * M (19 * m) m). This real bound permits m = 0 and U = ∅; it makes no execution-cost claim (cf. [AlmanWilliams2026, Lemma 11]).

theorem Cslib.Algorithms.MatrixMultiplication.Schonhage.sparse_leaf_bounds {L m : ℕ} (U : Finset (OutStr L)) (hU : ∀ w ∈ U, (innerSetO w).card = m) : (leaves U).card ≤ ∑ d ∈ Finset.range (m + 1), min (U.card * alpha m d) (beta L m d) ∧ (L = 19 * m → ↑(leaves U).card ≤ 2 ^ (-↑m / 9) * (2 ^ m * ↑U.card + 2 * ↑(M L m)))

Combine the order-wise minimum bound on leaves U with the explicit real bound available when L = 19 * m. Both conclusions assume only that each requested string has m inner positions; the specialization is conditional on the displayed equality of parameters.