pieces_run (KIL6: all piece calls)

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

theorem NLogN.KIL.pieces_run {I : List Sym} {iprog : Fin 1 → IStmt HS 1} (s : IState HS)
    (F : Fin HS → List ℤ) (v : Fin HS → ℕ) {M B : ℕ} (hM : zsz (M : ℤ) ≤ B)
    {q m n P R' : ℕ} (G' Suf : Shape) (child : Oracle (ZMod 2)) (cO : ℕ → ℕ) (ys : List (ZMod 2))
    (hq : 2 ≤ q) (hm : 2 ≤ m) (hG' : ∀ a ∈ G', 1 ≤ a) (hS : ∀ a ∈ Suf, 1 ≤ a) (hP : 1 ≤ P)
    (hR' : 1 ≤ R') (hO : ∀ j, m ^ j ≤ n → CallSpec I iprog child q m j P R' (vol (rowShape P R' G' Suf q n)) (cO j))
    (hlenP : ∀ o j' zs, zs.length = vol (rowShape P R' G' Suf q n) →
      (pieceStep child P R' G' Suf q m n o j' zs).length = vol (rowShape P R' G' Suf q n))
    (hv : ∀ i ∈ regD, v i ≤ M) (vN : v aN = n) (vQN : v aQN = q ^ n) (vP : v kP = P)
    (vRp : v aRp = R') (vGR : v aGR = vol G') (vS : v NLogN.KIL.kS = vol Suf)
    (FP : ∃ L, F kP = (P : ℤ) :: L) (FS : ∃ L, F NLogN.KIL.kS = (vol Suf : ℤ) :: L)
    (F23 : F 23 = []) (F8 : F 8 = []) (F9 : F 9 = []) (F10 : F 10 = []) (F11 : F 11 = [])
    (F0 : F 0 = enc2 ys) (hn1 : 1 ≤ n) (hys : ys.length = vol (rowShape P R' G' Suf q n))
    (hVM : vol (rowShape P R' G' Suf q n) ≤ M) (hmM : m ≤ M) (hB1 : 1 ≤ B) :
    ∃ v' : Fin HS → ℕ, (∀ i, i ∉ pcW → v' i = v i) ∧ (∀ i ∈ regD, v' i ≤ M) ∧
      IRuns I iprog (piecesI q m) (encK s (regState F v regD))
        (encK s (regState (Function.update F 0 (enc2 (runPieces (pieceStep child P R' G' Suf q m n)
          (fun j => m ^ j) 0 (pieceLevels m n) ys))) v' regD))
        (cPcs m n cO B)

Context. The lemma belongs to the part KIL6: all piece calls: piecesI q m: initialise the level registers (aJ = 0, aNN = n, q^0, q^n, aTw = q), count the base-m digits of n (aL), push dP = P and the tower dT = [q]; run level 0, then aL - 1 times (towerUp; next level); pop the tower and dP.

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.