Round-six lemma `s5_step`
ProvedJ6Seg.Src.s5_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.J6SegILSrc10):
theorem J6Seg.Src.s5_step (s0 : IState HS) (G : Fin HS → List ℤ) (B30 : List ℤ) {s : ℕ} {q : ℕ → Bool}
{n' A : ℕ} (hsA : s ≤ 2 ^ A) (hA : 2 ≤ A) {u : ℕ} (hu : u < n') (huA : u + 1 ≤ 2 ^ A) :
Sp s5B (encK s0 (update (s5S G B30 s q n' (u + 1)) 43 [(u : ℤ) + 1]))
(encK s0 (update (s5S G B30 s q n' u) 43 [(u : ℤ) + 1])) (c5 A)
Context. B-line IL, source-table producers, part 10: pass 5 (scSrc, the scatter)
For L = (range s).filter q (= LJ = Jlist (mkBlocks …)) on 30 and |L| on 31, n' (≥ s)
on iN: scP iN moves L reversed onto 15, pushes the count c = |L| on 13, and for
u = n' - 1, …, 0 pushes 0 and code (scSrc u) on 44 (scSrc u = some (idxOf u) if u ∈ L):
u ∈ L iff c > 0 and the top of 15 (the largest remaining entry, always ≤ u) equals u,
in which case the code is c - 1, the entry moves back to 30 and c decreases. Output:
44 := srcTab (sSrc L) (fun _ => 0) n' ++ F 44, everything else unchanged. Theorem scP_sp.
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.s5_step (s0 : IState HS) (G : Fin HS → List ℤ) (B30 : List ℤ) {s : ℕ} {q : ℕ → Bool}
{n' A : ℕ} (hsA : s ≤ 2 ^ A) (hA : 2 ≤ A) {u : ℕ} (hu : u < n') (huA : u + 1 ≤ 2 ^ A) :
Sp s5B (encK s0 (update (s5S G B30 s q n' (u + 1)) 43 [(u : ℤ) + 1]))
(encK s0 (update (s5S G B30 s q n' u) 43 [(u : ℤ) + 1])) (c5 A) := by sorry