mme_laser_value_lower_bound_wz
DisprovedAbstract laser-method bound — REAL-formula version (suffix _wz). Replaces mme_laser_value_lower_bound which is stated against the placeholder laserValueFormula := 1 (poisoned chain). For any 3-tensor T with grading G and cyclic-symmetric laser-aligned support pattern S, the Wigderson-Zuiddam laser value functional bounds the subrank capacity from below: laserValueFormula_wz G S ≤ subrankCapacity T. The proof (CW 1990 §5-§7 / WZ §6) constructs Salem-Spencer-indexed restrictions of T^{⊗N}, identifies blocks as MM tensors of multinomial dimensions, and optimizes over probability distributions on S. This is the SINGLE MOST REUSABLE node in the matrix-multiplication-exponent program — every subsequent ω-bound paper (Stothers, VW, Le Gall, Alman-VW) instantiates it with its own (T, G, S). See REPORT_placeholder_issue.md.
import Definitions.Def_mme_laser_value_formula_wz import Definitions.Def_mme_laser_pattern import Definitions.Def_mme_subrank_capacity open MME universe u
theorem mme_laser_value_lower_bound_wz {K : Type u} [Field K] {T : TensorObj K 3} {t : ℕ} (G : T.TypeGrading t) (S : Finset (Fin t × Fin t × Fin t)) (_hSym : LaserSymmetric S) (_hsupport : TensorObj.LaserAlignedSupport G S) : laserValueFormula_wz G S ≤ subrankCapacity T := by sorry