The natural-number part of the cost bound (`cost_nat`)
ProvedIntMul.Kappa.R6.IL3H.Hyp14.cost_natThe natural-number part of the cost bound.
The following holds (Lean statement, in the scope of module Solutions.R6IL3Top15):
theorem IntMul.Kappa.R6.IL3H.Hyp14.cost_nat (hc : CfgOK c) (CB : ℕ → ℝ) :
8 * (2 * moveCost Z + 19) + (cChainH c CB (cWc c) P K D S r w Z (3 * Z) (3 * Z) +
8 * (2 * moveCost Z + 19)) + 2 ≤
((chV c (cWc c) P K D S r w).q0 + (chV c (cWc c) P K D S r w).qB) *
⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r (3 * Z) (chV c (cWc c) P K D S r w).H : ℕ) : ℝ)⌋₊ +
401 * ⌊CB (D - (chV c (cWc c) P K D S r w).q0 - (chV c (cWc c) P K D S r w).qB) *
(((chV c (cWc c) P K D S r w).Bp * 2 ^ (K * (D - (chV c (cWc c) P K D S r w).q0)) * S *
Yu r (3 * Z) (chV c (cWc c) P K D S r w).H : ℕ) : ℝ)⌋₊ +
10 ^ 17 * (((Sc c + 1) * (2 * c.Wr + 14)) *
((P * 2 ^ (K * D) * S) * (r * (w + 1)) * (zsz (p : ℤ) + 1)))
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_nat (hc : CfgOK c) (CB : ℕ → ℝ) :
8 * (2 * moveCost Z + 19) + (cChainH c CB (cWc c) P K D S r w Z (3 * Z) (3 * Z) +
8 * (2 * moveCost Z + 19)) + 2 ≤
((chV c (cWc c) P K D S r w).q0 + (chV c (cWc c) P K D S r w).qB) *
⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r (3 * Z) (chV c (cWc c) P K D S r w).H : ℕ) : ℝ)⌋₊ +
401 * ⌊CB (D - (chV c (cWc c) P K D S r w).q0 - (chV c (cWc c) P K D S r w).qB) *
(((chV c (cWc c) P K D S r w).Bp * 2 ^ (K * (D - (chV c (cWc c) P K D S r w).q0)) * S *
Yu r (3 * Z) (chV c (cWc c) P K D S r w).H : ℕ) : ℝ)⌋₊ +
10 ^ 17 * (((Sc c + 1) * (2 * c.Wr + 14)) *
((P * 2 ^ (K * D) * S) * (r * (w + 1)) * (zsz (p : ℤ) + 1))) := by sorry