The child wrapper as an IL run

The child wrapper as an IL run. Q is the caller's invariant on the managed stacks (stable under changes of the data stack and of qP, rP); PT runs on the moved segment with list semantics F, length- and bound-preserving.

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

theorem NLogN.KFG.childI_runs (PT : IStmt HS Pp) (F : List GI → List GI) (Q : (Fin HS → List ℤ) → Prop)
    (hQs : ∀ g v0 vP vR, Q g → Q (Function.update (Function.update (Function.update g 0 v0) qP vP)
      NLogN.KFB.rP vR))
    (N off A q M Bb Z w w' cP : ℕ) (hN : N = A * M * q)
    (hA : zsz (A : ℤ) ≤ Bb) (hq : zsz (q : ℤ) ≤ Bb) (hM : zsz (M : ℤ) ≤ Bb) (h2 : zsz (2 : ℤ) ≤ Bb)
    (hA1 : 1 ≤ A) (hq1 : 1 ≤ q) (hM1 : 1 ≤ M)
    (hPT : ∀ (s' : IState HS) (g : Fin HS → List ℤ) (ys : List GI) (R : List ℤ),
      g 0 = gflat ys ++ R → Q g → ys.length = N → NLogN.KFB.GB w ys →
      IRuns I iprog PT (encK s' g) (encK s' (Function.update g 0 (gflat (F ys) ++ R))) cP ∧
        (F ys).length = N ∧ NLogN.KFB.GB w' (F ys))
    (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (hlen : off + N ≤ zs.length) (h0 : f 0 = gflat zs ++ l) (hQ : Q f) (hP : f qP = [])
    (hR : f NLogN.KFB.rP = []) (hb : NLogN.KFB.GB w zs) (hZ : zsz ((2 * off : ℕ) : ℤ) ≤ Z) :
    IRuns I iprog (childI off A q M PT) (encK s f)
      (encK s (Function.update f 0 (gflat (KFB.chL N off q M F zs) ++ l)))
      (cChild w w' off A q M Bb Z + cP)

Context. The lemma belongs to the part KFG: the IL wrapper of a child call (task D).

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.