Part C of a chunk (round six, `partC2_sp`)

Part C of a chunk (2^pk, 2^b at width M + 2).

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

theorem J6Seg.PreT.partC2_sp (s : IState HS) (W : Fin HS → ℤ) (c : Fin HS → List ℤ) {O L : Fin HS}
    (hO : O ∉ rg) (hO5 : O.val < 56) (hL : L ∉ rg) (hL5 : L.val < 56) (hOL : O ≠ L)
    {P lam A M pk b nb sn q : ℕ} {ℓ : ℤ} {lr : List ℤ} (hA : 2 ≤ A) (hW : VB W A)
    (h9 : W 9 = 2 ^ P) (h10 : W 10 = 2 ^ (P + 1)) (h24 : W 24 = lam) (h26 : W 26 = pk)
    (h28 : W 28 = b) (h7 : W 7 = nb) (h8 : W 8 = sn) (h6 : W 6 = q) (hsn : sn ≤ lam)
    (hpkM : pk ≤ M) (hbM : b ≤ M) (hcL : c L = ℓ :: lr) (hℓ : |ℓ| ≤ 2 ^ A) :
    Sp (partC O L) (encK s (J6Seg.PreT.RF W c))
      (encK s (J6Seg.PreT.RF (Function.update (Function.update (Function.update (Function.update W 6
          ((q : ℤ) - 1)) 1 0) 7 0) 8 0)
        (Function.update (Function.update c O
          (((8 + 4 * lam + (4 * nb + 2 * sn) : ℕ) : ℤ) :: ((lam : ℤ) :: 2 ^ P :: 2 ^ (P + 1) ::
            (nb : ℤ) :: ((8 + 4 * lam + (4 * nb + 2 * sn) : ℕ) : ℤ) :: 2 ^ pk :: 2 ^ b ::
            ((2 * (lam - sn) : ℕ) : ℤ) :: c O)))
          L ((ℓ + (1 + ((8 + 4 * lam + (4 * nb + 2 * sn) : ℕ) : ℤ))) :: lr))))
      (cPC2 A M)

Context. B-line IL, pre-tables (B5′, tabK2 layout), part 24: one chunk

chB2 O L = partA2 O; partB O; partC O L. From CS u q it pushes |tab q| :: tab q with tab q = tabK2 P pk b λ di gi gam dd (descsOf … q) onto O and adds 1 + |tab q| on L. Part C is the old program, re-costed with 2^pk, 2^b at width M + 2 (pk, b ≤ M).

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