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

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

import Definitions.Def_IntMul_Kappa_K_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.NetComplexLemma5
/-!
# Lemma 5 (complex construction) as a scalar gate network over a ring with `1/2`

Scalars lie in a commutative ring `R` in which `2` is invertible (the paper uses `ℤ[i, 1/2]`).
Parameters as in `NetScalar`: a ground set `Fin h`, a finite type `T` of triples with
`ind : T → Finset (Fin h)`, `#(ind t) = 3`, `ind` injective.

1. Generic scalar gates `CGate R W = Matrix W W R × Finset W`, runs, elementary gates with
   coefficients `egM A r c k = ∑ₓ k x · e_{r x, c x}`, inverse gates `invG` / `invNamed`
   (reverse the list, invert each gate), and the bridge to `AModel.NGate`.
2. One invocation `Inv`: sources `x_T`, targets `y_S`, side wires `A_{ST}` for ordered pairs of
   distinct triples with even intersection, central wires `C_i` and `C_*` (indexed by
   `Option (Fin h)`, `none = *`). Copy `A_{ST} += x_T`; side injection
   `y_S += -∑_T (|S∩T|-1)/2 · A_{ST}`; gather `C_i += ∑_{T ∋ i} x_T`, `C_* += ∑_T x_T`;
   scatter `y_S += (∑_{i∈S} C_i - C_*)/2`. Eight-row forward schedule (2) of the paper.
   `forward_invocation`: `y_S ↦ y_S + x_S`, everything else unchanged, for arbitrary scratch.
   `inverse_invocation`: the inverse schedule gives `y_S ↦ y_S - x_S`.
3. Three stages (`X → Y` forward, `Y → X` inverse, `X → Y` forward): `complex_exchange`
   `(X_a, Y_a) ↦ (-Y_a, X_a)` with scratch restored, i.e. the signed route
   `scalarRun gates v (ρ w) = ε w * v w` (`ε (X a) = 1`, `ε (Y a) = -1`, scratch `1`); and the
   corrected network (one extra gate negating the physical `X` outputs) with the unsigned route,
   in the exact form required by `AModel.network_realizes`.
-/

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

namespace NetComplex

open Matrix Finset AModel

/-! ## 1. Generic scalar gates over a commutative ring -/

section Generic

variable {R : Type*} [CommRing R] {W : Type*} [Fintype W] [DecidableEq W]

/-- A scalar gate: matrix and touched set. -/
abbrev CGate (R W : Type*) := Matrix W W R × Finset W

/-- `NGate.OK` without the label. -/
def SOK (g : CGate R W) : Prop :=
  ∀ w w', (w ∉ g.2 → g.1 w w' = if w = w' then 1 else 0) ∧
    (w ∈ g.2 → w' ∉ g.2 → g.1 w w' = 0)

/-- Scalar run of unlabelled gates. -/
def sRun (gs : List (CGate R W)) (v : W → R) : W → R :=
  gs.foldl (fun v g => g.1 *ᵥ v) v

/-- Matrix of a gate list (later gates on the left). -/
def runMat (gs : List (CGate R W)) : Matrix W W R :=
  gs.foldl (fun M g => g.1 * M) 1

lemma foldl_mat (gs : List (CGate R W)) (A : Matrix W W R) :
    gs.foldl (fun M g => g.1 * M) A = runMat gs * A := by
  induction gs generalizing A with
  | nil => simp [runMat]
  | cons g gs ih =>
    simp only [List.foldl_cons, runMat]
    rw [ih, ih (g.1 * 1), mul_one, mul_assoc]

lemma runMat_append (l₁ l₂ : List (CGate R W)) : runMat (l₁ ++ l₂) = runMat l₂ * runMat l₁ := by
  simp only [runMat, List.foldl_append]
  exact foldl_mat _ _

lemma runMat_cons (g : CGate R W) (l : List (CGate R W)) : runMat (g :: l) = runMat l * g.1 := by
  rw [show g :: l = [g] ++ l from rfl, runMat_append]
  simp [runMat]

lemma runMat_single (g : CGate R W) : runMat [g] = g.1 := by simp [runMat]

lemma sRun_eq (gs : List (CGate R W)) (v : W → R) : sRun gs v = runMat gs *ᵥ v := by
  induction gs generalizing v with
  | nil => simp [sRun, runMat]
  | cons g gs ih =>
    simp only [sRun, List.foldl_cons] at ih ⊢
    rw [ih, runMat_cons, ← Matrix.mulVec_mulVec]

/-- Attach labels to unlabelled gates. -/
def labelled {N M : Type*} (lab : N → M) (gs : List (N × CGate R W)) : List (NGate W R M) :=
  gs.map fun g => (g.2.1, g.2.2, lab g.1)

lemma scalarRun_labelled {N M : Type*} (lab : N → M) (gs : List (N × CGate R W)) (v : W → R) :
    scalarRun (labelled lab gs) v = sRun (gs.map Prod.snd) v := by
  induction gs generalizing v with
  | nil => rfl
  | cons g gs ih =>
    simp only [labelled, List.map_cons, scalarRun, sRun, List.foldl_cons] at ih ⊢
    exact ih _

lemma ok_labelled {N M : Type*} [AddGroup M] (lab : N → M) (gs : List (N × CGate R W))
    (h : ∀ g ∈ gs, SOK g.2) : ∀ g ∈ labelled lab gs, g.OK := by
  intro g hg
  simp only [labelled, List.mem_map] at hg
  obtain ⟨g', hg', rfl⟩ := hg
  exact h g' hg'

/-- Elementary gate matrix with coefficients: add `k x · (c x)` into `r x`, for `x ∈ A`. -/
def egM {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) : Matrix W W R :=
  ∑ x ∈ A, single (r x) (c x) (k x)

