κ-improvement development, part 23: item-language primitives

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

import Definitions.Def_IntMul_Kappa_K_Defs22
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_SApprox

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.AModelRuns
/-!
# Array model, Stage 2: runs of pivots as single interchanges of merged fields

Builds on `Solutions/AModel.lean` (whose definitions are unchanged).

* §1 Reshape (`mergeShape`, `mergeAddr`, `splitAddr`): merging adjacent fields is free —
  `pull_merge`, `pull_split`, general `pull_reshape`.
* §2 Block swap (`blockSwap`): it is the composition of the single position swaps
  (`chain_runPairs`), and after merging both runs it is one swap of two merged fields
  (`merge2_blockSwap`, `pull_blockSwap`).
* §3 A run of `r` consecutive pivots on contiguous active fields acts on arrays as that block swap
  (`runArr_pivotRun`), hence as one merged-field interchange (`runArr_pivotRun_merged`).
* §4 A pivot list splits into `numRuns` maximal runs (`groupRuns`, `flatMap_groupRuns`), and
  `runArr` over its swaps is the composition of one merged-field swap per run
  (`runArr_swapSteps_runs`).
-/

namespace AModel

/-! ## 1. Reshape -/

section Reshape

end Reshape

/-! ## 2. Block swaps -/

section BlockSwap

@[simp] lemma length_permIdx (f : ℕ → ℕ) (a : List ℕ) : (permIdx f a).length = a.length := by
  simp [permIdx]

/-! ### Segments of a block-swapped address -/

section Segments
variable {i j r : ℕ} {a : List ℕ} (hij : i + r ≤ j) (hj : j + r ≤ a.length)
include hij hj

end Segments

/-! ### Merging both runs -/

end BlockSwap

/-! ## 3. A run of consecutive pivots is one merged-field interchange -/

section PivotRun

variable {sh : Shape} {n Q : ℕ} (Λ : Layout sh n Q)

variable [NeZero Q]

end PivotRun

/-! ## 4. Counting runs -/

section Runs

variable {sh : Shape} {n Q : ℕ} (Λ : Layout sh n Q) [NeZero Q]

end Runs

end AModel

end

section
-- Source module: Solutions.KIL6Den
/-!
# KIL6: Lemma 12 as a uniform IL program — the list denotations

The IL program of KIL6 realises the Lemma 12 interchange with the following data flow (array
model, `AModelL12`):

1. **binary padding** `binShape … (2^u) → binShape … (q^e)`: two one-field paddings
   (`padL`, `embed_binShape`);
2. **high swaps**: `r = min ρ e` single-digit interchanges (`highSwaps`);
3. if `n = e - r > 0`, the **middle part** `l12mid`: the row field is the prefix
   `Pre ++ [q]^r` (volume `vol Pre · q^r`), padded to `padRows W Kp (q^r)` rows (`padL`); the
   Prop. 11 oracle runs on the pieces (`runPieces … pieceLevels`), with the gap
   `G ++ [q]^r` (the already interchanged high digits of the second chunk belong to the gap);
   the padding is scanned away (`unpadL`);
4. **binary extraction** (two `unpadL`).

Compared with `AModelL12.l12q` this variant needs no joining rotation: the interchanged high
digits `d⁺` simply stay inside the gap.  `l12v_correct` proves that it is the interchange
`swapPos` of the two `[2^u]` fields, from the same oracle specification `OracleSpec`.

The list functions `padL` / `unpadL` are the one-field embeddings / extractions in the chunk
form the IL loops produce (`embed_eq_padL`, `extract_eq_unpadL`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open AModel AModelL12

section Chunks

variable {α : Type*}

theorem length_flatMap_range {f : ℕ → List α} {L : ℕ} :
    ∀ X : ℕ, (∀ x < X, (f x).length = L) → ((List.range X).flatMap f).length = X * L
  | 0, _ => by simp
  | X + 1, hf => by
    rw [List.range_succ, List.flatMap_append, List.length_append,
      length_flatMap_range X (fun x hx => hf x (by omega))]
    simp [hf X (by omega)]; ring

end Chunks

/-! ## One-field padding and extraction in chunk form -/

section Pad

variable {α : Type*}

/-! ## Composing embeddings and extractions -/

end Pad

/-! ## The binary and row paddings in chunk form -/

section Shapes

variable {α : Type*}

end Shapes

/-! ## The variant procedure and its correctness -/

section Variant

variable {α : Type*}

end Variant

/-! ## Auxiliary facts: pieces, digits, maps -/

section Aux

variable {α β : Type*}

end Aux

end NLogN.KIL

end

section
-- Source module: Solutions.KFNGate
/-!
# KFN: classification of the scalar gates of the complex network (task 1)

Every `RStep.gate G` of `P8Lift.complexIface.net` is one of the two kinds of fine IL gates of
KFG:

* a **dyadic atom gate** `G = gateMat W_c as` (`KFG.gateMat`: `1 + Σ_a (c_a/2^{h_a}) e_{t_a,s_a}`)
  for a list of atoms with `c_a ∈ {±1}`, `h_a ≤ 1`, every atom `Ok` and no target of the list a
  source of the list (`KFG.NoTS`), so `KFG.gate_iruns` applies; these are the side injections,
  scatters, copies and gathers of the schedule (2) of `NetComplexLemma5` and their inverses;
* the **sign gate** `fixG`, a diagonal `±1` matrix (one unit scaling `KFG.UAtom` with `u = -1`
  per physical `X` wire).

`GOK G`: `G = 1 + Σ_{x ∈ l} (ε_x / 2^{h_x}) e_{t_x, s_x}` with `ε_x = ±1`, `h_x ≤ 1`, targets
never sources.  `cxNamed_GOK`: every gate of `cxNamed` is `GOK`.  `GOK_atoms`: a `GOK` matrix
transported along `W ≃ Fin n` is `gateMat n as` for an `Ok`, `NoTS` atom list.
**`complexIface_gate_class`**: the classification of all gate steps of `complexIface`.
-/

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

namespace NLogN.KFN

open Matrix Finset Complex

section Generic

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

theorem eMat_apply (l : List (W × W × ℤ × ℕ)) (p q : W) :
    eMat l p q = (l.map fun x => if x.1 = p ∧ x.2.1 = q then (x.2.2.1 : ℂ) / 2 ^ x.2.2.2 else 0).sum := by
  induction l with
  | nil => simp [eMat]
  | cons x l ih =>
    simp only [eMat, List.map_cons, List.sum_cons, Matrix.add_apply] at ih ⊢
    rw [ih, single_apply]

/-- `egM` with dyadic coefficients and disjoint targets/sources is `GOK`. -/
theorem egM_GOK {ι : Type*} (A : Finset ι) (r c : ι → W) (k : ι → ℂ) (ε : ι → ℤ) (hh : ι → ℕ)
    (hk : ∀ x ∈ A, k x = (ε x : ℂ) / 2 ^ hh x) (hε : ∀ x ∈ A, ε x = 1 ∨ ε x = -1)
    (hh1 : ∀ x ∈ A, hh x ≤ 1) (hts : ∀ x ∈ A, ∀ y ∈ A, r x ≠ c y) :
    GOK (1 + NetComplex.egM A r c k) := by
  refine ⟨A.toList.map fun x => (r x, c x, ε x, hh x), ?_, ?_, ?_⟩
  · congr 1
    rw [NetComplex.egM, eMat, List.map_map, ← Finset.sum_map_toList A (fun x => single (r x) (c x) (k x))]
    congr 1
    refine List.map_congr_left fun x hx => ?_
    rw [Finset.mem_toList] at hx
    simp [hk x hx]
  · intro x hx y hy
    simp only [List.mem_map, Finset.mem_toList] at hx hy
    obtain ⟨a, ha, rfl⟩ := hx
    obtain ⟨b, hb, rfl⟩ := hy
    exact hts a ha b hb
  · intro x hx
    simp only [List.mem_map, Finset.mem_toList] at hx
    obtain ⟨a, ha, rfl⟩ := hx
    exact ⟨hε a ha, hh1 a ha⟩

/-- Inverting a gate (`1 - (G - 1)`) keeps `GOK`. -/
theorem GOK_inv {G : Matrix W W ℂ} (h : GOK G) : GOK (1 - (G - 1)) := by
  obtain ⟨l, rfl, hts, hc⟩ := h
  refine ⟨l.map fun x => (x.1, x.2.1, -x.2.2.1, x.2.2.2), ?_, ?_, ?_⟩
  · have : ∀ l : List (W × W × ℤ × ℕ),
        eMat (l.map fun x => (x.1, x.2.1, -x.2.2.1, x.2.2.2)) = -eMat l := by
      intro l
      induction l with
      | nil => simp [eMat]
      | cons x l ih =>
        simp only [eMat, List.map_cons, List.sum_cons] at ih ⊢
        rw [ih, neg_add, Int.cast_neg, neg_div, single_neg]
    rw [this]; abel
  · intro x hx y hy
    simp only [List.mem_map] at hx hy
    obtain ⟨a, ha, rfl⟩ := hx
    obtain ⟨b, hb, rfl⟩ := hy
    exact hts a ha b hb
  · intro x hx
    simp only [List.mem_map] at hx
    obtain ⟨a, ha, rfl⟩ := hx
    obtain ⟨h1, h2⟩ := hc a ha
    refine ⟨?_, h2⟩
    rcases h1 with e | e <;> simp [e]

/-- **A `GOK` gate is a KFG atom gate.** -/
theorem GOK_atoms {n : ℕ} (e : W ≃ Fin n) {G : Matrix W W ℂ} (h : GOK G) :
    ∃ as : List KFG.Atom, (∀ a ∈ as, a.Ok n ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
      (fun i j => G (e.symm i) (e.symm j)) = KFG.gateMat n as := by
  obtain ⟨l, rfl, hts, hc⟩ := h
  refine ⟨atomsOf e l, ?_, ?_, ?_⟩
  · intro a ha
    simp only [atomsOf, List.mem_map] at ha
    obtain ⟨x, hx, rfl⟩ := ha
    have hne : x.1 ≠ x.2.1 := hts x hx x hx
    refine ⟨⟨(e x.1).isLt, (e x.2.1).isLt, fun h' => hne (e.injective (Fin.ext h')), ?_⟩, (hc x hx).2⟩
    rcases (hc x hx).1 with h1 | h1 <;> simp [KFB.Sm, h1]
  · intro a ha b hb
    simp only [atomsOf, List.mem_map] at ha hb
    obtain ⟨x, hx, rfl⟩ := ha
    obtain ⟨y, hy, rfl⟩ := hb
    exact fun h' => hts x hx y hy (e.injective (Fin.ext h'))
  · funext i j
    simp only [KFG.gateMat, Matrix.add_apply, Matrix.one_apply, eMat_apply, atomsOf, List.map_map]
    congr 1
    · simp [e.symm.injective.eq_iff]
    · congr 1
      refine List.map_congr_left fun x _ => ?_
      simp only [Function.comp_apply]
      have e1 : (x.1 = e.symm i) ↔ ((e x.1).val = i.val) := by
        rw [Equiv.eq_symm_apply, Fin.val_inj]
      have e2 : (x.2.1 = e.symm j) ↔ ((e x.2.1).val = j.val) := by
        rw [Equiv.eq_symm_apply, Fin.val_inj]
      by_cases h1 : (e x.1).val = i.val <;> by_cases h2 : (e x.2.1).val = j.val <;>
        simp [h1, h2, e1, e2, KFB.toC]

