The level cost bound (round six, `cLevBody_le`)
ProvedIntMul.Kappa.R6.IL.cLevBody_leThe level cost bound.
The following holds (Lean statement, in the scope of module Solutions.R6ILLevCost):
theorem IntMul.Kappa.R6.IL.cLevBody_le [NeZero W] (C : Bit.QHNet (ZMod 2) W T m) (P L' h v Bb : ℕ)
(cC : ℕ × ℕ × ℕ → ℕ) (hP : 1 ≤ P) (hL : 1 ≤ L') (hh : 1 ≤ h) (hv : P * L' * h = v) :
cLevBody C P L' h v Bb cC ≤ levB C v Bb + ((runsL C).map cC).sum
Context. Round six, item language: the cost of one level body
cLevBody_le: the cost of levBody C on streams of volume v is at most
levB C v Bb = KL C · (10^14 ((T + W) v + 1) + 10^11 (Bb + 2)²) plus the costs of the child
calls of all runs of all edges (runsL C).
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 AModel AModelL12 Finset
variable {W T m : ℕ}
theorem IntMul.Kappa.R6.IL.cLevBody_le [NeZero W] (C : Bit.QHNet (ZMod 2) W T m) (P L' h v Bb : ℕ)
(cC : ℕ × ℕ × ℕ → ℕ) (hP : 1 ≤ P) (hL : 1 ≤ L') (hh : 1 ≤ h) (hv : P * L' * h = v) :
cLevBody C P L' h v Bb cC ≤ levB C v Bb + ((runsL C).map cC).sum := by sorry