Round-six lemma `cTot_le`
ProvedNLogN.KFUU.R6Fine.cTot_leAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.R6FineNeed):
theorem NLogN.KFUU.R6Fine.cTot_le (w f V : ℕ) :
cTot w f V ≤ C0fine * ((w + 1) * (V + 1) * (f + 1) + (Nat.size V + w + f + 4) ^ 2)
Context. Fine-bit exposure §3: FineNeed6
fineU E idx i is fineE coreF (i = 0) or fineE coreB (i = 1); the descriptor stack is
dP. fineRun_F / fineRun_B: on the managed state of a FineBody6 call they compute
gflat (blkT (2^f) y a zs) / gflat (blkT y (2^f) a zs) at cost ≤ C0fine · cFine w f a y
(C0fine = 30000 + 1100 CU). fineNeed6_all : ∀ P, P.Ok → FineNeed6 P (the table tab,
SwapNeedτ and RowUCP are not used: no calls).
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_Defs70 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open NLogN NLogN.KFUU NLogN.KFUU.R6Fine set_option maxRecDepth 20000 open IntMul NLogN.KIL NLogN.KFB NLogN.KFC NLogN.KFT NLogN.KFU AModel AModelL12 NLogN.KFUU IntMul.Kappa.R6
theorem NLogN.KFUU.R6Fine.cTot_le (w f V : ℕ) :
cTot w f V ≤ C0fine * ((w + 1) * (V + 1) * (f + 1) + (Nat.size V + w + f + 4) ^ 2) := by sorry