Pull through a uniform block expansion

Pull through a uniform block expansion.

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

theorem NLogN.KFS.pull_flatMap (sh : Shape) (g : List ℕ → List ℕ) (hg : ∀ a, Valid sh a → Valid sh (g a))
    (f : α → List β) (B : ℕ) (hf : ∀ x, (f x).length = B) (d : α) (d' : β)
    (xs : List α) (hxs : xs.length = vol sh) :
    (AModel.pull sh sh g d xs).flatMap f =
      AModel.pull (sh ++ [B]) (sh ++ [B]) (fun a => g (a.take sh.length) ++ a.drop sh.length) d'
        (xs.flatMap f)

Context. The lemma belongs to the part KFS §1: lifting a pull through a fixed-length item expansion: If every item x of an array of shape sh is expanded into a block f x of B entries (bitsL w = flatMap (encW w) with B = w + 1, or gflat with B = 2), the expanded array has shape sh ++ [B], and a pull on sh becomes the pull on sh ++ [B] that acts on the first sh.length digits and fixes the last one (pull_flatMap). For the field swap swapPos p q (p, q < sh.length) this is again swapPos p q (pull_swapPos_flatMap).

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.