Lemma 13 for the fixed register-driven code `l13U l12` (round six, `l13U_body`)
ProvedIntMul.Kappa.R6.IL2.l13U_bodyLemma 13 for the fixed register-driven code l13U l12 (Lem13Body with the parameters in
the master registers σMR).
The following holds (Lean statement, in the scope of module Solutions.R6IL2Sw):
theorem IntMul.Kappa.R6.IL2.l13U_body (hτ : 0 ≤ τ) (hL : L12Canon tab l12 τ) :
∃ Kc : ℝ, 0 < Kc ∧
∀ {I : List Sym} (N0 N1 N2 N3 K f ρ R w : ℕ) (px py : Fin 3), px ≠ py → 6 ≤ K → ρ < K →
1 ≤ f → 1 ≤ N0 → 1 ≤ N1 → 1 ≤ N2 → 1 ≤ N3 → 1 ≤ R →
∀ (t : IState HS) (zs : List GI) (R0 : List Item),
Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t →
t.G 0 = ints (gflat zs) ++ R0 → zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R → 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 : ℝ) ≤ Kc * ((zs.length : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ τ + 1) +
(vol (rect N0 N1 N2 N3 (f * K)) : ℝ) * ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) ^ 3 +
min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) *
((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) * ((R : ℝ) * (w + 1) +
(zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 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.l13U_body (hτ : 0 ≤ τ) (hL : L12Canon tab l12 τ) :
∃ Kc : ℝ, 0 < Kc ∧
∀ {I : List Sym} (N0 N1 N2 N3 K f ρ R w : ℕ) (px py : Fin 3), px ≠ py → 6 ≤ K → ρ < K →
1 ≤ f → 1 ≤ N0 → 1 ≤ N1 → 1 ≤ N2 → 1 ≤ N3 → 1 ≤ R →
∀ (t : IState HS) (zs : List GI) (R0 : List Item),
Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t →
t.G 0 = ints (gflat zs) ++ R0 → zs.length = vol (rect N0 N1 N2 N3 (f * K)) * R → 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 : ℝ) ≤ Kc * ((zs.length : ℝ) * (w + 1) * (((f * K : ℕ) : ℝ) ^ τ + 1) +
(vol (rect N0 N1 N2 N3 (f * K)) : ℝ) * ((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) ^ 3 +
min 1 (80 * ((f : ℝ) - 1) * 2⁻¹ ^ K) * (vol (rect N0 N1 N2 N3 (f * K)) : ℝ) *
((zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1) * ((R : ℝ) * (w + 1) +
(zsz (2 * zs.length * (w + 1) : ℤ) : ℝ) + 1)) := by sorry