Round-six κ development, definitions part 23

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

import Definitions.Def_IntMul_Kappa_R6_Defs22
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
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_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_Kappa_K_Defs12
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs32
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs27
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_R6_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs19

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6IL3Top9
/-!
# Round six, item language (I3): the chain of the uniform Proposition 14

From the descriptor registers (`DescR`), `mainCH jZ` runs

* the size loop (`zloopC`, `j = size (32 W' P S r)`), then pushes `Zl = j + K D` on `vG`;
* the field-width loop (`gloopC`, `G = clog₂ (4 (Zl + cz)(Zl + cz + 2))`), then pushes `G` on `vG`;
* the depth loop (`dloopC`, `d = dep m D`, `W^d`);
* the core stage (`coreCH`) and the layer body (`bodyCH`).

**`chainQH`**: the run leaves `gflat zs* ++ l` on stack `0`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

def zIn : List (Fin HS × NE) := [(11, .lit 0), (12, .lit 1)]
def zlNE : NE := .add (.reg 11) (.mul (.reg 1) (.reg 22))
def dIn3 : List (Fin HS × NE) := [(11, .reg 22), (12, .lit 0), (13, .lit 1)]

/-- The entry of the chain. -/
def mainCH {Pp : ℕ} (jZ : Fin Pp) : IStmt HS Pp := withPushI (fr zIn) (.call jZ)

/-- After the size loop. -/
def zcontC {Pp : ℕ} (jG : Fin Pp) : IStmt HS Pp :=
  withPushI (fr [(vG, zlNE)]) (withPushI (fr zIn) (.call jG))

/-- After the field-width loop. -/
def gcontC {Pp : ℕ} (jD : Fin Pp) : IStmt HS Pp :=
  withPushI (fr [(vG, .reg 11)]) (withPushI (fr dIn3) (.call jD))

/-- The field-width constant. -/
abbrev czH : ℕ := 1

/-- The values of the chain. -/
structure ChV where
  za : ℕ
  Zl : ℕ
  G : ℕ
  d : ℕ
  q0 : ℕ
  Bp : ℕ
  H : ℕ
  qB : ℕ

/-- The values of the chain for a configuration and a descriptor. -/
def chV (c : Cfg) (cW P K D S r w : ℕ) : ChV :=
  let za := Nat.size (aV c P S r w D)
  let Zl := za + K * D
  let G := Gv czH Zl
  let d := dep c.m D
  let q0 := q0v c.m cW K D d G
  { za := za, Zl := Zl, G := G, d := d, q0 := q0, Bp := BpV c.W c.m K P D d G q0,
    H := w + EwH c D, qB := qBv c.m K D G q0 }

/-- The register bound of the chain. -/
def MbChain (c : Cfg) (cW P K D S r w : ℕ) : ℕ :=
  let v := chV c cW P K D S r w
  2 * aV c P S r w D + 2 * gBnd czH v.Zl + v.Zl + v.G + c.W ^ (v.d + 1) + c.m * D + 2 * c.m + D +
    (w + EwH c D + c.Aw * (D + 1) ^ c.p + (D + 1) ^ c.p + (cW + 4) * (K * D + K)) +
    MbBody c K P D S v.G v.q0 v.qB + 200

/-- The cost of the chain. -/
noncomputable def cChainH (c : Cfg) (CB : ℕ → ℝ) (cW P K D S r w Z Zr Bz : ℕ) : ℕ :=
  let v := chV c cW P K D S r w
  let cB := cBodyH c CB K S r v.H P D v.q0 v.qB v.Bp Z Zr Bz w
  let cC := cCoreH cB Z Bz (szC c)
  let cDl := cC + (v.d + 1) * cLoop 3 Bz
  let cGc := cFr1 12 Bz (cFrame 3 12 Bz + cDl + (3 * (2 * Bz + 2) + 1))
  let cGl := cGc + (v.G + 1) * cLoopS 15 2 Bz
  let cZc := cFr1 12 Bz (cFrame 2 12 Bz + cGl + (2 * (2 * Bz + 2) + 1))
  let cZl := cZc + (v.za + 1) * cLoopS (szZ c) 2 Bz
  cFrame 2 12 Bz + cZl + (2 * (2 * Bz + 2) + 1)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top10
