mme_laser_witness_at_prob_dist
DisprovedPointwise laser-method witness at a fixed probability distribution. For a t-way mode-graded 3-tensor T : TensorObj K 3 with cyclic-symmetric laser support S ⊆ (Fin t)^3 and laser-aligned grading G, and for ANY probability distribution π : (Fin t × Fin t × Fin t) → ℝ supported on S, the closed-form Wigderson-Zuiddam laser value at π,
V(π) = exp(log 2 · ( H(π) + (1/3) · Σ_σ π(σ) · log₂(d₀(σ)·d₁(σ)·d₂(σ)) ))
where H(π) = -Σ π log₂ π and dᵢ(σ) = dim_K(G.classOf i σᵢ), is bounded above by the polynomial-witness subrank capacity subrankCapacityPoly T.
This is the central new intermediate node in the decomposition of mme_laser_value_lower_bound_wz_poly. The pointwise (one π at a time) bound packages the full analytic-combinatorial chain from CW 1990 §5-§7 / WZ §6: tensor-power block decomposition (mme_graded_tensor_pow_block_decomp), Salem-Spencer indexing (mme_salem_spencer_eps_form), 3AP-free non-collision (mme_3AP_free_no_collision), MM-block dimensions (mme_block_tensor_is_matMul_kronPow_balanced), direct-sum Restrict (mme_independent_blocks_form_direct_sum_restrict_enum), and Stirling/multinomial counting (mme_laser_block_dimension_count_refined). Once the pointwise bound is available, the sup-over-distributions form laserValueFormula_wz G S ≤ subrankCapacityPoly T follows by abstract csSup_le.
Status: Open. This is the deep analytic-combinatorial leaf — every laser-method paper has this exact pointwise bound. Further decomposition into Stirling/multinomial/Hölder sub-lemmas is the next layer.
import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Mathlib.Analysis.SpecialFunctions.Log.Basic import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.LinearAlgebra.FiniteDimensional.Basic import Definitions.Def_mme_laser_pattern import Definitions.Def_mme_subrank_capacity_poly import Definitions.Def_mme_tensor_type_grading import Definitions.Def_mme_tensor_rank open MME BigOperators universe u
theorem mme_laser_witness_at_prob_dist {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) (π : (Fin t × Fin t × Fin t) → ℝ) (_hπ_supp : ∀ σ, σ ∉ S → π σ = 0) (_hπ_nn : ∀ σ, 0 ≤ π σ) (_hπ_sum : (∑ σ ∈ S, π σ) = 1) : Real.exp (Real.log 2 * ( (-(∑ σ ∈ S, π σ * (Real.log (π σ) / Real.log 2))) + (1 / 3) * (∑ σ ∈ S, π σ * (Real.log (((Module.finrank K (G.classOf 0 σ.1) : ℕ) : ℝ) * ((Module.finrank K (G.classOf 1 σ.2.1) : ℕ) : ℝ) * ((Module.finrank K (G.classOf 2 σ.2.2) : ℕ) : ℝ)) / Real.log 2)) ) ) ≤ subrankCapacityPoly T := by sorry