Selected Step-1 mixed-owner words have fine support
Provedmme_dwz_step1_mixed_selected_support_propertyasymmetric-hashingfine-supportmatrix-multiplicationstep-1-zeroing
The accepted X/Y word singletons selected in the mixed-owner Step-1 construction have nonzero fine square-Coppersmith--Winograd support in every coordinate whenever their filtered mixed tensor is nonzero. This is the exact support predicate consumed by the mixed singleton-cross restriction.
Preamble
import Definitions.Def_mme_dwz_step1_mixed_common_state_source_data open MME Module universe u set_option autoImplicit false open MME.DWZSourceAligned open MME.DWZGlobalCorrelated
Formal statement
theorem mme_dwz_step1_mixed_selected_support_property
{K : Type u} [Field K]
(m : ℕ) {p N L n : ℕ}
(reindex : Fin (N + 1) ≃ Fin L)
(q : (Fin (N + 2) → ZMod p) × ZMod p)
(edge : Fin n → Fin (N + 1) → Fin 15)
(competitor owner : Fin n)
(W : AddressZWord (sourceWord reindex edge owner)) :
Step1MixedSelectedSupportProperty
K m reindex q edge competitor owner W := by
sorrySource
Duan--Wu--Zhou, Faster Matrix Multiplication via Asymmetric Hashing, arXiv:2210.10173v5, Section 6, Additional Zeroing-Out Step 1 and Claim 6.2; https://arxiv.org/abs/2210.10173