Round-six lemma `coreCost_le`
ProvedIntMul.Kappa.R6.IL2.coreCost_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.R6IL2Sw):
theorem IntMul.Kappa.R6.IL2.coreCost_le {K ρ f : ℕ} (hK : 6 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) (g : Geo) (hg : g.Pos)
(hQe : g.Q = 2 ^ (f * K)) (Ks Kcr : ℝ) :
coreCost τ Ks Kcr K ρ f g ≤ 1 + 16 * Ks * ((g.V : ℝ) + 1) * ((f * K : ℕ) : ℝ) ^ τ +
2 * 10 ^ 15 * ((g.recG.V : ℝ) * ((zsz (g.V : ℤ) : ℝ) + 1) ^ 3 + g.V) +
Kcr * ((g.recG.V : ℝ) * ((zsz (g.V : ℤ) : ℝ) + 1) ^ 3 + (g.V : ℝ) +
min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (g.recG.V : ℝ) *
((zsz (g.V : ℤ) : ℝ) + 1) * ((g.B : ℝ) + (zsz (g.V : ℤ) : ℝ) + 1))
Context. Round six, item language (I2): the register-driven Lemma 13 core over any Lemma 12 table
Parametric copy of KFX.swE/swE_spec/swE_geo (KFX1Sw), KFL.coreCost/coreCost_le
(KFLMain) and the tail of KFX4Core (optA … l13U_body) with the OpenAI Lemma 12
(KFL.l12prog, KFL.l12C q, τ = 1 - 2^-50) replaced by any table tab, code l12 and
exponent τ satisfying IL.L12Canon tab l12 τ (0 ≤ τ ≤ 1).
l13U_body: L12Canon tab l12 τ → ∃ Kc > 0, (Lemma 13 for the code l13U l12).
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.IL2
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH NLogN.KFX AModel AModelL12 NetProp7 Butterfly IntMul.Kappa.R6.IL
variable {tab : Fin 1 → IStmt HS 1} {l12 : IStmt HS 1} {τ : ℝ}
theorem IntMul.Kappa.R6.IL2.coreCost_le {K ρ f : ℕ} (hK : 6 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) (g : Geo) (hg : g.Pos)
(hQe : g.Q = 2 ^ (f * K)) (Ks Kcr : ℝ) :
coreCost τ Ks Kcr K ρ f g ≤ 1 + 16 * Ks * ((g.V : ℝ) + 1) * ((f * K : ℕ) : ℝ) ^ τ +
2 * 10 ^ 15 * ((g.recG.V : ℝ) * ((zsz (g.V : ℤ) : ℝ) + 1) ^ 3 + g.V) +
Kcr * ((g.recG.V : ℝ) * ((zsz (g.V : ℤ) : ℝ) + 1) ^ 3 + (g.V : ℝ) +
min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (g.recG.V : ℝ) *
((zsz (g.V : ℤ) : ℝ) + 1) * ((g.B : ℝ) + (zsz (g.V : ℤ) : ℝ) + 1)) := by sorry