end Generic

/-! ## The gates of the complex construction -/

section Complex

variable {h : ℕ} {T : Type*} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}
/-- The side coefficient `kD = -(|S ∩ T| - 1)/2` is `±1/2`. -/
theorem kD_eq (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) (n : NetComplex.Nb ind) :
    (NetComplex.kD ind n : ℂ) =
      ((if #(ind n.1.1 ∩ ind n.1.2) = 0 then (1 : ℤ) else -1 : ℤ) : ℂ) / 2 ^ 1 := by
  have hle := NetComplex.inter_le_two hcard hinj n.2.1
  have hev := n.2.2
  unfold NetComplex.kD
  rw [invOf_eq_inv]
  generalize #(ind n.1.1 ∩ ind n.1.2) = c at hle hev ⊢
  interval_cases c
  · norm_num
  · simp at hev
  · norm_num

theorem kS_eq (o : Option (Fin h)) :
    (NetComplex.kS o : ℂ) = ((match o with | none => (-1 : ℤ) | some _ => 1 : ℤ) : ℂ) / 2 ^ 1 := by
  cases o <;> simp [NetComplex.kS, invOf_eq_inv] <;> ring

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

theorem sideG_GOK (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) {I : NetComplex.Inv ind Wt} (hG : I.Good) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1)
    (S : T) : GOK (I.sideG ℂ (σ : ℂ) S).1 := by
  refine egM_GOK _ _ _ _ (fun n => σ * (if #(ind n.1.1 ∩ ind n.1.2) = 0 then (1 : ℤ) else -1))
    (fun _ => 1) (fun n _ => ?_) (fun n _ => ?_) (fun _ _ => le_rfl)
    (fun x _ y _ => hG.ts _ _)
  · rw [kD_eq hcard hinj]; push_cast; ring
  · split_ifs <;> rcases hσ with rfl | rfl <;> simp

theorem copyG_GOK {I : NetComplex.Inv ind Wt} (hG : I.Good) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1)
    (t : T) : GOK (I.copyG ℂ (σ : ℂ) t).1 :=
  egM_GOK _ _ _ _ (fun _ => σ) (fun _ => 0) (fun n _ => by simp)
    (fun _ _ => hσ) (fun _ _ => by norm_num) (fun x _ y _ => (hG.ss _ _).symm)

theorem scatG_GOK {I : NetComplex.Inv ind Wt} (hG : I.Good) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1) :
    GOK (I.scatG ℂ (σ : ℂ)).1 := by
  refine egM_GOK _ _ _ _ (fun q => σ * (match q.1 with | none => (-1 : ℤ) | some _ => 1))
    (fun _ => 1) (fun q _ => ?_) (fun q _ => ?_) (fun _ _ => le_rfl)
    (fun x _ y _ => hG.tc _ _)
  · rw [kS_eq]; push_cast; ring
  · rcases q with ⟨_ | _, _⟩ <;> rcases hσ with rfl | rfl <;> simp

theorem gathG_GOK {I : NetComplex.Inv ind Wt} (hG : I.Good) (σ : ℤ) (hσ : σ = 1 ∨ σ = -1) :
    GOK (I.gathG ℂ (σ : ℂ)).1 :=
  egM_GOK _ _ _ _ (fun _ => σ) (fun _ => 0) (fun n _ => by simp)
    (fun _ _ => hσ) (fun _ _ => by norm_num) (fun x _ y _ => (hG.sc _ _).symm)

/-- Every gate of one invocation's schedule is `GOK`. -/
theorem named_GOK (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) {I : NetComplex.Inv ind Wt} (hG : I.Good) :
    ∀ g ∈ I.named ℂ, GOK g.2.1 := by
  intro g hg
  have e1 : ((-1 : ℂ)) = ((-1 : ℤ) : ℂ) := by push_cast; rfl
  have e2 : ((1 : ℂ)) = ((1 : ℤ) : ℂ) := by push_cast; rfl
  simp only [NetComplex.Inv.named, List.mem_append, List.mem_map, Finset.mem_toList,
    Finset.mem_univ, true_and, List.mem_singleton] at hg
  rcases hg with ((((((⟨S, rfl⟩ | rfl) | ⟨t, rfl⟩) | rfl) | rfl) | ⟨S, rfl⟩) | rfl) | ⟨t, rfl⟩
  · rw [e1]; exact sideG_GOK hcard hinj hG _ (Or.inr rfl) S
  · rw [e1]; exact scatG_GOK hG _ (Or.inr rfl)
  · rw [e2]; exact copyG_GOK hG _ (Or.inl rfl) t
  · rw [e2]; exact gathG_GOK hG _ (Or.inl rfl)
  · rw [e2]; exact scatG_GOK hG _ (Or.inl rfl)
  · rw [e2]; exact sideG_GOK hcard hinj hG _ (Or.inl rfl) S
  · rw [e1]; exact gathG_GOK hG _ (Or.inr rfl)
  · rw [e1]; exact copyG_GOK hG _ (Or.inr rfl) t

/-- **Every gate of the three-stage complex schedule is a dyadic `GOK` gate.** -/
theorem cxNamed_GOK (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) : ∀ g ∈ NetComplex.cxNamed ℂ ind, GOK g.2.1 := by
  intro g hg
  simp only [NetComplex.cxNamed, List.mem_flatMap, List.mem_map] at hg
  obtain ⟨j, _, p, _, g', hg', rfl⟩ := hg
  have hG := NetComplex.inv_good (ind := ind) j p
  unfold NetComplex.schedJ at hg'
  split_ifs at hg'
  · simp only [NetComplex.invNamed, List.mem_reverse, List.mem_map] at hg'
    obtain ⟨g'', hg'', rfl⟩ := hg'
    exact GOK_inv (named_GOK hcard hinj hG g'' hg'')
  · exact named_GOK hcard hinj hG g' hg'

/-- The sign gate is diagonal `±1`. -/
theorem fixG_diag :
    (NetComplex.fixG ℂ ind).1 = Matrix.diagonal fun w =>
      if w ∈ (Finset.univ.image (NetComplex.wX (ind := ind))) then -1 else 1 := by
  ext p q
  simp only [NetComplex.fixG]
  rw [Matrix.add_apply, NetComplex.egM_apply, Matrix.diagonal_apply,
    Matrix.one_apply]
  by_cases hpq : p = q
  · subst hpq
    simp only [if_true]
    by_cases hx : p ∈ Finset.univ.image (NetComplex.wX (ind := ind))
    · obtain ⟨a, -, rfl⟩ := Finset.mem_image.1 hx
      rw [if_pos hx, Finset.sum_eq_single a]
      · simp; norm_num
      · intro b _ hb; simp [NetComplex.wX, hb]
      · simp
    · rw [if_neg hx, Finset.sum_eq_zero]
      · simp
      · intro a _
        rw [if_neg]
        rintro ⟨h1, -⟩
        exact hx (Finset.mem_image.2 ⟨a, Finset.mem_univ _, h1⟩)
  · rw [if_neg hpq, if_neg hpq, zero_add, Finset.sum_eq_zero]
    intro a _
    rw [if_neg]
    rintro ⟨h1, h2⟩
    exact hpq (h1.symm.trans h2)

/-- Classification of the gates of the corrected complex network. -/
theorem cxFixNamed_class (hcard : ∀ t, #(ind t) = 3) (hinj : Function.Injective ind) (g) (hg : g ∈ NetComplex.cxFixNamed ℂ ind) :
    GOK g.2.1 ∨ g.2.1 = (NetComplex.fixG ℂ ind).1 := by
  simp only [NetComplex.cxFixNamed, List.mem_append, List.mem_map, List.mem_singleton] at hg
  rcases hg with ⟨g', hg', rfl⟩ | rfl
  · exact Or.inl (cxNamed_GOK hcard hinj g' hg')
  · exact Or.inr rfl

end Complex

/-! ## The step lists -/

section Steps

open P8Lift

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

theorem not_gate_rowAddsFor {m : ℕ} (w : R) (hh : Fin m) (js : List (Fin m)) (G : Matrix R R ℂ) :
    RStep.gate G ∉ rowAddsFor w hh js := by
  intro hm
  simp only [rowAddsFor, List.mem_flatMap] at hm
  obtain ⟨j, -, hj⟩ := hm
  split_ifs at hj
  · simp at hj
  · simp at hj

theorem not_gate_chunkFor {m : ℕ} (w : R) (ε : ℤ) (v : Fin m → ZMod 2) (G : Matrix R R ℂ) :
    RStep.gate G ∉ chunkFor w ε v := by
  intro hm
  unfold chunkFor at hm
  split_ifs at hm
  · simp only [List.mem_append, List.mem_singleton] at hm
    rcases hm with (h1 | h1) | h1
    · exact not_gate_rowAddsFor _ _ _ _ h1
    · cases h1
    · exact not_gate_rowAddsFor _ _ _ _ h1
  · simp at hm

theorem not_gate_edgeSteps {h : ℕ} (w : R) (V U : Submodule (ZMod 2) (NetComplexP8.Vc h))
    (G : Matrix R R ℂ) : RStep.gate G ∉ edgeSteps w V U := by
  intro hm
  simp only [edgeSteps, frameSteps, List.mem_flatMap] at hm
  obtain ⟨p, -, hp⟩ := hm
  exact not_gate_chunkFor _ _ _ _ hp

theorem gate_mem_netSteps {h : ℕ} (G : Matrix R R ℂ) :
    ∀ (gs : List (AModel.NGate R ℂ (NetComplexP8.LabG h))) (lab Mout : R → NetComplexP8.LabG h),
      RStep.gate G ∈ netSteps gs lab Mout → ∃ g ∈ gs, G = g.1
  | [], lab, Mout, hm => by
    simp only [netSteps, List.mem_flatMap] at hm
    obtain ⟨w, -, hw⟩ := hm
    exact absurd hw (not_gate_edgeSteps _ _ _ _)
  | g :: gs, lab, Mout, hm => by
    simp only [netSteps, gateSteps, List.mem_append, List.mem_flatMap, List.mem_singleton] at hm
    rcases hm with (⟨w, -, hw⟩ | h1) | h2
    · exact absurd hw (not_gate_edgeSteps _ _ _ _)
    · cases h1; exact ⟨g, List.mem_cons_self, rfl⟩
    · obtain ⟨g', hg', e⟩ := gate_mem_netSteps G gs _ Mout h2
      exact ⟨g', List.mem_cons_of_mem _ hg', e⟩

end Steps

/-! ## The classification for `complexIface` -/

open P8Lift in
/-- A gate step of `prog ind` is a gate of `cxFixNamed`. -/
theorem gate_mem_prog {h : ℕ} {T : Type} [Fintype T] [DecidableEq T] {ind : T → Finset (Fin h)}
    (G : Matrix (NetComplex.Wr ind) (NetComplex.Wr ind) ℂ) (hm : RStep.gate G ∈ prog ind) :
    ∃ g ∈ NetComplex.cxFixNamed ℂ ind, G = g.2.1 := by
  simp only [prog, List.mem_append, List.mem_flatMap, List.mem_singleton] at hm
  rcases hm with ((⟨w, -, hw⟩ | hn) | ⟨w, -, hw⟩) | hp
  · rcases w with a | a | s <;> simp [preSteps] at hw
  · obtain ⟨g, hg, rfl⟩ := gate_mem_netSteps G _ _ _ hn
    simp only [NetComplexP8.gatesF, NetComplex.labelled, List.mem_map] at hg
    obtain ⟨g', hg', rfl⟩ := hg
    exact ⟨g', hg', rfl⟩
  · rcases w with a | a | (s | s) <;> simp [postSteps] at hw
  · cases hp

/-- **Gate classification for the complex network (task 1).**  Every scalar gate step of
`complexIface` is either a dyadic atom gate `gateMat W_c as` (atoms `Ok`, `h ≤ 1`, coefficients
`±1`, targets never sources: `KFG.gate_iruns` applies) or a diagonal sign gate
(`-1` on a set of roles, `1` elsewhere: one `KFG.UAtom` with `u = -1` per role of the set). -/
theorem complexIface_gate_class_b (G : Matrix (Fin P8Lift.Wc) (Fin P8Lift.Wc) ℂ)
    (hm : P8Lift.RStep.gate G ∈ P8Lift.complexIface.net) :
    (∃ as : List KFG.Atom, (∀ a ∈ as, a.Ok P8Lift.Wc ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
        G = KFG.gateMat P8Lift.Wc as) ∨
      (∃ U : Finset (Fin P8Lift.Wc), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1) := by
  simp only [P8Lift.complexIface, List.mem_map] at hm
  obtain ⟨st, hst, he⟩ := hm
  cases st with
  | gate G0 =>
    simp only [P8Lift.RStep.map] at he
    injection he with he
    subst he
    obtain ⟨g, hg, rfl⟩ := gate_mem_prog G0 hst
    rcases cxFixNamed_class NetComplex.ind₀_card NetComplex.ind₀_inj g hg with hgok | hfix
    · obtain ⟨as, h1, h2, h3⟩ := GOK_atoms P8Lift.eW hgok
      exact Or.inl ⟨as, h1, h2, h3.symm ▸ rfl⟩
    · refine Or.inr ⟨(Finset.univ.image (NetComplex.wX (ind := NetComplex.ind₀))).map
        P8Lift.eW.toEmbedding, ?_⟩
      rw [hfix, fixG_diag]
      ext i j
      simp only [Matrix.diagonal_apply, Finset.mem_map_equiv, P8Lift.eW.symm.injective.eq_iff]
  | rowAdd => simp [P8Lift.RStep.map] at he
  | phase => simp [P8Lift.RStep.map] at he
  | perm => simp [P8Lift.RStep.map] at he
  | child => simp [P8Lift.RStep.map] at he

end NLogN.KFN

end

section
-- Source module: Solutions.KFNP14
/-!
# KFN: Proposition 14 in IL around the recursive `C`-layer

* `p14WithI P K D S ρ r E Cc`: the Proposition 14 wrapper `S_D ; C ; S_D ; b^D ; Q_p` around a
  `C`-layer **code family** `Cc : ℕ → IStmt HS Pp` (an item-language program, e.g. calling the
  Lemma 12/13 routines under a fixed `iprog`) of scale `E` (the truncation removes `E + ⌈D/2⌉`
  bits instead of `D + ⌈D/2⌉`).
* **`p14WithI_iruns`**: for every such implementation (`SImplI` on the layer layout), the
  output represents `prop14Proc … (tens Cm) z = Q_p(H0^{⊗D} z)`, disk, error `< √2·2^{-p}`;
  cost `kC (w + 2D) + cWrapE …`.
* **`prop14_il`**: with the recursive `C`-layer `cLayer`, conditional only on the row-addition
  hypothesis `RowHyp` (an `IStmt` code family under the fixed `iprog`) and the gate class.
* `gclass_of`, **`prop14_il_complex`**: the interface `P8Lift.complexIface` (`complexIface_gate_class`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFN

open IntMul RS AModel KIL KFD KFB KFG KFH Complex P8Lift Butterfly

section Wrap

variable {Pp : ℕ} {Isym : List Sym} {iprog : Fin Pp → IStmt HS Pp} {P K D S ρ : ℕ}

end Wrap

/-! ## Gate classes of finite networks -/

theorem gclass_of {W m s : ℕ} (J : Prop8IfaceR W m s)
    (h : ∀ G, RStep.gate G ∈ J.net →
      (∃ as : List KFG.Atom, (∀ a ∈ as, a.Ok W ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
        G = KFG.gateMat W as) ∨
      (∃ U : Finset (Fin W), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1)) :
    ∃ A, GClass J A := by
  suffices H : ∀ l : List (RStep (Fin W) m), (∀ G, RStep.gate G ∈ l → RStep.gate G ∈ J.net) →
      ∃ A, ∀ G, RStep.gate G ∈ l →
        (∃ as : List KFG.Atom, as.length ≤ A ∧ (∀ a ∈ as, a.Ok W ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
            G = KFG.gateMat W as) ∨
          (∃ U : Finset (Fin W), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1) by
    obtain ⟨A, hA⟩ := H J.net (fun G hG => hG)
    exact ⟨A, hA⟩
  intro l
  induction l with
  | nil => exact fun _ => ⟨0, fun G hG => by simp at hG⟩
  | cons a l ih =>
    intro hl
    obtain ⟨A, hA⟩ := ih fun G hG => hl G (List.mem_cons_of_mem _ hG)
    have mono : ∀ A' G, A ≤ A' →
        ((∃ as : List KFG.Atom, as.length ≤ A ∧ (∀ a ∈ as, a.Ok W ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
            G = KFG.gateMat W as) ∨
          (∃ U : Finset (Fin W), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1)) →
        ((∃ as : List KFG.Atom, as.length ≤ A' ∧ (∀ a ∈ as, a.Ok W ∧ a.h ≤ 1) ∧ KFG.NoTS as ∧
            G = KFG.gateMat W as) ∨
          (∃ U : Finset (Fin W), G = Matrix.diagonal fun w => if w ∈ U then -1 else 1)) := by
      intro A' G hA' hG
      rcases hG with ⟨as, h1, h2⟩ | h3
      · exact Or.inl ⟨as, h1.trans hA', h2⟩
      · exact Or.inr h3
    cases a with
    | gate G0 =>
      rcases h G0 (hl G0 List.mem_cons_self) with ⟨as, h1, h2, h3⟩ | hU
      · refine ⟨max A as.length, fun G hG => ?_⟩
        rcases List.mem_cons.1 hG with he | hG'
        · injection he with he; subst he
          exact Or.inl ⟨as, le_max_right _ _, h1, h2, h3⟩
        · exact mono _ G (le_max_left _ _) (hA G hG')
      · refine ⟨A, fun G hG => ?_⟩
        rcases List.mem_cons.1 hG with he | hG'
        · injection he with he; subst he; exact Or.inr hU
        · exact hA G hG'
    | _ =>
      refine ⟨A, fun G hG => ?_⟩
      rcases List.mem_cons.1 hG with he | hG'
      · cases he
      · exact hA G hG'

theorem complexIface_gclass : ∃ A, GClass P8Lift.complexIface A :=
  gclass_of _ complexIface_gate_class_b

/-! ## Proposition 14 in IL with the recursive `C`-layer -/

section Main

variable {Pp : ℕ} {Isym : List Sym} {iprog : Fin Pp → IStmt HS Pp}

end Main

end NLogN.KFN

end

section
-- Source module: Solutions.ResampleParams
/-!
# §9.1–9.2 Fixed rational choice and sizes

* `constants_ok`: the layer and dimension conditions of (38), `margins_ok`: the seven margins
  of (45) with `min gᵢ = 2⁻¹⁸¹ = 2κ`.
* Axis lengths `t_i ∈ {r/2, r}` with `∏ t_i = T`, last axis `r` (`axExp_sum`, `axLen_prod`,
  `axExp_last`), `p/(12d) ≤ ℓ ≤ p/(3d)` (`ell_bounds`), `24n ≤ T p < 48 n` (`Tp_bounds`).
* Source lengths: `(1-2η)t_i < s_i ≤ (1-η)t_i` ⇒ `S > T/2` (`S_gt_half`), `θ_i > η`
  (`theta_gt_eta`), `α⁴θ_i > p` (`alpha4_theta_gt_p`), `γ < 28 d² √b` (`gamma_bound`);
  existence of pairwise coprime odd `s_i` (`sources_exist`, from `RCop.coprime_params`).
* Radix digits (§9.2.3): `2q - 2 < S` (`degree_lt_S`) and `c_j < 2^{3b}` (`coeff_lt`).
-/

open Finset

namespace IntMul.OpenAI.RP

/-! ### (38) and (45) -/

/-! ### Axis lengths of the padded box -/

/-- Exponent of axis `i`: `ℓ - 1` for the first `dℓ - L` axes, `ℓ` for the others. -/
def axExp (L d : ℕ) (i : Fin d) : ℕ := if (i : ℕ) < mcnt L d then ell L d - 1 else ell L d

/-! ### Source lengths, resampling margins -/

/-! ### §9.2.3 radix-digit polynomials -/

end IntMul.OpenAI.RP

end

section
-- Source module: Solutions.KFMSm
/-!
# KFM Sm: bit bounds for register expressions from bounds on their atoms

`exSmS A s e`: every register, literal and `2^a` that `e` reads is at most `A` in absolute value,
and every divisor is positive. `exDgS e` is a degree (sums add one, products add). Then
`|e.eval s| ≤ A^{exDgS e}` (**`exSmS_abs`**), and `A^{exDgS e} < 2^B` gives `e.Bnd s B`
(**`exSmS_bnd`**), which is the hypothesis of the RS cost lemmas.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KFM

open IntMul RS

/-- Atom bounds (see the module doc). -/
def exSmS (A : ℕ) (s : IState HS) : Ex HS → Prop
  | .reg i => |s.top i| ≤ (A : ℤ)
  | .lit c => |c| ≤ (A : ℤ)
  | .add a b | .mul a b => exSmS A s a ∧ exSmS A s b
  | .neg a => exSmS A s a
  | .ndiv a b | .nmod a b => exSmS A s a ∧ exSmS A s b ∧ 0 < b.eval s
  | .pow2 a => exSmS A s a ∧ 0 ≤ a.eval s ∧ 2 ^ (a.eval s).toNat ≤ A
  | .sel c x y => exSmS A s c ∧ exSmS A s x ∧ exSmS A s y
  | _ => False

/-- The degree. -/
def exDgS : Ex HS → ℕ
  | .reg _ | .lit _ => 1
  | .add a b => max (exDgS a) (exDgS b) + 1
  | .mul a b => exDgS a + exDgS b
  | .neg a | .pow2 a => exDgS a
  | .ndiv a b | .nmod a b => max (exDgS a) (exDgS b)
  | .sel c x y => max (exDgS c) (max (exDgS x) (exDgS y))
  | _ => 1

end NLogN.KFM

end

section
-- Source module: Solutions.KFMS5
/-!
# KFM S5: a loop lemma with an arbitrary invariant state

`loopI_run` / `loopI_cost`: `rep i n body` with `n = N`. The body, started in
`(St k).upd i (N−k :: s.G i)`, ends in `(St (k+1)).upd i (N−k :: s.G i)`. Then the loop ends in
`St N`. The states `St k` may differ from `s` anywhere except on the counter stack `i`. This
covers nested loops and loops that push onto lists (descriptors).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul RS

/-- The state at the start of iteration `k`. -/
def lI (St : ℕ → IState HS) (s : IState HS) (i : Fin HS) (N k : ℕ) : IState HS :=
  (St k).upd i (.int ((N : ℤ) - k) :: s.G i)

end NLogN.KFM

end

section
-- Source module: Solutions.KFMS6
/-!
# KFM S6: the sources and their inverses (math side)

* `srcN n i = s_i`, `prodN n i = ∏_{j<i} s_j`, `muN n i = μ_i = (prodN n i)^{-1} mod s_i`.
* **`indZ_eq`**: for `0 ≤ m < s`, `(s − ((m + s − 1) mod s)) / s = [m = 1]`. This is the
  indicator the IL sum uses (only `nmod`/`ndiv`).
* **`sum_mu`**: `Σ_{y=1}^{s} y·[y·(P mod s) mod s = 1] = muInv P s` for coprime `P, s`, `s ≥ 2`.
* **`prod_mod_seq`**: the running product `c ↦ (c·s_{i−1−k}) mod s_i` ends at `prodN n i mod s_i`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP

/-- `d' = dℓ − L`. -/
noncomputable def dpN (n : ℕ) : ℕ := mcnt (IntMul.OpenAI.Glue.LP n) (IntMul.OpenAI.Glue.dP n)

/-- The source `s_i`. -/
noncomputable def srcN (n i : ℕ) : ℕ := srcS (IntMul.OpenAI.Glue.dP n) (dpN n) (IntMul.OpenAI.Glue.rP n) i

/-- `P_i = ∏_{j<i} s_j`. -/
noncomputable def prodN (n i : ℕ) : ℕ := ∏ j ∈ Finset.range i, srcN n j

/-- `μ_i = P_i^{-1} mod s_i`. -/
noncomputable def muN (n i : ℕ) : ℕ := muInv (prodN n i) (srcN n i)

/-- The running product modulo `s`. -/
def pmSeq (s : ℕ) (g : ℕ → ℕ) : ℕ → ℕ
  | 0 => 1
  | k + 1 => (pmSeq s g k * g k) % s

end NLogN.KFM

end

section
-- Source module: Solutions.KFMS7
/-!
# KFM S7: the source and inverse lists in IL (run lemmas)

Scratch stacks `1–5` (setup is a leaf procedure, UNIFORM amendment): `mOc = 1` outer counter,
`mS = 2` the source `s_i`, `mP = 3` the running product, `mM = 4` the sum, `mIc = 5` the inner
counter. The parameters are read from `zDp, zQ, zMh, zMf` (KFMS3).

* `srcE ix`: `s_j = 1 + Q·(j < d' ? M_h − j : M_f − (j − d'))` for `j = ix` (**`srcE_spec`**).
* `muB dst`: for `i = (top of mOc) − 1`, computes `P_i mod s_i` by a product loop, then
  `μ_i = Σ_{y=1}^{s_i} y·[y P_i ≡ 1]` by a sum loop, and pushes `μ_i` on `dst`
  (**`muB_run`**).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul RS

abbrev mOc : Fin HS := 1
abbrev mS : Fin HS := 2
abbrev mP : Fin HS := 3
abbrev mM : Fin HS := 4
abbrev mIc : Fin HS := 5

/-- The source value for generic parameters. -/
def srcV (d' Q Mh Mf j : ℕ) : ℕ := 1 + Q * (if j < d' then Mh - j else Mf - (j - d'))

/-- `s_j` for `j = ix`. -/
def srcE (ix : Ex HS) : Ex HS :=
  .add (.lit 1) (.mul (.reg zQ) (.sel (.add ix (.neg (.reg zDp))) (.add (.reg zMh) (.neg ix))
    (.add (.reg zMf) (.neg (.add ix (.neg (.reg zDp)))))))

def ixO : Ex HS := .add (.reg mOc) (.lit (-1))
def ixI : Ex HS := .add (.reg mIc) (.lit (-1))

/-- The product body: `P ← (P · s_j) mod s_i`, `j = (top of mIc) − 1`. -/
def pmB : RS := .asg mP (.nmod (.mul (.reg mP) (NLogN.KFM.srcE ixI)) (.reg mS))

/-- `[y·P mod s = 1]` for `y` on `mIc`. -/
def indE : Ex HS :=
  .ndiv (.add (.reg mS) (.neg (.nmod (.add (.nmod (.mul (.reg mIc) (.reg mP)) (.reg mS))
    (.add (.reg mS) (.lit (-1)))) (.reg mS)))) (.reg mS)

/-- The sum body: `M ← M + y·[y P ≡ 1]`. -/
def sumB : RS := .asg mM (.add (.reg mM) (.mul (.reg mIc) indE))

/-- One inverse: push `μ_i` on `dst`. -/
def muB (dst : Fin HS) : RS :=
  .seq (.push mS (NLogN.KFM.srcE ixO)) (.seq (.push mP (.lit 1)) (.seq (.rep mIc ixO pmB)
    (.seq (.push mM (.lit 0)) (.seq (.rep mIc (.reg mS) NLogN.KFM.sumB) (.seq (.push dst (.reg mM))
      (.seq (.pop mM) (.seq (.pop mP) (.pop mS))))))))

/-- All inverses: `μ_{d−1}, …, μ_0` pushed on `dst` (so `μ_0` ends on top). -/
def muP (dst : Fin HS) : RS := .rep mOc (.reg NLogN.KFM.zD) (muB dst)

/-- All sources: `s_{d−1}, …, s_0` pushed on `dst`. -/
def srcP (dst : Fin HS) : RS := .rep mOc (.reg NLogN.KFM.zD) (.push dst (NLogN.KFM.srcE ixO))

/-- The parameter registers hold `d', Q, M_h, M_f`. -/
structure SrcRegs (u : IState HS) (d' Q Mh Mf : ℕ) : Prop where
  hDp : ∃ L, u.G zDp = .int (d' : ℤ) :: L
  hQ : ∃ L, u.G zQ = .int (Q : ℤ) :: L
  hMh : ∃ L, u.G zMh = .int (Mh : ℤ) :: L
  hMf : ∃ L, u.G zMf = .int (Mf : ℤ) :: L

/-! ## The product loop -/

/-! ## The sum loop -/

/-! ## One inverse -/

/-- `dst` is not one of the stacks the source/inverse code reads or uses. -/
structure DstOk (dst : Fin HS) : Prop where
  lt : dst.val < 56
  ge : 6 ≤ dst.val
  ne : dst ≠ NLogN.KFM.zD ∧ dst ≠ zDp ∧ dst ≠ zQ ∧ dst ≠ zMh ∧ dst ≠ zMf

/-! ## Loops that push one value per index -/

/-- The values pushed after `k` of `d` iterations: `v (d−k), …, v (d−1)`. -/
def pushL (v : ℕ → ℤ) (d k : ℕ) : List ℤ := (List.range k).map fun t => v (d - k + t)

end NLogN.KFM

end

section
-- Source module: Solutions.KFMS9
/-!
# KFM S9: the cost of the source and inverse lists

Write `K = 10^7 (B+2)^2`. Assume every atom is at most `A`, with `A^k < 2^B` for `k ≤ 8`.

* **`pmLoop_cost`**: the product loop costs at most `(i+1)·40K`.
* **`sumLoop_cost`**: the sum loop costs at most `(s+1)·40K`.
* **`muB_cost`**: one inverse costs at most `(i+s+4)·40K`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul RS

/-- The bit environment: atoms `≤ A`, degree-`≤ 8` values fit in `B` bits. -/
structure CostEnv (A B : ℕ) : Prop where
  hA : 256 ≤ A
  hAB : ∀ k ≤ 8, A ^ k < 2 ^ B

/-! ## The product loop -/

/-! ## The sum loop -/

/-! ## Push loops -/

end NLogN.KFM

end

section
-- Source module: Solutions.KFMP18
/-!
# KFM 14: Proposition 18 as an explicit IL hypothesis `P18IL`

`P18IL` is the interface between the assembly (item 14) and Prop 18 in IL (item 13).

* The procedure table is **one fixed table** `kTable ext` (`ext`, `entry` and the descriptor stack
  `dS` are chosen before `n`). The final machine must not depend on `n`, so every `n`-dependent
  quantity (`p, ℓ, K, D`, the axis lengths `t_i`) is run-time data on stack `dS`, not a literal
  in the code.
* Data: two arrays `f, g` of `N = ∏ t_i` records in row-major order over `t_1 × … × t_D`
  (last axis fastest). Each record is `r = 2^ℓ` Gaussian coefficients at scale `2^p` (`RecRep`),
  in the unit disk, width `W = p + 2`. They sit on stack `0` (`f` on top). All other managed
  stacks are empty and the rest of the state (`s`) is arbitrary and preserved.
* Result: one array `h` (`RecRep r p`, width `W`) replacing `f, g` on stack `0`, within
  `2 N (3ℓ + 1) 2^{-p}` of `M_r(f, g) = (f ∗ g)/(r N)` in every coefficient (the bound of
  `GlueProp18.prop18_scaled_full`, with `√2 ≤ 2`, transported to the row-major order).
* Cost `≤ C₀ · N r (W + 1) · Ncost(6 lg n, d, K, ℓ, α) · (log(6 lg n) + 1)^A` for `n ≥ n₁`,
  with `D + 1 = d = dP n`, `ℓ = ℓP n`, `K = KP n`, `p = pP n`, `t_i ∈ {r/2, r}`.
-/

namespace NLogN.KFM

open IntMul KIL KFB KFH IntMul.OpenAI.Glue IntMul.OpenAI.RCost

noncomputable section

/-- The descriptor of a Prop 18 call: `[p, ℓ, K, D, t_1, …, t_D]`. -/
def desc18 (p ℓ K : ℕ) (ts : List ℕ) : List ℤ :=
  (p : ℤ) :: (ℓ : ℤ) :: (K : ℤ) :: (ts.length : ℤ) :: ts.map (fun t => (t : ℤ))

/-- **Proposition 18 in IL** (hypothesis of the assembly; to be proved in item 13). -/
def P18IL : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (entry : Fin (7 + E)) (dS : Fin HS)
    (C₀ : ℝ) (A n₁ : ℕ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ (Isym : List Sym) (n : ℕ), IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n →
  ∀ (ts : List ℕ), ts.length + 1 = IntMul.OpenAI.Glue.dP n → (∀ t ∈ ts, t = IntMul.OpenAI.Glue.rP n ∨ 2 * t = IntMul.OpenAI.Glue.rP n) →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zf zg : List GI) (l : List ℤ)
    (xf xg : List (Fin (IntMul.OpenAI.Glue.rP n) → ℂ)),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = desc18 (pP n) (ℓP n) (KP n) ts →
    f 0 = gflat zf ++ gflat zg ++ l →
    RecRep (IntMul.OpenAI.Glue.rP n) (pP n) zf xf → RecRep (IntMul.OpenAI.Glue.rP n) (pP n) zg xg →
    xf.length = ts.prod → xg.length = ts.prod →
    NLogN.KFB.GB (pP n + 2) zf → NLogN.KFB.GB (pP n + 2) zg →
    (∀ x ∈ xf, ‖x‖ ≤ 1) → (∀ x ∈ xg, ‖x‖ ≤ 1) →
    ∃ (zh : List GI) (xh : List (Fin (IntMul.OpenAI.Glue.rP n) → ℂ)) (c : ℕ),
      IRuns Isym (kTable ext) (.call entry) (NLogN.KIL.encK s f)
        (NLogN.KIL.encK s (Function.update f 0 (gflat zh ++ l))) c ∧
      RecRep (IntMul.OpenAI.Glue.rP n) (pP n) zh xh ∧ xh.length = ts.prod ∧ NLogN.KFB.GB (pP n + 2) zh ∧
      (∀ j < ts.prod, ∀ k : Fin (IntMul.OpenAI.Glue.rP n),
        ‖xh.getD j 0 k - (mrL (IntMul.OpenAI.Glue.rP n) ts xf xg).getD j 0 k‖ ≤
          2 * ts.prod * (3 * ℓP n + 1) * (2 : ℝ)⁻¹ ^ pP n) ∧
      (c : ℝ) ≤ C₀ * ((ts.prod * IntMul.OpenAI.Glue.rP n * (pP n + 3) : ℕ) : ℝ) *
        Ncost (6 * (lg n : ℝ)) (IntMul.OpenAI.Glue.dP n) (KP n) (ℓP n) (αP n) *
        (Real.log (6 * (lg n : ℝ)) + 1) ^ A

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFURevBase
/-!
# KFU §3: labelled layouts for the axis reversal

Addresses of the working array are tracked through *layouts*: lists of atom labels (`2j` is the
main part of axis `j`, of size `mz j`; `2j+1` is its extra bit, of size `2`, present when
`bg j`).  An axis of size `tz j = mz j · (2 if bg j)` is the pair `[mz j, 2]` in row-major order.

* `Dl ax0 lay xs`: the array `xs` (shape `ax0.map tz`) viewed in the layout `lay`.
* `POp g σ n`: an address map `g = permIdx σ` on `n` digits, `σ` onto `[0, n)`.
* `Dl_step`: a program realizing `pull (g lay').map asz → lay'.map asz` by `g` turns
  `Dl ax0 (g lay')` into `Dl ax0 lay'`.  `swapPos` and `KIL.swapMid` are `POp`s.
* `Dl_layA`: for the standard layout `layA ax` of an axis order `ax`, `Dl` is an ordinary pull
  onto `ax.map tz`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KFU

open AModel AModelL12

/-! ## Position permutations -/

theorem POp.length {g : List ℕ → List ℕ} {σ : ℕ → ℕ} {n : ℕ} (hP : POp g σ n) {b : List ℕ}
    (hb : b.length = n) : (g b).length = n := by
  rw [hP.eq b hb, length_permIdx, hb]

/-! ### `swapPos` -/

/-! ### `swapMid` -/

/-! ## Layouts -/

section Layout

variable (mz : ℕ → ℕ) (bg : ℕ → Bool)

end Layout

/-! ## The standard layout -/

section Std

variable (mz : ℕ → ℕ) (bg : ℕ → Bool)

end Std

end NLogN.KFU

end

section
-- Source module: Solutions.ResampleCRT
/-!
# §9.3 An explicit cyclic-convolution layout

* `Phi`: `ℤ/S → ∏ ℤ/s_i`, `k ↦ (μ_i k)_i` (the coordinate map of `x ↦ ∏ x_i^{μ_i}`), an additive
  equivalence for pairwise coprime `s_i` and units `μ_i` (`PhiEquiv`); every additive
  equivalence carries cyclic convolution to cyclic convolution (`conv_addEquiv`), so
  `Φ(u ∗ v) = Φu ∗ Φv` (`Phi_conv`).
* Mixed radix: `k mod P_i = Σ_{j<i} a_j P_j` (`mod_prefix_eq_sum`) and the coordinate formula
  (42): `μ_i k ≡ a_i + μ_i Σ_{j<i} a_j P_j (mod s_i)` (`coord_formula`).
* Triangular realization: the prefix-controlled cyclic shifts, processed for `i = d-1, …, 0`,
  send every valid address `a` to `b` of (42) (`shifts_realize`); each shift is a bijection of
  the padded box preserving the valid set `V` and its complement (`upd_inv`, `upd_valid`,
  `upd_invalid`).
-/

open Finset

namespace IntMul.OpenAI.RCRT

/-! ### Convolution is preserved by additive equivalences -/

section conv
variable {G H : Type*} [AddCommGroup G] [AddCommGroup H] [Fintype G] [Fintype H]
  {R : Type*} [CommRing R]

/-- Cyclic convolution on a finite abelian group. -/
def gconv (u v : G → R) : G → R := fun j => ∑ k, u k * v (j - k)

end conv

/-! ### The map `Φ` -/

variable {d : ℕ}

/-! ### Mixed radix and the coordinate formula (42) -/

/-! ### Realization by prefix-controlled cyclic shifts -/

section shifts
variable (s μ : ℕ → ℕ)

end shifts

end IntMul.OpenAI.RCRT

end

section
-- Source module: Solutions.KFMNeed
/-!
# KFM: the uniform interfaces `PhiNeed` and `SwapNeed` (hypotheses of the assembly)

These are stated in the style of `P18IL`. Each one asks for a fixed table `kTable ext`, with
`ext`, the entry points and the descriptor stack `dS` all chosen before any parameter. Every
size-dependent quantity is run-time data on `dS`. The data sit on stack `0` (array on top, then
an arbitrary tail `l`). Every other managed stack is empty (`f j = []` for `j ≠ 0, dS`), so a
procedure may use any stack as scratch as long as it leaves it as it found it. The unmanaged
part `s` underneath is arbitrary and preserved. On exit, `dS` still holds its descriptor.

* **`PhiNeed`**: uniform `Φ` / `Φ⁻¹` of §9.3, with the denotations `KFU.PhiD` / `KFU.PhiInvD`.
  These are KFU's `phi_spec` / `phiInv_spec` with the literals `w, h, d, bL, s_j, μ_j` moved into
  the descriptor `descPhi`. Cost: a constant times KFU's `cPhi` (Lemma 12 constant `1`), plus a
  descriptor term `(d+1)(h+w+size V_S+1)²`.
* **`SwapNeed`**: uniform Lemma 12 on Gaussian (record) arrays: interchange two axes `p < q` of
  equal size `2^u` in an array of any positive shape `sh`. This is KFS's `swAxG_spec`, with
  `w, u, p, q, sh` in the descriptor `descSw`. Records of `r` entries use the shape `sh ++ [r]`.
  Cost: `K (w+1)(V+1) u^τ`, plus a descriptor term `(|sh|+1)(size V+w+u+1)²`. The assembly
  builds the axis exposure (moving an axis innermost before a line map, and back after it)
  from these swaps. A `2^{h+1}` axis is split as `2 × 2^h` by a free reshape.

* **`TransNeed`**: uniform axis rotation (`transposeL t (V/t)`) on padded Gaussian arrays whose
  axes are all `2^h` or `2^{h+1}`. This is the exposure step that replaces nlogn's `transP 2`
  inside `GL.axisP`. Equal-size swaps cannot do it when the sizes are mixed (see the docstring).

The final theorem may take `P18IL ∧ PhiNeed ∧ TransNeed` (and `SwapNeed` if it is used). The tables are merged by relabelling
(`IRuns.relabel`).
-/

namespace NLogN.KFM

open IntMul KIL KFB AModel AModelL12

noncomputable section

/-! ## `Φ` / `Φ⁻¹` -/

/-- The bits `bL 0, …, bL (d-1)` as `0/1`. -/
def bitsZ (d : ℕ) (bL : ℕ → Bool) : List ℤ := (List.range d).map fun j => if bL j then 1 else 0

/-- The descriptor of a `Φ` / `Φ⁻¹` call:
`[w, h, d, bL 0..d-1 (0/1), s_0..s_{d-1}, μ_0..μ_{d-1}]`. -/
def descPhi (w h d : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ) : List ℤ :=
  (w : ℤ) :: (h : ℤ) :: (d : ℤ) ::
    (bitsZ d bL ++ (List.range d).map (fun j => (sF j : ℤ)) ++
      (List.range d).map (fun j => (μ j : ℤ)))

/-- The cost allowed for one `Φ` or `Φ⁻¹` call (`C₀` times this). -/
def cPhiU (w h d : ℕ) (bL : ℕ → Bool) (sF : ℕ → ℕ) : ℝ :=
  KFU.cPhi d w (vol (KFU.shR d (KFU.tP d h bL))) (vol (KFU.shR d (KFU.sP d sF)))
      (vol ((List.range (d - 1)).map sF)) (zsz ((2 * vol (KFU.shR d (KFU.sP d sF)) : ℕ) : ℤ)) 1 h +
    (((d + 1) * (h + w + Nat.size (vol (KFU.shR d (KFU.sP d sF))) + 1) ^ 2 : ℕ) : ℝ)

/-- **`Φ` and `Φ⁻¹` in IL, uniform** (hypothesis of the assembly). Forward entry `eF`: `xs` in
the k-order source shape `shK d (sP d sF)` becomes `PhiD xs` in the padded reversed shape
`shR d (tP d h bL)`. Backward entry `eB`: `ys` in that shape becomes `PhiInvD ys`. -/
def PhiNeed : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eF eB : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ),
    dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ (Isym : List Sym) (w h d : ℕ) (bL : ℕ → Bool) (sF μ : ℕ → ℕ),
    1 ≤ h → (∀ j < d, 1 ≤ sF j ∧ sF j ≤ 2 ^ (h + if bL j then 1 else 0) ∧ μ j < sF j) →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descPhi w h d bL sF μ →
    (∀ xs : List ℤ, f 0 = xs ++ l → xs.length = vol (KFU.shK d (KFU.sP d sF)) → Bnd w xs →
      ∃ c : ℕ, IRuns Isym (kTable ext) (.call eF) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (KFU.PhiD h d bL sF μ xs ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cPhiU w h d bL sF) ∧
    (∀ ys : List ℤ, f 0 = ys ++ l → ys.length = vol (KFU.shR d (KFU.tP d h bL)) → Bnd w ys →
      ∃ c : ℕ, IRuns Isym (kTable ext) (.call eB) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (KFU.PhiInvD h d bL sF μ ys ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cPhiU w h d bL sF)

/-! ## Axis swaps (Lemma 12 on Gaussian record arrays) -/

/-! ## Axis rotation on padded arrays (the exposure step around the line maps) -/

/-- The padded shape `[2^{h+b_0}, …, 2^{h+b_{k-1}}]` (`b_j ∈ {0,1}`). -/
def shPad (h : ℕ) (bs : List Bool) : Shape := bs.map fun b => 2 ^ (h + if b then 1 else 0)

/-- The descriptor of a rotation call: `[w, h, k, b_0, …, b_{k-1}]` (bits as `0/1`). -/
def descTr (w h : ℕ) (bs : List Bool) : List ℤ :=
  (w : ℤ) :: (h : ℤ) :: (bs.length : ℤ) :: bs.map (fun b => if b then 1 else 0)

/-- **Axis rotation in IL, uniform** (hypothesis of the assembly). A row-major Gaussian array
of the padded shape `t :: rest = shPad h bs` (every axis `2^h` or `2^{h+1}`) is transposed as
`t × vol rest → vol rest × t`. This is nlogn's `transposeL`, the map that `GL.axisP` gets from
`transP 2`. That radix-sort transpose costs `O(V log V)` and is not allowed here. This version
costs `K (k+1)(w+1)(V+1)(h^τ+1)`, as KFU's `rev_spec` does for one reversal. Equal-size Lemma 12
swaps alone (`SwapNeed`) cannot do it cheaply when the sizes are mixed: the extra bits of the
`2^{h+1}` axes have to be moved as in KFU `revC` (`fwdF`/`bwdF`). -/
def TransNeed : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (entry : Fin (7 + E)) (dS : Fin HS) (K : ℝ),
    dS ≠ 0 ∧ 0 ≤ K ∧
  ∀ (Isym : List Sym) (w h : ℕ) (bs : List Bool), 1 ≤ h → bs ≠ [] →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descTr w h bs →
    f 0 = gflat zs ++ l → zs.length = vol (shPad h bs) → NLogN.KFB.GB w zs →
    ∃ c : ℕ, IRuns Isym (kTable ext) (.call entry) (NLogN.KIL.encK s f)
        (NLogN.KIL.encK s (Function.update f 0
          (gflat (IntMul.HvdH.Ref.transposeL ((shPad h bs).headD 1) (vol (shPad h bs).tail) zs) ++ l))) c ∧
      (c : ℝ) ≤ K * (((bs.length + 1 : ℕ) : ℝ) * ((w : ℝ) + 1) * ((vol (shPad h bs) : ℝ) + 1) *
          ((h : ℝ) ^ KFS.τS + 1) + (((bs.length + 1) * (h + w + bs.length + 1) ^ 2 : ℕ) : ℝ))

end

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSB
/-!
# KFM SB: the `Φ` descriptor

* `bitP dst`: pushes the bits `b_j = [d' ≤ j]` (`t_j = r` exactly when `j ≥ d'`) for `j < d`
  (**`bitP_run`**, **`bitP_cost`**).
* **`descPhiP dst rw`**: pushes `descPhi w (ℓ−1) d bL s μ` (KFMNeed) on `dst`, with `w` read from
  the register `rw` (**`descPhiP_run_n`**, **`descPhiP_cost_n`**).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP RS

/-- `[d' ≤ j]` for `j = ix`. -/
def bitE (ix : Ex HS) : Ex HS := .sel (.add ix (.neg (.reg zDp))) (.lit 0) (.lit 1)

/-- All bits: `b_{d−1}, …, b_0` pushed on `dst`. -/
def bitP (dst : Fin HS) : RS := .rep mOc (.reg zD) (.push dst (NLogN.KFM.bitE ixO))

/-- `h = ℓ − 1`. -/
def hE : Ex HS := .add (.reg zEl) (.lit (-1))

/-- **The `Φ` descriptor**: `w` from register `rw`. -/
def descPhiP (dst rw : Fin HS) : RS :=
  .seq (muP dst) (.seq (NLogN.KFM.srcP dst) (.seq (bitP dst) (.seq (.push dst (.reg zD))
    (.seq (.push dst NLogN.KFM.hE) (.push dst (.reg rw))))))

/-- The bits of `n`: `t_j = r` exactly when `j ≥ d'`. -/
noncomputable def bLn (n : ℕ) (j : ℕ) : Bool := decide (dpN n ≤ j)

/-- The registers the descriptor code reads, for `n`. -/
structure DescRegs (t : IState HS) (n w : ℕ) (rw : Fin HS) : Prop where
  src : SrcRegs t (dpN n) (srcQ (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n)) (srcM (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n) (IntMul.OpenAI.Glue.rP n / 2))
    (srcM (IntMul.OpenAI.Glue.dP n) (IntMul.OpenAI.Glue.rP n) (IntMul.OpenAI.Glue.rP n))
  hD : ∃ L, t.G zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: L
  hEl : ∃ L, t.G zEl = .int (ℓP n : ℤ) :: L
  hW : ∃ L, t.G rw = .int (w : ℤ) :: L

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSC
/-!
# KFM SC: handing a descriptor to a procedure with an arbitrary descriptor stack

The `Need` interfaces fix their descriptor stack `dS` existentially, so `dS` may be any stack
(also one of the setup registers or a scratch stack `≥ 56`). The descriptor is therefore built
on a free stack `X` above a mark and then moved to `dS` with plain `mv` loops, which work on any
stack:

* **`mvLoop X Y`**: `while top X ≠ mark: mv X Y` (reverses the block) (**`mvLoop_runs`**).
* **`dropLoop D`**: `while top D ≠ mark: drop D` (**`dropLoop_runs`**).
* **`xfer X Y D`**: `mark D; mark Y; mvLoop X Y; unmark X; mvLoop Y D; unmark Y`. It moves the
  block above the mark on `X` to `D` in the same order, over a new mark on `D` (**`xfer_runs`**).
* **`unxfer D`**: `dropLoop D; unmark D` removes it again after the call (**`unxfer_runs`**).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}

/-- Not a mark. -/
def notMk : Cls → Bool := fun c => c != .mark

/-- `while top X ≠ mark: mv X Y`. -/
def mvLoop (X Y : Fin HS) : IStmt HS P := .loop X notMk (.op (.mv X Y))

/-- `while top D ≠ mark: drop D`. -/
def dropLoop (D : Fin HS) : IStmt HS P := .loop D notMk (.op (.drop D))

/-- The cost of moving one integer of size `≤ B`. -/
def cMv (B : ℕ) : ℕ := 2 * moveCost B + 49

/-- Move the block above the mark on `X` to `D` (same order), over a new mark on `D`. -/
def xfer (X Y D : Fin HS) : IStmt HS P :=
  .seq (.op (.mark D)) (.seq (.op (.mark Y)) (.seq (mvLoop X Y) (.seq (.op (.unmark X))
    (.seq (mvLoop Y D) (.op (.unmark Y))))))

/-- Remove the block above the mark on `D`, and the mark. -/
def unxfer (D : Fin HS) : IStmt HS P := .seq (dropLoop D) (.op (.unmark D))

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSD
/-!
# KFM SD: the Prop 18 descriptor

`desc18 p ℓ K ts = [p, ℓ, K, D, t_0, …, t_{D−1}]` (KFMP18) with `D = d − 1`, `p = 6b` and
`t_j = r` exactly when `j ≥ d'` (else `r/2`). These are the first `d − 1` axes of the padded
shape `shR d (tP d (ℓ−1) bL)` of `Φ` (the last of the `d` axes is the record axis, `t_{d−1} = r`).

* `tsE`: `t_{j−1}` for `j = ix` (`sel`), so that the push loop over `j = 0..d−1` leaves a junk
  entry `t_{−1}` on top, which `pop` removes.
* **`desc18P dst`** (**`desc18P_run_n`**, **`desc18P_cost_n`** `≤ 10^12 (b+1)^3`). It reads
  `b` from `zB` and `d, K, ℓ, r, d'` from the setup registers.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP RS

/-- `t_{ix−1}`: `r/2` if `ix − d' − 1 < 0`, else `r`. -/
def tsE : Ex HS :=
  .sel (.add (.add ixO (.neg (.reg zDp))) (.lit (-1))) (.ndiv (.reg zR) (.lit 2)) (.reg zR)

/-- The axis lengths: `t_0, …, t_{d−2}` on `dst`. -/
def tsP (dst : Fin HS) : RS := .seq (.rep mOc (.reg zD) (.push dst tsE)) (.pop dst)

/-- `p = 6b`. -/
def pE : Ex HS := .mul (.lit 6) (.reg NLogN.KFM.zB)

/-- `D = d − 1`. -/
def dmE : Ex HS := .add (.reg zD) (.lit (-1))

/-- **The Prop 18 descriptor.** -/
def desc18P (dst : Fin HS) : RS :=
  .seq (tsP dst) (.seq (.push dst dmE) (.seq (.push dst (.reg zK)) (.seq (.push dst (.reg zEl))
    (.push dst pE))))

/-- The axis lengths for `n`. -/
noncomputable def tsN (n : ℕ) : List ℕ :=
  (List.range (IntMul.OpenAI.Glue.dP n - 1)).map fun j => if dpN n ≤ j then IntMul.OpenAI.Glue.rP n else IntMul.OpenAI.Glue.rP n / 2

/-- Where `desc18P` may write. -/
structure D18Ok (dst : Fin HS) : Prop where
  lt : dst.val < 56
  ne : dst ≠ mOc ∧ dst ≠ zD ∧ dst ≠ zDp ∧ dst ≠ zR ∧ dst ≠ zK ∧ dst ≠ zEl ∧ dst ≠ NLogN.KFM.zB

/-- The registers `desc18P` reads. -/
structure D18Regs (t : IState HS) (n : ℕ) : Prop where
  hD : ∃ L, t.G zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: L
  hDp : ∃ L, t.G zDp = .int (dpN n : ℤ) :: L
  hR : ∃ L, t.G zR = .int (IntMul.OpenAI.Glue.rP n : ℤ) :: L
  hK : ∃ L, t.G zK = .int (KP n : ℤ) :: L
  hEl : ∃ L, t.G zEl = .int (ℓP n : ℤ) :: L
  hB : ∃ L, t.G NLogN.KFM.zB = .int (bP n : ℤ) :: L

/-- The value pushed for the counter `c` (index `j = c − 1`). -/
def tsV (d' r : ℕ) (j : ℕ) : ℤ := if d' + 1 ≤ j then (r : ℤ) else ((r / 2 : ℕ) : ℤ)

end NLogN.KFM

end

section
-- Source module: Solutions.KFMSE
/-!
# KFM SE: the axis-rotation descriptor (`TransNeed`)

`descTr w h bs = [w, h, k, b_0, …, b_{k−1}]` (KFMNeed). In kmain the array has the padded shape
`[t_0, …, t_{d−1}]` (`t_j = 2^{h + b_j}`, `h = ℓ − 1`, `b_j = [d' ≤ j]`). After `m` rotations
its shape is that list rotated left by `m`, so the descriptor of the next rotation uses the bits
`bR n m j = [d' ≤ (j + m) mod d]`.

* **`descTrP dst rw rm`**: pushes `descTr w (ℓ−1) (bsN n m)` with `w` read from register `rw`
  and `m` from register `rm` (**`descTrP_run_n`**, **`descTrP_cost_n`** `≤ 10^12 (b+1)^3`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP RS

/-- `[d' ≤ (ix + m) mod d]` for `m` on `rm`. -/
def rbitE (rm : Fin HS) : Ex HS :=
  .sel (.add (.nmod (.add ixO (.reg rm)) (.reg zD)) (.neg (.reg zDp))) (.lit 0) (.lit 1)

/-- The rotated bits on `dst`. -/
def rbitP (dst rm : Fin HS) : RS := .rep mOc (.reg zD) (.push dst (rbitE rm))

/-- **The rotation descriptor.** -/
def descTrP (dst rw rm : Fin HS) : RS :=
  .seq (rbitP dst rm) (.seq (.push dst (.reg zD)) (.seq (.push dst NLogN.KFM.hE) (.push dst (.reg rw))))

/-- The rotated bits for `n` after `m` rotations. -/
noncomputable def bsN (n m : ℕ) : List Bool :=
  (List.range (IntMul.OpenAI.Glue.dP n)).map fun j => decide (dpN n ≤ (j + m) % IntMul.OpenAI.Glue.dP n)

/-- Where `descTrP` may write. -/
structure TrOk (dst rw rm : Fin HS) : Prop where
  lt : dst.val < 56
  ne : dst ≠ mOc ∧ dst ≠ zD ∧ dst ≠ zDp ∧ dst ≠ zEl ∧ dst ≠ rw ∧ dst ≠ rm
  rw56 : rw.val < 56
  rm56 : rm.val < 56
  rmO : rm ≠ mOc

/-- The registers `descTrP` reads. -/
structure TrRegs (t : IState HS) (n w m : ℕ) (rw rm : Fin HS) : Prop where
  hD : ∃ L, t.G zD = .int (IntMul.OpenAI.Glue.dP n : ℤ) :: L
  hDp : ∃ L, t.G zDp = .int (dpN n : ℤ) :: L
  hEl : ∃ L, t.G zEl = .int (ℓP n : ℤ) :: L
  hW : ∃ L, t.G rw = .int (w : ℤ) :: L
  hM : ∃ L, t.G rm = .int (m : ℤ) :: L

end NLogN.KFM

end

section
-- Source module: Solutions.KFMLineNeed
/-!
# KFM: the line-map interface `LineNeed` (hypothesis of the assembly)

Steps 3a (`A` lines) and 3c (`B₀` lines) of the source transform, on the arrays exactly as kmain
holds them, in the style of `P18IL`: one fixed table `kTable ext`, entries `eA`, `eB` and a
descriptor stack `dS` chosen before `n`; all size-dependent data on `dS`.

**Arrays.** After `Φ`, stack `0` holds `gflat zs ++ l`: one Gaussian item per point of the
padded box `∏_{i<d} t_i` (row-major, axis `0` outermost, the shape `shR d (tP d (ℓ−1) bL)` of
`PhiNeed` without its component axis), numerators at scale `2^p`, `p = pP n`. Here
`t_i = tB n i = r` if `d' ≤ i`, else `r/2` (`= 2^{ℓ−1+b_i}`, the axes of `TransNeed`'s `shPad`),
and the source lengths are `s_i = sB n i = srcN n i ≤ t_i`.

* `RepPad p s t zs u`: `zs` holds the `s`-box function `u` padded into the `t`-box: the item at
  a point with every coordinate `< s_i` is `2^p u(point)`, every other item is `0`.
* `RepFull p t zs w`: `zs` holds the `t`-box function `w` (`2^p w(point)` everywhere).

**Forward (`eA`, step 3a).** `RepPad zs u`, `‖u‖ ≤ 1/2` ↦ `RepFull zs' w` with
`‖w − tensCLM (kerA M.A) u‖ ≤ εA · 2^{−p}` for every `M : AxisMaps p α s t` (this is
`chain_concrete`'s `hAt`; `Grid p w` holds because `w` has integer numerators).
**Backward (`eB`, step 3c).** `RepFull ys y`, `‖y‖ ≤ 1` ↦ `RepPad ys' v` with
`‖v − tensCLM (kerB M.B) y‖ ≤ εB · 2^{−p}` (`hBt`).

The error constants are those of `tensor_fp` with Lemma 19's per-axis widths (`AxisMaps.hS`,
`hB0`): `εA = d (6 sWidth p α + 4)`, `εB = Σ_i (jIter p s_i t_i α (10 eWidth p α + 12) + 4)`.

Cost: as `P18IL`, `C₀ · V · Ncost · (log p + 1)^A` (rows `d p^{1/2+δ} α` and `d²(1+ℓ^τ)` with
the polylog slack). Descriptor: `descLine = [p, α, h, d, b_0..b_{d−1}, s_0..s_{d−1}]`,
`h = ℓ − 1`, `b_j = [d' ≤ j]` (0/1). The proof may use `TransNeed` (axis exposure).
-/

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH IntMul.OpenAI.RT IntMul.OpenAI.Glue IntMul.OpenAI.RCost

noncomputable section

/-- The source lengths as a box. -/
def sB (n : ℕ) : Fin (IntMul.OpenAI.Glue.dP n) → ℕ := fun i => srcN n i

/-- The padded lengths as a box (`r` from `d'` on, else `r/2`). -/
def tB (n : ℕ) : Fin (IntMul.OpenAI.Glue.dP n) → ℕ := fun i => if dpN n ≤ i.val then IntMul.OpenAI.Glue.rP n else IntMul.OpenAI.Glue.rP n / 2

/-- Coordinate `i` of the row-major index `x` over the box `t`. -/
def boxIx {d : ℕ} (t : Fin d → ℕ) (x : ℕ) (i : Fin d) : ℕ := digL (List.ofFn t) x i

/-- `zs` holds the `s`-box function `u` padded into the `t`-box (scale `2^p`, zeros outside). -/
def RepPad {d : ℕ} (p : ℕ) (s t : Fin d → ℕ) [∀ i, NeZero (s i)] (zs : List GI)
    (u : ((i : Fin d) → ZMod (s i)) → ℂ) : Prop :=
  zs.length = (List.ofFn t).prod ∧ ∀ x < (List.ofFn t).prod,
    ((∀ i, boxIx t x i < s i) →
      gC (zs.getD x 0) = 2 ^ p * u (fun i => ((boxIx t x i : ℕ) : ZMod (s i)))) ∧
    ((¬ ∀ i, boxIx t x i < s i) → zs.getD x 0 = 0)

/-- `zs` holds the `t`-box function `w` (scale `2^p`). -/
def RepFull {d : ℕ} (p : ℕ) (t : Fin d → ℕ) [∀ i, NeZero (t i)] (zs : List GI)
    (w : ((i : Fin d) → ZMod (t i)) → ℂ) : Prop :=
  zs.length = (List.ofFn t).prod ∧ ∀ x < (List.ofFn t).prod,
    gC (zs.getD x 0) = 2 ^ p * w (fun i => ((boxIx t x i : ℕ) : ZMod (t i)))

/-- Error constant of the `A` lines. -/
def epsA (p α d : ℕ) : ℝ := (d * (6 * sWidth p α + 4) : ℕ)

/-- Error constant of the `B₀` lines. -/
def epsB {d : ℕ} (p α : ℕ) (s t : Fin d → ℕ) : ℝ :=
  ((∑ i, (jIter p (s i) (t i) α * (10 * eWidth p α + 12) + 4) : ℕ) : ℝ)

/-- The descriptor of a line-map call: `[p, α, h, d, b_0..b_{d−1}, s_0..s_{d−1}]`. -/
def descLine (p α h d : ℕ) (bL : ℕ → Bool) (sF : ℕ → ℕ) : List ℤ :=
  (p : ℤ) :: (α : ℤ) :: (h : ℤ) :: (d : ℤ) ::
    (bitsZ d bL ++ (List.range d).map (fun j => (sF j : ℤ)))

/-- The line-map descriptor for `n`. -/
def descLineN (n : ℕ) : List ℤ :=
  descLine (pP n) (αP n) (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n)

/-- The cost allowed for one line-map phase (as `P18IL`). -/
def cLineU (n A : ℕ) : ℝ :=
  VP n * Ncost (6 * (IntMul.lg n : ℝ)) (IntMul.OpenAI.Glue.dP n) (KP n) (ℓP n) (αP n) *
    (Real.log (6 * (IntMul.lg n : ℝ)) + 1) ^ A

/-- **The line maps in IL, uniform** (hypothesis of the assembly). -/
def LineNeed : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eA eB : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ)
    (A n₁ : ℕ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ (Isym : List Sym) (n : ℕ), IntMul.OpenAI.Glue.n0 ≤ n → n₁ ≤ n →
  ∀ [∀ i, NeZero (NLogN.KFM.sB n i)] [∀ i, NeZero (NLogN.KFM.tB n i)],
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descLineN n →
    (∀ (zs : List GI) (u : ((i : Fin (IntMul.OpenAI.Glue.dP n)) → ZMod (NLogN.KFM.sB n i)) → ℂ),
      f 0 = gflat zs ++ l → RepPad (pP n) (NLogN.KFM.sB n) (NLogN.KFM.tB n) zs u → ‖u‖ ≤ 1 / 2 →
      ∃ (zs' : List GI) (w : ((i : Fin (IntMul.OpenAI.Glue.dP n)) → ZMod (NLogN.KFM.tB n i)) → ℂ) (c : ℕ),
        IRuns Isym (kTable ext) (.call eA) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat zs' ++ l))) c ∧
        RepFull (pP n) (NLogN.KFM.tB n) zs' w ∧ NLogN.KFB.GB (pP n + 2) zs' ∧
        (∀ M : AxisMaps (d := IntMul.OpenAI.Glue.dP n) (pP n) (αP n) (NLogN.KFM.sB n) (NLogN.KFM.tB n),
          ‖w - tensCLM (kerA M.A) u‖ ≤ epsA (pP n) (αP n) (IntMul.OpenAI.Glue.dP n) * hp (pP n)) ∧
        (c : ℝ) ≤ C₀ * cLineU n A) ∧
    (∀ (ys : List GI) (y : ((i : Fin (IntMul.OpenAI.Glue.dP n)) → ZMod (NLogN.KFM.tB n i)) → ℂ),
      f 0 = gflat ys ++ l → RepFull (pP n) (NLogN.KFM.tB n) ys y → ‖y‖ ≤ 1 →
      ∃ (ys' : List GI) (v : ((i : Fin (IntMul.OpenAI.Glue.dP n)) → ZMod (NLogN.KFM.sB n i)) → ℂ) (c : ℕ),
        IRuns Isym (kTable ext) (.call eB) (NLogN.KIL.encK s f)
          (NLogN.KIL.encK s (Function.update f 0 (gflat ys' ++ l))) c ∧
        RepPad (pP n) (NLogN.KFM.sB n) (NLogN.KFM.tB n) ys' v ∧ NLogN.KFB.GB (pP n + 2) ys' ∧
        (∀ M : AxisMaps (d := IntMul.OpenAI.Glue.dP n) (pP n) (αP n) (NLogN.KFM.sB n) (NLogN.KFM.tB n),
          ‖v - tensCLM (kerB M.B) y‖ ≤ epsB (pP n) (αP n) (NLogN.KFM.sB n) (NLogN.KFM.tB n) * hp (pP n)) ∧
        (c : ℝ) ≤ C₀ * cLineU n A)

end

end NLogN.KFM

end