Round-six κ development, definitions part 62

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

import Definitions.Def_IntMul_Kappa_R6_Defs61
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs20
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs31
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_R6_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs20
import Definitions.Def_IntMul_Kappa_R6_Defs22
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_R6_Defs23
import Definitions.Def_IntMul_Kappa_R6_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs28

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.SynthKron
/-!
# §7 Lemma 17: signed packing, centered extraction, negacyclic fold, truncation

All the arithmetic content of Lemma 17, stated over `ℤ` (and over a coefficient model for the
ring-level identification).

* **Packing** (`gam`, `dig`): with carry `γ₀ = 0`, `d_j = (u_j + γ_j) mod B`,
  `γ_{j+1} = (u_j + γ_j - d_j)/B`; `pack_digit`, `pack_carry` (`γ_j ∈ {-1,0}` when `|u_j| < B`),
  `pack_telescope` (`∑ u_j B^j = ∑ d_j B^j + γ_r B^r`), `pack_sign` (`γ_r = -1 ↔ A_u < 0`).
* `pack_bound`: `|u_j| ≤ c`, `2c < B` give `2|A_u| < B^r`.
* `cnv` (ordinary product coefficients), `eval_mul_cnv` (`A_a A_c = ∑_{j<2r} h_j B^j`),
  `abs_cnv_le` and `coeff_bound31` (`|h_j| ≤ r 2^{2p} < 2^{3p}`, `2·2^{3p} < B₀ = 2^{4p}`).
* `twos_complement_exists`: a fixed-width signed block representation `Z = ∑ q_j B^j + ε B^J`.
* **Extraction** (`cent`, `rho`): `extract` proves the residual identity, `ρ_j ∈ {0,1}`, exact
  recovery `ĥ_j = h_j`, and `ρ_J + ε = 0`; `kron_recover` is the instance of Lemma 17.
* **Negacyclic fold**: `fold_formula`, `co_mul` and `co_mul_gauss` (the Gaussian numerators of
  `f g` are `(ac - be) + i(ae + bc)` folded modulo `y^r + 1`).
* **Truncation**: `truncNum_div` (`trunc₀(H / 2^{p+ℓ})` is `H.tdiv 2^{p+ℓ}`), `Qp_normalized`.
* **Scaling by appending zeros**: `append_zeros`.
-/

set_option linter.unusedSectionVars false

namespace Synth

open Finset Butterfly

/-! ## 1. Signed packing -/

section Pack

variable (B : ℤ) (u : ℕ → ℤ)

/-- The packing carry `γ_j`. -/
def gam : ℕ → ℤ
  | 0 => 0
  | j + 1 => (u j + gam j) / B

variable {B}

end Pack

/-! ## 2. Ordinary product coefficients -/

/-! ## 3. Fixed-width two's complement -/

/-! ## 4. Centered extraction -/

/-! ## 5. The negacyclic fold and the ring product -/

/-! ## 6. Truncation of the normalized product -/

/-! ## 7. Scaling by `M = 2^m`: appending zero bits -/

end Synth

end

section
-- Source module: Solutions.KFV3Tab
/-!
# KFV §4: the `J_E` exponent table, one record at a time

Round `h` of Lemma 16 twists record `j` by `y^{E_j}` with
`E_j = roundEx L ℓ h P j = Σ_{i ∈ P} twE ℓ h (x_i)`, `x_i` the coordinate of axis `i` at address
`j`. In a slot layout every `x_i` is a bit sum of the binary address, so
`E_j = -Σ_{(c, k₁, k₂) ∈ T} c · bit_{k₁}(j) · bit_{k₂}(j)`: the mask bit (slot `h` of axis `i`)
times the linear form of the lower slots (`c = 2^{ℓ-h+t}`). This is a masked linear table.

* `svE Q M T`: one expression for `(-Σ c·bit·bit) mod Q` of the index in register `rN`
  (`bitE k = (j / 2^k) mod 2`); **`tabP`** loops over the records with a down-counter on `rN` and
  pushes the entries on stack `14`, ending with entry `0` on top (the layout `rotF` consumes).
* **`tabP_fsp`**: the table `(range N).map (fun j => (-tv T j) mod Q)`, cost
  `cLp N ((18|T| + 7)·10^7 (B+2)^2 + …) B` with `B = zsz U`, `U` bounding the index, the moduli,
  the coefficients and the sums. That is `O(|T| B²)` **per record**: `|T| ≤ D ℓ`, `B = O(log N + ℓ)`,
  so the bound is polylogarithmic per record and does not grow with the record length `r`.
* **`roundEx_slot`**: in any slot layout (`slotLayout hS`, in particular the paper's
  `paperLayout`) `roundEx … j = -tv (trips …) j`, so `sOf r (roundEx …) = tabEntry` with
  `Q = 2r`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFV

open IntMul RS KIL KFD KFB AModel

/-! ## 1. The expression -/

/-- The record index `j = J - 1` from the down-counter `J` on `rN`. -/
def jE : Ex HS := .add (.reg rN) (.lit (-1))

/-- Bit `k` of the index. -/
def bitE (k : ℕ) : Ex HS := .nmod (.ndiv jE (.lit ((2 : ℤ) ^ k))) (.lit 2)

/-- One term `c · bit_{k₁} · bit_{k₂}`. -/
def trmE (t : ℕ × ℕ × ℕ) : Ex HS := .mul (.mul (.lit (t.1 : ℤ)) (bitE t.2.1)) (bitE t.2.2)

/-- The sum of the terms. -/
def sumE : List (ℕ × ℕ × ℕ) → Ex HS
  | [] => .lit 0
  | t :: T => .add (trmE t) (sumE T)

/-- `(Q M - Σ) mod Q`. -/
def svE (Q M : ℕ) (T : List (ℕ × ℕ × ℕ)) : Ex HS :=
  .nmod (.add (.lit ((Q * M : ℕ) : ℤ)) (.neg (sumE T))) (.lit (Q : ℤ))

/-! ## 2. Evaluation, side conditions, bounds -/

/-! ## 3. The table loop -/

/-- One record: push the entry, count down. -/
def tabB (Q M : ℕ) (T : List (ℕ × ℕ × ℕ)) : RS :=
  .seq (.push 14 (svE Q M T)) (.asg rN (.add (.reg rN) (.lit (-1))))

/-- **The exponent-table program** for `N` records. -/
def tabP (Q M N : ℕ) (T : List (ℕ × ℕ × ℕ)) : RS :=
  .seq (.push rN (.lit (N : ℤ))) (.seq (.rep c1 (.lit (N : ℤ)) (tabB Q M T)) (.pop rN))

/-! ## 4. The table of a round in a slot layout -/

section Slot

open Finset Synth GlueLayout GlueError Butterfly

variable {D : ℕ} [NeZero D] {a : Fin D → ℕ} {arr : List ℕ}

/-! ### The opposite round: the negated exponent -/

end Slot

end NLogN.KFV

end

section
-- Source module: Solutions.KFV4Proc
/-!
# KFV §8: Lemma 16 forward and opposite as IL programs (paper layout)

* `fwdP Rc n = Rc (n-1); …; Rc 0` and `oppP Rc n = Rc 0; …; Rc (n-1)`;
  `fwd_ok` / `opp_ok`: by induction on the rounds, they compute `runDown F n` / the `foldl` of
  the rounds (`procQc` / `procQIc` of `KFV1Coef`).
* `layerCode h`: prefix rounds `h < b` by `p14Leaf` with one-bit chunks (`dK` row: individual
  kernels), the top round by `topCode`, chunk rounds by any Proposition 14 code `Cch h`
  (in the merged table: `KFM.prop14Ph_kTable`, packaged by `layerOK_chunk`).
* `fwdRound h = layerCode h ; J_E` (exponent table `trips … h` and `twC`),
  `oppRound h = J_{-E} ; layerCode h` (table `negTr (2r) (trips … h)`).
* **`lemma16_fwd_IL`**: `fwdP fwdRound ℓ` computes `procQc p (paperLayout) ℓ (partAxes al)
  (paperSel) ℓ`, i.e. (`co_procQ`) the coefficients of `GlueError.procQ`, the computed forward
  procedure of Lemma 16 / `GlueProp18`;
  **`lemma16_opp_IL`**: `oppP oppRound ℓ` computes `procQIc …` (`co_procQI`: `GlueProp18.procQI`).
  Cost: the sum of the round costs `layerCost h + cTab + cTw`.
-/

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

namespace NLogN.KFV

open IntMul KFC KFT KFU KFB KFH KFD KIL AModel Butterfly

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

/-! ## 1. Round induction -/

/-- Rounds `n-1, …, 0`. -/
def fwdP (Rc : ℕ → IStmt HS Pp) : ℕ → IStmt HS Pp
  | 0 => .skip
  | n + 1 => .seq (Rc n) (fwdP Rc n)

/-! ## 2. The rounds of the paper's layout -/

end NLogN.KFV

end

section
-- Source module: Solutions.KFWSub
/-!
# KFW: literals read from registers (the uniformity meta-theorem for register programs)

A uniform register program `U` reads its run-time parameters from registers (tops of stacks).
`RS.sub σ U` replaces each register `i` with `σ i = some v` by the literal `v`; the result is
the (non-uniform) program with baked-in literals, for which a spec is usually already proved.

**`FSp.of_sub`**: if `FSp (U.sub σ) s t c`, the registers of `σ` hold their values in `s`
(`Agree σ s`) and `U` never writes them, then `FSp U s t (400 c)`.  Also `fok_of_sub`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul NLogN.RS KFD

theorem Agree.congr {σ : Fin HS → Option ℤ} {s t : IState HS} (h : Agree σ s)
    (he : ∀ i, (σ i).isSome → t.G i = s.G i) : Agree σ t := by
  intro i v hi
  rw [he i (by simp [hi])]; exact h i v hi

end NLogN.KFW

end

section
-- Source module: Solutions.KFX5Head
/-!
# KFX §5: the header of the uniform row addition

