The Lemma 12 program computes the variant procedure l12v

The Lemma 12 program computes the variant procedure l12v.

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

theorem NLogN.KFE.l12F_run {I : List Sym} {iprog : Fin 1 → IStmt HS 1} (s : IState HS)
    (F : Fin HS → List ℤ) {M B : ℕ} (hM : zsz (M : ℤ) ≤ B) (hB1 : 1 ≤ B) {q m W u : ℕ}
    (Pre G Suf : Shape) (child : Oracle (ZMod 2)) (cO : ℕ → ℕ) (xs : List (ZMod 2))
    (hq : 2 ≤ q) (hm : 2 ≤ m) (hW : 1 ≤ W) (hu : 1 ≤ u)
    (hPre : ∀ a ∈ Pre, 1 ≤ a) (hG : ∀ a ∈ G, 1 ≤ a) (hS : ∀ a ∈ Suf, 1 ≤ a)
    {LP LG LS LU : List ℤ} (FP : F kP = (vol Pre : ℤ) :: LP) (FG : F kG = (vol G : ℤ) :: LG)
    (FS : F NLogN.KIL.kS = (vol Suf : ℤ) :: LS) (FU : F aU = (u : ℤ) :: LU) (F0 : F 0 = enc2 xs)
    (F8 : F 8 = []) (F9 : F 9 = []) (F10 : F 10 = []) (F11 : F 11 = []) (F15 : F 15 = [])
    (F20 : F 20 = []) (F21 : F 21 = []) (F23 : F 23 = []) (F24 : F 24 = [])
    (hxs : xs.length = vol (binShape Pre G Suf (2 ^ u)))
    {e K : ℕ} (he : e = Nat.clog q (2 ^ u)) (hK : K = Nat.clog m e)
    (hMV : 2 * vol (qShape Pre G Suf q e) + m + W * e ≤ M)
    (hO : 1 ≤ e - min (W * K) e → ∀ j, m ^ j ≤ e - min (W * K) e →
      CallSpec I iprog child q m j (vol Pre) (padRows W K (q ^ min (W * K) e))
        (vol (rowShape (vol Pre) (padRows W K (q ^ min (W * K) e))
          (G ++ List.replicate (min (W * K) e) q) Suf q (e - min (W * K) e))) (cO j))
    (hlenP : 1 ≤ e - min (W * K) e → ∀ o j' zs, zs.length =
        vol (rowShape (vol Pre) (padRows W K (q ^ min (W * K) e))
          (G ++ List.replicate (min (W * K) e) q) Suf q (e - min (W * K) e)) →
      (pieceStep child (vol Pre) (padRows W K (q ^ min (W * K) e))
        (G ++ List.replicate (min (W * K) e) q) Suf q m (e - min (W * K) e) o j' zs).length =
        vol (rowShape (vol Pre) (padRows W K (q ^ min (W * K) e))
          (G ++ List.replicate (min (W * K) e) q) Suf q (e - min (W * K) e))) :
    IRuns I iprog (l12F q m W) (encK s F)
      (encK s (Function.update F 0 (enc2 (l12v child W m q K (W * K) e u Pre G Suf 0 xs))))
      (cL12F u e (min (W * K) e) K (e - min (W * K) e) (vol (qShape Pre G Suf q e))
        (vol (rowShape (vol Pre) (padRows W K (q ^ min (W * K) e))
          (G ++ List.replicate (min (W * K) e) q) Suf q (e - min (W * K) e))) m q 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.