Round-six lemma `sel_step`

An 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.J6SegILSrc6):

theorem J6Seg.Src.sel_step (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iK : Fin HS} (fS : Free iS)
    (fT : Free iT) (fK : Free iK) {s t A : ℕ} {K : ℤ} {LS LT LK : List ℤ}
    (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGK : G iK = K :: LK)
    (hs : 0 < s) (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A) (hKA : |K| ≤ 2 ^ A) (hA : 2 ≤ A)
    {n' j : ℕ} (hj : j < n') (hjA : j + 1 ≤ 2 ^ A) :
    Sp (selB iS iT iK)
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6Seg.selSrc s t) (fun _ => K) n' (j + 1) ++ G 44)))
      (encK s0 (tbS G [(j : ℤ) + 1] (tlT (J6Seg.selSrc s t) (fun _ => K) n' j ++ G 44)))
      (30 * uC A DD)

Context. B-line IL, source-table producers, part 6: the table loop, pass 1, the counts

Table loop (tab_loop): rep 43 (reg iN) b with n' on iN, the body at step k (index j = n' - 1 - k, i.e. 43 holds j + 1) pushing argOf j then J6Seg.Slab.code (src j) on 44; the loop leaves srcTab src argOf n' ++ G 44 on 44 (the table is produced last entry first). enc_base, enc_base44: rebasing the empty-43 precondition away.

Pass 1 (selP iS iT iK iN): src = selSrc s t, argOf = fun _ => K (the caller passes K = 2^(P'-p-1) on iK), n' on iN. Inputs: s on iS, t on iT, K on iK, n' on iN (all Free); 0 < s, s, t, n' ≤ 2^A, |K| ≤ 2^A, 2 ≤ A. Output: 44 := srcTab (selSrc s t) (fun _ => K) n' ++ F 44, everything else unchanged (43 is the loop counter, restored). Theorem selP_sp, cost (n' + 1) * (30 * uC A DD).

Counts (cntP iPre iPost iN): pushes pre on 37 (rNB), 2 post on 39 (rM), pre * (n' * (2 post)) on 40 (rTOT). Inputs pre on iPre, post on iPost, n' on iN (registers < 56, distinct from 37, 39, 40), all ≤ 2^A. Theorem cntP_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*).