Round-six lemma `coreBU_runs`
ProvedNLogN.KFX.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.KFX4Core):
theorem NLogN.KFX.coreBU_runs {q : ℕ} {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK q 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 l12prog (coreBU q) 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. KFX §4: the register-driven Lemma 13 core
The fixed code l13U q is KFL.l13code with every size-dependent literal read from the
master registers (MReg): w, 2·M·R on 1, 6 (for toBitsU/fromBitsU), the swap flags on
11, 12, and Q = 2^{fK}, B = R·2(w+1), 2^ρ, gx, N0, N1, N2, N3, A = zsz V, 2^K on
13, 15, 16, 17, 18, 19, 46, 47, 48, 49, f, K on 36, 37. The slot swaps preL px py are
realized by two optional swaps (optA: swap 0 or 2 by the flag on 11, optB: swap 1 by
the flag on 12). l13U_runs is KFL.l13_runs for this code.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open NLogN NLogN.KFX
open IntMul NLogN.RS NLogN.KIL NLogN.KFD NLogN.KFE NLogN.KFB NLogN.KFL NLogN.KFW NLogN.KFH AModel Butterfly
variable {N0 N1 N2 N3 K f ρ R w : ℕ} {px py : Fin 3} {t : IState HS}
theorem NLogN.KFX.coreBU_runs {q : ℕ} {Ksw Kc : ℝ} (hKsw : 0 ≤ Ksw) (hKc : 0 ≤ Kc) (HSw : SwEOK q 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 l12prog (coreBU q) 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