Lemma 13, register-driven (round six, `l13U_runs`)
ProvedIntMul.Kappa.R6.IL2.l13U_runsLemma 13, register-driven: the denotation and the cost pieces (KFL.l13_runs for
l13U).
The following holds (Lean statement, in the scope of module Solutions.R6IL2Sw):
theorem IntMul.Kappa.R6.IL2.l13U_runs {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK tab l12 τ Ksw)
(HC : CorrUOK Kc) (hne : px ≠ py) (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 GI) (R0 : List Item) (h0 : t.G 0 = ints (gflat zs) ++ R0)
(hl : zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R) (hGB : GB w zs) :
∃ c, IRuns I tab (l13U l12) t
(t.upd 0 (ints (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
(rowAddAddr K ρ f px py) R zs)) ++ R0)) c ∧
(c : ℝ) ≤ 2000 * (cTo (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ) +
4 * (26 + Ksw * (((gB N0 N1 N2 N3 K f R w).V : ℝ) + 1) *
((f * K : ℕ) : ℝ) ^ τ) +
(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) +
2000 * (cFrom (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ)
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.l13U_runs {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK tab l12 τ Ksw)
(HC : CorrUOK Kc) (hne : px ≠ py) (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 GI) (R0 : List Item) (h0 : t.G 0 = ints (gflat zs) ++ R0)
(hl : zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R) (hGB : GB w zs) :
∃ c, IRuns I tab (l13U l12) t
(t.upd 0 (ints (gflat (permRecs (rect N0 N1 N2 N3 (f * K))
(rowAddAddr K ρ f px py) R zs)) ++ R0)) c ∧
(c : ℝ) ≤ 2000 * (cTo (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ) +
4 * (26 + Ksw * (((gB N0 N1 N2 N3 K f R w).V : ℝ) + 1) *
((f * K : ℕ) : ℝ) ^ τ) +
(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) +
2000 * (cFrom (2 * (vol (rect N0 N1 N2 N3 (f * K)) * R)) w : ℝ) := by sorry