Round-six κ development, definitions part 2

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_KappaFramework

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.ButterflyGuard
/-!
# §5.4 An explicit guard-width bound (and the numeric parts of Proposition 14)

1. The constants `E = 64(W+m+1)³`, `B = s+E`, `ν = min{j ≥ 1 : m^j ≥ B}`, `C1 = max{20, ν+3}`,
   `C0 = 128 m B²` for the complex network `m = 10⁶`, `W_c`, `s_c`: `m^10 < B < m^11`, `ν = 11`,
   `C1 = 20`.
2. The depth recurrence `A(e) ≤ s A(e/m) + E`, `A ≤ 8e` at leaves, gives `A ≤ 8 d B^{k+1}
   ≤ 8 B² d^{ν+1}`, and the final chain `8mB²d^{ν+2}+8d+t+9 ≤ … < 128mB²d^{ν+3} ≤ C0 d^{C1}`.
3. Dyadic growth: a value at arithmetic depth `ℓ` (add, sub, halve, negate, multiply by `i`)
   lies in `2^{-(p+ℓ)} ℤ[i]` with modulus `≤ 2^ℓ`; hence `p+Δ` fractional and `Δ+3` integer and
   sign bits represent it exactly.
4. The final truncation `Q_p` toward zero: `|Q_p z| ≤ |z|`, `|Q_p z - z| < √2 · 2^{-p}`.
5. The width bookkeeping of the proof of Proposition 14.
-/

namespace Butterfly

open Complex

/-! ## 1. The constants -/

/-! ## 2. Depth recurrence and the chain -/

/-! ## 3. Dyadic depth invariant -/

/-- A Gaussian dyadic value of arithmetic depth `ℓ` above an input grid `2^{-p} ℤ[i]`:
it lies in `2^{-(p+ℓ)} ℤ[i]` and has modulus at most `2^ℓ`. -/
def DyGood (p ℓ : ℕ) (z : ℂ) : Prop :=
  (∃ a b : ℤ, z = ((a : ℂ) + (b : ℂ) * I) / 2 ^ (p + ℓ)) ∧ ‖z‖ ≤ 2 ^ ℓ

lemma DyGood.neg {p ℓ : ℕ} {z : ℂ} (hz : DyGood p ℓ z) : DyGood p ℓ (-z) := by
  obtain ⟨⟨a, b, rfl⟩, hn⟩ := hz
  exact ⟨⟨-a, -b, by push_cast; ring⟩, by rwa [norm_neg]⟩

/-! ## 4. Final truncation toward zero -/

/-! ## 5. Width bookkeeping in the proof of Proposition 14 -/

end Butterfly

end

section
-- Source module: Solutions.ButterflyTensor
/-!
# §5.1 Phase-frame identities and tensor products on selected bits

The `2 × 2` matrices of §5.1 of the OpenAI preprint "Integer multiplication below n log n":
`H0 = ½[[1,1],[1,-1]]`, `S = diag(1,i)`, `Z = diag(1,-1)`, `X = [[0,1],[1,0]]`,
`C = HSH = aI + bX` with `a = (1+i)/2`, `b = (1-i)/2`, and the identities (13), (14), (17), (18).

Tensor products over an arbitrary finite set `ι` of selected bits:
`tensF A x y = ∏ i, A i (x i) (y i)` for a family `A : ι → M₂`.
-/

namespace Butterfly

open Matrix Complex Finset

/-! ## Tensor products on selected bits -/

section Tensor

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

theorem tensF_one : tensF (fun _ : ι => (1 : M2)) = 1 := by
  ext x y
  simp only [tensF, Matrix.one_apply]
  rw [Finset.prod_boole]
  by_cases h : x = y
  · subst h; simp
  · have : ¬ ∀ i ∈ (univ : Finset ι), x i = y i := fun h' => h (funext fun i => h' i (mem_univ _))
    rw [if_neg this, if_neg h]

end Tensor

/-! ## (15): address permutations conjugate translations -/

section Translate

variable {K V : Type*} [Ring K] [AddCommGroup V] [Module K V] {β : Type*}

end Translate

/-! ## Elementary row additions generate `GL(m, F₂)` -/

/-- Over `F₂`, every invertible matrix is a product of elementary row additions
`1 + E_{ij}` (`i ≠ j`) — the binary changes of basis of §5.1 use only these. -/
theorem gl_f2_row_additions {m : Type*} [Fintype m] [DecidableEq m]
    (M : Matrix m m (ZMod 2)) (hM : M.det ≠ 0) :
    ∃ L : List (m × m), (∀ p ∈ L, p.1 ≠ p.2) ∧
      M = (L.map fun p => transvection p.1 p.2 (1 : ZMod 2)).prod := by
  obtain ⟨L, L', D, hD⟩ := Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec M
  have hD1 : diagonal D = 1 := by
    have hdet : (diagonal D).det ≠ 0 := by
      intro h0
      apply hM
      rw [hD, det_mul, det_mul, h0]; simp
    rw [det_diagonal] at hdet
    ext i j
    simp only [diagonal_apply, one_apply]
    split_ifs with h
    · subst h
      have : D i ≠ 0 := fun h0 => hdet (Finset.prod_eq_zero (mem_univ i) h0)
      exact (show ∀ a : ZMod 2, a ≠ 0 → a = 1 by decide) _ this
    · rfl
  -- each transvection over `F₂` is `1` or a row addition
  have key : ∀ t : TransvectionStruct m (ZMod 2), ∃ l : List (m × m), (∀ p ∈ l, p.1 ≠ p.2) ∧
      t.toMatrix = (l.map fun p => transvection p.1 p.2 (1 : ZMod 2)).prod := by
    intro t
    have hc : t.c = 0 ∨ t.c = 1 := by
      exact (show ∀ a : ZMod 2, a = 0 ∨ a = 1 by decide) _
    rcases hc with h | h
    · refine ⟨[], by simp, ?_⟩
      simp [TransvectionStruct.toMatrix, h, transvection_zero]
    · refine ⟨[(t.i, t.j)], by simpa using t.hij, ?_⟩
      simp [TransvectionStruct.toMatrix, h]
  have keyL : ∀ L : List (TransvectionStruct m (ZMod 2)), ∃ l : List (m × m),
      (∀ p ∈ l, p.1 ≠ p.2) ∧
      (L.map TransvectionStruct.toMatrix).prod =
        (l.map fun p => transvection p.1 p.2 (1 : ZMod 2)).prod := by
    intro L
    induction L with
    | nil => exact ⟨[], by simp, by simp⟩
    | cons t L ih =>
      obtain ⟨l₁, h₁, e₁⟩ := key t
      obtain ⟨l₂, h₂, e₂⟩ := ih
      refine ⟨l₁ ++ l₂, fun p hp => ?_, ?_⟩
      · rcases List.mem_append.1 hp with hp | hp
        exacts [h₁ p hp, h₂ p hp]
      · simp [e₁, e₂, List.prod_append]
  obtain ⟨l₁, h₁, e₁⟩ := keyL L
  obtain ⟨l₂, h₂, e₂⟩ := keyL L'
  refine ⟨l₁ ++ l₂, fun p hp => ?_, ?_⟩
  · rcases List.mem_append.1 hp with hp | hp
    exacts [h₁ p hp, h₂ p hp]
  · rw [hD, hD1, mul_one, e₁, e₂, List.map_append, List.prod_append]

