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

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

import Definitions.Def_IntMul_Kappa_K_Defs7

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.NetComplexP8Main
set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option synthInstance.maxSize 512

namespace NetComplexP8

open Matrix Finset Module NetLabels NetComplexOrtho NetComplex AModel AModelRat

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

variable (ind) in
/-- The triple of a gate name (`∅` for central gates, where it is unused). -/
def tri : Option T → Finset (Fin h)
  | some t => ind t
  | none => ∅

/-- Physical time of row `r` at stage `j` (stage 2 runs the inverse schedule backwards). -/
def time (j : Fin 3) (r : Fin 8) : ℕ := if j = 1 then 7 - r.val else r.val

/-- The `B`-factor of the table-(6) label at time `r`. -/
def Ψ1f (r : ℕ) (S : Finset (Fin h)) : Submodule (ZMod 2) (Vh h) := if r = 0 then L1 S else ⊤

/-- The `P`-factor of the table-(6) label at time `r`. -/
def Ψ2f : ℕ → Finset (Fin h) → Submodule (ZMod 2) (Vh h)
  | 2, S => L1 S
  | 3, _ => ⊤
  | 5, S => Pp S
  | 6, _ => ⊤
  | 7, _ => ⊤
  | _, _ => ⊥

variable (ind) in
/-- **Table (6)**: the label of every gate of the corrected complex network (`none` = the final
sign gate on the `X` outputs, label `F`). -/
def labS : Option (GName T) → Submodule (ZMod 2) (Vc h)
  | none => ⊤
  | some (j, p, (r, o)) =>
    lab j (ind p.1) (ind p.2) (Ψ1f (NetComplexP8.time j r) (tri ind o)) (Ψ2f (NetComplexP8.time j r) (tri ind o))

variable (ind) in
/-- `u_a = t_{a₁} ⊗ t_{a₂} ⊗ t_{a₃}`. -/
def uA (a : T × T × T) : Vc h := t3 (tt (ind a.1)) (tt (ind a.2.1)) (tt (ind a.2.2))

variable (ind) in
/-- Source labels: `U_a` on `X_a`, zero elsewhere. -/
def MinS : Wr ind → Submodule (ZMod 2) (Vc h)
  | Sum.inl a => Submodule.span (ZMod 2) {NetComplexP8.uA ind a}
  | Sum.inr _ => ⊥

variable (ind) in
/-- Sink labels: `U_a^⊥` on `Y_a`, `F` elsewhere. -/
def MoutS : Wr ind → Submodule (ZMod 2) (Vc h)
  | Sum.inr (Sum.inl a) => NetLabels.orth 1 (Submodule.span (ZMod 2) {NetComplexP8.uA ind a})
  | _ => ⊤

lemma pj_zero (a : T × T × T) : pj 0 a = (a.2.1, a.2.2) := rfl
lemma cj_zero (a : T × T × T) : cj 0 a = a.1 := rfl
lemma pj_one (a : T × T × T) : pj 1 a = (a.1, a.2.2) := rfl
lemma cj_one (a : T × T × T) : cj 1 a = a.2.1 := rfl
lemma pj_two (a : T × T × T) : pj 2 a = (a.1, a.2.1) := rfl
lemma cj_two (a : T × T × T) : cj 2 a = a.2.2 := rfl

/-! ## Helpers -/

lemma out3 (hh : 7 ≤ h) {S : Finset (Fin h)} (hS : S.card = 3) : ∃ k, k ∉ S :=
  exists_out S (by omega)

lemma HasON_Pp' (hh : 7 ≤ h) {S : Finset (Fin h)} (hS : S.card = 3) : HasON (Pp S) := by
  obtain ⟨k, hk⟩ := out3 hh hS
  exact HasON_Pp hS hk

lemma HasON_lab' (hh : 7 ≤ h) {j : Fin 3} {S1 S2 : Finset (Fin h)}
    {Ψ1 Ψ2 : Submodule (ZMod 2) (Vh h)} (hS1 : S1.card = 3) (hS2 : S2.card = 3) (h1 : HasON Ψ1)
    (h2 : HasON Ψ2) : HasON (lab j S1 S2 Ψ1 Ψ2) := by
  obtain ⟨k1, hk1⟩ := out3 hh hS1
  obtain ⟨k2, hk2⟩ := out3 hh hS2
  exact HasON_lab hS1 hS2 j hk1 hk2 h1 h2

lemma HasON_topC : HasON (⊤ : Submodule (ZMod 2) (Vc h)) :=
  T3_top ▸ HasON_T3 HasON_top HasON_top HasON_top

lemma upW {m : ℕ} {U V : Submodule (ZMod 2) (Fin m → ZMod 2)} (hU : HasON U) (hV : HasON V)
    (hi : IncW U V) : Up U V := ⟨hU.nondegOn, hV.nondegOn, hi⟩

lemma upRefl {m : ℕ} {U : Submodule (ZMod 2) (Fin m → ZMod 2)} (hU : HasON U) : Up U U :=
  upW hU hU (incW_refl U)

lemma HasON_u (hh : 7 ≤ h) {S1 S2 S3 : Finset (Fin h)} (h1 : S1.card = 3) (h2 : S2.card = 3)
    (h3 : S3.card = 3) : HasON (Submodule.span (ZMod 2) {t3 (tt S1) (tt S2) (tt S3)}) := by
  rw [srcX h1 h2 h3]; exact HasON_lab' hh h2 h3 HasON_top (HasON_L1 h1)

lemma HasON_uperp (hh : 7 ≤ h) {S1 S2 S3 : Finset (Fin h)} (h1 : S1.card = 3) (h2 : S2.card = 3)
    (h3 : S3.card = 3) :
    HasON (NetLabels.orth 1 (Submodule.span (ZMod 2) {t3 (tt S1) (tt S2) (tt S3)})) := by
  rw [sinkY h1 h2 h3]; exact HasON_lab' hh h1 h2 HasON_top (HasON_Pp' hh h3)

lemma HasON_uA (hcard : ∀ t, (ind t).card = 3) (hh : 7 ≤ h) (a : T × T × T) :
    HasON (Submodule.span (ZMod 2) {NetComplexP8.uA ind a}) := HasON_u hh (hcard _) (hcard _) (hcard _)

lemma HasON_uAperp (hcard : ∀ t, (ind t).card = 3) (hh : 7 ≤ h) (a : T × T × T) :
    HasON (NetLabels.orth 1 (Submodule.span (ZMod 2) {NetComplexP8.uA ind a})) :=
  HasON_uperp hh (hcard _) (hcard _) (hcard _)

/-! ## Generic chains -/

theorem chainOK_mono {M : Type*} {P Q : M → M → Prop} (hPQ : ∀ a b, P a b → Q a b) :
    ∀ (s : M) (xs : List M) (e : M), chainOK P s xs e → chainOK Q s xs e := by
  intro s xs
  induction xs generalizing s with
  | nil => intro e h; exact hPQ _ _ h
  | cons x xs ih => intro e h; exact ⟨hPQ _ _ h.1, ih x e h.2⟩

theorem chainOK_map {M N : Type*} (f : M → N) (P : N → N → Prop) :
    ∀ (s : M) (xs : List M) (e : M),
      chainOK P (f s) (xs.map f) (f e) ↔ chainOK (fun a b => P (f a) (f b)) s xs e := by
  intro s xs
  induction xs generalizing s with
  | nil => intro e; exact Iff.rfl
  | cons x xs ih => intro e; simp only [List.map_cons, chainOK, ih]

theorem chain2_map {M N β : Type*} [AddCommMonoid β] (f : M → N) (F : N → N → β) :
    ∀ (s : M) (xs : List M) (e : M),
      chain2 F (f s) (xs.map f) (f e) = chain2 (fun a b => F (f a) (f b)) s xs e := by
  intro s xs
  induction xs generalizing s with
  | nil => intro e; rfl
  | cons x xs ih => intro e; simp only [List.map_cons, chain2, ih]

/-- Along increasing edges the residual dimensions telescope. -/
theorem chain2_up {m : ℕ} :
    ∀ (s : Submodule (ZMod 2) (Fin m → ZMod 2)) (xs : List (Submodule (ZMod 2) (Fin m → ZMod 2)))
      (e : Submodule (ZMod 2) (Fin m → ZMod 2)), chainOK (fun V U => Up U V) s xs e →
      ((chain2 Fd s xs e : ℕ) : ℤ) = finrank (ZMod 2) e - finrank (ZMod 2) s := by
  intro s xs
  induction xs generalizing s with
  | nil => intro e h; exact Fd_up h
  | cons x xs ih =>
    intro e h
    simp only [chain2]
    push_cast
    rw [Fd_up h.1, ih x e h.2]
    ring

lemma up_edge {m : ℕ} {U V : Submodule (ZMod 2) (Fin m → ZMod 2)} (h : Up U V) : EdgeOK V U :=
  Or.inl h

/-- A side wire joining the `Y`-triple `y` and the `X`-triple `x` (neighbours). -/
theorem side_generic (hh : 7 ≤ h) (j : Fin 3) {S1 S2 x y : Finset (Fin h)} (hS1 : S1.card = 3)
    (hS2 : S2.card = 3) (hx : x.card = 3) (hy : y.card = 3) (hxy : tt y ⬝ᵥ tt x = 0) :
    chainOK (fun V U => Up U V) ⊥
      [lab j S1 S2 (L1 y) ⊥, lab j S1 S2 ⊤ (L1 x), lab j S1 S2 ⊤ (Pp y), lab j S1 S2 ⊤ ⊤] ⊤ := by
  obtain ⟨k1, hk1⟩ := out3 hh hS1
  obtain ⟨k2, hk2⟩ := out3 hh hS2
  obtain ⟨k, hk⟩ := exists_out (x ∪ y) (by
    have := Finset.card_union_le x y; omega)
  have hkx : k ∉ x := fun e => hk (Finset.mem_union_left _ e)
  have hky : k ∉ y := fun e => hk (Finset.mem_union_right _ e)
  have i1 : IncW ⊥ (lab j S1 S2 (L1 y) ⊥) := by
    have := inc_be hS1 hS2 (Ψ2 := ⊥) j bot_le (y := tt y) (tt_mem_L1 _) (tt_norm hy)
      (orth_bot _) hk1
    rwa [lab_bot] at this
  simp only [chainOK]
  refine ⟨upW HasON_bot ?_ i1,
    upW ?_ ?_ (inc_pi hS1 hS2 j le_top bot_le (y := tt x) (tt_mem_L1 _) (tt_norm hx) (orth_bot _)),
    upW ?_ ?_ (inc_pi hS1 hS2 j le_rfl (L1_le_Pp hxy) (y := ek k) (ek_mem_Pp hky) (dot_ek_ek _)
      (orth_L1 (dot_tt_ek hkx))),
    upW ?_ ?_ (inc_pi hS1 hS2 j le_rfl le_top (y := tt y) Submodule.mem_top (tt_norm hy)
      (orth_Pp y)),
    upW ?_ HasON_topC (inc_sink hS1 hS2 j hk1 hk2)⟩
  · exact HasON_lab' hh hS1 hS2 (HasON_L1 hy) HasON_bot
  · exact HasON_lab' hh hS1 hS2 (HasON_L1 hy) HasON_bot
  · exact HasON_lab' hh hS1 hS2 HasON_top (HasON_L1 hx)
  · exact HasON_lab' hh hS1 hS2 HasON_top (HasON_L1 hx)
  · exact HasON_lab' hh hS1 hS2 HasON_top (HasON_Pp' hh hy)
  · exact HasON_lab' hh hS1 hS2 HasON_top (HasON_Pp' hh hy)
  · exact HasON_lab' hh hS1 hS2 HasON_top HasON_top
  · exact HasON_lab' hh hS1 hS2 HasON_top HasON_top

