The body computes levelR

The body computes levelR.

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

theorem NLogN.KFD.bodyF_run {N : ℕ} [NeZero N] (hN : 1 < N) (P L' : ℕ) (A B Cs : Shape)
    (hpos : ∀ a ∈ P :: L' :: hdShape A B Cs m N, 1 ≤ a)
    (tpl : IMat m → List (TStep m)) (Pr : IMat m → Prop) (hfr : FramesOK Pr C.gates C.Min C.Mout)
    (hT : ∀ X, Pr X → AModel.edgeSteps C N X = (tpl X).map (TStep.eval N))
    (Bb : ℕ) (hTOK : ∀ X, Pr X → ∀ T, TStep.sh T ∈ tpl X → TOK T N Bb)
    (hV : zsz ((vol (P :: W * L' :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb) (hSB : SubBnd N Bb)
    (G0 : Fin HS → List Item) (hG : LevG G0 m W N P L' A B Cs)
    (j0 : Fin Pp) (child : Fin (m + m) → Fin (m + m) → List (ZMod 2) → List (ZMod 2)) (cC : ℕ)
    (hsw : ∀ X, Pr X → ∀ a b, TStep.sw a b ∈ tpl X → ∀ (t : IState HS) (R : List Item)
      (ys : List (ZMod 2)), NLogN.KIL.Inv G0 t → ys.length = vol (P :: L' :: hdShape A B Cs m N) →
      IRuns I iprog (NLogN.KIL.swC m j0 (a : ℕ) (b : ℕ)) (t.upd 0 (ints (enc2 ys) ++ R))
        (t.upd 0 (ints (enc2 (child a b ys)) ++ R)) cC ∧
      (child a b ys).length = vol (P :: L' :: hdShape A B Cs m N))
    (t : IState HS) (ht : NLogN.KIL.Inv G0 t) (R : List Item) (xs : List (ZMod 2))
    (hxs : xs.length = vol (P :: W * L' :: hdShape A B Cs m N)) :
    IRuns I iprog (bodyF C tpl j0) (t.upd 0 (ints (enc2 xs) ++ R))
      (t.upd 0 (ints (enc2 (levelR C N P L' A B Cs child xs)) ++ R))
      (bodyCF C tpl N P L' A B Cs cC Bb)

Context. The lemma belongs to the part KFD: the fine body of one uniform level: bodyF C tpl j0 is KIL5's bodyU with every per-element piece replaced by its fine form: fcode (subU …), the row split / merge by KFC's bwdF / fwdF, the fine network netCF with fine frame changes edgeCF (fine level steps fcode (stepU …)), the fine routing fcode (rebuildCU …). bodyF_run: the same denotation levelR as bodyU_run, with the fine cost bodyCF.

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.