end Butterfly

end

section
-- Source module: Solutions.NetComplexPhase
/-!
# Proposition 8 (binary phase interface): the algebra over `ℂ`

1. The `2 × 2` matrices `H = (1/√2)[[1,1],[1,-1]]`, `C = H diag(1,i) H = aI + bX`
   (`a = (1+i)/2`, `b = (1-i)/2`), `Z = diag(1,-1)`; `C⁻¹ = āI + b̄X`; `C = i Z C⁻¹ Z`,
   `C⁻¹ = -i Z C Z`; `H Z H = X`.
2. Binary weights: `wt(z + w) = wt z + wt w - 2 |supp z ∩ supp w|`; if `z · w = 0` over `𝔽₂`,
   weight is additive mod 4; for a family orthogonal to `y` and pairwise orthogonal,
   `wt(y + ∑ cⱼ vⱼ) ≡ wt y + ∑ [cⱼ] wt vⱼ (mod 4)`; `2[u·x] ≡ 2 ∑_{j ∈ supp u} xⱼ (mod 4)`.
3. The phase identity `i^{ε[b]} = (1+iε)/2 + (1-iε)/2 · (-1)^b` for `ε = ±1`.
4. The normalized Walsh–Hadamard transform `WH` on functions `(Fin m → ZMod 2) → ℂ` (the
   matrix `H^{⊗m}`, `WH_eq_tensor`), `WH ∘ WH = id`, the general tensor-conjugation formula
   `WH (∏ᵢ dᵢ(xᵢ) · WH g) = (⊗ᵢ Kᵢ) g`, and its instances:
   * `WH_char`: `W diag((-1)^{v·x}) W⁻¹ = X_v` (translation by `v`);
   * `WH_phase`: `W diag(i^{ε[v·x]}) W⁻¹ = (1+iε)/2 · I + (1-iε)/2 · X_v`, i.e. `aI + bX_v` for
     `ε = 1` and its inverse `āI + b̄X_v` for `ε = -1`;
   * `WH_full`: `W diag(i^{wt x}) W⁻¹ = C^{⊗m}` (the frame of the full label);
   * `WH_mixed`: `W diag(i^{wt x + 2[u·x]}) W⁻¹ = (C⁻¹ on supp u) ⊗ (C elsewhere)`, and with
     `Z` conjugation on `supp u` and the scalar `i^{|supp u|}` this becomes `C^{⊗m}` again.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetComplexPhase

open Matrix Finset Complex

/-! ## 1. The `2 × 2` matrices -/

/-- `1/√2` as a complex number. -/
noncomputable def rs2 : ℂ := ((Real.sqrt 2 : ℝ) : ℂ)⁻¹

noncomputable def Hm : Matrix (Fin 2) (Fin 2) ℂ := rs2 • !![1, 1; 1, -1]
def Xm : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; 1, 0]
def Zm : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, -1]
def Dm : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, I]

/-- `C = H diag(1, i) H`. -/
noncomputable def Cm : Matrix (Fin 2) (Fin 2) ℂ := Hm * Dm * Hm
/-- `C⁻¹ = ā I + b̄ X`. -/
noncomputable def Cinv : Matrix (Fin 2) (Fin 2) ℂ := ((1 - I) / 2) • 1 + ((1 + I) / 2) • Xm

/-! ## 2. Binary weights -/

section Weight

variable {m : ℕ}

end Weight

/-! ## 3. The phase identity -/

/-! ## 4. The Walsh–Hadamard transform `H^{⊗m}` and its conjugations -/

section WH

variable {m : ℕ}

end WH

end NetComplexPhase

end

section
-- Source module: Solutions.P8LiftIface
/-!
# A restricted Proposition 8 interface (only the paper's cheap local operations)

`Butterfly.Prop8Iface` allows an arbitrary matrix as a non-recursive step, which makes it
vacuous. Here the non-recursive steps are restricted to the operations of §3.5/§5.1, each
of which touches every state entry a bounded number of times:

* `gate G` — a pointwise scalar gate across roles at equal addresses (`G` on the roles,
  identity on the addresses);
* `rowAdd w i j` — a binary row addition `x(j,c) += x(i,c)` (all columns `c`) on the address
  bits of role `w`, i.e. an address permutation;
* `phase w k₀ k₁ a` — the diagonal phase `i^{k₀ + k₁|κ| + Σ_{(r,c)} a_r x(r,c)}` on role `w`
  (covers `Z_u` with `a = 2u`, `S` on selected bits, scalars `i^{27|κ|}`);
* `perm σ` — a permutation of the roles;
* `child w h fwd` — a recursive call on slot `h` of role `w` (forward or the (17) inverse).

The step list is independent of the column type `κ` (the same program for every `κ`).

* `Prop8IfaceR.toIface`: the forgetful map to `Butterfly.Prop8Iface` (so `recOp_eq`,
  `recCost_le`, `prop14_output` apply).
* `den_row_card_le`: every local step's matrix has at most `|R|` nonzero entries per row
  (`≤ 1` except for gates), so one local step costs `≤ W · V` entry operations.
* `recCostR_le`: the §5.3 bound for the recursion whose local work is the actual work
  `≤ nloc · W · V` of the local steps (`nloc` = number of local steps, independent of `κ`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace P8Lift

open Matrix Finset Complex Butterfly

namespace RStep

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

/-- The nonzero entries of row `p`. -/
noncomputable def rowSupp (A : ROp R m κ) (p : R × Addr m κ) : Finset (R × Addr m κ) :=
  univ.filter fun q => A p q ≠ 0

/-- Entry operations of one application of a step: the number of nonzero matrix entries. -/
noncomputable def work (T : Op κ) (st : RStep R m) : ℕ :=
  ∑ p, (rowSupp (st.den T) p).card

end RStep

open RStep

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

namespace Prop8IfaceR

variable {W s : ℕ}

variable [NeZero W]

end Prop8IfaceR

end P8Lift

end

section
-- Source module: Solutions.R6CxStep
/-!
# Round six, complex side: networks with slot-set children and temporaries (`Prop8IfaceH`)

Design decision 2 of `jain6/ARCH.md`. Compared with `P8Lift.Prop8IfaceR`:

* a child step `child w S neg` acts on a **slot set** `S ⊆ Fin m` of role `w` (all columns),
  with a **sign set** `neg`: with exact children it applies `C⁻¹` on the slots of `neg ∩ S`
  and `C` on the other slots of `S` (implemented as `(-i)^{|neg ∩ S||κ|} Z_N C^{⊗(S×κ)} Z_N`,
  one forward call of width `|S|`, by (17));
* roles are `Fin W ⊕ Fin T`: `W` data/scratch roles and `T` temporaries;
* correctness (**clean temporaries**): temporaries start at zero and are discarded, so only the
  data-to-data block of the denotation is constrained: it is block diagonal with `C^{⊗(Fin m × κ)}`
  on every role `inl _` (`DataCorrect`). This is Jain's tape model (a copy is a fresh zero
  stream, erased after use); `targetH` (dirty temporaries restored) implies it (`dataCorrect_of_targetH`);
