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

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

import Definitions.Def_IntMul_Kappa_K_Defs6

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.NetComplexP8Tensor
/-!
# Prop. 8, part 2: tensor labels over `𝔽₂` in `𝔽₂^{h³}`

The label space of the complex network is `F^{⊗3}` with `F = 𝔽₂^h` and the dot product; we index
it directly by `Fin (h ^ 3)` (through `e3 : Fin h × Fin h × Fin h ≃ Fin (h ^ 3)`), so that the
labels live in the same space `Fin m → ZMod 2` (`m = h³`) as the phase frames of
`NetComplexInterface`.

* `t3 x y z`: the pure tensor; `t3_dot`: `⟨x⊗y⊗z, x'⊗y'⊗z'⟩ = ⟨x,x'⟩⟨y,y'⟩⟨z,z'⟩`.
* `T3 U₀ U₁ U₂`: the span of pure tensors; monotonicity, distributivity over `⊔`, `⊥` factors.
* Orthonormal spanning sets (`HasON`): nondegeneracy, dimension `= card`, orthogonal sums, and
  tensor products (`ON_T3`: the tensor products of orthonormal bases form an orthonormal basis,
  of cardinality the product — this replaces `NetLabels.finrank_tensorSub`, which needs
  characteristic zero).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetComplexP8

open Matrix Finset Module NetLabels NetComplexOrtho

/-! ## 1. Pure tensors in `𝔽₂^{h³}` -/

section Tensor

variable {h : ℕ}

/-- One slot `F = 𝔽₂^h`. -/
abbrev Vh (h : ℕ) := Fin h → ZMod 2
/-- The label space `F^{⊗3} = 𝔽₂^{h³}`. -/
abbrev Vc (h : ℕ) := Fin (h ^ 3) → ZMod 2

/-- `Fin h × Fin h × Fin h ≃ Fin (h ^ 3)`. -/
def e3 (h : ℕ) : Fin h × Fin h × Fin h ≃ Fin (h ^ 3) :=
  ((Equiv.refl (Fin h)).prodCongr finProdFinEquiv).trans
    (finProdFinEquiv.trans (finCongr (by ring)))

/-- The pure tensor `x ⊗ y ⊗ z`. -/
def t3 (x y z : Vh h) : Vc h := fun i => tp x (tp y z) ((e3 h).symm i)

lemma dot_reindex (f g : Fin h × Fin h × Fin h → ZMod 2) :
    (fun i => f ((e3 h).symm i)) ⬝ᵥ (fun i => g ((e3 h).symm i)) = f ⬝ᵥ g := by
  simp only [dotProduct]
  exact Fintype.sum_equiv (e3 h).symm _ _ (fun _ => rfl)

theorem t3_dot (x y z x' y' z' : Vh h) :
    t3 x y z ⬝ᵥ t3 x' y' z' = (x ⬝ᵥ x') * ((y ⬝ᵥ y') * (z ⬝ᵥ z')) := by
  unfold t3
  rw [dot_reindex, tp_dotProduct, tp_dotProduct]

lemma t3_add0 (x x' y z : Vh h) : t3 (x + x') y z = t3 x y z + t3 x' y z := by
  funext i; simp [t3, tp, add_mul]
lemma t3_add1 (x y y' z : Vh h) : t3 x (y + y') z = t3 x y z + t3 x y' z := by
  funext i; simp [t3, tp, add_mul, mul_add]
lemma t3_add2 (x y z z' : Vh h) : t3 x y (z + z') = t3 x y z + t3 x y z' := by
  funext i; simp [t3, tp, mul_add]
lemma t3_smul0 (c : ZMod 2) (x y z : Vh h) : t3 (c • x) y z = c • t3 x y z := by
  funext i; simp [t3, tp, mul_assoc]
lemma t3_smul1 (c : ZMod 2) (x y z : Vh h) : t3 x (c • y) z = c • t3 x y z := by
  funext i; simp [t3, tp]; ring
lemma t3_smul2 (c : ZMod 2) (x y z : Vh h) : t3 x y (c • z) = c • t3 x y z := by
  funext i; simp [t3, tp]; ring
lemma t3_zero0 (y z : Vh h) : t3 0 y z = 0 := by funext i; simp [t3, tp]
lemma t3_zero1 (x z : Vh h) : t3 x 0 z = 0 := by funext i; simp [t3, tp]
lemma t3_zero2 (x y : Vh h) : t3 x y 0 = 0 := by funext i; simp [t3, tp]

/-- `U₀ ⊗ U₁ ⊗ U₂ ⊂ F^{⊗3}`. -/
def T3 (U0 U1 U2 : Submodule (ZMod 2) (Vh h)) : Submodule (ZMod 2) (Vc h) :=
  Submodule.span (ZMod 2) {v | ∃ x ∈ U0, ∃ y ∈ U1, ∃ z ∈ U2, v = t3 x y z}

