Mixed coarse projection equals the owner's ordinary projection

Proved

mme_dwz_step1MixedCoarseProj_eq_owner_gradedAddressProj

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

asymmetric-hashinggraded-addresslinear-mapmatrix-multiplication

In each mode, composing the canonical equality transport from a mixed coarse address with its graded-address projection is exactly the ordinary coarse-address projection for that mode's owner.

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_step1MixedCoarseProj_eq_owner_gradedAddressProj
    {K : Type u} [Field K] {N L n : ℕ}
    (reindex : Fin (N + 1) ≃ Fin L)
    (edge : Fin n → Fin (N + 1) → Fin 15)
    (competitor owner : Fin n) (i : Fin 3) :
    step1MixedCoarseProj K reindex edge competitor owner i =
      gradedAddressProj (cwSquareCanonicalGrading K 6) L
        (coarseAddress
          (sourceWord reindex edge
            (step1MixedOwnerIndex competitor owner i))) i := by
  sorry

Source

Formal address-transport normalization for Duan--Wu--Zhou Additional Zeroing-Out Step 1, arXiv:2210.10173v5, Section 6.

View graph