lemma egM_apply {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (w w' : W) :
    egM A r c k w w' = ∑ x ∈ A, if r x = w ∧ c x = w' then k x else 0 := by
  simp [egM, Matrix.sum_apply, single_apply]

lemma egM_mulVec {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (v : W → R) (w : W) :
    (egM A r c k *ᵥ v) w = ∑ x ∈ A, if r x = w then k x * v (c x) else 0 := by
  simp only [mulVec, dotProduct, egM_apply, Finset.sum_mul]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun x _ => ?_
  by_cases h : r x = w <;> simp [h]

lemma egM_smul {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (s : R) :
    egM A r c (fun x => s * k x) = s • egM A r c k := by
  simp [egM, Finset.smul_sum, smul_single]

lemma egM_ok {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (K : Finset W)
    (hK : ∀ x ∈ A, r x ∈ K ∧ c x ∈ K) : SOK ((1 + egM A r c k, K) : CGate R W) := by
  intro w w'
  refine ⟨fun hw => ?_, fun hw hw' => ?_⟩
  · simp only [Matrix.add_apply, one_apply, egM_apply]
    rw [Finset.sum_eq_zero, add_zero]
    intro x hx
    have : r x ≠ w := fun h => hw (h ▸ (hK x hx).1)
    simp [this]
  · simp only [Matrix.add_apply, one_apply, egM_apply]
    have hne : w ≠ w' := fun h => hw' (h ▸ hw)
    rw [Finset.sum_eq_zero]
    · simp [hne]
    intro x hx
    have : c x ≠ w' := fun h => hw' (h ▸ (hK x hx).2)
    simp [this]

lemma egM_mul {ι κ : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (B : Finset κ)
    (r' c' : κ → W) (k' : κ → R) :
    egM A r c k * egM B r' c' k' =
      ∑ x ∈ A, ∑ y ∈ B, if c x = r' y then single (r x) (c' y) (k x * k' y) else 0 := by
  simp only [egM, Finset.sum_mul, Finset.mul_sum]
  rw [Finset.sum_comm]
  refine Finset.sum_congr rfl fun x _ => ?_
  refine Finset.sum_congr rfl fun y _ => ?_
  by_cases h : c x = r' y
  · simp [h]
  · simp [h]

lemma egM_mul_zero {ι κ : Type*} (A : Finset ι) (r c : ι → W) (k : ι → R) (B : Finset κ)
    (r' c' : κ → W) (k' : κ → R) (h : ∀ x y, c x ≠ r' y) : egM A r c k * egM B r' c' k' = 0 := by
  rw [egM_mul]
  exact Finset.sum_eq_zero fun x _ => Finset.sum_eq_zero fun y _ => by simp [h x y]

/-- Blocks whose net effects `1 + f i` pairwise compose to zero products run as `1 + ∑ f`. -/
lemma runMat_flatMap {ι : Type*} (L : List ι) (blk : ι → List (CGate R W))
    (f : ι → Matrix W W R) (hb : ∀ i ∈ L, runMat (blk i) = 1 + f i)
    (hz : ∀ i ∈ L, ∀ j ∈ L, f i * f j = 0) :
    runMat (L.flatMap blk) = 1 + (L.map f).sum := by
  induction L with
  | nil => simp [runMat]
  | cons i L ih =>
    rw [List.flatMap_cons, runMat_append, ih (fun j hj => hb j (List.mem_cons_of_mem _ hj))
      (fun a ha b hb' => hz a (List.mem_cons_of_mem _ ha) b (List.mem_cons_of_mem _ hb')),
      hb i List.mem_cons_self]
    have : (L.map f).sum * f i = 0 := by
      rw [← List.sum_map_mul_right]
      exact List.sum_eq_zero fun x hx => by
        obtain ⟨j, hj, rfl⟩ := List.mem_map.1 hx
        exact hz j (List.mem_cons_of_mem _ hj) i List.mem_cons_self
    rw [List.map_cons, List.sum_cons]
    simp only [mul_add, add_mul, one_mul, mul_one, this]
    abel

lemma runMat_map {ι : Type*} (L : List ι) (g : ι → CGate R W)
    (f : ι → Matrix W W R) (hb : ∀ i ∈ L, (g i).1 = 1 + f i)
    (hz : ∀ i ∈ L, ∀ j ∈ L, f i * f j = 0) :
    runMat (L.map g) = 1 + (L.map f).sum := by
  rw [show L.map g = L.flatMap fun i => [g i] by induction L <;> simp_all]
  exact runMat_flatMap L _ f (fun i hi => by simp [runMat, hb i hi]) hz

/-- The inverse of a gate `1 + f` with `f² = 0` is `1 - f`; we write it as `1 - (M - 1)`. -/
def invG (g : CGate R W) : CGate R W := (1 - (g.1 - 1), g.2)

/-- The inverse schedule: reverse the list and invert every gate (names are kept). -/
def invNamed {N : Type*} (l : List (N × CGate R W)) : List (N × CGate R W) :=
  (l.map fun g => (g.1, invG g.2)).reverse

lemma invG_ok {g : CGate R W} (hg : SOK g) : SOK (invG g) := by
  intro w w'
  obtain ⟨h1, h2⟩ := hg w w'
  refine ⟨fun hw => ?_, fun hw hw' => ?_⟩
  · simp only [invG, Matrix.sub_apply, one_apply, h1 hw]
    split_ifs <;> simp
  · have hne : w ≠ w' := fun e => hw' (e ▸ hw)
    simp [invG, Matrix.sub_apply, one_apply, h2 hw hw', hne]

lemma invNamed_ok {N : Type*} (l : List (N × CGate R W)) (h : ∀ g ∈ l, SOK g.2) :
    ∀ g ∈ invNamed l, SOK g.2 := by
  intro g hg
  simp only [invNamed, List.mem_reverse, List.mem_map] at hg
  obtain ⟨g', hg', rfl⟩ := hg
  exact invG_ok (h g' hg')

/-- The inverse schedule undoes the schedule, provided each gate is `1 + f` with `f² = 0`. -/
lemma runMat_invNamed {N : Type*} (l : List (N × CGate R W))
    (h : ∀ g ∈ l, (g.2.1 - 1) * (g.2.1 - 1) = 0) :
    runMat ((invNamed l).map Prod.snd) * runMat (l.map Prod.snd) = 1 := by
  induction l with
  | nil => simp [invNamed, runMat]
  | cons g l ih =>
    have hg := h g List.mem_cons_self
    have ih' := ih (fun g' hg' => h g' (List.mem_cons_of_mem _ hg'))
    have e : (invNamed (g :: l)).map Prod.snd = (invNamed l).map Prod.snd ++ [invG g.2] := by
      simp [invNamed]
    rw [e, runMat_append, List.map_cons, runMat_cons g.2, runMat_single]
    simp only [invG]
    rw [mul_assoc, ← mul_assoc (runMat _) (runMat _), ih', one_mul]
    have : (1 - (g.2.1 - 1)) * g.2.1 = 1 - (g.2.1 - 1) * (g.2.1 - 1) := by noncomm_ring
    rw [this, hg, sub_zero]

end Generic

/-! ## 2. One invocation (complex construction) -/

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]

/-- Ordered neighbor pairs `(S, T)`: distinct triples with even intersection. -/
abbrev Nb := {st : T × T // st.1 ≠ st.2 ∧ #(ind st.1 ∩ ind st.2) % 2 = 0}

/-- Incidence of a central wire `o` (`some i` = `C_i`, `none` = `C_*`) with a triple. -/
def incB : Option (Fin h) → T → Bool
  | none, _ => true
  | some i, t => decide (i ∈ ind t)

/-- Incidences `(o, T)`. -/
abbrev Pinc : Finset (Option (Fin h) × T) := univ.filter fun q => incB ind q.1 q.2 = true

/-- Scatter coefficient: `1/2` from `C_i`, `-1/2` from `C_*`. -/
def kS : Option (Fin h) → R
  | none => -⅟2
  | some _ => ⅟2

/-- Side-injection coefficient for the neighbor pair `(S, T)`: `-(|S ∩ T| - 1)/2`. -/
def kD (n : Nb ind) : R := -(((#(ind n.1.1 ∩ ind n.1.2) : ℕ) : R) - 1) * ⅟2

/-- The wires of one invocation. -/
structure Inv (W : Type*) where
  src : T → W
  tgt : T → W
  side : Nb ind → W
  cen : Option (Fin h) → W

variable {ind}

/-- Wires of an invocation are distinct. -/
structure Inv.Good (I : Inv ind W) : Prop where
  src_inj : Function.Injective I.src
  tgt_inj : Function.Injective I.tgt
  side_inj : Function.Injective I.side
  cen_inj : Function.Injective I.cen
  st : ∀ a b, I.src a ≠ I.tgt b
  ss : ∀ a n, I.src a ≠ I.side n
  sc : ∀ a i, I.src a ≠ I.cen i
  ts : ∀ a n, I.tgt a ≠ I.side n
  tc : ∀ a i, I.tgt a ≠ I.cen i
  sic : ∀ n i, I.side n ≠ I.cen i

variable (R)

/-- Side injection into target `y_S` with sign `s` (one gate per target). -/
def Inv.sideG (I : Inv ind W) (s : R) (S : T) : CGate R W :=
  (1 + egM (univ.filter fun n : Nb ind => n.1.1 = S) (fun n => I.tgt n.1.1) I.side
      (fun n => s * kD ind n),
   insert (I.tgt S) ((univ.filter fun n : Nb ind => n.1.1 = S).image I.side))

/-- Copy of source `x_T` into the side wires `A_{ST}` with sign `s` (one gate per source). -/
def Inv.copyG (I : Inv ind W) (s : R) (t : T) : CGate R W :=
  (1 + egM (univ.filter fun n : Nb ind => n.1.2 = t) I.side (fun n => I.src n.1.2)
      (fun _ => s * 1),
   insert (I.src t) ((univ.filter fun n : Nb ind => n.1.2 = t).image I.side))

/-- Scatter `y_S += s (∑_{i ∈ S} C_i - C_*)/2` (one gate on targets and center). -/
def Inv.scatG (I : Inv ind W) (s : R) : CGate R W :=
  (1 + egM (Pinc ind) (fun q => I.tgt q.2) (fun q => I.cen q.1) (fun q => s * kS q.1),
   univ.image I.tgt ∪ univ.image I.cen)

/-- Gather `C_i += s ∑_{T ∋ i} x_T`, `C_* += s ∑_T x_T` (one gate on sources and center). -/
def Inv.gathG (I : Inv ind W) (s : R) : CGate R W :=
  (1 + egM (Pinc ind) (fun q => I.cen q.1) (fun q => I.src q.2) (fun _ => s * 1),
   univ.image I.src ∪ univ.image I.cen)

/-- The forward schedule (2) of one invocation, rows 0–7 with signs `−J, −R, +V, +G, +R, +J,
−G, −V`, with names (row, triple). -/
noncomputable def Inv.named (I : Inv ind W) : List (NetScalar.IName T × CGate R W) :=
  ((univ : Finset T).toList.map fun S => ((0, some S), I.sideG R (-1) S)) ++
  [((1, none), I.scatG R (-1))] ++
  ((univ : Finset T).toList.map fun t => ((2, some t), I.copyG R 1 t)) ++
  [((3, none), I.gathG R 1)] ++
  [((4, none), I.scatG R 1)] ++
  ((univ : Finset T).toList.map fun S => ((5, some S), I.sideG R 1 S)) ++
  [((6, none), I.gathG R (-1))] ++
  ((univ : Finset T).toList.map fun t => ((7, some t), I.copyG R (-1) t))

noncomputable def Inv.gates (I : Inv ind W) : List (CGate R W) := (I.named R).map Prod.snd

/-- Row matrices: `D` side injection, `B` copy, `C` scatter, `G` gather. -/
def Inv.Dm (I : Inv ind W) : Matrix W W R :=
  egM univ (fun n : Nb ind => I.tgt n.1.1) I.side (kD ind)
def Inv.Bm (I : Inv ind W) : Matrix W W R :=
  egM univ I.side (fun n : Nb ind => I.src n.1.2) (fun _ => 1)
def Inv.Cm (I : Inv ind W) : Matrix W W R :=
  egM (Pinc ind) (fun q => I.tgt q.2) (fun q => I.cen q.1) (fun q => kS q.1)
def Inv.Gm (I : Inv ind W) : Matrix W W R :=
  egM (Pinc ind) (fun q => I.cen q.1) (fun q => I.src q.2) (fun _ => 1)
/-- Net change `J`: `y_S += x_S`. -/
def Inv.Jm (I : Inv ind W) : Matrix W W R := egM univ I.tgt I.src (fun _ => 1)

/-- Kernel matrix `∑_{S,T} κ S T · e_{y_S, x_T}`. -/
def Inv.kern (I : Inv ind W) (κ : T → T → R) : Matrix W W R :=
  ∑ S, ∑ t, single (I.tgt S) (I.src t) (κ S t)

variable {R}

lemma Inv.kern_add (I : Inv ind W) (κ κ' : T → T → R) :
    I.kern R κ + I.kern R κ' = I.kern R (κ + κ') := by
  simp only [Inv.kern, ← Finset.sum_add_distrib, Pi.add_apply, single_add]

lemma Inv.sum_single_collect (I : Inv ind W) {ι : Type*} (A : Finset ι) (a b : ι → T)
    (k : ι → R) : ∑ x ∈ A, single (I.tgt (a x)) (I.src (b x)) (k x) =
      I.kern R (fun S t => ∑ x ∈ A, if a x = S ∧ b x = t then k x else 0) := by
  unfold Inv.kern
  have hs : ∀ (S t : T) (f : ι → R), single (I.tgt S) (I.src t) (∑ x ∈ A, f x) =
      ∑ x ∈ A, single (I.tgt S) (I.src t) (f x) := fun S t f =>
    map_sum (singleAddMonoidHom (I.tgt S) (I.src t)) f A
  simp only [hs]
  symm
  rw [Finset.sum_congr rfl fun S _ => Finset.sum_comm, Finset.sum_comm]
  refine Finset.sum_congr rfl fun x _ => ?_
  rw [Finset.sum_eq_single (a x)]
  · rw [Finset.sum_eq_single (b x)]
    · simp
    · intro t _ ht; simp [Ne.symm ht]
    · simp
  · intro S _ hS
    exact Finset.sum_eq_zero fun t _ => by simp [Ne.symm hS]
  · simp

lemma ite_single {α β : Type*} [DecidableEq α] [DecidableEq β] (p : Prop) [Decidable p]
    (i : α) (j : β) (c : R) :
    (if p then (single i j c : Matrix α β R) else 0) = single i j (if p then c else 0) := by
  split_ifs <;> simp

/-- The central coefficient: `∑_{o ∋ S, T} kS o = (|S ∩ T| - 1)/2`. -/
lemma central_coeff (S t : T) :
    ∑ o, (if incB ind o S = true ∧ incB ind o t = true then (kS o : R) else 0) =
      (((#(ind S ∩ ind t) : ℕ) : R) - 1) * ⅟2 := by
  rw [Fintype.sum_option]
  simp only [incB, kS, and_self, if_true, decide_eq_true_eq]
  rw [show (∑ i : Fin h, if i ∈ ind S ∧ i ∈ ind t then (⅟2 : R) else 0) =
      ∑ i ∈ univ, if i ∈ ind S ∩ ind t then (⅟2 : R) else 0 by simp [Finset.mem_inter],
    Finset.sum_ite_mem, Finset.univ_inter, Finset.sum_const, nsmul_eq_mul]
  ring

variable {I : Inv ind W}

lemma Inv.Cm_mul_Gm (hG : I.Good) : I.Cm R * I.Gm R =
    I.kern R (fun S t => (((#(ind S ∩ ind t) : ℕ) : R) - 1) * ⅟2) := by
  unfold Inv.Cm Inv.Gm
  rw [egM_mul]
  simp only [hG.cen_inj.eq_iff, ite_single, mul_one]
  rw [← Finset.sum_product' (f := fun (q q' : Option (Fin h) × T) => single (I.tgt q.2) (I.src q'.2)
    (if q.1 = q'.1 then (kS q.1 : R) else 0))]
  rw [I.sum_single_collect (Pinc ind ×ˢ Pinc ind) (fun x => x.1.2) (fun x => x.2.2)]
  congr 1
  funext S t
  rw [← central_coeff S t, Finset.sum_product]
  simp only [Finset.sum_filter, Fintype.sum_prod_type]
  refine Finset.sum_congr rfl fun o _ => ?_
  rw [Finset.sum_eq_single S]
  · rw [Finset.sum_eq_single o]
    · rw [Finset.sum_eq_single t]
      · by_cases h1 : incB ind o S = true <;> by_cases h2 : incB ind o t = true <;> simp [h1, h2]
      · intro t' _ ht'; split_ifs <;> simp_all
      · simp
    · intro o' _ ho'
      exact Finset.sum_eq_zero fun t' _ => by split_ifs <;> simp_all
    · simp
  · intro S' _ hS'
    split_ifs
    · exact Finset.sum_eq_zero fun o' _ => Finset.sum_eq_zero fun t' _ => by split_ifs <;> simp_all
    · rfl
  · simp

/-- Side coefficient as a kernel: `-(|S ∩ T| - 1)/2` on neighbor pairs, `0` otherwise. -/
def sideCoeff (ind : T → Finset (Fin h)) (S t : T) : R :=
  if S ≠ t ∧ #(ind S ∩ ind t) % 2 = 0 then -(((#(ind S ∩ ind t) : ℕ) : R) - 1) * ⅟2 else 0

lemma Inv.Dm_mul_Bm (hG : I.Good) : I.Dm R * I.Bm R = I.kern R (sideCoeff ind) := by
  unfold Inv.Dm Inv.Bm
  rw [egM_mul]
  simp only [hG.side_inj.eq_iff, mul_one, Finset.sum_ite_eq, Finset.mem_univ, if_true]
  rw [I.sum_single_collect univ (fun n : Nb ind => n.1.1) (fun n => n.1.2)]
  congr 1
  funext S t
  unfold sideCoeff
  by_cases hP : S ≠ t ∧ #(ind S ∩ ind t) % 2 = 0
  · rw [if_pos hP, Finset.sum_eq_single (⟨(S, t), hP⟩ : Nb ind)]
    · simp [kD]
    · intro n _ hn
      rw [if_neg]
      rintro ⟨h1, h2⟩
      exact hn (Subtype.ext (Prod.ext h1 h2))
    · simp
  · rw [if_neg hP]
    refine Finset.sum_eq_zero fun n _ => ?_
    rw [if_neg]
    rintro ⟨h1, h2⟩
    exact hP (h1 ▸ h2 ▸ n.2)

lemma Inv.Jm_eq : I.Jm R = I.kern R (fun S t => if S = t then 1 else 0) := by
  unfold Inv.Jm egM
  have hc := I.sum_single_collect (univ : Finset T) id id (fun _ => (1 : R))
  simp only [id] at hc
  rw [hc]
  congr 1
  funext S t
  by_cases e : S = t
  · subst e; simp
  · rw [if_neg e]
    exact Finset.sum_eq_zero fun x _ => if_neg fun (h' : x = S ∧ x = t) => e (h'.1 ▸ h'.2)

/-- Distinct triples have intersection at most two. -/
lemma inter_le_two (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) {S t : T}
    (e : S ≠ t) : #(ind S ∩ ind t) ≤ 2 := by
  have hle : #(ind S ∩ ind t) ≤ 3 := (hcard S) ▸ Finset.card_le_card Finset.inter_subset_left
  have hne : #(ind S ∩ ind t) ≠ 3 := by
    intro h3
    have h1 : ind S ∩ ind t = ind S :=
      Finset.eq_of_subset_of_card_le Finset.inter_subset_left (by rw [h3, hcard])
    have h2 : ind S ∩ ind t = ind t :=
      Finset.eq_of_subset_of_card_le Finset.inter_subset_right (by rw [h3, hcard])
    exact e (hinj (h1.symm.trans h2))
  omega

/-- The key coefficient identity: central `(|S∩T|-1)/2` plus side equals `[S = T]`. -/
lemma key_coeff (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) (S t : T) :
    (((#(ind S ∩ ind t) : ℕ) : R) - 1) * ⅟2 + sideCoeff ind S t = if S = t then 1 else 0 := by
  unfold sideCoeff
  by_cases e : S = t
  · subst e
    rw [Finset.inter_self, hcard]
    simp only [ne_eq, not_true_eq_false, false_and, if_false, add_zero, if_true]
    rw [show ((3 : ℕ) : R) - 1 = 2 by push_cast; ring, mul_invOf_self]
  · have hle := inter_le_two hcard hinj e
    rw [if_neg e]
    generalize #(ind S ∩ ind t) = n at hle ⊢
    interval_cases n
    · simp [e]
    · simp
    · simp only [ne_eq, e, not_false_eq_true, true_and, Nat.reduceMod, if_true]
      ring

/-- Net target change of a forward invocation: `R G + J V = (y += x)`. -/
lemma Inv.CG_add_DB (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) (hG : I.Good) :
    I.Cm R * I.Gm R + I.Dm R * I.Bm R = I.Jm R := by
  rw [I.Cm_mul_Gm hG, I.Dm_mul_Bm hG, Inv.Jm_eq, Inv.kern_add]
  congr 1
  funext S t
  exact key_coeff hcard hinj S t

lemma Inv.runMat_side (hG : I.Good) (k : Fin 8) (s : R) :
    runMat (((univ : Finset T).toList.map fun S =>
      (((k, some S) : NetScalar.IName T), I.sideG R s S)).map Prod.snd) = 1 + s • I.Dm R := by
  rw [List.map_map]
  rw [runMat_map _ _ (fun S => egM (univ.filter fun n : Nb ind => n.1.1 = S)
    (fun n => I.tgt n.1.1) I.side (fun n => s * kD ind n)) (fun _ _ => rfl)
    (fun _ _ _ _ => egM_mul_zero _ _ _ _ _ _ _ _ fun x y => (hG.ts _ _).symm)]
  rw [Finset.sum_map_toList]
  unfold Inv.Dm egM
  rw [Finset.smul_sum]
  simp only [smul_single, smul_eq_mul]
  rw [Finset.sum_fiberwise]

lemma Inv.runMat_copy (hG : I.Good) (k : Fin 8) (s : R) :
    runMat (((univ : Finset T).toList.map fun t =>
      (((k, some t) : NetScalar.IName T), I.copyG R s t)).map Prod.snd) = 1 + s • I.Bm R := by
  rw [List.map_map]
  rw [runMat_map _ _ (fun t => egM (univ.filter fun n : Nb ind => n.1.2 = t)
    I.side (fun n => I.src n.1.2) (fun _ => s * 1)) (fun _ _ => rfl)
    (fun _ _ _ _ => egM_mul_zero _ _ _ _ _ _ _ _ fun x y => hG.ss _ _)]
  rw [Finset.sum_map_toList]
  unfold Inv.Bm egM
  rw [Finset.smul_sum]
  simp only [smul_single, smul_eq_mul]
  rw [Finset.sum_fiberwise (f := fun n : Nb ind => single (I.side n) (I.src n.1.2) (s * 1))]

lemma Inv.runMat_scat (k : Fin 8) (s : R) :
    runMat ([(((k, none) : NetScalar.IName T), I.scatG R s)].map Prod.snd) = 1 + s • I.Cm R := by
  simp [runMat, Inv.scatG, Inv.Cm, ← egM_smul]

lemma Inv.runMat_gath (k : Fin 8) (s : R) :
    runMat ([(((k, none) : NetScalar.IName T), I.gathG R s)].map Prod.snd) = 1 + s • I.Gm R := by
  simp [runMat, Inv.gathG, Inv.Gm, ← egM_smul]

/-- **Lemma 5, matrix form.** The forward schedule of one invocation has matrix `1 + J`. -/
theorem Inv.runMat_gates (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind)
    (hG : I.Good) : runMat (I.gates R) = 1 + I.Jm R := by
  have z : ∀ {ι κ : Type _} (A : Finset ι) (r c : ι → W) (k : ι → R) (B : Finset κ)
      (r' c' : κ → W) (k' : κ → R),
      (∀ x y, c x ≠ r' y) → egM A r c k * egM B r' c' k' = 0 := fun A r c k B r' c' k' h =>
    egM_mul_zero A r c k B r' c' k' h
  have key := NetScalar.eight_rows (I.Bm R) (I.Gm R) (I.Cm R) (I.Dm R)
    (z _ _ _ _ _ _ _ _ fun _ _ => hG.ss _ _) (z _ _ _ _ _ _ _ _ fun _ _ => hG.sc _ _)
    (z _ _ _ _ _ _ _ _ fun _ _ => hG.st _ _) (z _ _ _ _ _ _ _ _ fun _ _ => hG.st _ _)
    (z _ _ _ _ _ _ _ _ fun _ _ => hG.ss _ _) (z _ _ _ _ _ _ _ _ fun _ _ => hG.sc _ _)
    (z _ _ _ _ _ _ _ _ fun _ _ => hG.st _ _) (z _ _ _ _ _ _ _ _ fun _ _ => hG.st _ _)
    (z _ _ _ _ _ _ _ _ fun _ _ => (hG.sic _ _).symm)
    (z _ _ _ _ _ _ _ _ fun _ _ => (hG.tc _ _).symm)
    (z _ _ _ _ _ _ _ _ fun _ _ => (hG.tc _ _).symm)
    (z _ _ _ _ _ _ _ _ fun _ _ => hG.sic _ _) (z _ _ _ _ _ _ _ _ fun _ _ => (hG.ts _ _).symm)
    (z _ _ _ _ _ _ _ _ fun _ _ => (hG.ts _ _).symm)
  rw [I.CG_add_DB hcard hinj hG] at key
  simp only [Inv.gates, Inv.named, List.map_append, runMat_append, I.runMat_side hG,
    I.runMat_copy hG, I.runMat_scat, I.runMat_gath, neg_one_smul, one_smul, ← sub_eq_add_neg]
  simpa only [mul_assoc] using key

/-- Every gate `1 + f` of an invocation has `f² = 0`. -/
lemma Inv.gates_sq (hG : I.Good) : ∀ g ∈ I.named R, (g.2.1 - 1) * (g.2.1 - 1) = 0 := by
  intro g hg
  simp only [Inv.named, List.mem_append, List.mem_map, Finset.mem_toList, Finset.mem_univ,
    true_and, List.mem_singleton] at hg
  rcases hg with ((((((⟨S, rfl⟩ | rfl) | ⟨t, rfl⟩) | rfl) | rfl) | ⟨S, rfl⟩) | rfl) | ⟨t, rfl⟩ <;>
    simp only [Inv.sideG, Inv.copyG, Inv.scatG, Inv.gathG, add_sub_cancel_left] <;>
    exact egM_mul_zero _ _ _ _ _ _ _ _ fun _ _ => by
      first | exact (hG.ts _ _).symm | exact hG.ss _ _ | exact (hG.tc _ _).symm | exact hG.sc _ _

variable (R) in
/-- The inverse schedule of an invocation. -/
noncomputable def Inv.invGates (I : Inv ind W) : List (CGate R W) :=
  (invNamed (I.named R)).map Prod.snd

/-- **Inverse invocation, matrix form**: `1 - J`. -/
theorem Inv.runMat_invGates (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind)
    (hG : I.Good) : runMat (I.invGates R) = 1 - I.Jm R := by
  have h1 := runMat_invNamed (I.named R) (I.gates_sq hG)
  have hJ : I.Jm R * I.Jm R = 0 := egM_mul_zero _ _ _ _ _ _ _ _ fun _ _ => hG.st _ _
  change runMat (I.invGates R) * runMat (I.gates R) = 1 at h1
  rw [I.runMat_gates hcard hinj hG] at h1
  calc runMat (I.invGates R) = runMat (I.invGates R) * ((1 + I.Jm R) * (1 - I.Jm R)) := by
        rw [show (1 + I.Jm R) * (1 - I.Jm R) = 1 - I.Jm R * I.Jm R by noncomm_ring, hJ,
          sub_zero, mul_one]
    _ = 1 - I.Jm R := by rw [← mul_assoc, h1, one_mul]

/-- Every gate of an invocation is a valid gate on its touched set. -/
theorem Inv.gates_ok (I : Inv ind W) : ∀ g ∈ I.named R, SOK g.2 := by
  intro g hg
  simp only [Inv.named, List.mem_append, List.mem_map, Finset.mem_toList, Finset.mem_univ,
    true_and, List.mem_singleton] at hg
  have hs : ∀ s S, SOK (I.sideG R s S) := fun s S => egM_ok _ _ _ _ _ fun x hx => by
    have : x.1.1 = S := (Finset.mem_filter.1 hx).2
    refine ⟨by simp [this], Finset.mem_insert_of_mem (Finset.mem_image_of_mem _ hx)⟩
  have hc : ∀ s t, SOK (I.copyG R s t) := fun s t => egM_ok _ _ _ _ _ fun x hx => by
    have : x.1.2 = t := (Finset.mem_filter.1 hx).2
    refine ⟨Finset.mem_insert_of_mem (Finset.mem_image_of_mem _ hx), by simp [this]⟩
  have hsc : ∀ s, SOK (I.scatG R s) := fun s => egM_ok _ _ _ _ _ fun x _ => by simp
  have hga : ∀ s, SOK (I.gathG R s) := fun s => egM_ok _ _ _ _ _ fun x _ => by simp
  rcases hg with ((((((⟨S, rfl⟩ | rfl) | ⟨t, rfl⟩) | rfl) | rfl) | ⟨S, rfl⟩) | rfl) | ⟨t, rfl⟩
  exacts [hs _ S, hsc _, hc _ t, hga _, hsc _, hs _ S, hga _, hc _ t]

end Invocation

/-! ## 3. The complex construction: three stages of invocations on the data banks -/

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 sum_emb)

/-- Wires: `X a`, `Y a` (`a ∈ 𝒯³`), side wires `A_{ST}` and central wires `C_i`, `C_*` of each
invocation `(stage j, bank p)`. -/
abbrev Wr := (T × T × T) ⊕ (T × T × T) ⊕ (Fin 3 × (T × T) × Nb ind) ⊕
  (Fin 3 × (T × T) × Option (Fin h))

variable {ind}

def wX (a : T × T × T) : Wr ind := Sum.inl a
def wY (a : T × T × T) : Wr ind := Sum.inr (Sum.inl a)
def wS (j : Fin 3) (p : T × T) (n : Nb ind) : Wr ind := Sum.inr (Sum.inr (Sum.inl (j, p, n)))
def wC (j : Fin 3) (p : T × T) (o : Option (Fin h)) : Wr ind :=
  Sum.inr (Sum.inr (Sum.inr (j, p, o)))

/-- Logical sources and targets of stage `j`: `X → Y` at stages 1 and 3, `Y → X` at stage 2. -/
def srcW (j : Fin 3) (a : T × T × T) : Wr ind := if j = 1 then wY a else wX a
def tgtW (j : Fin 3) (a : T × T × T) : Wr ind := if j = 1 then wX a else wY a

lemma srcW_ne_tgtW (j : Fin 3) (a b : T × T × T) : (srcW j a : Wr ind) ≠ tgtW j b := by
  unfold srcW tgtW wX wY; split_ifs <;> simp

/-- The invocation of stage `j` on bank `p`. -/
def inv (j : Fin 3) (p : T × T) : Inv ind (Wr ind) :=
  ⟨fun t => srcW j (emb j p t), fun t => tgtW j (emb j p t), wS j p, wC j p⟩

lemma inv_good (j : Fin 3) (p : T × T) : (NetComplex.inv j p : Inv ind (Wr ind)).Good := by
  have e := emb_inj (T := T) j p
  refine ⟨fun t t' h' => e ?_, fun t t' h' => e ?_, fun n n' h' => ?_, fun i i' h' => ?_,
    fun a b => srcW_ne_tgtW _ _ _, fun a n => ?_, fun a i => ?_, fun a n => ?_, fun a i => ?_,
    fun n i => ?_⟩ <;>
    simp only [NetComplex.inv, srcW, tgtW, wX, wY, wS, wC] at * <;> (try split_ifs at *) <;> simp_all

/-- Gate names: stage, invocation (bank), and the name inside the invocation. -/
abbrev GName (T : Type*) := Fin 3 × (T × T) × NetScalar.IName T

variable (R ind)

/-- The schedule of invocation `(j, p)`: forward at stages 1 and 3 (`j = 0, 2`), the inverse
forward schedule at stage 2 (`j = 1`). -/
noncomputable def schedJ (j : Fin 3) (p : T × T) : List (NetScalar.IName T × CGate R (Wr ind)) :=
  if j = 1 then invNamed ((NetComplex.inv j p).named R) else (NetComplex.inv j p).named R

/-- The named gate list of the complex construction: stage 1 (`X → Y`, forward), stage 2
(`Y → X`, inverse forward schedule), stage 3 (`X → Y`, forward). -/
noncomputable def cxNamed : List (GName T × CGate R (Wr ind)) :=
  ([0, 1, 2] : List (Fin 3)).flatMap fun j => (univ : Finset (T × T)).toList.flatMap fun p =>
    (schedJ R ind j p).map fun g => ((j, p, g.1), g.2)

/-- The scalar gates of the complex construction. -/
noncomputable def cxGates : List (CGate R (Wr ind)) := (cxNamed R ind).map Prod.snd

/-- The gates with labels attached by a naming function. -/
noncomputable def cxGatesL {M : Type*} (lab : GName T → M) : List (NGate (Wr ind) R M) :=
  labelled lab (cxNamed R ind)

/-- The underlying permutation of roles: `X a ↔ Y a`, auxiliaries fixed. -/
def ρ : Wr ind → Wr ind
  | Sum.inl a => Sum.inr (Sum.inl a)
  | Sum.inr (Sum.inl a) => Sum.inl a
  | Sum.inr (Sum.inr x) => Sum.inr (Sum.inr x)

/-- Route signs: an input at `X a` arrives at `Y a` with sign `+1`, an input at `Y a` arrives
at `X a` with sign `-1`, every scratch input arrives at itself with sign `+1`. -/
def ε : Wr ind → R
  | Sum.inl _ => 1
  | Sum.inr (Sum.inl _) => -1
  | Sum.inr (Sum.inr _) => 1

variable {R ind}

/-- Stage matrix `K_j = ∑_a e_{tgt a, src a}`. -/
def Kst (j : Fin 3) : Matrix (Wr ind) (Wr ind) R := egM univ (tgtW j) (srcW j) (fun _ => 1)

/-- Stage sign: `+1` (forward) at stages 1, 3; `-1` (inverse) at stage 2. -/
def σ (j : Fin 3) : R := if j = 1 then -1 else 1

lemma runMat_stage (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) (j : Fin 3) :
    runMat ((univ : Finset (T × T)).toList.flatMap fun p => (schedJ R ind j p).map Prod.snd) =
      1 + (σ j : R) • (Kst j : Matrix (Wr ind) (Wr ind) R) := by
  rw [runMat_flatMap _ _ (fun p => (σ j : R) • (NetComplex.inv j p : Inv ind (Wr ind)).Jm R)]
  · rw [Finset.sum_map_toList, ← Finset.smul_sum]
    congr 2
    unfold Kst Inv.Jm egM
    exact sum_emb j fun a => single (tgtW j a) (srcW j a) (1 : R)
  · intro p _
    unfold schedJ σ
    split_ifs
    · rw [show (invNamed ((NetComplex.inv j p).named R)).map Prod.snd = (NetComplex.inv j p).invGates R from rfl,
        (NetComplex.inv j p).runMat_invGates hcard hinj (inv_good j p), neg_one_smul, sub_eq_add_neg]
    · rw [one_smul]
      exact (NetComplex.inv j p).runMat_gates hcard hinj (inv_good j p)
  · intro p _ p' _
    rw [smul_mul_smul_comm, Inv.Jm, Inv.Jm,
      egM_mul_zero (univ : Finset T) (NetComplex.inv j p).tgt (NetComplex.inv j p).src _ _ (NetComplex.inv j p').tgt
        (NetComplex.inv j p').src _ fun _ _ => srcW_ne_tgtW _ _ _, smul_zero]

lemma cxGates_eq : cxGates R ind = ([0, 1, 2] : List (Fin 3)).flatMap fun j =>
    (univ : Finset (T × T)).toList.flatMap fun p => (schedJ R ind j p).map Prod.snd := by
  simp only [cxGates, cxNamed, List.map_flatMap, List.map_map]
  rfl

lemma runMat_cxGates (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) :
    runMat (cxGates R ind) = (1 + (σ 2 : R) • Kst 2) * ((1 + (σ 1 : R) • Kst 1) * (1 + (σ 0 : R) • Kst 0)) := by
  rw [cxGates_eq]
  simp only [List.flatMap_cons, List.flatMap_nil, List.append_nil, runMat_append,
    runMat_stage hcard hinj, mul_assoc]

lemma stage_apply (j : Fin 3) (u : Wr ind → R) (w : Wr ind) :
    ((1 + (σ j : R) • Kst j) *ᵥ u) w = u w + σ j * ∑ a, if tgtW j a = w then u (srcW j a) else 0 := by
  rw [Matrix.add_mulVec, Matrix.one_mulVec, Pi.add_apply, Matrix.smul_mulVec, Pi.smul_apply,
    Kst, egM_mulVec, smul_eq_mul]
  simp

/-- **Lemma 5, complex exchange (signed route).** The three stages send
`(X_a, Y_a) ↦ (-Y_a, X_a)` and restore every auxiliary wire, for arbitrary initial values:
the output on role `ρ w` is `ε w` times the input on role `w`. -/
theorem complex_exchange (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind)
    (v : Wr ind → R) (w : Wr ind) : sRun (cxGates R ind) v (NetComplex.ρ ind w) = NetComplex.ε R ind w * v w := by
  rw [sRun_eq, runMat_cxGates hcard hinj, ← Matrix.mulVec_mulVec, ← Matrix.mulVec_mulVec]
  rcases w with a | a | x
  · simp only [NetComplex.ρ, NetComplex.ε, stage_apply, srcW, tgtW, wX, wY]
    simp only [σ, Fin.isValue, Fin.reduceEq, if_false, if_true, Sum.inr.injEq, Sum.inl.injEq,
      reduceCtorEq, Finset.sum_ite_eq', Finset.mem_univ, Finset.sum_const_zero, add_zero]
    ring
  · simp only [NetComplex.ρ, NetComplex.ε, stage_apply, srcW, tgtW, wX, wY]
    simp only [σ, Fin.isValue, Fin.reduceEq, if_false, if_true, Sum.inr.injEq, Sum.inl.injEq,
      reduceCtorEq, Finset.sum_ite_eq', Finset.mem_univ, Finset.sum_const_zero, add_zero]
    ring
  · simp only [NetComplex.ρ, NetComplex.ε, stage_apply, srcW, tgtW, wX, wY]
    simp

theorem cxNamed_ok : ∀ g ∈ cxNamed R ind, SOK g.2 := by
  intro g hg
  simp only [cxNamed, List.mem_flatMap, List.mem_map] at hg
  obtain ⟨j, _, p, _, g', hg', rfl⟩ := hg
  unfold schedJ at hg'
  split_ifs at hg'
  · exact invNamed_ok _ (NetComplex.inv j p).gates_ok g' hg'
  · exact (NetComplex.inv j p).gates_ok g' hg'

/-! ### The corrected network: negate the physical `X` outputs -/

variable (R ind)

/-- One gate negating every `X` wire. -/
def fixG : CGate R (Wr ind) := (1 + egM univ wX wX (fun _ => -2), univ.image wX)

/-- The corrected named gate list (`none` names the sign gate). -/
noncomputable def cxFixNamed : List (Option (GName T) × CGate R (Wr ind)) :=
  (cxNamed R ind).map (fun g => (some g.1, g.2)) ++ [(none, fixG R ind)]

noncomputable def cxFixGatesL {M : Type*} (lab : Option (GName T) → M) :
    List (NGate (Wr ind) R M) :=
  labelled lab (cxFixNamed R ind)

variable {R ind}

lemma fixG_apply (u : Wr ind → R) (w : Wr ind) :
    ((fixG R ind).1 *ᵥ u) w = match w with
      | Sum.inl _ => -u w
      | Sum.inr _ => u w := by
  rw [fixG, Matrix.add_mulVec, Matrix.one_mulVec, Pi.add_apply, egM_mulVec]
  rcases w with a | b
  · simp only [wX, Sum.inl.injEq, Finset.sum_ite_eq', Finset.mem_univ, if_true]
    ring
  · simp [wX]

/-- **Corrected complex exchange.** After negating the physical `X` outputs, the circuit
routes every role `w` to `ρ w` unchanged (scratch roles included). -/
theorem complex_exchange_fixed (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind)
    (v : Wr ind → R) (w : Wr ind) :
    sRun ((cxFixNamed R ind).map Prod.snd) v (NetComplex.ρ ind w) = v w := by
  have e : (cxFixNamed R ind).map Prod.snd = cxGates R ind ++ [fixG R ind] := by
    simp [cxFixNamed, cxGates, List.map_map, Function.comp_def]
  rw [e, sRun_eq, runMat_append, runMat_single, ← Matrix.mulVec_mulVec, ← sRun_eq, fixG_apply]
  rcases w with a | a | x
  · simpa [NetComplex.ρ, NetComplex.ε] using complex_exchange hcard hinj v (Sum.inl a)
  · have := complex_exchange hcard hinj v (Sum.inr (Sum.inl a))
    simp only [NetComplex.ρ, NetComplex.ε] at this ⊢
    rw [this]; ring
  · simpa [NetComplex.ρ, NetComplex.ε] using complex_exchange hcard hinj v (Sum.inr (Sum.inr x))

theorem cxFixNamed_ok : ∀ g ∈ cxFixNamed R ind, SOK g.2 := by
  intro g hg
  simp only [cxFixNamed, List.mem_append, List.mem_map, List.mem_singleton] at hg
  rcases hg with ⟨g', hg', rfl⟩ | rfl
  · exact cxNamed_ok g' hg'
  · exact egM_ok _ _ _ _ _ fun x _ => by simp

/-- **Corrected complex exchange, network form**: exactly the hypotheses `hg`, `hρ` of
`AModel.network_realizes`, for any labelling of the gates. -/
theorem complex_exchange_fixed_net {M : Type*} [AddGroup M] (hcard : ∀ t, #(ind t) = 3)
    (hinj : Function.Injective ind) (lab : Option (GName T) → M) :
    (∀ g ∈ cxFixGatesL R ind lab, g.OK) ∧
      ∀ (v : Wr ind → R) w, scalarRun (cxFixGatesL R ind lab) v (NetComplex.ρ ind w) = v w := by
  refine ⟨ok_labelled lab _ cxFixNamed_ok, fun v w => ?_⟩
  rw [cxFixGatesL, scalarRun_labelled]
  exact complex_exchange_fixed hcard hinj v w

end Complex

end NetComplex

end

section
-- Source module: Solutions.NetProp7Chain
/-!
# Prop. 7, part 3: generic bookkeeping for `frameSum`

1. `frameSum_eq_chain`: the frame-change sum regrouped per wire: each wire contributes the
   sum of `f` over the consecutive differences of its label sequence (source label, the labels
   of the gates touching it in order, sink label).
2. `frameSum_rank_cast`: casting the rank sum to `ℚ`.
3. Transport of a gate network along a wire equivalence `Wr ≃ Fin W` and an additive label map
   (`trG`): gates stay OK, the scalar run is conjugated, and `frameSum` becomes `frameSum (f ∘ φ)`.
-/

set_option linter.unusedSectionVars false

namespace NetProp7

open Matrix Finset AModel

section ChainSec

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

/-- Sum of `f` over the consecutive differences of the label sequence `s, xs…, e`. -/
def chain (f : M → β) : M → List M → M → β
  | s, [], e => f (e - s)
  | s, x :: xs, e => f (x - s) + chain f x xs e

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

/-- The labels of the gates touching `w`, in order. -/
def labelsOn (w : Wr) (gates : List (NGate Wr R M)) : List M :=
  (gates.filter fun g => decide (w ∈ g.2.1)).map fun g => g.2.2

lemma labelsOn_cons (w : Wr) (g : NGate Wr R M) (gs : List (NGate Wr R M)) :
    labelsOn w (g :: gs) = if w ∈ g.2.1 then g.2.2 :: labelsOn w gs else labelsOn w gs := by
  unfold labelsOn
  by_cases hw : w ∈ g.2.1 <;> simp [hw]

end ChainSec

section Cast

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

end Cast

section Transport

variable {Wr V R M M' : Type*} [Fintype Wr] [DecidableEq Wr] [Fintype V] [DecidableEq V]
  [CommRing R]

/-- Transport a gate along `e : Wr ≃ V` and a label map `φ`. -/
def trG (e : Wr ≃ V) (φ : M → M') (g : NGate Wr R M) : NGate V R M' :=
  (g.1.submatrix e.symm e.symm, g.2.1.map e.toEmbedding, φ g.2.2)

end Transport

end NetProp7

end

section
-- Source module: Solutions.NetProp7Route
/-!
# Prop. 7, part 1: the bit network in physical gate order

At stage 2 the paper runs, at time `r`, the inverse of row `7 − r` (logical source `Y`, target
`X`), so that at every stage 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.
Over `𝔽₂` every gate is an involution, so the inverse schedule is the reversed gate list.

`named7` is `NetScalar.bitNamed` with the stage-2 invocation lists reversed. We prove that it
has the same matrix (`runMat_named7`) and hence the same routing (`bit_exchange7`).
-/

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

namespace NetProp7

open Matrix Finset AModel NetScalar

section Rev

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

end Rev

section Inv

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

end Inv

section Bit

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

/-- The named block of the invocation `(j, p)`: forward rows, reversed at stage 2 (`j = 1`). -/
noncomputable def blk (j : Fin 3) (p : T × T) : List (NetScalar.GName T × SGate (NetScalar.Wr ind)) :=
  if j = 1 then (((NetScalar.inv j p : NetScalar.Inv ind (NetScalar.Wr ind)).named.map fun g => ((j, p, g.1), g.2))).reverse
  else (NetScalar.inv j p : NetScalar.Inv ind (NetScalar.Wr ind)).named.map fun g => ((j, p, g.1), g.2)

/-- The bit network in physical order. -/
noncomputable def named7 : List (NetScalar.GName T × SGate (NetScalar.Wr ind)) :=
  ([0, 1, 2] : List (Fin 3)).flatMap fun j => (univ : Finset (T × T)).toList.flatMap fun p =>
    NetProp7.blk ind j p

variable {ind}

end Bit

end NetProp7

end

section
-- Source module: Solutions.NetProp7Names
/-!
# Prop. 7, part 4: which gates touch each wire

`namesOn w l` lists, in order, the names of the gates of `l` that touch the wire `w`. We compute
it for every wire of the physical-order bit network `named7`:

* `X a` is touched at stage `j` only by the invocation on its bank `pj j a`, at times
  `2, 3, 6, 7` (`names_X`); `Y a` at times `0, 1, 4, 5` (`names_Y`);
* a side wire `A_{ST}` of invocation `(j, p)` only by that invocation, at times `0, 2, 5, 7`
  (`names_S`), a central wire at times `1, 3, 4, 6` (`names_C`).

At stage 2 (`j = 1`) the list is reversed, which turns the rows `r` into the times `7 − r`.
-/

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

namespace NetProp7

open Finset NetScalar

/-! ## 1. Generic list facts -/

section Gen

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

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

lemma filter_eq_toList {α : Type*} [DecidableEq α] (t : α) :
    ∀ l : List α, l.Nodup → (l.filter fun x => decide (x = t)) = if t ∈ l then [t] else [] := by
  intro l
  induction l with
  | nil => simp
  | cons x l ih =>
    intro hl
    rw [List.nodup_cons] at hl
    rw [List.filter_cons, ih hl.2]
    by_cases hx : x = t
    · subst hx; simp [hl.1]
    · simp [hx, Ne.symm hx]

/-- A list with a single contributing index. -/
lemma flatMap_single {ι β : Type*} [DecidableEq ι] (F : ι → List β) (p₀ : ι) :
    ∀ l : List ι, l.Nodup → p₀ ∈ l → (∀ p ∈ l, p ≠ p₀ → F p = []) → l.flatMap F = F p₀ := by
  intro l
  induction l with
  | nil => simp
  | cons x l ih =>
    intro hl hp hF
    rw [List.nodup_cons] at hl
    rw [List.flatMap_cons]
    by_cases hx : x = p₀
    · subst hx
      rw [List.flatMap_eq_nil_iff.2 (fun p hp' => hF p (List.mem_cons_of_mem _ hp')
        (fun e => hl.1 (e ▸ hp'))), List.append_nil]
    · rw [hF x List.mem_cons_self hx, List.nil_append]
      exact ih hl.2 ((List.mem_cons.1 hp).resolve_left (Ne.symm hx))
        (fun p hp' => hF p (List.mem_cons_of_mem _ hp'))

lemma flatMap_univ_single {ι β : Type*} [Fintype ι] [DecidableEq ι] (F : ι → List β) (p₀ : ι)
    (hF : ∀ p, p ≠ p₀ → F p = []) : (univ : Finset ι).toList.flatMap F = F p₀ :=
  flatMap_single F p₀ _ (Finset.nodup_toList _) (by simp) (fun p _ hp => hF p hp)

lemma flatMap_univ_nil {ι β : Type*} [Fintype ι] (F : ι → List β)
    (hF : ∀ p, F p = []) : (univ : Finset ι).toList.flatMap F = [] :=
  List.flatMap_eq_nil_iff.2 fun p _ => hF p

end Gen

/-! ## 2. One invocation -/

section Invocation

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

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

end Invocation

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

section Bit

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

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

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

variable (ind)

variable {ind}

end Bit

end NetProp7

end