Round-six lemma `kFinA_le6`
ProvedIntMul.Kappa.R6.kFinA_le6An 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.R6MCost):
theorem IntMul.Kappa.R6.kFinA_le6 : kFinA6 Q D ≤ 10 ^ 9 * (Q.T * (Q.p + 1 + KFM.fmB (8 * Q.p)) + Q.p + 1)
Context. Round-six machine: the cost of bigE in the unit ZU6
The frozen KFMCost at the round-six parameters. ZU6 Q = T (p + 1 + fmB (8p)) + (b + 1)^6 + n.
Every cost of bigE other than the interface calls is O(ZU6 Q), and the descriptor parts of a
call are O((b+1)^2).
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_Defs16
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6
open Finset IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFT NLogN.KFU NLogN.RS IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFM
variable {Q : Q6} (hQ : QOk Q) {D : ℕ} (hD : Q.d = D + 1)
include hQ hD
theorem IntMul.Kappa.R6.kFinA_le6 : kFinA6 Q D ≤ 10 ^ 9 * (Q.T * (Q.p + 1 + KFM.fmB (8 * Q.p)) + Q.p + 1) := by sorry