Prove2Me

Tensor-specific Salem--Spencer assembly for the coupled q=6q=6 constituent

Proved
mme_CW_q6_coupled_tensor_extraction_below_raw_of_pruning

by marwahaha · Aug 24, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycoppersmith-winograddirect-sumlaser-methodmatrix-multiplicationsalem-spencertensor-restriction

Fix τ\tau with 3τ≥23\tau\ge2 and a nonnegative base

V<4 63τ(63τ+2).V<4\,6^{3\tau}(6^{3\tau}+2).

For a sufficiently large NN, put L=⌊2N/(63τ+2)⌋L=\lfloor2N/(6^{3\tau}+2)\rfloor and G=N−LG=N-L. Assume the elementary type-count and pruning certificate

L>0,L+G=N,341L<100G.L>0,\qquad L+G=N,\qquad 341L<100G.

Then the Salem--Spencer hashing, collision pruning, and coupled-block assembly produce a finite family of matrix-multiplication tensors with a concrete restriction

⨁i⟨aN,i,bN,i,cN,i⟩  ≤Restrict  (D6⊗π(D6)⊗π2(D6))⊗2N\bigoplus_i\langle a_{N,i},b_{N,i},c_{N,i}\rangle \;\leq_{\mathrm{Restrict}}\; \bigl(D_6\otimes\pi(D_6)\otimes\pi^2(D_6)\bigr)^{\otimes2N}

and weighted volume

V2N≤∑i(aN,ibN,icN,i)τ.V^{2N}\le\sum_i(a_{N,i}b_{N,i}c_{N,i})^{\tau}.

This theorem is the tensor-specific core of CW90 journal pp. 270--272 after the independent floor-rounding argument has been removed. Its proof should instantiate the already formalized Salem--Spencer existence theorem and 3AP collision lemma, then construct the actual mode restrictions and direct sum. The strict sub-bound absorbs all subexponential counting losses.

Preamble
import Mathlib.Analysis.SpecificLimits.Basic
import Definitions.Def_mme_CW_coupled_value
open MME BigOperators Filter
universe u
Formal statement
theorem mme_CW_q6_coupled_tensor_extraction_below_raw_of_pruning
    {K : Type u} [Field K]
    (tau : ℝ) (htau : 2 ≤ 3 * tau)
    (V : ℝ) (hV : 0 ≤ V)
    (hVlt :
      V < 4 * (6 : ℝ) ^ (3 * tau) *
        ((6 : ℝ) ^ (3 * tau) + 2)) :
    ∀ᶠ N : ℕ in atTop,
      let lambda : ℝ := 2 / ((6 : ℝ) ^ (3 * tau) + 2)
      let L : ℕ := ⌊lambda * (N : ℝ)⌋₊
      let G : ℕ := N - L
      (0 < L ∧ L + G = N ∧ 341 * L < 100 * G) →
      ∃ (k : ℕ) (a b c : Fin k → ℕ),
        TensorObj.Restrict
          (TensorObj.bigAdd (fun i => MMObj K (a i) (b i) (c i)))
          ((cyclicSymmetrization (coupledObj K 6)).kronPow (2 * N)) ∧
        V ^ (2 * N) ≤
          ∑ i, (((a i * b i * c i : ℕ) : ℝ) ^ tau) := by sorry
Source
D. Coppersmith and S. Winograd, Matrix Multiplication via Arithmetic Progressions, Journal of Symbolic Computation 9 (1990), coupled-constituent proof on journal pp. 270--272 (PDF pp. 20--22), especially the 2N-th power, Salem--Spencer hashing, shared-block pruning, C-tensor assembly, and weighted-volume estimate; https://www.sciencedirect.com/science/article/pii/S0747717108800132

View graph