gflat of a swapped Gaussian array

gflat of a swapped Gaussian array.

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

theorem NLogN.KFS.gflat_pull_swapPos (sh : Shape) {p q : ℕ} (hp : p < sh.length) (hq : q < sh.length)
    (hs : sh.getD p 0 = sh.getD q 0) (d : GI) (zs : List GI) (hzs : zs.length = vol sh) :
    gflat (AModel.pull sh sh (swapPos p q) d zs) =
      AModel.pull (sh ++ [2]) (sh ++ [2]) (swapPos p q) 0 (gflat zs)

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.