From the row-addition parameters on the background stacks `36 … 45`
(`[mC^k, K, e, t, S0, B, r, H, i, j]`) the header computes the master registers `σMR` of
`l13U`: the third row `h ∉ {i, j}`, the sorted rows `s0 < s1 < s2`, the slots `px, py`, the
factors `N0 … N3` of the shape `shR`, `Q = 2^{fK}`, `2^K`, `2^ρ` (`ρ = e % K`), the swap flags,
`gx`, and (by a halving loop) `A = zsz V`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxRecDepth 20000

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## The sorted rows -/

/-! ## Expression combinators -/

theorem clean56 {e : Ex HS} (h : ∀ i ∈ e.regs, i.val < 56) : e.Clean := KFL.clean_all e h

section Comb

variable {u : IState HS} {Bb : ℕ}

theorem ESp.max {a b : Ex HS} {x y : ℤ} (ha : ESp a u Bb x) (hb : ESp b u Bb y)
    (h : zsz (x - y) ≤ Bb) : ESp (eMax a b) u Bb (max x y) :=
  ESp.sel (ESp.sub ha hb h) hb.clean ha.clean
    (fun hl => ESp.of_eq hb (by rw [max_eq_right (by linarith)]))
    (fun hl => ESp.of_eq ha (by rw [max_eq_left (by linarith)]))

theorem ESp.sq {a : Ex HS} {x : ℤ} (ha : ESp a u Bb x) (h : zsz (x * x) ≤ Bb) :
    ESp (eSq a) u Bb (x * x) := ESp.mul ha ha h

end Comb

/-! ## The parameter expressions -/

theorem rowσ_at (k K e t S0 B r H : ℕ) (i j : Fin mC) (q : Fin 10) :
    rowσ k K e t S0 B r H i j (KFW.rowR q) = some (rowVals k K e t S0 B r H i j q) := by
  have hq := q.isLt
  unfold rowσ KFW.rowR
  rw [dif_pos (by simp only; omega)]
  congr 2; ext; simp

/-! ## Arithmetic of the rows -/

/-! ## The shape factors -/

/-! ## Specifications of the parameter expressions -/

theorem mC_eq : mC = 1000000 := by norm_num [mC]

theorem f1_pos (k : ℕ) : 1 ≤ mC ^ k := Nat.one_le_pow _ _ (by norm_num)

section PFacts

variable {k K e T S0 B r H : ℕ} (hp : PF k K e T S0 B r)
include hp

theorem PF.eT : e < T := by
  have := hp.ht; have := Nat.mod_lt e (show 0 < K by have := hp.k1; omega)
  have := Nat.mod_le e K; omega

theorem PF.mT : mC ^ (k + 1) ≤ T := by
  have h1 : mC ^ (k + 1) - 1 ≤ K * (mC ^ (k + 1) - 1) := Nat.le_mul_of_pos_left _ hp.k1
  have := hp.he; have := hp.eT
  have : 1 ≤ mC ^ (k + 1) := Nat.one_le_pow _ _ (by norm_num)
  omega

theorem PF.fm : mC ^ k * mC ≤ T := by rw [← pow_succ]; exact hp.mT

theorem PF.mCT : mC ≤ T := by
  have := hp.fm; have := f1_pos k
  calc mC = 1 * mC := (one_mul _).symm
    _ ≤ mC ^ k * mC := Nat.mul_le_mul_right _ this
    _ ≤ T := hp.fm

theorem PF.TV : 2 ^ T ≤ VbR T S0 B r H := by
  unfold VbR
  have := hp.s0; have := hp.b; have := hp.r
  calc 2 ^ T = 1 * 2 ^ T * 1 := by ring
    _ ≤ B * 2 ^ T * S0 := Nat.mul_le_mul (Nat.mul_le_mul_right _ hp.b) hp.s0
    _ ≤ (B * 2 ^ T * S0) * (2 * r * (H + 1)) := Nat.le_mul_of_pos_right _ (by positivity)
    _ = 2 * (B * 2 ^ T * S0) * r * (H + 1) := by ring

end PFacts

section Par

variable {k K e T S0 B r H : ℕ} {i j : Fin mC} {u : IState HS} {Bb : ℕ}
  (hp : PF k K e T S0 B r) (hA : Agree (rowσ k K e T S0 B r H i j) u)
  (hBb : zsz ((VbR T S0 B r H : ℕ) : ℤ) ≤ Bb)

omit hA in
include hp hBb in
theorem TB : T + 1 ≤ Bb := by
  have h := zsz_nat_le (hp.TV (H := H))
  have e : zsz (((2 ^ T : ℕ)) : ℤ) = T + 1 := by push_cast; exact zsz_two_pow_r6c T
  omega

omit hA in
include hp hBb in
theorem zT {v : ℤ} (h0 : -(T : ℤ) ≤ v) (h1 : v ≤ T) : zsz v ≤ Bb :=
  le_trans (zsz_mono_r6c (b := (T : ℤ)) (by
    rw [Int.natAbs_natCast]
    exact Int.ofNat_le.mp (by rw [Int.natCast_natAbs]; exact abs_le.mpr ⟨h0, h1⟩))) (le_trans (zsz_natCast_le_self T) (by have := TB hp hBb; omega))

omit hA in
include hp hBb in
theorem zS {v : ℤ} (h0 : -(10 ^ 24 : ℤ) ≤ v) (h1 : v ≤ 10 ^ 24) : zsz v ≤ Bb := by
  have h80 : zsz v ≤ 80 := zsz_le_of_lt (by
    have : (v.natAbs : ℤ) ≤ 10 ^ 24 := by rw [Int.natCast_natAbs]; exact abs_le.mpr ⟨h0, h1⟩
    have : v.natAbs ≤ 10 ^ 24 := by exact_mod_cast this
    have : (10 : ℕ) ^ 24 < 2 ^ 80 := by norm_num
    omega)
  have := TB hp hBb; have := hp.mCT; rw [mC_eq] at this; omega

include hp hA hBb

omit hp hBb in
theorem sPr (q : Fin 10) (hb : zsz (rowVals k K e T S0 B r H i j q) ≤ Bb) :
    ESp (pr q) u Bb (rowVals k K e T S0 B r H i j q) :=
  ESp.ofAgree hA (rowσ_at k K e T S0 B r H i j q)
    (by have := q.isLt; simp only [KFW.rowR]; omega) hb

omit hp hBb in
theorem sPr' (q : Fin 10) {v : ℤ} (hv : rowVals k K e T S0 B r H i j q = v) (hb : zsz v ≤ Bb) :
    ESp (pr q) u Bb v := hv ▸ sPr hA q (hv ▸ hb)

theorem sIp : ESp (pr 8) u Bb ((i : ℕ) : ℤ) :=
  sPr' hA 8 rfl (zT hp hBb (by omega) (by
    have := i.isLt; have := hp.mCT; exact_mod_cast (by omega : (i : ℕ) ≤ T)))

theorem sJp : ESp (pr 9) u Bb ((j : ℕ) : ℤ) :=
  sPr' hA 9 rfl (zT hp hBb (by omega) (by
    have := j.isLt; have := hp.mCT; exact_mod_cast (by omega : (j : ℕ) ≤ T)))

omit hA in
theorem sLit (c : ℤ) (h0 : -(10 ^ 24 : ℤ) ≤ c) (h1 : c ≤ 10 ^ 24) : ESp (.lit c) u Bb c :=
  ESp.lit (zS hp hBb h0 h1)

omit hp hA hBb in
theorem hR_le (i j : ℕ) : hR i j ≤ 2 := by unfold hR; split_ifs <;> omega

