mme_laser_value_lower_bound

The abstract laser-method lower bound.

Given an order-3 tensor $T : \mathrm{TensorObj}\, K\, 3$ with a $t$-grading $G$, a cyclically-symmetric support pattern $S \subseteq (\mathrm{Fin}\,t)^3$, and the structural hypothesis that $T.t$'s rank-one expansion uses only type-triples in $S$ (TensorObj.LaserAlignedSupport), the subrank capacity of $T$ is bounded below by the closed-form laser value formula:

In particular, for any real $V > 1$ with $V \leq \mathrm{laserValueFormula}\,G\,S$, we have $V \leq \widetilde V(T)$, which then plugs into the abstract Strassen bridge mme_omega_le_of_subrank_capacity to yield an ω-bound.

Proof outline (Coppersmith–Winograd 1990 §5–§7, Wigderson–Zuiddam §6):

1. Tensor-power block decomposition. $T^{\otimes 2N}$ splits as a sum of block tensors $T_{IJK}$ indexed by triples $(I, J, K) \in (\mathrm{Fin}\,t)^{2N} \times \cdots$; each $T_{IJK}$ corresponds to a fixed type-triple statistic.

2. Block ≅ matrix-multiplication. Each non-zero $T_{IJK}$ is, up to permutation, a matrix-multiplication tensor $\langle a, b, c\rangle$ of explicit multinomial dimensions determined by the type-multiplicity statistics of $(I, J, K)$ and the grading class dimensions.

3. Salem–Spencer indexing. Restrict block indices to a 3-AP-free set $S \subseteq [N]$ (Behrend 1946; Mathlib.Combinatorics.Additive.AP.Three.Behrend.roth_lower_bound). Combined with LaserSymmetric, this kills all collisions between surviving blocks — the sum-of-blocks becomes a direct sum.

4. Counting + optimization. Stirling/multinomial bounds on the number of surviving blocks plus their dimensions, optimized over probability distributions on $S$ (via the constraint that marginals match), yield the closed-form laserValueFormula lower bound.

Reusability — the central pillar. This theorem is the single most reusable node in the matrix-multiplication-exponent program. Every subsequent ω-bound paper (Stothers 2010 $< 2.3737$, Vassilevska Williams 2012 $< 2.3727$, Le Gall 2014 $< 2.3729$, Alman–VW 2020 $< 2.3729$) instantiates this exact theorem with its own choice of tensor, grading, and support pattern; only the closed-form value-formula lower bound differs across the papers. Future agents formalising any of these improvements will reuse mme_laser_value_lower_bound verbatim.

Status. Open. Decomposes in Layer 3 into the four steps above as separate first-class theorem nodes.