* `hist`: the multiset of child widths `|S|` is `histMS h` (`n_w` children of width `w`),
  and every child width is `< m`.

Local steps are those of `P8Lift.RStep` (gates, row additions, phases, role permutations).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

/-- The multiset of child widths of a histogram `[(w, n_w)]`: `n_w` copies of `w`. -/
def histMS (h : List (ℕ × ℕ)) : Multiset ℕ := (h.map fun p => Multiset.replicate p.2 p.1).sum

@[simp] lemma histMS_nil : histMS [] = 0 := rfl

/-- Steps of a round-six complex network. -/
inductive HStep (R : Type) (m : ℕ) where
  | gate (G : Matrix R R ℂ)
  | rowAdd (w : R) (i j : Fin m) (hij : i ≠ j)
  | phase (w : R) (k₀ k₁ : ℕ) (a : Fin m → ℕ)
  | perm (σ : Equiv.Perm R)
  | child (w : R) (S neg : Finset (Fin m))

namespace HStep

variable {R : Type} {m : ℕ}

/-- The width `|S|` of a child step. -/
def width : HStep R m → Option ℕ
  | child _ S _ => some S.card
  | _ => none

/-- A restricted step as a round-six step (a single-slot child `h` becomes the slot set `{h}`,
sign set `∅` (forward) or `{h}` (inverse)). -/
def ofR : RStep R m → HStep R m
  | .gate G => gate G
  | .rowAdd w i j hij => rowAdd w i j hij
  | .phase w k₀ k₁ a => phase w k₀ k₁ a
  | .perm σ => perm σ
  | .child w h fwd => child w {h} (if fwd then ∅ else {h})

end HStep

/-! ## Slot-set families and the child semantics -/

section Sem

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

/-- `A` on the slots of `S` (all columns), identity elsewhere. -/
def setFam (S : Finset (Fin m)) (A : M2) : Fin m × κ → M2 := fun p => if p.1 ∈ S then A else 1

/-- `C⁻¹` on `neg ∩ S`, `C` on `S \ neg`, identity elsewhere. -/
noncomputable def slotFam (S neg : Finset (Fin m)) : Fin m × κ → M2 := fun p =>
  if p.1 ∈ S then (if p.1 ∈ neg then Cinv else Cm) else 1

/-- The exact child: `C^{⊗(S × κ)}` on the bits of the slots `S`. -/
noncomputable def chEx (S : Finset (Fin m)) : Op (Fin m × κ) := tensF (setFam (κ := κ) S Cm)

/-- The signed child: `(-i)^{|N||κ|} Z_N · ch S · Z_N` with `N = neg ∩ S` (17). -/
noncomputable def signedOp (ch : Finset (Fin m) → Op (Fin m × κ)) (S neg : Finset (Fin m)) :
    Op (Fin m × κ) :=
  ((-I) ^ ((neg ∩ S).card * Fintype.card κ)) •
    (tensF (setFam (κ := κ) (neg ∩ S) Zm) * ch S * tensF (setFam (κ := κ) (neg ∩ S) Zm))

lemma prod_setScalar (N : Finset (Fin m)) (c : ℂ) :
    ∏ p : Fin m × κ, (if p.1 ∈ N then c else 1) = c ^ (N.card * Fintype.card κ) := by
  rw [Fintype.prod_prod_type]
  have e : ∀ x : Fin m, ∏ _c : κ, (if x ∈ N then c else 1) =
      if x ∈ N then c ^ Fintype.card κ else 1 := by
    intro x; split_ifs <;> simp
  simp_rw [e]
  rw [Fintype.prod_ite_mem, Finset.prod_const, ← pow_mul, mul_comm]

/-- **Exact signed child** = the slot family `C^{±1}` (one forward call of width `|S|`). -/
theorem signedOp_chEx (S neg : Finset (Fin m)) :
    signedOp (chEx (κ := κ)) S neg = tensF (slotFam (κ := κ) S neg) := by
  unfold signedOp chEx
  rw [← tensF_mul, ← tensF_mul, ← prod_setScalar (κ := κ) (neg ∩ S) (-I), ← tensF_smul]
  congr 1; funext p
  simp only [setFam, slotFam, Finset.mem_inter]
  by_cases hS : p.1 ∈ S
  · by_cases hN : p.1 ∈ neg
    · simp only [hN, hS, and_self, if_true]
      rw [Cinv_eq_ZCZ]
    · simp [hN, hS]
  · simp [hS]

/-- The single-slot operator of `P8Lift` is a slot family. -/
theorem slotOp_tens (h : Fin m) (A : M2) :
    (slotOp h (tens A) : Op (Fin m × κ)) = tensF (fun p : Fin m × κ => if p.1 = h then A else 1) := by
  ext x y
  simp only [slotOp, tens, tensF, slotBits]
  rw [Fintype.prod_prod_type, Fintype.prod_eq_mul_prod_compl h]
  simp only [if_true]
  have hrest : ∏ r ∈ ({h}ᶜ : Finset (Fin m)), ∏ c : κ,
      (if r = h then A else (1 : M2)) (x (r, c)) (y (r, c)) =
      if ∀ h', h' ≠ h → ∀ j, x (h', j) = y (h', j) then 1 else 0 := by
    have : ∀ r ∈ ({h}ᶜ : Finset (Fin m)), ∏ c : κ,
        (if r = h then A else (1 : M2)) (x (r, c)) (y (r, c)) =
        if ∀ j, x (r, j) = y (r, j) then 1 else 0 := by
      intro r hr
      rw [Finset.mem_compl, Finset.mem_singleton] at hr
      simp only [hr, if_false, one_apply]
      rw [Finset.prod_boole]; simp
    rw [Finset.prod_congr rfl this, Finset.prod_boole]
    simp [Finset.mem_compl]
  rw [hrest]
  split_ifs <;> simp

end Sem

/-! ## Denotations -/

section Den

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

namespace HStep