theorem sHr_r6c : ESp eHr u Bb ((hR i j : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_eq i.isLt mC_eq
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_eq j.isLt mC_eq
  have I0 : (0 : ℤ) ≤ ((i : ℕ) : ℤ) := Nat.cast_nonneg _
  have J0 : (0 : ℤ) ≤ ((j : ℕ) : ℤ) := Nat.cast_nonneg _
  have I1 : ((i : ℕ) : ℤ) ≤ 10 ^ 6 := by exact_mod_cast hi.le
  have J1 : ((j : ℕ) : ℤ) ≤ 10 ^ 6 := by exact_mod_cast hj.le
  have hIJ : ((i : ℕ) : ℤ) * ((j : ℕ) : ℤ) ≤ 10 ^ 12 := by nlinarith
  refine ESp.sel (ESp.neg (ESp.mul (sIp hp hA hBb) (sJp hp hA hBb)
    (zS hp hBb (by nlinarith) (by nlinarith))))
    (clean56 (by decide)) (clean56 (by decide)) (fun hl => ?_) (fun hl => ?_)
  · have h1 : (i : ℕ) ≠ 0 := by rintro h; simp [h] at hl
    have h2 : (j : ℕ) ≠ 0 := by rintro h; simp [h] at hl
    have : hR i j = 0 := by simp [hR, h1, h2]
    rw [this]; exact ESp.of_eq (sLit hp hBb 0 (by norm_num) (by norm_num)) (by simp)
  · have h0 : (i : ℕ) = 0 ∨ (j : ℕ) = 0 := by
      by_contra hc; push Not at hc
      have a1 : (0 : ℤ) < ((i : ℕ) : ℤ) := by exact_mod_cast Nat.pos_of_ne_zero hc.1
      have a2 : (0 : ℤ) < ((j : ℕ) : ℤ) := by exact_mod_cast Nat.pos_of_ne_zero hc.2
      have : (0 : ℤ) < ((i : ℕ) : ℤ) * ((j : ℕ) : ℤ) := mul_pos a1 a2
      exact hl (by linarith)
    have l1 := sLit (u := u) hp hBb 1 (by norm_num) (by norm_num)
    have pI0 : 0 ≤ (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) := mul_self_nonneg _
    have pJ0 : 0 ≤ (((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1) := mul_self_nonneg _
    have pI1 : (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) ≤ 10 ^ 12 := by nlinarith
    have pJ1 : (((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1) ≤ 10 ^ 12 := by nlinarith
    have pP : (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) *
        ((((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1)) ≤ 10 ^ 24 := by
      calc _ ≤ (10 ^ 12 : ℤ) * 10 ^ 12 := mul_le_mul pI1 pJ1 pJ0 (by norm_num)
        _ = 10 ^ 24 := by norm_num
    have pP0 := mul_nonneg pI0 pJ0
    have sI1 := ESp.sq (ESp.sub (sIp hp hA hBb) l1 (zS hp hBb (by linarith) (by linarith)))
      (zS hp hBb (by linarith) (by linarith))
    have sJ1 := ESp.sq (ESp.sub (sJp hp hA hBb) l1 (zS hp hBb (by linarith) (by linarith)))
      (zS hp hBb (by linarith) (by linarith))
    refine ESp.sel (ESp.neg (ESp.mul sI1 sJ1 (zS hp hBb (by linarith) pP)))
      (clean_lit_r6c _) (clean_lit_r6c _) (fun hl2 => ?_) (fun hl2 => ?_)
    · have h1 : (i : ℕ) ≠ 1 := by rintro h; simp [h] at hl2
      have h2 : (j : ℕ) ≠ 1 := by rintro h; simp [h] at hl2
      have : hR i j = 1 := by unfold hR; split_ifs <;> omega
      rw [this]; exact ESp.of_eq l1 (by simp)
    · have h3 : (i : ℕ) = 1 ∨ (j : ℕ) = 1 := by
        by_contra hc; push Not at hc
        have a1 : ((i : ℕ) : ℤ) - 1 ≠ 0 := by
          intro h; apply hc.1; exact_mod_cast (by linarith : ((i : ℕ) : ℤ) = 1)
        have a2 : ((j : ℕ) : ℤ) - 1 ≠ 0 := by
          intro h; apply hc.2; exact_mod_cast (by linarith : ((j : ℕ) : ℤ) = 1)
        have := mul_pos (mul_self_pos.2 a1) (mul_self_pos.2 a2)
        exact hl2 (by linarith)
      have : hR i j = 2 := by unfold hR; split_ifs <;> omega
      rw [this]; exact ESp.of_eq (sLit hp hBb 2 (by norm_num) (by norm_num)) (by simp)

theorem sBm : ESp eBm u Bb ((max (i : ℕ) (j : ℕ) : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_eq i.isLt mC_eq
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_eq j.isLt mC_eq
  exact ESp.of_eq (ESp.max (sIp hp hA hBb) (sJp hp hA hBb) (zS hp hBb (by omega) (by omega)))
    (by push_cast; rfl)

theorem sT2 : ESp eT2 u Bb ((s2R i j : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_eq i.isLt mC_eq
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_eq j.isLt mC_eq
  have := hR_le i j
  exact ESp.of_eq (ESp.max (sHr_r6c hp hA hBb) (sBm hp hA hBb) (zS hp hBb (by omega) (by omega)))
    (by unfold s2R; push_cast; rfl)

end Par

end NLogN.KFX

end

section
-- Source module: Solutions.R6IL2Head
/-!
# Round six, item language (I2): the row-addition header for any label dimension `m`

Parametric copy of the `m`-dependent part of `KFX5Head` (the frozen file has the OpenAI label
dimension `mC = 100^3` hard-wired): the register assignment `rowσ m …` of the ten row-addition
parameters `[m^k, K, e, t, S0, B, r, H, i, j]` (`i j : Fin m`), the shape factors `N0R … N3R`,
the admissibility facts `PF m …` (now also `6 ≤ K` and `16 ≤ m ≤ 10^6`; round six has `m = 576`),
and the specifications `x…` of the header expressions (the expressions themselves are the frozen
ones: they read `m^k` from a register, so they do not depend on `m`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option maxRecDepth 20000

namespace IntMul.Kappa.R6.IL2

open IntMul NLogN RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH
  NLogN.KFX AModel Butterfly

/-! ## The row-addition parameters for label dimension `m` -/

theorem rowσ_at {m : ℕ} (k K e t S0 B r H : ℕ) (i j : Fin m) (q : Fin 10) :
    rowσ m k K e t S0 B r H i j (KFW.rowR q) = some (rowVals m k K e t S0 B r H i j q) := by
  have hq := q.isLt
  unfold rowσ KFW.rowR
  rw [dif_pos (by simp only; omega)]
  congr 2; ext; simp

/-! ## The shape factors -/

/-! ## Specifications of the parameter expressions -/

theorem f1_pos {m : ℕ} (hm : 1 ≤ m) (k : ℕ) : 1 ≤ m ^ k := Nat.one_le_pow _ _ hm

section PFacts

variable {m k K e T S0 B r H : ℕ} (hp : PF m k K e T S0 B r)
include hp

theorem PF.eT : e < T := by
  have := hp.ht; have := Nat.mod_lt e (show 0 < K by have := hp.k1; omega)
  have := Nat.mod_le e K; omega

theorem PF.mT : m ^ (k + 1) ≤ T := by
  have h1 : m ^ (k + 1) - 1 ≤ K * (m ^ (k + 1) - 1) := Nat.le_mul_of_pos_left _ hp.k1
  have := hp.he; have := hp.eT
  have : 1 ≤ m ^ (k + 1) := Nat.one_le_pow _ _ hp.m1
  omega

theorem PF.T80 : 80 ≤ T := by
  have h1 : m ≤ m ^ (k + 1) := Nat.le_self_pow (by omega) m
  have h2 : 6 * 15 ≤ K * (m ^ (k + 1) - 1) :=
    Nat.mul_le_mul hp.k6 (by have := hp.m16; omega)
  have := hp.he; have := hp.eT
  omega

theorem PF.fm : m ^ k * m ≤ T := by rw [← pow_succ]; exact hp.mT

theorem PF.mCT : m ≤ T := by
  have := hp.fm; have := f1_pos hp.m1 k
  calc m = 1 * m := (one_mul _).symm
    _ ≤ m ^ k * m := Nat.mul_le_mul_right _ this
    _ ≤ T := hp.fm

theorem PF.TV : 2 ^ T ≤ VbR T S0 B r H := by
  unfold VbR
  have := hp.s0; have := hp.b; have := hp.r
  calc 2 ^ T = 1 * 2 ^ T * 1 := by ring
    _ ≤ B * 2 ^ T * S0 := Nat.mul_le_mul (Nat.mul_le_mul_right _ hp.b) hp.s0
    _ ≤ (B * 2 ^ T * S0) * (2 * r * (H + 1)) := Nat.le_mul_of_pos_right _ (by positivity)
    _ = 2 * (B * 2 ^ T * S0) * r * (H + 1) := by ring

end PFacts

section Par

variable {m k K e T S0 B r H : ℕ} {i j : Fin m} {u : IState HS} {Bb : ℕ}
  (hp : PF m k K e T S0 B r) (hA : Agree (rowσ m k K e T S0 B r H i j) u)
  (hBb : zsz ((VbR T S0 B r H : ℕ) : ℤ) ≤ Bb)

omit hA in
include hp hBb in
theorem TB : T + 1 ≤ Bb := by
  have h := zsz_nat_le (hp.TV (H := H))
  have e : zsz (((2 ^ T : ℕ)) : ℤ) = T + 1 := by push_cast; exact zsz_two_pow_r6c T
  omega

omit hA in
include hp hBb in
theorem zT {v : ℤ} (h0 : -(T : ℤ) ≤ v) (h1 : v ≤ T) : zsz v ≤ Bb :=
  le_trans (zsz_mono_r6c (b := (T : ℤ)) (by
    rw [Int.natAbs_natCast]
    exact Int.ofNat_le.mp (by rw [Int.natCast_natAbs]; exact abs_le.mpr ⟨h0, h1⟩))) (le_trans (zsz_natCast_le_self T) (by have := TB hp hBb; omega))

omit hA in
include hp hBb in
theorem zS {v : ℤ} (h0 : -(10 ^ 24 : ℤ) ≤ v) (h1 : v ≤ 10 ^ 24) : zsz v ≤ Bb := by
  have h80 : zsz v ≤ 80 := zsz_le_of_lt (by
    have : (v.natAbs : ℤ) ≤ 10 ^ 24 := by rw [Int.natCast_natAbs]; exact abs_le.mpr ⟨h0, h1⟩
    have : v.natAbs ≤ 10 ^ 24 := by exact_mod_cast this
    have : (10 : ℕ) ^ 24 < 2 ^ 80 := by norm_num
    omega)
  have := TB hp hBb; have := hp.T80; omega

include hp hA hBb

omit hp hBb in
theorem sPr (q : Fin 10) (hb : zsz (rowVals m k K e T S0 B r H i j q) ≤ Bb) :
    ESp (pr q) u Bb (rowVals m k K e T S0 B r H i j q) :=
  ESp.ofAgree hA (rowσ_at k K e T S0 B r H i j q)
    (by have := q.isLt; simp only [KFW.rowR]; omega) hb

omit hp hBb in
theorem sPr' (q : Fin 10) {v : ℤ} (hv : rowVals m k K e T S0 B r H i j q = v) (hb : zsz v ≤ Bb) :
    ESp (pr q) u Bb v := hv ▸ sPr hA q (hv ▸ hb)

theorem sIp : ESp (pr 8) u Bb ((i : ℕ) : ℤ) :=
  sPr' hA 8 rfl (zT hp hBb (by omega) (by
    have := i.isLt; have := hp.mCT; exact_mod_cast (by omega : (i : ℕ) ≤ T)))

theorem sJp : ESp (pr 9) u Bb ((j : ℕ) : ℤ) :=
  sPr' hA 9 rfl (zT hp hBb (by omega) (by
    have := j.isLt; have := hp.mCT; exact_mod_cast (by omega : (j : ℕ) ≤ T)))

omit hA in
theorem sLit (c : ℤ) (h0 : -(10 ^ 24 : ℤ) ≤ c) (h1 : c ≤ 10 ^ 24) : ESp (.lit c) u Bb c :=
  ESp.lit (zS hp hBb h0 h1)

omit hp hA hBb in
theorem hR_le (i j : ℕ) : hR i j ≤ 2 := by unfold hR; split_ifs <;> omega

theorem sHr_r6c : ESp eHr u Bb ((hR i j : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_le i.isLt hp.mle
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_le j.isLt hp.mle
  have I0 : (0 : ℤ) ≤ ((i : ℕ) : ℤ) := Nat.cast_nonneg _
  have J0 : (0 : ℤ) ≤ ((j : ℕ) : ℤ) := Nat.cast_nonneg _
  have I1 : ((i : ℕ) : ℤ) ≤ 10 ^ 6 := by exact_mod_cast hi.le
  have J1 : ((j : ℕ) : ℤ) ≤ 10 ^ 6 := by exact_mod_cast hj.le
  have hIJ : ((i : ℕ) : ℤ) * ((j : ℕ) : ℤ) ≤ 10 ^ 12 := by nlinarith
  refine ESp.sel (ESp.neg (ESp.mul (sIp hp hA hBb) (sJp hp hA hBb)
    (zS hp hBb (by nlinarith) (by nlinarith))))
    (clean56 (by decide)) (clean56 (by decide)) (fun hl => ?_) (fun hl => ?_)
  · have h1 : (i : ℕ) ≠ 0 := by rintro h; simp [h] at hl
    have h2 : (j : ℕ) ≠ 0 := by rintro h; simp [h] at hl
    have : hR i j = 0 := by simp [hR, h1, h2]
    rw [this]; exact ESp.of_eq (sLit hp hBb 0 (by norm_num) (by norm_num)) (by simp)
  · have h0 : (i : ℕ) = 0 ∨ (j : ℕ) = 0 := by
      by_contra hc; push Not at hc
      have a1 : (0 : ℤ) < ((i : ℕ) : ℤ) := by exact_mod_cast Nat.pos_of_ne_zero hc.1
      have a2 : (0 : ℤ) < ((j : ℕ) : ℤ) := by exact_mod_cast Nat.pos_of_ne_zero hc.2
      have : (0 : ℤ) < ((i : ℕ) : ℤ) * ((j : ℕ) : ℤ) := mul_pos a1 a2
      exact hl (by linarith)
    have l1 := sLit (u := u) hp hBb 1 (by norm_num) (by norm_num)
    have pI0 : 0 ≤ (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) := mul_self_nonneg _
    have pJ0 : 0 ≤ (((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1) := mul_self_nonneg _
    have pI1 : (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) ≤ 10 ^ 12 := by nlinarith
    have pJ1 : (((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1) ≤ 10 ^ 12 := by nlinarith
    have pP : (((i : ℕ) : ℤ) - 1) * (((i : ℕ) : ℤ) - 1) *
        ((((j : ℕ) : ℤ) - 1) * (((j : ℕ) : ℤ) - 1)) ≤ 10 ^ 24 := by
      calc _ ≤ (10 ^ 12 : ℤ) * 10 ^ 12 := mul_le_mul pI1 pJ1 pJ0 (by norm_num)
        _ = 10 ^ 24 := by norm_num
    have pP0 := mul_nonneg pI0 pJ0
    have sI1 := ESp.sq (ESp.sub (sIp hp hA hBb) l1 (zS hp hBb (by linarith) (by linarith)))
      (zS hp hBb (by linarith) (by linarith))
    have sJ1 := ESp.sq (ESp.sub (sJp hp hA hBb) l1 (zS hp hBb (by linarith) (by linarith)))
      (zS hp hBb (by linarith) (by linarith))
    refine ESp.sel (ESp.neg (ESp.mul sI1 sJ1 (zS hp hBb (by linarith) pP)))
      (clean_lit_r6c _) (clean_lit_r6c _) (fun hl2 => ?_) (fun hl2 => ?_)
    · have h1 : (i : ℕ) ≠ 1 := by rintro h; simp [h] at hl2
      have h2 : (j : ℕ) ≠ 1 := by rintro h; simp [h] at hl2
      have : hR i j = 1 := by unfold hR; split_ifs <;> omega
      rw [this]; exact ESp.of_eq l1 (by simp)
    · have h3 : (i : ℕ) = 1 ∨ (j : ℕ) = 1 := by
        by_contra hc; push Not at hc
        have a1 : ((i : ℕ) : ℤ) - 1 ≠ 0 := by
          intro h; apply hc.1; exact_mod_cast (by linarith : ((i : ℕ) : ℤ) = 1)
        have a2 : ((j : ℕ) : ℤ) - 1 ≠ 0 := by
          intro h; apply hc.2; exact_mod_cast (by linarith : ((j : ℕ) : ℤ) = 1)
        have := mul_pos (mul_self_pos.2 a1) (mul_self_pos.2 a2)
        exact hl2 (by linarith)
      have : hR i j = 2 := by unfold hR; split_ifs <;> omega
      rw [this]; exact ESp.of_eq (sLit hp hBb 2 (by norm_num) (by norm_num)) (by simp)

theorem sBm : ESp eBm u Bb ((max (i : ℕ) (j : ℕ) : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_le i.isLt hp.mle
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_le j.isLt hp.mle
  exact ESp.of_eq (ESp.max (sIp hp hA hBb) (sJp hp hA hBb) (zS hp hBb (by omega) (by omega)))
    (by push_cast; rfl)

theorem sT2 : ESp eT2 u Bb ((s2R i j : ℕ) : ℤ) := by
  have hi : (i : ℕ) < 1000000 := lt_of_lt_of_le i.isLt hp.mle
  have hj : (j : ℕ) < 1000000 := lt_of_lt_of_le j.isLt hp.mle
  have := hR_le i j
  exact ESp.of_eq (ESp.max (sHr_r6c hp hA hBb) (sBm hp hA hBb) (zS hp hBb (by omega) (by omega)))
    (by unfold s2R; push_cast; rfl)

end Par

end IntMul.Kappa.R6.IL2

end

section
-- Source module: Solutions.KFMRep
/-!
# KFM: arrays as lists and as box functions

The machine holds the arrays of the chain as row-major lists of Gaussian integers (numerators
at scale `2^p`); `LineNeed`/`ChirpNeedR` relate them to box functions by `RepPad`/`RepFull`.
Here the box function of a list is made explicit, so every list the machine produces names its
function:

* `kL K`: the coordinates of a box point as a list; `boxIx` is `decode` (`digL_decode`).
* **`funF p t zs`** (full `t`-box) and **`funP p s t zs`** (the `s`-box read out of the padded
  `t`-box): `toC (zs[enc K]) / 2^p`.
* **`repFull_iff`**, **`repPad_iff`**: a list represents exactly its own function (so the function
  a call returns is determined by the returned list).
* `grid_funF`, `grid_funP`: these functions are on the grid of `Q_p`.
* Pointwise list maps: **`RepPad.smul`** (`g z = c·z`, e.g. `× 2^γ`), **`RepPad.conj`**,
  **`RepPad.gmul`** (`zipWith (gmulT p)` is `Q_p(u · v)`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

open IntMul KIL KFB IntMul.HvdH AModel Complex

noncomputable section

/-! ## Coordinates -/

variable {d : ℕ}

/-! ## The function of a list -/

/-- The full `t`-box function of a row-major list. -/
def funF (p : ℕ) (t : Fin d → ℕ) (zs : List GI) (K : (i : Fin d) → ZMod (t i)) : ℂ :=
  toC (zs.getD (encode (List.ofFn t) (kL K)) 0) / 2 ^ p

/-! ## Grid -/

/-! ## Pointwise maps -/

end

end NLogN.KFM

end

section
-- Source module: Solutions.J6SegLn12
/-!
# Segmented inverse (S2), machine side 12: the `B₀` pass in the round-six regime

* `LJ_length_ge`: the near-boundary line has at least `2w + 1` positions (`[0,w)`, `[s-w,s)`
  and the cut `λ`), so the cyclic coupling window `K = w` fits;
* `FitSpec6 M`: the per-axis properties of `r6_axisMaps_fit` (`‖B_i‖ ≤ 1/2`, the `S̃` and
  `B̃₀` bounds, `B̃₀ 0 = 0`); `r6_fitSpec`: such `M` exist for `n ≥ n₁`;
* `mapsLine6`: the machine's line maps (`lineB` with `λ = lamP d`, `w = K = wF d`,
  `n_c = t_i/λ`, `R = ⌊p/7⌋`, `P = segPF p d s_i`);
* **`r6_passB`**: for `n ≥ n₁`, every source list, every `M` with `FitSpec6 M` and every
  `RepFull ys y`, `‖y‖ ≤ 1`: the `tensorGo` of the machine's line maps is `RepPad` of a `v`
  with `GB (p+2)` and `‖v − tensCLM (kerB M.B) y‖ ≤ errW6 · 2^{-p}` — the representation and
  error part of the `eB` clause of `LineBody6`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Complex

namespace J6Seg
open IntMul IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf NLogN.KFM NLogN.KFY IntMul.OpenAI.RT
open IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

/-! ## Size of the near-boundary line -/

/-! ## The round-six statement -/

section r6
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ) [∀ i, NeZero (sD6 src D i)]
  [∀ i, NeZero (tD6 P n D i)]

/-- The per-axis properties of the maps fixed by `r6_axisMaps_fit`. -/
def FitSpec6 (M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D)) : Prop :=
  ∀ i : Fin (D + 1), ‖M.B i‖ ≤ 1 / 2 ∧
    (∀ U : ℕ → ℤ × ℤ, (∀ k, ‖IntMul.HvdH.P47.toC (U k)‖ ≤ 2 ^ pP6 P n) →
      ∀ k : ZMod (tD6 P n D i),
      ‖IntMul.HvdH.P47.toC (Sapprox (pP6 P n) (sD6 src D i) (tD6 P n D i) (αN6 P n) U k.val) -
        2 ^ pP6 P n * M.A i (fun j => IntMul.HvdH.P47.toC (U j.val) / 2 ^ pP6 P n) k‖
        ≤ 6 * sWidth (pP6 P n) (αN6 P n) + 4) ∧
    (∀ W : ℕ → ℤ × ℤ, (∀ k, ‖IntMul.HvdH.P47.toC (W k)‖ ≤ 2 ^ pP6 P n) →
      ∀ l : ZMod (sD6 src D i),
      ‖IntMul.HvdH.P47.toC (B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i))
          (pP6 P n / 7) (lamP (dP6 P n)) (wF (dP6 P n))
          (sD6 src D i) (tD6 P n D i) (αN6 P n) W l.val) -
        2 ^ pP6 P n * M.B i (fun k => IntMul.HvdH.P47.toC (W k.val) / 2 ^ pP6 P n) l‖ ≤ 9) ∧
    B0seg (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sD6 src D i)) (pP6 P n / 7)
      (lamP (dP6 P n)) (wF (dP6 P n)) (sD6 src D i) (tD6 P n D i) (αN6 P n)
      (fun _ => (0, 0)) = fun _ => (0, 0)

/-- The machine's `B₀` line maps (axis `i`: `t_i`-lines to `t_i`-lines). -/
noncomputable def mapsLine6 : List (ℕ × (List GI → List GI)) :=
  (List.range (D + 1)).map fun i => ((List.ofFn (tD6 P n D)).getD i 1,
    lineB (pP6 P n) (segPF (pP6 P n) (dP6 P n) ((List.ofFn (sD6 src D)).getD i 1)) (pP6 P n / 7)
      ((List.ofFn (sD6 src D)).getD i 1) ((List.ofFn (tD6 P n D)).getD i 1)
      (lamP (dP6 P n)) (wF (dP6 P n)) (αN6 P n) (wF (dP6 P n))
      ((List.ofFn (tD6 P n D)).getD i 1 / lamP (dP6 P n)))

end r6

end J6Seg

end

section
-- Source module: Solutions.J6AMath6
/-!
# A lines (PR #5 block chirp), part 6: `ALineHyp6` from one IL obligation

* `HA6`: the half-block `H = 2^{⌊log₂ m⌋}` (`m = sWidth p α`), so `1 ≤ H ≤ m` and `2H` is a
  power of two.
* `mapsA6`: the machine's `A` line maps, `chirpC` along every axis.
* `AIL6 P tab`: a procedure `eA` turns `gflat zs ++ l` into
  `gflat (tensorGo (mapsA6 …) zs) ++ l`, exactly, at cost `≤ C₀ · cU6 P n A`.
* **`ALineHyp6_of_AIL6`**: `AIL6 P tab → ALineHyp6 P tab` (`P.Ok`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Complex

namespace J6Seg
open IntMul IntMul.HvdH IntMul.HvdH.Ref IntMul.HvdH.RefPf NLogN.KFM NLogN.KFY IntMul.OpenAI.RT
open NLogN NLogN.KIL NLogN.KFB AModel
open IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

/-- The half-block `2^{⌊log₂ m⌋}`. -/
noncomputable def HA6 (P : Prm) (n : ℕ) : ℕ := 2 ^ Nat.log 2 (sWidth (pP6 P n) (αN6 P n))

/-- The machine's `A` line maps. -/
noncomputable def mapsA6 (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ) : List (ℕ × (List GI → List GI)) :=
  J6A.mapsGen (tD6 P n D) fun i => J6A.chirpC (pP6 P n) ((List.ofFn (sD6 src D)).getD i 1)
    ((List.ofFn (tD6 P n D)).getD i 1) (αN6 P n) (HA6 P n)

end J6Seg

end

section
-- Source module: Solutions.J6SegSw1
/-!
# B-line machine, sweep 1: in-place axis maps

The machine keeps the array in its row-major layout and applies the line map of axis `i` in
place (no axis rotation). For a box `dims` and an axis `i`, the array is `(pre, n, post)`
(`pre = ∏_{j<i}`, `n = dims_i`, `post = ∏_{j>i}`), and

* `axisL n post f L`: every `(n, post)` block is transposed, `f` is applied to each of its `post`
  lines, and the block is transposed back;
* **`axisL_getD`**: entry `b (n·post) + a·post + c` of `axisL n post f L` is entry `a` of `f`
  applied to the line `k ↦ L[b (n·post) + k·post + c]`;
* **`digL_split`**: the row-major digits of `b (n·post) + a·post + c`;
* **`axisL_listOf`**: on `listOf dims g`, `axisL` is the slice map `j ↦ A (k ↦ g (j[i ↦ k])) (j i)`.
-/

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY

namespace J6Seg

/-! ## Products of a list around a position -/

/-! ## Row-major digits of a split index -/

/-! ## In-place axis maps -/

section axis
variable {α : Type*} [Inhabited α]

/-- The line through `b, c` of a `(pre, n, post)` array. -/
def lineAt (n post : ℕ) (L : List α) (b c : ℕ) : List α :=
  (List.range n).map fun k => L.getD (b * (n * post) + k * post + c) default

/-- The transposed block of one `(n, post)` block. -/
def blkImg (n post : ℕ) (f : List α → List α) (B : List α) : List α :=
  transposeL post n ((IntMul.HvdH.Ref.chunkL n (transposeL n post B)).flatMap f)

/-- In-place application of the line map `f` along the middle axis of a `(pre, n, post)` array. -/
def axisL (n post : ℕ) (f : List α → List α) (L : List α) : List α :=
  (IntMul.HvdH.Ref.chunkL (n * post) L).flatMap (blkImg n post f)

/-- The in-place sweep: axes `0, …, k-1` in order. -/
def sweepL (dims : List ℕ) (F : ℕ → List α → List α) : ℕ → List α → List α
  | 0, L => L
  | k + 1, L => axisL (dims.getD k 1) (dims.drop (k + 1)).prod (F k) (sweepL dims F k L)

end axis

/-! ## The sweep is the tensor product -/

/-- The line maps of `A` (identity beyond `K`). -/
def linesOf (K : ℕ) (dims : List ℕ) (A : Fin K → (ℕ → ℤ × ℤ) → (ℕ → ℤ × ℤ)) :
    ℕ → List (ℤ × ℤ) → List (ℤ × ℤ) :=
  fun i => if h : i < K then fun X => (List.range (dims.getD i 1)).map
    (A ⟨i, h⟩ fun k => X.getD k default) else id

end J6Seg

end

section
-- Source module: Solutions.J6SegSw2
/-!
# B-line machine, sweep 2: the per-axis passes on line representations

A `(pre, n, post)` array `L` *represents* the lines `φ b c` (`LRep pre n post L φ`) when
`L[b (n·post) + a·post + c] = (φ b c)[a]`. The machine's passes act on representations:

* **`LRep_axisL`**: the in-place axis map applies `f` to every line;
* **`LRep_slabPass`**: a monotone slab pass (output slab `l` = `h l` of input slab `src l`, or
  zeros) applies `slabLine` to every line (selection, `J` gather and scatter, output);
* **`LRep_kerPass`**: expose `(A, m, post) → (A, post, m)` (`blkTg`), apply a kernel to each
  contiguous `m`-row (indexed by its block), expose back;
* **`LRep_split` / `LRep_join`**: `(pre, nc·λ, post)` is `(pre·nc, λ, post)`;
* **`LRep_chunkPass`**: the chunk kernel `chunksG g λ nc` on every line, by one `λ`-exposure.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY

namespace J6Seg

section passes
variable {α β : Type*} [Inhabited α] [Inhabited β]

/-- `L` is a `(pre, n, post)` array whose lines are `φ b c`. -/
def LRep (pre n post : ℕ) (L : List α) (φ : ℕ → ℕ → List α) : Prop :=
  L.length = pre * (n * post) ∧ (∀ b < pre, ∀ c < post, (φ b c).length = n) ∧
  ∀ b < pre, ∀ a < n, ∀ c < post,
    L.getD (b * (n * post) + a * post + c) default = (φ b c).getD a default

/-! ## Slab passes -/

/-- One output slab: input slab `k` mapped by `h`, or zeros. -/
def slabOf (B : List α) (post : ℕ) (src : Option ℕ) (h : α → β) : List β :=
  match src with
  | some k => ((B.drop (k * post)).take post).map h
  | none => List.replicate post default

/-- **A slab pass**: in each `(n, post)` block, output slab `l < n'` is `h l` applied to input
slab `src l` (or zeros when `src l = none`). -/
def slabPass (n n' post : ℕ) (src : ℕ → Option ℕ) (h : ℕ → α → β) (L : List α) : List β :=
  (IntMul.HvdH.Ref.chunkL (n * post) L).flatMap fun B => (List.range n').flatMap fun l => slabOf B post (src l) (h l)

/-- The line map of a slab pass. -/
def slabLine (n' : ℕ) (src : ℕ → Option ℕ) (h : ℕ → α → β) (x : List α) : List β :=
  (List.range n').map fun l => match src l with
    | some k => h l (x.getD k default)
    | none => default

/-! ## Exposures and kernels on rows -/

/-- Blockwise transposition (the shape of the fine exposure): `a` blocks `m × k → k × m`. -/
def blkTg (m k a : ℕ) (zs : List α) : List α :=
  (List.range a).flatMap fun i => transposeL m k ((zs.drop (i * (m * k))).take (m * k))

/-- A row-indexed kernel on `R` consecutive rows of length `n`. -/
def rowMap (n R : ℕ) (g : ℕ → List α → List α) (X : List α) : List α :=
  (List.range R).flatMap fun r => g r ((X.drop (r * n)).take n)

/-- **A kernel pass**: expose `(A, m, post) → (A, post, m)`, apply `g b` to every row of block
`b`, expose back. -/
def kerPass (m post A : ℕ) (g : ℕ → List α → List α) (L : List α) : List α :=
  blkTg post m A (rowMap m (A * post) (fun r => g (r / post)) (blkTg m post A L))

/-! ## Reshaping `(pre, nc·λ, post) ↔ (pre·nc, λ, post)` -/

/-- The `nc` chunks of a line, joined. -/
def joinC (nc : ℕ) (ψ : ℕ → List α) : List α := (List.range nc).flatMap ψ

/-- A kernel on consecutive `λ`-chunks (generic `chunksL`). -/
def chunksG (g : ℕ → List α → List α) (lam nc : ℕ) (x : List α) : List α :=
  (List.range nc).flatMap fun q => g q ((x.drop (q * lam)).take lam)

end passes

end J6Seg

end

section
-- Source module: Solutions.J6SegSw3
/-!
# B-line machine, sweep 3: the `B₀` axis map as seven passes

On a `(pre, N, post)` array of Gaussian items (`N = n_c λ`), the in-place `B₀` line map of the
axis (`axisL N post (lineB …)`) is computed by (`axisPipe`):

1. a selection slab pass (row `rowSel l`, scaled by `2^{P-p-1}`, zeros for `l ≥ s`);
2. the chunk kernel `chunkK` on every `λ`-chunk (one `λ`-exposure);
3. a slab gather of the `m` near-boundary rows `LJ` (padded to `G` rows);
4. the `J` kernel (`fwdK`, `bwdK`, coupling window) on every `G`-row (one `G`-exposure);
5. a slab scatter back to the `N` rows;
6. the chunk kernel again;
7. the output slab pass on the pair `(Y, Y₂)`: `outE l (Y - Y₂)`.

Real and imaginary parts are carried together (`liftG`). **`axisPipe_eq`** proves the equality.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY

namespace J6Seg

/-! ## Pairs of arrays -/

/-! ## Gaussian lifts -/

/-- A real kernel applied to both parts. -/
def liftG (f : List ℤ → List ℤ) (x : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  List.zip (f (x.map Prod.fst)) (f (x.map Prod.snd))

/-! ## The passes of the `B₀` axis map -/

section pipe
variable (p P R s t lam w α K nc G : ℕ)

/-- Selection source. -/
def selSrc (l : ℕ) : Option ℕ := if l < s then some (rowSel s t l) else none

/-- Selection scaling. -/
def selH (_ : ℕ) (z : ℤ × ℤ) : ℤ × ℤ := (z.1 * 2 ^ (P - p - 1), z.2 * 2 ^ (P - p - 1))

/-- Gather source: the near-boundary rows, then zero padding. -/
def jSrc (r : ℕ) : Option ℕ :=
  if r < (LJ s t lam w).length then some ((LJ s t lam w).getD r 0) else none

/-- Scatter source. -/
def scSrc (u : ℕ) : Option ℕ := if u ∈ LJ s t lam w then some ((LJ s t lam w).idxOf u) else none

/-- The coupling values `W` from the gathered values `v` (capacitance solve + window). -/
def wOf (v : List ℤ) : List ℤ :=
  (List.range (LJ s t lam w).length).map fun r => dotF P (ccL P R s t lam w α K r)
    ((zext K (bwdK P (bsOf P (LJ s t lam w) (lam + w) (s - lam - w)
        (capI P (TT P R s t α) (BB s t lam w)))
      (fwdK P (fsOf P (LJ s t lam w) (lam + w) (s - lam - w)
        (capI P (TT P R s t α) (BB s t lam w))) v []) [] [])).drop r)

/-- The `J` kernel on a padded `G`-row. -/
def jKer (v : List ℤ) : List ℤ :=
  wOf P R s t lam w α K (v.take (LJ s t lam w).length) ++
    List.replicate (G - (LJ s t lam w).length) 0

/-- The output map on `(Y, Y₂)`. -/
def outH (l : ℕ) (z : (ℤ × ℤ) × (ℤ × ℤ)) : ℤ × ℤ :=
  if l < s then (outE p P s t α l (z.1.1 - z.2.1), outE p P s t α l (z.1.2 - z.2.2)) else (0, 0)

/-- **The `B₀` axis map as seven passes** on a `(pre, n_c λ, post)` array. -/
def axisPipe (pre post : ℕ) (L : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  let S := slabPass (nc * lam) (nc * lam) post (selSrc s t) (selH p P) L
  let Y := kerPass lam post (pre * nc) (fun b => liftG (chunkK P R s t lam α (b % nc))) S
  let Jg := slabPass (nc * lam) G post (jSrc s t lam w) (fun _ z => z) Y
  let W := kerPass G post pre (fun _ => liftG (jKer P R s t lam w α K G)) Jg
  let Wp := slabPass G (nc * lam) post (scSrc s t lam w) (fun _ z => z) W
  let Y2 := kerPass lam post (pre * nc) (fun b => liftG (chunkK P R s t lam α (b % nc))) Wp
  slabPass (nc * lam) (nc * lam) post (fun l => some l) (outH p P s t α) (List.zip Y Y2)

variable {p P R s t lam w α K nc G}

/-! ## The line identity -/

variable (P R s t lam w α K nc) in
/-- The scattered coupling values of `segLineC` (the right-hand side of the second solve). -/
def wpOf (x : List ℤ) : List ℤ :=
  (List.range (nc * lam)).map fun u => if u ∈ LJ s t lam w then
    (wOf P R s t lam w α K ((List.range (LJ s t lam w).length).map fun r =>
      (applyL P R s t lam α nc x).getD ((LJ s t lam w).getD r 0) 0)).getD
      ((LJ s t lam w).idxOf u) 0 else 0

end pipe

end J6Seg

end

section
-- Source module: Solutions.J6SegSw4
/-!
# B-line machine, sweep 4: the machine computes `tensorGo mapsLine6`

* **`pipeSweep`**: the machine applies an axis program `Fp k` for `k = 0, 1, …` in place;
* **`pipeSweep_eq`**: if every `Fp k` is the in-place axis map of `F k`, the machine is `sweepL`;
* **`sweepL_tensorGo'`**: `sweepL` of line maps of slice form is `tensorGo`;
* **`r6_maps_eq`**: in the round-six regime `mapsLine6 = mapsBs` and `λ ∣ t_i`, `s_i < t_i`;
* **`r6_machine`**: in the round-six regime, the seven-pass machine (`pipe6`, axes `0..d-1`)
  computes `tensorGo (mapsLine6 P n src D)` on every array of the right length.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open IntMul IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY IntMul.Kappa.R6
open NLogN.KFB (GI gflat)

namespace J6Seg

/-! ## The machine sweep -/

/-- The machine: axis programs `Fp 0, …, Fp (k-1)` in order. -/
def pipeSweep {α : Type*} (Fp : ℕ → List α → List α) : ℕ → List α → List α
  | 0, L => L
  | k + 1, L => Fp k (pipeSweep Fp k L)

/-! ## The round-six parameters -/

section r6
variable (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D : ℕ)

/-- `s_i` and `t_i` as functions of `ℕ`. -/
noncomputable def sI6 (i : ℕ) : ℕ := (List.ofFn (sD6 src D)).getD i 1
noncomputable def tI6 (i : ℕ) : ℕ := (List.ofFn (tD6 P n D)).getD i 1

/-- The padded length of the near-boundary line of axis `i` (a power of two). -/
noncomputable def GJ6 (i : ℕ) : ℕ :=
  2 ^ Nat.clog 2 (LJ (sI6 src D i) (tI6 P n D i) (lamP (dP6 P n)) (wF (dP6 P n))).length

/-- **The machine's program for axis `k`** (the seven passes at the round-six parameters). -/
noncomputable def pipe6 (k : ℕ) : List GI → List GI :=
  axisPipe (pP6 P n) (segPF (pP6 P n) (dP6 P n) (sI6 src D k)) (pP6 P n / 7) (sI6 src D k)
    (tI6 P n D k) (lamP (dP6 P n)) (wF (dP6 P n)) (αN6 P n) (wF (dP6 P n))
    (tI6 P n D k / lamP (dP6 P n)) (GJ6 P n src D k)
    ((List.ofFn (tD6 P n D)).take k).prod ((List.ofFn (tD6 P n D)).drop (k + 1)).prod

end r6

end J6Seg

end

section
-- Source module: Solutions.J6SegILRow
/-!
# B-line IL: the row-kernel interface (shared by the chunk kernel B3 and the `J` kernel B4)

`RowBody6 Isym tbl e dT tabOf Pre g C`: procedure `e` of the table `tbl` applies the row map
`g q` to the row `x` on top of stack `0`, reading the tables `tabOf q` from stack `dT` (left in
place), in the convention of `FineBody6`: every other managed stack is empty, and the base state
`s` (where the caller keeps its own data) is preserved.

* the chunk kernel (B3): `g q = liftG (chunkK P R s t λ α q)`, `tabOf = chunkTab …`
  (`chunkTab` below), rows of length `λ`;
* the `J` kernel (B4): `g _ = liftG (jKer P R s t λ w α K G)`, rows of length `G`.

`chunkTab ρ b q`: the tables of chunk `q` as one integer list: the header `[λ, P, ρ, b, nb]`
(`2^ρ = 2λ` the Kronecker record length, `b` the Kronecker digit width, `nb` the number of blocks), the four stage
tables `di, gi, gam, dd` (length `λ` each), then per block of the chunk `n :: am ++ ap`
(`descsOf`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

namespace J6Seg
open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFH NLogN.KFM IntMul.OpenAI.RT AModel
open IntMul.Kappa.R6

/-- **A row kernel as a procedure** (the convention of `FineBody6`). -/
def RowBody6 {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (e : Fin Pp) (dT : Fin HS)
    (tabOf : ℕ → List ℤ) (Pre : List GI → Prop) (g : ℕ → List GI → List GI) (C : ℝ) : Prop :=
  ∀ (q : ℕ) (s : IState HS) (F : Fin HS → List ℤ) (x : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dT → F j = []) → F dT = tabOf q → F 0 = gflat x ++ l → Pre x →
    ∃ c : ℕ, IRuns Isym tbl (.call e) (encK s F)
        (encK s (Function.update F 0 (gflat (g q x) ++ l))) c ∧ (c : ℝ) ≤ C

end J6Seg

end

section
-- Source module: Solutions.J6SegKr0
/-!
# B3 (chunk kernel), part 0: one uniform Kronecker record product with general truncation

`KFV10Rec.recU_runs` with the truncation `Δ` free (there `Δ = p + ρ`; the program `recU` reads
`2^Δ` from the parameter stack `kD`): on records `zx, zy` of length `r` (entries `|·| ≤ 2^p`,
digit width `b` with `2 r 2^{2p} < 2^{b-1}`), `recU` leaves the reversed record
`kmulD r Δ zx zy`, entry `j` = the `y^r + 1`-folded numerators truncated by `2^Δ`.
With `Δ = 0` and zero-padded records this is the exact Gaussian polynomial product
(the Toeplitz stages of the chunk kernel).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option maxRecDepth 10000

namespace NLogN.KFV

open IntMul KIL KFD KFT KFB KFC RS

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

/-- The folded numerators truncated by `2^Δ`. -/
def _root_.J6Seg.kmulD (r Δ : ℕ) (zx zy : List GI) : List GI :=
  List.zip ((List.range r).map fun j => fdt Δ (hRe r zx zy j) (hRe r zx zy (j + r)))
    ((List.range r).map fun j => fdt Δ (hIm r zx zy j) (hIm r zx zy (j + r)))

end NLogN.KFV

end

section
-- Source module: Solutions.J6SegKr1
/-!
# B3 (chunk kernel), part 1: the Gaussian stages as list maps

The chunk kernel on a Gaussian row is `liftG (chunkK q)`. Here it is rewritten in the form the
IL computes:

* `liftG_comp`, `liftG_append`: `liftG` commutes with composition / concatenation of
  length-preserving maps;
* `dgG c z`: the diagonal stage on pairs (`liftG (dgL P c) = dgG P c`);
* **`kmulD_toep`**: the zero-padded Kronecker record product with `Δ = 0` gives the exact
  lower-triangular Toeplitz sums `convL` of both parts (`2 n ≤ r + 1`);
* `lwG`, `upG`: the Toeplitz stages on pairs from `kmulD` (`liftG (lwL P c) = lwG`, …);
* `blkG`, `chunkG`: the block solve and the chunk kernel on pairs (`liftG (chunkL …) = chunkG …`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open Finset

namespace J6Seg

open IntMul NLogN NLogN.KFV

/-! ## `liftG` algebra -/

/-- Output length depends only on input length. -/
def LPres (f : List ℤ → List ℤ) : Prop := ∀ y y' : List ℤ, y.length = y'.length → (f y).length = (f y').length

/-! ## The diagonal stage -/

section stages
variable (P : ℕ)

/-- The diagonal stage on pairs. -/
def dgG (c : List ℤ) (z : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  List.zipWith (fun a w => (fmul P a w.1, fmul P a w.2)) c z

/-! ## Toeplitz sums by one record product -/

/-- A Gaussian row padded with zeros to length `r`. -/
def padG (r : ℕ) (z : List (ℤ × ℤ)) : List (ℤ × ℤ) := z ++ List.replicate (r - z.length) (0, 0)

/-- The first `n` entries of a real table as a padded Gaussian record. -/
def realG (r n : ℕ) (c : List ℤ) : List (ℤ × ℤ) :=
  ((c.take n).map fun a => (a, 0)) ++ List.replicate (r - n) (0, 0)

/-! ## Toeplitz stages on pairs -/

/-- The lower Toeplitz stage on pairs, from one record product. -/
def lwG (r : ℕ) (c : List ℤ) (z : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  ((kmulD r 0 (padG r z) (realG r z.length c)).take z.length).map fun w => (rs P w.1, rs P w.2)

/-- The upper Toeplitz stage on pairs. -/
def upG (r : ℕ) (c : List ℤ) (z : List (ℤ × ℤ)) : List (ℤ × ℤ) := (lwG P r c z.reverse).reverse

/-! ## The block solve and the chunk kernel on pairs -/

/-- The block solve on pairs. -/
def blkG (r : ℕ) (di gi gam dd am ap : List ℤ) (z : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  dgG P dd (dgG P gi (upG P r ap (dgG P gam (lwG P r am (dgG P gi (dgG P di z))))))

end stages

end J6Seg

end

section
-- Source module: Solutions.J6AIL1
/-!
# A lines, IL side 1: the per-block kernel as a list function

`aKerL w2 bk win Q aTab rTab cTab x` (row `x` of length `win`, the gathered window):

All three stages use the one rounding exponent `Q` (the IL kernel has one `rP` register); the
tables `aTab`, `rTab` are stored scaled by `2^Q`, so the first two stages are exact:

1. scale: `y = dgG Q aTab (x.take w2)` (`aTab_i = 2^Q a_i`: exact products `a_i x_i`);
2. correlate: `z = lwG Q (2n) rTab (padG n y)` with `n = w2 + bk` (`rTab_e = 2^Q r_e`: exact lower
   Toeplitz sums, one record product);
3. extract `z[w2 .. w2 + bk)` and rescale: `dgG Q cTab` (one rounding `rs Q` per entry);
4. pad with zeros to `win`.

* `aKerL_getD`: the entries of `aKerL` as fixed-point products of the explicit window sums.
* The tables of block `b` of an `A` line: `aTabA`, `rTabA`, `cTabA`.
* **`aKer_chirp`**: on the gathered window of block `b`, `aKerL` with these tables gives the
  `chirpC` outputs `k = b·bk + κ`, `κ < bk`.
-/

set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace J6A

open IntMul.HvdH J6Seg Finset

/-- **The per-block `A` kernel.** -/
def aKerL (w2 bk win Q : ℕ) (aTab rTab cTab : List ℤ) (x : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  dgG Q cTab (((lwG Q (2 * (w2 + bk)) rTab (padG (w2 + bk) (dgG Q aTab (x.take w2)))).drop w2).take bk)
    ++ List.replicate (win - bk) (0, 0)

/-- The window sums of the kernel (unscaled table entries `a`, `r`). -/
def kSum (w2 : ℕ) (a r : ℕ → ℤ) (xs : ℕ → ℤ) (κ : ℕ) : ℤ :=
  ∑ i ∈ range w2, a i * xs i * r (w2 + κ - i)

/-! ## The tables of an `A` line and the kernel on a gathered window -/

section tabs
variable (p s t α H b : ℕ)

/-- `W = H + m + 3`. -/
def WA : ℕ := H + sWidth p α + 3

/-- The rounding exponent `Q = 3P - σ` (`P = 2p`, `σ = p/2`). -/
def QA : ℕ := 3 * (2 * p) - p / 2

/-- The first output of block `b`. -/
def kkA : ℕ := b * (2 * H)

/-- The input scaling of block `b` (unscaled). -/
def aFA (i : ℕ) : ℤ := aT (2 * p) s t α H (kkA H b) (jcB s t H (kkA H b) - WA p α H + i)

/-- The correlation kernel of block `b` (unscaled, read backwards). -/
def rFA (e : ℕ) : ℤ :=
  expNeg (2 * p) (t ^ 3 * α ^ 2) (s * ((t : ℤ) * (jcB s t H (kkA H b) - WA p α H +
    ((2 * WA p α H + H : ℕ) : ℤ) - (e : ℤ)) - s * kcB H (kkA H b)).natAbs ^ 2)

/-- The input scaling table of block `b` (`2W` entries, scaled by `2^Q`). -/
def aTabA : List ℤ := (List.range (2 * WA p α H)).map fun (i : ℕ) => 2 ^ QA p * aFA p s t α H b i

/-- The correlation table of block `b` (`2W + 2H` entries, scaled by `2^Q`). -/
def rTabA : List ℤ :=
  (List.range (2 * WA p α H + 2 * H)).map fun (e : ℕ) => 2 ^ QA p * rFA p s t α H b e

/-- The output scaling table (`2H` entries). -/
def cTabA : List ℤ := (List.range (2 * H)).map fun (κ : ℕ) => cT (2 * p) (p / 2) s t α H (kkA H b + κ)

end tabs

end J6A

end

section
-- Source module: Solutions.J6AIL2
/-!
# A lines, IL side 2: copies and regrouping of line representations

* `dupL K L`: `K` copies of `L` concatenated (what the IL duplication leaves on stack `0`);
* **`LRep_cpy`**: `K = 2^f` copies of a `(pre, n, post)` array, followed by the two fine
  exposures `(1, K, N) → (1, N, K)` and `(pre, n·post, K) → (pre, K, n·post)`, are the
  `(pre, K·n, post)` array whose lines are `K` copies of the old lines;
* **`LRep_rgp`**: a `(pre, K·M·w, post)` array (`K = 2^f` classes of `M` windows of length `w`),
  after the exposures `(pre, K, M·w·post) → (pre, M·w·post, K)` and
  `(pre·M, w·post, K) → (pre·M, K, w·post)`, is the `(pre·(M·K), w, post)` array whose row
  `b·(M K) + j K + r` is window `j` of class `r` of line `b`.
-/

set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

open IntMul.HvdH IntMul.HvdH.Ref

namespace J6A

open J6Seg

section lists
variable {α : Type*} [Inhabited α]

/-- `K` copies of `L`. -/
def dupL (K : ℕ) (L : List α) : List α := (List.replicate K L).flatten

/-- Copies followed by the two exposures. -/
def cpy (K n post pre : ℕ) (L : List α) : List α :=
  blkTg (n * post) K pre (blkTg K (pre * (n * post)) 1 (dupL K L))

/-- Regrouping the classes of windows into rows. -/
def rgp (K M w post pre : ℕ) (L : List α) : List α :=
  blkTg (w * post) K (pre * M) (blkTg K (M * w * post) pre L)

end lists

end J6A

end

section
-- Source module: Solutions.J6SegILSlab1
/-!
# B-line IL, B1 (streaming slab pass) §1: the list level

The IL slab pass streams a `(pre, n, m)` array of *units* (an integer, or a pair of integers
for the zipped output pass) block by block. A block is driven by a **command list**
`cs : List (ℤ × ℤ)` of pairs `(op, arg)`:

* `op < 0`: drop the current input slab (`m` units);
* `op = 0`: emit a zero slab (`m` zeros);
* `op > 0`: emit the current input slab mapped unit-wise by `g arg` (the slab is kept).

`runC m g cs B` is the output of one block. For a monotone source `src` (`MonoSrc`),
`ctlOf n n' src argOf` is the command list (drops to the next source slab, then an emit;
a zero emit for `none`; final drops), and **`runC_ctlOf`**: the block output is the block of
`slabPass n n' m src (fun l => g (argOf l))`. **`slabPass_blocks`**: the whole pass is the
concatenation of the block outputs.

**`flat_slabPass`**: for a flattening `φ : α → List γ` with two entries per item and a map `h`
acting entry-wise (`φ (h l x) = (φ x).map (h' l)`), `flatMap φ` commutes with slab passes
(`post ↦ 2 post`). Instances: `gflat` (passes 1, 3, 5) and `pflat` on `zip Y Y₂` (pass 7,
`pflat (zip Y Y₂) = zip (gflat Y) (gflat Y₂)`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedVariables false

open IntMul.HvdH IntMul.HvdH.Ref NLogN.KFM NLogN.KFY

namespace J6Seg

/-! ## Commands -/

section cmd
variable {U : Type*}

/-- The output of one block driven by the commands `cs`. -/
def runC (m : ℕ) (g : ℤ → U → ℤ) : List (ℤ × ℤ) → List U → List ℤ
  | [], _ => []
  | (op, a) :: cs, inp =>
    if op < 0 then runC m g cs (inp.drop m)
    else if op = 0 then List.replicate m 0 ++ runC m g cs inp
    else (inp.take m).map (g a) ++ runC m g cs inp

/-- The drop command. -/
def dropC : ℤ × ℤ := (-1, 0)

/-- The commands of the output slabs `ls` from the input position `cur`, and the final position. -/
def ctlAux (src : ℕ → Option ℕ) (argOf : ℕ → ℤ) : List ℕ → ℕ → List (ℤ × ℤ) × ℕ
  | [], cur => ([], cur)
  | l :: ls, cur =>
    match src l with
    | none => ((0, 0) :: (ctlAux src argOf ls cur).1, (ctlAux src argOf ls cur).2)
    | some k => (List.replicate (k - cur) dropC ++ (1, argOf l) :: (ctlAux src argOf ls k).1,
        (ctlAux src argOf ls k).2)

/-- **The command list of a block.** -/
def ctlOf (n n' : ℕ) (src : ℕ → Option ℕ) (argOf : ℕ → ℤ) : List (ℤ × ℤ) :=
  (ctlAux src argOf (List.range n') 0).1 ++
    List.replicate (n - (ctlAux src argOf (List.range n') 0).2) dropC

/-- A monotone source below `n` on the first `n'` output slabs. -/
def MonoSrc (n n' : ℕ) (src : ℕ → Option ℕ) : Prop :=
  (∀ l < n', ∀ k, src l = some k → k < n) ∧
  ∀ l₁ l₂ k₁ k₂, l₁ < l₂ → l₂ < n' → src l₁ = some k₁ → src l₂ = some k₂ → k₁ ≤ k₂

/-- The source slabs at or after `cur` along `ls`, in order. -/
def SrcFrom (src : ℕ → Option ℕ) (n : ℕ) : List ℕ → ℕ → Prop
  | [], _ => True
  | l :: ls, cur => match src l with
    | none => SrcFrom src n ls cur
    | some k => cur ≤ k ∧ k < n ∧ SrcFrom src n ls k

variable [Inhabited U]

/-- One output slab of a block (integer outputs, zeros for `none`). -/
def slabZ (B : List U) (m : ℕ) (src : Option ℕ) (h : U → ℤ) : List ℤ :=
  match src with
  | some k => ((B.drop (k * m)).take m).map h
  | none => List.replicate m 0

@[simp] theorem slabZ_none (B : List U) (m : ℕ) (h : U → ℤ) :
    slabZ B m none h = List.replicate m 0 := rfl

@[simp] theorem slabZ_some (B : List U) (m k : ℕ) (h : U → ℤ) :
    slabZ B m (some k) h = ((B.drop (k * m)).take m).map h := rfl

/-- The number of drop commands of a block. -/
def nDrop : List (ℤ × ℤ) → ℕ
  | [] => 0
  | (op, _) :: cs => (if op < 0 then 1 else 0) + nDrop cs

end cmd

/-! ## Slab passes as block outputs -/

/-! ## Flattening -/

section flat
variable {α β γ δ : Type*} [Inhabited α] [Inhabited β] [Inhabited γ] [Inhabited δ]

/-- The pair flattening of the zipped output pass. -/
def pflat (zs : List ((ℤ × ℤ) × (ℤ × ℤ))) : List (ℤ × ℤ) :=
  zs.flatMap fun z => [(z.1.1, z.2.1), (z.1.2, z.2.2)]

end flat

/-! ## Splitting a command list; validity -/

section valid
variable {U : Type*}

/-- Each emitting or dropping command finds its slab: the drops so far are below `n`. -/
def VC (n : ℕ) : List (ℤ × ℤ) → ℕ → Prop
  | [], _ => True
  | (op, _) :: cs, d => (op ≠ 0 → d < n) ∧ VC n cs (d + if op < 0 then 1 else 0)

end valid

end J6Seg

end

section
-- Source module: Solutions.J6AIL6
/-!
# A lines, IL side 6: the per-axis pipeline at the list level

On a `(pre, t, post)` array the `A` line map of an axis is computed by six list passes, each of
which has an IL counterpart:

1. `cpy 32 t post pre`: the lines `X` become `dupL 32 X` (32 copies);
2. the **gather** slab pass `slabPass (32 t) (8 (M win)) post (srcG …)`: output slab
   `l = (r M + j) win + e` (`r < 8`, `j < M`, `e < win`) is, for `e < 2W`, the input
   `X[(jc_b - W + e) mod s]` of block `b = 8 j + r`, read from copy `4 r + c` (`c ∈ {0,1,2}` handles
   the wrap-around, `posE`), and `0` otherwise; inside a class `r` the windows of the blocks
   `r, r + 8, …` are disjoint and increasing, so the source is monotone;
3. `rgp 8 M win`: the windows become rows; row `b'` holds the window of block `b' % (8M)`;
4. the kernel pass `kerPass win post (pre·8M) (fun b => gK (b % 8M))` (`gK q` the per-block kernel
   `aKerL` with the tables of block `q`);
5. the **compress** slab pass `slabPass (8M win) t post srcC`: output `k` is entry `k % 2H` of
   row `k / 2H`.

**`pipeAL_rep`**: the result represents the lines `(range t).map (chirpC p s t α H U_X)`;
**`pipeAL_eq`**: the pipeline is `axisL t post` of that line map.
**`monoSrc_G`**, **`monoSrc_C`**: the two sources are monotone (the IL slab passes need this).
-/

set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace J6A

open IntMul.HvdH J6Seg

/-! ## The sources -/

/-- The position of the extended index `j ∈ [-W, s + W)` in three consecutive copies of a line
of length `t`: `j < 0` in copy `0`, `0 ≤ j < s` in copy `1`, `s ≤ j` in copy `2`. -/
def posE (s t : ℕ) (j : ℤ) : ℕ :=
  if j < 0 then ((s : ℤ) + j).toNat else if j < s then t + j.toNat else 2 * t + (j - s).toNat

/-- The block of window `Q' = r M + j` (`r < 8`, `j < M`): `8 j + r`. -/
def blkW (M Q' : ℕ) : ℕ := 8 * (Q' % M) + Q' / M

/-- **The gather source.** -/
def srcG (s t H W M win : ℕ) (l : ℕ) : Option ℕ :=
  if l % win < 2 * W then
    some (l / win / M * (4 * t) +
      posE s t (jcB s t H (kkA H (blkW M (l / win))) - W + ((l % win : ℕ) : ℤ)))
  else none

/-- **The compress source.** -/
def srcC (H win : ℕ) (l : ℕ) : Option ℕ := some (l / (2 * H) * win + l % (2 * H))

/-- The kernel of block `q`. -/
def gK (p s t α H win q : ℕ) : List (ℤ × ℤ) → List (ℤ × ℤ) :=
  aKerL (2 * WA p α H) (2 * H) win (QA p) (aTabA p s t α H q) (rTabA p s t α H q)
    (cTabA p s t α H q)

/-- **The per-axis pipeline** (`M = t / 16H`, `win = 8H`). -/
def pipeAL (p s t α H pre post : ℕ) (L : List (ℤ × ℤ)) : List (ℤ × ℤ) :=
  slabPass (t / (16 * H) * 8 * (8 * H)) t post (srcC H (8 * H)) (fun _ z => z)
    (kerPass (8 * H) post (pre * (t / (16 * H) * 8))
      (fun b => gK p s t α H (8 * H) (b % (t / (16 * H) * 8)))
      (rgp 8 (t / (16 * H)) (8 * H) post pre
        (slabPass (32 * t) (8 * (t / (16 * H) * (8 * H))) post
          (srcG s t H (WA p α H) (t / (16 * H)) (8 * H)) (fun _ z => z) (cpy 32 t post pre L))))

/-! ## Geometry -/

/-! ## The gather source is monotone -/

/-! ## The pipeline on representations -/

end J6A

end