Lemma 13 for the fixed register-driven code `l13U q` (round six, `l13U_body`)
ProvedNLogN.KFX.l13U_bodyLemma 13 for the fixed register-driven code l13U q (Lem13Body with the parameters in
the master registers σMR).
The following holds (Lean statement, in the scope of module Solutions.KFX4Core):
theorem NLogN.KFX.l13U_body :
∃ (q : ℕ) (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 l12prog (l13U q) 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 - (2 : ℝ)⁻¹ ^ 50) + 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. 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
theorem NLogN.KFX.l13U_body :
∃ (q : ℕ) (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 l12prog (l13U q) 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 - (2 : ℝ)⁻¹ ^ 50) + 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