/-- The matrix of a step; `ch S` is what a forward child call computes on the slots `S` (as an
operator on the whole role array). Local steps are the `RStep` matrices. -/
noncomputable def den (ch : Finset (Fin m) → Op (Fin m × κ)) : HStep R m → ROp R m κ
  | gate G => (RStep.gate G : RStep R m).den (1 : Op κ)
  | rowAdd w i j hij => (RStep.rowAdd w i j hij : RStep R m).den (1 : Op κ)
  | phase w k₀ k₁ a => (RStep.phase w k₀ k₁ a : RStep R m).den (1 : Op κ)
  | perm σ => (RStep.perm σ : RStep R m).den (1 : Op κ)
  | child w S neg => wireOp w (signedOp ch S neg)

end HStep

/-- Denotation of a step list (first step applied first). -/
noncomputable def denListH (ch : Finset (Fin m) → Op (Fin m × κ)) (l : List (HStep R m)) :
    ROp R m κ :=
  l.foldl (fun acc st => st.den ch * acc) 1

lemma foldl_denH_mul (ch : Finset (Fin m) → Op (Fin m × κ)) (l : List (HStep R m))
    (A : ROp R m κ) : l.foldl (fun acc st => st.den ch * acc) A = denListH ch l * A := by
  induction l generalizing A with
  | nil => simp [denListH]
  | cons s l ih =>
    simp only [denListH, List.foldl_cons]
    rw [ih, ih (s.den ch * 1), mul_one, mul_assoc]

@[simp] lemma denListH_nil (ch : Finset (Fin m) → Op (Fin m × κ)) :
    denListH ch ([] : List (HStep R m)) = 1 := rfl

lemma denListH_cons (ch : Finset (Fin m) → Op (Fin m × κ)) (s : HStep R m) (l : List (HStep R m)) :
    denListH ch (s :: l) = denListH ch l * s.den ch := by
  simp only [denListH, List.foldl_cons]
  rw [foldl_denH_mul, mul_one]; rfl

lemma denListH_single (ch : Finset (Fin m) → Op (Fin m × κ)) (s : HStep R m) :
    denListH ch [s] = s.den ch := by
  rw [denListH_cons, denListH_nil, one_mul]

lemma denListH_append (ch : Finset (Fin m) → Op (Fin m × κ)) (l₁ l₂ : List (HStep R m)) :
    denListH ch (l₁ ++ l₂) = denListH ch l₂ * denListH ch l₁ := by
  simp only [denListH, List.foldl_append]
  exact foldl_denH_mul _ _ _

end Den

/-! ## The interface -/

