Round-six lemma `zextP_spec`
ProvedJ6Seg.JK.zextP_specAn 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.J6SegILJKer10):
theorem J6Seg.JK.zextP_spec {zl lm lk : List ℤ} {K B : ℕ} (hZ : G Z = zl) (hTMP : G TMP = [])
(hTM2 : G TM2 = []) (hER : G ER = []) (hE : G E = []) (hCM : G CM = [])
(hm : G HM = (zl.length : ℤ) :: lm)
(hk : G HK = (K : ℤ) :: lk) (hKm : K ≤ zl.length) (hB : Bnd B zl)
(hcB : zsz ((zl.length + 2 * K : ℕ) : ℤ) ≤ B) :
Sp zextP (encK s G) (encK s (update G E (zext K zl)))
((zl.length + K + 2) * (2 * 10 ^ 5 * (B + 2)))
Context. B-line IL, the J kernel (B4), part 10: the cyclic extension
zextP builds E = zext K zl = zl.drop (m - K) ++ zl ++ zl.take K from Z = zl (m = |zl|
on HM, K ≤ m on HK), leaving Z as it was: the reversed extension is assembled on ER by
three copies (dupMv) and moved onto E (zextP_spec). Linear cost.
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_Defs66
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL Function Finset
variable {s : IState HS} {G : Fin HS → List ℤ}
theorem J6Seg.JK.zextP_spec {zl lm lk : List ℤ} {K B : ℕ} (hZ : G Z = zl) (hTMP : G TMP = [])
(hTM2 : G TM2 = []) (hER : G ER = []) (hE : G E = []) (hCM : G CM = [])
(hm : G HM = (zl.length : ℤ) :: lm)
(hk : G HK = (K : ℤ) :: lk) (hKm : K ≤ zl.length) (hB : Bnd B zl)
(hcB : zsz ((zl.length + 2 * K : ℕ) : ℤ) ≤ B) :
Sp zextP (encK s G) (encK s (update G E (zext K zl)))
((zl.length + K + 2) * (2 * 10 ^ 5 * (B + 2))) := by sorry