midF_run (KFE: the fine Lemma 12 program)

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

theorem NLogN.KFE.midF_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)
    (hv : ∀ i ∈ regD, v i ≤ M) {q m W K r n : ℕ} (Pre G Suf : Shape) (child : Oracle (ZMod 2))
    (cO : ℕ → ℕ) (ys : List (ZMod 2)) (hq : 2 ≤ q) (hm : 2 ≤ m) (hW : 1 ≤ W)
    (hPre : ∀ a ∈ Pre, 1 ≤ a) (hG : ∀ a ∈ G, 1 ≤ a) (hS : ∀ a ∈ Suf, 1 ≤ a)
    {LP LS : List ℤ} (FP : F kP = (vol Pre : ℤ) :: LP) (FS : F NLogN.KIL.kS = (vol Suf : ℤ) :: LS)
    (vP : v kP = vol Pre) (vS : v NLogN.KIL.kS = vol Suf) (vK : v aK = K) (vQR : v aQR = q ^ r)
    (vN : v aN = n) (vQN : v aQN = q ^ n) (vGR : v aGR = vol G * q ^ r)
    (F0 : F 0 = enc2 ys) (F15 : F 15 = []) (F20 : F 20 = []) (F21 : F 21 = [])
    (F23 : F 23 = []) (F8 : F 8 = []) (F9 : F 9 = []) (F10 : F 10 = []) (F11 : F 11 = [])
    (hys : ys.length = vol (qShape Pre G Suf q (r + n))) (hn1 : 1 ≤ n) (hWK : W ^ K ≤ q ^ r)
    (hVM : 2 * vol (qShape Pre G Suf q (r + n)) ≤ M) (hWM : W ≤ M) (hmM : m ≤ M) (hB1 : 1 ≤ B)
    (hO : ∀ j, m ^ j ≤ n → CallSpec I iprog child q m j (vol Pre) (padRows W K (q ^ r))
      (vol (rowShape (vol Pre) (padRows W K (q ^ r)) (G ++ List.replicate r q) Suf q n)) (cO j))
    (hlenP : ∀ o j' zs, zs.length =
        vol (rowShape (vol Pre) (padRows W K (q ^ r)) (G ++ List.replicate r q) Suf q n) →
      (pieceStep child (vol Pre) (padRows W K (q ^ r)) (G ++ List.replicate r q) Suf q m n o j'
        zs).length =
        vol (rowShape (vol Pre) (padRows W K (q ^ r)) (G ++ List.replicate r q) Suf q n)) :
    ∃ v' : Fin HS → ℕ, (∀ i ∈ regD, v' i ≤ M) ∧
      (∀ i, i ∉ [aJ, aNN, aQO, aQM, aTw, aY, aL, aDg, aWK, aRp, pX, pB, pZ, pT] → v' i = v i) ∧
      IRuns I iprog (midF q m W) (encK s (regState F v regD))
        (encK s (regState (Function.update F 0 (enc2 (l12mid child W m q K r Pre G Suf n 0 ys)))
          v' regD))
        (cMidF K (vol (rowShape (vol Pre) (padRows W K (q ^ r)) (G ++ List.replicate r q) Suf q n))
          m n cO B)

Context. The lemma belongs to the part KFE: the fine Lemma 12 program.

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.