Round-six lemma `g3_step`
ProvedJ6Seg.Src.g3_stepAn 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.J6SegILSrc9):
theorem J6Seg.Src.g3_step (s0 : IState HS) (G : Fin HS → List ℤ) (B30 : List ℤ) (L : List ℕ) {n' A : ℕ}
{L31 : List ℤ}
(h31 : G 31 = (L.length : ℤ) :: L31) (hLA : ∀ x ∈ L, x ≤ 2 ^ A) (hlA : L.length ≤ 2 ^ A)
(hA : 2 ≤ A) {j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
Sp g3B (encK s0 (update (g3S G B30 L n' (j + 1)) 43 [(j : ℤ) + 1]))
(encK s0 (update (g3S G B30 L n' j) 43 [(j : ℤ) + 1])) (2 * (10 * uC A DD) + 200 * (A * DD + 1 + 1))
Context. B-line IL, source-table producers, part 9: pass 3 (jSrc, the gather)
gthP iN: with a list L (= LJ) on 30 (head = index 0) and |L| on 31 (as left by ljP),
and n' (= G ≥ |L|) on iN (Free): move L reversed onto 15 (mvK 30 15 43 (reg 31)),
then for j = n' - 1, …, 0 push 0 and code (src j) on 44, with
src j = if j < |L| then some L[j] else none (jSrc for L = LJ), moving L[j] back from 15
to 30. Output: 44 := srcTab src (fun _ => 0) n' ++ F 44, everything else (in particular
15, 30, 31) unchanged. Theorem gthP_sp, cost (|L| + n' + 2) * (40 * uC A DD).
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_Defs65 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src set_option maxRecDepth 20000 open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg open J6Seg.Slab (srcTab)
theorem J6Seg.Src.g3_step (s0 : IState HS) (G : Fin HS → List ℤ) (B30 : List ℤ) (L : List ℕ) {n' A : ℕ}
{L31 : List ℤ}
(h31 : G 31 = (L.length : ℤ) :: L31) (hLA : ∀ x ∈ L, x ≤ 2 ^ A) (hlA : L.length ≤ 2 ^ A)
(hA : 2 ≤ A) {j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
Sp g3B (encK s0 (update (g3S G B30 L n' (j + 1)) 43 [(j : ℤ) + 1]))
(encK s0 (update (g3S G B30 L n' j) 43 [(j : ℤ) + 1])) (2 * (10 * uC A DD) + 200 * (A * DD + 1 + 1)) := by sorry