/-- A central wire: the only decreasing edge is time 3 → 4, losing exactly `h`. -/
theorem center_generic (hh : 7 ≤ h) (j : Fin 3) {S1 S2 : Finset (Fin h)} (hS1 : S1.card = 3)
    (hS2 : S2.card = 3) :
    chainOK EdgeOK ⊥ [lab j S1 S2 ⊤ ⊥, lab j S1 S2 ⊤ ⊤, lab j S1 S2 ⊤ ⊥, lab j S1 S2 ⊤ ⊤] ⊤ ∧
      ((chain2 Fd ⊥ [lab j S1 S2 ⊤ ⊥, lab j S1 S2 ⊤ ⊤, lab j S1 S2 ⊤ ⊥, lab j S1 S2 ⊤ ⊤] ⊤ : ℕ) : ℤ) =
        h ^ 3 + 2 * h := by
  obtain ⟨k1, hk1⟩ := out3 hh hS1
  obtain ⟨k2, hk2⟩ := out3 hh hS2
  have H1 := HasON_lab' hh hS1 hS2 (j := j) HasON_top HasON_bot
  have H3 := HasON_lab' hh hS1 hS2 (j := j) HasON_top HasON_top
  have hA : Up ⊥ (lab j S1 S2 ⊤ ⊥) := by
    have := inc_be hS1 hS2 (Ψ2 := ⊥) j bot_le (y := ek k1) Submodule.mem_top (dot_ek_ek _)
      (orth_bot _) hk1
    rw [lab_bot] at this
    exact upW HasON_bot H1 this
  have hB : Up (lab j S1 S2 ⊤ ⊥) (lab j S1 S2 ⊤ ⊤) :=
    upW H1 H3 (inc_pi hS1 hS2 j le_rfl bot_le (y := ek k1) Submodule.mem_top (dot_ek_ek _)
      (orth_bot _))
  have hC : Up (lab j S1 S2 ⊤ ⊤) ⊤ := upW H3 HasON_topC (inc_sink hS1 hS2 j hk1 hk2)
  refine ⟨⟨Or.inl hA, Or.inl hB, Or.inr hB, Or.inl hB, Or.inl hC⟩, ?_⟩
  simp only [chain2]
  push_cast
  rw [Fd_up hA, Fd_up hB, Fd_down hB, Fd_up hC, finrank_lab_center hS1 hS2 j, finrank_top,
    finrank_fin_fun, finrank_bot]
  push_cast
  ring

/-! ## Lemma 6, wire by wire -/

variable (hcard : ∀ t, (ind t).card = 3) (hh : 7 ≤ h)
include hcard hh