variable {U0 U1 U2 U0' U1' U2' : Submodule (ZMod 2) (Vh h)}

lemma mem_T3 {x y z : Vh h} (hx : x ∈ U0) (hy : y ∈ U1) (hz : z ∈ U2) :
    t3 x y z ∈ T3 U0 U1 U2 :=
  Submodule.subset_span ⟨x, hx, y, hy, z, hz, rfl⟩

lemma T3_mono (h0 : U0 ≤ U0') (h1 : U1 ≤ U1') (h2 : U2 ≤ U2') : T3 U0 U1 U2 ≤ T3 U0' U1' U2' :=
  Submodule.span_mono fun _ ⟨x, hx, y, hy, z, hz, e⟩ => ⟨x, h0 hx, y, h1 hy, z, h2 hz, e⟩

lemma T3_bot0 : T3 ⊥ U1 U2 = (⊥ : Submodule (ZMod 2) (Vc h)) := by
  rw [eq_bot_iff, T3, Submodule.span_le]
  rintro _ ⟨x, hx, y, -, z, -, rfl⟩
  rw [(Submodule.mem_bot _).1 hx, t3_zero0]; exact Submodule.zero_mem _
lemma T3_bot1 : T3 U0 ⊥ U2 = (⊥ : Submodule (ZMod 2) (Vc h)) := by
  rw [eq_bot_iff, T3, Submodule.span_le]
  rintro _ ⟨x, -, y, hy, z, -, rfl⟩
  rw [(Submodule.mem_bot _).1 hy, t3_zero1]; exact Submodule.zero_mem _
lemma T3_bot2 : T3 U0 U1 ⊥ = (⊥ : Submodule (ZMod 2) (Vc h)) := by
  rw [eq_bot_iff, T3, Submodule.span_le]
  rintro _ ⟨x, -, y, -, z, hz, rfl⟩
  rw [(Submodule.mem_bot _).1 hz, t3_zero2]; exact Submodule.zero_mem _

lemma T3_sup0 (A B : Submodule (ZMod 2) (Vh h)) :
    T3 (A ⊔ B) U1 U2 ≤ T3 A U1 U2 ⊔ T3 B U1 U2 := by
  rw [T3, Submodule.span_le]
  rintro _ ⟨x, hx, y, hy, z, hz, rfl⟩
  obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.mem_sup.1 hx
  rw [SetLike.mem_coe, t3_add0]
  exact Submodule.add_mem_sup (mem_T3 ha hy hz) (mem_T3 hb hy hz)
lemma T3_sup1 (A B : Submodule (ZMod 2) (Vh h)) :
    T3 U0 (A ⊔ B) U2 ≤ T3 U0 A U2 ⊔ T3 U0 B U2 := by
  rw [T3, Submodule.span_le]
  rintro _ ⟨x, hx, y, hy, z, hz, rfl⟩
  obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.mem_sup.1 hy
  rw [SetLike.mem_coe, t3_add1]
  exact Submodule.add_mem_sup (mem_T3 hx ha hz) (mem_T3 hx hb hz)
lemma T3_sup2 (A B : Submodule (ZMod 2) (Vh h)) :
    T3 U0 U1 (A ⊔ B) ≤ T3 U0 U1 A ⊔ T3 U0 U1 B := by
  rw [T3, Submodule.span_le]
  rintro _ ⟨x, hx, y, hy, z, hz, rfl⟩
  obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.mem_sup.1 hz
  rw [SetLike.mem_coe, t3_add2]
  exact Submodule.add_mem_sup (mem_T3 hx hy ha) (mem_T3 hx hy hb)

end Tensor

/-! ## 2. Orthogonality -/

section Orth

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

/-- `w` is orthogonal to `U`. -/
def Orth (U : Submodule (ZMod 2) (ι → ZMod 2)) (w : ι → ZMod 2) : Prop := ∀ z ∈ U, z ⬝ᵥ w = 0

/-- `U ⊥ U'`. -/
def OrthS (U U' : Submodule (ZMod 2) (ι → ZMod 2)) : Prop := ∀ a ∈ U, ∀ b ∈ U', a ⬝ᵥ b = 0

lemma orth_bot (w : ι → ZMod 2) : Orth ⊥ w := fun z hz => by
  rw [(Submodule.mem_bot _).1 hz, zero_dotProduct]

lemma orth_sup {U U' : Submodule (ZMod 2) (ι → ZMod 2)} {w : ι → ZMod 2} (h : Orth U w)
    (h' : Orth U' w) : Orth (U ⊔ U') w := fun z hz => by
  obtain ⟨a, ha, b, hb, rfl⟩ := Submodule.mem_sup.1 hz
  rw [add_dotProduct, h a ha, h' b hb, add_zero]

lemma orth_span {S : Set (ι → ZMod 2)} {w : ι → ZMod 2} (h : ∀ z ∈ S, z ⬝ᵥ w = 0) :
    Orth (Submodule.span (ZMod 2) S) w := by
  intro z hz
  induction hz using Submodule.span_induction with
  | mem z hz => exact h z hz
  | zero => exact zero_dotProduct _
  | add a b _ _ ha hb => rw [add_dotProduct, ha, hb, add_zero]
  | smul c a _ ha => rw [smul_dotProduct, ha, smul_zero]

lemma orthS_span {S S' : Set (ι → ZMod 2)} (h : ∀ a ∈ S, ∀ b ∈ S', a ⬝ᵥ b = 0) :
    OrthS (Submodule.span (ZMod 2) S) (Submodule.span (ZMod 2) S') := by
  intro a ha b hb
  have h1 : ∀ a ∈ S, Orth (Submodule.span (ZMod 2) S') a := fun a ha =>
    orth_span fun b hb => by rw [dotProduct_comm]; exact h a ha b hb
  exact orth_span (fun z hz => by rw [dotProduct_comm]; exact h1 z hz b hb) a ha

lemma orthS_sup_left {U U' W : Submodule (ZMod 2) (ι → ZMod 2)} (h : OrthS U W) (h' : OrthS U' W) :
    OrthS (U ⊔ U') W := fun a ha b hb => by
  obtain ⟨x, hx, y, hy, rfl⟩ := Submodule.mem_sup.1 ha
  rw [add_dotProduct, h x hx b hb, h' y hy b hb, add_zero]

lemma orthS_bot_left (W : Submodule (ZMod 2) (ι → ZMod 2)) : OrthS ⊥ W := fun a ha b _ => by
  rw [(Submodule.mem_bot _).1 ha, zero_dotProduct]

end Orth

section OrthT3

variable {h : ℕ} {U0 U1 U2 U0' U1' U2' : Submodule (ZMod 2) (Vh h)}

lemma orth_T3_0 {x : Vh h} (y z : Vh h) (hx : Orth U0 x) : Orth (T3 U0 U1 U2) (t3 x y z) :=
  orth_span fun _ ⟨a, ha, b, _, c, _, e⟩ => by rw [e, t3_dot, hx a ha, zero_mul]
lemma orth_T3_1 (x : Vh h) {y : Vh h} (z : Vh h) (hy : Orth U1 y) :
    Orth (T3 U0 U1 U2) (t3 x y z) :=
  orth_span fun _ ⟨a, _, b, hb, c, _, e⟩ => by rw [e, t3_dot, hy b hb, zero_mul, mul_zero]
lemma orth_T3_2 (x y : Vh h) {z : Vh h} (hz : Orth U2 z) : Orth (T3 U0 U1 U2) (t3 x y z) :=
  orth_span fun _ ⟨a, _, b, _, c, hc, e⟩ => by rw [e, t3_dot, hz c hc, mul_zero, mul_zero]

lemma orthS_T3_0 (h0 : OrthS U0 U0') : OrthS (T3 U0 U1 U2) (T3 U0' U1' U2') :=
  orthS_span fun _ ⟨a, ha, b, _, c, _, e⟩ _ ⟨a', ha', b', _, c', _, e'⟩ => by
    rw [e, e', t3_dot, h0 a ha a' ha', zero_mul]
lemma orthS_T3_1 (h1 : OrthS U1 U1') : OrthS (T3 U0 U1 U2) (T3 U0' U1' U2') :=
  orthS_span fun _ ⟨a, _, b, hb, c, _, e⟩ _ ⟨a', _, b', hb', c', _, e'⟩ => by
    rw [e, e', t3_dot, h1 b hb b' hb', zero_mul, mul_zero]

end OrthT3

/-! ## 3. Orthonormal spanning sets -/

section ON

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

/-- `U` is spanned by an orthonormal finite set. -/
def HasON (U : Submodule (ZMod 2) (ι → ZMod 2)) : Prop :=
  ∃ B : Finset (ι → ZMod 2), Orthonormal2 B ∧ Submodule.span (ZMod 2) ↑B = U

lemma ON_dot {B : Finset (ι → ZMod 2)} (hB : Orthonormal2 B) {b c : ι → ZMod 2} (hb : b ∈ B)
    (hc : c ∈ B) : b ⬝ᵥ c = if b = c then 1 else 0 := by
  split_ifs with e
  · subst e; exact hB.1 b hb
  · exact hB.2 b hb c hc e

/-- A subspace with an orthonormal spanning set is nondegenerate. -/
theorem HasON.nondeg {U : Submodule (ZMod 2) (ι → ZMod 2)} (hU : HasON U) : Nondeg U := by
  obtain ⟨B, hB, rfl⟩ := hU
  intro x hx hxy
  obtain ⟨f, -, hf⟩ := Submodule.mem_span_finset.1 hx
  have hc : ∀ b ∈ B, f b = 0 := by
    intro b hb
    have := hxy b (Submodule.subset_span hb)
    rw [← hf, sum_dotProduct] at this
    rw [Finset.sum_eq_single b] at this
    · rwa [smul_dotProduct, hB.1 b hb, smul_eq_mul, mul_one] at this
    · intro c hc hcb
      rw [smul_dotProduct, hB.2 c hc b hb hcb, smul_zero]
    · intro h; exact absurd hb h
  rw [← hf]
  exact Finset.sum_eq_zero fun b hb => by rw [hc b hb, zero_smul]

lemma HasON.nondegOn {U : Submodule (ZMod 2) (ι → ZMod 2)} (hU : HasON U) :
    NondegOn (1 : Matrix ι ι (ZMod 2)) U :=
  (NetComplexLabels.nondegOn_one_iff U).2 hU.nondeg

/-- The dimension of the span of an orthonormal set is its cardinality. -/
theorem finrank_ON {B : Finset (ι → ZMod 2)} (hB : Orthonormal2 B) :
    finrank (ZMod 2) (Submodule.span (ZMod 2) (↑B : Set (ι → ZMod 2))) = B.card := by
  rw [finrank_span_set_eq_card (orthonormal_linearIndependent hB)]
  simp

lemma HasON_bot : HasON (⊥ : Submodule (ZMod 2) (ι → ZMod 2)) :=
  ⟨∅, ⟨by simp, by simp⟩, by simp⟩

lemma ON_union {B B' : Finset (ι → ZMod 2)} (hB : Orthonormal2 B) (hB' : Orthonormal2 B')
    (hO : ∀ b ∈ B, ∀ c ∈ B', b ⬝ᵥ c = 0) : Orthonormal2 (B ∪ B') := by
  refine ⟨fun b hb => ?_, fun b hb c hc hbc => ?_⟩
  · rcases Finset.mem_union.1 hb with hb | hb
    · exact hB.1 b hb
    · exact hB'.1 b hb
  · rcases Finset.mem_union.1 hb with hb | hb <;> rcases Finset.mem_union.1 hc with hc | hc
    · exact hB.2 b hb c hc hbc
    · exact hO b hb c hc
    · rw [dotProduct_comm]; exact hO c hc b hb
    · exact hB'.2 b hb c hc hbc

lemma HasON_sup {U U' : Submodule (ZMod 2) (ι → ZMod 2)} (hU : HasON U) (hU' : HasON U')
    (hO : OrthS U U') : HasON (U ⊔ U') := by
  obtain ⟨B, hB, rfl⟩ := hU
  obtain ⟨B', hB', rfl⟩ := hU'
  refine ⟨B ∪ B', ON_union hB hB' fun b hb c hc =>
    hO b (Submodule.subset_span hb) c (Submodule.subset_span hc), ?_⟩
  rw [Finset.coe_union, Submodule.span_union]

/-- Dimension of an orthogonal sum. -/
theorem finrank_sup_orth {U U' : Submodule (ZMod 2) (ι → ZMod 2)} (hU' : Nondeg U')
    (hO : OrthS U U') : finrank (ZMod 2) ↥(U ⊔ U') = finrank (ZMod 2) U + finrank (ZMod 2) U' := by
  have hinf : U ⊓ U' = ⊥ := by
    rw [eq_bot_iff]
    intro x hx
    rw [Submodule.mem_bot]
    exact hU' x hx.2 fun y hy => hO x hx.1 y hy
  have := Submodule.finrank_sup_add_finrank_inf_eq U U'
  rw [hinf, finrank_bot, add_zero] at this
  exact this

end ON

/-! ## 4. Tensor products of orthonormal sets -/

section ONT3

variable {h : ℕ}

/-- The tensor products of three finite sets. -/
noncomputable def img3 (B0 B1 B2 : Finset (Vh h)) : Finset (Vc h) :=
  (B0 ×ˢ B1 ×ˢ B2).image fun p => t3 p.1 p.2.1 p.2.2

variable {B0 B1 B2 : Finset (Vh h)}

lemma t3_dot_ON (h0 : Orthonormal2 B0) (h1 : Orthonormal2 B1) (h2 : Orthonormal2 B2)
    {p q : Vh h × Vh h × Vh h} (hp : p ∈ B0 ×ˢ B1 ×ˢ B2) (hq : q ∈ B0 ×ˢ B1 ×ˢ B2) :
    t3 p.1 p.2.1 p.2.2 ⬝ᵥ t3 q.1 q.2.1 q.2.2 = if p = q then 1 else 0 := by
  simp only [Finset.mem_product] at hp hq
  rw [t3_dot, ON_dot h0 hp.1 hq.1, ON_dot h1 hp.2.1 hq.2.1, ON_dot h2 hp.2.2 hq.2.2]
  obtain ⟨a, b, c⟩ := p
  obtain ⟨a', b', c'⟩ := q
  simp only [Prod.mk.injEq]
  by_cases e1 : a = a' <;> by_cases e2 : b = b' <;> by_cases e3 : c = c' <;> simp [e1, e2, e3]

theorem ON_T3 (h0 : Orthonormal2 B0) (h1 : Orthonormal2 B1) (h2 : Orthonormal2 B2) :
    Orthonormal2 (img3 B0 B1 B2) ∧
      Submodule.span (ZMod 2) (↑(img3 B0 B1 B2) : Set (Vc h)) =
        T3 (Submodule.span (ZMod 2) ↑B0) (Submodule.span (ZMod 2) ↑B1)
          (Submodule.span (ZMod 2) ↑B2) ∧
      (img3 B0 B1 B2).card = B0.card * (B1.card * B2.card) := by
  have hd := fun {p q : Vh h × Vh h × Vh h} (hp : p ∈ B0 ×ˢ B1 ×ˢ B2)
    (hq : q ∈ B0 ×ˢ B1 ×ˢ B2) => t3_dot_ON h0 h1 h2 hp hq
  have hinj : Set.InjOn (fun p : Vh h × Vh h × Vh h => t3 p.1 p.2.1 p.2.2) ↑(B0 ×ˢ B1 ×ˢ B2) := by
    intro p hp q hq e
    by_contra hne
    have := hd hp hq
    simp only at e
    rw [if_neg hne, ← e, hd hp hp, if_pos rfl] at this
    exact one_ne_zero this
  refine ⟨⟨?_, ?_⟩, ?_, ?_⟩
  · intro b hb
    obtain ⟨p, hp, rfl⟩ := Finset.mem_image.1 hb
    rw [hd hp hp, if_pos rfl]
  · intro b hb c hc hbc
    obtain ⟨p, hp, rfl⟩ := Finset.mem_image.1 hb
    obtain ⟨q, hq, rfl⟩ := Finset.mem_image.1 hc
    rw [hd hp hq, if_neg (fun e => hbc (by rw [e]))]
  · apply le_antisymm
    · rw [Submodule.span_le]
      intro b hb
      obtain ⟨p, hp, rfl⟩ := Finset.mem_image.1 hb
      simp only [Finset.mem_product] at hp
      exact mem_T3 (Submodule.subset_span hp.1) (Submodule.subset_span hp.2.1)
        (Submodule.subset_span hp.2.2)
    · rw [T3, Submodule.span_le]
      rintro _ ⟨x, hx, y, hy, z, hz, rfl⟩
      set S := Submodule.span (ZMod 2) (↑(img3 B0 B1 B2) : Set (Vc h))
      have k2 : ∀ x ∈ B0, ∀ y ∈ B1, ∀ z ∈ Submodule.span (ZMod 2) (↑B2 : Set (Vh h)),
          t3 x y z ∈ S := by
        intro x hx y hy z hz
        induction hz using Submodule.span_induction with
        | mem z hz => exact Submodule.subset_span (Finset.mem_image.2
            ⟨(x, y, z), Finset.mem_product.2 ⟨hx, Finset.mem_product.2 ⟨hy, hz⟩⟩, rfl⟩)
        | zero => rw [t3_zero2]; exact S.zero_mem
        | add a b _ _ ha hb => rw [t3_add2]; exact S.add_mem ha hb
        | smul c a _ ha => rw [t3_smul2]; exact S.smul_mem c ha
      have k1 : ∀ x ∈ B0, ∀ y ∈ Submodule.span (ZMod 2) (↑B1 : Set (Vh h)),
          ∀ z ∈ Submodule.span (ZMod 2) (↑B2 : Set (Vh h)), t3 x y z ∈ S := by
        intro x hx y hy
        induction hy using Submodule.span_induction with
        | mem y hy => exact k2 x hx y hy
        | zero => intro z _; rw [t3_zero1]; exact S.zero_mem
        | add a b _ _ ha hb => intro z hz; rw [t3_add1]; exact S.add_mem (ha z hz) (hb z hz)
        | smul c a _ ha => intro z hz; rw [t3_smul1]; exact S.smul_mem c (ha z hz)
      have k0 : ∀ x ∈ Submodule.span (ZMod 2) (↑B0 : Set (Vh h)),
          ∀ y ∈ Submodule.span (ZMod 2) (↑B1 : Set (Vh h)),
          ∀ z ∈ Submodule.span (ZMod 2) (↑B2 : Set (Vh h)), t3 x y z ∈ S := by
        intro x hx
        induction hx using Submodule.span_induction with
        | mem x hx => exact k1 x hx
        | zero => intro y _ z _; rw [t3_zero0]; exact S.zero_mem
        | add a b _ _ ha hb =>
          intro y hy z hz; rw [t3_add0]; exact S.add_mem (ha y hy z hz) (hb y hy z hz)
        | smul c a _ ha => intro y hy z hz; rw [t3_smul0]; exact S.smul_mem c (ha y hy z hz)
      exact k0 x hx y hy z hz
  · rw [img3, Finset.card_image_of_injOn hinj, Finset.card_product, Finset.card_product]

lemma HasON_T3 {U0 U1 U2 : Submodule (ZMod 2) (Vh h)} (h0 : HasON U0) (h1 : HasON U1)
    (h2 : HasON U2) : HasON (T3 U0 U1 U2) := by
  obtain ⟨B0, hB0, rfl⟩ := h0
  obtain ⟨B1, hB1, rfl⟩ := h1
  obtain ⟨B2, hB2, rfl⟩ := h2
  obtain ⟨hO, hs, -⟩ := ON_T3 hB0 hB1 hB2
  exact ⟨_, hO, hs⟩

end ONT3

end NetComplexP8

end

section
-- Source module: Solutions.NetComplexP8Labels
/-!
# Prop. 8, part 3: the table-(6) labels of the complex network over `𝔽₂` and Lemma 6

Slot space `F = 𝔽₂^h` (dot product); `t_S` the indicator of a triple, `⟨S⟩ = ⟨t_S⟩`,
`S^⊥ = t_S^⊥`, `e_k` the coordinate units. At stage `j` (0-indexed) of the bank with fixed
triples `S₁, S₂` (the coordinates other than `j`, in order):

* `bet j S₁ S₂ Ψ = B ⊗_j Ψ ⊗ Q`: `0` (j = 0), `S₁^⊥ ⊗ Ψ ⊗ ⟨S₂⟩` (j = 1),
  `S₁^⊥ ⊗ F ⊗ Ψ ⊔ ⟨S₁⟩ ⊗ S₂^⊥ ⊗ Ψ` (j = 2; here `B = (t_{S₁} ⊗ t_{S₂})^⊥ ⊂ F ⊗ F`);
* `piS j S₁ S₂ Ψ = P ⊗_j Ψ ⊗ Q`;
* `lab j S₁ S₂ Ψ₁ Ψ₂ = (B ⊗ Ψ₁ ⊥ P ⊗ Ψ₂) ⊗ Q`.

The gate labels of table (6) are `lab` with `(Ψ₁, Ψ₂)` = `(⟨t⟩, 0)`, `(F, 0)`, `(F, ⟨t⟩)`,
`(F, F)`, `(F, 0)`, `(F, t^⊥)`, `(F, F)`, `(F, F)` at times `0, …, 7`.

For every edge type we prove `IncW U V`: `U ≤ V`, and either `U = V` or the residual
`V ∩ U^⊥` contains an explicit norm-one vector (a pure tensor of coordinate units and triple
indicators — the paper's "coordinate units outside small supports"); every label has an
orthonormal spanning set (`HasON`), hence is nondegenerate; and the dimension facts needed for
the count (`finrank_lab_center`: the central loss is exactly `h`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetComplexP8

open Matrix Finset Module NetLabels NetComplexOrtho

variable {h : ℕ}

/-! ## 1. One slot -/

section Slot

/-- The triple indicator `t_S`. -/
def tt (S : Finset (Fin h)) : Vh h := NetLabels.ind (ZMod 2) S
/-- The triple line `⟨t_S⟩`. -/
def L1 (S : Finset (Fin h)) : Submodule (ZMod 2) (Vh h) := Submodule.span (ZMod 2) {tt S}
/-- The triple complement `t_S^⊥`. -/
def Pp (S : Finset (Fin h)) : Submodule (ZMod 2) (Vh h) := perp (tt S)
/-- The coordinate unit `e_k`. -/
def ek (k : Fin h) : Vh h := Pi.single k 1

lemma dot_ek_ek (k : Fin h) : ek k ⬝ᵥ ek k = 1 := by simp [ek]

lemma dot_ek_ek_ne {k l : Fin h} (hkl : k ≠ l) : ek k ⬝ᵥ ek l = 0 := by
  simp [ek, Pi.single_apply, hkl.symm]

lemma dot_ek_tt {k : Fin h} {S : Finset (Fin h)} (hk : k ∉ S) : ek k ⬝ᵥ tt S = 0 := by
  simp [ek, tt, NetLabels.ind, hk]

lemma dot_tt_ek {k : Fin h} {S : Finset (Fin h)} (hk : k ∉ S) : tt S ⬝ᵥ ek k = 0 := by
  rw [dotProduct_comm]; exact dot_ek_tt hk

lemma tt_norm {S : Finset (Fin h)} (hS : S.card = 3) : tt S ⬝ᵥ tt S = 1 :=
  NetComplexLabels.dot_triple_self S hS

lemma tt_mem_L1 (S : Finset (Fin h)) : tt S ∈ L1 S := Submodule.mem_span_singleton_self _

lemma orth_L1 {S : Finset (Fin h)} {y : Vh h} (hy : tt S ⬝ᵥ y = 0) : Orth (L1 S) y := by
  intro z hz
  obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
  rw [smul_dotProduct, hy, smul_zero]

lemma orth_Pp (S : Finset (Fin h)) : Orth (Pp S) (tt S) := fun z hz => by
  rw [dotProduct_comm]; exact mem_perp.1 hz

lemma ek_mem_Pp {k : Fin h} {S : Finset (Fin h)} (hk : k ∉ S) : ek k ∈ Pp S :=
  mem_perp.2 (dot_tt_ek hk)

lemma L1_le_Pp {S T : Finset (Fin h)} (hST : tt S ⬝ᵥ tt T = 0) : L1 T ≤ Pp S :=
  (Submodule.span_singleton_le_iff_mem _ _).2 (mem_perp.2 hST)

lemma orthS_Pp_L1 (S : Finset (Fin h)) : OrthS (Pp S) (L1 S) := fun a ha b hb => by
  obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hb
  rw [dotProduct_smul, dotProduct_comm, mem_perp.1 ha, smul_zero]

/-- `F = t^⊥ ⊔ ⟨t⟩`. -/
lemma top_split {S : Finset (Fin h)} (hS : S.card = 3) :
    (⊤ : Submodule (ZMod 2) (Vh h)) = Pp S ⊔ L1 S := by
  have := split (⊤ : Submodule (ZMod 2) (Vh h)) Submodule.mem_top (tt_norm hS)
  rw [top_inf_eq, sup_comm] at this
  exact this

lemma ek_inj : Function.Injective (ek : Fin h → Vh h) := by
  intro k l e
  by_contra hkl
  have := congrFun e k
  simp [ek, Pi.single_apply, hkl] at this

/-- The coordinate units. -/
noncomputable def Btop (h : ℕ) : Finset (Vh h) := univ.image ek

lemma ON_top : Orthonormal2 (Btop h) ∧ Submodule.span (ZMod 2) (↑(Btop h) : Set (Vh h)) = ⊤ ∧
    (Btop h).card = h := by
  refine ⟨⟨fun b hb => ?_, fun b hb c hc hbc => ?_⟩, ?_, ?_⟩
  · obtain ⟨k, -, rfl⟩ := Finset.mem_image.1 hb; exact dot_ek_ek k
  · obtain ⟨k, -, rfl⟩ := Finset.mem_image.1 hb
    obtain ⟨l, -, rfl⟩ := Finset.mem_image.1 hc
    exact dot_ek_ek_ne fun e => hbc (e ▸ rfl)
  · rw [eq_top_iff]
    intro x _
    have hx : x = ∑ k, x k • ek k := by
      funext i; simp [ek, Finset.sum_apply, Pi.single_apply]
    rw [hx]
    exact Submodule.sum_mem _ fun k _ => Submodule.smul_mem _ _
      (Submodule.subset_span (Finset.mem_image_of_mem _ (Finset.mem_univ k)))
  · rw [Btop, Finset.card_image_of_injective _ ek_inj, Finset.card_univ, Fintype.card_fin]

lemma ON_L1 {S : Finset (Fin h)} (hS : S.card = 3) :
    Orthonormal2 ({tt S} : Finset (Vh h)) ∧
      Submodule.span (ZMod 2) (↑({tt S} : Finset (Vh h)) : Set (Vh h)) = L1 S := by
  refine ⟨⟨fun b hb => ?_, fun b hb c hc hbc => ?_⟩, by simp [L1]⟩
  · rw [Finset.mem_singleton.1 hb]; exact tt_norm hS
  · rw [Finset.mem_singleton.1 hb, Finset.mem_singleton.1 hc] at hbc; exact absurd rfl hbc

lemma HasON_top : HasON (⊤ : Submodule (ZMod 2) (Vh h)) := ⟨Btop h, ON_top.1, ON_top.2.1⟩

lemma HasON_L1 {S : Finset (Fin h)} (hS : S.card = 3) : HasON (L1 S) :=
  ⟨_, (ON_L1 hS).1, (ON_L1 hS).2⟩

lemma nondeg_Pp {S : Finset (Fin h)} (hS : S.card = 3) : Nondeg (Pp S) := by
  have := nondeg_perp (⊤ : Submodule (ZMod 2) (Vh h)) HasON_top.nondeg Submodule.mem_top
    (tt_norm hS)
  rwa [top_inf_eq] at this

/-- `t^⊥` has an orthonormal basis (it contains a coordinate unit outside the triple). -/
lemma HasON_Pp {S : Finset (Fin h)} (hS : S.card = 3) {k : Fin h} (hk : k ∉ S) :
    HasON (Pp S) := by
  obtain ⟨B, -, hON, hsp⟩ := exists_orthonormal_basis _ (Pp S) rfl (nondeg_Pp hS)
    (Or.inr ⟨ek k, ek_mem_Pp hk, dot_ek_ek k⟩)
  exact ⟨B, hON, hsp⟩

lemma exists_out (S : Finset (Fin h)) (hS : S.card < h) : ∃ k, k ∉ S := by
  by_contra hc
  push Not at hc
  have : S = univ := Finset.eq_univ_of_forall hc
  rw [this, Finset.card_univ, Fintype.card_fin] at hS
  omega

/-- `T3 ⊤ ⊤ ⊤ = ⊤`. -/
lemma T3_top : T3 (⊤ : Submodule (ZMod 2) (Vh h)) ⊤ ⊤ = ⊤ := by
  obtain ⟨hO, hs, hc⟩ := ON_top (h := h)
  obtain ⟨hO3, hs3, hc3⟩ := ON_T3 hO hO hO
  rw [hs] at hs3
  rw [← hs3]
  apply Submodule.eq_top_of_finrank_eq
  rw [finrank_ON hO3, hc3, hc, finrank_fin_fun]
  ring

/-- `⟨a⟩ ⊗ ⟨b⟩ ⊗ ⟨c⟩ = ⟨a ⊗ b ⊗ c⟩`. -/
lemma T3_L1 {S1 S2 S3 : Finset (Fin h)} (h1 : S1.card = 3) (h2 : S2.card = 3) (h3 : S3.card = 3) :
    T3 (L1 S1) (L1 S2) (L1 S3) = Submodule.span (ZMod 2) {t3 (tt S1) (tt S2) (tt S3)} := by
  obtain ⟨o1, s1⟩ := ON_L1 h1
  obtain ⟨o2, s2⟩ := ON_L1 h2
  obtain ⟨o3, s3⟩ := ON_L1 h3
  obtain ⟨-, hs, -⟩ := ON_T3 o1 o2 o3
  rw [s1, s2, s3] at hs
  rw [← hs]
  simp [img3]

end Slot

/-! ## 2. The labels of a stage -/

section Labels

/-- `B ⊗_j Ψ ⊗ Q`. -/
def bet (j : Fin 3) (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    Submodule (ZMod 2) (Vc h) :=
  if j = 0 then ⊥ else if j = 1 then T3 (Pp S1) Ψ (L1 S2)
  else T3 (Pp S1) ⊤ Ψ ⊔ T3 (L1 S1) (Pp S2) Ψ

/-- `P ⊗_j Ψ ⊗ Q`. -/
def piS (j : Fin 3) (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    Submodule (ZMod 2) (Vc h) :=
  if j = 0 then T3 Ψ (L1 S1) (L1 S2) else if j = 1 then T3 (L1 S1) Ψ (L1 S2)
  else T3 (L1 S1) (L1 S2) Ψ

/-- The label `(B ⊗ Ψ₁ ⊥ P ⊗ Ψ₂) ⊗ Q` of stage `j`. -/
def lab (j : Fin 3) (S1 S2 : Finset (Fin h)) (Ψ1 Ψ2 : Submodule (ZMod 2) (Vh h)) :
    Submodule (ZMod 2) (Vc h) :=
  bet j S1 S2 Ψ1 ⊔ piS j S1 S2 Ψ2

/-- Inclusion with an explicit norm-one residual vector (or equality). -/
def IncW {ι : Type*} [Fintype ι] (U V : Submodule (ZMod 2) (ι → ZMod 2)) : Prop :=
  U ≤ V ∧ (U = V ∨ ∃ w ∈ V, w ⬝ᵥ w = 1 ∧ Orth U w)

lemma incW_refl {ι : Type*} [Fintype ι] (U : Submodule (ZMod 2) (ι → ZMod 2)) : IncW U U :=
  ⟨le_rfl, Or.inl rfl⟩

lemma incW_of_eq {ι : Type*} [Fintype ι] {U V : Submodule (ZMod 2) (ι → ZMod 2)} (e : U = V) :
    IncW U V := e ▸ incW_refl U

variable {S1 S2 : Finset (Fin h)} {Ψ1 Ψ2 Ψ1' Ψ2' : Submodule (ZMod 2) (Vh h)}

lemma bet0 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) : bet 0 S1 S2 Ψ = ⊥ := rfl
lemma bet1 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    bet 1 S1 S2 Ψ = T3 (Pp S1) Ψ (L1 S2) := rfl
lemma bet2 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    bet 2 S1 S2 Ψ = T3 (Pp S1) ⊤ Ψ ⊔ T3 (L1 S1) (Pp S2) Ψ := rfl
lemma piS0 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    piS 0 S1 S2 Ψ = T3 Ψ (L1 S1) (L1 S2) := rfl
lemma piS1 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    piS 1 S1 S2 Ψ = T3 (L1 S1) Ψ (L1 S2) := rfl
lemma piS2 (S1 S2 : Finset (Fin h)) (Ψ : Submodule (ZMod 2) (Vh h)) :
    piS 2 S1 S2 Ψ = T3 (L1 S1) (L1 S2) Ψ := rfl

lemma fin3_cases (j : Fin 3) : j = 0 ∨ j = 1 ∨ j = 2 := by fin_cases j <;> simp

lemma piS_bot (j : Fin 3) : piS j S1 S2 ⊥ = ⊥ := by
  rcases fin3_cases j with rfl | rfl | rfl
  · rw [piS0, T3_bot0]
  · rw [piS1, T3_bot1]
  · rw [piS2, T3_bot2]

lemma bet_bot (j : Fin 3) : bet j S1 S2 ⊥ = ⊥ := by
  rcases fin3_cases j with rfl | rfl | rfl
  · rfl
  · rw [bet1, T3_bot1]
  · rw [bet2, T3_bot2, T3_bot2, sup_bot_eq]

lemma lab_bot (j : Fin 3) : lab j S1 S2 ⊥ ⊥ = ⊥ := by
  rw [lab, bet_bot, piS_bot, sup_bot_eq]

lemma lab_mono (j : Fin 3) (h1 : Ψ1 ≤ Ψ1') (h2 : Ψ2 ≤ Ψ2') :
    lab j S1 S2 Ψ1 Ψ2 ≤ lab j S1 S2 Ψ1' Ψ2' := by
  unfold lab
  apply sup_le_sup
  · rcases fin3_cases j with rfl | rfl | rfl
    · rw [bet0, bet0]
    · rw [bet1, bet1]; exact T3_mono le_rfl h1 le_rfl
    · rw [bet2, bet2]
      exact sup_le_sup (T3_mono le_rfl le_rfl h1) (T3_mono le_rfl le_rfl h1)
  · rcases fin3_cases j with rfl | rfl | rfl
    · rw [piS0, piS0]; exact T3_mono h2 le_rfl le_rfl
    · rw [piS1, piS1]; exact T3_mono le_rfl h2 le_rfl
    · rw [piS2, piS2]; exact T3_mono le_rfl le_rfl h2

/-! ### The residual vectors -/

/-- `p ⊗_j y ⊗ q`. -/
def piV (j : Fin 3) (S1 S2 : Finset (Fin h)) (y : Vh h) : Vc h :=
  if j = 0 then t3 y (tt S1) (tt S2) else if j = 1 then t3 (tt S1) y (tt S2)
  else t3 (tt S1) (tt S2) y

/-- `b ⊗_j y ⊗ q` with `b` a coordinate unit in `B`. -/
def beV (j : Fin 3) (S2 : Finset (Fin h)) (k : Fin h) (y : Vh h) : Vc h :=
  if j = 1 then t3 (ek k) y (tt S2) else t3 (ek k) (ek k) y

variable (hS1 : S1.card = 3) (hS2 : S2.card = 3)
include hS1 hS2

lemma piV_mem (j : Fin 3) {y : Vh h} (hy : y ∈ Ψ2) : piV j S1 S2 y ∈ lab j S1 S2 Ψ1 Ψ2 := by
  apply Submodule.mem_sup_right
  rcases fin3_cases j with rfl | rfl | rfl
  · exact mem_T3 hy (tt_mem_L1 _) (tt_mem_L1 _)
  · exact mem_T3 (tt_mem_L1 _) hy (tt_mem_L1 _)
  · exact mem_T3 (tt_mem_L1 _) (tt_mem_L1 _) hy

lemma piV_norm (j : Fin 3) {y : Vh h} (hy : y ⬝ᵥ y = 1) : piV j S1 S2 y ⬝ᵥ piV j S1 S2 y = 1 := by
  rcases fin3_cases j with rfl | rfl | rfl <;>
  simp [piV, t3_dot, tt_norm hS1, tt_norm hS2, hy]

lemma piV_orth (j : Fin 3) {y : Vh h} (hy : Orth Ψ2 y) :
    Orth (lab j S1 S2 Ψ1 Ψ2) (piV j S1 S2 y) := by
  rcases fin3_cases j with rfl | rfl | rfl
  · exact orth_sup (orth_bot _) (orth_T3_0 _ _ hy)
  · exact orth_sup (orth_T3_0 _ _ (orth_Pp S1)) (orth_T3_1 _ _ hy)
  · exact orth_sup (orth_sup (orth_T3_0 _ _ (orth_Pp S1)) (orth_T3_1 _ _ (orth_Pp S2)))
      (orth_T3_2 _ _ hy)

lemma beV_mem (j : Fin 3) (hj : j ≠ 0) {k : Fin h} (hk : k ∉ S1) {y : Vh h} (hy : y ∈ Ψ1) :
    beV j S2 k y ∈ lab j S1 S2 Ψ1 Ψ2 := by
  apply Submodule.mem_sup_left
  rcases fin3_cases j with rfl | rfl | rfl
  · exact absurd rfl hj
  · exact mem_T3 (ek_mem_Pp hk) hy (tt_mem_L1 _)
  · exact Submodule.mem_sup_left (mem_T3 (ek_mem_Pp hk) Submodule.mem_top hy)

lemma beV_norm (j : Fin 3) (k : Fin h) {y : Vh h} (hy : y ⬝ᵥ y = 1) :
    beV j S2 k y ⬝ᵥ beV j S2 k y = 1 := by
  unfold beV
  split_ifs <;> simp [t3_dot, dot_ek_ek, tt_norm hS2, hy]

lemma beV_orth (j : Fin 3) (hj : j ≠ 0) {k : Fin h} (hk : k ∉ S1) {y : Vh h} (hy : Orth Ψ1 y) :
    Orth (lab j S1 S2 Ψ1 Ψ2) (beV j S2 k y) := by
  rcases fin3_cases j with rfl | rfl | rfl
  · exact absurd rfl hj
  · exact orth_sup (orth_T3_1 _ _ hy) (orth_T3_0 _ _ (orth_L1 (dot_tt_ek hk)))
  · exact orth_sup (orth_sup (orth_T3_2 _ _ hy) (orth_T3_2 _ _ hy))
      (orth_T3_0 _ _ (orth_L1 (dot_tt_ek hk)))

/-- Growth of the `P`-component (with `Ψ₁ ≤ Ψ₁'`), witnessed by `p ⊗ y ⊗ q`. -/
theorem inc_pi (j : Fin 3) (h1 : Ψ1 ≤ Ψ1') (h2 : Ψ2 ≤ Ψ2') {y : Vh h} (hy : y ∈ Ψ2')
    (hyy : y ⬝ᵥ y = 1) (ho : Orth Ψ2 y) : IncW (lab j S1 S2 Ψ1 Ψ2) (lab j S1 S2 Ψ1' Ψ2') :=
  ⟨lab_mono j h1 h2, Or.inr ⟨piV j S1 S2 y, piV_mem hS1 hS2 j hy, piV_norm hS1 hS2 j hyy,
    piV_orth hS1 hS2 j ho⟩⟩

/-- Growth of the `B`-component, witnessed by `b ⊗ y ⊗ q` (labels equal at stage 1, `B = 0`). -/
theorem inc_be (j : Fin 3) (h1 : Ψ1 ≤ Ψ1') {y : Vh h} (hy : y ∈ Ψ1') (hyy : y ⬝ᵥ y = 1)
    (ho : Orth Ψ1 y) {k : Fin h} (hk : k ∉ S1) :
    IncW (lab j S1 S2 Ψ1 Ψ2) (lab j S1 S2 Ψ1' Ψ2) := by
  by_cases hj : j = 0
  · subst hj; unfold lab; rw [bet0, bet0]; exact incW_refl _
  · exact ⟨lab_mono j h1 le_rfl, Or.inr ⟨beV j S2 k y, beV_mem hS1 hS2 j hj hk hy,
      beV_norm hS1 hS2 j k hyy, beV_orth hS1 hS2 j hj hk ho⟩⟩

/-- At stage 3, `A ⊗ F = F^{⊗3}`. -/
theorem lab2_top : lab 2 S1 S2 ⊤ ⊤ = ⊤ := by
  rw [eq_top_iff, ← T3_top]
  unfold lab
  rw [bet2, piS2]
  have e1 := T3_sup0 (U1 := ⊤) (U2 := ⊤) (Pp S1) (L1 S1)
  rw [← top_split hS1] at e1
  have e2 := T3_sup1 (U0 := L1 S1) (U2 := ⊤) (Pp S2) (L1 S2)
  rw [← top_split hS2] at e2
  calc T3 ⊤ ⊤ ⊤ ≤ T3 (Pp S1) ⊤ ⊤ ⊔ T3 (L1 S1) ⊤ ⊤ := e1
    _ ≤ T3 (Pp S1) ⊤ ⊤ ⊔ (T3 (L1 S1) (Pp S2) ⊤ ⊔ T3 (L1 S1) (L1 S2) ⊤) := sup_le_sup le_rfl e2
    _ = _ := by rw [sup_assoc]

/-- Last label of a scratch wire to its sink `F`. -/
theorem inc_sink (j : Fin 3) {k l : Fin h} (hk : k ∉ S1) (hl : l ∉ S2) :
    IncW (lab j S1 S2 ⊤ ⊤) ⊤ := by
  rcases fin3_cases j with rfl | rfl | rfl
  · refine ⟨le_top, Or.inr ⟨t3 (ek k) (ek k) (ek k), Submodule.mem_top, by
      simp [t3_dot, dot_ek_ek], ?_⟩⟩
    exact orth_sup (orth_bot _) (orth_T3_1 _ _ (orth_L1 (dot_tt_ek hk)))
  · refine ⟨le_top, Or.inr ⟨t3 (ek l) (ek l) (ek l), Submodule.mem_top, by
      simp [t3_dot, dot_ek_ek], ?_⟩⟩
    exact orth_sup (orth_T3_2 _ _ (orth_L1 (dot_tt_ek hl)))
      (orth_T3_2 _ _ (orth_L1 (dot_tt_ek hl)))
  · exact incW_of_eq (lab2_top hS1 hS2)

/-! ### Orthonormal spanning sets and dimensions -/

lemma orthS_bet_piS (j : Fin 3) : OrthS (bet j S1 S2 Ψ1) (piS j S1 S2 Ψ2) := by
  rcases fin3_cases j with rfl | rfl | rfl
  · exact orthS_bot_left _
  · exact orthS_T3_0 (orthS_Pp_L1 S1)
  · exact orthS_sup_left (orthS_T3_0 (orthS_Pp_L1 S1)) (orthS_T3_1 (orthS_Pp_L1 S2))

lemma HasON_bet (j : Fin 3) {k1 k2 : Fin h} (hk1 : k1 ∉ S1) (hk2 : k2 ∉ S2) (hΨ : HasON Ψ1) :
    HasON (bet j S1 S2 Ψ1) := by
  rcases fin3_cases j with rfl | rfl | rfl
  · exact HasON_bot
  · exact HasON_T3 (HasON_Pp hS1 hk1) hΨ (HasON_L1 hS2)
  · exact HasON_sup (HasON_T3 (HasON_Pp hS1 hk1) HasON_top hΨ)
      (HasON_T3 (HasON_L1 hS1) (HasON_Pp hS2 hk2) hΨ) (orthS_T3_0 (orthS_Pp_L1 S1))

lemma HasON_piS (j : Fin 3) (hΨ : HasON Ψ2) : HasON (piS j S1 S2 Ψ2) := by
  rcases fin3_cases j with rfl | rfl | rfl
  · exact HasON_T3 hΨ (HasON_L1 hS1) (HasON_L1 hS2)
  · exact HasON_T3 (HasON_L1 hS1) hΨ (HasON_L1 hS2)
  · exact HasON_T3 (HasON_L1 hS1) (HasON_L1 hS2) hΨ

/-- **Every table-(6) label is spanned by an orthonormal set** (hence nondegenerate). -/
theorem HasON_lab (j : Fin 3) {k1 k2 : Fin h} (hk1 : k1 ∉ S1) (hk2 : k2 ∉ S2) (hΨ1 : HasON Ψ1)
    (hΨ2 : HasON Ψ2) : HasON (lab j S1 S2 Ψ1 Ψ2) :=
  HasON_sup (HasON_bet hS1 hS2 j hk1 hk2 hΨ1) (HasON_piS hS1 hS2 j hΨ2) (orthS_bet_piS hS1 hS2 j)

lemma finrank_piS_top (j : Fin 3) : finrank (ZMod 2) (piS j S1 S2 ⊤) = h := by
  obtain ⟨ot, st, ct⟩ := ON_top (h := h)
  obtain ⟨o1, s1⟩ := ON_L1 hS1
  obtain ⟨o2, s2⟩ := ON_L1 hS2
  rcases fin3_cases j with rfl | rfl | rfl
  · obtain ⟨hO, hs, hc⟩ := ON_T3 ot o1 o2
    rw [st, s1, s2] at hs
    rw [piS0, ← hs, finrank_ON hO, hc, ct]; simp
  · obtain ⟨hO, hs, hc⟩ := ON_T3 o1 ot o2
    rw [st, s1, s2] at hs
    rw [piS1, ← hs, finrank_ON hO, hc, ct]; simp
  · obtain ⟨hO, hs, hc⟩ := ON_T3 o1 o2 ot
    rw [st, s1, s2] at hs
    rw [piS2, ← hs, finrank_ON hO, hc, ct]; simp

/-- **The central loss**: `dim (A ⊗ F ⊗ Q) = dim (B ⊗ F ⊗ Q) + h`. -/
theorem finrank_lab_center (j : Fin 3) :
    finrank (ZMod 2) (lab j S1 S2 ⊤ ⊤) = finrank (ZMod 2) (lab j S1 S2 ⊤ ⊥) + h := by
  have e : lab j S1 S2 ⊤ ⊥ = bet j S1 S2 ⊤ := by rw [lab, piS_bot, sup_bot_eq]
  rw [e, lab, finrank_sup_orth (HasON_piS hS1 hS2 j HasON_top).nondeg (orthS_bet_piS hS1 hS2 j),
    finrank_piS_top hS1 hS2 j]

end Labels

/-! ## 3. Stage boundaries and terminals -/

section Boundary

variable {S1 S2 S3 : Finset (Fin h)} (hS1 : S1.card = 3) (hS2 : S2.card = 3) (hS3 : S3.card = 3)
include hS1 hS2 hS3

/-- `X`: stage 1 → stage 2 (`A' ⊗ ⟨t⟩ ⊗ Q' ⊂ (B' ⊗ F) ⊥ (P' ⊗ ⟨t⟩)`, residual `B' ⊗ t^⊥ ⊗ Q'`). -/
theorem bX01 {k l : Fin h} (hk : k ∉ S1) (hl : l ∉ S2) :
    IncW (lab 0 S2 S3 ⊤ ⊤) (lab 1 S1 S3 ⊤ (L1 S2)) := by
  unfold lab
  rw [bet0, piS0, bet1, piS1, bot_sup_eq]
  refine ⟨?_, Or.inr ⟨t3 (ek k) (ek l) (tt S3), Submodule.mem_sup_left
    (mem_T3 (ek_mem_Pp hk) Submodule.mem_top (tt_mem_L1 _)), by
      simp [t3_dot, dot_ek_ek, tt_norm hS3], orth_T3_1 _ _ (orth_L1 (dot_tt_ek hl))⟩⟩
  calc T3 ⊤ (L1 S2) (L1 S3) ≤ T3 (Pp S1) (L1 S2) (L1 S3) ⊔ T3 (L1 S1) (L1 S2) (L1 S3) := by
        rw [top_split hS1]; exact T3_sup0 _ _
    _ ≤ _ := sup_le_sup (T3_mono le_rfl le_top le_rfl) le_rfl

/-- `X`: stage 2 → stage 3. -/
theorem bX12 {k l : Fin h} (hk : k ∉ S1) (hl : l ∉ S3) :
    IncW (lab 1 S1 S3 ⊤ ⊤) (lab 2 S1 S2 ⊤ (L1 S3)) := by
  unfold lab
  rw [bet1, piS1, bet2, piS2]
  refine ⟨sup_le ?_ ?_, Or.inr ⟨t3 (ek k) (ek k) (ek l), Submodule.mem_sup_left
    (Submodule.mem_sup_left (mem_T3 (ek_mem_Pp hk) Submodule.mem_top Submodule.mem_top)), by
      simp [t3_dot, dot_ek_ek], orth_sup (orth_T3_2 _ _ (orth_L1 (dot_tt_ek hl)))
        (orth_T3_2 _ _ (orth_L1 (dot_tt_ek hl)))⟩⟩
  · exact le_sup_of_le_left (le_sup_of_le_left (T3_mono le_rfl le_rfl le_top))
  · calc T3 (L1 S1) ⊤ (L1 S3) ≤ T3 (L1 S1) (Pp S2) (L1 S3) ⊔ T3 (L1 S1) (L1 S2) (L1 S3) := by
          rw [top_split hS2]; exact T3_sup1 _ _
      _ ≤ _ := sup_le_sup (le_sup_of_le_right (T3_mono le_rfl le_rfl le_top)) le_rfl

/-- `Y`: stage 1 → stage 2 (equal labels). -/
theorem bY01 : lab 0 S2 S3 ⊤ (Pp S1) = lab 1 S1 S3 (L1 S2) ⊥ := by
  unfold lab
  rw [bet0, piS0, bet1, piS1, T3_bot1, bot_sup_eq, sup_bot_eq]

/-- `Y`: stage 2 → stage 3 (equal labels). -/
theorem bY12 : lab 1 S1 S3 ⊤ (Pp S2) = lab 2 S1 S2 (L1 S3) ⊥ := by
  unfold lab
  rw [bet1, piS1, bet2, piS2, T3_bot2, sup_bot_eq]

/-- The source label of `X_a`: `U_a = ⟨u_a⟩` is the first gate label. -/
theorem srcX : Submodule.span (ZMod 2) {t3 (tt S1) (tt S2) (tt S3)} = lab 0 S2 S3 ⊤ (L1 S1) := by
  unfold lab
  rw [bet0, piS0, bot_sup_eq, T3_L1 hS1 hS2 hS3]

/-- The source label of `Y_a`: zero. -/
theorem srcY : (⊥ : Submodule (ZMod 2) (Vc h)) = lab 0 S2 S3 (L1 S1) ⊥ := by
  rw [lab, bet0, piS0, T3_bot0, sup_bot_eq]

/-- The sink label of `Y_a`: `U_a^⊥` is the last gate label `(B ⊗ F) ⊥ (P ⊗ t^⊥)`. -/
theorem sinkY : NetLabels.orth 1 (Submodule.span (ZMod 2) {t3 (tt S1) (tt S2) (tt S3)}) =
    lab 2 S1 S2 ⊤ (Pp S3) := by
  set u := t3 (tt S1) (tt S2) (tt S3)
  have hu : piV 2 S1 S2 (tt S3) = u := rfl
  have hO : Orth (lab 2 S1 S2 ⊤ (Pp S3)) u := hu ▸ piV_orth hS1 hS2 2 (orth_Pp S3)
  have hsplit : (⊤ : Submodule (ZMod 2) (Vc h)) ≤
      lab 2 S1 S2 ⊤ (Pp S3) ⊔ Submodule.span (ZMod 2) {u} := by
    have e3 := T3_sup2 (U0 := L1 S1) (U1 := L1 S2) (Pp S3) (L1 S3)
    rw [← top_split hS3] at e3
    have e4 := lab2_top hS1 hS2 (S1 := S1) (S2 := S2)
    unfold lab at e4 ⊢
    rw [piS2] at e4 ⊢
    rw [← e4, ← T3_L1 hS1 hS2 hS3, sup_assoc]
    exact sup_le_sup le_rfl e3
  apply le_antisymm
  · intro x hx
    obtain ⟨l, hl, v, hv, rfl⟩ := Submodule.mem_sup.1 (hsplit (Submodule.mem_top (x := x)))
    obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hv
    have h1 := (NetComplexLabels.mem_orth_one.1 hx) u (Submodule.mem_span_singleton_self u)
    rw [dotProduct_add, dotProduct_smul, dotProduct_comm, hO l hl,
      show u ⬝ᵥ u = 1 from piV_norm hS1 hS2 2 (tt_norm hS3), smul_eq_mul, mul_one,
      zero_add] at h1
    rw [h1, zero_smul, add_zero]
    exact hl
  · intro x hx
    rw [NetComplexLabels.mem_orth_one]
    intro z hz
    obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
    rw [smul_dotProduct, dotProduct_comm, hO x hx, smul_zero]

end Boundary

end NetComplexP8

end

section
-- Source module: Solutions.NetComplexInterface
/-!
# Proposition 8: the complex network with phase frames

Labels are phase functions `q : 𝔽₂^m → ZMod 4` (an additive group); the frame of `q` is
`Φ_q = W diag(i^q) W` (`W = H^{⊗m}`, `W⁻¹ = W`), so `Φ_{q+q'} = Φ_q Φ_{q'}` and `Φ_0 = id`.
For a label `U` one takes `q_U(x) = wt(P_U x) mod 4`, so `Φ_{q_U} = C_U` of the paper.

* `network_realizes_var`: the abstract network theorem with role-dependent endpoint differences
  (same proof as `AModel.network_realizes`).
* `phase_interface`: the corrected complex network (signed exchange of `NetComplexLemma5`
  followed by negation of the physical `X` outputs), run on arrays `𝔽₂^m → ℂ` with any gate
  labelling, outputs `Φ_{q_sink(ρ w) - q_source(w)} f_w` on role `ρ w`.
* `phase_interface_full`: if that difference is `wt` (zero → full label), the route applies
  `C^{⊗m}`.
* `phase_interface_mixed` + `Z_correct_tensor`: if the difference is `wt + 2[u·x]` (the pair
  `X_a → Y_a`), the route applies `C⁻¹` on `supp u` and `C` elsewhere, and applying `Z` on
  `supp u` before and after together with the scalar `i^{wt u}` gives `C^{⊗m}` again.
-/

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

namespace NetComplexInterface

open Matrix Finset AModel NetComplex NetComplexPhase Complex

/-! ## The network theorem with role-dependent endpoint differences -/

section Var

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

/-- Same as `AModel.network_realizes`, but without assuming the endpoint difference is uniform:
the output on `ρ w` is `Φ (Mout (ρ w) - Min w) (f w)`. -/
theorem network_realizes_var (Φ : M → (Ω → R) →ₗ[R] (Ω → R))
    (hadd : ∀ a b x, Φ (a + b) x = Φ a (Φ b x)) (hzero : ∀ x, Φ 0 x = x)
    (gates : List (NGate Wr R M)) (hg : ∀ g ∈ gates, g.OK)
    (ρ : Wr → Wr) (hρ : ∀ (v : Wr → R) w, scalarRun gates v (ρ w) = v w)
    (Min Mout : Wr → M) (f : Wr → Ω → R) :
    ∀ w, netRun Φ gates Min Mout f (ρ w) = Φ (Mout (ρ w) - Min w) (f w) := by
  intro w
  have hinv := physRun_inv Φ hadd gates hg (Min, f) (fun w => Φ (-Min w) (f w))
    (fun w => by simp [← hadd, hzero]) (ρ w)
  have hlog : gates.foldl logStep (fun w => Φ (-Min w) (f w)) (ρ w) = Φ (-Min w) (f w) := by
    funext ω
    rw [logRun_apply, hρ]
  simp only [netRun]
  rw [hinv, hlog, ← hadd, sub_add_cancel, ← hadd, ← sub_eq_add_neg]

end Var

/-! ## Phase frames -/

section Frames

variable {m : ℕ}

/-- Arrays on one wire. -/
abbrev Arr (m : ℕ) := (Fin m → ZMod 2) → ℂ

lemma WH_add (f₁ f₂ : NetComplexInterface.Arr m) : WH (f₁ + f₂) = WH f₁ + WH f₂ := by
  funext y
  simp only [WH, Pi.add_apply, mul_add, Finset.sum_add_distrib]

lemma WH_smul (c : ℂ) (f : NetComplexInterface.Arr m) : WH (c • f) = c • WH f := by
  funext y
  simp only [WH, Pi.smul_apply, smul_eq_mul, Finset.mul_sum]
  refine Finset.sum_congr rfl fun x _ => ?_
  ring

/-- Phase-frame application `g ↦ W diag(i^q) W g`. -/
noncomputable def phaseOp (q : (Fin m → ZMod 2) → ZMod 4) (g : NetComplexInterface.Arr m) : NetComplexInterface.Arr m :=
  WH (fun x => I ^ (q x).val * WH g x)

/-- The frame `Φ_q = W diag(i^q) W` as a linear map. -/
noncomputable def PhiQ (q : (Fin m → ZMod 2) → ZMod 4) : NetComplexInterface.Arr m →ₗ[ℂ] NetComplexInterface.Arr m where
  toFun := phaseOp q
  map_add' f₁ f₂ := by
    funext y
    change WH _ y = WH _ y + WH _ y
    have e : (fun x => I ^ (q x).val * WH (f₁ + f₂) x) =
        fun x => 1 * (I ^ (q x).val * WH f₁ x) + 1 * (I ^ (q x).val * WH f₂ x) := by
      funext x; rw [WH_add]; simp only [Pi.add_apply]; ring
    rw [e, WH_lin]; ring
  map_smul' c f := by
    funext y
    change WH _ y = c * WH _ y
    have e : (fun x => I ^ (q x).val * WH (c • f) x) =
        fun x => c * (I ^ (q x).val * WH f x) + 0 * (I ^ (q x).val * WH f x) := by
      funext x; rw [WH_smul]; simp only [Pi.smul_apply, smul_eq_mul]; ring
    rw [e, WH_lin]; ring

lemma I_pow_val_add (a b : ZMod 4) : I ^ (a + b).val = I ^ a.val * I ^ b.val := by
  rw [← pow_add]
  apply I_pow_mod
  push_cast
  simp only [ZMod.natCast_val, ZMod.cast_id', id]

lemma PhiQ_add (a b : (Fin m → ZMod 2) → ZMod 4) (g : NetComplexInterface.Arr m) :
    PhiQ (a + b) g = PhiQ a (PhiQ b g) := by
  change phaseOp (a + b) g = phaseOp a (phaseOp b g)
  simp only [phaseOp, WH_WH]
  congr 1
  funext x
  rw [Pi.add_apply, I_pow_val_add, mul_assoc]

lemma PhiQ_zero (g : NetComplexInterface.Arr m) : PhiQ 0 g = g := by
  change phaseOp 0 g = g
  simp only [phaseOp, Pi.zero_apply, ZMod.val_zero, pow_zero, one_mul]
  exact WH_WH g

end Frames

/-! ## The interface for the complex network -/

section Interface

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

noncomputable instance : Invertible (2 : ℂ) := invertibleOfNonzero two_ne_zero

/-- The tensor power `C^{⊗m}` acting on arrays. -/
noncomputable def Cten (g : NetComplexInterface.Arr m) : NetComplexInterface.Arr m := fun y => ∑ z, (∏ i, CK (y i) (z i)) * g z

/-- `C⁻¹` on `supp u`, `C` elsewhere. -/
noncomputable def Mten (u : Fin m → ZMod 2) (g : NetComplexInterface.Arr m) : NetComplexInterface.Arr m :=
  fun y => ∑ z, (∏ i, (if i ∈ supp u then CKinv else CK) (y i) (z i)) * g z

/-- `Z` on the coordinates of `supp u`. -/
noncomputable def Zu (u : Fin m → ZMod 2) (g : NetComplexInterface.Arr m) : NetComplexInterface.Arr m :=
  fun z => (∏ i, (if i ∈ supp u then chi (z i) else 1)) * g z

/-- **Z correction.** `i^{wt u} · Z_u ∘ Mten u ∘ Z_u = C^{⊗m}` (from `C = i Z C⁻¹ Z`). -/
theorem Z_correct_tensor (u : Fin m → ZMod 2) (g : NetComplexInterface.Arr m) :
    I ^ NetComplexPhase.wt u • Zu u (Mten u (Zu u g)) = Cten g := by
  funext y
  simp only [Pi.smul_apply, smul_eq_mul, Zu, Mten, Cten, Finset.mul_sum]
  refine Finset.sum_congr rfl fun z _ => ?_
  rw [← Z_correction u y z]
  simp only [Finset.prod_mul_distrib]
  ring

end Interface

end NetComplexInterface

end

section
-- Source module: Solutions.NetComplexP8Edge
/-!
# Prop. 8, part 4: one edge

For labels `U` (tail) and `V` (head) in `𝔽₂^m`:

* `Up U V`: both nondegenerate, `U ≤ V`, and `U = V` or `V ∩ U^⊥` contains a norm-one vector;
  `EdgeOK V U := Up U V ∨ Up V U` (comparable, nondegenerate, nonalternating residual).
* `Fd V U = dim (V ∩ U^⊥) + dim (U ∩ V^⊥)`: the residual dimension `|dim V − dim U|`
  (`Fd_up`, `Fd_down`).
* `edge_kernel` (**Proposition 8, per edge**): the residual has an orthonormal basis `B` with
  `|B| = Fd V U`, and the phase-frame change `C_V C_U⁻¹ = Φ_{q_V − q_U}` is the product of one
  translation kernel `aI + bX_v` or its inverse per `v ∈ B`.
-/

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

namespace NetComplexP8

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexPhase NetComplexLabels
  NetComplexInterface Complex

variable {m : ℕ}

/-- An increasing edge `U → V`. -/
def Up (U V : Submodule (ZMod 2) (Fin m → ZMod 2)) : Prop :=
  NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) U ∧
    NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) V ∧ IncW U V

/-- An edge with head `V`, tail `U`: comparable nondegenerate labels, nonalternating residual. -/
def EdgeOK (V U : Submodule (ZMod 2) (Fin m → ZMod 2)) : Prop := Up U V ∨ Up V U

/-- Residual dimension. -/
noncomputable def Fd (V U : Submodule (ZMod 2) (Fin m → ZMod 2)) : ℕ :=
  finrank (ZMod 2) ↥(V ⊓ orth 1 U) + finrank (ZMod 2) ↥(U ⊓ orth 1 V)

lemma inf_orth_eq_bot {U V : Submodule (ZMod 2) (Fin m → ZMod 2)}
    (hU : NondegOn (1 : Matrix (Fin m) (Fin m) (ZMod 2)) U) (hUV : U ≤ V) :
    U ⊓ orth 1 V = ⊥ := by
  rw [eq_bot_iff]
  intro x hx
  rw [Submodule.mem_bot]
  refine hU x hx.1 fun y hy => ?_
  rw [bf_symm one_isSymm]
  exact (mem_orth.1 hx.2) y (hUV hy)

lemma Fd_up {U V : Submodule (ZMod 2) (Fin m → ZMod 2)} (h : Up U V) :
    (Fd V U : ℤ) = finrank (ZMod 2) V - finrank (ZMod 2) U := by
  obtain ⟨hU, hV, hle, -⟩ := h
  have := finrank_diff one_isSymm hU hV hle
  rw [Fd, inf_orth_eq_bot hU hle, finrank_bot]
  omega

lemma Fd_down {U V : Submodule (ZMod 2) (Fin m → ZMod 2)} (h : Up V U) :
    (Fd V U : ℤ) = finrank (ZMod 2) U - finrank (ZMod 2) V := by
  rw [Fd, add_comm]; exact Fd_up h

/-- `i^{[k mod 4]} = i^k`. -/
lemma I_pow_val_intCast (k : ℤ) : I ^ ((k : ZMod 4).val) = I ^ k := by
  rw [← zpow_natCast, ZMod.val_intCast]
  have hk := Int.mul_ediv_add_emod k 4
  conv_rhs => rw [← hk]
  rw [zpow_add₀ I_ne_zero, _root_.zpow_mul, show I ^ (4 : ℤ) = 1 by
    rw [show (4 : ℤ) = ((2 * 2 : ℕ) : ℤ) by norm_num, zpow_natCast, pow_mul, I_sq]; ring,
    _root_.one_zpow, one_mul]
  norm_num

/-- A norm-one binary vector has odd weight. -/
lemma wt_odd {v : (Fin m → ZMod 2)} (hv : v ⬝ᵥ v = 1) : NetComplexPhase.wt v % 2 = 1 := by
  have h : ((NetComplexPhase.wt v : ℕ) : ZMod 2) = 1 := by
    rw [wt_eq_sum, ← hv]
    push_cast
    simp only [dotProduct]
    refine Finset.sum_congr rfl fun i _ => ?_
    rcases NetComplexOrtho.zmod2_cases (v i) with e | e <;> rw [e] <;> decide
  have := congrArg ZMod.val h
  rw [ZMod.val_natCast] at this
  exact this

/-- The sign of the kernel of a residual vector of odd weight. -/
def sgn (v : (Fin m → ZMod 2)) : ℤ := if NetComplexPhase.wt v % 4 = 1 then 1 else -1

lemma sgn_pm (v : (Fin m → ZMod 2)) : sgn v = 1 ∨ sgn v = -1 := by unfold sgn; split_ifs <;> simp

lemma wt_cast_sgn {v : (Fin m → ZMod 2)} (hv : v ⬝ᵥ v = 1) : ((NetComplexPhase.wt v : ℤ) : ZMod 4) = (sgn v : ZMod 4) := by
  have ho := wt_odd hv
  have e : ((NetComplexPhase.wt v : ℤ) : ZMod 4) = ((NetComplexPhase.wt v % 4 : ℕ) : ZMod 4) := by
    push_cast; rw [ZMod.natCast_mod]
  rw [e]
  unfold sgn
  have : NetComplexPhase.wt v % 4 = 1 ∨ NetComplexPhase.wt v % 4 = 3 := by omega
  rcases this with h1 | h3
  · rw [if_pos h1, h1]; rfl
  · rw [if_neg (by omega), h3]; rfl

/-- The phase function as a product of single-vector phases. -/
lemma phase_prod (q : (Fin m → ZMod 2) → ZMod 4) (B : Finset (Fin m → ZMod 2)) (s : ℤ) (hs : s = 1 ∨ s = -1)
    (hB : ∀ v ∈ B, v ⬝ᵥ v = 1)
    (hq : ∀ x, q x = s * ((∑ v ∈ B, (v ⬝ᵥ x).val * NetComplexPhase.wt v : ℕ) : ZMod 4)) (x : (Fin m → ZMod 2)) :
    I ^ (q x).val =
      ((B.toList.map fun v => (s * sgn v, v)).map
        fun p => I ^ (p.1 * ((p.2 ⬝ᵥ x).val : ℤ))).prod := by
  have e : q x = ((∑ v ∈ B, s * sgn v * ((v ⬝ᵥ x).val : ℤ) : ℤ) : ZMod 4) := by
    rw [hq x]
    push_cast
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun v hv => ?_
    have := wt_cast_sgn (hB v hv)
    push_cast at this
    rw [this]; ring
  rw [e, I_pow_val_intCast, List.map_map, Finset.prod_map_toList]
  have hz : ∀ (S : Finset (Fin m → ZMod 2)) (f : (Fin m → ZMod 2) → ℤ), I ^ (∑ v ∈ S, f v) = ∏ v ∈ S, I ^ f v := by
    intro S f
    induction S using Finset.induction_on with
    | empty => simp
    | insert a S ha ih => rw [Finset.sum_insert ha, Finset.prod_insert ha, zpow_add₀ I_ne_zero, ih]
  rw [hz]
  rfl

/-- `Φ_q` for `q` a sum of single-vector phases is a product of translation kernels. -/
lemma phiQ_kernels (q : (Fin m → ZMod 2) → ZMod 4) (B : Finset (Fin m → ZMod 2)) (s : ℤ) (hs : s = 1 ∨ s = -1)
    (hB : ∀ v ∈ B, v ⬝ᵥ v = 1)
    (hq : ∀ x, q x = s * ((∑ v ∈ B, (v ⬝ᵥ x).val * NetComplexPhase.wt v : ℕ) : ZMod 4)) (g : NetComplexInterface.Arr m) :
    PhiQ q g = (B.toList.map fun v => (s * sgn v, v)).foldr (fun p g' => transK p.1 p.2 g') g := by
  have hL : ∀ p ∈ B.toList.map (fun v => (s * sgn v, v)), p.1 = 1 ∨ p.1 = -1 := by
    intro p hp
    obtain ⟨v, -, rfl⟩ := List.mem_map.1 hp
    rcases hs with rfl | rfl <;> rcases sgn_pm v with e | e <;> simp [e]
  rw [← WH_phase_list _ hL g]
  change WH _ = _
  congr 1
  funext x
  rw [phase_prod q B s hs hB hq x]

/-- **Proposition 8, one edge.** For an edge with comparable nondegenerate labels and
nonalternating residual, the residual has an orthonormal basis `B` of size `Fd V U`
(`= |dim V − dim U|`), and the phase-frame change `C_V C_U⁻¹` is the product of the translation
kernels `K_{ε,v}` (`ε = ±1`), one per `v ∈ B`. -/
theorem edge_kernel {U V : Submodule (ZMod 2) (Fin m → ZMod 2)} (hE : EdgeOK V U) :
    ∃ B : Finset (Fin m → ZMod 2), 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 (ℤ × (Fin m → ZMod 2)), 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 := by
  -- residual of an increasing edge
  have key : ∀ {U V : Submodule (ZMod 2) (Fin m → ZMod 2)}, Up U V → ∃ B : Finset (Fin m → ZMod 2), (∀ b ∈ B, b ∈ V ⊓ orth 1 U)
      ∧ Orthonormal2 B ∧ Submodule.span (ZMod 2) ↑B = V ⊓ orth 1 U ∧ B.card = Fd V U := by
    intro U V h
    obtain ⟨hU, hV, hle, hc⟩ := h
    have hnd := (nondegOn_one_iff _).1 (nondeg_diff one_isSymm hU hV hle)
    have hcase : V ⊓ orth 1 U = ⊥ ∨ ∃ x ∈ V ⊓ orth 1 U, x ⬝ᵥ x = 1 := by
      rcases hc with rfl | ⟨w, hw, hww, ho⟩
      · left
        exact inf_orth_eq_bot hU le_rfl
      · exact Or.inr ⟨w, ⟨hw, mem_orth_one.2 ho⟩, hww⟩
    obtain ⟨B, hBE, hB, hsp, hcard⟩ := exists_orthonormal_basis_card _ hnd hcase
    refine ⟨B, hBE, hB, hsp, ?_⟩
    rw [hcard, Fd, inf_orth_eq_bot hU hle, finrank_bot, add_zero]
  rcases hE with h | h
  · obtain ⟨B, hBE, hB, hsp, hcard⟩ := key h
    refine ⟨B, hB, Or.inl hsp, hcard, _, ?_, ?_, fun g => phiQ_kernels _ B 1 (Or.inl rfl) hB.1
      (fun x => ?_) g⟩
    · simp [List.map_map, Function.comp_def]
    · intro p hp
      obtain ⟨v, -, rfl⟩ := List.mem_map.1 hp
      rcases sgn_pm v with e | e <;> simp [e]
    · rw [Pi.sub_apply, qL_diff U V h.1 h.2.1 h.2.2.1 B hBE hB hsp x]
      push_cast; ring
  · obtain ⟨B, hBE, hB, hsp, hcard⟩ := key h
    refine ⟨B, hB, Or.inr hsp, by rw [hcard, Fd, Fd, add_comm], _, ?_, ?_,
      fun g => phiQ_kernels _ B (-1) (Or.inr rfl) hB.1 (fun x => ?_) g⟩
    · simp [List.map_map, Function.comp_def]
    · intro p hp
      obtain ⟨v, -, rfl⟩ := List.mem_map.1 hp
      rcases sgn_pm v with e | e <;> simp [e]
    · have := qL_diff V U h.1 h.2.1 h.2.2.1 B hBE hB hsp x
      rw [Pi.sub_apply, ← neg_sub, this]
      push_cast; ring

end NetComplexP8

end

section
-- Source module: Solutions.NetComplexProp8
/-!
# Proposition 8, route statement with the prescribed terminal labels

Terminal labels (§3.3): source `U_a = ⟨u_a⟩` on `X_a`, `0` elsewhere; sink `U_a^⊥` on `Y_a`,
`F` elsewhere. With phase labels `q_U = wt ∘ P_U (mod 4)` as frames `Φ_{q_U} = C_U`, and with
any intermediate gate labels, the corrected complex network applies `C^{⊗m}` on every route
`w ↦ ρ w` except `X_a → Y_a`, which becomes `C^{⊗m}` after `Z` on `supp u_a` before the
network and `i^{wt u_a} Z` after it. Here `u_a` is any unit vector of odd weight (for
`u_a = t_{a₁} ⊗ t_{a₂} ⊗ t_{a₃}`: norm `1` by `NetComplexLabels.dot_cubeTriple_self`, weight 27).
-/

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

namespace NetComplexProp8

open Matrix Finset AModel NetComplex NetComplexPhase NetComplexInterface NetComplexLabels Complex

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

/-- Source phase labels: `q_{U_a}` on `X_a`, `q_0 = 0` elsewhere. -/
noncomputable def Min8 (u : T × T × T → Fin m → ZMod 2) : Wr ind → ((Fin m → ZMod 2) → ZMod 4)
  | Sum.inl a => qL (ZMod 2 ∙ u a)
  | Sum.inr _ => qL ⊥

/-- Sink phase labels: `q_{U_a^⊥}` on `Y_a`, `q_F` elsewhere. -/
noncomputable def Mout8 (u : T × T × T → Fin m → ZMod 2) : Wr ind → ((Fin m → ZMod 2) → ZMod 4)
  | Sum.inr (Sum.inl a) => qL (NetLabels.orth 1 (ZMod 2 ∙ u a))
  | _ => qL ⊤

end NetComplexProp8

end

section
-- Source module: Solutions.NetComplexNum
/-!
# The concrete complex network (`h = 100`): neighbour count and the numbers of §3.1, §3.5

* `count_nb_c`: a triple `S ⊂ [n]` has `C(n-3, 3) + 3(n-3)` complex neighbours (distinct triples
  with even intersection): `C(n-3,3)` with intersection `0` and `3(n-3)` with intersection `2`.
* For `T₀` = triples of `Fin 100`: `z_c = 147731`, `|Nb| = 161700 · 147731`, and the wire count
  `W_c = 2N + I(v z_c + c_c) = 1873807244643542670000` (`c_c = 101` central wires `C_i`, `C_*`).
* The numbers of Proposition 8: `L_c = I c_c h`, `s_c = W_c m - 2N + 2L_c =
  1873807244636671267308000000 < W_c m`, `L_c / N = 101/539`, deficit `2N - 2L_c > 0`.
-/

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

namespace NetComplex

open Finset

/-! ## 1. Counting complex neighbours -/

section Count

variable {n : ℕ}

/-- Triples disjoint from `S`: `C(n-3, 3)`. -/
lemma count_inter0 (S : Finset (Fin n)) (hS : S.card = 3) :
    (univ.filter fun U : Finset (Fin n) => U.card = 3 ∧ (S ∩ U).card = 0).card =
      (n - 3).choose 3 := by
  have : (univ.filter fun U : Finset (Fin n) => U.card = 3 ∧ (S ∩ U).card = 0) =
      powersetCard 3 Sᶜ := by
    ext U
    simp only [mem_filter, mem_univ, true_and, mem_powersetCard, Finset.card_eq_zero]
    constructor
    · rintro ⟨h3, h0⟩
      refine ⟨fun x hx => Finset.mem_compl.2 fun hxS => ?_, h3⟩
      have : x ∈ S ∩ U := mem_inter.2 ⟨hxS, hx⟩
      rw [h0] at this; simp at this
    · rintro ⟨hsub, h3⟩
      refine ⟨h3, eq_empty_of_forall_notMem fun x hx => ?_⟩
      exact Finset.mem_compl.1 (hsub (mem_inter.1 hx).2) (mem_inter.1 hx).1
  rw [this, card_powersetCard, card_compl, hS, Fintype.card_fin]

/-- Triples meeting `S` in two points: `3(n-3)`. -/
lemma count_inter2 (S : Finset (Fin n)) (hS : S.card = 3) :
    (univ.filter fun U : Finset (Fin n) => U.card = 3 ∧ (S ∩ U).card = 2).card =
      3 * (n - 3) := by
  have hc : (S ×ˢ Sᶜ).card = 3 * (n - 3) := by
    rw [card_product, card_compl, hS, Fintype.card_fin]
  rw [← hc]
  symm
  apply Finset.card_bij (fun p _ => insert p.2 (S.erase p.1))
  · rintro ⟨s, x⟩ hp
    simp only [mem_product, Finset.mem_compl] at hp
    obtain ⟨hs, hx⟩ := hp
    have hxe : x ∉ S.erase s := fun h => hx (mem_of_mem_erase h)
    simp only [mem_filter, mem_univ, true_and]
    refine ⟨by rw [card_insert_of_notMem hxe, card_erase_of_mem hs, hS], ?_⟩
    have : S ∩ insert x (S.erase s) = S.erase s := by
      ext y
      simp only [mem_inter, mem_insert, mem_erase]
      constructor
      · rintro ⟨hy, rfl | h⟩
        · exact absurd hy hx
        · exact h
      · rintro ⟨hne, hy⟩; exact ⟨hy, Or.inr ⟨hne, hy⟩⟩
    rw [this, card_erase_of_mem hs, hS]
  · rintro ⟨s, x⟩ hp ⟨s', x'⟩ hp' e
    simp only [mem_product, Finset.mem_compl] at hp hp'
    simp only at e
    have hxx : x = x' := by
      have : x ∈ insert x' (S.erase s') := e ▸ mem_insert_self x _
      rcases mem_insert.1 this with h | h
      · exact h
      · exact absurd (mem_of_mem_erase h) hp.2
    have hss : s = s' := by
      by_contra hne
      have : s ∈ insert x' (S.erase s') := mem_insert_of_mem (mem_erase.2 ⟨hne, hp.1⟩)
      rw [← e] at this
      rcases mem_insert.1 this with h | h
      · exact hp.2 (h ▸ hp.1)
      · exact (mem_erase.1 h).1 rfl
    rw [hss, hxx]
  · intro U hU
    simp only [mem_filter, mem_univ, true_and] at hU
    obtain ⟨hU3, hU2⟩ := hU
    have h1 : (S \ U).card = 1 := by
      have := card_sdiff_add_card_inter S U
      omega
    have h2 : (U \ S).card = 1 := by
      have := card_sdiff_add_card_inter U S
      rw [inter_comm] at this
      omega
    obtain ⟨s, hs⟩ := card_eq_one.1 h1
    obtain ⟨x, hx⟩ := card_eq_one.1 h2
    have hsS : s ∈ S \ U := by rw [hs]; exact mem_singleton_self s
    have hxU : x ∈ U \ S := by rw [hx]; exact mem_singleton_self x
    refine ⟨(s, x), ?_, ?_⟩
    · simp only [mem_product, Finset.mem_compl]
      exact ⟨(mem_sdiff.1 hsS).1, (mem_sdiff.1 hxU).2⟩
    · ext y
      simp only [mem_insert, mem_erase]
      constructor
      · rintro (rfl | ⟨hne, hy⟩)
        · exact (mem_sdiff.1 hxU).1
        · by_contra hyU
          have : y ∈ S \ U := mem_sdiff.2 ⟨hy, hyU⟩
          rw [hs] at this
          exact hne (mem_singleton.1 this)
      · intro hy
        by_cases hyS : y ∈ S
        · right
          refine ⟨fun e => ?_, hyS⟩
          rw [e] at hy
          exact (mem_sdiff.1 hsS).2 hy
        · left
          have : y ∈ U \ S := mem_sdiff.2 ⟨hy, hyS⟩
          rw [hx] at this
          exact mem_singleton.1 this

/-- **Complex neighbours of a triple**: `C(n-3,3) + 3(n-3)`. -/
theorem count_nb_c (S : Finset (Fin n)) (hS : S.card = 3) :
    (univ.filter fun U : Finset (Fin n) => U.card = 3 ∧ U ≠ S ∧ (S ∩ U).card % 2 = 0).card =
      (n - 3).choose 3 + 3 * (n - 3) := by
  rw [← count_inter0 S hS, ← count_inter2 S hS, ← card_union_of_disjoint]
  · congr 1
    ext U
    simp only [mem_filter, mem_univ, true_and, mem_union]
    constructor
    · rintro ⟨h3, hne, hev⟩
      have hle : (S ∩ U).card ≤ 3 := hS ▸ card_le_card inter_subset_left
      have hne3 : (S ∩ U).card ≠ 3 := by
        intro h33
        have e1 : S ∩ U = S := eq_of_subset_of_card_le inter_subset_left (by rw [h33, hS])
        have e2 : S ∩ U = U := eq_of_subset_of_card_le inter_subset_right (by rw [h33, h3])
        exact hne (e2.symm.trans e1)
      omega
    · rintro (⟨h3, h0⟩ | ⟨h3, h2⟩)
      · refine ⟨h3, ?_, by rw [h0]⟩
        rintro rfl; rw [inter_self, hS] at h0; omega
      · refine ⟨h3, ?_, by rw [h2]⟩
        rintro rfl; rw [inter_self, hS] at h2; omega
  · rw [disjoint_filter]
    intro U _ h0 h2
    omega

end Count

/-! ## 2. The concrete network -/

/-- The triples of `Fin 100`. -/
abbrev T₀ := {S : Finset (Fin 100) // S.card = 3}

/-- The indicator map of the triple family. -/
def ind₀ : NetComplex.T₀ → Finset (Fin 100) := Subtype.val

lemma ind₀_card (t : NetComplex.T₀) : (NetComplex.ind₀ t).card = 3 := t.2
lemma ind₀_inj : Function.Injective ind₀ := Subtype.val_injective

lemma card_T₀ : Fintype.card NetComplex.T₀ = 161700 := by
  rw [Fintype.card_finset_len, Fintype.card_fin, Nat.choose_eq_descFactorial_div_factorial]
  norm_num [Nat.descFactorial, Nat.factorial]

/-- `z_c = C(97,3) + 3 · 97 = 147731`. -/
lemma card_nbr_c (S : NetComplex.T₀) :
    Fintype.card {U : NetComplex.T₀ // S ≠ U ∧ (NetComplex.ind₀ S ∩ NetComplex.ind₀ U).card % 2 = 0} = 147731 := by
  have e : ∀ U : NetComplex.T₀, (S ≠ U ∧ (NetComplex.ind₀ S ∩ NetComplex.ind₀ U).card % 2 = 0) ↔
      (U.1 ≠ S.1 ∧ (S.1 ∩ U.1).card % 2 = 0) := fun U =>
    ⟨fun ⟨h1, h2⟩ => ⟨fun h => h1 (Subtype.ext h.symm), h2⟩,
     fun ⟨h1, h2⟩ => ⟨fun h => h1 (congrArg Subtype.val h.symm), h2⟩⟩
  rw [Fintype.card_congr (Equiv.subtypeEquivRight e)]
  rw [Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter
    (fun U : Finset (Fin 100) => U.card = 3)
    (fun U => U ≠ S.1 ∧ (S.1 ∩ U).card % 2 = 0)),
    Fintype.card_subtype]
  rw [show (univ.filter fun U : Finset (Fin 100) =>
      U.card = 3 ∧ U ≠ S.1 ∧ (S.1 ∩ U).card % 2 = 0) =
      univ.filter fun U : Finset (Fin 100) => U.card = 3 ∧ U ≠ S.1 ∧ (S.1 ∩ U).card % 2 = 0
    from rfl, count_nb_c S.1 S.2, Nat.choose_eq_descFactorial_div_factorial]
  norm_num [Nat.descFactorial, Nat.factorial]

lemma card_Nb₀ : Fintype.card (Nb NetComplex.ind₀) = 161700 * 147731 := by
  rw [Fintype.card_subtype, Finset.card_filter, Fintype.sum_prod_type]
  have : ∀ S : NetComplex.T₀, (∑ U : NetComplex.T₀, if (S, U).1 ≠ (S, U).2 ∧
      (NetComplex.ind₀ (S, U).1 ∩ NetComplex.ind₀ (S, U).2).card % 2 = 0 then 1 else 0) = 147731 := by
    intro S
    rw [← card_nbr_c S, Fintype.card_subtype, Finset.card_filter]
  simp only [this, Finset.sum_const, Finset.card_univ, NetComplex.card_T₀, smul_eq_mul]

/-- **(4)**: `W_c = 2N + I(v z_c + c_c) = 1873807244643542670000`. -/
theorem card_Wr₀ : Fintype.card (Wr NetComplex.ind₀) = 1873807244643542670000 := by
  simp only [Wr, Fintype.card_sum, Fintype.card_prod, NetComplex.card_T₀, NetComplex.card_Nb₀, Fintype.card_fin,
    Fintype.card_option]

end NetComplex

end