postLoop_runs (`FM`: untwisting, lifting and carrying)

The following holds (Lean statement, in the scope of module NLogN.SSFM3):

theorem NLogN.postLoop_runs (s : IState NS) (n M Q k K : ℕ) (D : List ℤ)
    (RX LW L2 LH LY LM LQ LC LN LF : List Item)
    (hn : 1 ≤ n) (hM1 : 1 ≤ M) (hM : M ≤ n) (hKQ : K * Q = n) (hk : k ≤ n)
    (hK : zsz (K : ℤ) ≤ n) (hDl : D.length = K) (hD : Canon (2 ^ n + 1) D)
    (hX : s.G DX = ints D ++ RX) (hW : s.G W = .int (2 ^ n) :: LW)
    (h2 : s.G W2 = .int (2 ^ (n - k)) :: L2) (hH : s.G HB = .int (2 ^ (n - 1)) :: LH)
    (hY : s.G CYS = .int 0 :: LY) (hRM : s.G RMs = .int (2 ^ M) :: LM)
    (hRQ : s.G RQ = .int (2 ^ Q) :: LQ) (hC : s.G CC = .int K :: LC)
    (hN : s.G RN = .int (2 ^ n) :: LN) (hF : s.G RF = .int (2 ^ n + 1) :: LF) :
    IRuns I iprog (.loop CC (fun c => c != .zero) postStep) s
      (((((s.upd DX RX).upd NLogN.DG ((ints (carZ M (NLogN.liftL n k Q K D) 0).1).reverse ++ s.G NLogN.DG)).upd CYS
        (.int (carZ M (NLogN.liftL n k Q K D) 0).2 :: LY)).upd W (.int 1 :: LW)).upd CC (.int 0 :: LC))
      (K * (60000 * (n + 3) + 30) + 30)

Context. The lemma belongs to the part FM: untwisting, lifting and carrying.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.