The cost of the general procedure against the structural cost (round six, `costN_real`)
ProvedIntMul.Kappa.R6.IL.costN_realThe cost of the general procedure against the structural cost.
The following holds (Lean statement, in the scope of module Solutions.R6ILCostR):
theorem IntMul.Kappa.R6.IL.costN_real (C : Bit.QHNet (ZMod 2) W T m) (q Bb : ℕ) (hm : 2 ≤ m) (hruns : C.RunsOK) :
∀ e, 1 ≤ e → ∀ V : ℕ, (costN C q Bb e V : ℝ) ≤
(2 * cq q + Kv C : ℝ) * ((V : ℝ) * Bit.cH C e) + (KA C q : ℝ) * ovN C e * ((Bb : ℝ) + 2) ^ 2
Context. Round six, item language: the cost of the general procedure against costH
costN_real: costN e V ≤ (2 cq + Kv) · V · cH e + KA · ovN e · (Bb + 2)² for e ≥ 1, where
ovN counts (e + 1) per node of the call tree; ovN_le: ovN e ≤ (e + 1) (S + 1) ^ depH e.
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_Defs13
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE AModel AModelL12 Finset
variable {W T m : ℕ} [NeZero W]
theorem IntMul.Kappa.R6.IL.costN_real (C : Bit.QHNet (ZMod 2) W T m) (q Bb : ℕ) (hm : 2 ≤ m) (hruns : C.RunsOK) :
∀ e, 1 ≤ e → ∀ V : ℕ, (costN C q Bb e V : ℝ) ≤
(2 * cq q + Kv C : ℝ) * ((V : ℝ) * Bit.cH C e) + (KA C q : ℝ) * ovN C e * ((Bb : ℝ) + 2) ^ 2 := by sorry