Admissibility of the coupled floor profile at every q
Provedmme_CW_coupled_floor_pruningalgebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication
Fix and with , and set
Then for all sufficiently large one has , , and .
Here is the fraction of the tensor positions that Coppersmith--Winograd assign to the two "low" blocks of the coupled constituent, the remaining positions carrying the two coupled blocks. The last conjunct is the margin the hashing step consumes: since and , give , the limiting ratio is at least , comfortably above . The quantitative input is mme_CW_coupled_pruning_ratio, which supplies for exactly this range of and .
This is the general- form of mme_CW_q6_coupled_exact_floor_pruning, additionally recording , which the capacity estimate needs and which does not follow from and alone (truncated subtraction allows when ).
Preamble
import Mathlib.Analysis.SpecificLimits.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real open Filter
Formal statement
theorem mme_CW_coupled_floor_pruning
(q : ℕ) (hq : 3 ≤ q) (tau : ℝ) (htau : 2 ≤ 3 * tau) :
∀ᶠ N : ℕ in atTop,
let lambda : ℝ := 2 / ((q : ℝ) ^ (3 * tau) + 2)
let L : ℕ := ⌊lambda * (N : ℝ)⌋₊
let G : ℕ := N - L
0 < L ∧ 0 < G ∧ L + G = N ∧ 341 * L < 100 * G := by
sorrySource
Don Coppersmith and Shmuel Winograd, Matrix multiplication via arithmetic progressions, Journal of Symbolic Computation 9(3), 1990, 251-280; the coupled four-sum constituent (d) on printed p. 266 and its value lemma on printed p. 270. General-q form of the q=6 chain used for omega < 2.376.