κ-improvement development, part 6: array model and networks

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs5

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.NetComplexP8Names
/-!
# Prop. 8, part 1: the complex network in physical gate order, and which gates touch each wire

`cxNamed` (NetComplexLemma5) runs stage 2 as `invNamed` of the forward schedule: the list is
reversed and every gate is replaced by its inverse `1 - (M - 1)`. With logical source `Y` and
target `X` at stage 2, time `r` of stage 2 is the inverse of row `7 - r`, and the gates touch the
physical wires in the order `Y`-side, `Y`-center, `X`-side, `X`-center, `Y`-center, `Y`-side,
`X`-center, `X`-side — exactly the paper's order. So no reordering is needed: we compute, for
every wire, the ordered list of names of the gates of `cxFixNamed` touching it.

* `X a`: rows `2,3,6,7` at stages 1, 3; rows `5,4,1,0` (times `2,3,6,7`) at stage 2; then the
  sign gate `none`.
* `Y a`: rows `0,1,4,5` at stages 1, 3; rows `7,6,3,2` (times `0,1,4,5`) at stage 2.
* side wire `A_{ST}`: rows `0,2,5,7` (reversed at stage 2); central wire: rows `1,3,4,6`
  (reversed at stage 2).

Also: per-wire regrouping of `frameSum2` / `FramesOK2` (`chain2`, `chainOK`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option synthInstance.maxSize 512

namespace NetComplexP8

open Finset NetComplex AModel AModelRat
open NetProp7 (labelsOn labelsOn_cons)

/-! ## 0. Per-wire regrouping for pair functions -/

section Chain2

variable {M β : Type*} [AddCommMonoid β]

/-- `F (x₁, s) + F (x₂, x₁) + ⋯ + F (e, xₙ)` (head label first). -/
def chain2 (F : M → M → β) : M → List M → M → β
  | s, [], e => F e s
  | s, x :: xs, e => F x s + chain2 F x xs e

/-- All consecutive pairs `(head, tail)` satisfy `P`. -/
def chainOK (P : M → M → Prop) : M → List M → M → Prop
  | s, [], e => P e s
  | s, x :: xs, e => P x s ∧ chainOK P x xs e

variable {Wr R : Type*} [Fintype Wr] [DecidableEq Wr] [AddGroup M]

theorem frameSum2_eq_chain (F : M → M → β) :
    ∀ (gates : List (NGate Wr R M)) (lab Mout : Wr → M),
      frameSum2 F gates lab Mout = ∑ w, chain2 F (lab w) (labelsOn w gates) (Mout w) := by
  intro gates
  induction gates with
  | nil => intro lab Mout; simp [frameSum2, labelsOn, chain2]
  | cons g gs ih =>
    intro lab Mout
    rw [frameSum2, ih]
    simp only [labelsOn_cons]
    have e : ∀ x, chain2 F (lab x) (if x ∈ g.2.1 then g.2.2 :: labelsOn x gs else labelsOn x gs)
        (Mout x) = (if x ∈ g.2.1 then F g.2.2 (lab x) else 0) +
          chain2 F (labStep lab g x) (labelsOn x gs) (Mout x) := by
      intro x
      by_cases hx : x ∈ g.2.1 <;> simp [hx, labStep, chain2]
    simp only [e, Finset.sum_add_distrib, Finset.sum_ite_mem, Finset.univ_inter]

theorem framesOK2_iff_chain (P : M → M → Prop) :
    ∀ (gates : List (NGate Wr R M)) (lab Mout : Wr → M),
      FramesOK2 P gates lab Mout ↔ ∀ w, chainOK P (lab w) (labelsOn w gates) (Mout w) := by
  intro gates
  induction gates with
  | nil => intro lab Mout; simp [FramesOK2, labelsOn, chainOK]
  | cons g gs ih =>
    intro lab Mout
    simp only [FramesOK2, ih, labelsOn_cons]
    constructor
    · rintro ⟨h1, h2⟩ w
      by_cases hw : w ∈ g.2.1
      · simp only [hw, if_true, chainOK]
        refine ⟨h1 w hw, ?_⟩
        have := h2 w
        simpa [labStep, hw] using this
      · simp only [hw, if_false]
        have := h2 w
        simpa [labStep, hw] using this
    · intro h
      refine ⟨fun w hw => ?_, fun w => ?_⟩
      · have := h w
        simp only [hw, if_true, chainOK] at this
        exact this.1
      · have := h w
        by_cases hw : w ∈ g.2.1
        · simp only [hw, if_true, chainOK] at this
          simpa [labStep, hw] using this.2
        · simp only [hw, if_false] at this
          simpa [labStep, hw] using this

end Chain2

/-! ## 1. Names of the gates touching a wire -/

section Gen

variable {N N' R W : Type*} [DecidableEq W]

/-- Names of the gates touching `w`, in order. -/
def namesOn (w : W) (l : List (N × (Matrix W W R × Finset W))) : List N :=
  (l.filter fun g => decide (w ∈ g.2.2)).map Prod.fst

lemma namesOn_append (w : W) (l₁ l₂ : List (N × (Matrix W W R × Finset W))) :
    namesOn w (l₁ ++ l₂) = namesOn w l₁ ++ namesOn w l₂ := by
  simp [namesOn, List.filter_append]

lemma namesOn_reverse (w : W) (l : List (N × (Matrix W W R × Finset W))) :
    namesOn w l.reverse = (namesOn w l).reverse := by
  simp [namesOn, List.filter_reverse, List.map_reverse]

lemma namesOn_flatMap {ι : Type*} (w : W) (L : List ι) (F : ι → List (N × (Matrix W W R × Finset W))) :
    namesOn w (L.flatMap F) = L.flatMap fun i => namesOn w (F i) := by
  induction L with
  | nil => simp [namesOn]
  | cons i L ih => simp only [List.flatMap_cons, namesOn_append, ih]

lemma namesOn_rename (w : W) (f : N → N') (l : List (N × (Matrix W W R × Finset W))) :
    namesOn w (l.map fun g => (f g.1, g.2)) = (namesOn w l).map f := by
  simp [namesOn, List.filter_map, List.map_map, Function.comp_def]

lemma namesOn_single (w : W) (n : N) (g : Matrix W W R × Finset W) :
    namesOn w [(n, g)] = if w ∈ g.2 then [n] else [] := by
  by_cases hw : w ∈ g.2 <;> simp [namesOn, hw]

lemma namesOn_row {T : Type*} [Fintype T] [DecidableEq T] (w : W) (k : Fin 8)
    (g : T → Matrix W W R × Finset W) (o : Option T) (hP : ∀ S, w ∈ (g S).2 ↔ some S = o) :
    namesOn w ((univ : Finset T).toList.map fun S => (((k, some S) : NetScalar.IName T), g S)) =
      o.toList.map fun S => ((k, some S) : NetScalar.IName T) := by
  unfold namesOn
  rw [List.filter_map, List.map_map]
  have : (fun x : T => decide (w ∈ ((fun S => (((k, some S) : NetScalar.IName T), g S)) x).2.2)) =
      fun x => decide (some x = o) := by
    funext x; simp only [hP]
  simp only [Function.comp_def, this]
  cases o with
  | none => simp
  | some t =>
    simp only [Option.some.injEq]
    rw [show (fun x : T => decide (x = t)) = fun x => decide (x = t) from rfl,
      NetProp7.filter_eq_toList t _ (Finset.nodup_toList _)]
    simp

lemma namesOn_invNamed [CommRing R] (w : W) (l : List (N × (Matrix W W R × Finset W))) :
    namesOn w (invNamed l) = (namesOn w l).reverse := by
  unfold invNamed
  rw [namesOn_reverse]
  congr 1
  simp [namesOn, List.filter_map, List.map_map, Function.comp_def, invG]

end Gen

/-! ## 2. One invocation -/

section Invocation

variable {R : Type*} [CommRing R] [Invertible (2 : R)]
variable {h : ℕ} {T : Type*} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}
variable {W : Type*} [Fintype W] [DecidableEq W] (I : NetComplex.Inv ind W)

lemma mem_sideG (s : R) (w : W) (S : T) :
    w ∈ (I.sideG R s S).2 ↔ w = I.tgt S ∨ ∃ n : Nb ind, n.1.1 = S ∧ I.side n = w := by
  simp [NetComplex.Inv.sideG]

lemma mem_copyG (s : R) (w : W) (t : T) :
    w ∈ (I.copyG R s t).2 ↔ w = I.src t ∨ ∃ n : Nb ind, n.1.2 = t ∧ I.side n = w := by
  simp [NetComplex.Inv.copyG]

lemma mem_scatG (s : R) (w : W) :
    w ∈ (I.scatG R s).2 ↔ (∃ t, I.tgt t = w) ∨ ∃ i, I.cen i = w := by
  simp [NetComplex.Inv.scatG]

lemma mem_gathG (s : R) (w : W) :
    w ∈ (I.gathG R s).2 ↔ (∃ t, I.src t = w) ∨ ∃ i, I.cen i = w := by
  simp [NetComplex.Inv.gathG]

lemma namesOn_named (w : W) (oS oC : Option T) (bS bG : Prop) [Decidable bS] [Decidable bG]
    (hS : ∀ S, w ∈ (I.sideG R 1 S).2 ↔ some S = oS) (hC : ∀ t, w ∈ (I.copyG R 1 t).2 ↔ some t = oC)
    (hsc : w ∈ (I.scatG R 1).2 ↔ bS) (hga : w ∈ (I.gathG R 1).2 ↔ bG) :
    namesOn w (I.named R) =
      (oS.toList.map fun S => ((0, some S) : NetScalar.IName T)) ++
      (if bS then [(1, none)] else []) ++
      (oC.toList.map fun S => ((2, some S) : NetScalar.IName T)) ++
      (if bG then [(3, none)] else []) ++
      (if bS then [(4, none)] else []) ++
      (oS.toList.map fun S => ((5, some S) : NetScalar.IName T)) ++
      (if bG then [(6, none)] else []) ++
      (oC.toList.map fun S => ((7, some S) : NetScalar.IName T)) := by
  have hS' : ∀ s S, w ∈ (I.sideG R s S).2 ↔ some S = oS := fun s S => by
    rw [← hS S]; simp [mem_sideG]
  have hC' : ∀ s t, w ∈ (I.copyG R s t).2 ↔ some t = oC := fun s t => by
    rw [← hC t]; simp [mem_copyG]
  have hsc' : ∀ s, w ∈ (I.scatG R s).2 ↔ bS := fun s => by rw [← hsc]; simp [mem_scatG]
  have hga' : ∀ s, w ∈ (I.gathG R s).2 ↔ bG := fun s => by rw [← hga]; simp [mem_gathG]
  unfold NetComplex.Inv.named
  simp only [namesOn_append, namesOn_single, namesOn_row w _ _ _ (hS' _),
    namesOn_row w _ _ _ (hC' _), hsc', hga']

variable {I} (hG : I.Good)
include hG

lemma names_src (t₀ : T) :
    namesOn (I.src t₀) (I.named R) = [(2, some t₀), (3, none), (6, none), (7, some t₀)] := by
  rw [namesOn_named I _ none (some t₀) False True]
  · simp
  · intro S; simp only [mem_sideG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨hG.st _ _, fun n _ e => hG.ss _ _ e.symm⟩
  · intro t; simp only [mem_copyG, Option.some.injEq, hG.src_inj.eq_iff]
    constructor
    · rintro (e | ⟨n, -, e⟩)
      · exact e.symm
      · exact absurd e.symm (hG.ss _ _)
    · rintro rfl; exact Or.inl rfl
  · simp only [mem_scatG, iff_false, not_or, not_exists]
    exact ⟨fun t e => hG.st _ _ e.symm, fun i e => hG.sc _ _ e.symm⟩
  · simp only [mem_gathG, iff_true]; exact Or.inl ⟨t₀, rfl⟩

lemma names_tgt (t₀ : T) :
    namesOn (I.tgt t₀) (I.named R) = [(0, some t₀), (1, none), (4, none), (5, some t₀)] := by
  rw [namesOn_named I _ (some t₀) none True False]
  · simp
  · intro t; simp only [mem_sideG, Option.some.injEq, hG.tgt_inj.eq_iff]
    constructor
    · rintro (e | ⟨n, -, e⟩)
      · exact e.symm
      · exact absurd e.symm (hG.ts _ _)
    · rintro rfl; exact Or.inl rfl
  · intro S; simp only [mem_copyG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨fun e => hG.st _ _ e.symm, fun n _ e => hG.ts _ _ e.symm⟩
  · simp only [mem_scatG, iff_true]; exact Or.inl ⟨t₀, rfl⟩
  · simp only [mem_gathG, iff_false, not_or, not_exists]
    exact ⟨fun t e => hG.st _ _ e, fun i e => hG.tc _ _ e.symm⟩

lemma names_cen (i₀ : Option (Fin h)) :
    namesOn (I.cen i₀) (I.named R) = [(1, none), (3, none), (4, none), (6, none)] := by
  rw [namesOn_named I _ none none True True]
  · simp
  · intro S; simp only [mem_sideG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨fun e => hG.tc _ _ e.symm, fun n _ e => hG.sic _ _ e⟩
  · intro S; simp only [mem_copyG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨fun e => hG.sc _ _ e.symm, fun n _ e => hG.sic _ _ e⟩
  · simp only [mem_scatG, iff_true]; exact Or.inr ⟨i₀, rfl⟩
  · simp only [mem_gathG, iff_true]; exact Or.inr ⟨i₀, rfl⟩

lemma names_side (n₀ : Nb ind) :
    namesOn (I.side n₀) (I.named R) =
      [(0, some n₀.1.1), (2, some n₀.1.2), (5, some n₀.1.1), (7, some n₀.1.2)] := by
  rw [namesOn_named I _ (some n₀.1.1) (some n₀.1.2) False False]
  · simp
  · intro S; simp only [mem_sideG, Option.some.injEq]
    constructor
    · rintro (e | ⟨n, hn, e⟩)
      · exact absurd e.symm (hG.ts _ _)
      · rw [hG.side_inj e] at hn; exact hn.symm
    · rintro rfl; exact Or.inr ⟨n₀, rfl, rfl⟩
  · intro t; simp only [mem_copyG, Option.some.injEq]
    constructor
    · rintro (e | ⟨n, hn, e⟩)
      · exact absurd e.symm (hG.ss _ _)
      · rw [hG.side_inj e] at hn; exact hn.symm
    · rintro rfl; exact Or.inr ⟨n₀, rfl, rfl⟩
  · simp only [mem_scatG, iff_false, not_or, not_exists]
    exact ⟨fun t e => hG.ts _ _ e, fun i e => hG.sic _ _ e.symm⟩
  · simp only [mem_gathG, iff_false, not_or, not_exists]
    exact ⟨fun t e => hG.ss _ _ e, fun i e => hG.sic _ _ e.symm⟩

omit hG in
lemma names_none (w : W) (h1 : ∀ t, I.src t ≠ w) (h2 : ∀ t, I.tgt t ≠ w)
    (h3 : ∀ n, I.side n ≠ w) (h4 : ∀ i, I.cen i ≠ w) : namesOn w (I.named R) = [] := by
  rw [namesOn_named I _ none none False False]
  · simp
  · intro S; simp only [mem_sideG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨fun e => h2 _ e.symm, fun n _ e => h3 _ e⟩
  · intro S; simp only [mem_copyG, reduceCtorEq, iff_false, not_or, not_exists, not_and]
    exact ⟨fun e => h1 _ e.symm, fun n _ e => h3 _ e⟩
  · simp only [mem_scatG, iff_false, not_or, not_exists]; exact ⟨h2, h4⟩
  · simp only [mem_gathG, iff_false, not_or, not_exists]; exact ⟨h1, h4⟩

end Invocation

/-! ## 3. The complex network -/

section Complex

variable {R : Type*} [CommRing R] [Invertible (2 : R)]
variable {h : ℕ} {T : Type*} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}

open NetScalar (emb emb_inj)

/-- The bank of `a` at stage `j` (the two other coordinates). -/
def pj (j : Fin 3) (a : T × T × T) : T × T := ((NetScalar.embEquiv j).symm a).1
/-- The varying (`j`th) coordinate of `a`. -/
def cj (j : Fin 3) (a : T × T × T) : T := ((NetScalar.embEquiv j).symm a).2

lemma emb_eq_iff (j : Fin 3) (p : T × T) (t : T) (a : T × T × T) :
    emb j p t = a ↔ p = pj j a ∧ t = cj j a := by
  rw [show emb j p t = NetScalar.embEquiv j (p, t) from rfl, ← Equiv.eq_symm_apply,
    Prod.ext_iff]
  rfl

lemma emb_pj_cj (j : Fin 3) (a : T × T × T) : emb j (pj j a) (cj j a) = a :=
  (emb_eq_iff j _ _ a).2 ⟨rfl, rfl⟩

variable (R ind)

/-- The named block of invocation `(j, p)` inside `cxNamed`. -/
noncomputable def blkC (j : Fin 3) (p : T × T) : List (GName T × CGate R (Wr ind)) :=
  (schedJ R ind j p).map fun g => ((j, p, g.1), g.2)

variable {R ind}

lemma namesOn_blkC (w : Wr ind) (j : Fin 3) (p : T × T) :
    namesOn w (blkC R ind j p) =
      if j = 1 then ((namesOn w ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R)).map
          fun n => (j, p, n)).reverse
      else (namesOn w ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R)).map fun n => (j, p, n) := by
  unfold blkC schedJ
  split_ifs
  · rw [namesOn_rename w (fun n => ((j, p, n) : GName T)), namesOn_invNamed, List.map_reverse]
  · rw [namesOn_rename w (fun n => ((j, p, n) : GName T))]

lemma namesOn_cxNamed (w : Wr ind) :
    namesOn w (cxNamed R ind) = ([0, 1, 2] : List (Fin 3)).flatMap fun j =>
      (univ : Finset (T × T)).toList.flatMap fun p => namesOn w (blkC R ind j p) := by
  unfold cxNamed
  rw [namesOn_flatMap]
  congr 1
  funext j
  rw [namesOn_flatMap]
  rfl

lemma inv_src (j : Fin 3) (p : T × T) (t : T) :
    (NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).src t = srcW j (emb j p t) := rfl
lemma inv_tgt (j : Fin 3) (p : T × T) (t : T) :
    (NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).tgt t = tgtW j (emb j p t) := rfl
lemma inv_side (j : Fin 3) (p : T × T) (n : Nb ind) :
    (NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).side n = wS j p n := rfl
lemma inv_cen (j : Fin 3) (p : T × T) (i : Option (Fin h)) :
    (NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).cen i = wC j p i := rfl

lemma namesInv_X (j : Fin 3) (p : T × T) (a : T × T × T) :
    namesOn (wX a) ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R) =
      if p = pj j a then
        (if j = 1 then [(0, some (cj j a)), (1, none), (4, none), (5, some (cj j a))]
          else [(2, some (cj j a)), (3, none), (6, none), (7, some (cj j a))])
      else [] := by
  by_cases hp : p = pj j a
  · subst hp
    by_cases hj : j = 1
    · have : (wX a : Wr ind) = (NetComplex.inv j (pj j a) : NetComplex.Inv ind (Wr ind)).tgt (cj j a) := by
        rw [inv_tgt, emb_pj_cj]; simp [tgtW, hj]
      rw [this, names_tgt (inv_good _ _)]; simp [hj]
    · have : (wX a : Wr ind) = (NetComplex.inv j (pj j a) : NetComplex.Inv ind (Wr ind)).src (cj j a) := by
        rw [inv_src, emb_pj_cj]; simp [srcW, hj]
      rw [this, names_src (inv_good _ _)]; simp [hj]
  · rw [if_neg hp]
    apply names_none
    · intro t e
      rw [inv_src] at e
      unfold srcW at e
      split_ifs at e
      · simp [wX, wY] at e
      · simp only [wX, Sum.inl.injEq] at e
        exact hp ((emb_eq_iff j p t a).1 e).1
    · intro t e
      rw [inv_tgt] at e
      unfold tgtW at e
      split_ifs at e
      · simp only [wX, Sum.inl.injEq] at e
        exact hp ((emb_eq_iff j p t a).1 e).1
      · simp [wX, wY] at e
    · intro n e; simp [inv_side, wS, wX] at e
    · intro i e; simp [inv_cen, wC, wX] at e

lemma namesInv_Y (j : Fin 3) (p : T × T) (a : T × T × T) :
    namesOn (wY a) ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R) =
      if p = pj j a then
        (if j = 1 then [(2, some (cj j a)), (3, none), (6, none), (7, some (cj j a))]
          else [(0, some (cj j a)), (1, none), (4, none), (5, some (cj j a))])
      else [] := by
  by_cases hp : p = pj j a
  · subst hp
    by_cases hj : j = 1
    · have : (wY a : Wr ind) = (NetComplex.inv j (pj j a) : NetComplex.Inv ind (Wr ind)).src (cj j a) := by
        rw [inv_src, emb_pj_cj]; simp [srcW, hj]
      rw [this, names_src (inv_good _ _)]; simp [hj]
    · have : (wY a : Wr ind) = (NetComplex.inv j (pj j a) : NetComplex.Inv ind (Wr ind)).tgt (cj j a) := by
        rw [inv_tgt, emb_pj_cj]; simp [tgtW, hj]
      rw [this, names_tgt (inv_good _ _)]; simp [hj]
  · rw [if_neg hp]
    apply names_none
    · intro t e
      rw [inv_src] at e
      unfold srcW at e
      split_ifs at e
      · simp only [wY, Sum.inr.injEq, Sum.inl.injEq] at e
        exact hp ((emb_eq_iff j p t a).1 e).1
      · simp [wX, wY] at e
    · intro t e
      rw [inv_tgt] at e
      unfold tgtW at e
      split_ifs at e
      · simp [wX, wY] at e
      · simp only [wY, Sum.inr.injEq, Sum.inl.injEq] at e
        exact hp ((emb_eq_iff j p t a).1 e).1
    · intro n e; simp [inv_side, wS, wY] at e
    · intro i e; simp [inv_cen, wC, wY] at e

lemma namesInv_S (j j' : Fin 3) (p p' : T × T) (n : Nb ind) :
    namesOn (wS j' p' n) ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R) =
      if j = j' ∧ p = p' then
        [(0, some n.1.1), (2, some n.1.2), (5, some n.1.1), (7, some n.1.2)]
      else [] := by
  by_cases hp : j = j' ∧ p = p'
  · obtain ⟨rfl, rfl⟩ := hp
    rw [if_pos ⟨rfl, rfl⟩, ← inv_side j p n, names_side (inv_good _ _)]
  · rw [if_neg hp]
    apply names_none
    · intro t e; rw [inv_src] at e; unfold srcW at e; split_ifs at e <;> simp [wS, wX, wY] at e
    · intro t e; rw [inv_tgt] at e; unfold tgtW at e; split_ifs at e <;> simp [wS, wX, wY] at e
    · intro n' e; simp only [inv_side, wS, Sum.inr.injEq, Sum.inl.injEq, Prod.mk.injEq] at e
      exact hp ⟨e.1, e.2.1⟩
    · intro i e; simp [inv_cen, wC, wS] at e

lemma namesInv_C (j j' : Fin 3) (p p' : T × T) (i : Option (Fin h)) :
    namesOn (wC j' p' i) ((NetComplex.inv j p : NetComplex.Inv ind (Wr ind)).named R) =
      if j = j' ∧ p = p' then [(1, none), (3, none), (4, none), (6, none)] else [] := by
  by_cases hp : j = j' ∧ p = p'
  · obtain ⟨rfl, rfl⟩ := hp
    rw [if_pos ⟨rfl, rfl⟩, ← inv_cen j p i, names_cen (inv_good _ _)]
  · rw [if_neg hp]
    apply names_none
    · intro t e; rw [inv_src] at e; unfold srcW at e; split_ifs at e <;> simp [wC, wX, wY] at e
    · intro t e; rw [inv_tgt] at e; unfold tgtW at e; split_ifs at e <;> simp [wC, wX, wY] at e
    · intro n' e; simp [inv_side, wS, wC] at e
    · intro i' e; simp only [inv_cen, wC, Sum.inr.injEq, Prod.mk.injEq] at e
      exact hp ⟨e.1, e.2.1⟩

theorem names_X (a : T × T × T) :
    namesOn (wX a) (cxNamed R ind) =
      (([(2, some (cj 0 a)), (3, none), (6, none), (7, some (cj 0 a))] :
          List (NetScalar.IName T)).map fun n => ((0 : Fin 3), pj 0 a, n)) ++
      ((([(0, some (cj 1 a)), (1, none), (4, none), (5, some (cj 1 a))] :
          List (NetScalar.IName T)).map fun n => ((1 : Fin 3), pj 1 a, n)).reverse ++
      ((([(2, some (cj 2 a)), (3, none), (6, none), (7, some (cj 2 a))] :
          List (NetScalar.IName T)).map fun n => ((2 : Fin 3), pj 2 a, n)))) := by
  rw [namesOn_cxNamed]
  simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil]
  have st : ∀ j : Fin 3, ((univ : Finset (T × T)).toList.flatMap fun p =>
      namesOn (wX a) (blkC R ind j p)) = namesOn (wX a) (blkC R ind j (pj j a)) := fun j =>
    NetProp7.flatMap_univ_single _ _ fun p hp => by rw [namesOn_blkC, namesInv_X, if_neg hp]; simp
  rw [st, st, st]
  simp only [namesOn_blkC, namesInv_X, if_true]
  simp

theorem names_Y (a : T × T × T) :
    namesOn (wY a) (cxNamed R ind) =
      (([(0, some (cj 0 a)), (1, none), (4, none), (5, some (cj 0 a))] :
          List (NetScalar.IName T)).map fun n => ((0 : Fin 3), pj 0 a, n)) ++
      ((([(2, some (cj 1 a)), (3, none), (6, none), (7, some (cj 1 a))] :
          List (NetScalar.IName T)).map fun n => ((1 : Fin 3), pj 1 a, n)).reverse ++
      ((([(0, some (cj 2 a)), (1, none), (4, none), (5, some (cj 2 a))] :
          List (NetScalar.IName T)).map fun n => ((2 : Fin 3), pj 2 a, n)))) := by
  rw [namesOn_cxNamed]
  simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil]
  have st : ∀ j : Fin 3, ((univ : Finset (T × T)).toList.flatMap fun p =>
      namesOn (wY a) (blkC R ind j p)) = namesOn (wY a) (blkC R ind j (pj j a)) := fun j =>
    NetProp7.flatMap_univ_single _ _ fun p hp => by rw [namesOn_blkC, namesInv_Y, if_neg hp]; simp
  rw [st, st, st]
  simp only [namesOn_blkC, namesInv_Y, if_true]
  simp

lemma stages_single {β : Type*} (F : Fin 3 → List β) (j : Fin 3)
    (hF : ∀ j', j' ≠ j → F j' = []) : ([0, 1, 2] : List (Fin 3)).flatMap F = F j :=
  NetProp7.flatMap_single F j _ (by decide) (by fin_cases j <;> simp) (fun p _ hp => hF p hp)

theorem names_S (j : Fin 3) (p : T × T) (n : Nb ind) :
    namesOn (wS j p n) (cxNamed R ind) =
      if j = 1 then
        (([(0, some n.1.1), (2, some n.1.2), (5, some n.1.1), (7, some n.1.2)] :
          List (NetScalar.IName T)).map fun k => (j, p, k)).reverse
      else ([(0, some n.1.1), (2, some n.1.2), (5, some n.1.1), (7, some n.1.2)] :
          List (NetScalar.IName T)).map fun k => (j, p, k) := by
  rw [namesOn_cxNamed, stages_single _ j]
  · rw [NetProp7.flatMap_univ_single _ p]
    · simp only [namesOn_blkC, namesInv_S, and_self, if_true]
    · intro p' hp'
      simp [namesOn_blkC, namesInv_S, hp']
  · intro j' hj'
    apply NetProp7.flatMap_univ_nil
    intro p'
    simp [namesOn_blkC, namesInv_S, hj']

theorem names_C (j : Fin 3) (p : T × T) (i : Option (Fin h)) :
    namesOn (wC j p i) (cxNamed R ind) =
      if j = 1 then
        (([(1, none), (3, none), (4, none), (6, none)] : List (NetScalar.IName T)).map
          fun k => (j, p, k)).reverse
      else ([(1, none), (3, none), (4, none), (6, none)] : List (NetScalar.IName T)).map
          fun k => (j, p, k) := by
  rw [namesOn_cxNamed, stages_single _ j]
  · rw [NetProp7.flatMap_univ_single _ p]
    · simp only [namesOn_blkC, namesInv_C, and_self, if_true]
    · intro p' hp'
      simp [namesOn_blkC, namesInv_C, hp']
  · intro j' hj'
    apply NetProp7.flatMap_univ_nil
    intro p'
    simp [namesOn_blkC, namesInv_C, hj']

/-- Names on the corrected network: the names on `cxNamed`, then the sign gate on `X` wires. -/
theorem namesOn_cxFix (w : Wr ind) :
    namesOn w (cxFixNamed R ind) = (namesOn w (cxNamed R ind)).map some ++
      (match w with | Sum.inl _ => [none] | Sum.inr _ => []) := by
  unfold cxFixNamed
  rw [namesOn_append, namesOn_rename w (some : GName T → Option (GName T)), namesOn_single]
  congr 1
  rcases w with a | b
  · simp [fixG, wX]
  · simp [fixG, wX]

/-- Labels along a wire of a labelled named list. -/
lemma labelsOn_labelled {N M : Type*} [AddGroup M] {W : Type*} [Fintype W] [DecidableEq W]
    (lab : N → M) (w : W) (l : List (N × CGate R W)) :
    labelsOn w (labelled lab l) = (namesOn w l).map lab := by
  induction l with
  | nil => rfl
  | cons g l ih =>
    simp only [labelled, List.map_cons, labelsOn_cons] at ih ⊢
    rw [ih]
    by_cases hw : w ∈ g.2.2 <;> simp [namesOn, hw, List.filter_cons]

end Complex

end NetComplexP8

end

section
-- Source module: Solutions.NetLabels
open Matrix Module

set_option linter.unusedSectionVars false

namespace NetLabels

variable {K : Type*} [Field K] {ι : Type*} [Fintype ι] [DecidableEq ι]

/-- The bilinear form `xᵀ G y`. -/
def bf (G : Matrix ι ι K) (x y : ι → K) : K := x ⬝ᵥ G *ᵥ y

/-- Orthogonal complement `U^⊥ = {y | ∀ x ∈ U, xᵀ G y = 0}`. -/
def orth (G : Matrix ι ι K) (U : Submodule K (ι → K)) : Submodule K (ι → K) :=
  (Matrix.toBilin' G).orthogonal U

/-- `U` is nondegenerate for `G`. -/
def NondegOn (G : Matrix ι ι K) (U : Submodule K (ι → K)) : Prop :=
  ∀ x ∈ U, (∀ y ∈ U, bf G x y = 0) → x = 0

lemma bf_eq_toBilin' (G : Matrix ι ι K) (x y : ι → K) : bf G x y = Matrix.toBilin' G x y := by
  rw [Matrix.toBilin'_apply']; rfl

lemma mem_orth {G : Matrix ι ι K} {U : Submodule K (ι → K)} {y : ι → K} :
    y ∈ orth G U ↔ ∀ x ∈ U, bf G x y = 0 := by
  simp only [orth, LinearMap.BilinForm.mem_orthogonal_iff, bf_eq_toBilin']

lemma bf_symm {G : Matrix ι ι K} (hG : G.IsSymm) (x y : ι → K) : bf G x y = bf G y x := by
  unfold bf
  rw [Matrix.dotProduct_mulVec, dotProduct_comm, ← Matrix.mulVec_transpose, hG.eq]

lemma bf_sub_right (G : Matrix ι ι K) (x y y' : ι → K) : bf G x (y - y') = bf G x y - bf G x y' := by
  simp [bf, mulVec_sub, dotProduct_sub]
lemma bf_smul_left (G : Matrix ι ι K) (c : K) (x y : ι → K) : bf G (c • x) y = c * bf G x y := by
  simp [bf, smul_dotProduct]

theorem isCompl_orth {G : Matrix ι ι K} (hG : G.IsSymm) {U : Submodule K (ι → K)}
    (hU : NondegOn G U) : IsCompl U (orth G U) := by
  apply LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate
  · intro x y h
    rw [← bf_eq_toBilin'] at h ⊢
    rw [bf_symm hG]; exact h
  · constructor
    · intro x hx
      have := hU x.1 x.2 (fun y hy => by
        have := hx ⟨y, hy⟩
        simpa [LinearMap.BilinForm.restrict_apply, ← bf_eq_toBilin'] using this)
      exact Subtype.ext this
    · intro x hx
      have := hU x.1 x.2 (fun y hy => by
        have := hx ⟨y, hy⟩
        rw [bf_symm hG]
        simpa [LinearMap.BilinForm.restrict_apply, ← bf_eq_toBilin'] using this)
      exact Subtype.ext this

/-- The projection matrix onto `U` along `U^⊥` (zero if `U ⊕ U^⊥ ≠ F`). -/
noncomputable def proj (G : Matrix ι ι K) (U : Submodule K (ι → K)) : Matrix ι ι K := by
  classical
  exact if h : IsCompl U (orth G U) then LinearMap.toMatrix' (U.projection (orth G U) h) else 0

lemma proj_mulVec_of_isCompl {G : Matrix ι ι K} {U : Submodule K (ι → K)}
    (h : IsCompl U (orth G U)) (x : ι → K) :
    proj G U *ᵥ x = U.projection (orth G U) h x := by
  unfold proj
  rw [dif_pos h, LinearMap.toMatrix'_mulVec]

section proj
variable {G : Matrix ι ι K} (hG : G.IsSymm) {U : Submodule K (ι → K)} (hU : NondegOn G U)
include hG hU

theorem proj_mulVec_mem (x : ι → K) : proj G U *ᵥ x ∈ U := by
  rw [proj_mulVec_of_isCompl (isCompl_orth hG hU)]
  exact Submodule.projection_apply_mem _ _

theorem sub_proj_mulVec_mem (x : ι → K) : x - proj G U *ᵥ x ∈ orth G U := by
  have h := isCompl_orth hG hU
  rw [proj_mulVec_of_isCompl h]
  have := Submodule.projection_add_projection_eq_self h x
  rw [← eq_sub_of_add_eq' this]
  exact Submodule.projection_apply_mem _ _

theorem proj_mulVec_of_mem {x : ι → K} (hx : x ∈ U) : proj G U *ᵥ x = x := by
  rw [proj_mulVec_of_isCompl (isCompl_orth hG hU)]
  exact Submodule.projection_apply_of_mem_left _ hx

/-- Uniqueness of the projection. -/
theorem proj_unique (P : Matrix ι ι K) (h1 : ∀ x, P *ᵥ x ∈ U)
    (h2 : ∀ x, x - P *ᵥ x ∈ orth G U) : P = proj G U := by
  have hc := isCompl_orth hG hU
  apply Matrix.toLin'.injective
  apply LinearMap.ext
  intro x
  simp only [Matrix.toLin'_apply]
  have hmem : P *ᵥ x - proj G U *ᵥ x ∈ U ⊓ orth G U := by
    refine ⟨U.sub_mem (h1 x) (proj_mulVec_mem hG hU x), ?_⟩
    have := (orth G U).sub_mem (sub_proj_mulVec_mem hG hU x) (h2 x)
    simpa using this
  rw [hc.inf_eq_bot, Submodule.mem_bot, sub_eq_zero] at hmem
  exact hmem

end proj

section diff
variable {G : Matrix ι ι K} (hG : G.IsSymm)
include hG

variable {U V : Submodule K (ι → K)} (hU : NondegOn G U) (hV : NondegOn G V) (hUV : U ≤ V)
include hU hV hUV

theorem sub_proj_mem_diff (v : ι → K) (hv : v ∈ V) : v - proj G U *ᵥ v ∈ V ⊓ orth G U :=
  ⟨V.sub_mem hv (hUV (proj_mulVec_mem hG hU v)), sub_proj_mulVec_mem hG hU v⟩

theorem nondeg_diff : NondegOn G (V ⊓ orth G U) := by
  intro w hw hww
  apply hV w hw.1
  intro v hv
  have h1 := hww _ (sub_proj_mem_diff hG hU hV hUV v hv)
  have h2 : bf G w (proj G U *ᵥ v) = 0 := by
    rw [bf_symm hG]; exact (mem_orth.1 hw.2) _ (proj_mulVec_mem hG hU v)
  rw [bf_sub_right, h2, sub_zero] at h1
  exact h1

/-- `P_V − P_U` is the projection onto `V ∩ U^⊥` along its orthogonal complement. -/
theorem proj_sub_proj : proj G V - proj G U = proj G (V ⊓ orth G U) := by
  apply proj_unique hG (nondeg_diff hG hU hV hUV)
  · intro x
    rw [Matrix.sub_mulVec]
    refine ⟨V.sub_mem (proj_mulVec_mem hG hV x) (hUV (proj_mulVec_mem hG hU x)), ?_⟩
    show _ ∈ orth G U
    rw [mem_orth]
    intro u hu
    have e1 := (mem_orth.1 (sub_proj_mulVec_mem hG hU x)) u hu
    have e2 := (mem_orth.1 (sub_proj_mulVec_mem hG hV x)) u (hUV hu)
    rw [bf_sub_right] at e1 e2 ⊢
    linear_combination e1 - e2
  · intro x
    rw [mem_orth]
    intro w hw
    have e1 := (mem_orth.1 (sub_proj_mulVec_mem hG hV x)) w hw.1
    have e2 : bf G w (proj G U *ᵥ x) = 0 := by
      rw [bf_symm hG]; exact (mem_orth.1 hw.2) _ (proj_mulVec_mem hG hU x)
    rw [Matrix.sub_mulVec, bf_sub_right, bf_sub_right] at *
    linear_combination e1 + e2

theorem finrank_diff : finrank K ↥(V ⊓ orth G U) + finrank K U = finrank K V := by
  have hsup : U ⊔ (V ⊓ orth G U) = V := by
    apply le_antisymm (sup_le hUV inf_le_left)
    intro v hv
    have := Submodule.add_mem_sup (proj_mulVec_mem hG hU v) (sub_proj_mem_diff hG hU hV hUV v hv)
    simpa using this
  have hinf : U ⊓ (V ⊓ orth G U) = ⊥ := by
    have := (isCompl_orth hG hU).inf_eq_bot
    exact eq_bot_iff.2 (fun x hx => by
      rw [← this]; exact ⟨hx.1, hx.2.2⟩)
  have := Submodule.finrank_sup_add_finrank_inf_eq U (V ⊓ orth G U)
  rw [hsup, hinf, finrank_bot] at this
  omega

end diff

section source
variable {G : Matrix ι ι K} (hG : G.IsSymm) {U : Submodule K (ι → K)} (hU : NondegOn G U)
include hG hU

theorem nondeg_orth (hdet : G.det ≠ 0) : NondegOn G (orth G U) := by
  intro w hw hww
  have hall : ∀ y, bf G w y = 0 := by
    intro y
    have e1 := hww _ (sub_proj_mulVec_mem hG hU y)
    have e2 : bf G w (proj G U *ᵥ y) = 0 := by
      rw [bf_symm hG]; exact (mem_orth.1 hw) _ (proj_mulVec_mem hG hU y)
    rw [bf_sub_right, e2, sub_zero] at e1
    exact e1
  have hGw : G *ᵥ w = 0 := by
    funext i
    have := hall (Pi.single i 1)
    rw [bf_symm hG, bf, single_dotProduct, one_mul] at this
    exact this
  by_contra hne
  exact hdet (Matrix.exists_mulVec_eq_zero_iff.1 ⟨w, hne, hGw⟩)

/-- `P_{U^⊥} = 1 − P_U`. -/
theorem proj_orth (hdet : G.det ≠ 0) : proj G (orth G U) = 1 - proj G U := by
  symm
  apply proj_unique hG (nondeg_orth hG hU hdet)
  · intro x
    rw [Matrix.sub_mulVec, Matrix.one_mulVec]
    exact sub_proj_mulVec_mem hG hU x
  · intro x
    rw [Matrix.sub_mulVec, Matrix.one_mulVec, sub_sub_cancel, mem_orth]
    intro y hy
    rw [bf_symm hG]; exact (mem_orth.1 hy) _ (proj_mulVec_mem hG hU x)

end source

section telescope
variable {G : Matrix ι ι K} (hG : G.IsSymm)
include hG

variable (U : ℕ → Submodule K (ι → K)) (hnd : ∀ i, NondegOn G (U i))
include hnd

end telescope

/-- A line `K ∙ v` is nondegenerate as soon as `⟨v, v⟩ ≠ 0`. -/
theorem nondegOn_span_singleton (G : Matrix ι ι K) {v : ι → K} (hv : bf G v v ≠ 0) :
    NondegOn G (K ∙ v) := by
  intro x hx hxx
  obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hx
  have := hxx v (Submodule.mem_span_singleton_self v)
  rw [bf_smul_left] at this
  rcases mul_eq_zero.1 this with h | h
  · rw [h, zero_smul]
  · exact absurd h hv

/-! ### (c) The bit-network form `I − J/9` on `K^h`. -/

section bit

/-- The Gram matrix `I − J/9`. -/
def bitGram (K : Type*) [Field K] (h : ℕ) : Matrix (Fin h) (Fin h) K :=
  1 - (9 : K)⁻¹ • Matrix.of (fun _ _ => (1 : K))

variable [CharZero K]

end bit

section triples
variable {h : ℕ}

/-- Indicator vector of a subset. -/
def ind (K : Type*) [Field K] (S : Finset (Fin h)) : Fin h → K := fun i => if i ∈ S then 1 else 0

lemma ind_dotProduct_ind (S T : Finset (Fin h)) : ind K S ⬝ᵥ ind K T = (S ∩ T).card := by
  simp only [dotProduct, ind, mul_ite, mul_one, mul_zero]
  rw [← Finset.sum_filter, ← Finset.sum_filter]
  simp only [Finset.sum_const, nsmul_eq_mul, mul_one]
  congr 2
  ext i; simp [Finset.mem_filter, and_comm]

variable [CharZero K]

end triples

/-! ### (d) Tensor products of labels (Kronecker Gram matrices). -/

section general
variable {G : Matrix ι ι K} (hG : G.IsSymm)
include hG

end general

section tensor
variable {κ : Type*} [Fintype κ] [DecidableEq κ]
open scoped Kronecker

/-- Pure tensor `x ⊗ y` as a function on `ι × κ`. -/
def tp (x : ι → K) (y : κ → K) : ι × κ → K := fun p => x p.1 * y p.2

lemma tp_dotProduct (x x' : ι → K) (y y' : κ → K) :
    tp x y ⬝ᵥ tp x' y' = (x ⬝ᵥ x') * (y ⬝ᵥ y') := by
  simp only [tp, dotProduct, Fintype.sum_prod_type, Finset.sum_mul_sum]
  refine Finset.sum_congr rfl (fun _ _ => Finset.sum_congr rfl (fun _ _ => by ring))

section kron
variable {G : Matrix ι ι K} {H : Matrix κ κ K} (hG : G.IsSymm) (hH : H.IsSymm)
  {U : Submodule K (ι → K)} {V : Submodule K (κ → K)} (hU : NondegOn G U) (hV : NondegOn H V)
include hG hH hU hV

variable (hGd : G.det ≠ 0) (hHd : H.det ≠ 0)
include hGd hHd

end kron

end tensor

section cube
open scoped Kronecker
variable {h : ℕ}

variable [CharZero K]

end cube

end NetLabels

end

section
-- Source module: Solutions.NetComplexOrtho
/-!
# Orthonormal bases of binary symmetric spaces (end of the proof of Lemma 6)

On `V = ι → 𝔽₂` with the dot product: every subspace `E` that is nondegenerate and either zero
or nonalternating (contains a vector of norm one) has an orthonormal basis: a finite set of
pairwise orthogonal norm-one vectors spanning `E`; its cardinality is `dim E`.

The proof follows the paper: pick a unit vector `w₀ ∈ E`. If `E ∩ w₀^⊥` is zero or
nonalternating, split off `w₀`. Otherwise `E ∩ w₀^⊥` is alternating, nonzero and
nondegenerate; choose `a, b` in it with `a · b = 1`; then `w = w₀ + a` is a unit vector and
`w₀ + b` is a unit vector orthogonal to `w`, so `E ∩ w^⊥` is nonalternating. Split off `w` and
recurse (`E ∩ w^⊥` is nondegenerate and has dimension `dim E - 1`).
-/

set_option linter.unusedSectionVars false

namespace NetComplexOrtho

open Matrix Finset Module

variable {ι : Type*} [Fintype ι] [DecidableEq ι]

lemma zmod2_add_self (a : ZMod 2) : a + a = 0 := by revert a; decide

lemma zmod2_cases (a : ZMod 2) : a = 0 ∨ a = 1 := by revert a; decide

/-- Nondegeneracy of a subspace for the dot product. -/
def Nondeg (E : Submodule (ZMod 2) (ι → ZMod 2)) : Prop :=
  ∀ x ∈ E, (∀ y ∈ E, x ⬝ᵥ y = 0) → x = 0

/-- The hyperplane `w^⊥`. -/
def perp (w : (ι → ZMod 2)) : Submodule (ZMod 2) (ι → ZMod 2) where
  carrier := {y | w ⬝ᵥ y = 0}
  add_mem' {a b} ha hb := by
    simp only [Set.mem_ofPred_eq] at *
    rw [dotProduct_add, ha, hb, add_zero]
  zero_mem' := by simp
  smul_mem' c x hx := by
    simp only [Set.mem_ofPred_eq] at *
    rw [dotProduct_smul, hx, smul_zero]

lemma mem_perp {w y : (ι → ZMod 2)} : y ∈ perp w ↔ w ⬝ᵥ y = 0 := Iff.rfl

lemma norm_add (x y : (ι → ZMod 2)) : (x + y) ⬝ᵥ (x + y) = x ⬝ᵥ x + y ⬝ᵥ y := by
  rw [add_dotProduct, dotProduct_add, dotProduct_add, dotProduct_comm y x]
  have := NetComplexOrtho.zmod2_add_self (x ⬝ᵥ y)
  linear_combination this

/-- `E = ⟨w⟩ + (E ∩ w^⊥)` for a unit `w ∈ E`. -/
lemma split (E : Submodule (ZMod 2) (ι → ZMod 2)) {w : (ι → ZMod 2)} (hw : w ∈ E) (hww : w ⬝ᵥ w = 1) :
    E = (Submodule.span (ZMod 2) {w}) ⊔ (E ⊓ perp w) := by
  apply le_antisymm
  · intro y hy
    have : y = (w ⬝ᵥ y) • w + (y - (w ⬝ᵥ y) • w) := by abel
    rw [this]
    refine Submodule.add_mem_sup (Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self w))
      ⟨E.sub_mem hy (E.smul_mem _ hw), ?_⟩
    show w ⬝ᵥ _ = 0
    rw [dotProduct_sub, dotProduct_smul, hww, smul_eq_mul, mul_one, sub_self]
  · exact sup_le ((Submodule.span_singleton_le_iff_mem _ _).2 hw) inf_le_left

lemma nondeg_perp (E : Submodule (ZMod 2) (ι → ZMod 2)) (hE : Nondeg E) {w : (ι → ZMod 2)} (hw : w ∈ E)
    (hww : w ⬝ᵥ w = 1) : Nondeg (E ⊓ perp w) := by
  intro x hx hxy
  apply hE x hx.1
  intro y hy
  have hy' := hy
  rw [split E hw hww] at hy'
  obtain ⟨p, hp, q, hq, rfl⟩ := Submodule.mem_sup.1 hy'
  obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hp
  rw [dotProduct_add, hxy q hq, dotProduct_smul, dotProduct_comm, hx.2, smul_zero, add_zero]

lemma finrank_perp (E : Submodule (ZMod 2) (ι → ZMod 2)) {w : (ι → ZMod 2)} (hw : w ∈ E) (hww : w ⬝ᵥ w = 1) :
    finrank (ZMod 2) ↥(E ⊓ perp w) + 1 = finrank (ZMod 2) E := by
  have hw0 : w ≠ 0 := by rintro rfl; simp at hww
  have hdisj : (Submodule.span (ZMod 2) {w}) ⊓ (E ⊓ perp w) = ⊥ := by
    rw [eq_bot_iff]
    intro x hx
    obtain ⟨hx1, hx2⟩ := Submodule.mem_inf.1 hx
    obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hx1
    have : w ⬝ᵥ (c • w) = 0 := (Submodule.mem_inf.1 hx2).2
    rw [dotProduct_smul, hww, smul_eq_mul, mul_one] at this
    simp [this]
  have := Submodule.finrank_sup_add_finrank_inf_eq (Submodule.span (ZMod 2) {w}) (E ⊓ perp w)
  rw [← split E hw hww, hdisj, finrank_bot, add_zero, finrank_span_singleton hw0] at this
  omega

/-- The key step: a unit vector `w ∈ E` such that `E ∩ w^⊥` is zero or nonalternating. -/
lemma good_unit (E : Submodule (ZMod 2) (ι → ZMod 2)) (hE : Nondeg E) {w₀ : (ι → ZMod 2)} (hw₀ : w₀ ∈ E)
    (hn₀ : w₀ ⬝ᵥ w₀ = 1) :
    ∃ w ∈ E, w ⬝ᵥ w = 1 ∧ (E ⊓ perp w = ⊥ ∨ ∃ c ∈ E ⊓ perp w, c ⬝ᵥ c = 1) := by
  by_cases h : E ⊓ perp w₀ = ⊥ ∨ ∃ c ∈ E ⊓ perp w₀, c ⬝ᵥ c = 1
  · exact ⟨w₀, hw₀, hn₀, h⟩
  push Not at h
  obtain ⟨hne, halt⟩ := h
  obtain ⟨a, ha, ha0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hne
  have hnd := nondeg_perp E hE hw₀ hn₀
  have : ¬ ∀ y ∈ E ⊓ perp w₀, a ⬝ᵥ y = 0 := fun hall => ha0 (hnd a ha hall)
  push Not at this
  obtain ⟨b, hb, hab⟩ := this
  have hab1 : a ⬝ᵥ b = 1 := (NetComplexOrtho.zmod2_cases _).resolve_left hab
  have hzero : ∀ c ∈ E ⊓ perp w₀, c ⬝ᵥ c = 0 := fun c hc =>
    (NetComplexOrtho.zmod2_cases _).resolve_right (halt c hc)
  refine ⟨w₀ + a, E.add_mem hw₀ ha.1, ?_, Or.inr ⟨w₀ + b, ⟨E.add_mem hw₀ hb.1, ?_⟩, ?_⟩⟩
  · rw [norm_add, hn₀, hzero a ha, add_zero]
  · show (w₀ + a) ⬝ᵥ (w₀ + b) = 0
    rw [add_dotProduct, dotProduct_add, dotProduct_add, hn₀, mem_perp.1 hb.2,
      dotProduct_comm a w₀, mem_perp.1 ha.2, hab1]
    decide
  · rw [norm_add, hn₀, hzero b hb, add_zero]

/-- An orthonormal family. -/
def Orthonormal2 (B : Finset (ι → ZMod 2)) : Prop :=
  (∀ b ∈ B, b ⬝ᵥ b = 1) ∧ ∀ b ∈ B, ∀ c ∈ B, b ≠ c → b ⬝ᵥ c = 0

/-- **Orthonormal basis theorem over `𝔽₂`.** A nondegenerate subspace that is zero or contains
a vector of norm one has an orthonormal basis. -/
theorem exists_orthonormal_basis :
    ∀ (n : ℕ) (E : Submodule (ZMod 2) (ι → ZMod 2)), finrank (ZMod 2) E = n → Nondeg E →
      (E = ⊥ ∨ ∃ x ∈ E, x ⬝ᵥ x = 1) →
      ∃ B : Finset (ι → ZMod 2), (∀ b ∈ B, b ∈ E) ∧ Orthonormal2 B ∧ Submodule.span (ZMod 2) ↑B = E := by
  intro n
  induction n with
  | zero =>
    intro E hn _ _
    refine ⟨∅, by simp, ⟨by simp, by simp⟩, ?_⟩
    rw [Finset.coe_empty, Submodule.span_empty]
    exact (Submodule.finrank_eq_zero.1 hn).symm
  | succ n ih =>
    intro E hn hE hcase
    rcases hcase with hbot | ⟨w₀, hw₀, hn₀⟩
    · rw [hbot, finrank_bot] at hn; omega
    obtain ⟨w, hw, hww, hgood⟩ := good_unit E hE hw₀ hn₀
    have hfin := finrank_perp E hw hww
    obtain ⟨B, hBE, ⟨hB1, hB2⟩, hBspan⟩ :=
      ih (E ⊓ perp w) (by omega) (nondeg_perp E hE hw hww) hgood
    have hwB : w ∉ B := fun h => by
      have : w ⬝ᵥ w = 0 := (hBE w h).2
      rw [hww] at this
      exact one_ne_zero this
    refine ⟨insert w B, ?_, ⟨?_, ?_⟩, ?_⟩
    · intro b hb
      rcases Finset.mem_insert.1 hb with rfl | hb
      · exact hw
      · exact (hBE b hb).1
    · intro b hb
      rcases Finset.mem_insert.1 hb with rfl | hb
      · exact hww
      · exact hB1 b hb
    · intro b hb c hc hbc
      rcases Finset.mem_insert.1 hb with e1 | hb' <;> rcases Finset.mem_insert.1 hc with e2 | hc'
      · exact absurd (e1.trans e2.symm) hbc
      · subst e1; exact (hBE c hc').2
      · subst e2; rw [dotProduct_comm]; exact (hBE b hb').2
      · exact hB2 b hb' c hc' hbc
    · rw [Finset.coe_insert, Submodule.span_insert, hBspan, ← split E hw hww]

/-- An orthonormal family is linearly independent. -/
theorem orthonormal_linearIndependent {B : Finset (ι → ZMod 2)} (hB : Orthonormal2 B) :
    LinearIndependent (ZMod 2) ((↑) : B → (ι → ZMod 2)) := by
  rw [linearIndependent_iff']
  intro s g hg i hi
  have := congrArg (fun x => (i : (ι → ZMod 2)) ⬝ᵥ x) hg
  simp only [dotProduct_sum, dotProduct_smul, dotProduct_zero, smul_eq_mul] at this
  rw [Finset.sum_eq_single i] at this
  · rwa [hB.1 i i.2, mul_one] at this
  · intro j _ hji
    rw [hB.2 i i.2 j j.2 (fun e => hji (Subtype.ext e.symm)), mul_zero]
  · intro h; exact absurd hi h

/-- **Orthonormal basis theorem, with cardinality.** -/
theorem exists_orthonormal_basis_card (E : Submodule (ZMod 2) (ι → ZMod 2)) (hE : Nondeg E)
    (hcase : E = ⊥ ∨ ∃ x ∈ E, x ⬝ᵥ x = 1) :
    ∃ B : Finset (ι → ZMod 2), (∀ b ∈ B, b ∈ E) ∧ Orthonormal2 B ∧ Submodule.span (ZMod 2) ↑B = E ∧
      B.card = finrank (ZMod 2) E := by
  obtain ⟨B, h1, h2, h3⟩ := exists_orthonormal_basis _ E rfl hE hcase
  refine ⟨B, h1, h2, h3, ?_⟩
  rw [← h3, finrank_span_set_eq_card (orthonormal_linearIndependent h2)]
  simp

end NetComplexOrtho

end

section
-- Source module: Solutions.NetComplexLabels
/-!
# Labels of the complex network over `𝔽₂` (§3.3, §3.5)

The label field of the complex construction is `F = 𝔽₂^h` with the ordinary dot product
(`NetLabels.bf` with Gram matrix `1`), and `F^{⊗3}` with Gram `1 ⊗ 1 ⊗ 1 = 1`.

1. `bf_one`: `bf 1 x y = x · y`; `nondegOn_one_iff`: `NondegOn 1 = NetComplexOrtho.Nondeg`.
2. Triples: `t_T · t_T = 1`, distinct triples with even intersection are orthogonal, triple
   lines are nondegenerate; `u_a · u_a = 1` for `u_a = t_{a₁} ⊗ t_{a₂} ⊗ t_{a₃}`, `U_a`
   nondegenerate; tensor products of nondegenerate labels are nondegenerate.
3. Projections through orthonormal bases: `P_E x = ∑_{v ∈ B} (v · x) v`; for nested
   nondegenerate labels `U ≤ V` whose residual `E = V ∩ U^⊥` has an orthonormal basis `B`,
   `q_V(x) - q_U(x) ≡ ∑_{v∈B} wt(v)[v·x] (mod 4)` with `q_U(x) = wt(P_U x)`.
4. Terminal labels: `q_0 = 0`, `q_F = wt`, and for a unit line `U = ⟨u⟩` with odd weight,
   `q_{U^⊥}(x) - q_U(x) ≡ wt(x) + 2[u·x] (mod 4)` — the hypotheses of
   `NetComplexInterface.phase_interface_full` / `phase_interface_mixed`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetComplexLabels

open Matrix Finset Module NetLabels NetComplexPhase
open scoped Kronecker

/-! ## 1. The dot product as a label form -/

section Dot

variable {ι : Type*} [Fintype ι] [DecidableEq ι]

lemma bf_one (x y : ι → ZMod 2) : bf (1 : Matrix ι ι (ZMod 2)) x y = x ⬝ᵥ y := by
  simp [bf]

lemma one_isSymm : (1 : Matrix ι ι (ZMod 2)).IsSymm := Matrix.isSymm_one

lemma nondegOn_one_iff (E : Submodule (ZMod 2) (ι → ZMod 2)) :
    NondegOn (1 : Matrix ι ι (ZMod 2)) E ↔ NetComplexOrtho.Nondeg E := by
  simp only [NondegOn, NetComplexOrtho.Nondeg, bf_one]

lemma mem_orth_one {U : Submodule (ZMod 2) (ι → ZMod 2)} {y : ι → ZMod 2} :
    y ∈ orth (1 : Matrix ι ι (ZMod 2)) U ↔ ∀ x ∈ U, x ⬝ᵥ y = 0 := by
  rw [mem_orth]; simp only [bf_one]

end Dot

/-! ## 2. Triples over `𝔽₂` -/

section Triples

variable {h : ℕ}

lemma dot_ind (S T : Finset (Fin h)) :
    ind (ZMod 2) S ⬝ᵥ ind (ZMod 2) T = ((S ∩ T).card : ZMod 2) :=
  ind_dotProduct_ind S T

/-- `t_T · t_T = 1` for a triple. -/
theorem dot_triple_self (T : Finset (Fin h)) (hT : T.card = 3) :
    ind (ZMod 2) T ⬝ᵥ ind (ZMod 2) T = 1 := by
  rw [dot_ind, Finset.inter_self, hT]; rfl

/-- Complex neighbours (even intersection) are orthogonal. -/
theorem dot_triple_neighbors (S T : Finset (Fin h)) (hST : (S ∩ T).card % 2 = 0) :
    ind (ZMod 2) S ⬝ᵥ ind (ZMod 2) T = 0 := by
  rw [dot_ind, ZMod.natCast_eq_zero_iff]; omega

end Triples

/-! ## 3. Projections through orthonormal bases and the phase difference -/

section Proj

variable {m : ℕ}

lemma vmv (v y : (Fin m → ZMod 2)) : Matrix.vecMulVec v v *ᵥ y = (v ⬝ᵥ y) • v := by
  funext i
  simp only [Matrix.mulVec, Matrix.vecMulVec, dotProduct, Matrix.of_apply, Pi.smul_apply,
    smul_eq_mul, Finset.sum_mul, Finset.mul_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  ring

/-- `P_E x = ∑_{v ∈ B} (v · x) v` for an orthonormal basis `B` of `E`. -/
theorem proj_eq_sum (E : Submodule (ZMod 2) (Fin m → ZMod 2)) (hE : NondegOn (1 : Matrix (Fin m) (Fin m) _) E)
    (B : Finset (Fin m → ZMod 2)) (hBE : ∀ b ∈ B, b ∈ E) (hB : NetComplexOrtho.Orthonormal2 B)
    (hspan : Submodule.span (ZMod 2) (↑B : Set (Fin m → ZMod 2)) = E) (x : (Fin m → ZMod 2)) :
    proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) E *ᵥ x = ∑ v ∈ B, (v ⬝ᵥ x) • v := by
  have hP := proj_unique one_isSymm hE (∑ v ∈ B, Matrix.vecMulVec v v) ?_ ?_
  · rw [← hP, Matrix.sum_mulVec]
    refine Finset.sum_congr rfl fun v _ => ?_
    rw [vmv]
  · intro y
    rw [Matrix.sum_mulVec]
    exact E.sum_mem fun v hv => by
      rw [vmv]
      exact E.smul_mem _ (hBE v hv)
  · intro y
    rw [mem_orth_one]
    intro z hz
    rw [← hspan] at hz
    induction hz using Submodule.span_induction with
    | mem z hz =>
      rw [dotProduct_sub, Matrix.sum_mulVec, dotProduct_sum]
      rw [Finset.sum_eq_single z]
      · rw [vmv, dotProduct_smul, hB.1 z hz, smul_eq_mul, mul_one, dotProduct_comm, sub_self]
      · intro v hv hvz
        rw [vmv, dotProduct_smul, hB.2 z hz v hv (Ne.symm hvz), smul_zero]
      · intro h; exact absurd hz h
    | zero => simp
    | add a b _ _ ha hb => rw [add_dotProduct, ha, hb, add_zero]
    | smul c a _ ha => rw [smul_dotProduct, ha, smul_zero]

/-- The phase label `q_U(x) = wt(P_U x) mod 4`. -/
noncomputable def qL (U : Submodule (ZMod 2) (Fin m → ZMod 2)) (x : (Fin m → ZMod 2)) : ZMod 4 :=
  (NetComplexPhase.wt (proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) U *ᵥ x) : ZMod 4)

/-- **Phase difference along an edge.** For nested nondegenerate labels `U ≤ V` whose
residual `E = V ∩ U^⊥` has an orthonormal basis `B`,
`q_V(x) - q_U(x) ≡ ∑_{v ∈ B} wt(v) [v · x] (mod 4)`. -/
theorem qL_diff (U V : Submodule (ZMod 2) (Fin m → ZMod 2))
    (hU : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) U)
    (hV : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) V) (hUV : U ≤ V)
    (B : Finset (Fin m → ZMod 2)) (hBE : ∀ b ∈ B, b ∈ V ⊓ orth 1 U) (hB : NetComplexOrtho.Orthonormal2 B)
    (hspan : Submodule.span (ZMod 2) (↑B : Set (Fin m → ZMod 2)) = V ⊓ orth 1 U) (x : (Fin m → ZMod 2)) :
    qL V x - qL U x = ((∑ v ∈ B, (v ⬝ᵥ x).val * NetComplexPhase.wt v : ℕ) : ZMod 4) := by
  have hE := nondeg_diff one_isSymm hU hV hUV
  have hPV : proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) V *ᵥ x =
      proj 1 U *ᵥ x + ∑ v ∈ B, (v ⬝ᵥ x) • v := by
    rw [← proj_eq_sum _ hE B hBE hB hspan, ← proj_sub_proj one_isSymm hU hV hUV,
      Matrix.sub_mulVec]
    abel
  rw [qL, qL, hPV, wt_orth_sum]
  · ring
  · intro v hv
    exact (mem_orth_one.1 (hBE v hv).2) _ (proj_mulVec_mem one_isSymm hU x)
  · exact fun j hj k hk hjk => hB.2 j hj k hk hjk

/-- `q_0 = 0`. -/
theorem qL_bot (x : (Fin m → ZMod 2)) : qL ⊥ x = 0 := by
  have : proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) ⊥ *ᵥ x = 0 := by
    have h := proj_mulVec_mem (G := (1 : Matrix (Fin m) (Fin m) (ZMod 2))) one_isSymm
      (U := ⊥) (fun y hy _ => (Submodule.mem_bot _).1 hy) x
    exact (Submodule.mem_bot _).1 h
  rw [qL, this]
  simp [NetComplexPhase.wt, supp]

/-- `q_F = wt`. -/
theorem qL_top (x : (Fin m → ZMod 2)) : qL ⊤ x = (NetComplexPhase.wt x : ZMod 4) := by
  have hT : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) ⊤ := by
    intro y _ hy
    funext i
    have := hy (Pi.single i 1) Submodule.mem_top
    rw [bf_one, dotProduct_single, mul_one] at this
    exact this
  rw [qL, proj_mulVec_of_mem one_isSymm hT Submodule.mem_top]

/-- The projection onto a unit line: `P_{⟨u⟩} x = (u · x) u`. -/
theorem proj_line (u : (Fin m → ZMod 2)) (hu : u ⬝ᵥ u = 1) (x : (Fin m → ZMod 2)) :
    proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) (ZMod 2 ∙ u) *ᵥ x = (u ⬝ᵥ x) • u := by
  have hE : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) (ZMod 2 ∙ u) :=
    nondegOn_span_singleton _ (by rw [bf_one, hu]; decide)
  rw [proj_eq_sum _ hE {u} (by simp [Submodule.mem_span_singleton_self])
    ⟨by simp [hu], by simp⟩ (by simp), Finset.sum_singleton]

/-- `P_{⟨u⟩^⊥} x = x + (u · x) u` over `𝔽₂`. -/
theorem proj_line_perp (u : (Fin m → ZMod 2)) (hu : u ⬝ᵥ u = 1) (x : (Fin m → ZMod 2)) :
    proj (1 : Matrix (Fin m) (Fin m) (ZMod 2)) (orth 1 (ZMod 2 ∙ u)) *ᵥ x = x + (u ⬝ᵥ x) • u := by
  have hE : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) (ZMod 2 ∙ u) :=
    nondegOn_span_singleton _ (by rw [bf_one, hu]; decide)
  rw [proj_orth one_isSymm hE (by rw [det_one]; exact one_ne_zero), Matrix.sub_mulVec,
    Matrix.one_mulVec, proj_line u hu, sub_eq_add_neg]
  congr 1
  funext i
  simp only [Pi.neg_apply, Pi.smul_apply, smul_eq_mul]
  generalize u ⬝ᵥ x * u i = a
  exact (by decide : ∀ a : ZMod 2, -a = a) a

/-- **The pair `X_a → Y_a`.** For a unit vector `u` of odd weight (e.g. `u_a`, weight 27),
`q_{⟨u⟩^⊥}(x) - q_{⟨u⟩}(x) ≡ wt(x) + 2[u · x] (mod 4)`. -/
theorem qL_line_perp_diff (u : (Fin m → ZMod 2)) (hu : u ⬝ᵥ u = 1) (hodd : NetComplexPhase.wt u % 2 = 1) (x : (Fin m → ZMod 2)) :
    qL (orth 1 (ZMod 2 ∙ u)) x - qL (ZMod 2 ∙ u) x =
      ((NetComplexPhase.wt x + 2 * (u ⬝ᵥ x).val : ℕ) : ZMod 4) := by
  rw [qL, qL, proj_line_perp u hu, proj_line u hu]
  set c := u ⬝ᵥ x
  -- `x = (x + c u) + c u` with orthogonal summands
  have horth : (x + c • u) ⬝ᵥ (c • u) = 0 := by
    simp only [add_dotProduct, dotProduct_smul, smul_dotProduct, smul_eq_mul, hu, mul_one]
    rw [dotProduct_comm x u]
    show c * (c + c) = 0
    rw [NetComplexOrtho.zmod2_add_self, mul_zero]
  have hx := wt_add_mod4 (x + c • u) (c • u) horth
  have hxx : x + c • u + c • u = x := by
    rw [add_assoc, ← add_smul]
    have : c + c = 0 := NetComplexOrtho.zmod2_add_self c
    rw [this, zero_smul, add_zero]
  rw [hxx] at hx
  push_cast
  rw [hx, wt_smul]
  push_cast
  obtain ⟨k, hk⟩ : ∃ k, NetComplexPhase.wt u = 2 * k + 1 := ⟨NetComplexPhase.wt u / 2, by omega⟩
  rw [hk]
  push_cast
  ring_nf
  have h4 : (4 : ZMod 4) = 0 := rfl
  rcases NetComplexOrtho.zmod2_cases c with hc | hc
  · rw [hc]; simp
  · rw [hc]; simp; ring_nf; linear_combination (-1 - (k : ZMod 4)) * h4

end Proj

end NetComplexLabels

end