Round-six κ development, definitions part 17

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

import Definitions.Def_IntMul_Kappa_R6_Defs16
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_Kappa_R6_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs25
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_R6_Defs1

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6ZParam
/-!
# Round six, chirp: the chirp procedure parameters of a size `Q`

The frozen `KFZParam` facts for a round-six size `Q` with `QOk Q` and `Q.d = D + 1`:
`h = ℓ - 1`, `σ = d - d'`, the bits `bs6`, the sources `ss6`, `t_i = 2^{h + bit i}`,
`(D+1) h + σ = L`, the chirp descriptor `descChirp6`, the chirp-table descriptor
`descT (sB D) (tB D)`, the register width `BN6 ≤ 5p` with `RB`, and the Prop 18 descriptor side
conditions `MG`.
-/

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

namespace IntMul.Kappa.R6

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

noncomputable section

/-- The bit of axis `j`. -/
def bit6 (Q : Q6) (j : ℕ) : ℕ := if Q.dp ≤ j then 1 else 0

/-- The bit list. -/
def bs6 (Q : Q6) : List ℕ := (List.range Q.d).map (bit6 Q)

/-- The source list. -/
def ss6 (Q : Q6) : List ℕ := (List.range Q.d).map Q.src

/-- `σ = d - d'`. -/
def σ6 (Q : Q6) : ℕ := Q.d - Q.dp

/-- The register width. -/
def BN6 (Q : Q6) : ℕ := dlV Q.p Q.h Q.d + (Q.d * Q.h + σ6 Q) + 8 + Q.K + Q.α + 1

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6ZMain
/-!
# Round six, chirp: `P18Body6 → chirpG6`

The frozen `KFZMain.chirpNeedR_of_P18` at the round-six sizes: the chirp procedure `body`
(`KFZFull`) is the own procedure of the merged table `mExt4 ext₁₈ ∅ ∅ ∅ [body]` in `kTableP tab`;
the Prop 18 procedure (from `P18Body6`) is reached through `g4₁`. The descriptor stack is
`cS = 36`. Per call `M̃r = mrtCall t F G H` with `H` the Prop 18 result, within `errW6 · 2^{-p}`.

* **`chirp_of_P18`**: one table, entry, constants for all sizes `Q` of the parameters `P` with
  `QOk Q`: the grid tables `θ̃, θ̃⁻, ã, b̃` with their `Phases` facts and `chirpG6`.
-/

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

namespace IntMul.Kappa.R6

open IntMul NLogN NLogN.KIL KFB NLogN.KFM IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFZ
  IntMul.OpenAI.RC IntMul.OpenAI.RT

noncomputable section

/-- The merged extension list of the chirp table: Prop 18, three empty slots, the chirp body. -/
def extZ6 {E18 : ℕ} (ext18 : Fin E18 → IStmt HS (7 + E18)) (entry18 : Fin (7 + E18))
    (d18 : Fin HS) : Fin (E18 + 0 + 0 + 0 + 1) → IStmt HS (7 + (E18 + 0 + 0 + 0 + 1)) :=
  mExt4 ext18 (Fin.elim0 : Fin 0 → IStmt HS (7 + 0)) (Fin.elim0 : Fin 0 → IStmt HS (7 + 0))
    (Fin.elim0 : Fin 0 → IStmt HS (7 + 0))
    (fun _ => body (g4₁ E18 0 0 0 1 entry18) d18)

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MCtx
/-!
# Round-six machine: the merged table, the contexts and `BigSpec`

The frozen `KFMBig11` at the round-six parameters.

* `ixM6`: the index data of the merged table `mExt4 ext₁ ext₂ ext₃ ext₄ [bigP6]` (setup, `Φ`,
  lines, chirp; chirp descriptor stack `cS`).
* **`ctx_exists6`**: from the per-size guarantees of `Φ` (`CrtBody6`), the lines (`LineBody6`)
  and the chirp (`chirp_of_P18`), a `BigCtx6` exists for every admissible size and every `Isym`,
  with the fixed constants and the canonical descriptor bounds `dzB`.
* **`bigSpec_of6`**: contexts and setup runs for all `n ≥ N₁` give `BigSpec`.
-/

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

/-- The index data of the merged table (own procedure `0` is `bigP6`). -/
def ixM6 (E₁ E₂ E₃ E₄ : ℕ) (eS : Fin (7 + E₁)) (eF eI : Fin (7 + E₂)) (eA eB : Fin (7 + E₃))
    (eC : Fin (7 + E₄)) (dSΦ dSL : Fin HS) : Ix6 (7 + (E₁ + E₂ + E₃ + E₄ + 1)) where
  P₁ := E₁
  P₂ := E₂
  P₃ := E₃
  P₄ := E₄
  g₁ := g4₁ E₁ E₂ E₃ E₄ 1
  g₂ := g4₂ E₁ E₂ E₃ E₄ 1
  g₃ := g4₃ E₁ E₂ E₃ E₄ 1
  g₄ := g4₄ E₁ E₂ E₃ E₄ 1
  eS := eS
  eF := eF
  eI := eI
  eA := eA
  eB := eB
  eC := eC
  dSΦ := dSΦ
  dSL := dSL
  dSC := NLogN.KFZ.cS

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MCost
/-!
# Round-six machine: the cost of `bigE` in the unit `ZU6`

The frozen `KFMCost` at the round-six parameters. `ZU6 Q = T (p + 1 + fmB (8p)) + (b + 1)^6 + n`.
Every cost of `bigE` other than the interface calls is `O(ZU6 Q)`, and the descriptor parts of a
call are `O((b+1)^2)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open Finset IntMul NLogN NLogN.KIL KFB KFT KFU RS IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM

noncomputable section

/-- The unit. -/
def ZU6 (Q : Q6) : ℕ := Q.T * (Q.p + 1 + KFM.fmB (8 * Q.p)) + (Q.b + 1) ^ 6 + Q.n

/-! ## Descriptors -/

end

end IntMul.Kappa.R6

end

section
-- Source module: Solutions.R6MTotal
/-!
# Round-six machine: the total cost of one context

* `cU6_mono`, `ZU6_le`: the unit `ZU6` is within `Kz6 · cU6 A` (`A ≥ 2`).
* **`total_le6`**: the setup (within `C_S · cU6 A_S`) plus `kMul6 + kFin6 + 2` of a context is at
  most `Ctot6 · cU6 A'` with `A' = A_Φ + A_L + A_C + A_S + 2`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace IntMul.Kappa.R6

open Finset IntMul NLogN NLogN.KIL KFB KFT KFU RS IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM

noncomputable section

/-- The constant of the unit. -/
def Kz6 (P : Prm) : ℝ := (32500 * (NLogN.KFZ.Cfm : ℝ) + 200) * ((P.x : ℝ) + 4) ^ 2

/-- The constant of the total. -/
def Ctot6 (P : Prm) (CΦ CL CC CS : ℝ) : ℝ := 10 ^ 11 * Kz6 P + 3 * CΦ + 6 * CL + 3 * CC + CS + 2

end

end IntMul.Kappa.R6

end