Strict cyclic tau-value product for two tensor factors

Proved

mme_cyclic_kron_two_strict_below_product

by marwahaha · Sep 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-complexityasymptotic-spectrumcoppersmith-winogradmatrix-multiplicationtensor-product

Let A and B be three-tensors over a field. If the cyclic symmetrization of A has every nonnegative tau-value strictly below a positive endpoint A0, and that of B has every nonnegative tau-value strictly below a positive endpoint B0, then the cyclic symmetrization of A tensor B has every nonnegative tau-value strictly below A0 B0. This is the two-factor strict product rule used to assemble the coupled and matrix-multiplication factors in the Phi233 constituents.

Preamble

import Mathlib.Tactic
import Theorems.Thm_mme_cyclic_kronFin_multiplicities_of_each_strict_below_product
import Theorems.Thm_mme_cyclicSymmetrization_mono_restrict
import Theorems.Thm_mme_HasTauValueAtLeast_mono_restrict
import Theorems.Thm_mme_toQ_kronFin

open MME BigOperators

universe u

set_option autoImplicit false

Formal statement

theorem mme_cyclic_kron_two_strict_below_product
    {K : Type u} [Field K]
    (A B : TensorObj K 3) (tau endpointA endpointB : ℝ)
    (hendpointA : 0 < endpointA) (hendpointB : 0 < endpointB)
    (hA : ∀ V : ℝ, 0 ≤ V → V < endpointA →
      HasTauValueAtLeast (cyclicSymmetrization A) tau V)
    (hB : ∀ V : ℝ, 0 ≤ V → V < endpointB →
      HasTauValueAtLeast (cyclicSymmetrization B) tau V)
    (V : ℝ) (hV : 0 ≤ V) (hVlt : V < endpointA * endpointB) :
    HasTauValueAtLeast
      (cyclicSymmetrization (TensorObj.kron A B)) tau V := by
  sorry

Source

Standard multiplicativity of asymptotic tensor value under tensor product, in the strict-below formulation used by the laser-method constituent analysis.

View graph