Coordinate vanishing supplies both rejected Step-1 singleton zeros

import Definitions.Def_mme_dwz_step1_projector_basis_api
import Definitions.Def_mme_dwz_cw_square_fine_split_grading
import Theorems.Thm_mme_basisZAllowed_map_eq_zero_of_selected_singletons
import Theorems.Thm_mme_piTensorProduct_map_eq_zero_of_selected_basis_singletons_at_mode
import Theorems.Thm_mme_dwz_source_address_useful_z_supported_implies_step1_words

open MME Module PiTensorProduct
open MME.DWZStep1Support
open MME.DWZSourceAligned

universe u

set_option autoImplicit false

theorem mme_dwz_step1_rejected_singletons_zero_of_coordinate_word_zero
    {K : Type u} [Field K]
    (m : ℕ) {N : ℕ} (outer : Fin N → Fin 15)
    (copy : DWZSquare.BrokenBlockCopy
      (DWZTable2StandardForm.UsefulBlock m outer))
    (hCoordinateZero : ∀
      (x : AddressModeWord outer 0)
      (y : AddressModeWord outer 1)
      (z : AddressZWord outer),
      (∃ r : Fin N,
        (cwSquareFineSplitGrading K 6).blockTensor
          (fun i ↦ ![
            MME.DWZStep1Support.fineSplitGrade
              (addressModeLeftGrade x r)
              (addressModeRightGrade x r),
            MME.DWZStep1Support.fineSplitGrade
              (addressModeLeftGrade y r)
              (addressModeRightGrade y r),
            MME.DWZStep1Support.fineSplitGrade
              (z r).leftGrade (z r).rightGrade] i) = 0) →
      let G := brokenAddressGrading K m outer copy
      let sx := DWZComponentRestriction.basisLabelProjection
        (coarseAddressModeBasis K outer 0) id {x}
      let sy := DWZComponentRestriction.basisLabelProjection
        (coarseAddressModeBasis K outer 1) id {y}
      let sz := DWZComponentRestriction.basisLabelProjection
        (coarseAddressZBasis K outer) id {z}
      let selected : ∀ i : Fin 3,
          (coarseAddressObj K outer).V i →ₗ[K]
            (coarseAddressObj K outer).V i :=
        Function.update
          (Function.update
            (Function.update (fun _ ↦ LinearMap.id) 0 sx) 1 sy) 2 sz
      PiTensorProduct.map
        (fun i ↦ (G.blockProj i 0).comp (selected i))
        (coarseAddressObj K outer).t = 0) :
    (∀ (x : AddressModeWord outer 0),
      ¬ addressXWordPassesStep1 m outer x →
      let G := brokenAddressGrading K m outer copy
      let base : ∀ i : Fin 3,
          (coarseAddressObj K outer).V i →ₗ[K] G.classOf i 0 :=
        fun i ↦ G.blockProj i 0
      let singleton := DWZComponentRestriction.basisLabelProjection
        (coarseAddressModeBasis K outer 0) id {x}
      PiTensorProduct.map
        (Function.update base 0 ((base 0).comp singleton))
        (coarseAddressObj K outer).t = 0) ∧
    (∀ (y : AddressModeWord outer 1),
      ¬ addressYWordPassesStep1 m outer y →
      let G := brokenAddressGrading K m outer copy
      let base : ∀ i : Fin 3,
          (coarseAddressObj K outer).V i →ₗ[K] G.classOf i 0 :=
        fun i ↦ G.blockProj i 0
      let xMaps := Function.update base 0
        ((base 0).comp (addressXStep1Projector K m outer))
      let singleton := DWZComponentRestriction.basisLabelProjection
        (coarseAddressModeBasis K outer 1) id {y}
      PiTensorProduct.map
        (Function.update xMaps 1 ((xMaps 1).comp singleton))
        (coarseAddressObj K outer).t = 0) := by
  sorry