ditLoop_runs (The inverse FFT (decimation in time) over `ℤ/(2^n+1)`, as a recursive procedure)

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

theorem NLogN.ditLoop_runs (s : IState NS) (n E : ℕ) (lo hi : List ℤ)
    (RV RX LW LC LE LN LF : List Item) (hn : 1 ≤ n) (hlen : lo.length = hi.length)
    (hE : lo.length * E = n) (hcz : zsz (lo.length : ℤ) ≤ n)
    (hlo : Canon (2 ^ n + 1) lo) (hhi : Canon (2 ^ n + 1) hi)
    (hV : s.G NLogN.V = ints lo ++ RV) (hX : s.G DX = ints hi ++ RX) (hW : s.G W = .int (2 ^ n) :: LW)
    (hC : s.G CC = .int lo.length :: LC) (hDE : s.G NLogN.DE = .int (2 ^ E) :: LE)
    (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) ditStep) s
      (((((((s.upd NLogN.V RV).upd DX RX).upd NLogN.P1
        ((ints (dcomX (2 ^ n + 1) n E 0 lo hi)).reverse ++ s.G NLogN.P1)).upd P2
        ((ints (dcomY (2 ^ n + 1) n E 0 lo hi)).reverse ++ s.G P2)).upd W
          (.int 1 :: LW)).upd CC (.int 0 :: LC)))
      (lo.length * (150000 * (n + 3) + 30) + 30)

Context. The lemma belongs to the part The inverse FFT (decimation in time) over ℤ/(2^n+1), as a recursive procedure.

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.