The lines, register-driven (round six, `linesU_runs`)
ProvedIntMul.Kappa.R6.IL2.linesU_runsThe lines, register-driven.
The following holds (Lean statement, in the scope of module Solutions.R6IL2Sw):
theorem IntMul.Kappa.R6.IL2.linesU_runs {Ksw : ℝ} (hKsw : 0 ≤ Ksw) (HSw : SwEOK tab l12 τ Ksw)
(hp : PPos N0 N1 N2 N3 K f ρ R) (I : List Sym) :
∀ (ls : List Line), (∀ l ∈ ls, LineOK l) →
∀ (t : IState HS) (zs : List ℤ) (R0 : List Item),
Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t →
KFL.Bits zs → t.G 0 = ints zs ++ R0 → zs.length = (gB N0 N1 N2 N3 K f R w).V →
∃ c : ℕ, IRuns I tab (linesU l12 ls) t
(t.upd 0 (ints (rixT (gB N0 N1 N2 N3 K f R w)
(fun c => ls.foldr (fun l c => lineP K ρ f l c) c) zs) ++ R0)) c ∧
(c : ℝ) ≤ 1 + ls.length * (2 * Ksw * (((gB N0 N1 N2 N3 K f R w).V : ℝ) + 1) *
((f * K : ℕ) : ℝ) ^ τ +
400 * cRotG K f (gB N0 N1 N2 N3 K f R w) (zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3))
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.linesU_runs {Ksw : ℝ} (hKsw : 0 ≤ Ksw) (HSw : SwEOK tab l12 τ Ksw)
(hp : PPos N0 N1 N2 N3 K f ρ R) (I : List Sym) :
∀ (ls : List Line), (∀ l ∈ ls, LineOK l) →
∀ (t : IState HS) (zs : List ℤ) (R0 : List Item),
Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t →
KFL.Bits zs → t.G 0 = ints zs ++ R0 → zs.length = (gB N0 N1 N2 N3 K f R w).V →
∃ c : ℕ, IRuns I tab (linesU l12 ls) t
(t.upd 0 (ints (rixT (gB N0 N1 N2 N3 K f R w)
(fun c => ls.foldr (fun l c => lineP K ρ f l c) c) zs) ++ R0)) c ∧
(c : ℝ) ≤ 1 + ls.length * (2 * Ksw * (((gB N0 N1 N2 N3 K f R w).V : ℝ) + 1) *
((f * K : ℕ) : ℝ) ^ τ +
400 * cRotG K f (gB N0 N1 N2 N3 K f R w) (zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3)) := by sorry