The cost of a Proposition 18 call at round six (round six, `cost6`)

The cost of a Proposition 18 call at round six.

The following holds (Lean statement, in the scope of module Solutions.R6P18Cost):

theorem NLogN.KFV.R6P.cost6 (P : Prm) (hP : P.Ok) (C₀ Kc : ℝ) (Cs : ℕ) (hC₀ : 0 ≤ C₀) (hKc : 0 ≤ Kc) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (Ew : ℕ → ℕ) (K₀ n : ℕ), Par6 P Ew K₀ n →
    ∀ (ts : List ℕ) [NeZero ts.length], 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 →
      (total6 C₀ P.lamp Kc Cs (pP6 P n) (ℓP6 P n) (KP6 P n) ts : ℝ) ≤ C * cU6 P n 1

Context. Round six, Proposition 18: the cost

total6: the exact cost of a call of the Proposition 18 entry of ext6 (setup, core with the layout programs, Lemma 16 procedures with the round-six chunk cost cChunk6, teardown). cost6: for every choice of the constants of the Proposition 14 call, the swap and the setup, total6 ≤ C · cU6 P n 1 whenever the side conditions Par6 hold and the input has ∏ t_i · r = T records. The rows: layout d, rounds ℓ + d, chunk calls ℓ d^lamp (zsz p + 1), Kronecker products (ℓ + log₂ p + 1)(ln p + 1), setup and moves O(1) (all per bit, against Ncost6 · (log lg n + 1)).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).