The cost closure (round six, `cost`)
ProvedIntMul.Kappa.R6.IL3H.Hyp14.costThe cost closure.
The following holds (Lean statement, in the scope of module Solutions.R6IL3Top15):
theorem IntMul.Kappa.R6.IL3H.Hyp14.cost (hc : CfgOK c) {Kc Cc θ : ℝ} (hKc : 0 ≤ Kc) (hCc : 0 ≤ Cc) (hθ0 : 0 ≤ θ)
(hθl : θ ≤ lamp) :
(IntMul.Kappa.R6.IL3H.cP14 c Kc Cc θ P K D S r w Z : ℝ) ≤
C0c c Kc Cc * ((P * 2 ^ (K * D) * S * r : ℕ) : ℝ) * ((w : ℝ) + 1) *
((zsz (p : ℤ) : ℝ) + 1) * (D : ℝ) ^ lamp
Context. 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).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs23
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL3H IntMul.Kappa.R6.IL3H.Hyp14
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
variable {c : IntMul.Kappa.R6.IL3H.Cfg} {P K D S r p w Z : ℕ} {lamp : ℝ} (h : Hyp14 c P K D S r p w Z lamp)
include h
theorem IntMul.Kappa.R6.IL3H.Hyp14.cost (hc : CfgOK c) {Kc Cc θ : ℝ} (hKc : 0 ≤ Kc) (hCc : 0 ≤ Cc) (hθ0 : 0 ≤ θ)
(hθl : θ ≤ lamp) :
(IntMul.Kappa.R6.IL3H.cP14 c Kc Cc θ P K D S r w Z : ℝ) ≤
C0c c Kc Cc * ((P * 2 ^ (K * D) * S * r : ℕ) : ℝ) * ((w : ℝ) + 1) *
((zsz (p : ℤ) : ℝ) + 1) * (D : ℝ) ^ lamp := by sorry