Round-six κ development, definitions part 16

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

import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_MultitapeModel
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_MachineRef
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_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_HvdH_M_Defs3
import Definitions.Def_IntMul_Kappa_R6_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_R6_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_R6_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs19
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs23
import Definitions.Def_IntMul_Kappa_R6_Defs23
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_K_Defs9
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs24
import Definitions.Def_IntMul_Kappa_R6_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs17
import Definitions.Def_IntMul_Kappa_K_Defs18
import Definitions.Def_IntMul_Kappa_K_Defs22
import Definitions.Def_IntMul_Kappa_K_Defs25

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.HReg
/-!
# Register programs

`RS` is a small structured language over the register stacks `0 … 55`: assignments of
expressions, pushes and pops, conditionals and counted loops.  `RS.run` is its functional
semantics on `IState`s, and `RS.code_runs` shows that the compiled `IStmt` realises it with cost
`RS.cost`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

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

namespace RS

/-! ## Frame -/

/-! ## Compilation -/

/-! ## Sequences and reasoning lemmas -/

theorem iter_ip (f : IState HS → IState HS) (hf : ∀ t, (f t).ip = t.ip ∧ (f t).out = t.out) :
    ∀ k t, (f^[k] t).ip = t.ip ∧ (f^[k] t).out = t.out
  | 0, t => ⟨rfl, rfl⟩
  | k + 1, t => by
    rw [Function.iterate_succ_apply']
    exact ⟨(hf _).1.trans (iter_ip f hf k t).1, (hf _).2.trans (iter_ip f hf k t).2⟩

theorem run_ip_out : ∀ (p : RS) (s : IState HS), (p.run s).ip = s.ip ∧ (p.run s).out = s.out
  | skip, s => ⟨rfl, rfl⟩
  | asg i e, s | push i e, s | pop i, s => by simp [run]
  | seq a b, s => by
    simp only [run]
    exact ⟨(run_ip_out b _).1.trans (run_ip_out a s).1, (run_ip_out b _).2.trans (run_ip_out a s).2⟩
  | ite c a b, s => by
    simp only [run]; split_ifs
    · exact run_ip_out a s
    · exact run_ip_out b s
  | rep i n b, s => by
    simp only [run, IState.upd_ip, IState.upd_out]
    have := iter_ip (fun t => decSt i (b.run t))
      (fun t => by simp only [decSt, IState.upd_ip, IState.upd_out]; exact run_ip_out b t)
      (n.eval s).toNat (s.upd i (.int (n.eval s) :: s.G i))
    simpa using this

/-! ## Cost bounds -/

/-- Two register-program results agree when all their stacks agree. -/
theorem run_ext {p : RS} {s t : IState HS} (h : ∀ j, (p.run s).G j = t.G j) (hip : s.ip = t.ip)
    (hout : s.out = t.out) : p.run s = t :=
  IState.ext' h ((run_ip_out p s).1.trans hip) ((run_ip_out p s).2.trans hout)

@[simp] theorem run_push_G (i : Fin HS) (e : Ex HS) (s : IState HS) (j : Fin HS) :
    ((push i e).run s).G j = if j = i then .int (e.eval s) :: s.G i else s.G j := by
  simp [run, IState.upd_G]

@[simp] theorem run_pop_G (i : Fin HS) (s : IState HS) (j : Fin HS) :
    ((pop i).run s).G j = if j = i then (s.G i).tail else s.G j := by
  simp [run, IState.upd_G]

theorem run_seq (a b : RS) (s : IState HS) : (seq a b).run s = b.run (a.run s) := rfl

end RS

end NLogN

end

section
-- Source module: NLogN.HRM
/-!
# Register programs with multiplication calls

`RM` extends the register programs `RS` by `mul k i j`, which pushes `top j * top i` onto `k`
by calling the multiplication procedure `pM` with the calling convention

  `ARG = 55 : a :: b :: L  ↦  (a * b) :: L`,

all other stacks unchanged.  The cost of a call and the inputs on which it may be used are a
parameter `M : MulSpec`; `RM.code_runs` holds whenever the procedure meets `MulOK M`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul

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

theorem IOp.run_ipout {o : IOp HS} {s s' : IState HS} {c : ℕ} (h : o.run s = some (s', c)) :
    s'.ip = s.ip ∧ s'.out = s.out := by
  cases o <;> simp only [IOp.run] at h <;> (repeat' split at h) <;> (try simp at h) <;>
    (try split_ifs at h) <;> (try simp at h) <;>
    (try (obtain ⟨rfl, rfl⟩ := h)) <;> (try (obtain ⟨_, rfl, rfl⟩ := h)) <;>
    simp_all

namespace RM

open RS (decSt decE asgCost)

/-! ## Frame -/

/-! ## Reasoning lemmas -/

theorem run_ip_out : ∀ (p : RM) (s : IState HS), (p.run s).ip = s.ip ∧ (p.run s).out = s.out
  | rs p, s => RS.run_ip_out p s
  | mul k i j, s => by simp [run]
  | seq a b, s => by
    simp only [run]
    exact ⟨(run_ip_out b _).1.trans (run_ip_out a s).1, (run_ip_out b _).2.trans (run_ip_out a s).2⟩
  | ite c a b, s => by
    simp only [run]; split_ifs
    · exact run_ip_out a s
    · exact run_ip_out b s
  | rep i n b, s => by
    simp only [run, IState.upd_ip, IState.upd_out]
    have := RS.iter_ip (fun t => decSt i (b.run t))
      (fun t => by simp only [decSt, IState.upd_ip, IState.upd_out]; exact run_ip_out b t)
      (n.eval s).toNat (s.upd i (.int (n.eval s) :: s.G i))
    simpa using this
  | op o, s => by
    simp only [run]; split
    · rename_i r hr
      exact IOp.run_ipout hr
    · exact ⟨rfl, rfl⟩
  | prc _ _ _ _ _ _ hio, s => hio s

theorem run_ext {p : RM} {s t : IState HS} (h : ∀ j, (p.run s).G j = t.G j) (hip : s.ip = t.ip)
    (hout : s.out = t.out) : p.run s = t :=
  IState.ext' h ((run_ip_out p s).1.trans hip) ((run_ip_out p s).2.trans hout)

theorem run_seq (a b : RM) (s : IState HS) : (seq a b).run s = b.run (a.run s) := rfl

/-! ## Counted loops through a family of states -/

end RM

end NLogN

end

section
-- Source module: NLogN.SSLoops
/-!
# Generic counted loops over item arrays
-/

namespace NLogN

open IntMul

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

theorem ints_append (A B : List ℤ) : ints (A ++ B) = ints A ++ ints B := by simp [ints]
theorem ints_reverse (A : List ℤ) : ints A.reverse = (ints A).reverse := by simp [ints]

end NLogN

end

section
-- Source module: NLogN.HSort
/-!
# Stable radix sort of fixed-width records on a register stack

* `mvK X Y C n`: move `n` integers from `X` to `Y` (reversed); `mvK_spec`, `mvK_cost`.
* `radixPass k`, `radixSort kb`: the pure stable partition pass / LSD radix sort on the first
  component (the key) of each record; `radixSort_keys`: for keys forming a permutation of
  `0, …, N-1` (with `N ≤ 2^kb`) the record with key `q` ends up at position `q`.
* `passP w`, `sortP w`: the register programs (records of width `w ≥ 1` on stack `0`, record
  count on `1`, key bits `kb` on `2`; scratch `46 … 53`); `sortP_spec`, `sortP_cost`.
All per-element code uses `Ex.Lin` expressions only; costs are bounded with the linear lemmas.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul RS

theorem mvK_states {X Y C : Fin HS} (hXY : X ≠ Y) (hXC : X ≠ C) (hYC : Y ≠ C) (n : Ex HS)
    (s : IState HS) (L : List ℤ) (R : List Item) (hX : s.G X = ints L ++ R)
    (hn : n.eval s = L.length) :
    RepStates C n (seq (push Y (.reg X)) (pop X)) s (mvSt_s X Y s L R) where
  nonneg := by rw [hn]; positivity
  hw := by simp [RS.writes, hXC.symm, hYC.symm]
  h0 := by simp [mvSt_s, ← hX]
  hG := fun k => by simp [mvSt_s, hXC.symm, hYC.symm]
  step := by
    intro k hk
    rw [hn, Int.toNat_natCast] at hk
    have hd : L.drop k = L[k] :: L.drop (k + 1) := List.drop_eq_getElem_cons hk
    have ht : L.take (k + 1) = L.take k ++ [L[k]] := (List.take_concat_get' L k hk).symm
    apply run_ext _ (by simp [withCtr, mvSt_s]) (by simp [withCtr, mvSt_s])
    intro j
    simp only [run_seq, run_push_G, run_pop_G, withCtr, mvSt_s, IState.upd_G, Ex.eval, IState.top]
    by_cases h1 : j = X
    · rw [h1, hd]
      simp only [if_neg hXY, if_neg hXC, ite_true, ints_cons, List.cons_append, List.tail_cons]
    by_cases h2 : j = Y
    · rw [h2, hd, ht]
      simp only [if_neg hXY.symm, if_neg hYC, if_neg hXC, ite_true, ints_cons, List.cons_append,
        ints_append, List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append,
        List.singleton_append, List.map_cons, List.map_nil, ints, List.append_assoc, List.map_append]
      simp [hXY]
    · simp [h1, h2]

theorem mvK_spec {X Y C : Fin HS} (hXY : X ≠ Y) (hXC : X ≠ C) (hYC : Y ≠ C) (hX5 : X.val < 56)
    (hY5 : Y.val < 56) (hC5 : C.val < 56) (n : Ex HS) (hnc : n.Clean) (s : IState HS)
    (L : List ℤ) (R : List Item) (hX : s.G X = ints L ++ R) (hno : n.ok s)
    (hn : n.eval s = L.length) :
    (mvK X Y C n).ok s ∧
      (mvK X Y C n).run s = (s.upd X R).upd Y ((ints L).reverse ++ s.G Y) := by
  have H := mvK_states hXY hXC hYC n s L R hX hn
  refine ⟨H.ok hC5 hnc hno ?_, ?_⟩
  · intro k hk
    rw [hn, Int.toNat_natCast] at hk
    have hd : L.drop k = L[k] :: L.drop (k + 1) := List.drop_eq_getElem_cons hk
    have e1 : (withCtr C s (n.eval s).toNat k (mvSt_s X Y s L R k)).G X =
        .int L[k] :: (ints (L.drop (k + 1)) ++ R) := by
      simp only [withCtr, mvSt_s, IState.upd_G, if_neg hXY, if_neg hXC, ite_true]
      rw [hd]; rfl
    refine ⟨⟨hY5, clean_of_lt hX5, IState.isInt_of_r6c e1⟩, hX5, ?_⟩
    apply IState.isInt_of_r6c (L := ints (L.drop (k + 1)) ++ R) (a := L[k])
    simp [run_push_G, hXY, e1]
  · rw [mvK, H.run, hn, Int.toNat_natCast]
    simp [mvSt_s]

/-! ## Radix sort: pure functions -/

/-! ## One pass as a register program

Registers: data `0`, record count `1`; scratch `46` (ones), `47` (zeros), `48`, `49` (their
element counts), `50` (loop counter), `51` (counter of `mvK`), `52` (holds `2^k`). -/

/-! ## The radix sort program

Data on `0`, record count on `1`, number of key bits on `2`; scratch `46 … 53`. -/

/-! ## Costs -/

/-! ## Correctness of radix sort for distinct keys -/

end NLogN

end

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

lemma Valid.take {sh : Shape} {a : List ℕ} (h : Valid sh a) (k : ℕ) :
    Valid (sh.take k) (a.take k) := List.forall₂_take k h

end Reshape

/-! ## 2. Block swaps -/

section BlockSwap

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

/-! ### Merging both runs -/

end BlockSwap

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

/-! ## 4. Counting runs -/

end AModel

end

section
-- Source module: Solutions.KIL4Tbl
/-!
# KIL4: the offset table generator with run-time stage data

KIL2's `genP Q ac` has one stage per field of the prefix `A` of the target, every number (`Q`,
the radix `a`, the control `c`, the suffix volume `M`) a literal.  The uniform generator `genPU n`
reads the stages from four stage stacks (`34 … 37`: `a`, `c`, `M`, `a·M`, the last stage on top) and
`-Q` from the parameter stack `23`; its code depends only on the number `n` of stages.

* `gStageT`, `rsim_gStage`: the stage as a template; the literal stage simulates it.
* `stagesU_sp`, `genPU_sp`: the generator pushes `tbl Q ac` on stack `14`, pops the stage stacks.
* `tbl_zeros`, `tbl_app_congr`: the table only depends on the controls; runs of control-`0`
  fields collapse to one field of their volume (the "collapsed" stage lists of the uniform
  shifts have at most `2m + 3` stages whatever the shape).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Parameter stacks of the uniform shift -/

/-! ## Templates -/

theorem RSim.mvK {π : PMap} (X Y C : Fin HS) {n n' : Ex HS} (h : ESim π n n') :
    RSim π (NLogN.mvK X Y C n) (NLogN.mvK X Y C n') :=
  .rep C h (.seq (.push Y (.reg X)) (.pop X))

/-! ## The literal stage in stack form -/

/-! ## One uniform stage -/

/-! ## The generator -/

/-! ## Cost of the generator -/

/-! ## Collapsing control-`0` fields of the table -/

end NLogN.KIL

end

section
-- Source module: Solutions.KFDBase
/-!
# KFD base: fine compilation of register programs

The register programs `RS` of KIL1–KIL6 are compiled by `RS.code`, whose counted loop
`rep i n b` keeps a *binary* counter on `i` and decrements it in every iteration (cost
`Θ(zsz n)` per iteration).  `fcode` compiles the same program with a *unary* counter instead:

* `rep i n b ↦ push i n; toUL i i; loop i isMk (unmark i; fcode b); drop i`

(the value `n` stays below the `n` marks as a sentinel; `toUL` is the linear binary → unary
conversion of `KFCUnary`).  Everything else is compiled as by `RS.code`.

`fcode_runs` (**simulation**): if `p.ok s` and every loop body leaves its counter alone
(`FOK p`: the counter is not *touched* — read or written — by the body, and avoids the
`toUL` scratch stacks `26 … 29`), then `fcode p` realises `p.run` with the cost `fcost p s`.
The run is proved relative to a set of *ghost* stacks (the counters of the enclosing loops,
which hold marks in the fine run and the binary count in the `RS` semantics).

`fcost_le_cost`: `fcost p s ≤ 100 · p.cost s` (coarse transfer of every `KIL` cost bound).
The point of `fcost` is the loop: per iteration it charges `fcost b + 31` plus the amortised
`toUL` cost, i.e. `O(1)` overhead per iteration, independent of the size of the count.

`FSp p s t c` is the fine analogue of `KIL.Sp`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN

open IntMul RS

namespace KFD

open KFC (marks marks_zero isMk NM toUL cUL uK uR uY uB)

/-! ## Expression congruence -/

/-! ## Touched stacks, fine compilability -/

/-! ## The fine compilation and its cost -/

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

/-! ## Ghost stacks -/

/-! ## The simulation -/

/-! ## Top level -/

/-! ## Coarse transfer: `fcost ≤ 100 · cost` -/

/-! ## Fine specifications -/

/-! ## Loops -/

/-- Per-element cost of a move of an entry of bit size `≤ w`. -/
theorem mvBody_fcost (X Y : Fin HS) (t : IState HS) (a : ℤ) (L : List Item) (w : ℕ)
    (hX : t.G X = .int a :: L) (hXY : X ≠ Y) (ha : zsz a ≤ w) :
    fcost (.seq (.push Y (.reg X)) (.pop X)) t ≤ 250 * (w + 2) := by
  simp only [fcost, Ex.cost, Ex.eval, IState.top_eq_r6c hX]
  have e2 : ((RS.push Y (.reg X)).run t).top X = a := IState.top_eq_r6c (L := L)
    (by simp only [run_push_G, if_neg hXY, hX])
  rw [e2]
  simp only [dupCost, zipCost, moveCost]
  omega

/-- **Fine `mvK`**: `n` entries moved, cost `n.cost + cRep N + N · 250 (w + 2)`. -/
theorem FSp.mvK' {X Y C : Fin HS} (hXY : X ≠ Y) (hXC : X ≠ C) (hYC : Y ≠ C) (hX5 : X.val < 56)
    (hY5 : Y.val < 56) (hC5 : C.val < 56) (n : Ex HS) (hnc : n.Clean) (s : IState HS)
    (L : List ℤ) (R : List Item) (hX : s.G X = ints L ++ R) (hno : n.ok s)
    (hn : n.eval s = L.length) (w : ℕ) (hL : Bnd w L) :
    FSp (NLogN.mvK X Y C n) s ((s.upd X R).upd Y ((ints L).reverse ++ s.G Y))
      (n.cost s + cRep L.length + L.length * (250 * (w + 2))) := by
  have H := mvK_spec hXY hXC hYC hX5 hY5 hC5 n hnc s L R hX hno hn
  refine ⟨H.1, H.2, ?_⟩
  have HS := mvK_states hXY hXC hYC n s L R hX hn
  have := fcost_rep_le HS (250 * (w + 2)) (by
    intro k hk
    rw [hn, Int.toNat_natCast] at hk
    have hd : L.drop k = L[k] :: L.drop (k + 1) := List.drop_eq_getElem_cons hk
    have e1 : (withCtr C s (n.eval s).toNat k (mvSt_s X Y s L R k)).G X =
        .int L[k] :: (ints (L.drop (k + 1)) ++ R) := by
      simp only [withCtr, mvSt_s, IState.upd_G, if_neg hXY, if_neg hXC, ite_true]
      rw [hd]; rfl
    exact mvBody_fcost X Y _ _ _ w e1 hXY (hL _ (List.getElem_mem hk)))
  rw [hn, Int.toNat_natCast] at this
  exact this

open KIL in
/-- `FSp.mvK'` on managed states (as `KIL.Sp.mvK`). -/
theorem FSp.mvK {X Y C : Fin HS} (hXY : X ≠ Y) (hXC : X ≠ C) (hYC : Y ≠ C) (hX5 : X.val < 56)
    (hY5 : Y.val < 56) (hC5 : C.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (n : Ex HS)
    (hnc : n.Clean) (hno : n.ok (encK s f)) (L l : List ℤ) (hX : f X = L ++ l)
    (hn : n.eval (encK s f) = L.length) (w : ℕ) (hL : Bnd w L) :
    FSp (NLogN.mvK X Y C n) (encK s f)
      (encK s (Function.update (Function.update f X l) Y (L.reverse ++ f Y)))
      (n.cost (encK s f) + cRep L.length + L.length * (250 * (w + 2))) := by
  have hXs : (encK s f).G X = ints L ++ (ints l ++ s.G X) := by simp [hX, ints_append]
  have H := FSp.mvK' hXY hXC hYC hX5 hY5 hC5 n hnc (encK s f) L _ hXs hno hn w hL
  refine H.congr ?_
  refine IState.ext' (fun j => ?_) rfl rfl
  by_cases h1 : j = Y
  · subst h1; simp [Ne.symm hXY, ints_append, ints_reverse]
  by_cases h2 : j = X
  · subst h2; simp [hXY]
  · simp [h1, h2]

/-! ## Literal-to-register simulation -/

end KFD

end NLogN

end

section
-- Source module: Solutions.KFGGate
/-!
# KFG: dyadic gate atoms, dyadic gates, unit scalings, role swaps and role permutations

All steps are pair passes (`pairW`) on the scaled encoding `Enc`.

* `Atom` `⟨t, s, c, h⟩`: `y_t += (c / 2^h) y_s` (`c ∈ {-1,0,1}²`).  The target's scale becomes
  `E = max (e t) (e s + h)`; the pass computes `z_t ← 2^{E - e t} z_t + c · 2^{E - e s - h} z_s`
  (exact).  `enc_atom`.
* `gateP as e L`: a list of atoms whose targets are never sources (`NoTS`), applied in order;
  `enc_gate`: the result encodes `y_w + Σ_{a.t = w} (c_a / 2^{h_a}) y_{a.s}`, i.e. the gate matrix
  `1 + Σ_a (c_a/2^{h_a}) e_{a.t, a.s}` applied pointwise across roles.
* `UAtom` `⟨t, u, t'⟩`: `y_t ← u y_t` (a pass on `t` and a partner role `t'`); `enc_uatom`.
* `swapW`: exchange of two roles (and their scales); `perm_swaps`: every permutation of `Fin W`
  is a product of at most `|supp σ| ≤ W` swaps; `enc_permP`: the role permutation.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFG

open IntMul RS AModel KIL KFD KFB Complex

/-! ## Gate atoms -/

namespace Atom

variable (a : Atom) (e : ℕ → ℕ)

end Atom

/-! ## Gates: lists of atoms -/

/-! ## The gate matrix -/

/-! ## Unit scalings -/

def UAtom.Ok (b : UAtom) (W : ℕ) : Prop := b.t < W ∧ b.t' < W ∧ b.t ≠ b.t' ∧ Sm b.u

/-! ## Role swaps and permutations -/

end NLogN.KFG

end

section
-- Source module: Solutions.KFHKer
/-!
# KFH: an individual selected-bit kernel as one `qop` pass on a record array

The layer layout of Proposition 14 is `[P] × [2^K]^D × [S]` (`Butterfly.layerShape`), records in
lexicographic order.  Bit `ρ` of chunk `i` has record stride `stT = 2^ρ · vol(suffix after
chunk i)`: the address with that bit flipped is `j ± stT` (`layer_partner`).  On the flat
Gaussian list (records of `r` coefficients) the paired entries are at distance `B1 = stT · r`,
in blocks of `2 B1`; this is exactly the two-stream pass `KFB.qop [M] B1 G` with
`G = P · 2^{K i} · 2^{K-ρ-1}` groups.

* `encode_set`, `getD_digit`: mixed-radix arithmetic of one changed digit.
* `layer_partner`: selected bit `i` of record `j` is `j / stT % 2`; flipping it moves to
  `j + (b - bit) stT`.
* `ker_rep`: if `toC M = 2^e A` entrywise (`KerOk`), `qopL [M] (stT r) G` represents
  `selOp (tensF (kerAt i A))` (the kernel (25) of `A` on bit `i`) at scale `F + e`.
* `kerP_fsp`: the self-contained pass `kerP = qopW [M] (stT r) G 0`, cost `cQopW`, width `+2`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFH

open IntMul RS AModel KIL KFD KFB Complex

/-! ## Mixed-radix arithmetic -/

/-! ## The layer layout -/

variable {P K D S ρ : ℕ}

/-! ## The kernel pass on records -/

theorem RecRep.getD {r F : ℕ} {zs : List GI} {xs : List (Fin r → ℂ)} (h : RecRep r F zs xs)
    {j : ℕ} (hj : j < xs.length) (c : Fin r) :
    toC (zs.getD (j * r + c) 0) = 2 ^ F * xs.getD j 0 c := h.2 j c hj

/-! ## The self-contained pass -/

end NLogN.KFH

end

section
-- Source module: Solutions.KFMBaseSap
open Complex

namespace IntMul.HvdH.SPf
open IntMul.HvdH

/-- A pair of integers as a Gaussian integer in `ℂ`. -/
def toC (p : ℤ × ℤ) : ℂ := (p.1 : ℂ) + (p.2 : ℂ) * I

end IntMul.HvdH.SPf

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

def β : ℚ := 1 / 2

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

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

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

end IntMul.OpenAI.RP

end

section
-- Source module: Solutions.KFMErr
/-!
# KFM 14: the error chain of the computed pipeline (§9.7.1), abstract form

Arrays are functions `ι → ℂ` with the sup norm; `hp = 2^{-p}`. Every computed procedure is
an arbitrary function with an error bound on grid inputs (`Grid p f`: `Q_p f = f`), so the IL
denotations (and `P18IL`) plug in later.

* `QA p f`: `Q_p` on every entry; `QA_grid`, `norm_QA_le`, `norm_QA_sub_le` (`≤ √2 hp`).
* **`phase_err`**: `‖Q_p(ẽ·x) - e·x‖ ≤ 4hp`, `‖Q_p(ẽ·x)‖ ≤ ‖x‖` (unit phases, `|ẽ-e| ≤ 2hp`).
* `BilC M`: bilinear contraction; **`bil_err`**.
* **`mc_err`**: the computed complex convolution `Q_p(θ̃⁻ · M̃r(Q_p(θ̃⁺f), Q_p(θ̃⁺g)))` is within
  `(Er + 12) hp` of `θ⁻ · Mr(θ⁺ f, θ⁺ g)` (one operand of norm `≤ .7`).
* **`chirp_err`**: `Q_p(ã · M̃C(ã, Q_p(ã · x)))` is within `(Ec + 10) hp` of `a · MC(a, a · x)`.
* **`source_err`**: `2^γ B̃₀(C̃(Ã u))` is within `2^γ (εA + Ec + εB) hp` of `2^γ B₀(QF(A u))`.
* **`pipeline_err`**: with `z = Q_p(F̃u · F̃v)` and `F̃⁺ = conj ∘ F̃ ∘ conj`,
  `‖F̃⁺ z - G(Fu · Fv)‖ ≤ (3Es + 2) hp`.
-/

namespace NLogN.KFM

open Complex

noncomputable section

section Arr

variable {ι : Type*} [Fintype ι]

lemma truncR_neg' (p : ℕ) (x : ℝ) : Butterfly.truncR p (-x) = -Butterfly.truncR p x := by
  unfold Butterfly.truncR Butterfly.truncNum
  rcases lt_trichotomy x 0 with h | h | h
  · rw [if_pos (by linarith), if_neg (by linarith), neg_mul, Int.floor_neg]; push_cast; ring
  · subst h; simp
  · rw [if_neg (by linarith), if_pos h.le, neg_mul, Int.ceil_neg]; push_cast; ring

lemma Qp_conj (p : ℕ) (z : ℂ) : Butterfly.Qp p (starRingEnd ℂ z) = starRingEnd ℂ (Butterfly.Qp p z) := by
  apply Complex.ext <;> simp [Butterfly.Qp, truncR_neg']

lemma QA_cnj (p : ℕ) (f : ι → ℂ) : QA p (cnj f) = cnj (QA p f) := by
  funext i; exact Qp_conj p (f i)

lemma Grid.cnj {p : ℕ} {f : ι → ℂ} (h : Grid p f) : Grid p (cnj f) := by
  unfold Grid at *; rw [QA_cnj, h]

end Arr

/-! ## Bilinear contractions -/

/-! ## The computed complex convolution `M̃_C` (§9.4.1) -/

/-! ## The computed chirp transform (§9.5) -/

/-! ## The source transform (§9.5.1) -/

/-! ## The pipeline (§9.7.2) -/

end

end NLogN.KFM

end

section
-- Source module: Solutions.R6BitNBStmt
/-!
# Round six, bit side: the statement `bitNetR6` (interface)

Accepted restatement (coordinator, 2026-10-19): the round-six bit network as a `QHNet` over
`ZMod 2` with `W = 148225616` roles and `m = 529`, valid runs, admissible Bruhat data and formal
frame correctness at every power of every large prime, and Jain's histogram. Consumed through
`prop11H_formal`.

`bitNetR6_mom` is the moment-dominance variant (all that `prop11H_formal` / `costH_bound` use):
it follows from `bitNetR6` (`bitNetR6_mom_of`).

This file holds the statements only (sorry-free). The pending `bitNetR6` lives in
`R6BitNBStmtX`; `bitNetR6_mom` is proved in `R6BitNBNetE`.
-/

namespace IntMul.Kappa.R6.Bit

/-- **Moment-dominance variant.** -/
def BitNetR6MomStmt : Prop :=
  ∃ (T : ℕ) (C : QHNet (ZMod 2) 148225616 T 529) (q₀ : ℕ), C.RunsOK ∧
    (∀ q, q.Prime → q₀ < q → ∀ f, C.EdgesOK (q ^ f) ∧ C.FormalOK (q ^ f)) ∧
    ∀ τ : ℝ, 0 < τ → τ ≤ 1 → histMoment C.hist 529 τ ≤ histMoment Jain.bitR6 529 τ

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6Params
/-!
# Round six: the parameter map `n ↦ (b, b', p, L, T, d, ℓ, r, K, α², V)` and the cost `Ncost6`

Stack parameters (Colkitt/Jain, `stack-notes.tex` §1 Idea D, Idea C):

* `b = lg n` (`bP6`), `b' = b^(1+x)` (`b'P6`; `x : ℕ` so `⌈b^(1+x)⌉ = b^(1+x)`), `p = 6 b'` (`pP6`);
* `L` (`LP6`) = least `L` with `4n ≤ 2^L b'`, `T = 2^L` (`TP6`), so `4n ≤ T b' < 8n`;
* `d = ⌊b^ε⌋` (`dP6`), `ℓ = ⌈L/d⌉ = (L + d - 1)/d` (`ℓP6`), `r = 2^ℓ` (`rP6`),
  `K = ℓ - 1` (`KP6`, one chunk per axis);
* `α² = ⌊p/(48d)⌋ = ⌊b'/(8d)⌋` (`α2P6`, a natural number), `α = √(α²)` (`αP6`),
  `γ = 2 d α²` (`γP6`);
* bit volume `V = T p` (`VP6`), with `24 n ≤ V ≤ 48 n`.

## Normalization (same as OpenAI's `RCost.Ncost`)
`Ncost6` is the **per-bit** cost: the Table-1 cost divided by `V = T p`.  The machine time is
`C₀ (V · Ncost6 · polylog + n)`; since `V ≤ 48 n`, a bound `Ncost6 ≤ C b^(1-gap) polylog`
gives time `O(n lg^(1-gap) polylog)`.

`Ncost6 P n = d + ℓ d^λ' + d p^δ + (ℓ + log₂ p) + p^δ + ℓ (d ln p)^τ + 1`
(rows: prefix moves `1-ε`; butterflies `ε(1-λ')`; fine exposures/Gaussian/chirps/reserved axes
`1-ε-poly`; pointwise products `ε`; precision `p^δ = b^poly`; CRT reversal
`ε(1-τ) = max(ε,1-ε)(1-τ)` as `ε ≥ 1/2`).  Note `ℓ ≈ b^(1-ε)` and `p^δ ≤ 6 b^poly`.
-/

open Real

namespace IntMul.Kappa.R6

noncomputable section

/-! ## 1. The parameter map -/

/-- `r = 2^ℓ`. -/
def rP6 (P : Prm) (n : ℕ) : ℕ := 2 ^ ℓP6 P n

/-! ## 2. Elementary facts about `lg` -/

/-! ## 3. Facts valid as soon as `b ≥ 4` -/

/-! ## 4. Eventual facts (box exponent and volume) -/

/-! ## 5. The cost bound -/

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6Ifaces
/-!
# Round six: the stack interfaces of the top-level assembly (fixed statements)

This file fixes the names and statements of every stack interface that the round-six top-level
assembly `kappa_final6` (file `R6MFinal.lean`) takes as a hypothesis. Each one is a `Prop`
depending on the parameter record `P : Prm` (and, where it runs inside the machine's table, on
the Lemma 12 table `tab` of the bit network). The interfaces are

| name | piece | intended `Ncost6` row (margin) |
|---|---|---|
| `SetupNeed6` | §9.2 parameters, sources (sieve), register file | lower order (`O(V)` suffices) |
| `CrtNeed6` | `Φ` / `Φ⁻¹` with the E′ CRT reversal | `d` (`1-ε`) and `ℓ (d ln p)^τ` (`max(ε,1-ε)(1-τ)`) |
| `FineNeed6` | fine-bit exposure (Idea A) | feeds `d p^δ` (`1-ε-poly`) |
| `LineNeed6` | `A` lines (PR #5 chirped Gaussian), `B₀` lines (segmented inverse) | `d p^δ` (`1-ε-poly`) |
| `P14Need6` | the uniform Prop 14 `P14UH'` (file `R6IL3Iface2`; proved in `R6IL3Cfg6`) | `ℓ d^λ'` (`ε(1-λ')`) |
| `P18IL6` | Prop 18 from `P14UH'` | `ℓ d^λ'`, `d`, `ℓ + log₂ p` (`ε`), `p^δ` |

**Weakness.** Every cost bound is stated against the whole unit
`cU6 P n A = V · Ncost6 · (log lg n + 1)^A` (the assembly makes a bounded number of calls, so this
is all it needs); the docstrings name the row the construction is meant to meet. Every error
bound is `errW6 P n · 2^{-p} = 2^{⌊p/2⌋ - p}` (much larger than the frozen constants; the final
rounding has room for it since `γ = 2 d α² ≤ b'/4` and `p = 6 b'`). The interfaces are stated
only at the round-six parameters of `n` for `n ≥ n₁` (`n₁` chosen by the prover), for every
source list satisfying `SrcOK6`. The interfaces used inside the machine's table receive as
hypotheses everything the assembly has about the Lemma 12 table `tab` (`SwapNeedτ`, `RowUCP`,
`FineU6`, `P14UH`).

**Parameters** (all for `n` and `P`): digit bits `b' = b'P6`, `p = 6b'`, `L = LP6`, `T = 2^L`,
`d = dP6`, `ℓ = ℓP6`, `h = ℓ - 1`, `r = 2^ℓ`, `K = ℓ - 1`, the natural `α = αN6 = ⌊√(p/(48d))⌋`,
`γ = 2 d α²`, the number of half axes `d' = dℓ - L`; axis `j < d` has `t_j = 2^h` for `j < d'`
and `t_j = 2^{h+1}` for `j ≥ d'` (`tF6`), so `∏ t_j = T` and the last axis has length `r`.
Sources: `SrcOK6` (odd, pairwise coprime, `t_j - 2w_j < s_j ≤ t_j - w_j`, `w_j = ⌊t_j/(8d²)⌋`,
Jain's window with `η ≈ 1/(8d²) ≤ 1/(4 d L^ε)`), and `μ_j = (∏_{i<j} s_i)⁻¹ mod s_j` (`muR6`).
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFH NLogN.KFM IntMul.OpenAI.RT AModel

noncomputable section

/-! ## Run-time parameters of the machine -/

/-- The source box on `Fin (D+1)`. -/
def sD6 (s : ℕ → ℕ) (D : ℕ) : Fin (D + 1) → ℕ := fun i => s i.val

/-- The padded box on `Fin (D+1)`. -/
def tD6 (P : Prm) (n D : ℕ) : Fin (D + 1) → ℕ := fun i => tF6 P n i.val

/-! ## The register file left by the setup -/

/-! ## The setup -/

/-- **`SetupNeed6`: the §9.2 setup (sources by the sieve), as one procedure.**

For rational `ε` (so that `d = ⌊b^ε⌋` is computable), for any Lemma 12 table `tab`: a fixed
table `kTableP tab ext` with an entry `eS`, and for each `n ≥ n₁` a source list `src n` with
`SrcOK6`, such that from the state after the reads (`KFM.readSt x y`, `|x| = |y| = n`) the call
reaches a state with the register file `BaseOK6`, stacks `0` and `pW` empty, `ARGM` as after the
reads, and no output yet.

Cost row: lower order. The construction costs `poly(b) · d · r ≪ V`; the statement allows
`C₀ · cU6`. (Sources: `J6Sieve.exists_coprime_in_windows_of_log` with `A_j = t_j - 2w_j`,
`H = w_j`, searched in increasing order.) -/
def SetupNeed6 (P : Prm) : Prop :=
  (∃ q : ℚ, P.ε = q) →
  ∀ tab : Fin 1 → IStmt HS 1,
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eS : Fin (7 + E)) (src : ℕ → ℕ → ℕ) (C₀ : ℝ)
    (A n₁ : ℕ), 0 ≤ C₀ ∧
  ∀ n, n₁ ≤ n → SrcOK6 P n (src n) ∧
    ∀ (Isym : List Sym) (x y : List Bool), x.length = n → y.length = n →
      ∃ (t : IState HS) (c : ℕ), IRuns Isym (IL.kTableP tab ext) (.call eS) (readSt x y) t c ∧
        BaseOK6 P n (src n) t ∧ t.G 0 = [] ∧ t.G pW = [] ∧ t.G ARGM = (readSt x y).G ARGM ∧
        t.out = [] ∧ (c : ℝ) ≤ C₀ * cU6 P n A

/-! ## `Φ` with the E′ CRT reversal -/

/-! ## Fine-bit exposure -/

/-- The descriptor of a fine exposure `[w, f, a, y]`. -/
def descFine (w f a y : ℕ) : List ℤ := [(w : ℤ), (f : ℤ), (a : ℤ), (y : ℤ)]

/-- Blockwise transposition: `a` consecutive blocks, each an `m × k` row-major array, each
transposed to `k × m`. -/
def blkT (m k a : ℕ) (zs : List GI) : List GI :=
  (List.range a).flatMap fun i =>
    IntMul.HvdH.Ref.transposeL m k ((zs.drop (i * (m * k))).take (m * k))

/-- The cost allowed for one fine exposure: `(w+1)(V+1)(f+1)` plus a descriptor term. -/
def cFine (w f a y : ℕ) : ℝ :=
  ((w : ℝ) + 1) * (((a * 2 ^ f * y : ℕ) : ℝ) + 1) * ((f : ℝ) + 1) +
    (((Nat.size (a * 2 ^ f * y) + w + f + 4) ^ 2 : ℕ) : ℝ)

/-- The guarantee of the fine exposure procedures `eF` (`(A, 2^f, Y) → (A, Y, 2^f)`) and `eB`
(its inverse) in a table `tbl`. -/
def FineBody6 {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (eF eB : Fin Pp)
    (dS : Fin HS) (C₀ : ℝ) : Prop :=
  ∀ (w f a y : ℕ) (s : IState HS) (F : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → F j = []) → F dS = descFine w f a y → F 0 = gflat zs ++ l →
    1 ≤ y → zs.length = a * (2 ^ f * y) → GB w zs →
    (∃ c : ℕ, IRuns Isym tbl (.call eF) (encK s F)
        (encK s (Function.update F 0 (gflat (blkT (2 ^ f) y a zs) ++ l))) c ∧
      (c : ℝ) ≤ C₀ * cFine w f a y) ∧
    (∃ c : ℕ, IRuns Isym tbl (.call eB) (encK s F)
        (encK s (Function.update F 0 (gflat (blkT y (2 ^ f) a zs) ++ l))) c ∧
      (c : ℝ) ≤ C₀ * cFine w f a y)

/-- **Fine exposure as procedures** of any extension of `kTableP tab` (placed by the user, as in
`P14UH`). -/
def FineU6 (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (eF eB : Fin nU) (dS : Fin HS) (C₀ : ℝ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nU → Fin (7 + E)),
      (∀ i, IL.kTableP tab ext (idx i) = U E idx i) →
      ∀ Isym : List Sym, FineBody6 Isym (IL.kTableP tab ext) (idx eF) (idx eB) dS C₀

/-- **`FineNeed6`: fine-bit exposure (Idea A, Jain's fine-field lemma (a)).** An array of
Gaussian items of shape `(A, 2^f, Y)` (row-major, `A = |X|·|J|` blocks, the `f` low bits `u` of
the exposed axis, the suffix `Y`) is brought to `(A, Y, 2^f)` and back, in `f` digit moves of
`O(V)` each.

Cost row: `O((w+1) V f)` per exposure with `f = O(log p)`, used `O(1)` times per axis inside the
line maps: row `d p^δ` (margin `1-ε-poly`). -/
def FineNeed6 (P : Prm) : Prop :=
  ∀ tab : Fin 1 → IStmt HS 1, IL.SwapNeedτ tab P.τ → IL2.RowUCP 576 P.τ tab → FineU6 tab

/-! ## The line maps (segmented inverse, PR #5) -/

/-- The body of `LineNeed6` in one table. -/
def LineBody6 (P : Prm) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eA eB : Fin (7 + E)) (dS : Fin HS) (C₀ : ℝ)
    (A n₁ : ℕ), dS ≠ 0 ∧ 0 ≤ C₀ ∧
  ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
  ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
  ∃ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D),
  ∀ (Isym : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = descLine6 P n src →
    (∀ (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (sD6 src D i)) → ℂ),
      f 0 = gflat zs ++ l → RepPad (pP6 P n) (sD6 src D) (tD6 P n D) zs u → ‖u‖ ≤ 1 / 2 →
      ∃ (zs' : List GI) (w : ((i : Fin (D + 1)) → ZMod (tD6 P n D i)) → ℂ) (c : ℕ),
        IRuns Isym (IL.kTableP tab ext) (.call eA) (encK s f)
          (encK s (Function.update f 0 (gflat zs' ++ l))) c ∧
        RepFull (pP6 P n) (tD6 P n D) zs' w ∧ GB (pP6 P n + 2) zs' ∧
        ‖w - tensCLM (kerA M.A) u‖ ≤ errW6 P n * hp (pP6 P n) ∧
        (c : ℝ) ≤ C₀ * cU6 P n A) ∧
    (∀ (ys : List GI) (y : ((i : Fin (D + 1)) → ZMod (tD6 P n D i)) → ℂ),
      f 0 = gflat ys ++ l → RepFull (pP6 P n) (tD6 P n D) ys y → ‖y‖ ≤ 1 →
      ∃ (ys' : List GI) (v : ((i : Fin (D + 1)) → ZMod (sD6 src D i)) → ℂ) (c : ℕ),
        IRuns Isym (IL.kTableP tab ext) (.call eB) (encK s f)
          (encK s (Function.update f 0 (gflat ys' ++ l))) c ∧
        RepPad (pP6 P n) (sD6 src D) (tD6 P n D) ys' v ∧ GB (pP6 P n + 2) ys' ∧
        ‖v - tensCLM (kerB M.B) y‖ ≤ errW6 P n * hp (pP6 P n) ∧
        (c : ℝ) ≤ C₀ * cU6 P n A)

/-- **`LineNeed6`: the line maps of the source transform** (steps 3a and 3c of §9.5), on the
arrays exactly as the machine holds them (as the frozen `KFM.LineNeed`): `A` lines take the padded
`s`-box function `u` to the full `t`-box function `≈ (⊗ A_i) u`, `B₀` lines take `y` to the padded
`≈ (⊗ B_i) y`, for per-axis exact maps `M : AxisMaps6` fixed per `n` (and source list) before the
input. Implementation: PR #5's chirped-correlation Gaussian for `S'`/`A`, the segmented inverse
(exact q-LU / Woodbury) for `B₀`, each axis exposed by `FineU6`.

Cost row: `d p^δ` (Gaussian line maps, margin `1-ε-poly`); the statement allows `C₀ · cU6`. -/
def LineNeed6 (P : Prm) : Prop :=
  ∀ tab : Fin 1 → IStmt HS 1, IL.SwapNeedτ tab P.τ → IL2.RowUCP 576 P.τ tab → FineU6 tab →
    LineBody6 P tab

/-! ## Proposition 14 and Proposition 18 -/

/-- The body of `P18IL6` in one table (the frozen `KFM.P18IL` at the round-six parameters). -/
def P18Body6 (P : Prm) (tab : Fin 1 → IStmt HS 1) : 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 : ℕ), n₁ ≤ n →
  ∀ (ts : List ℕ), ts.length + 1 = dP6 P n → (∀ t ∈ ts, t = rP6 P n ∨ 2 * t = rP6 P n) →
    ts.prod * rP6 P n = TP6 P n →
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (zf zg : List GI) (l : List ℤ)
    (xf xg : List (Fin (rP6 P n) → ℂ)),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = desc18 (pP6 P n) (ℓP6 P n) (KP6 P n) ts →
    f 0 = gflat zf ++ gflat zg ++ l →
    RecRep (rP6 P n) (pP6 P n) zf xf → RecRep (rP6 P n) (pP6 P n) zg xg →
    xf.length = ts.prod → xg.length = ts.prod →
    GB (pP6 P n + 2) zf → GB (pP6 P n + 2) zg →
    (∀ x ∈ xf, ‖x‖ ≤ 1) → (∀ x ∈ xg, ‖x‖ ≤ 1) →
    ∃ (zh : List GI) (xh : List (Fin (rP6 P n) → ℂ)) (c : ℕ),
      IRuns Isym (IL.kTableP tab ext) (.call entry) (encK s f)
        (encK s (Function.update f 0 (gflat zh ++ l))) c ∧
      RecRep (rP6 P n) (pP6 P n) zh xh ∧ xh.length = ts.prod ∧ GB (pP6 P n + 2) zh ∧
      (∀ j < ts.prod, ∀ k : Fin (rP6 P n),
        ‖xh.getD j 0 k - (mrL (rP6 P n) ts xf xg).getD j 0 k‖ ≤ errW6 P n * hp (pP6 P n)) ∧
      (c : ℝ) ≤ C₀ * cU6 P n A

/-- **`P18IL6`: Proposition 18 in IL at the round-six parameters**, built on the uniform
Prop 14 (`IL3.P14UH' tab Ew P.lamp` with a guard `EwOK6`). Data: two row-major arrays of
`N = ∏ t_i` records of `r` Gaussian coefficients (`RecRep r p`, norm `≤ 1`); result within
`errW6 · 2^{-p}` of `M_r(f, g) = (f ∗ g)/(r N)`; descriptor `desc18 p ℓ K ts`.

Cost rows: the `ℓ` simultaneous butterfly rounds `ℓ d^λ'` (margin `ε(1-λ')`), the prefix moves `d`
(`1-ε`), the packed products `ℓ + log₂ p` (`ε`) and the precision `p^δ`. The statement allows
`C₀ · cU6`. -/
def P18IL6 (P : Prm) : Prop :=
  ∀ (tab : Fin 1 → IStmt HS 1) (Ew : ℕ → ℕ), EwOK6 P Ew → IL3.P14UH' tab Ew P.lamp →
    IL.SwapNeedτ tab P.τ → IL2.RowUCP 576 P.τ tab → FineU6 tab → P18Body6 P tab

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MTab
/-!
# Round-six machine: the top level and merged tables

* **`kappa_of_big6`**: the frozen `KFM.kappa_of_big` with the round-six final reduction
  `kappaBound_of_machine6`: a merged table with the FM multiplier at `pM` and a large-`n`
  procedure meeting `BigSpec` with cost `Tb` inside `C₀ (V · Ncost6 · (log lg n + 1)^A + n)` gives
  `KappaBound κ` for every `κ < P.gap`.
* **`mExt4`**: four interface tables `kTableP tab ext_i` and the machine's own procedures merged
  into one `kTableP tab (mExt4 …)` (the frozen `KFM.mExt` with one more slot and `kTable → kTableP
  tab`); **`mTab4_g1 … mTab4_g4`**, **`mTab4_own`** are the hypotheses of `IRuns.relabel`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM IL

noncomputable section

/-! ## The top level -/

/-! ## Merging four interface tables -/

section Merge

variable {E₁ E₂ E₃ E₄ E₀ : ℕ}

variable (tab : Fin 1 → IStmt HS 1) (ext₁ : Fin E₁ → IStmt HS (7 + E₁))
  (ext₂ : Fin E₂ → IStmt HS (7 + E₂)) (ext₃ : Fin E₃ → IStmt HS (7 + E₃))
  (ext₄ : Fin E₄ → IStmt HS (7 + E₄)) (own : Fin E₀ → IStmt HS (7 + (E₁ + E₂ + E₃ + E₄ + E₀)))

def g4₂ (E₁ E₂ E₃ E₄ E₀ : ℕ) : Fin (7 + E₂) → Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  gI E₂ _ E₁ (by omega)
def g4₃ (E₁ E₂ E₃ E₄ E₀ : ℕ) : Fin (7 + E₃) → Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  gI E₃ _ (E₁ + E₂) (by omega)
def g4₄ (E₁ E₂ E₃ E₄ E₀ : ℕ) : Fin (7 + E₄) → Fin (7 + (E₁ + E₂ + E₃ + E₄ + E₀)) :=
  gI E₄ _ (E₁ + E₂ + E₃) (by omega)

end Merge

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MQ
/-!
# Round-six machine: the run-time parameters of one size

`Q6` bundles the parameter record `P`, the input size `n` and the source list `src` (chosen by
the setup). All parameters of the machine are functions of `Q : Q6` (`Q.b = b'`, `Q.p = 6b'`,
`Q.L`, `Q.d`, `Q.ℓ`, `Q.h = ℓ − 1`, `Q.α`, `Q.K`, `Q.r`, the boxes `Q.sB D`, `Q.tB D`, `S`, `M`,
the error allowance `Q.er = errW6` and the source-transform error `Q.Es`).

`QOk Q` collects the numerical facts the assembly uses (proved for large `n` in `R6MFacts`).

* `prod_tB`, `tB_last`, `tBox_eq6`, `crtOK6`: the boxes.
* `regIdx6`, `BaseOK6.of_agree`, `BaseOK6.upd`: the register file is kept by writes elsewhere.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM IntMul.OpenAI.RT AModel

noncomputable section

namespace Q6

variable (Q : Q6)

abbrev r : ℕ := rP6 Q.P Q.n

abbrev dp : ℕ := dpN6 Q.P Q.n
abbrev mu : ℕ → ℕ := muR6 Q.src
abbrev sB (D : ℕ) : Fin (D + 1) → ℕ := sD6 Q.src D
abbrev tB (D : ℕ) : Fin (D + 1) → ℕ := tD6 Q.P Q.n D

abbrev dPh : List ℤ := descPhi6 Q.P Q.n Q.src
abbrev dLn : List ℤ := descLine6 Q.P Q.n Q.src
abbrev dCh : List ℤ := descChirp6 Q.P Q.n Q.src
/-- The register file. -/
abbrev Base (t : IState HS) : Prop := BaseOK6 Q.P Q.n Q.src t

end Q6

namespace QOk

variable {Q : Q6} (hQ : QOk Q)
include hQ

end QOk

/-! ## The register file -/

/-- The register stacks of `BaseOK6`. -/
def regIdx6 : List (Fin HS) := [6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 25, 26, 27, 28]

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MCpy
/-!
# Round-six machine: copying a stored descriptor

The setup leaves the descriptors of the interface calls on `zPh`, `zLn`, `zCh` (`BaseOK6`). Before
a call, `cpyD Z X k c` copies the `k d + c` integers on top of `Z` onto the builder stack `X`
and leaves `Z` as it was (`d` from `zDd`; scratch `40`, counter `41`):
`mvK Z 40 41 n` moves them to `40` reversed, then a counted loop pushes each one back on `Z` and
on `X`.

* **`cpyD_sp`**: the specification on managed states.
* **`cpyD_run`**: the form `callW_I` uses: from any state with the descriptor on top of `Z`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL RS

noncomputable section

/-- The scratch stack of the copy. -/
abbrev yC : Fin HS := 40
/-- The counter of the copy. -/
abbrev cC : Fin HS := 41

/-- `k` copies of `zDd` plus `c`. -/
def lenE : ℕ → ℕ → Ex HS
  | 0, c => .lit c
  | k + 1, c => .add (.reg zDd) (lenE k c)

/-- One step of the copy loop. -/
def cpyB (Z X : Fin HS) : RS := .seq (.push X (.reg yC)) (.seq (.push Z (.reg yC)) (.pop yC))

/-- **The copy.** -/
def cpyD (Z X : Fin HS) (k c : ℕ) : RS := .seq (mvK Z yC cC (lenE k c)) (.rep cC (lenE k c) (cpyB Z X))

/-- The states of the loop. -/
def cpyF (f : Fin HS → List ℤ) (Z X : Fin HS) (rv : List ℤ) (k : ℕ) : Fin HS → List ℤ :=
  Function.update (Function.update (Function.update f yC (rv.drop k)) X (rv.take k).reverse) Z
    (rv.take k).reverse

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MPh
/-!
# Round-six machine: the interface calls

The frozen `KFMBig2` / `KFMBig3` at the round-six parameters. Every interface call is
`callW (cpyD Z X k c) X Y dS e`: the builder copies the stored descriptor (`zLn`, `zCh`, `zPh`,
length `k d + c`) onto the builder stack `X = bX dS`. The interfaces run in their own tables
`kTableP tab ext` and are relabelled into the merged table (`callW_I`).

* `lineG6`, `chirpG6`, `phiG6`: the per-size guarantees (bodies of `LineNeed6`, the chirp, and
  `CrtNeed6`).
* **`lineA_phase6`**, **`lineB_phase6`**, **`chirp_phase6`**, **`phi_phase6`**.
* **`phiF_rep6`**: the digits after `Φ` (frozen `phiF_rep`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open AModel AModelL12 IntMul NLogN NLogN.KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT
  IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM

noncomputable section

/-! ## The builder of a call -/

/-- The cost bound of `cpyD` for a descriptor of length `len` with entries of `B` bits. -/
def kCpy (k len B : ℕ) : ℕ := 2 * (2 * k + 2) * 2000 * (B + 2) + len * (40000 * (B + 2) + 30) + 64

/-! ## The guarantees per size -/

section Guar

variable {E : ℕ}

/-- **The line maps for one size** (body of `LineBody6` after the axis maps). -/
def lineG6 (Isym : List Sym) (tbl : Fin (7 + E) → IStmt HS (7 + E)) (eA eB : Fin (7 + E))
    (dS : Fin HS) (C₀ : ℝ) (A : ℕ) (Q : Q6) (D : ℕ) [∀ i, NeZero (Q.sB D i)]
    [∀ i, NeZero (Q.tB D i)] (M : AxisMaps6 Q.α (Q.sB D) (Q.tB D)) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = Q.dLn →
    (∀ (zs : List GI) (u : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ),
      f 0 = gflat zs ++ l → RepPad Q.p (Q.sB D) (Q.tB D) zs u → ‖u‖ ≤ 1 / 2 →
      ∃ (zs' : List GI) (w : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) (c : ℕ),
        IRuns Isym tbl (.call eA) (encK s f) (encK s (Function.update f 0 (gflat zs' ++ l))) c ∧
        RepFull Q.p (Q.tB D) zs' w ∧ GB (Q.p + 2) zs' ∧
        ‖w - tensCLM (kerA M.A) u‖ ≤ Q.er * hp Q.p ∧
        (c : ℝ) ≤ C₀ * cU6 Q.P Q.n A) ∧
    (∀ (ys : List GI) (y : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ),
      f 0 = gflat ys ++ l → RepFull Q.p (Q.tB D) ys y → ‖y‖ ≤ 1 →
      ∃ (ys' : List GI) (v : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) (c : ℕ),
        IRuns Isym tbl (.call eB) (encK s f) (encK s (Function.update f 0 (gflat ys' ++ l))) c ∧
        RepPad Q.p (Q.sB D) (Q.tB D) ys' v ∧ GB (Q.p + 2) ys' ∧
        ‖v - tensCLM (kerB M.B) y‖ ≤ Q.er * hp Q.p ∧
        (c : ℝ) ≤ C₀ * cU6 Q.P Q.n A)

/-- **The chirp for one size** (as the frozen `chirpGN`, error `Q.er`). -/
def chirpG6 (Isym : List Sym) (tbl : Fin (7 + E) → IStmt HS (7 + E)) (eC : Fin (7 + E))
    (dS : Fin HS) (C₀ : ℝ) (A : ℕ) (Q : Q6) (D : ℕ) [∀ i, NeZero (Q.tB D i)]
    (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = Q.dCh →
    ∀ (xs : List GI) (x : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ),
      f 0 = gflat xs ++ l → RepFull Q.p (Q.tB D) xs x → ‖x‖ ≤ 6 / 10 →
      ∃ (Mrt : (((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ)),
        (∀ f g, Grid Q.p f → Grid Q.p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 →
          ‖Mrt f g - mrX (Q.tB D) f g‖ ≤ Q.er * hp Q.p) ∧
      ∃ (ys : List GI) (c : ℕ),
        IRuns Isym tbl (.call eC) (encK s f) (encK s (Function.update f 0 (gflat ys ++ l))) c ∧
        RepFull Q.p (Q.tB D) ys (chirpT Q.p (mcT Q.p Mrt θt θit) bt at' x) ∧
        GB (Q.p + 2) ys ∧
        (c : ℝ) ≤ C₀ * cU6 Q.P Q.n A

/-- **`Φ` for one size** (body of `CrtBody6`). -/
def phiG6 (Isym : List Sym) (tbl : Fin (7 + E) → IStmt HS (7 + E)) (eF eB : Fin (7 + E))
    (dS : Fin HS) (C₀ : ℝ) (A : ℕ) (Q : Q6) : Prop :=
  ∀ (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ),
    (∀ j, j ≠ 0 → j ≠ dS → f j = []) →
    f dS = Q.dPh →
    (∀ xs : List ℤ, f 0 = xs ++ l →
      xs.length = vol (KFU.shK Q.d (KFU.sP Q.d Q.src)) → Bnd (Q.p + 2) xs →
      ∃ c : ℕ, IRuns Isym tbl (.call eF) (encK s f)
          (encK s (Function.update f 0 (KFU.PhiD Q.h Q.d Q.bL Q.src Q.mu xs ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cU6 Q.P Q.n A) ∧
    (∀ ys : List ℤ, f 0 = ys ++ l →
      ys.length = vol (KFU.shR Q.d (KFU.tP Q.d Q.h Q.bL)) → Bnd (Q.p + 2) ys →
      ∃ c : ℕ, IRuns Isym tbl (.call eB) (encK s f)
          (encK s (Function.update f 0 (KFU.PhiInvD Q.h Q.d Q.bL Q.src Q.mu ys ++ l))) c ∧
        (c : ℝ) ≤ C₀ * cU6 Q.P Q.n A)

end Guar

/-! ## The phases -/

/-- The cost bound of a call with a copied descriptor of `k d + c` entries of `Bd` bits. -/
def kCall6 (Q : Q6) (k c Bd : ℕ) (C₀ : ℝ) (A : ℕ) : ℝ :=
  1 + (kCpy k (k * Q.d + c) (Bd + Q.b) : ℝ) + 3 * (k * Q.d + c) * KFM.cMv Bd + 101 +
    C₀ * cU6 Q.P Q.n A

/-! ## The digits after `Φ` -/

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MFt
/-!
# Round-six machine: the source transform and one input

The frozen `KFMChain` / `KFMBig4` / `KFMBig5` / `KFMBig6` at the round-six parameters:

* `lemma20_6`, **`source_call6`**, `w_small6`: Lemma 20 and one source transform with the exact
  per-axis maps `AxisMaps6` (only `A, B, hA, hB, hid` are used);
* **`ftil_phase6`**: `A`-lines; chirp; `B₀`-lines; `×2^γ`;
* `Ix6`, **`BigCtx6`**: the fixed data and the context of one size;
* `digW_runs6`, **`inP_phase6`**: one input.
-/

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

namespace IntMul.Kappa.R6

open AModel AModelL12 IntMul NLogN NLogN.KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT
  IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM Complex NLogN.KFZ

noncomputable section

/-! ## Lemma 20 with `AxisMaps6` -/

/-! ## The source transform -/

/-- The cost bound of the shift pass. -/
def kShl6 (Q : Q6) (D : ℕ) : ℕ :=
  cItem (2 ^ (Q.L + 1)) (1000 * (Q.p + 2 + 2 * (D + 1) * Q.α ^ 2 + 2))
      (Q.p + 2 + 2 * (D + 1) * Q.α ^ 2 + 1) + 2 * cCnt (2 ^ (Q.L + 1)) +
    cW (2 ^ (2 * (D + 1) * Q.α ^ 2)) + cW ((2 ^ (Q.L + 1) : ℕ) : ℤ)

section Ftil

variable {P P₃ P₄ : ℕ} {Isym : List Sym} {iprog : Fin P → IStmt HS P} {tab : Fin 1 → IStmt HS 1}
  {ext₃ : Fin P₃ → IStmt HS (7 + P₃)} {g₃ : Fin (7 + P₃) → Fin P}
  {ext₄ : Fin P₄ → IStmt HS (7 + P₄)} {g₄ : Fin (7 + P₄) → Fin P}

/-- The source transform. -/
def ftilP6 (g₃ : Fin (7 + P₃) → Fin P) (g₄ : Fin (7 + P₄) → Fin P) (eA eB : Fin (7 + P₃))
    (eC : Fin (7 + P₄)) (dSL dSC : Fin HS) : IStmt HS P :=
  .seq (callW (cpyD zLn (bX dSL) 2 4) (bX dSL) (bY dSL) dSL (g₃ eA))
    (.seq (callW (cpyD zCh (bX dSC) 2 5) (bX dSC) (bY dSC) dSC (g₄ eC))
      (.seq (callW (cpyD zLn (bX dSL) 2 4) (bX dSL) (bY dSL) dSL (g₃ eB)) (shlW KFM.rG)))

end Ftil

/-! ## The context of one size -/

/-- The fixed data of the program: the table maps of the four interfaces (setup, `Φ`, lines,
chirp), their entries and descriptor stacks. -/
structure Ix6 (P : ℕ) where
  P₁ : ℕ
  P₂ : ℕ
  P₃ : ℕ
  P₄ : ℕ
  g₁ : Fin (7 + P₁) → Fin P
  g₂ : Fin (7 + P₂) → Fin P
  g₃ : Fin (7 + P₃) → Fin P
  g₄ : Fin (7 + P₄) → Fin P
  eS : Fin (7 + P₁)
  eF : Fin (7 + P₂)
  eI : Fin (7 + P₂)
  eA : Fin (7 + P₃)
  eB : Fin (7 + P₃)
  eC : Fin (7 + P₄)
  dSΦ : Fin HS
  dSL : Fin HS
  dSC : Fin HS

/-- **Everything the run for one size uses.** -/
structure BigCtx6 {E : ℕ} (ix : Ix6 (7 + E)) (Isym : List Sym) (tab : Fin 1 → IStmt HS 1)
    (extM : Fin E → IStmt HS (7 + E)) (Q : Q6) (D : ℕ) [∀ i, NeZero (Q.sB D i)]
    [∀ i, NeZero (Q.tB D i)] where
  hQ : QOk Q
  hD : Q.d = D + 1
  H : KFU.CrtOK (D + 1) Q.src Q.mu
  -- `Φ`
  ext₂ : Fin ix.P₂ → IStmt HS (7 + ix.P₂)
  hp₂ : ∀ j, IL.kTableP tab extM (ix.g₂ j) = (IL.kTableP tab ext₂ j).ren id ix.g₂
  CΦ : ℝ
  AΦ : ℕ
  hdΦ : ix.dSΦ ≠ 0
  hΦ : phiG6 Isym (IL.kTableP tab ext₂) ix.eF ix.eI ix.dSΦ CΦ AΦ Q
  BΦ : ℕ
  hBΦ : ∀ x ∈ Q.dPh, zsz x ≤ BΦ
  -- lines
  ext₃ : Fin ix.P₃ → IStmt HS (7 + ix.P₃)
  hp₃ : ∀ j, IL.kTableP tab extM (ix.g₃ j) = (IL.kTableP tab ext₃ j).ren id ix.g₃
  CL : ℝ
  AL : ℕ
  hdL : ix.dSL ≠ 0
  M : AxisMaps6 Q.α (Q.sB D) (Q.tB D)
  hL : lineG6 Isym (IL.kTableP tab ext₃) ix.eA ix.eB ix.dSL CL AL Q D M
  BL : ℕ
  hBL : ∀ x ∈ Q.dLn, zsz x ≤ BL
  -- chirp
  ext₄ : Fin ix.P₄ → IStmt HS (7 + ix.P₄)
  hp₄ : ∀ j, IL.kTableP tab extM (ix.g₄ j) = (IL.kTableP tab ext₄ j).ren id ix.g₄
  CC : ℝ
  AC : ℕ
  hdC : ix.dSC ≠ 0
  θt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ
  θit : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ
  at' : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ
  bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ
  ζ : ℂ
  hζ : ζ ^ Q.tB D (Fin.last D) = -1
  hθ : Phases Q.p (twX (Q.tB D) ζ) θt
  hθi : Phases Q.p (fun j => (twX (Q.tB D) ζ j)⁻¹) θit
  ha : Phases Q.p (fun j => (starRingEnd ℂ) (chirp (Q.sB D) (Q.tB D) j)) at'
  hb' : Phases Q.p (chirp (Q.sB D) (Q.tB D)) bt
  hbg : Grid Q.p bt
  hC : chirpG6 Isym (IL.kTableP tab ext₄) ix.eC ix.dSC CC AC Q D θt θit at' bt
  BC : ℕ
  hBC : ∀ x ∈ Q.dCh, zsz x ≤ BC

/-! ## The digit cut -/

/-- The cost of the digit cut. -/
def kDig6 (Q : Q6) : ℕ :=
  cDigU Q.b Q.e Q.M Q.S + cW (2 ^ Q.e) + cW (((2 * (Q.S - Q.M) : ℕ) : ℤ)) + cW (Q.M : ℤ) +
    cW (2 ^ Q.b)

/-! ## One input -/

variable {E : ℕ} {ix : Ix6 (7 + E)} {Isym : List Sym} {tab : Fin 1 → IStmt HS 1}
  {extM : Fin E → IStmt HS (7 + E)} {Q : Q6} {D : ℕ}
  [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]

/-- One input: the top of `ARGM` to the array `U`. -/
def inP6 (ix : Ix6 (7 + E)) : IStmt HS (7 + E) :=
  .seq (.op (.mv ARGM tX)) (.seq digW
    (.seq (callW (cpyD zPh (bX ix.dSΦ) 3 3) (bX ix.dSΦ) (bY ix.dSΦ) ix.dSΦ (ix.g₂ ix.eF))
      (ftilP6 ix.g₃ ix.g₄ ix.eA ix.eB ix.eC ix.dSL ix.dSC)))

/-- The digits `ū` of `x` on the box. -/
def ubar6 (C : BigCtx6 ix Isym tab extM Q D) (x : ℕ) :
    ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ :=
  fun k => (dgt Q.b Q.M x ((eB Q.src Q.mu C.H).symm k).val : ℂ)

/-- The cost bound of one source transform. -/
def kFt6 (C : BigCtx6 ix Isym tab extM Q D) : ℝ :=
  kCall6 Q 2 4 C.BL C.CL C.AL + kCall6 Q 2 5 C.BC C.CC C.AC + kCall6 Q 2 4 C.BL C.CL C.AL +
    kShl6 Q D

/-- The cost bound of one input. -/
def kIn6 (C : BigCtx6 ix Isym tab extM Q D) : ℝ :=
  ((2 * moveCost (Q.n + 1) + 19 + kDig6 Q : ℕ) : ℝ) + kCall6 Q 3 3 C.BΦ C.CΦ C.AΦ + kFt6 C

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MMul
/-!
# Round-six machine: the product and the rounding passes

The frozen `KFMBig7` / `KFMBig8` at the round-six parameters.

* **`mul_phase6`**: both inputs, the Gaussian product, conjugation and the third transform.
* **`finA_runs6`**: `conj; ×S; ×S; ×2^{2b+4}; round_p`.
-/

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

namespace IntMul.Kappa.R6

open AModel AModelL12 IntMul NLogN NLogN.KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT
  IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM Complex NLogN.KFZ

noncomputable section

/-! ## The product phase -/

/-- The width of the transform outputs. -/
def wU6 (Q : Q6) (D : ℕ) : ℕ := Q.p + 2 + (2 * (D + 1) * Q.α ^ 2 + 1)

/-- The cost of the Gaussian product pass. -/
def kGm6 (Q : Q6) (D : ℕ) : ℕ :=
  2 ^ Q.L * (4 * KFM.fmB (2 * wU6 Q D)) + 10 ^ 6 * (2 ^ Q.L + 1) * (wU6 Q D + Q.p + 1) +
    2 * cCnt (2 * 2 ^ Q.L) + cW (2 ^ Q.p) + cW ((2 * 2 ^ Q.L : ℕ) : ℤ) + cW ((2 ^ Q.L : ℕ) : ℤ)

/-- The cost of a conjugation pass at width `B`. -/
def kCj6 (Q : Q6) (B : ℕ) : ℕ :=
  cConj (2 ^ Q.L) B + cW ((2 * 2 ^ Q.L : ℕ) : ℤ) + cW ((2 ^ Q.L : ℕ) : ℤ)

variable {E : ℕ} {ix : Ix6 (7 + E)} {Isym : List Sym} {tab : Fin 1 → IStmt HS 1}
  {extM : Fin E → IStmt HS (7 + E)} {Q : Q6} {D : ℕ}
  [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]

/-- The product program. -/
def mulP6 (ix : Ix6 (7 + E)) : IStmt HS (7 + E) :=
  .seq (inP6 ix) (.seq (.seq (mvNU KFM.rT2 0 pO) (mvNU KFM.rT2 pO pW)) (.seq (inP6 ix) (.seq gmulW
    (.seq conjW (ftilP6 ix.g₃ ix.g₄ ix.eA ix.eB ix.eC ix.dSL ix.dSC)))))

/-- The cost bound of the product phase. -/
def kMul6 (C : BigCtx6 ix Isym tab extM Q D) : ℝ :=
  kIn6 C + ((2 * cMvN (2 ^ (Q.L + 1)) (wU6 Q D) : ℕ) : ℝ) + kIn6 C + (kGm6 Q D : ℝ) +
    (kCj6 Q (Q.p + 1) : ℝ) + kFt6 C

/-! ## The rounding passes -/

/-- The width of the rounding passes. -/
def wFR6 (Q : Q6) (D : ℕ) : ℕ := wU6 Q D + 4 * Q.b + 5

/-- The cost of one `×S` pass. -/
def kSm6 (Q : Q6) (D : ℕ) : ℕ :=
  cItem (2 ^ (Q.L + 1)) (KFM.fmB (2 * wFR6 Q D) + 5000 * (wFR6 Q D + 0 + 3)) (2 * wFR6 Q D) +
    2 * cCnt (2 ^ (Q.L + 1)) + cW (Q.S : ℤ) + cW (2 ^ 0) + cW ((2 ^ (Q.L + 1) : ℕ) : ℤ)

/-- The cost of the `×2^{2b+4}` pass. -/
def kShF6 (Q : Q6) (D : ℕ) : ℕ :=
  cItem (2 ^ (Q.L + 1)) (1000 * (wFR6 Q D + (2 * Q.b + 4) + 2)) (wFR6 Q D + (2 * Q.b + 4) + 1) +
    2 * cCnt (2 ^ (Q.L + 1)) + cW (2 ^ (2 * Q.b + 4)) + cW ((2 ^ (Q.L + 1) : ℕ) : ℤ)

/-- The cost of the rounding pass. -/
def kRd6 (Q : Q6) (D : ℕ) : ℕ :=
  cItem (2 ^ (Q.L + 1)) (3000 * (wFR6 Q D + Q.p + 3)) (2 * wFR6 Q D + 1) +
    2 * cCnt (2 ^ (Q.L + 1)) + cW (2 ^ (Q.p - 1)) + cW (2 ^ Q.p) +
    cW ((2 ^ (Q.L + 1) : ℕ) : ℤ)

/-- The cost of `finA`. -/
def kFinA6 (Q : Q6) (D : ℕ) : ℕ :=
  kCj6 Q (wU6 Q D) + (kSm6 Q D + (kSm6 Q D + (kShF6 Q D + kRd6 Q D)))

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MFin
/-!
# Round-six machine: the read-out and one run

The frozen `KFMBig9` / `KFMBig10` at the round-six parameters.

* `zsz_cN6`, `cconv_ubar6`, `pt_val6`, `zsW_GB6`: the rounded numerators are the coefficients.
* **`fin_phase6`**: `finA; Φ⁻¹; carries; write`.
* **`big_run6`**: `bigP6 = setup; mulP6; finP6` from the state after the reads, the setup being
  a call into a sub-table.
-/

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

namespace IntMul.Kappa.R6

open Finset AModel AModelL12 IntMul NLogN NLogN.KIL KFB KFT RS IntMul.HvdH IntMul.OpenAI.RT
  IntMul.OpenAI.RC IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM Complex

noncomputable section

variable {E : ℕ} {ix : Ix6 (7 + E)} {Isym : List Sym} {tab : Fin 1 → IStmt HS 1}
  {extM : Fin E → IStmt HS (7 + E)} {Q : Q6} {D : ℕ}
  [instS : ∀ i, NeZero (Q.sB D i)] [instT : ∀ i, NeZero (Q.tB D i)]

/-- The final closeness (the conclusion of `final_call3`). -/
def Close6 (C : BigCtx6 ix Isym tab extM Q D) (x y : ℕ)
    (Z : ((i : Fin (D + 1)) → ZMod (Q.sB D i)) → ℂ) : Prop :=
  ∀ j, ‖(2 : ℂ) ^ (2 * Q.b + 4) * ((∏ i, (Q.sB D i : ℝ) : ℝ) : ℂ) *
      (((∏ i, (Q.sB D i : ℝ) : ℝ) : ℂ) * cnj Z j) - cconv (Q.sB D) (ubar6 C x) (ubar6 C y) j‖ <
    1 / 2

/-- The rounded array. -/
def zsWf6 (Q : Q6) (zsZ : List GI) : List GI :=
  (zsZ.map gconj).map fun z => (rndV Q.p Q.b Q.S z.1, rndV Q.p Q.b Q.S z.2)

/-- The read-out program. -/
def finP6 (ix : Ix6 (7 + E)) : IStmt HS (7 + E) :=
  .seq finA (.seq (callW (cpyD zPh (bX ix.dSΦ) 3 3) (bX ix.dSΦ) (bY ix.dSΦ) ix.dSΦ (ix.g₂ ix.eI))
    (.seq carW (writeI 0 KFM.rO)))

/-- The cost bound of the read-out. -/
def kFin6 (C : BigCtx6 ix Isym tab extM Q D) : ℝ :=
  (kFinA6 Q D : ℝ) + kCall6 Q 3 3 C.BΦ C.CΦ C.AΦ +
    ((cCarU Q.b (Q.p + 2) Q.S + cW (Q.S : ℤ) + cW (2 ^ Q.b) + outRCost (2 * Q.n) : ℕ) : ℝ)

/-! ## One run -/

/-- **The program `bigE`**: the setup (a call into the setup sub-table), the product, the
read-out. -/
def bigP6 (ix : Ix6 (7 + E)) : IStmt HS (7 + E) :=
  .seq (.call (ix.g₁ ix.eS)) (.seq (mulP6 ix) (finP6 ix))

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6ZSD
/-!
# Round six, chirp: the Prop 18 descriptor for any parameters

The frozen `KFMSD.desc18P_run_n` / `desc18P_cost_n` with the values of `n` (`dP n, dpN n, rP n,
KP n, ℓP n, bP n`) replaced by free values `d₀ d₁ r₀ K₀ ℓ₀ b₀` on the registers.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFM

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

/-- The axis lengths: `d₀ - 1` entries, `r` from index `d₁` on, `r/2` before. -/
def tsG (d₀ d₁ r₀ : ℕ) : List ℕ :=
  (List.range (d₀ - 1)).map fun j => if d₁ ≤ j then r₀ else r₀ / 2

/-- The registers `desc18P` reads, with free values. -/
structure D18G (t : IState HS) (d₀ d₁ r₀ K₀ ℓ₀ b₀ : ℕ) : Prop where
  hD : ∃ L, t.G zD = .int (d₀ : ℤ) :: L
  hDp : ∃ L, t.G zDp = .int (d₁ : ℤ) :: L
  hR : ∃ L, t.G zR = .int (r₀ : ℤ) :: L
  hK : ∃ L, t.G zK = .int (K₀ : ℤ) :: L
  hEl : ∃ L, t.G zEl = .int (ℓ₀ : ℤ) :: L
  hB : ∃ L, t.G zB = .int (b₀ : ℤ) :: L

end NLogN.KFM

end

section
-- Source module: Solutions.R6ZCall
/-!
# Round six, chirp: the Prop 18 call and the product phase for any parameters

* `MG`, `dsG`: the side conditions and the Prop 18 descriptor for free `p h d σ K` (the frozen
  `KFZCall.M_runs` reads them through `n`).
* **`M_runsG`**: the frozen `M_runs` without `n`.
* **`PP_runsP`**: the frozen `PP_runs` in `IL.kTableP tab ext`, without `n`.
-/

set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KFZ

open IntMul NLogN.KIL KFB NLogN.KFM IntMul.OpenAI.Glue

/-- The side conditions of the descriptor program for free parameters. -/
structure MG (p h d σ K : ℕ) : Prop where
  p6 : 6 * (p / 6) = p
  b8 : 8 ≤ p / 6
  d1 : 1 ≤ d
  db : d ≤ p / 6
  r : 2 ^ (h + 1) ≤ 2 ^ (p / 6)
  Kd : K ≤ p / 6
  lb : h + 1 ≤ p / 6

/-- The Prop 18 descriptor for free parameters. -/
def dsG (p h d σ K : ℕ) : List ℤ := desc18 p (h + 1) K (tsG d (d - σ) (2 ^ (h + 1)))

end NLogN.KFZ

end