/-- **`X_a`**: every edge increases (the labels of §3.3 and table (6)). -/
theorem chain_X (a : T × T × T) :
    chainOK (fun V U => Up U V) (MinS ind (wX a))
      ((namesOn (wX a) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (wX a)) := by
  rw [namesOn_cxFix, names_X]
  (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
         List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
         time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
         if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
         Nat.reduceMod, Nat.reduceSub, List.append_nil])
     (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
  simp only [chainOK]
  obtain ⟨k1, hk1⟩ := out3 hh (hcard a.1)
  obtain ⟨k2, hk2⟩ := out3 hh (hcard a.2.1)
  obtain ⟨k3, hk3⟩ := out3 hh (hcard a.2.2)
  refine ⟨upW ?_ ?_ (incW_of_eq (srcX (hcard _) (hcard _) (hcard _))),
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 0 le_rfl le_top (y := ek k1) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk1))),
    upRefl ?_, upRefl ?_,
    upW ?_ ?_ (bX01 (hcard _) (hcard _) (hcard _) hk1 hk2),
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 1 le_rfl le_top (y := ek k2) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk2))),
    upRefl ?_, upRefl ?_,
    upW ?_ ?_ (bX12 (hcard _) (hcard _) (hcard _) hk1 hk3),
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 2 le_rfl le_top (y := ek k3) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk3))),
    upRefl ?_, upRefl ?_,
    upW ?_ ?_ (incW_of_eq (lab2_top (hcard _) (hcard _))), upRefl ?_⟩
  all_goals (first
             | with_reducible exact HasON_topC
             | with_reducible exact HasON_bot
             | with_reducible exact HasON_uA hcard hh _
             | with_reducible exact HasON_uAperp hcard hh _
             |
               (with_reducible refine HasON_lab' hh (hcard _) (hcard _) ?_ ?_) <;>
                 first
                 | with_reducible exact HasON_top
                 | with_reducible exact HasON_bot
                 | with_reducible exact HasON_L1 (hcard _)
                 | with_reducible exact HasON_Pp' hh (hcard _))

/-- **`Y_a`**: every edge increases. -/
theorem chain_Y (a : T × T × T) :
    chainOK (fun V U => Up U V) (MinS ind (wY a))
      ((namesOn (wY a) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (wY a)) := by
  rw [namesOn_cxFix, names_Y]
  (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
         List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
         time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
         if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
         Nat.reduceMod, Nat.reduceSub, List.append_nil])
     (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
  simp only [chainOK]
  obtain ⟨k1, hk1⟩ := out3 hh (hcard a.1)
  obtain ⟨k2, hk2⟩ := out3 hh (hcard a.2.1)
  obtain ⟨k3, hk3⟩ := out3 hh (hcard a.2.2)
  refine ⟨upW ?_ ?_ (incW_of_eq (srcY (hcard _) (hcard _) (hcard _))),
    upW ?_ ?_ (inc_be (hcard _) (hcard _) 0 le_top (y := ek k1) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk1)) hk2),
    upRefl ?_,
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 0 le_rfl bot_le (y := ek k1) (ek_mem_Pp hk1)
      (dot_ek_ek _) (orth_bot _)),
    upW ?_ ?_ (incW_of_eq (bY01 (hcard _) (hcard _) (hcard _))),
    upW ?_ ?_ (inc_be (hcard _) (hcard _) 1 le_top (y := ek k2) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk2)) hk1),
    upRefl ?_,
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 1 le_rfl bot_le (y := ek k2) (ek_mem_Pp hk2)
      (dot_ek_ek _) (orth_bot _)),
    upW ?_ ?_ (incW_of_eq (bY12 (hcard _) (hcard _) (hcard _))),
    upW ?_ ?_ (inc_be (hcard _) (hcard _) 2 le_top (y := ek k3) Submodule.mem_top
      (dot_ek_ek _) (orth_L1 (dot_tt_ek hk3)) hk1),
    upRefl ?_,
    upW ?_ ?_ (inc_pi (hcard _) (hcard _) 2 le_rfl bot_le (y := ek k3) (ek_mem_Pp hk3)
      (dot_ek_ek _) (orth_bot _)),
    upW ?_ ?_ (incW_of_eq (sinkY (hcard _) (hcard _) (hcard _)).symm)⟩
  all_goals (first
             | with_reducible exact HasON_topC
             | with_reducible exact HasON_bot
             | with_reducible exact HasON_uA hcard hh _
             | with_reducible exact HasON_uAperp hcard hh _
             |
               (with_reducible refine HasON_lab' hh (hcard _) (hcard _) ?_ ?_) <;>
                 first
                 | with_reducible exact HasON_top
                 | with_reducible exact HasON_bot
                 | with_reducible exact HasON_L1 (hcard _)
                 | with_reducible exact HasON_Pp' hh (hcard _))

omit hcard hh in
lemma nb_dot (n : Nb ind) : tt (ind n.1.1) ⬝ᵥ tt (ind n.1.2) = 0 :=
  NetComplexLabels.dot_triple_neighbors _ _ n.2.2

omit hcard hh in
lemma nb_dot' (n : Nb ind) : tt (ind n.1.2) ⬝ᵥ tt (ind n.1.1) = 0 := by
  rw [dotProduct_comm]; exact nb_dot n

/-- **Side wires**: every edge increases. -/
theorem chain_S (j : Fin 3) (p : T × T) (n : Nb ind) :
    chainOK (fun V U => Up U V) (MinS ind (wS j p n))
      ((namesOn (wS j p n) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (wS j p n)) := by
  rw [namesOn_cxFix, names_S]
  rcases fin3_cases j with rfl | rfl | rfl
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact side_generic hh 0 (hcard _) (hcard _) (hcard _) (hcard _) (nb_dot n)
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact side_generic hh 1 (hcard _) (hcard _) (hcard _) (hcard _) (nb_dot' n)
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact side_generic hh 2 (hcard _) (hcard _) (hcard _) (hcard _) (nb_dot n)

/-- **Central wires**: comparable labels, one decreasing edge (3 → 4), count `m + 2h`. -/
theorem chain_C (j : Fin 3) (p : T × T) (o : Option (Fin h)) :
    chainOK EdgeOK (MinS ind (wC j p o))
      ((namesOn (wC j p o) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (wC j p o)) ∧
    ((chain2 Fd (MinS ind (wC j p o))
      ((namesOn (wC j p o) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (wC j p o)) : ℕ) : ℤ) =
        h ^ 3 + 2 * h := by
  rw [namesOn_cxFix, names_C]
  rcases fin3_cases j with rfl | rfl | rfl
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact center_generic hh 0 (hcard _) (hcard _)
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact center_generic hh 1 (hcard _) (hcard _)
  · (( (simp only [List.map_append, List.map_cons, List.map_nil, List.reverse_cons, List.reverse_nil,
           List.nil_append, List.cons_append, List.singleton_append, labS, MinS, MoutS, wX, wY, wS, wC,
           time, tri, pj_zero, cj_zero, pj_one, cj_one, pj_two, cj_two, Fin.isValue, Fin.reduceEq,
           if_true, if_false, Fin.val_zero, Fin.val_one, Fin.val_two, Fin.coe_ofNat_eq_mod,
           Nat.reduceMod, Nat.reduceSub, List.append_nil])
       (simp only [Ψ1f, Ψ2f, OfNat.ofNat_ne_zero, one_ne_zero, if_false, if_true, Nat.reduceEqDiff])))
    exact center_generic hh 2 (hcard _) (hcard _)

/-! ## Terminal dimensions and the count -/

omit hh in
lemma uA_norm (a : T × T × T) : NetComplexP8.uA ind a ⬝ᵥ NetComplexP8.uA ind a = 1 := by
  simp [NetComplexP8.uA, t3_dot, tt_norm (hcard _)]

omit hcard hh in
lemma finrank_topC : finrank (ZMod 2) ↥(⊤ : Submodule (ZMod 2) (Vc h)) = h ^ 3 := by
  rw [finrank_top, finrank_fin_fun]

omit hh in
lemma finrank_uA (a : T × T × T) :
    finrank (ZMod 2) ↥(Submodule.span (ZMod 2) {NetComplexP8.uA ind a}) = 1 :=
  finrank_span_singleton fun e => by
    have := uA_norm hcard a
    rw [e, zero_dotProduct] at this
    exact zero_ne_one this

lemma finrank_uAperp (a : T × T × T) :
    finrank (ZMod 2) ↥(NetLabels.orth 1 (Submodule.span (ZMod 2) {NetComplexP8.uA ind a})) = h ^ 3 - 1 := by
  have := finrank_diff NetComplexLabels.one_isSymm (HasON_uA hcard hh a).nondegOn HasON_topC.nondegOn le_top
  rw [top_inf_eq, finrank_uA hcard a, finrank_topC] at this
  omega

lemma count_X (a : T × T × T) :
    ((chain2 Fd (MinS ind (wX a)) ((namesOn (wX a) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (wX a)) : ℕ) : ℤ) = (h : ℤ) ^ 3 - 1 := by
  rw [chain2_up _ _ _ (NetComplexP8.chain_X hcard hh a)]
  rw [show MoutS ind (wX a) = ⊤ from rfl,
    show MinS ind (wX a) = Submodule.span (ZMod 2) {NetComplexP8.uA ind a} from rfl,
    finrank_topC, finrank_uA hcard a]
  push_cast; ring

lemma count_Y (a : T × T × T) :
    ((chain2 Fd (MinS ind (wY a)) ((namesOn (wY a) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (wY a)) : ℕ) : ℤ) = (h : ℤ) ^ 3 - 1 := by
  rw [chain2_up _ _ _ (NetComplexP8.chain_Y hcard hh a)]
  rw [show MoutS ind (wY a) = NetLabels.orth 1 (Submodule.span (ZMod 2) {NetComplexP8.uA ind a}) from rfl,
    show MinS ind (wY a) = ⊥ from rfl, finrank_uAperp hcard hh a, finrank_bot]
  have : 1 ≤ h ^ 3 := Nat.one_le_pow _ _ (by omega)
  push_cast [this]; ring

lemma count_S (j : Fin 3) (p : T × T) (n : Nb ind) :
    ((chain2 Fd (MinS ind (wS j p n)) ((namesOn (wS j p n) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (wS j p n)) : ℕ) : ℤ) = (h : ℤ) ^ 3 := by
  rw [chain2_up _ _ _ (NetComplexP8.chain_S hcard hh j p n)]
  rw [show MoutS ind (wS j p n) = ⊤ from rfl, show MinS ind (wS j p n) = ⊥ from rfl,
    finrank_topC, finrank_bot]
  push_cast; ring

/-- **Lemma 6, the count (general `h ≥ 7`, any card-3 family)**:
`Σ_e |Δ dim| = 2N(m − 1) + I (z v m + c (m + 2h)) = W m − 2N + 2L` with `N = v³`, `m = h³`,
`I = 3v²`, `z v = |Nb|`, `c = h + 1`, `L = I c h`. -/
theorem count_total :
    ((∑ w : Wr ind, chain2 Fd (MinS ind w) ((namesOn w (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind w) : ℕ) : ℤ) =
      2 * (Fintype.card T : ℤ) ^ 3 * ((h : ℤ) ^ 3 - 1) +
        3 * (Fintype.card T : ℤ) ^ 2 * ((Fintype.card (Nb ind) : ℤ) * (h : ℤ) ^ 3 +
          ((h : ℤ) + 1) * ((h : ℤ) ^ 3 + 2 * h)) := by
  push_cast
  simp only [Fintype.sum_sum_type]
  have cX : ∀ a : T × T × T, ((chain2 Fd (MinS ind (Sum.inl a))
      ((namesOn (Sum.inl a) (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind (Sum.inl a)) : ℕ) : ℤ)
      = (h : ℤ) ^ 3 - 1 := count_X hcard hh
  have cY : ∀ a : T × T × T, ((chain2 Fd (MinS ind (Sum.inr (Sum.inl a)))
      ((namesOn (Sum.inr (Sum.inl a)) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (Sum.inr (Sum.inl a))) : ℕ) : ℤ) = (h : ℤ) ^ 3 - 1 := count_Y hcard hh
  have cS : ∀ x : Fin 3 × (T × T) × Nb ind, ((chain2 Fd (MinS ind (Sum.inr (Sum.inr (Sum.inl x))))
      ((namesOn (Sum.inr (Sum.inr (Sum.inl x))) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (Sum.inr (Sum.inr (Sum.inl x)))) : ℕ) : ℤ) = (h : ℤ) ^ 3 :=
    fun x => count_S hcard hh x.1 x.2.1 x.2.2
  have cC : ∀ x : Fin 3 × (T × T) × Option (Fin h),
      ((chain2 Fd (MinS ind (Sum.inr (Sum.inr (Sum.inr x))))
      ((namesOn (Sum.inr (Sum.inr (Sum.inr x))) (cxFixNamed ℂ ind)).map (labS ind))
      (MoutS ind (Sum.inr (Sum.inr (Sum.inr x)))) : ℕ) : ℤ) = (h : ℤ) ^ 3 + 2 * h :=
    fun x => (NetComplexP8.chain_C hcard hh x.1 x.2.1 x.2.2).2
  simp only [cX, cY, cS, cC, Finset.sum_const, Finset.card_univ, Fintype.card_prod,
    Fintype.card_fin, Fintype.card_option, nsmul_eq_mul]
  push_cast
  ring

end NetComplexP8

end

section
-- Source module: Solutions.NetComplexP8Final
/-!
# Proposition 8 (complex network, binary phase interface), assembled

The corrected complex network `cxFixNamed` (Lemma 5, physical gate order) carries the labels of
table (6) (`labS`). To use the generic network bookkeeping (`FramesOK2`, `frameSum2`, which
need an additive group of labels) we label the gates by `FreeAddGroup.of (labS g)` and decode
with `dec` (`dec ∘ of = id`); relabelling by `q_U = wt ∘ P_U (mod 4)` gives exactly the
phase-frame network `cxFixGatesL ℂ ind (q ∘ labS)` of `NetComplexProp8`.

* `prop8_edges`: every edge of the network joins comparable nondegenerate labels whose residual
  has an orthonormal basis `B` of size `|Δ dim|`, and the edge's phase-frame difference
  `C_V C_U⁻¹` is a product of one translation kernel `aI + bX_v` or its inverse per `v ∈ B`.
* `prop8_count_general`: `Σ_e |B_e| = 2N(m−1) + I(zvm + c(m+2h))` for general `h ≥ 7`.
* `prop8` (`h = 100`): `W_c = 1873807244643542670000`, `Σ_e |B_e| = s_c =
  1873807244636671267308000000 < W_c m`, `wt u_a = 27`, and every route is `C^{⊗m}` (after the
  `Z` correction on `X_a → Y_a`).
-/

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

namespace NetComplexP8

open Matrix Finset Module NetLabels NetComplexOrtho NetComplex AModel AModelRat
  NetComplexPhase NetComplexLabels NetComplexInterface Complex

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

/-! ## Weight of `u_a` -/

lemma val_mul_zmod2 (a b : ZMod 2) : (a * b).val = a.val * b.val := by
  revert a b; decide

theorem wt_t3 (x y z : Vh h) : NetComplexPhase.wt (t3 x y z) = NetComplexPhase.wt x * (NetComplexPhase.wt y * NetComplexPhase.wt z) := by
  rw [wt_eq_sum, wt_eq_sum, wt_eq_sum, wt_eq_sum]
  have e : ∑ i : Fin (h ^ 3), ZMod.val (t3 x y z i) =
      ∑ c : Fin h × Fin h × Fin h, ZMod.val (x c.1) * (ZMod.val (y c.2.1) * ZMod.val (z c.2.2)) :=
    Fintype.sum_equiv (e3 h).symm _ _ (fun i => by simp [t3, tp, val_mul_zmod2])
  rw [e]
  simp only [Fintype.sum_prod_type]
  rw [Finset.sum_mul_sum, Finset.sum_mul]
  simp only [Finset.mul_sum]

theorem wt_tt (S : Finset (Fin h)) : NetComplexPhase.wt (tt S) = S.card := by
  rw [wt_eq_sum]
  have : ∀ i, (tt S i).val = if i ∈ S then 1 else 0 := by
    intro i; simp only [tt, NetLabels.ind]; split_ifs <;> rfl
  simp only [this, Finset.sum_boole, Finset.filter_mem_eq_inter, Finset.univ_inter]
  simp

/-- `wt u_a = 3³ = 27`. -/
theorem wt_uA (hcard : ∀ t, (ind t).card = 3) (a : T × T × T) : NetComplexPhase.wt (NetComplexP8.uA ind a) = 27 := by
  rw [NetComplexP8.uA, wt_t3, wt_tt, wt_tt, wt_tt, hcard, hcard, hcard]

/-! ## The network with subspace labels -/

/-- Labels as an additive group (free on the subspaces). -/
abbrev LabG (h : ℕ) := FreeAddGroup (Submodule (ZMod 2) (Vc h))

/-- Decoding a label. -/
noncomputable def dec : LabG h → Submodule (ZMod 2) (Vc h) := Function.invFun FreeAddGroup.of

@[simp] lemma dec_of (U : Submodule (ZMod 2) (Vc h)) : dec (FreeAddGroup.of U) = U :=
  Function.leftInverse_invFun FreeAddGroup.of_injective U

variable (ind) in
/-- The corrected complex network with the gate labels of table (6). -/
noncomputable def gatesF : List (NGate (Wr ind) ℂ (LabG h)) :=
  labelled (fun n => FreeAddGroup.of (labS ind n)) (cxFixNamed ℂ ind)

variable (ind) in
noncomputable def MinF (w : Wr ind) : LabG h := FreeAddGroup.of (MinS ind w)
variable (ind) in
noncomputable def MoutF (w : Wr ind) : LabG h := FreeAddGroup.of (MoutS ind w)

lemma labelsOn_gatesF (w : Wr ind) :
    NetProp7.labelsOn w (gatesF ind) =
      ((namesOn w (cxFixNamed ℂ ind)).map (labS ind)).map FreeAddGroup.of := by
  rw [gatesF, NetComplexP8.labelsOn_labelled, List.map_map]; rfl

/-- The per-edge statement of Proposition 8 (head `V`, tail `U`). -/
def EdgeP (V U : Submodule (ZMod 2) (Vc h)) : Prop :=
  EdgeOK V U ∧ ∃ B : Finset (Vc h), Orthonormal2 B ∧
    (Submodule.span (ZMod 2) ↑B = V ⊓ orth 1 U ∨ Submodule.span (ZMod 2) ↑B = U ⊓ orth 1 V) ∧
    B.card = Fd V U ∧
    ∃ L : List (ℤ × Vc h), L.map Prod.snd = B.toList ∧ (∀ p ∈ L, p.1 = 1 ∨ p.1 = -1) ∧
      ∀ g, PhiQ (qL V - qL U) g = L.foldr (fun p g' => transK p.1 p.2 g') g

variable (hcard : ∀ t, (ind t).card = 3) (hh : 7 ≤ h)
include hcard hh

/-- **Lemma 6 (edges).** Every edge joins comparable nondegenerate labels with nonalternating
(or zero) residual. -/
theorem lemma6_edges :
    FramesOK2 (fun a b => EdgeOK (dec a) (dec b)) (gatesF ind) (MinF ind) (MoutF ind) := by
  rw [framesOK2_iff_chain]
  intro w
  rw [labelsOn_gatesF, show MinF ind w = FreeAddGroup.of (MinS ind w) from rfl,
    show MoutF ind w = FreeAddGroup.of (MoutS ind w) from rfl, chainOK_map]
  simp only [dec_of]
  rcases w with a | a | x | x
  · exact chainOK_mono (fun _ _ e => up_edge e) _ _ _ (NetComplexP8.chain_X hcard hh a)
  · exact chainOK_mono (fun _ _ e => up_edge e) _ _ _ (NetComplexP8.chain_Y hcard hh a)
  · exact chainOK_mono (fun _ _ e => up_edge e) _ _ _ (NetComplexP8.chain_S hcard hh x.1 x.2.1 x.2.2)
  · exact (NetComplexP8.chain_C hcard hh x.1 x.2.1 x.2.2).1

/-- **Proposition 8 (edges).** Every frame change of the network is a product of translation
kernels, one per vector of an orthonormal basis of the edge residual. -/
theorem prop8_edges :
    FramesOK2 (fun a b => EdgeP (dec a) (dec b)) (gatesF ind) (MinF ind) (MoutF ind) :=
  framesOK2_mono (fun _ _ e => ⟨e, edge_kernel e⟩) _ _ _ (lemma6_edges hcard hh)

/-- **The count (general `h`).** -/
theorem prop8_count_general :
    ((frameSum2 (fun a b => Fd (dec a) (dec b)) (gatesF ind) (MinF ind) (MoutF ind) : ℕ) : ℤ) =
      2 * (Fintype.card T : ℤ) ^ 3 * ((h : ℤ) ^ 3 - 1) +
        3 * (Fintype.card T : ℤ) ^ 2 * ((Fintype.card (Nb ind) : ℤ) * (h : ℤ) ^ 3 +
          ((h : ℤ) + 1) * ((h : ℤ) ^ 3 + 2 * h)) := by
  rw [frameSum2_eq_chain]
  have e : ∀ w, chain2 (fun a b => Fd (dec a) (dec b)) (MinF ind w)
      (NetProp7.labelsOn w (gatesF ind)) (MoutF ind w) =
      chain2 Fd (MinS ind w) ((namesOn w (cxFixNamed ℂ ind)).map (labS ind)) (MoutS ind w) := by
    intro w
    rw [labelsOn_gatesF, show MinF ind w = FreeAddGroup.of (MinS ind w) from rfl,
      show MoutF ind w = FreeAddGroup.of (MoutS ind w) from rfl, chain2_map]
    simp only [dec_of]
  simp only [e]
  exact count_total hcard hh

omit hcard hh in
/-- Relabelling by phases gives the phase network of `NetComplexProp8`. -/
theorem gatesF_phase :
    mapG (fun a => qL (dec a)) (gatesF ind) = cxFixGatesL ℂ ind (fun n => qL (labS ind n)) := by
  simp only [mapG, gatesF, cxFixGatesL, labelled, List.map_map, Function.comp_def, dec_of]

omit hcard hh in
theorem Min8_eq (w : Wr ind) :
    NetComplexProp8.Min8 (NetComplexP8.uA ind) w = qL (dec (MinF ind w)) := by
  rcases w with a | b <;> simp [NetComplexProp8.Min8, MinF, MinS]

omit hcard hh in
theorem Mout8_eq (w : Wr ind) :
    NetComplexProp8.Mout8 (NetComplexP8.uA ind) w = qL (dec (MoutF ind w)) := by
  rcases w with a | b | c <;> simp [NetComplexProp8.Mout8, MoutF, MoutS]

/-! ## The concrete network (`h = 100`) -/

omit hcard hh in
/-- The count for `h = 100`: `s_c = 1873807244636671267308000000`. -/
theorem prop8_count :
    frameSum2 (fun a b => Fd (dec a) (dec b)) (gatesF NetComplex.ind₀) (MinF NetComplex.ind₀) (MoutF NetComplex.ind₀) =
      1873807244636671267308000000 := by
  have e := prop8_count_general (ind := NetComplex.ind₀) NetComplex.ind₀_card (by norm_num)
  rw [NetComplex.card_T₀, NetComplex.card_Nb₀] at e
  push_cast at e
  exact_mod_cast e

end NetComplexP8

end

section
-- Source module: Solutions.P8LiftFrame
/-!
# Phase frames on `κ` columns and the frame-change step lists

* `PhiMat q`: the matrix of the one-column frame `Φ_q = PhiQ q`; `PhiK q = (PhiMat q)^{⊗κ}`
  is the frame on `κ` columns (§3.5: the `k`-th tensor power). `PhiK (a + b) = PhiK a * PhiK b`,
  `PhiK 0 = 1`.
* `PhiMat_kernels`: if `Φ_d = ∏ transK` (Proposition 8 per edge) then `PhiMat d = ∏ Tk`.
* `frameSteps w L`: the restricted steps (one kernel chunk per entry of `L`) on wire `w`;
  `frameSteps_den`: they compute `wireOp w (colT (∏ Tk))`; one child call per entry.
* `edgeSteps w V U`: the steps for the frame change of an edge `U → V` (kernels chosen by
  `prop8_edges`); `edgeSteps_den`: `wireOp w (PhiK (qL V - qL U))`, with `Fd V U` child calls.
-/

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

namespace P8Lift

open Matrix Finset Complex Butterfly NetComplexPhase NetComplexInterface

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]

/-- The matrix of the one-column frame `Φ_q`. -/
noncomputable def PhiMat (q : (Fin m → ZMod 2) → ZMod 4) : M1 m := LinearMap.toMatrix' (PhiQ q)

/-- The frame on `κ` columns: `Φ_q^{⊗κ}`. -/
noncomputable def PhiK (q : (Fin m → ZMod 2) → ZMod 4) : Op (Fin m × κ) := colT (PhiMat q)

lemma PhiMat_add (a b : (Fin m → ZMod 2) → ZMod 4) : PhiMat (a + b) = PhiMat a * PhiMat b := by
  have : PhiQ (a + b) = (PhiQ a).comp (PhiQ b) := LinearMap.ext fun g => PhiQ_add a b g
  rw [PhiMat, this, LinearMap.toMatrix'_comp]; rfl

lemma PhiMat_zero : PhiMat (0 : (Fin m → ZMod 2) → ZMod 4) = 1 := by
  have : PhiQ (0 : (Fin m → ZMod 2) → ZMod 4) = LinearMap.id := LinearMap.ext fun g => PhiQ_zero g
  rw [PhiMat, this, LinearMap.toMatrix'_id]

lemma PhiK_add (a b : (Fin m → ZMod 2) → ZMod 4) :
    (PhiK (a + b) : Op (Fin m × κ)) = PhiK a * PhiK b := by
  rw [PhiK, PhiMat_add, colT_mul]; rfl

lemma PhiK_zero : (PhiK (0 : (Fin m → ZMod 2) → ZMod 4) : Op (Fin m × κ)) = 1 := by
  rw [PhiK, PhiMat_zero, colT_one]

lemma PhiMat_mulVec (q : (Fin m → ZMod 2) → ZMod 4) (g : (Fin m → ZMod 2) → ℂ) :
    PhiMat q *ᵥ g = PhiQ q g := LinearMap.toMatrix'_mulVec _ _

lemma list_prod_mulVec (L : List (ℤ × (Fin m → ZMod 2))) (g : (Fin m → ZMod 2) → ℂ) :
    (L.map fun p => Tk p.1 p.2).prod *ᵥ g = L.foldr (fun p g' => transK p.1 p.2 g') g := by
  induction L with
  | nil => simp
  | cons p L ih =>
    rw [List.map_cons, List.prod_cons, ← Matrix.mulVec_mulVec, ih, Tk_mulVec]; rfl

/-- **Edge kernels as matrices.** -/
theorem PhiMat_kernels (d : (Fin m → ZMod 2) → ZMod 4) (L : List (ℤ × (Fin m → ZMod 2)))
    (hL : ∀ g, PhiQ d g = L.foldr (fun p g' => transK p.1 p.2 g') g) :
    PhiMat d = (L.map fun p => Tk p.1 p.2).prod := by
  apply Matrix.toLin'.injective
  apply LinearMap.ext
  intro g
  rw [Matrix.toLin'_apply, Matrix.toLin'_apply, PhiMat_mulVec, list_prod_mulVec, hL]

section Steps

variable {R : Type} [Fintype R] [DecidableEq R]

/-- One kernel chunk per entry of `L`, on wire `w` (last entry applied first). -/
noncomputable def frameSteps (w : R) (L : List (ℤ × (Fin m → ZMod 2))) : List (RStep R m) :=
  L.reverse.flatMap fun p => chunkFor w p.1 p.2

theorem frameSteps_den (w : R) (L : List (ℤ × (Fin m → ZMod 2)))
    (hL : ∀ p ∈ L, (p.1 = 1 ∨ p.1 = -1) ∧ p.2 ≠ 0) :
    denListR (Butterfly.tens Butterfly.Cm : Op κ) (frameSteps w L) =
      wireOp w (colT (L.map fun p => Tk p.1 p.2).prod) := by
  induction L with
  | nil => simp [frameSteps, colT_one, wireOp_one]
  | cons p L ih =>
    have ih' := ih fun q hq => hL q (List.mem_cons_of_mem _ hq)
    simp only [frameSteps, List.reverse_cons, List.flatMap_append, List.flatMap_cons,
      List.flatMap_nil, List.append_nil] at ih' ⊢
    rw [denListR_append, ih', chunkFor_den w p.1 (hL p List.mem_cons_self).1 p.2
      (hL p List.mem_cons_self).2, wireOp_mul, List.map_cons, List.prod_cons, colT_mul]

theorem frameSteps_count (w : R) (L : List (ℤ × (Fin m → ZMod 2)))
    (hL : ∀ p ∈ L, p.2 ≠ 0) :
    (frameSteps w L).countP RStep.isChild = L.length := by
  induction L with
  | nil => simp [frameSteps]
  | cons p L ih =>
    have ih' := ih fun q hq => hL q (List.mem_cons_of_mem _ hq)
    simp only [frameSteps, List.reverse_cons, List.flatMap_append, List.flatMap_cons,
      List.flatMap_nil, List.append_nil, List.countP_append] at ih' ⊢
    rw [ih', chunkFor_count w p.1 p.2 (hL p List.mem_cons_self), List.length_cons]

end Steps

/-! ## Edge kernels from Proposition 8 -/

section Edge

open NetComplexP8 NetComplexLabels

variable {h : ℕ}

/-- What a kernel list for the edge `U → V` must satisfy. -/
def KerSpec (V U : Submodule (ZMod 2) (Vc h)) (L : List (ℤ × Vc h)) : Prop :=
  (∀ p ∈ L, (p.1 = 1 ∨ p.1 = -1) ∧ p.2 ≠ 0) ∧ L.length = Fd V U ∧
    ∀ g, PhiQ (qL V - qL U) g = L.foldr (fun p g' => transK p.1 p.2 g') g

lemma ne_zero_of_dot {v : Vc h} (hv : v ⬝ᵥ v = 1) : v ≠ 0 := by
  rintro rfl; simp at hv

theorem kerSpec_of_edgeP {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) :
    ∃ L, KerSpec V U L := by
  obtain ⟨-, B, hB, -, hcard, L, hLB, hpm, hPhi⟩ := hE
  refine ⟨L, fun p hp => ⟨hpm p hp, ?_⟩, ?_, hPhi⟩
  · have : p.2 ∈ B.toList := hLB ▸ List.mem_map_of_mem hp
    exact ne_zero_of_dot (hB.1 _ (Finset.mem_toList.1 this))
  · rw [← List.length_map (f := Prod.snd), hLB, Finset.length_toList, hcard]

/-- The kernel list chosen for an edge. -/
noncomputable def kers (V U : Submodule (ZMod 2) (Vc h)) : List (ℤ × Vc h) := by
  classical
  exact if hh : ∃ L, KerSpec V U L then Classical.choose hh else []

lemma kers_spec {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) : KerSpec V U (kers V U) := by
  have hh := kerSpec_of_edgeP hE
  unfold kers
  rw [dif_pos hh]
  exact Classical.choose_spec hh

variable {R : Type} [Fintype R] [DecidableEq R]

/-- The restricted steps for the frame change `U → V` on wire `w`. -/
noncomputable def edgeSteps (w : R) (V U : Submodule (ZMod 2) (Vc h)) : List (RStep R (h ^ 3)) :=
  frameSteps w (kers V U)

/-- **Frame change of an edge**: `wireOp w (Φ_{q_V - q_U}^{⊗κ})`. -/
theorem edgeSteps_den (w : R) {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) :
    denListR (Butterfly.tens Butterfly.Cm : Op κ) (edgeSteps w V U) = wireOp w (PhiK (qL V - qL U)) := by
  have hs := kers_spec hE
  rw [edgeSteps, frameSteps_den w _ hs.1, PhiK, PhiMat_kernels _ _ hs.2.2]

/-- The frame change of an edge uses `Fd V U` child calls. -/
theorem edgeSteps_count (w : R) {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) :
    (edgeSteps w V U).countP RStep.isChild = Fd V U := by
  have hs := kers_spec hE
  rw [edgeSteps, frameSteps_count w _ fun p hp => (hs.1 p hp).2, hs.2.1]

end Edge

end P8Lift

end

section
-- Source module: Solutions.P8LiftNet
/-!
# The restricted step list simulating the physical phase-frame network on `κ` columns

For a labelled gate list (labels in `LabG h`, decoded by `dec`) whose every frame change is a
Proposition 8 edge (`FramesOK2 EdgeP`), `netSteps` is the restricted step list: for each gate,
the edge chunks of all touched wires followed by the pointwise gate; at the end, the edge chunks
to the sink labels. `netSteps_run`: its denotation is the physical run `netRun` with the
column frames `Φ_q^{⊗κ}`, for every column type `κ`. `netSteps_count`: its child calls number
`frameSum2 Fd`.
-/

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

namespace P8Lift

open Matrix Finset Complex Butterfly NetComplexPhase NetComplexInterface NetComplexP8
  NetComplexLabels AModel AModelRat

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {R : Type} [Fintype R] [DecidableEq R]

/-! ## Block operators acting on states -/

lemma blockOp_mulVec (A : R → Op (Fin m × κ)) (F : R × Addr m κ → ℂ) (p : R × Addr m κ) :
    (blockOp A *ᵥ F) p = (A p.1 *ᵥ fun x => F (p.1, x)) p.2 := by
  simp only [mulVec, dotProduct, blockOp, ite_mul, zero_mul]
  rw [Fintype.sum_prod_type]
  simp only [Finset.sum_ite_irrel, Finset.sum_const_zero]
  rw [Finset.sum_ite_eq]
  simp

lemma gate_mulVec (G : Matrix R R ℂ) (F : R × Addr m κ → ℂ) (p : R × Addr m κ) :
    ((RStep.gate G : RStep R m).den (Butterfly.tens Butterfly.Cm : Op κ) *ᵥ F) p = ∑ w', G p.1 w' * F (w', p.2) := by
  simp only [mulVec, dotProduct, RStep.den, mul_ite, mul_one, mul_zero, ite_mul, zero_mul]
  rw [Fintype.sum_prod_type]
  refine Finset.sum_congr rfl fun w' _ => ?_
  rw [Finset.sum_ite_eq]; simp

/-- Steps on distinct wires, each a wire operator, compose to a block operator. -/
theorem denListR_flatMap_wire (T : Op κ) (S : R → List (RStep R m)) (A : R → Op (Fin m × κ)) :
    ∀ ws : List R, ws.Nodup → (∀ w ∈ ws, denListR T (S w) = wireOp w (A w)) →
      denListR T (ws.flatMap S) = blockOp fun r => if r ∈ ws then A r else 1 := by
  intro ws
  induction ws with
  | nil => intro _ _; simp only [List.flatMap_nil, denListR_nil, List.not_mem_nil, if_false]
           exact blockOp_one.symm
  | cons w ws ih =>
    intro hnd hS
    rw [List.nodup_cons] at hnd
    rw [List.flatMap_cons, denListR_append, ih hnd.2 fun w' h => hS w' (List.mem_cons_of_mem _ h),
      hS w List.mem_cons_self, wireOp, blockOp_mul]
    congr 1; funext r
    by_cases hr : r = w
    · subst hr; simp [hnd.1]
    · simp [hr]

/-! ## The step list -/

variable {h : ℕ}

/-- Column frames as linear maps on wire arrays. -/
noncomputable def PhiL (κ : Type) [Fintype κ] [DecidableEq κ] (q : (Fin (h ^ 3) → ZMod 2) → ZMod 4) :
    (Addr (h ^ 3) κ → ℂ) →ₗ[ℂ] (Addr (h ^ 3) κ → ℂ) :=
  Matrix.mulVecLin (PhiK q)

lemma PhiL_add (a b : (Fin (h ^ 3) → ZMod 2) → ZMod 4) (x : Addr (h ^ 3) κ → ℂ) :
    PhiL κ (a + b) x = PhiL κ a (PhiL κ b x) := by
  simp only [PhiL, Matrix.mulVecLin_apply, PhiK_add, Matrix.mulVec_mulVec]

lemma PhiL_zero (x : Addr (h ^ 3) κ → ℂ) : PhiL κ (0 : (Fin (h ^ 3) → ZMod 2) → ZMod 4) x = x := by
  simp only [PhiL, Matrix.mulVecLin_apply, PhiK_zero, Matrix.one_mulVec]

/-- Steps of one gate: the edge chunks of all touched wires, then the pointwise gate. -/
noncomputable def gateSteps (g : NGate R ℂ (LabG h)) (lab : R → LabG h) : List (RStep R (h ^ 3)) :=
  (g.2.1.toList.flatMap fun w => edgeSteps w (dec g.2.2) (dec (lab w))) ++ [RStep.gate g.1]

/-- The full step list of a labelled gate list, ending with the frame changes to `Mout`. -/
noncomputable def netSteps : List (NGate R ℂ (LabG h)) → (R → LabG h) → (R → LabG h) →
    List (RStep R (h ^ 3))
  | [], lab, Mout => (univ : Finset R).toList.flatMap fun w => edgeSteps w (dec (Mout w)) (dec (lab w))
  | g :: gs, lab, Mout => gateSteps g lab ++ netSteps gs (labStep lab g) Mout

/-- Labels as phase functions. -/
noncomputable def qd (lab : R → LabG h) : R → (Fin (h ^ 3) → ZMod 2) → ZMod 4 :=
  fun w => qL (dec (lab w))

/-- The physical step of one gate is simulated by its steps. -/
theorem gateSteps_run (g : NGate R ℂ (LabG h)) (hg : g.OK) (lab : R → LabG h)
    (hE : ∀ w ∈ g.2.1, EdgeP (dec g.2.2) (dec (lab w))) (F : R × Addr (h ^ 3) κ → ℂ) :
    denListR (Butterfly.tens Butterfly.Cm : Op κ) (gateSteps g lab) *ᵥ F = fun p =>
      (physStep (PhiL κ) (qd lab, fun w x => F (w, x)) (g.1, g.2.1, qL (dec g.2.2))).2 p.1 p.2 := by
  rw [gateSteps, denListR_append,
    denListR_flatMap_wire _ _ (fun w => PhiK (qL (dec g.2.2) - qL (dec (lab w)))) _
      (Finset.nodup_toList _) (fun w hw => edgeSteps_den w (hE w (Finset.mem_toList.1 hw)))]
  rw [show denListR (Butterfly.tens Butterfly.Cm : Op κ) [RStep.gate g.1] = (RStep.gate g.1 : RStep R (h ^ 3)).den
    (Butterfly.tens Butterfly.Cm) by simp [denListR]]
  rw [← Matrix.mulVec_mulVec]
  funext p
  rw [gate_mulVec]
  simp only [blockOp_mulVec, Finset.mem_toList, physStep]
  by_cases hp : p.1 ∈ g.2.1
  · rw [if_pos hp, Finset.sum_apply, ← Finset.sum_subset (Finset.subset_univ g.2.1)]
    · refine Finset.sum_congr rfl fun w' hw' => ?_
      rw [if_pos hw']
      simp [PhiL, qd]
    · intro w' _ hw'
      simp [(hg p.1 w').2 hp hw']
  · rw [if_neg hp, Finset.sum_eq_single p.1]
    · rw [(hg p.1 p.1).1 hp, if_pos rfl, if_neg hp, one_mul, one_mulVec]
    · intro b _ hb; rw [(hg p.1 b).1 hp, if_neg (Ne.symm hb), zero_mul]
    · simp

lemma labStep_qd (lab : R → LabG h) (g : NGate R ℂ (LabG h)) (F0 : R → Addr (h ^ 3) κ → ℂ) :
    qd (labStep lab g) = (physStep (PhiL κ) (qd lab, F0) (g.1, g.2.1, qL (dec g.2.2))).1 := by
  funext w
  simp only [qd, labStep, physStep]
  split_ifs <;> rfl

/-- **Simulation.** The restricted step list computes the physical network run with column
frames, for every column type `κ`. -/
theorem netSteps_run (Mout : R → LabG h) :
    ∀ (gates : List (NGate R ℂ (LabG h))) (lab : R → LabG h), (∀ g ∈ gates, g.OK) →
      FramesOK2 (fun a b => EdgeP (dec a) (dec b)) gates lab Mout →
      ∀ F : R × Addr (h ^ 3) κ → ℂ,
        denListR (Butterfly.tens Butterfly.Cm : Op κ) (netSteps gates lab Mout) *ᵥ F = fun p =>
          netRun (PhiL κ) (mapG (fun a => qL (dec a)) gates) (qd lab) (qd Mout)
            (fun w x => F (w, x)) p.1 p.2 := by
  intro gates
  induction gates with
  | nil =>
    intro lab _ hF F
    rw [netSteps, denListR_flatMap_wire _ _ (fun w => PhiK (qL (dec (Mout w)) - qL (dec (lab w))))
      _ (Finset.nodup_toList _) (fun w _ => edgeSteps_den w (hF w))]
    funext p
    rw [blockOp_mulVec]
    simp [netRun, mapG, PhiL, qd]
  | cons g gs ih =>
    intro lab hok hF F
    obtain ⟨hF1, hF2⟩ := hF
    rw [netSteps, denListR_append, ← Matrix.mulVec_mulVec,
      gateSteps_run g (hok g List.mem_cons_self) lab hF1 F,
      ih (labStep lab g) (fun g' h' => hok g' (List.mem_cons_of_mem _ h')) hF2]
    funext p
    simp only [netRun, mapG, List.map_cons, List.foldl_cons]
    rw [labStep_qd (F0 := fun w x => F (w, x))]

/-- **Child count** of the step list: `frameSum2 Fd`. -/
theorem netSteps_count (Mout : R → LabG h) :
    ∀ (gates : List (NGate R ℂ (LabG h))) (lab : R → LabG h),
      FramesOK2 (fun a b => EdgeP (dec a) (dec b)) gates lab Mout →
      (netSteps gates lab Mout).countP RStep.isChild =
        frameSum2 (fun a b => Fd (dec a) (dec b)) gates lab Mout := by
  have flat : ∀ (ws : List R) (S : R → List (RStep R (h ^ 3))),
      (ws.flatMap S).countP RStep.isChild = (ws.map fun w => (S w).countP RStep.isChild).sum := by
    intro ws S
    induction ws with
    | nil => simp
    | cons w ws ih => simp [List.countP_append, ih]
  intro gates
  induction gates with
  | nil =>
    intro lab hF
    rw [netSteps, flat, frameSum2]
    rw [← Finset.sum_map_toList]
    congr 1
    refine List.map_congr_left fun w _ => ?_
    exact edgeSteps_count w (hF w)
  | cons g gs ih =>
    intro lab hF
    obtain ⟨hF1, hF2⟩ := hF
    rw [netSteps, List.countP_append, ih _ hF2, frameSum2, gateSteps, List.countP_append, flat]
    have : (([RStep.gate g.1] : List (RStep R (h ^ 3))).countP RStep.isChild) = 0 := by
      simp [RStep.isChild]
    rw [this, add_zero, ← Finset.sum_map_toList]
    congr 2
    refine List.map_congr_left fun w hw => ?_
    exact edgeSteps_count w (hF1 w (Finset.mem_toList.1 hw))

end P8Lift

end

section
-- Source module: Solutions.P8LiftRoute
/-!
# Routes on `κ` columns

* `PhiMat_wt`: the full-label frame `Φ_{wt}` is `C^{⊗m}` (`CtenMat`); `colT_CtenMat`: on `κ`
  columns it is `C^{⊗(Fin m × κ)} = tens Cm`.
* `Zcorr_cols`: for the pair `X_a → Y_a`, the frame `Φ_{wt + 2[u·x]}` becomes `tens Cm` after
  `Z_u` (on every column) before and `i^{wt u · |κ|} Z_u` after.
* `colT_ZuMat`: `Z_u` on all columns is the diagonal phase `i^{Σ_{(r,c)} 2u_r x(r,c)}`, i.e. the
  restricted `phase` step.
* `route_cols`: the network theorem with column frames.
-/

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

namespace P8Lift

open Matrix Finset Complex Butterfly NetComplexInterface NetComplexP8 NetComplexLabels AModel AModelRat

variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]

/-- The matrix of `C^{⊗m}` on one column. -/
noncomputable def CtenMat (m : ℕ) : M1 m := fun y z => ∏ i, NetComplexPhase.CK (y i) (z i)

/-- The matrix of `Mten u`. -/
noncomputable def MtenMat (u : Fin m → ZMod 2) : M1 m := fun y z =>
  ∏ i, (if i ∈ NetComplexPhase.supp u then NetComplexPhase.CKinv else NetComplexPhase.CK) (y i) (z i)

/-- The matrix of `Z_u`. -/
noncomputable def ZuMat (u : Fin m → ZMod 2) : M1 m :=
  diagonal fun z => ∏ i, (if i ∈ NetComplexPhase.supp u then NetComplexPhase.chi (z i) else 1)

lemma mat_ext_mulVec {A B : M1 m} (h : ∀ g, A *ᵥ g = B *ᵥ g) : A = B := by
  apply Matrix.toLin'.injective
  apply LinearMap.ext
  intro g
  rw [Matrix.toLin'_apply, Matrix.toLin'_apply, h]

lemma PhiQ_wt (g : (Fin m → ZMod 2) → ℂ) :
    PhiQ (fun x => (NetComplexPhase.wt x : ZMod 4)) g = Cten g := by
  funext y
  change NetComplexPhase.WH _ y = _
  have e : (fun x => I ^ ((NetComplexPhase.wt x : ZMod 4)).val * NetComplexPhase.WH g x) =
      fun x => I ^ NetComplexPhase.wt x * NetComplexPhase.WH g x := by
    funext x
    congr 1
    apply NetComplexPhase.I_pow_mod
    simp only [ZMod.natCast_val, ZMod.cast_id', id]
  rw [e, NetComplexPhase.WH_full]
  rfl

lemma PhiQ_mixed (u : Fin m → ZMod 2) (g : (Fin m → ZMod 2) → ℂ) :
    PhiQ (fun x => ((NetComplexPhase.wt x + 2 * (u ⬝ᵥ x).val : ℕ) : ZMod 4)) g = Mten u g := by
  funext y
  change NetComplexPhase.WH _ y = _
  have e : (fun x => I ^ (((NetComplexPhase.wt x + 2 * (u ⬝ᵥ x).val : ℕ) : ZMod 4)).val *
      NetComplexPhase.WH g x) =
      fun x => I ^ (NetComplexPhase.wt x + 2 * (u ⬝ᵥ x).val) * NetComplexPhase.WH g x := by
    funext x
    congr 1
    apply NetComplexPhase.I_pow_mod
    simp only [ZMod.natCast_val, ZMod.cast_id', id]
  rw [e, NetComplexPhase.WH_mixed]
  rfl

theorem PhiMat_wt : PhiMat (fun x => (NetComplexPhase.wt x : ZMod 4)) = CtenMat m :=
  mat_ext_mulVec fun g => by rw [PhiMat_mulVec, PhiQ_wt]; rfl

theorem PhiMat_mixed (u : Fin m → ZMod 2) :
    PhiMat (fun x => ((NetComplexPhase.wt x + 2 * (u ⬝ᵥ x).val : ℕ) : ZMod 4)) = MtenMat u :=
  mat_ext_mulVec fun g => by rw [PhiMat_mulVec, PhiQ_mixed]; rfl

lemma ZuMat_mulVec (u : Fin m → ZMod 2) (g : (Fin m → ZMod 2) → ℂ) : ZuMat u *ᵥ g = Zu u g := by
  funext z; simp [ZuMat, mulVec_diagonal, Zu]

theorem Zcorr_mat (u : Fin m → ZMod 2) :
    I ^ NetComplexPhase.wt u • (ZuMat u * MtenMat u * ZuMat u) = CtenMat m := by
  apply mat_ext_mulVec
  intro g
  rw [Matrix.smul_mulVec, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec]
  simp only [ZuMat_mulVec]
  rw [show MtenMat u *ᵥ Zu u g = Mten u (Zu u g) from rfl, Z_correct_tensor]
  rfl

lemma CK_eq_Cm (a b : Fin 2) : NetComplexPhase.CK a b = Butterfly.Cm a b := by
  rw [Cm_apply']; rfl

theorem colT_CtenMat : (colT (CtenMat m) : Op (Fin m × κ)) = Butterfly.tens Butterfly.Cm := by
  ext x y
  simp only [colT, CtenMat, Butterfly.tens, Butterfly.tensF, col]
  rw [Fintype.prod_prod_type, Finset.prod_comm]
  refine Finset.prod_congr rfl fun c _ => Finset.prod_congr rfl fun i _ => CK_eq_Cm _ _

/-- **The `X_a → Y_a` correction on `κ` columns.** -/
theorem Zcorr_cols (u : Fin m → ZMod 2) :
    (I ^ NetComplexPhase.wt u) ^ Fintype.card κ •
      ((colT (ZuMat u) : Op (Fin m × κ)) * colT (MtenMat u) * colT (ZuMat u)) = Butterfly.tens Butterfly.Cm := by
  rw [← colT_mul, ← colT_mul, ← colT_smul, Zcorr_mat, colT_CtenMat]

lemma chi_eq_I (b : ZMod 2) : NetComplexPhase.chi b = I ^ (2 * b.val) := by
  rw [NetComplexPhase.chi, pow_mul, I_sq]

/-- `Z_u` on all columns is the phase `i^{Σ_{(r,c)} 2 u_r x(r,c)}`. -/
theorem colT_ZuMat (u : Fin m → ZMod 2) :
    (colT (ZuMat u) : Op (Fin m × κ)) =
      diagonal fun x => I ^ (∑ p : Fin m × κ, (2 * (u p.1).val) * (x p).val) := by
  rw [ZuMat, colT_diagonal]
  congr 1; funext x
  rw [← Finset.prod_pow_eq_pow_sum, Fintype.prod_prod_type, Finset.prod_comm]
  refine Finset.prod_congr rfl fun r _ => Finset.prod_congr rfl fun c _ => ?_
  show _ = I ^ (2 * (u r).val * (x (r, c)).val)
  simp only [col, NetComplexPhase.supp, Finset.mem_filter, Finset.mem_univ, true_and]
  rcases NetComplexOrtho.zmod2_cases (u r) with e | e
  · rw [e]; simp
  · rw [e, if_pos (by decide)]
    have h1 : ZMod.val (1 : ZMod 2) = 1 := rfl
    rw [h1, mul_one]
    exact chi_eq_I (x (r, c))

/-! ## The network theorem with column frames -/

section Net

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

theorem route_cols (hcard : ∀ t, (ind t).card = 3) (hinj : Function.Injective ind)
    (lab : Option (NetComplex.GName T) → ((Fin (h ^ 3) → ZMod 2) → ZMod 4))
    (Min Mout : NetComplex.Wr ind → ((Fin (h ^ 3) → ZMod 2) → ZMod 4))
    (f : NetComplex.Wr ind → Addr (h ^ 3) κ → ℂ) (w : NetComplex.Wr ind) :
    netRun (PhiL κ) (NetComplex.cxFixGatesL ℂ ind lab) Min Mout f (NetComplex.ρ ind w) =
      PhiK (Mout (NetComplex.ρ ind w) - Min w) *ᵥ f w :=
  network_realizes_var (PhiL κ) PhiL_add PhiL_zero _
    (NetComplex.complex_exchange_fixed_net hcard hinj lab).1 (NetComplex.ρ ind)
    (NetComplex.complex_exchange_fixed_net hcard hinj lab).2 Min Mout f w

end Net

end P8Lift

end

section
-- Source module: Solutions.P8LiftAssemble
/-!
# The full restricted program of the complex network, for every number of columns

On the roles `Wr ind` of the corrected complex network (gates `gatesF ind` with the labels of
table (6)), the program `prog ind` is:

1. `Z_{u_a}` (a restricted `phase` step) on every `X_a`;
2. `netSteps`: for each gate, the Proposition 8 kernel chunks (row additions, one child call,
   row additions undone) for every touched wire, then the pointwise gate; finally the chunks to
   the sink labels;
3. `i^{27|κ|} Z_{u_a}` (one `phase` step) on every `Y_a`;
4. the role permutation `ρ` (`X_a ↔ Y_a`).

`prog_correct`: for every column type `κ`, its denotation is `C^{⊗(Fin m × κ)}` on every role.
`prog_count`: it has `frameSum2 Fd` child calls (`= 2N(m−1) + …`, see `prop8_count_general`).
-/

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

namespace P8Lift

open Matrix Finset Complex Butterfly NetComplexInterface NetComplexP8 NetComplexLabels AModel
  AModelRat

variable {κ : Type} [Fintype κ] [DecidableEq κ]

section Generic

variable {R : Type} [Fintype R] [DecidableEq R] {m : ℕ}

/-- The same operator on every role. -/
def roleDiagR (A : Op (Fin m × κ)) : ROp R m κ := blockOp fun _ => A

lemma rop_ext {A B : ROp R m κ} (h : ∀ F, A *ᵥ F = B *ᵥ F) : A = B := by
  apply Matrix.toLin'.injective
  apply LinearMap.ext
  intro g
  rw [Matrix.toLin'_apply, Matrix.toLin'_apply, h]

lemma denListR_single (T0 : Op κ) (st : RStep R m) : denListR T0 [st] = st.den T0 := by
  simp [denListR]

lemma den_phase (T0 : Op κ) (w : R) (k₀ k₁ : ℕ) (a : Fin m → ℕ) :
    (RStep.phase w k₀ k₁ a : RStep R m).den T0 =
      wireOp w (diagonal fun x => I ^ RStep.phExp k₀ k₁ a x) := by
  ext ⟨p1, p2⟩ ⟨q1, q2⟩
  simp only [RStep.den, wireOp, blockOp, diagonal_apply, Prod.mk.injEq]
  by_cases h1 : p1 = q1
  · subst h1
    by_cases h2 : p1 = w
    · simp [h2, diagonal_apply]
    · simp [h2, one_apply]
  · simp [h1]

lemma perm_mulVec (T0 : Op κ) (σ : Equiv.Perm R) (F : R × Addr m κ → ℂ) (p : R × Addr m κ) :
    ((RStep.perm σ : RStep R m).den T0 *ᵥ F) p = F (σ.symm p.1, p.2) := by
  simp only [mulVec, dotProduct, RStep.den, ite_mul, one_mul, zero_mul]
  rw [Finset.sum_eq_single (σ.symm p.1, p.2)]
  · simp
  · intro q _ hq
    rw [if_neg]
    rintro ⟨h1, h2⟩
    exact hq (Prod.ext (by simp [h1]) h2.symm)
  · simp

lemma denListR_wires (T0 : Op κ) (S : R → List (RStep R m)) (A : R → Op (Fin m × κ))
    (hS : ∀ w, denListR T0 (S w) = wireOp w (A w)) :
    denListR T0 ((univ : Finset R).toList.flatMap S) = blockOp A := by
  rw [denListR_flatMap_wire T0 S A _ (Finset.nodup_toList _) fun w _ => hS w]
  congr 1; funext r; simp

end Generic

variable {h : ℕ} {T : Type} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}

lemma ρ_invol (w : NetComplex.Wr ind) : NetComplex.ρ ind (NetComplex.ρ ind w) = w := by
  rcases w with a | a | s <;> rfl

variable (ind) in
/-- The role permutation `ρ`. -/
def ρE : Equiv.Perm (NetComplex.Wr ind) where
  toFun := NetComplex.ρ ind
  invFun := NetComplex.ρ ind
  left_inv := ρ_invol
  right_inv := ρ_invol

variable (ind) in
/-- The `Z_{u_a}` phase coefficients `2 (u_a)_r`. -/
def uaN (a : T × T × T) : Fin (h ^ 3) → ℕ := fun r => 2 * (NetComplexP8.uA ind a r).val

variable (ind) in
def preSteps : NetComplex.Wr ind → List (RStep (NetComplex.Wr ind) (h ^ 3))
  | Sum.inl a => [RStep.phase (Sum.inl a) 0 0 (uaN ind a)]
  | _ => []

variable (ind) in
def postSteps : NetComplex.Wr ind → List (RStep (NetComplex.Wr ind) (h ^ 3))
  | Sum.inr (Sum.inl a) => [RStep.phase (Sum.inr (Sum.inl a)) 0 27 (uaN ind a)]
  | _ => []

variable (ind κ) in
noncomputable def preOp : NetComplex.Wr ind → Op (Fin (h ^ 3) × κ)
  | Sum.inl a => colT (ZuMat (NetComplexP8.uA ind a))
  | _ => 1

variable (ind κ) in
noncomputable def postOp : NetComplex.Wr ind → Op (Fin (h ^ 3) × κ)
  | Sum.inr (Sum.inl a) => (I ^ 27) ^ Fintype.card κ • colT (ZuMat (NetComplexP8.uA ind a))
  | _ => 1

lemma preSteps_den (w : NetComplex.Wr ind) :
    denListR (Butterfly.tens Cm : Op κ) (preSteps ind w) = wireOp w (preOp κ ind w) := by
  rcases w with a | a | s
  · simp only [preSteps, preOp]
    rw [show denListR (Butterfly.tens Cm : Op κ) [RStep.phase (Sum.inl a) 0 0 (uaN ind a)] =
      (RStep.phase (Sum.inl a) 0 0 (uaN ind a) : RStep (NetComplex.Wr ind) (h ^ 3)).den (Butterfly.tens Cm)
      by simp [denListR], den_phase, colT_ZuMat]
    congr 2; funext x; simp [RStep.phExp, uaN]
  · exact (wireOp_one _).symm
  · exact (wireOp_one _).symm

lemma postSteps_den (w : NetComplex.Wr ind) :
    denListR (Butterfly.tens Cm : Op κ) (postSteps ind w) = wireOp w (postOp κ ind w) := by
  rcases w with a | a | s
  · exact (wireOp_one _).symm
  · simp only [postSteps, postOp]
    rw [show denListR (Butterfly.tens Cm : Op κ) [RStep.phase (Sum.inr (Sum.inl a)) 0 27 (uaN ind a)] =
      (RStep.phase (Sum.inr (Sum.inl a)) 0 27 (uaN ind a) : RStep (NetComplex.Wr ind) (h ^ 3)).den
        (Butterfly.tens Cm) by simp [denListR], den_phase, colT_ZuMat]
    congr 1
    ext x y
    simp only [diagonal_apply, Matrix.smul_apply, smul_eq_mul]
    split_ifs
    · simp only [RStep.phExp, uaN, zero_add, pow_add, pow_mul]
    · simp
  · exact (wireOp_one _).symm

variable (ind) in
/-- **The restricted program** of the complex network (independent of `κ`). -/
noncomputable def prog : List (RStep (NetComplex.Wr ind) (h ^ 3)) :=
  (univ : Finset (NetComplex.Wr ind)).toList.flatMap (preSteps ind) ++
    netSteps (gatesF ind) (MinF ind) (MoutF ind) ++
    (univ : Finset (NetComplex.Wr ind)).toList.flatMap (postSteps ind) ++
    [RStep.perm (ρE ind)]

lemma gatesF_ok : ∀ g ∈ gatesF ind, g.OK :=
  NetComplex.ok_labelled _ _ NetComplex.cxFixNamed_ok

variable (hcard : ∀ t, (ind t).card = 3) (hh : 7 ≤ h) (hinj : Function.Injective ind)
include hcard hh

/-- **Correctness of the restricted program, every `κ`.** -/
theorem prog_correct (hinj : Function.Injective ind) :
    denListR (Butterfly.tens Cm : Op κ) (prog ind) = roleDiagR (Butterfly.tens Cm) := by
  apply rop_ext
  intro F
  rw [prog, denListR_append, denListR_append, denListR_append, ← Matrix.mulVec_mulVec,
    ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec,
    denListR_wires _ _ _ preSteps_den, denListR_wires _ _ _ postSteps_den,
    netSteps_run (MoutF ind) (gatesF ind) (MinF ind) gatesF_ok (prop8_edges hcard hh)]
  have hq1 : qd (MinF ind) = NetComplexProp8.Min8 (NetComplexP8.uA ind) := funext fun w => (Min8_eq w).symm
  have hq2 : qd (MoutF ind) = NetComplexProp8.Mout8 (NetComplexP8.uA ind) := funext fun w => (Mout8_eq w).symm
  rw [gatesF_phase, hq1, hq2]
  funext p
  rw [denListR_single, perm_mulVec, blockOp_mulVec]
  show (postOp κ ind (NetComplex.ρ ind p.1) *ᵥ fun x => netRun (PhiL κ) _ _ _ _
    (NetComplex.ρ ind p.1) x) p.2 = _
  rw [route_cols hcard hinj, roleDiagR, blockOp_mulVec]
  have hpre : (fun x => (blockOp (preOp κ ind) *ᵥ F) (p.1, x)) =
      preOp κ ind p.1 *ᵥ fun x => F (p.1, x) := by
    funext x; rw [blockOp_mulVec]
  rw [hpre, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec]
  congr 1
  rcases p with ⟨a | a | s, x⟩
  · -- `X_a → Y_a`
    have hd : NetComplexProp8.Mout8 (NetComplexP8.uA ind) (NetComplex.ρ ind (Sum.inl a)) -
        NetComplexProp8.Min8 (NetComplexP8.uA ind) (Sum.inl a : NetComplex.Wr ind) =
        fun x => ((NetComplexPhase.wt x + 2 * (NetComplexP8.uA ind a ⬝ᵥ x).val : ℕ) : ZMod 4) := by
      funext x
      simp only [NetComplex.ρ, NetComplexProp8.Mout8, NetComplexProp8.Min8, Pi.sub_apply]
      exact qL_line_perp_diff (NetComplexP8.uA ind a) (uA_norm hcard a) (wt_odd (uA_norm hcard a)) x
    simp only [NetComplex.ρ] at hd ⊢
    rw [hd, PhiK, PhiMat_mixed]
    simp only [postOp, preOp]
    rw [smul_mul_assoc, smul_mul_assoc, ← wt_uA hcard a]
    exact Zcorr_cols (NetComplexP8.uA ind a)
  · have hd : NetComplexProp8.Mout8 (NetComplexP8.uA ind) (NetComplex.ρ ind (Sum.inr (Sum.inl a))) -
        NetComplexProp8.Min8 (NetComplexP8.uA ind) (Sum.inr (Sum.inl a) : NetComplex.Wr ind) =
        fun x => (NetComplexPhase.wt x : ZMod 4) := by
      funext x
      simp only [NetComplex.ρ, NetComplexProp8.Mout8, NetComplexProp8.Min8, Pi.sub_apply, qL_top,
        qL_bot, sub_zero]
    simp only [NetComplex.ρ] at hd ⊢
    rw [hd, PhiK, PhiMat_wt, colT_CtenMat]
    simp [postOp, preOp]
  · have hd : NetComplexProp8.Mout8 (NetComplexP8.uA ind) (NetComplex.ρ ind (Sum.inr (Sum.inr s))) -
        NetComplexProp8.Min8 (NetComplexP8.uA ind) (Sum.inr (Sum.inr s) : NetComplex.Wr ind) =
        fun x => (NetComplexPhase.wt x : ZMod 4) := by
      funext x
      simp only [NetComplex.ρ, NetComplexProp8.Mout8, NetComplexProp8.Min8, Pi.sub_apply, qL_top,
        qL_bot, sub_zero]
    simp only [NetComplex.ρ] at hd ⊢
    rw [hd, PhiK, PhiMat_wt, colT_CtenMat]
    simp [postOp, preOp]

/-- **Child count of the restricted program.** -/
theorem prog_count :
    (prog ind).countP RStep.isChild =
      frameSum2 (fun a b => Fd (dec a) (dec b)) (gatesF ind) (MinF ind) (MoutF ind) := by
  have hz : ∀ (S : NetComplex.Wr ind → List (RStep (NetComplex.Wr ind) (h ^ 3))),
      (∀ w, (S w).countP RStep.isChild = 0) →
      ((univ : Finset (NetComplex.Wr ind)).toList.flatMap S).countP RStep.isChild = 0 := by
    intro S hS
    rw [List.countP_eq_zero]
    intro st hst
    obtain ⟨w, _, hw⟩ := List.mem_flatMap.1 hst
    have := hS w
    rw [List.countP_eq_zero] at this
    exact this st hw
  rw [prog, List.countP_append, List.countP_append, List.countP_append,
    hz _ (fun w => by rcases w with a | a | s <;> simp [preSteps, RStep.isChild]),
    hz _ (fun w => by rcases w with a | a | (s | s) <;> simp [postSteps, RStep.isChild]),
    netSteps_count (MoutF ind) (gatesF ind) (MinF ind) (prop8_edges hcard hh)]
  simp [RStep.isChild]

end P8Lift

end

section
-- Source module: Solutions.P8LiftFinal
/-!
# The restricted Proposition 8 interface for the complex network (`h = 100`)

* `RStep.map`: transporting a restricted program along a bijection of roles
  (`den_map`, `denListR_map`: conjugation by the induced permutation of states).
* `eW : Wr ind₀ ≃ Fin W_c` with `W_c = 1873807244643542670000` (from `card_Wr₀`).
* **`complexIface : Prop8IfaceR W_c (100^3) s_c`**, `s_c = 1873807244636671267308000000`:
  the restricted program `prog ind₀` (row additions, pointwise gates, `Z`/scalar phases, one
  role permutation, and exactly `s_c` child calls), proved to compute `C^{⊗(Fin m × κ)}` on
  every role for every column type `κ`.
* `complexIface_main`: hence (via `toIface`) the recursion `recOp` computes `C^{⊗}` at every
  depth, and `s_c < W_c · m`.
-/

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

namespace P8Lift

open Matrix Finset Complex Butterfly NetComplexP8 AModelRat

section Map

variable {R R' : Type} [Fintype R] [DecidableEq R] [Fintype R'] [DecidableEq R'] {m : ℕ}
  {κ : Type} [Fintype κ] [DecidableEq κ]

/-- Transport a step along a bijection of roles. -/
def RStep.map (e : R ≃ R') : RStep R m → RStep R' m
  | .gate G => .gate fun i j => G (e.symm i) (e.symm j)
  | .rowAdd w i j hij => .rowAdd (e w) i j hij
  | .phase w k₀ k₁ a => .phase (e w) k₀ k₁ a
  | .perm σ => .perm (e.permCongr σ)
  | .child w h fwd => .child (e w) h fwd

/-- The induced bijection of states. -/
def stE (e : R ≃ R') : R × Addr m κ ≃ R' × Addr m κ := e.prodCongr (Equiv.refl _)

lemma RStep.isChild_map (e : R ≃ R') (st : RStep R m) : (st.map e).isChild = st.isChild := by
  cases st <;> rfl

lemma childR_map (e : R ≃ R') (w : R) (h : Fin m) (T : Op κ) :
    RStep.childR (e w) h T = (RStep.childR w h T).submatrix (stE e).symm (stE e).symm := by
  ext ⟨p1, p2⟩ ⟨q1, q2⟩
  simp only [RStep.childR, submatrix_apply, stE, Equiv.prodCongr_symm, Equiv.prodCongr_apply,
    Equiv.coe_refl, Prod.map_apply, id_eq, Equiv.refl_symm]
  simp only [e.symm.injective.eq_iff, Equiv.symm_apply_eq]

theorem RStep.den_map_apply (T : Op κ) (e : R ≃ R') (st : RStep R m) (p q : R' × Addr m κ) :
    (st.map e).den T p q = st.den T (e.symm p.1, p.2) (e.symm q.1, q.2) := by
  obtain ⟨p1, p2⟩ := p
  obtain ⟨q1, q2⟩ := q
  cases st with
  | gate G => rfl
  | rowAdd w i j hij =>
    show (if p1 = q1 then _ else _) = (if e.symm p1 = e.symm q1 then _ else _)
    simp only [e.symm.injective.eq_iff, Equiv.symm_apply_eq]
  | phase w k₀ k₁ a =>
    simp only [RStep.map, RStep.den, diagonal_apply, Prod.mk.injEq, e.symm.injective.eq_iff,
      Equiv.symm_apply_eq]
  | perm σ =>
    show (if p1 = e.permCongr σ q1 ∧ p2 = q2 then (1 : ℂ) else 0) =
      (if e.symm p1 = σ (e.symm q1) ∧ p2 = q2 then 1 else 0)
    have hc : (p1 = e.permCongr σ q1 ∧ p2 = q2) ↔ (e.symm p1 = σ (e.symm q1) ∧ p2 = q2) := by
      rw [Equiv.permCongr_apply, Equiv.symm_apply_eq]
    by_cases h : e.symm p1 = σ (e.symm q1) ∧ p2 = q2
    · rw [if_pos (hc.2 h), if_pos h]
    · rw [if_neg (fun h' => h (hc.1 h')), if_neg h]
  | child w h fwd =>
    cases fwd
    · exact congrFun (congrFun (childR_map e w h _) (p1, p2)) (q1, q2)
    · exact congrFun (congrFun (childR_map e w h _) (p1, p2)) (q1, q2)

theorem RStep.den_map (T : Op κ) (e : R ≃ R') (st : RStep R m) :
    (st.map e).den T = (st.den T).submatrix (stE e).symm (stE e).symm := by
  ext p q
  rw [submatrix_apply, RStep.den_map_apply]
  rfl

theorem denListR_map (T : Op κ) (e : R ≃ R') (l : List (RStep R m)) :
    denListR T (l.map (RStep.map e)) = (denListR T l).submatrix (stE e).symm (stE e).symm := by
  induction l using List.reverseRecOn with
  | nil => simp [denListR]
  | append_singleton l s ih =>
    rw [List.map_append, List.map_singleton, denListR_append, denListR_append, ih,
      denListR_single, denListR_single, RStep.den_map, submatrix_mul_equiv]

lemma roleDiagR_map (e : R ≃ R') (A : Op (Fin m × κ)) :
    (roleDiagR A : ROp R m κ).submatrix (stE e).symm (stE e).symm = roleDiagR A := by
  ext ⟨p1, p2⟩ ⟨q1, q2⟩
  simp [roleDiagR, blockOp, stE]

end Map

/-! ## The instance -/

/-- `W_c`. -/
abbrev Wc : ℕ := 1873807244643542670000
/-- `s_c`. -/
abbrev sc : ℕ := 1873807244636671267308000000

/-- **(a)** The roles of the complex network, numbered. -/
noncomputable def eW : NetComplex.Wr NetComplex.ind₀ ≃ Fin Wc :=
  Fintype.equivFinOfCardEq NetComplex.card_Wr₀

instance : NeZero Wc := ⟨by norm_num⟩

/-- **The restricted Proposition 8 interface of the complex network.** -/
noncomputable def complexIface : Prop8IfaceR Wc (100 ^ 3) sc where
  net := (prog NetComplex.ind₀).map (RStep.map P8Lift.eW)
  count := by
    rw [List.countP_map]
    have : (RStep.isChild ∘ RStep.map (m := 100 ^ 3) P8Lift.eW) = RStep.isChild := by
      funext st; exact RStep.isChild_map P8Lift.eW st
    rw [this, prog_count NetComplex.ind₀_card (by norm_num), prop8_count]
  correct κ _ _ := by
    rw [denListR_map, prog_correct NetComplex.ind₀_card (by norm_num) NetComplex.ind₀_inj,
      roleDiagR_map]
    rfl

end P8Lift

end