/-!
# Round six, item language (I3): the entry procedure of the uniform Proposition 14

`p14CH jZ = dIn ; mainCH jZ ; dOut` (the frozen descriptor moves of `KFWC15`).

**`p14QH`**: on `encK st f` with the descriptor `[P, K, D, S, ρ, r, p, w, Z]` on stack `36`, the
array on stack `0` and the stacks `1 … 49` (but `36`) empty, `p14CH jZ` leaves
`gflat zs* ++ l` on stack `0` and restores every other stack.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The entry procedure. -/
def p14CH {Pp : ℕ} (jZ : Fin Pp) : IStmt HS Pp := .seq dIn (.seq (mainCH jZ) dOut)

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top11
/-!
# Round six, item language (I3): the cost of the chain in units

With `n = P 2^{K D} S`, `U = Yu r Zr H`, `X = (Sc c + 1) U`, `Y = (Sc c + 1) n U`:

**`cChainH_le`**: `cChainH ≤ (q₀ + q_B) ⌊CB 1 · n U⌋ + 401 ⌊CB E · n' U⌋
  + 10^10 (G + d + q₀ + q_B) X + 10^10 z_a (Sc+1)(Zr+3)^2 + 10^15 Y`
(`E = D - q₀ - q_B`, `n' = B' 2^{K (D - q₀)} S ≤ 2 n`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The bound on all frame sizes and program constants of a configuration. -/
def Sc (c : Cfg) : ℕ := szC c + szB c + szZ c + εSD.size + eL.size + 100

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top12
/-!
# Round six, item language (I3): the parameter facts of the uniform Proposition 14

Under the hypotheses of `P14NeedH'` (bundled in `Hyp14`, with guard `EwH c` and
`K₀ = K0c c = 2^{Zc c}`), the chain values `chV c (cWc c) P K D S r w` satisfy:

* `Zc c ≤ K`, `K + 5 < Z` (so every configuration constant is below `Z`);
* `Zl ≤ 2 Z + W'`, `Zl ≤ 2 p + W' + 5`, `G ≤ 2 zsz p + 2 W' + 10`;
* the field-width guards `4 Zl (Zl+2) ≤ 2^G`, `16 Zl (Zl+2) 2^G ≤ 2^K`;
* the chunk bound `cW d + 2 ⌊D/m⌋ G ≤ K D`;
* the kernel count `K (q₀ + q_B) ≤ K₀ D (zsz p + 1) + 2 K`;
* the width/exponent bounds of the body.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The size of all configuration constants. -/
noncomputable def Zc (c : Cfg) : ℕ :=
  c.Wr + c.W + c.Aw + c.p + cLH c + c.m + Sc c + c.Aw * (2 * c.m + 1) ^ c.p + 64

/-- The constant `K₀` of the uniform Proposition 14. -/
noncomputable def K0c (c : Cfg) : ℕ := 2 ^ Zc c

/-- The width exponent of the padding `W ≤ 2^cW`. -/
def cWc (c : Cfg) : ℕ := Nat.clog 2 c.W

/-- **The hypotheses of `P14NeedH'`** at guard `EwH c`, `K₀ = K0c c` (with `vol = P 2^{KD} S`). -/
structure Hyp14 (c : Cfg) (P K D S r p w Z : ℕ) (lamp : ℝ) : Prop where
  K6 : 6 ≤ K
  r1 : 1 ≤ r
  KZ : 80 * Z * (Z + 2) ≤ 2 ^ K
  S1 : 1 ≤ S
  P1 : 1 ≤ P
  D1 : 1 ≤ D
  Z32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z
  pZ : zsz (p : ℤ) ≤ Z
  Ew : EwH c D ≤ w + 1
  wZ : w + EwH c D + 2 < 2 ^ Z
  rZ : 2 * (2 * Z + 4) ^ 3 + 2 ≤ r
  h1 : zsz ((P * 2 ^ (K * D) * S * r + w + EwH c D : ℕ) : ℤ) ≤ p
  h2 : (p + K0c c) ^ 5 ≤ 2 ^ K
  h3 : ((K0c c * D * (zsz (p : ℤ) + 1) : ℕ) : ℝ) ≤ K * (D : ℝ) ^ lamp
  l0 : 0 ≤ lamp
  l1 : lamp ≤ 1

namespace Hyp14

variable {c : Cfg} {P K D S r p w Z : ℕ} {lamp : ℝ} (h : Hyp14 c P K D S r p w Z lamp)
include h

end Hyp14

namespace Hyp14

variable {c : Cfg} {P K D S r p w Z : ℕ} {lamp : ℝ} (h : Hyp14 c P K D S r p w Z lamp)
include h

end Hyp14

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top13
/-!
# Round six, item language (I3): the size bounds and the level claims of the chain

Under `Hyp14`, with `Zr = 3 Z` and `CB = CBc c Kc G Cc θ` (the closed form of `cbRec_of` with the
row factor `Kc (G+2) + 1` of `RowUCC`):

* `VbH` at the top level and at the middle level, and `MbChain`, are below `2^{3Z}`;
* `lvAllH`: every level claim `LvH … E` holds;
* `midPre`: the middle-part preconditions `MidPre`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The level cost coefficients at field width `G`. -/
noncomputable def CBc (c : Cfg) (Kc : ℝ) (G : ℕ) (Cc θ : ℝ) : ℕ → ℝ :=
  CBH c.m (Kc * (G + 2) + 1 + 1) Cc (10 ^ 14 * (2 * c.m + 1)) θ

namespace Hyp14

variable {c : Cfg} {P K D S r p w Z : ℕ} {lamp : ℝ} (h : Hyp14 c P K D S r p w Z lamp)
include h

end Hyp14

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Top15
/-!
# Round six, item language (I3): the cost closure of the uniform Proposition 14

Under `Hyp14` (with `Zr = Bz = 3 Z`, level costs `CBc c Kc G Cc θ`, `0 ≤ θ ≤ lamp`), the cost of
the entry procedure `p14CH` plus the call overhead is at most

  `C0c c Kc Cc · (n r) · (w + 1) · (zsz p + 1) · D^lamp`,

`C0c c Kc Cc = 20125 (Kc + 2)(2 W' + 12)(Cc + 10^14 (2m+1)) + 10^17 (Sc c + 1)(2 W' + 14)`.

The kernel levels contribute `(q₀ + q_B) · CB 1 · n U` with `q₀ + q_B ≤ 3 D^lamp`
(hypothesis (3)) and `CB 1 ≤ (Kc + 2)(G + 2)(Cc + D₀)`, `G + 2 ≤ (2 W' + 12)(zsz p + 1)`;
the middle level `401 · CB E · n' U ≤ 802 (Kc+2)(G+2)(Cc+D₀) D^lamp n U`; the loops
`(G + d + q₀ + q_B) (Sc+1) U` and `z_a (Sc+1)(3Z+3)^2 ≤ 27 (Sc+1) r`; `U ≤ 25 r (w+1)`.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

/-- The constant of the uniform Proposition 14. -/
noncomputable def C0c (c : Cfg) (Kc Cc : ℝ) : ℝ :=
  20125 * (((Kc + 2) * (2 * c.Wr + 12)) * (Cc + 10 ^ 14 * (2 * c.m + 1))) +
    10 ^ 17 * (((Sc c + 1 : ℕ) : ℝ) * (2 * c.Wr + 14))

/-- The total cost of the entry procedure (with the call overhead `2`). -/
noncomputable def cP14 (c : Cfg) (Kc Cc θ : ℝ) (P K D S r w Z : ℕ) : ℕ :=
  8 * (2 * moveCost Z + 19) + (cChainH c (CBc c Kc (chV c (cWc c) P K D S r w).G Cc θ) (cWc c)
    P K D S r w Z (3 * Z) (3 * Z) + 8 * (2 * moveCost Z + 19)) + 2

namespace Hyp14

variable {c : Cfg} {P K D S r p w Z : ℕ} {lamp : ℝ} (h : Hyp14 c P K D S r p w Z lamp)
include h

end Hyp14

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.R6IL3Iface2
/-!
# Round six, item language (I3): the uniform Proposition 14 with explicit size hypotheses

`P14NeedH'` is `IL3.P14NeedH` (same descriptor, stacks, guarantees and cost shape
`C₀ · vol·r · (w+1) · (zsz p + 1) · D^lamp`) with three additional hypotheses on the caller:

1. `zsz (vol·r + w + Ew D) ≤ p`        — the precision dominates the local sizes;
2. `(p + K₀)^5 ≤ 2^K`                   — the chunk width dominates `log p` (field-width guards);
3. `K₀ · D · (zsz p + 1) ≤ K · D^lamp`  — the kernel (reserved) parts, `≈ D (zsz p) / K` levels
   of cost `O(n r (w+1) (zsz p + 1))` each, fit the `(zsz p + 1) D^lamp` budget.

`K₀` is a constant of the construction (existential in `P14UH'`).  All three hold at the
round-six parameters for large `n` and every `K₀` (`IL3.p14_hyps_r6`; (3) is
`ε (2 - lamp) < 1`).
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.IL3

open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFH NLogN.KFV AModel Butterfly
  IntMul.Kappa.R6.IL

/-- **The uniform Proposition 14 with explicit size hypotheses** (see the module doc). -/
def P14NeedH' {Pp : ℕ} (Isym : List Sym) (tbl : Fin Pp → IStmt HS Pp) (e14 : Fin Pp)
    (dS14 : Fin HS) (Ew : ℕ → ℕ) (lamp : ℝ) (K₀ : ℕ) (C₀ : ℝ) : Prop :=
  ∀ {K r Z P D S ρ p w : ℕ} (hρ : ρ < K),
    6 ≤ K → 1 ≤ r → 80 * Z * (Z + 2) ≤ 2 ^ K → 1 ≤ S → 1 ≤ P → 1 ≤ D →
    zsz ((32 * (vol (layerShape P K D S) * r) : ℕ) : ℤ) ≤ Z → zsz (p : ℤ) ≤ Z →
    Ew D ≤ w + 1 → w + Ew D + 2 < 2 ^ Z →
    2 * (2 * Z + 4) ^ 3 + 2 ≤ r → (K * D + P + 10) * (Z + 2) ≤ vol (layerShape P K D S) * r →
    zsz ((vol (layerShape P K D S) * r + w + Ew D : ℕ) : ℤ) ≤ p →
    (p + K₀) ^ 5 ≤ 2 ^ K →
    ((K₀ * D * (zsz (p : ℤ) + 1) : ℕ) : ℝ) ≤ K * (D : ℝ) ^ lamp →
    ∀ (st : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
      (xs : List (Fin r → ℂ)), RecRep r p zs xs →
      xs.length = vol (layerShape P K D S) → f 0 = gflat zs ++ l →
      f dS14 = desc14 P K D S ρ r p w Z → (∀ j, p14Free dS14 j → f j = []) →
      GB w zs → (∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1) →
      ∃ (zs' : List GI) (c : ℕ),
        RecRep r p zs' (prop14Proc (P := P) (S := S) hρ p (tens Cm : Butterfly.Op (Fin D)) xs) ∧
        GB (p + 1) zs' ∧
        (∀ j (h : j < (prop14Proc (P := P) (S := S) hρ p (tens Cm : Butterfly.Op (Fin D)) xs).length)
          (h' : j < (layerH P K D S ρ hρ xs).length), ∀ c,
          ‖(prop14Proc (P := P) (S := S) hρ p (tens Cm : Butterfly.Op (Fin D)) xs)[j] c -
            (layerH P K D S ρ hρ xs)[j] c‖ < Real.sqrt 2 * 2⁻¹ ^ p) ∧
        IRuns Isym tbl (.call e14) (encK st f) (encK st (Function.update f 0 (gflat zs' ++ l))) c ∧
        (c : ℝ) ≤ C₀ * ((vol (layerShape P K D S) * r : ℕ) : ℝ) * (w + 1) * ((zsz (p : ℤ) : ℝ) + 1) *
          (D : ℝ) ^ lamp

/-- **Uniform Proposition 14, round six, explicit-hypothesis form.** -/
def P14UH' (tab : Fin 1 → IStmt HS 1) (Ew : ℕ → ℕ) (lamp : ℝ) : Prop :=
  ∃ (nU : ℕ) (U : ∀ E : ℕ, (Fin nU → Fin (7 + E)) → Fin nU → IStmt HS (7 + E))
    (entry : Fin nU) (dS14 : Fin HS) (K₀ : ℕ) (C₀ : ℝ),
    dS14 = 36 ∧ 0 ≤ C₀ ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nU → Fin (7 + E)),
      (∀ i, kTableP tab ext (idx i) = U E idx i) →
      ∀ Isym : List Sym, P14NeedH' Isym (kTableP tab ext) (idx entry) dS14 Ew lamp K₀ C₀

end IntMul.Kappa.R6.IL3

end

section
-- Source module: Solutions.R6IL3Top16
/-!
# Round six, item language (I3): the uniform Proposition 14 with explicit size hypotheses

**`p14UH'_of`**: for a configuration `c` (`CfgOK c`), exponents `0 ≤ τ ≤ θ ≤ lamp ≤ 1`, a
level constant `Cc` with the moment condition of `cbRec_of`, and compact-control row additions
`RowUCCP c.m τ tab` in every extension of `kTableP tab`, the uniform Proposition 14
`P14UH' tab (EwH c) lamp` holds, with `K₀ = K0c c = 2^{Zc c}` and `C₀ = C0c c Kc Cc`.

The procedure list `UUH` places the level procedure (`0`), the kernel loop (`1`), the
size loop (`2`), the field-width loop (`3`), the depth loop with the core and the body (`4`),
the entry (`5`), and then the row procedures.
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx IntMul.Kappa.R6.IL IntMul.Kappa.R6.IL3

/-- **Compact-control row additions as procedures** of any extension of `kTableP tab`
(the table form of `RowUCC`). -/
def RowUCCP (m : ℕ) (τ : ℝ) (tab : Fin 1 → IStmt HS 1) : Prop :=
  ∃ (nR : ℕ) (UR : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → Fin nR → IStmt HS (7 + E))
    (rowC : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → IStmt HS (7 + E)) (Kc : ℝ), 0 ≤ Kc ∧
    ∀ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (idx : Fin nR → Fin (7 + E)),
      (∀ q, kTableP tab ext (idx q) = UR E idx q) →
      ∀ Isym : List Sym, RowUCC m τ Isym (kTableP tab ext) (rowC E idx) Kc

/-- The row-procedure placement inside the list. -/
def iRH {nR E : ℕ} (idx : Fin (6 + nR) → Fin (7 + E)) : Fin nR → Fin (7 + E) :=
  fun q => idx ⟨q.val + 6, by omega⟩

/-- **The procedure list** of the round-six uniform Proposition 14. -/
noncomputable def UUH (c : Cfg) (nR : ℕ) (UR : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → Fin nR → IStmt HS (7 + E))
    (rowC : ∀ E : ℕ, (Fin nR → Fin (7 + E)) → IStmt HS (7 + E)) (E : ℕ)
    (idx : Fin (6 + nR) → Fin (7 + E)) (i : Fin (6 + nR)) : IStmt HS (7 + E) :=
  if h6 : i.val < 6 then
  (if i.val = 0 then levCH c (idx ⟨0, by omega⟩) (rowC E (iRH idx))
  else if i.val = 1 then kerLoopC (idx ⟨1, by omega⟩) (idx ⟨0, by omega⟩)
  else if i.val = 2 then zloopC c (idx ⟨2, by omega⟩) (zcontC (idx ⟨3, by omega⟩))
  else if i.val = 3 then gloopC czH (idx ⟨3, by omega⟩) (gcontC (idx ⟨4, by omega⟩))
  else if i.val = 4 then dloopC c.m c.W (idx ⟨4, by omega⟩)
    (coreCH c (cWc c) (bodyCH c (idx ⟨1, by omega⟩) (idx ⟨0, by omega⟩)))
  else p14CH (idx ⟨2, by omega⟩))
  else UR E (iRH idx) ⟨i.val - 6, by have := i.isLt; omega⟩

end IntMul.Kappa.R6.IL3H

end

section
-- Source module: Solutions.ResampleHvdH
/-! Copy (renamed namespace `IntMul.OpenAI.RH`) of the base thread's HvdH Prop 4.7(i)
(`intmul/base/Sol_prop_4_7_i.lean`): Gaussian resampling identity, maps S, T, C, D, P_s, P_t. -/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

section Resample

open Complex Real

namespace IntMul.OpenAI.RH

/-! ### Definitions (HvdH §2.4, §4.1) -/

/-! ### Gaussian sums -/

/-! ### Characters -/

/-! ### Linearity -/

/-! ### The resampling identity (HvdH Theorem 4.2) -/

end IntMul.OpenAI.RH

end Resample

section Bounds

open Real

namespace IntMul.OpenAI.RH

end IntMul.OpenAI.RH

end Bounds

section Maps

open Complex Real

namespace IntMul.OpenAI.RH

/-- nearest integer `[x] = ⌊x + 1/2⌋` -/
noncomputable def rnd (x : ℝ) : ℤ := ⌊x + 1 / 2⌋

section maps
variable {s t : ℕ} [NeZero s] [NeZero t]

variable (s t) in
/-- `β_j = ⟨t j / s⟩` -/
noncomputable def beta (j : ℤ) : ℝ := (t : ℝ) * j / s - rnd ((t : ℝ) * j / s)

end maps

end IntMul.OpenAI.RH

end Maps

section Prop47

open Complex Real

namespace IntMul.OpenAI.RH

end IntMul.OpenAI.RH

end Prop47

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 register file left by the setup -/

/-! ## The setup -/

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

/-! ## Fine-bit exposure -/

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

/-- **Exact per-axis resampling maps** (the `A, B, hA, hB, hid` part of the frozen
`KFM.AxisMaps`, without the Lemma 19 fixed-point fields): `‖A_i‖, ‖B_i‖ ≤ 1` and
`P_S(F_s u / s) = 2^{2α²} B_i(P_T(F_t(A_i u) / t))` on every axis. Under `α ≥ 2`,
`α² (t_i/s_i - 1) ≥ 1` these exist by `prop_4_7_i` (`A = S`, `B` = the inverse map). -/
structure AxisMaps6 {d : ℕ} (α : ℕ) (s t : Fin d → ℕ) [∀ i, NeZero (s i)]
    [∀ i, NeZero (t i)] where
  A : (i : Fin d) → (ZMod (s i) → ℂ) →L[ℂ] (ZMod (t i) → ℂ)
  B : (i : Fin d) → (ZMod (t i) → ℂ) →L[ℂ] (ZMod (s i) → ℂ)
  hA : ∀ i, ‖A i‖ ≤ 1
  hB : ∀ i, ‖B i‖ ≤ 1
  hid : ∀ i u, IntMul.OpenAI.RH.permS (s i) (t i) ((s i : ℂ)⁻¹ • ZMod.dft u) =
    (2 : ℂ) ^ (2 * α ^ 2) • B i (IntMul.OpenAI.RH.permT (s i) (t i) ((t i : ℂ)⁻¹ • ZMod.dft (A i u)))

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

/-- The guard bound the assembly can supply: `Ew D ≤ C D^{C1}`. -/
def EwOK6 (P : Prm) (Ew : ℕ → ℕ) : Prop := ∃ C : ℕ, ∀ D, 1 ≤ D → Ew D ≤ C * D ^ P.C1

/-- **`P14Need6`: the uniform Proposition 14 for round six** (`IL3.P14UH'`, Track D2), produced
from the bit network's canonical Lemma 12 code (`IL.L12Canon`) and a complex network `J` whose
gates lie in the class `IL3H.GClassH J A`, with a guard `Ew = O(D^{C1})` (crude depth guard,
`R6Guard.crude_guard_C1`). Proved by `IL3H.p14Need6_all` (`R6IL3Cfg6`).

Cost row: `ℓ d^λ'` (the `(K+1) D^lamp` factor of `P14NeedH`; margin `ε(1-λ')`). -/
def P14Need6 (P : Prm) : Prop :=
  ∀ (tab : Fin 1 → IStmt HS 1) (l12 : IStmt HS 1), IL.L12Canon tab l12 P.τ →
  ∀ (T : ℕ) (J : Cx.Prop8IfaceH 207387136 T 576 Jain.cxR6) (A : ℕ), IL3H.GClassH J A →
    histMoment Jain.cxR6 576 P.σ < 207387136 →
    2 + 576 * Real.log (histRankSum Jain.cxR6) ≤ P.C1 →
    ∃ Ew : ℕ → ℕ, EwOK6 P Ew ∧ IL3.P14UH' tab Ew P.lamp

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6IL3Cfg6
/-!
# Round six, item language (I3): the configuration of the complex network

**`cfg6_of`**: from a round-six complex network `J : Cx.Prop8IfaceH 207387136 T 576 Jain.cxR6`
in the gate class `GClassH J A`, the moment bound `histMoment cxR6 576 σ < 207387136` and the
depth guard `2 + 576 log(histRankSum cxR6) ≤ C1` (with `P.Ok`), the configuration
`c = cfg6 P J A` (`W = 207387136`, `T`, `m = 576`, `A`, `p = C1`, `net = netF J`) satisfies
`CfgOK c`, `c.p ≤ C1`, and the moment condition `hCc` of `p14UH'_of` at `τ = P.τ`,
`θ = max τ σ ≤ lampOf τ σ ≤ lamp` (some `Cc ≥ 0`).

**`p14Need6_of`** (the shape of the `P14Need6` switch): adding `IL.L12Canon tab l12 P.τ`,
`∃ Ew, IL3.P14UH' tab Ew P.lamp ∧ EwOK6 P Ew` (with `Ew = EwH c`).

## What `GClassH J A` requires (`Solutions/R6IL3Norm.lean`, `def GClassH`)

Every gate step `HStep.gate G ∈ J.net` (`G : Matrix (Fin W ⊕ Fin T) (Fin W ⊕ Fin T) ℂ`) is
either

* **a KFG atom list**: `∃ as : List NLogN.KFG.Atom`, `as.length ≤ A`, every atom `a` has
  `a.Ok (W + T)` and `a.h ≤ 1`, `NLogN.KFG.NoTS as`, and
  `G = (NLogN.KFG.gateMat (W + T) as).submatrix (roleEqv W T) (roleEqv W T)`.
  Here (`Solutions/KFGGate.lean`) an atom `⟨t, s, c, h⟩ : KFG.Atom` is `y_t += (c / 2^h) y_s`;
  `a.Ok W := a.t < W ∧ a.s < W ∧ a.t ≠ a.s ∧ Sm a.c` with `Sm c := |c.re| ≤ 1 ∧ |c.im| ≤ 1`
  (Gaussian integer, `Solutions/KFBGauss.lean`); `NoTS as := ∀ a b ∈ as, a.t ≠ b.s` (no target is
  a source); `gateMat W as p q = [p = q] + Σ_{a : t = p, s = q} c_a / 2^{h_a}`; the role numbering
  `roleEqv W T = finSumFinEquiv` (`Solutions/R6IL3Norm.lean`) puts data roles `0 … W-1` first
  and temporaries `W … W+T-1` after;
* **a `±1` role diagonal**: `∃ U : Finset (Fin W ⊕ Fin T)`,
  `G = Matrix.diagonal fun w => if w ∈ U then -1 else 1`.

The other step kinds (`rowAdd`, `phase`, `perm`, `child`) are unrestricted (children are
normalized by `Prop8IfaceH'.norm`).
-/

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

namespace IntMul.Kappa.R6.IL3H

open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW
  Complex P8Lift Butterfly IntMul.Kappa.R6.Cx IntMul.Kappa.R6.IL IntMul.Kappa.R6.IL3

/-! ## Histogram facts -/

/-! ## The configuration -/

/-- The configuration before the scale constant. -/
noncomputable def cfg0 (P : Prm) {T A : ℕ} (J : Prop8IfaceH 207387136 T 576 Jain.cxR6) : Cfg :=
  ⟨207387136, T, 576, A, 0, P.C1, netF J⟩

/-- **The round-six configuration.** -/
noncomputable def cfg6 (P : Prm) {T : ℕ} (A : ℕ) (J : Prop8IfaceH 207387136 T 576 Jain.cxR6) : Cfg :=
  ⟨207387136, T, 576, A,
    2 * cLH (cfg0 P (A := A) J) + 1 + (netF J).length * dwloc (207387136 + T) A +
      2 * (207387136 + T) * (chWs (cfg0 P (A := A) J)).length + 4, P.C1, netF J⟩

end IntMul.Kappa.R6.IL3H

end