Mixed-singleton maps equal source-family maps pointwise
Provedmme_dwz_step1FilteredMixedSingletonMaps_eq_sourceFamily_applyasymmetric-hashingmap-normal-formmatrix-multiplicationmixed-owner
At each of the three tensor modes, the mixed-owner Step-1 singleton map is exactly the corresponding ordinary source-family map, with the surviving Z-word singleton inserted in mode two.
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_step1FilteredMixedSingletonMaps_eq_sourceFamily_apply
{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))
(i : Fin 3) :
step1FilteredMixedSingletonMaps K m reindex q edge
competitor owner W i =
step1MixedSourceFamilySingletonMaps K m reindex q edge
competitor owner W i := by
sorrySource
Duan--Wu--Zhou, Faster Matrix Multiplication via Asymmetric Hashing, arXiv:2210.10173v5, Section 6, Additional Zeroing-Out Steps 1 and 2; https://arxiv.org/abs/2210.10173