gflat_mvL (KFB: the `child` step (a recursive call on one slot of one role))

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

theorem NLogN.KFB.gflat_mvL {A X Y : ℕ} (zs : List GI) (hl : zs.length = A * X * Y) :
    gflat (NLogN.KFB.mvL X Y zs) = AModel.pull [A, Y, X, 2] [A, X, Y, 2] gS 0 (gflat zs)

Context. The lemma belongs to the part KFB: the child step (a recursive call on one slot of one role): Role w's segment, as Gaussian indices (hi, s, lo) (s = the n bits of slot h), is rearranged to (hi, lo, s) by KFC's fwdF (q = 2^n, the real/imaginary pair kept as the last field), so that slot h becomes 2^{n(m-1)} contiguous blocks of 2^n entries; a program PT computing an operator T blockwise runs on the segment; bwdF moves the field back.

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.