Dependent and update presentations of three selected owner maps agree

Proved

mme_dwz_broken_owner_three_words_maps_pointwise

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

asymmetric-hashingmatrix-multiplicationstep-1-zeroingtensor-basis

For each of the three tensor modes, selecting the packaged X, Y, or Z address word and then applying the broken-owner block projection is identical to the literal nested-update presentation of the three singleton projectors.

Preamble

import Definitions.Def_mme_dwz_broken_owner_three_words_data

open MME Module
open MME.DWZSourceAligned

universe u

set_option autoImplicit false

Formal statement

theorem mme_dwz_broken_owner_three_words_maps_pointwise
    {K : Type u} [Field K]
    (m : ℕ) {N : ℕ} (outer : Fin N → Fin 15)
    (copy : DWZSquare.BrokenBlockCopy
      (DWZTable2StandardForm.UsefulBlock m outer))
    (x : AddressModeWord outer 0)
    (y : AddressModeWord outer 1)
    (z : AddressZWord outer) (i : Fin 3) :
    brokenOwnerThreeWordsWordMap K m outer copy x y z i =
      brokenOwnerThreeWordsSelectedMap K m outer copy x y z i := 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