Uniform Lemma 12 on Gaussian arrays in the l12prog table: KFS.swAxG_spec with w, u, p, q, sh read from the…

Uniform Lemma 12 on Gaussian arrays in the l12prog table: KFS.swAxG_spec with w, u, p, q, sh read from the descriptor on dS.

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

theorem NLogN.KFW.swGU_spec :
    ∃ q₀ : ℕ, ∀ q', q'.Prime → q₀ < q' → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u w : ℕ) (sh : Shape) (p q : ℕ), 1 ≤ u → (∀ a ∈ sh, 1 ≤ a) → p < q → q < sh.length →
      sh.getD p 0 = 2 ^ u → sh.getD q 0 = 2 ^ u →
      ∀ (I : List Sym) (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ),
      (∀ j, j ≠ 0 → j ≠ NLogN.KFW.dS → f j = []) → f NLogN.KFW.dS = KFM.descSw w u p q sh →
      f 0 = gflat zs ++ l → zs.length = vol sh → NLogN.KFB.GB w zs →
      ∃ c : ℕ, IRuns I l12prog (swGU q') (encK s f)
        (encK s (Function.update f 0 (gflat (pull sh sh (swapPos p q) 0 zs) ++ l))) c ∧
        (c : ℝ) ≤ K * (((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τS +
          (((sh.length + 1) * (Nat.size (vol sh) + w + u + 1) ^ 2 : ℕ) : ℝ))

Context. The lemma belongs to the part KFW: uniform Lemma 12 on Gaussian arrays (SwapNeed): swGU q = descP ; swWU q ; popP: read the descriptor descSw w u p q sh on dS into the registers of swWU (descP), run the register-driven integer swap on the shape sh ++ [2], and pop the registers again. swGU_spec, and swapNeed : KFM.SwapNeed with the table kTable (fun _ => (swGU q).ren id (gL 1)) (one fixed prime q).

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_Defs22.