Round-six lemma `coreBU_runs`
ProvedIntMul.Kappa.R6.IL2.coreBU_runsAn 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.coreBU_runs {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK tab l12 τ Ksw)
(HC : CorrUOK Kc) (hK6 : 6 ≤ K) (hp : PPos N0 N1 N2 N3 K f ρ R)
(I : List Sym) (t : IState HS) (hA : Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t)
(zs : List ℤ) (R0 : List Item) (hb : KFL.Bits zs) (h0 : t.G 0 = ints zs ++ R0)
(hlen : zs.length = (gB N0 N1 N2 N3 K f R w).V) :
∃ c : ℕ, IRuns I tab (coreBU l12) t
(t.upd 0 (ints (rixT (gB N0 N1 N2 N3 K f R w) (RAc K ρ f) zs) ++ R0)) c ∧
(c : ℝ) ≤ 400 * coreCost τ Ksw Kc K ρ f (gB N0 N1 N2 N3 K f R w) +
10 ^ 10 * (((zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3 : ℕ) : ℝ) + 2) ^ 2
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} {τ : ℝ}
variable {N0 N1 N2 N3 K f ρ R w : ℕ} {px py : Fin 3} {t : IState HS}
theorem IntMul.Kappa.R6.IL2.coreBU_runs {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK tab l12 τ Ksw)
(HC : CorrUOK Kc) (hK6 : 6 ≤ K) (hp : PPos N0 N1 N2 N3 K f ρ R)
(I : List Sym) (t : IState HS) (hA : Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t)
(zs : List ℤ) (R0 : List Item) (hb : KFL.Bits zs) (h0 : t.G 0 = ints zs ++ R0)
(hlen : zs.length = (gB N0 N1 N2 N3 K f R w).V) :
∃ c : ℕ, IRuns I tab (coreBU l12) t
(t.upd 0 (ints (rixT (gB N0 N1 N2 N3 K f R w) (RAc K ρ f) zs) ++ R0)) c ∧
(c : ℝ) ≤ 400 * coreCost τ Ksw Kc K ρ f (gB N0 N1 N2 N3 K f R w) +
10 ^ 10 * (((zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3 : ℕ) : ℝ) + 2) ^ 2 := by sorry