Pass 5 producer (round six, `scP_sp`)

Pass 5 producer. L = fA q s on 30, |L| on 31, n' ≥ s on iN.

The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc10):

theorem J6Seg.Src.scP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iN : Fin HS} (fN : Free iN)
    (s : ℕ) (q : ℕ → Bool) {n' A : ℕ} {L30 L31 LN : List ℤ}
    (h30 : F 30 = zLs (fA q s) ++ L30) (h31 : F 31 = ((fA q s).length : ℤ) :: L31)
    (hGN : F iN = (n' : ℤ) :: LN) (hsn : s ≤ n') (hnA : n' ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (scP iN) (encK s0 F)
      (encK s0 (update F 44 (srcTab (sSrc (fA q s)) (fun _ => 0) n' ++ F 44)))
      ((s + n' + 2) * (200 * uC A DD))

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*).