Sub-base cyclic value of the coupled constituent at every q
Provedmme_CW_coupled_raw_cyclic_value_belowEvery base strictly below is a -value of the cyclic symmetrisation of the coupled Coppersmith--Winograd constituent, for every .
Formally: for , and ,
This is obtained from the even-power extractions of mme_CW_coupled_tensor_extraction_below_raw together with the admissibility of the floor profile (mme_CW_coupled_floor_pruning), fed into mme_HasTauValueAtLeast_of_cofinal_finite_extractions along the cofinal subsequence with zero error.
Why the sub-base form. The platform's HasTauValueAtLeast T tau V requires, for each fixed , infinitely many with an extraction achieving — a loss that does not depend on . The laser construction only delivers , and eventually falls below any fixed . So the sharp base is not reachable this way, while every is, because decays exponentially and therefore swallows the sub-exponential loss. This is why every value theorem along the successful route is stated in _below form.
General- form of mme_CW_q6_coupled_raw_cyclic_value_below.
import Definitions.Def_mme_CW_coupled_value open MME universe u
theorem mme_CW_coupled_raw_cyclic_value_below
{K : Type u} [Field K] (q : ℕ) (hq : 3 ≤ q)
(tau : ℝ) (htau : 2 ≤ 3 * tau)
(V : ℝ) (hV : 0 ≤ V)
(hVlt :
V < 4 * (q : ℝ) ^ (3 * tau) *
((q : ℝ) ^ (3 * tau) + 2)) :
HasTauValueAtLeast (cyclicSymmetrization (coupledObj K q)) tau V := by
sorry