Mixed selected full maps equal the Step-1 filtered maps

Proved

mme_dwz_step1_mixed_selected_full_maps_eq_filtered

by marwahaha · Aug 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

asymmetric-hashingmap-normal-formmatrix-multiplicationstep-1-zeroing

The full-source map family obtained by projecting to the mixed competitor-X/Y and owner-Z coarse address, selecting the chosen address words, and applying the broken-owner postmaps is exactly the existing Step-1 filtered mixed-owner X/Y map family.

Preamble

import Definitions.Def_mme_dwz_step1_mixed_selected_full_map_data

open MME Module

universe u

set_option autoImplicit false

open MME.DWZSourceAligned
open MME.DWZGlobalCorrelated

Formal statement

theorem mme_dwz_step1_mixed_selected_full_maps_eq_filtered
    {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))
    (x : AddressModeWord (sourceWord reindex edge competitor) 0)
    (y : AddressModeWord (sourceWord reindex edge competitor) 1) :
    step1MixedSelectedFullMaps K m reindex q edge
        competitor owner W x y =
      step1FilteredMixedSelectedXYMaps K m reindex q edge
        competitor owner W x y := by
  sorry

Source

Duan--Wu--Zhou, Faster Matrix Multiplication via Asymmetric Hashing, arXiv:2210.10173v5, Section 6, Additional Zeroing-Out Step 1; https://arxiv.org/abs/2210.10173

View graph