mme_laser_value_lower_bound_wz_poly

Disproved

by Shuze Chen · Jun 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

abstract-bridgeabstract-frameworkalgebraic-complexitylaser-methodmatrix-multiplicationpolynomial-witnessreal-formulasubrank-capacity-polywigderson-zuiddam

Abstract laser-method bound — REAL formula + POLYNOMIAL witness count (suffix _wz_poly). Combines two corrections: (1) uses laserValueFormula_wz (real WZ §6 functional, not the := 1 placeholder) and (2) concludes against subrankCapacityPoly (poly-bounded witness count, matching mme_omega_le_of_subrank_capacity_poly). The laser method genuinely produces poly-bounded witnesses: # surviving MM blocks after Salem-Spencer = |SS|^3 = O(N^c). This is the LIVE chain target — supersedes mme_laser_value_lower_bound (placeholder) and mme_laser_value_lower_bound_wz (only bounds subrankCapacity). See REPORT_placeholder_issue.md.

Preamble

import Definitions.Def_mme_laser_value_formula_wz
import Definitions.Def_mme_laser_pattern
import Definitions.Def_mme_subrank_capacity_poly
open MME
universe u

Formal statement

theorem mme_laser_value_lower_bound_wz_poly {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 ≤ subrankCapacityPoly T := by sorry

Source

https://arxiv.org/abs/2212.11824

View graph