/-- **Clean-temporary correctness**: the data-to-data block of `N` is `C^{⊗}` on every data role
(temporaries enter as zero and their outputs are discarded). -/
def DataCorrect {W T m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ] (N : ROp (Fin W ⊕ Fin T) m κ) :
    Prop :=
  ∀ (w w' : Fin W) (x y : Addr m κ),
    N (Sum.inl w, x) (Sum.inl w', y) = if w = w' then (tens Cm : Op (Fin m × κ)) x y else 0

/-- **Round-six complex network interface** (design decision 2): one `κ`-independent program on
`W` data/scratch roles and `T` temporaries, whose child calls act on slot sets of width `< m`
with child-width multiset `histMS h`, computing `C^{⊗(Fin m × κ)}` on every data/scratch role
when the temporaries start at zero (their outputs are discarded), for every column type `κ`. -/
structure Prop8IfaceH (W T m : ℕ) (h : List (ℕ × ℕ)) where
  net : List (HStep (Fin W ⊕ Fin T) m)
  small : ∀ w ∈ net.filterMap HStep.width, w < m
  hist : ((net.filterMap HStep.width : List ℕ) : Multiset ℕ) = histMS h
  correct : ∀ (κ : Type) [Fintype κ] [DecidableEq κ],
    DataCorrect (W := W) (T := T) (denListH (chEx (κ := κ)) net)

namespace Prop8IfaceH

variable {W T m : ℕ} {h : List (ℕ × ℕ)}

/-- Child widths (in program order). -/
def widths (J : Prop8IfaceH W T m h) : List ℕ := J.net.filterMap HStep.width

end Prop8IfaceH

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxRec
/-!
# R2: the recursive C-layer through a `Prop8IfaceH` network on any number of axes

`recOpH J e : Op (Fin e)` computes `C^{⊗e}` on `e` selected bits:

* if `0 < m ≤ e`: write `e = m f + r` (`f = e / m`, `r = e % m`) and split the axes as
  `Fin e ≃ (Fin m × Fin f) ⊕ Fin r` (`axSplit`). On the first block run one invocation of the
  network `J` with columns `Fin f`; a child `child w S neg` runs `recOpH J (|S| f)` on the bits
  `S × Fin f` (embedded through `Fin (|S| f) ≃ S × Fin f`), which is a strictly smaller
  instance since `|S| < m`. The parent result is read off the data role `inl 0`. The `r`
  leftover axes get their individual kernels (25) (`leafOp`).
* otherwise (`e < m`): the individual kernels (`leafOp e`).

`recOpH_eq`: `recOpH J e = tens Cm` for every `e` (strong induction on `e`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

/-! ## Reindexing and sum-type tensor products -/

section Reindex

variable {α β ι : Type} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq α] [DecidableEq β]
  [DecidableEq ι]

/-- Transport an operator along a bijection of selected bits. -/
def reindexOp (φ : ι ≃ α) (X : Op α) : Op ι := fun x y => X (x ∘ φ.symm) (y ∘ φ.symm)

/-- Tensor product of operators on disjoint bit sets `α ⊕ β`. -/
def opSum (A : Op α) (B : Op β) : Op (α ⊕ β) := fun x y =>
  A (x ∘ Sum.inl) (y ∘ Sum.inl) * B (x ∘ Sum.inr) (y ∘ Sum.inr)

end Reindex

/-- `Fin (m f + r)`-axes split: `Fin e ≃ (Fin m × Fin (e / m)) ⊕ Fin (e % m)`. -/
def axSplit (m e : ℕ) : Fin e ≃ (Fin m × Fin (e / m)) ⊕ Fin (e % m) :=
  (finCongr (Nat.div_add_mod e m).symm).trans
    (finSumFinEquiv.symm.trans (Equiv.sumCongr finProdFinEquiv.symm (Equiv.refl _)))

/-- `S × β ≃ S ×ˢ univ`. -/
def prodSub {α : Type} (S : Finset α) (β : Type) [Fintype β] :
    ↥S × β ≃ ↥(S ×ˢ (univ : Finset β)) where
  toFun x := ⟨(x.1.1, x.2), Finset.mem_product.2 ⟨x.1.2, mem_univ _⟩⟩
  invFun y := (⟨y.1.1, (Finset.mem_product.1 y.2).1⟩, y.1.2)
  left_inv x := rfl
  right_inv y := rfl

/-- The bits of a child of width `|S|` on `f` columns. -/
noncomputable def childEqv {m : ℕ} (S : Finset (Fin m)) (f : ℕ) :
    Fin (S.card * f) ≃ ↥(S ×ˢ (univ : Finset (Fin f))) :=
  finProdFinEquiv.symm.trans ((Equiv.prodCongr S.equivFin.symm (Equiv.refl _)).trans (prodSub S _))

/-- One role's block of a role operator. -/
def blk {R : Type} {m : ℕ} {κ : Type} (N : ROp R m κ) (w : R) : Op (Fin m × κ) :=
  fun x y => N (w, x) (w, y)

/-! ## The recursion -/

variable {W T m : ℕ} {h : List (ℕ × ℕ)} [NeZero W]

lemma child_lt {m e : ℕ} (hme : 0 < m ∧ m ≤ e) {c : ℕ} (hc : c < m) : c * (e / m) < e := by
  have hf : 0 < e / m := Nat.div_pos hme.2 hme.1
  calc c * (e / m) < m * (e / m) := Nat.mul_lt_mul_of_pos_right hc hf
    _ ≤ e := Nat.mul_div_le e m

/-- **The recursive C-layer** on `e` axes through the network `J`. -/
noncomputable def recOpH (J : Prop8IfaceH W T m h) (e : ℕ) : Op (Fin e) :=
  if hme : 0 < m ∧ m ≤ e then
    reindexOp (axSplit m e)
      (opSum
        (blk (denListH (fun S : Finset (Fin m) =>
            if hS : S.card < m then
              embed (S ×ˢ univ) (childEqv S (e / m)) (recOpH J (S.card * (e / m)))
            else embed (S ×ˢ univ) (childEqv S (e / m)) (leafOp (S.card * (e / m)))) J.net)
          (Sum.inl 0))
        (leafOp (e % m)))
  else leafOp e
termination_by e
decreasing_by exact child_lt hme hS

/-- The child operator used at a node. -/
noncomputable def chRec (J : Prop8IfaceH W T m h) (e : ℕ) (S : Finset (Fin m)) :
    Op (Fin m × Fin (e / m)) :=
  if S.card < m then embed (S ×ˢ univ) (childEqv S (e / m)) (recOpH J (S.card * (e / m)))
  else embed (S ×ˢ univ) (childEqv S (e / m)) (leafOp (S.card * (e / m)))

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxCost
/-!
# R2: cost of the recursive C-layer through a `Prop8IfaceH` network (moment recurrence)

Cost model (§5.3, as `Butterfly.recCost`, now on any number of axes `e = m f + r`): a node on
`e ≥ m` axes and data volume `V` costs `Lloc · V` for the local steps of one network invocation
(`locWork_le_vol`: `Lloc = nloc (W+T)²/W` bounds the actual entry operations), `r · V` for the
`r = e mod m` leftover individual kernels, and one recursive call on `|S| f` axes and volume
`V / W` per child; a leaf (`e < m`) costs `e · V` (individual kernels).

* `recCostH_lin`: `recCostH e V = V · recCostH e 1`.
* `recCostH_unit_node`: the per-volume recurrence `c(e) = Lloc + r + (1/W) ∑_w n_w c(w f)`.
* **`recCostH_le`**: if `∑_w n_w (w/m)^σ < W` (`histMoment h m σ < W`), then
  `recCostH e V ≤ K · V · e^σ` for all `e, V ≥ 0` (via `moment_recurrence_bound` applied to the
  running maximum of `c`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

variable {W T m : ℕ} {h : List (ℕ × ℕ)} [NeZero W]

/-- The cost of `recOpH J e` on data volume `V`. -/
noncomputable def recCostH (J : Prop8IfaceH W T m h) (Lloc : ℝ) (e : ℕ) (V : ℝ) : ℝ :=
  if hme : 0 < m ∧ m ≤ e then
    Lloc * V + ((e % m : ℕ) : ℝ) * V +
      (J.widths.attach.map fun w => recCostH J Lloc (w.1 * (e / m)) (V / W)).sum
  else (e : ℝ) * V
termination_by e
decreasing_by exact child_lt hme (J.small w.1 w.2)

/-! ## The local work of one invocation -/

section Local

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

/-- Local steps as restricted steps. -/
def HStep.locR : HStep R m → Option (RStep R m)
  | .gate G => some (.gate G)
  | .rowAdd w i j hij => some (.rowAdd w i j hij)
  | .phase w k₀ k₁ a => some (.phase w k₀ k₁ a)
  | .perm σ => some (.perm σ)
  | .child .. => none

end Local

/-- Entry operations of the local steps of one invocation. -/
noncomputable def Prop8IfaceH.locWork (J : Prop8IfaceH W T m h) (κ : Type) [Fintype κ]
    [DecidableEq κ] : ℕ :=
  ((J.net.filterMap HStep.locR).map fun r => r.work (1 : Op κ)).sum

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6CxMerge
/-!
# NC3: the PR #15 whole-residual merge

For a linearly independent family `v₁, …, v_ρ` in `𝔽₂^m` (e.g. an orthonormal residual basis of
a Proposition 8 edge) and signs `ε_k = ±1`, the edge operator
`∏_k (aI + bX_{v_k})^{ε_k}` (on every column: `colT (∏ Tk ε_k v_k)`) is conjugate, by a word of
binary row additions `P` (an element of `GL_m(𝔽₂)` sending `v_k ↦ e_{h_k}`), to
`(-i)^{|N||κ|} Z_N C^{⊗(S × κ)} Z_N` with `S = {h_k}` (`|S| = ρ`) and `N = {h_k : ε_k = -1}`:
**one** forward child call of width `ρ`.

* `conj_rowAdds`: conjugation of a kernel product by row additions (15).
* `kernels_single`: kernels on distinct unit vectors `e_{h_k}` = the slot family (they live on
  distinct slots and commute).
* `exists_rowAdds`: every independent family is sent to distinct unit vectors by a word of row
  additions (basis extension + `gl_f2_row_additions`).
* **`merge_identity`** (operator form) and **`merge_chunk`** (step form: row additions, one
  child `child w S neg`, row additions reversed).
* `mergedChunk`, `mergedChunk_den`, `mergedChunk_widths`: the chosen chunk for a kernel list
  `L` (in `P8Lift.frameSteps` form) with independent vectors; `mergedChunk_den_frameSteps`:
  same denotation as the single-slot chunks `frameSteps w L`, but child widths `[|L|]`
  instead of `|L|` ones. Orthonormal version `lin_indep_of_orthonormal`.
* `edgeStepsH`: the merged frame change of a Proposition 8 edge (`EdgeP`): denotation
  `wireOp w (PhiK (qL V - qL U))` as `P8Lift.edgeSteps`, one child of width `Fd V U`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

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

/-! ## Row-addition words -/

/-- One row addition `z_j += z_i` (identity if `i = j`) on a single column. -/
def raS (p : Fin m × Fin m) (z : Fin m → ZMod 2) : Fin m → ZMod 2 :=
  if p.1 = p.2 then z else ra p.1 p.2 z

/-- A word of row additions on a single column (first letter applied first). -/
def raL (js : List (Fin m × Fin m)) (z : Fin m → ZMod 2) : Fin m → ZMod 2 :=
  js.foldl (fun z p => raS p z) z

lemma raS_invol (p : Fin m × Fin m) (z : Fin m → ZMod 2) : raS p (raS p z) = z := by
  unfold raS; split_ifs with h
  · rfl
  · exact ra_invol h z

/-- The address permutation of one letter. -/
def PmS (p : Fin m × Fin m) : Op (Fin m × κ) := if p.1 = p.2 then 1 else Pm p.1 p.2

/-- The address permutation of a word (first letter applied first). -/
def PL : List (Fin m × Fin m) → Op (Fin m × κ)
  | [] => 1
  | p :: js => PL js * PmS p

lemma PL_append (js js' : List (Fin m × Fin m)) :
    (PL (js ++ js') : Op (Fin m × κ)) = PL js' * PL js := by
  induction js with
  | nil => simp [PL]
  | cons p js ih => simp only [List.cons_append, PL, ih, mul_assoc]

lemma Pm_mul_Pm {i j : Fin m} (hij : i ≠ j) : (Pm i j * Pm i j : Op (Fin m × κ)) = 1 := by
  have := Pm_conj (κ := κ) hij 1
  rw [mul_one] at this
  rw [this]
  ext x z
  simp only [one_apply]
  have : rowAddr i j x = rowAddr i j z ↔ x = z :=
    ⟨fun h => by rw [← rowAddr_invol hij x, h, rowAddr_invol hij], fun h => h ▸ rfl⟩
  simp only [this]

lemma PmS_mul_PmS (p : Fin m × Fin m) : (PmS p * PmS p : Op (Fin m × κ)) = 1 := by
  unfold PmS; split_ifs with h
  · simp
  · exact Pm_mul_Pm h

/-- Conjugating a kernel product by one letter. -/
lemma PmS_conj_prod {ι : Type*} (p : Fin m × Fin m) (ks : List ι) (ε : ι → ℤ)
    (v : ι → Fin m → ZMod 2) :
    PmS p * (colT ((ks.map fun k => Tk (ε k) (v k)).prod) : Op (Fin m × κ)) * PmS p =
      colT ((ks.map fun k => Tk (ε k) (raS p (v k))).prod) := by
  induction ks with
  | nil => simp [colT_one, PmS_mul_PmS]
  | cons k ks ih =>
    simp only [List.map_cons, List.prod_cons, colT_mul]
    have e : ∀ A B : Op (Fin m × κ), PmS p * (A * B) * PmS p =
        (PmS p * A * PmS p) * (PmS p * B * PmS p) := by
      intro A B
      calc PmS p * (A * B) * PmS p = PmS p * A * (PmS p * PmS p) * B * PmS p := by
            rw [PmS_mul_PmS, mul_one]; simp only [mul_assoc]
        _ = _ := by simp only [mul_assoc]
    rw [e, ih]
    congr 1
    unfold PmS raS
    split_ifs with h
    · simp
    · exact colT_Tk_rowAdd h _ _

/-- **Conjugation by a row-addition word** (15): `P⁻¹ · K(P v) · P = K(v)`. -/
theorem conj_rowAdds {ι : Type*} (ks : List ι) (ε : ι → ℤ) :
    ∀ (js : List (Fin m × Fin m)) (v : ι → Fin m → ZMod 2),
      (PL js.reverse * colT ((ks.map fun k => Tk (ε k) (raL js (v k))).prod) * PL js :
        Op (Fin m × κ)) = colT ((ks.map fun k => Tk (ε k) (v k)).prod) := by
  intro js
  induction js with
  | nil => intro v; simp [PL, raL]
  | cons p js ih =>
    intro v
    have h1 := ih fun k => raS p (v k)
    have e : ∀ k, raL (p :: js) (v k) = raL js (raS p (v k)) := fun k => rfl
    simp only [e, List.reverse_cons, PL_append, PL]
    calc (PL [] * PmS p * PL js.reverse *
          colT ((ks.map fun k => Tk (ε k) (raL js (raS p (v k)))).prod) * (PL js * PmS p) :
          Op (Fin m × κ))
        = PmS p * (PL js.reverse *
          colT ((ks.map fun k => Tk (ε k) (raL js (raS p (v k)))).prod) * PL js) * PmS p := by
          simp only [PL, one_mul, mul_assoc]
      _ = _ := by rw [h1, PmS_conj_prod]; simp only [raS_invol]

/-! ## Kernels on distinct unit vectors -/

/-- `C` for `ε = 1`, `C⁻¹` otherwise. -/
noncomputable def Mε (e : ℤ) : M2 := if e = 1 then Cm else Cinv

lemma colT_Tk_unit (e : ℤ) (he : e = 1 ∨ e = -1) (h : Fin m) :
    (colT (Tk e (Pi.single h 1)) : Op (Fin m × κ)) =
      tensF (fun p : Fin m × κ => if p.1 = h then Mε e else 1) := by
  rcases he with rfl | rfl
  · rw [colT_Tk_single_pos, slotOp_tens]; simp [Mε]
  · rw [colT_Tk_single_neg, slotOp_tens]; simp [Mε]

/-- **Distinct-slot kernels multiply to the slot family.** -/
theorem kernels_single {ι : Type*} (ks : List ι) (ε : ι → ℤ) (hε : ∀ k ∈ ks, ε k = 1 ∨ ε k = -1)
    (hh : ι → Fin m) (hnd : (ks.map hh).Nodup) :
    (colT ((ks.map fun k => Tk (ε k) (Pi.single (hh k) 1)).prod) : Op (Fin m × κ)) =
      tensF (slotFam (κ := κ) (ks.map hh).toFinset ((ks.filter fun k => ε k ≠ 1).map hh).toFinset) := by
  induction ks with
  | nil =>
    simp only [List.map_nil, List.prod_nil, colT_one]
    rw [← tensF_one]; congr 1
  | cons k ks ih =>
    rw [List.map_cons, List.nodup_cons] at hnd
    simp only [List.map_cons, List.prod_cons, colT_mul]
    rw [ih (fun k' hk' => hε k' (List.mem_cons_of_mem _ hk')) hnd.2,
      colT_Tk_unit _ (hε k List.mem_cons_self), ← tensF_mul]
    congr 1; funext p
    have hnot : hh k ∉ ks.map hh := hnd.1
    have hnot' : hh k ∉ (ks.filter fun k => ε k ≠ 1).map hh := fun h' =>
      hnot (List.map_subset _ (List.filter_subset_self ks) h')
    by_cases hp : p.1 = hh k
    · have hrest : slotFam (κ := κ) (ks.map hh).toFinset ((ks.filter fun k => ε k ≠ 1).map hh).toFinset p
          = 1 := by
        simp only [slotFam, hp, List.mem_toFinset, hnot, if_false]
      rw [hrest, mul_one]
      simp only [slotFam, hp, if_true]
      rw [if_pos (by simp)]
      by_cases he : ε k = 1
      · have e2 : hh k ∉ (((k :: ks).filter fun k => ε k ≠ 1).map hh).toFinset := by
          rw [List.filter_cons]; simpa [he] using hnot'
        rw [if_neg e2]; simp [Mε, he]
      · have e2 : hh k ∈ (((k :: ks).filter fun k => ε k ≠ 1).map hh).toFinset := by
          rw [List.filter_cons]; simp [he]
        rw [if_pos e2]; simp [Mε, he]
    · have e1 : (p.1 ∈ ((k :: ks).map hh).toFinset) ↔ p.1 ∈ (ks.map hh).toFinset := by
        simp [hp]
      have e2 : (p.1 ∈ (((k :: ks).filter fun k => ε k ≠ 1).map hh).toFinset) ↔
          p.1 ∈ ((ks.filter fun k => ε k ≠ 1).map hh).toFinset := by
        rw [List.filter_cons]; split_ifs <;> simp [hp]
      have e1' : p.1 ∈ (hh k :: ks.map hh).toFinset ↔ p.1 ∈ (ks.map hh).toFinset := by simp [hp]
      simp only [slotFam, e1, e2, if_neg hp, one_mul]
      simp only [e1']

/-! ## Existence of the row-addition word -/

lemma transvection_mulVec (i j : Fin m) (y : Fin m → ZMod 2) :
    transvection i j (1 : ZMod 2) *ᵥ y = ra j i y := by
  funext r
  simp [transvection, Matrix.single, mulVec, dotProduct, add_mul, Finset.sum_add_distrib,
    Matrix.one_apply, ra]
  by_cases h : r = i
  · subst h; simp
  · have h' : i ≠ r := Ne.symm h
    simp [h, h']

lemma raL_transvections (L : List (Fin m × Fin m)) (hL : ∀ p ∈ L, p.1 ≠ p.2)
    (z : Fin m → ZMod 2) :
    raL (L.reverse.map fun p => (p.2, p.1)) z =
      (L.map fun p => transvection p.1 p.2 (1 : ZMod 2)).prod *ᵥ z := by
  induction L with
  | nil => simp [raL]
  | cons p L ih =>
    have e : raL ((p :: L).reverse.map fun p => (p.2, p.1)) z =
        raS (p.2, p.1) (raL (L.reverse.map fun p => (p.2, p.1)) z) := by
      simp [raL, List.foldl_append]
    rw [e, ih fun q hq => hL q (List.mem_cons_of_mem _ hq), List.map_cons, List.prod_cons,
      ← mulVec_mulVec, raS, if_neg (Ne.symm (hL p List.mem_cons_self)), transvection_mulVec]

/-- **Every independent family is sent to distinct unit vectors by a row-addition word.** -/
theorem exists_rowAdds {n : ℕ} (v : Fin n → Fin m → ZMod 2) (hv : LinearIndependent (ZMod 2) v) :
    ∃ (js : List (Fin m × Fin m)) (hh : Fin n → Fin m), Function.Injective hh ∧
      ∀ k, raL js (v k) = Pi.single (hh k) 1 := by
  classical
  let b := Module.Basis.sumExtend hv
  have hb : ∀ k, b (Sum.inl k) = v k := by
    intro k
    simp only [b, Module.Basis.sumExtend, Module.Basis.reindex_apply]
    rw [Module.Basis.extend_apply_self]
    rfl
  letI : Fintype (Module.Basis.sumExtendIndex hv) := Fintype.ofFinite _
  have hcard : Fintype.card (Fin n ⊕ Module.Basis.sumExtendIndex hv) = m := by
    rw [← Module.finrank_eq_card_basis b, Module.finrank_fin_fun]
  let e := Fintype.equivFinOfCardEq hcard
  let b' := b.reindex e
  have hb' : ∀ k, b' (e (Sum.inl k)) = v k := by
    intro k; simp [b', hb]
  let A := b'.equivFun
  let M := LinearMap.toMatrix' A.toLinearMap
  have hM : ∀ z, M *ᵥ z = A z := fun z => LinearMap.toMatrix'_mulVec _ z
  have hdet : M.det ≠ 0 := by
    have h1 : M * LinearMap.toMatrix' A.symm.toLinearMap = 1 := by
      rw [← LinearMap.toMatrix'_comp]
      have : A.toLinearMap ∘ₗ A.symm.toLinearMap = LinearMap.id := by
        ext; simp
      rw [this, LinearMap.toMatrix'_id]
    intro h0
    have := congrArg Matrix.det h1
    rw [det_mul, h0, zero_mul, det_one] at this
    exact zero_ne_one this
  obtain ⟨L, hL, hML⟩ := gl_f2_row_additions M hdet
  refine ⟨L.reverse.map fun p => (p.2, p.1), fun k => e (Sum.inl k),
    fun k k' hk => Sum.inl_injective (e.injective hk), fun k => ?_⟩
  rw [raL_transvections L hL, ← hML, hM, ← hb']
  funext r
  rw [Module.Basis.equivFun_self, Pi.single_apply]
  by_cases hr : r = e (Sum.inl k)
  · simp [hr]
  · rw [if_neg (Ne.symm hr), if_neg hr]

/-! ## The merge identity -/

/-- The slot set `{h_k}` and sign set `{h_k : ε_k ≠ 1}` of a merged child. -/
def mSlots {n : ℕ} (hh : Fin n → Fin m) : Finset (Fin m) := ((List.finRange n).map hh).toFinset

def mNeg {n : ℕ} (ε : Fin n → ℤ) (hh : Fin n → Fin m) : Finset (Fin m) :=
  (((List.finRange n).filter fun k => ε k ≠ 1).map hh).toFinset

lemma card_mSlots {n : ℕ} {hh : Fin n → Fin m} (hinj : Function.Injective hh) :
    (mSlots hh).card = n := by
  rw [mSlots, List.toFinset_card_of_nodup ((List.nodup_finRange n).map hinj), List.length_map,
    List.length_finRange]

lemma mNeg_subset {n : ℕ} (ε : Fin n → ℤ) (hh : Fin n → Fin m) : mNeg ε hh ⊆ mSlots hh := by
  intro x hx
  simp only [mNeg, mSlots, List.mem_toFinset, List.mem_map] at hx ⊢
  obtain ⟨k, _, rfl⟩ := hx
  exact ⟨k, List.mem_finRange k, rfl⟩

/-- **PR #15 whole-residual merge (operator form).** For independent `v_k` and signs `±1` there
is a row-addition word `P` and slots `S` (`|S| = n`), `N ⊆ S`, such that for every number of
columns `∏_k (aI + bX_{v_k})^{ε_k} = P⁻¹ ((-i)^{|N||κ|} Z_N C^{⊗(S×κ)} Z_N) P`. -/
theorem merge_identity {n : ℕ} (ε : Fin n → ℤ) (hε : ∀ k, ε k = 1 ∨ ε k = -1)
    (v : Fin n → Fin m → ZMod 2) (hv : LinearIndependent (ZMod 2) v) :
    ∃ (js : List (Fin m × Fin m)) (S neg : Finset (Fin m)), S.card = n ∧ neg ⊆ S ∧
      ∀ (κ : Type) [Fintype κ] [DecidableEq κ],
        (PL js.reverse * signedOp (chEx (κ := κ)) S neg * PL js : Op (Fin m × κ)) =
          colT (((List.finRange n).map fun k => Tk (ε k) (v k)).prod) := by
  obtain ⟨js, hh, hinj, hjs⟩ := exists_rowAdds v hv
  refine ⟨js, mSlots hh, mNeg ε hh, card_mSlots hinj, mNeg_subset ε hh, fun κ _ _ => ?_⟩
  rw [signedOp_chEx, ← conj_rowAdds (List.finRange n) ε js v]
  simp only [hjs]
  rw [kernels_single _ ε (fun k _ => hε k) hh ((List.nodup_finRange n).map hinj)]
  rfl

/-! ## Step form -/

section Steps

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

/-- The row additions of a word, on wire `w`. -/
def rowAddsL (w : R) (js : List (Fin m × Fin m)) : List (HStep R m) :=
  js.flatMap fun p => if hij : p.1 = p.2 then [] else [HStep.rowAdd w p.1 p.2 hij]

lemma den_rowAddsL (ch : Finset (Fin m) → Op (Fin m × κ)) (w : R) :
    ∀ js : List (Fin m × Fin m), denListH ch (rowAddsL w js) = wireOp w (PL js)
  | [] => by simp [rowAddsL, PL, wireOp_one]
  | p :: js => by
    rw [rowAddsL, List.flatMap_cons, denListH_append, ← rowAddsL, den_rowAddsL ch w js, PL,
      ← wireOp_mul]
    congr 1
    unfold PmS
    split_ifs with h
    · simp [wireOp_one]
    · rw [denListH_single]
      exact den_rowAdd (1 : Op κ) w p.1 p.2 h

lemma widths_rowAddsL (w : R) (js : List (Fin m × Fin m)) :
    (rowAddsL w js).filterMap HStep.width = [] := by
  induction js with
  | nil => rfl
  | cons p js ih =>
    rw [rowAddsL, List.flatMap_cons, List.filterMap_append, ← rowAddsL, ih]
    split_ifs <;> rfl

/-- The merged chunk: row additions, one child of width `|S|`, row additions undone. -/
def chunkH (w : R) (js : List (Fin m × Fin m)) (S neg : Finset (Fin m)) : List (HStep R m) :=
  rowAddsL w js ++ [HStep.child w S neg] ++ rowAddsL w js.reverse

lemma widths_chunkH (w : R) (js : List (Fin m × Fin m)) (S neg : Finset (Fin m)) :
    (chunkH w js S neg).filterMap HStep.width = [S.card] := by
  simp [chunkH, List.filterMap_append, widths_rowAddsL, HStep.width]

lemma den_chunkH (w : R) (js : List (Fin m × Fin m)) (S neg : Finset (Fin m)) :
    denListH (chEx (κ := κ)) (chunkH w js S neg) =
      wireOp w (PL js.reverse * signedOp (chEx (κ := κ)) S neg * PL js) := by
  rw [chunkH, denListH_append, denListH_append, den_rowAddsL, den_rowAddsL, denListH_single,
    HStep.den, wireOp_mul, wireOp_mul, mul_assoc]

/-- **PR #15 merge (step form).** The edge operator `∏_k (aI+bX_{v_k})^{ε_k}` on wire `w` is
computed by one chunk with a single child call of width `n`. -/
theorem merge_chunk (w : R) {n : ℕ} (ε : Fin n → ℤ) (hε : ∀ k, ε k = 1 ∨ ε k = -1)
    (v : Fin n → Fin m → ZMod 2) (hv : LinearIndependent (ZMod 2) v) :
    ∃ c : List (HStep R m), c.filterMap HStep.width = [n] ∧
      ∀ (κ : Type) [Fintype κ] [DecidableEq κ], denListH (chEx (κ := κ)) c =
        wireOp w (colT (((List.finRange n).map fun k => Tk (ε k) (v k)).prod)) := by
  obtain ⟨js, S, neg, hS, -, h⟩ := merge_identity ε hε v hv
  exact ⟨chunkH w js S neg, by rw [widths_chunkH, hS], fun κ _ _ => by rw [den_chunkH, h κ]⟩

/-- Linear independence of the vectors of a kernel list `L` (indexed by position). -/
def LIndep (L : List (ℤ × (Fin m → ZMod 2))) : Prop :=
  LinearIndependent (ZMod 2) fun k : Fin L.length => (L.get k).2

/-- The merged chunk chosen for a kernel list (empty for `L = []`). -/
noncomputable def mergedChunk (w : R) (L : List (ℤ × (Fin m → ZMod 2))) : List (HStep R m) := by
  classical
  exact if hL : L ≠ [] ∧ (∀ p ∈ L, p.1 = 1 ∨ p.1 = -1) ∧ LIndep L then
    Classical.choose (merge_chunk w (fun k => (L.get k).1)
      (fun k => hL.2.1 _ (List.get_mem L k)) _ hL.2.2)
  else []

end Steps

/-! ## Merged Proposition 8 edges -/

section Edge

open NetComplexP8 NetComplexLabels

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

/-- A kernel list for the edge `U → V` coming from an orthonormal residual basis. -/
def KerSpecH (V U : Submodule (ZMod 2) (Vc h)) (L : List (ℤ × Vc h)) : Prop :=
  KerSpec V U L ∧ ∃ B : Finset (Vc h), NetComplexOrtho.Orthonormal2 B ∧ L.map Prod.snd = B.toList

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

/-- The merged frame change of an edge `U → V` on wire `w`. -/
noncomputable def edgeStepsH (w : R) (V U : Submodule (ZMod 2) (Vc h)) : List (HStep R (h ^ 3)) :=
  mergedChunk w (kersH V U)

end Edge

end IntMul.Kappa.R6.Cx

end