Uniform Lemma 12 on w-bit integer arrays (KFS.swW_spec with the registers sW = w, sU = u, sN = V, sP = vol…

Uniform Lemma 12 on w-bit integer arrays (KFS.swW_spec with the registers sW = w, sU = u, sN = V, sP = vol Pre, sG = vol G, sS = vol Suf · (w+1)).

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

theorem NLogN.KFW.swWU_spec :
    ∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u w : ℕ) (Pre G Suf : Shape), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      ∀ (I : List Sym) (t : IState HS) (xs : List ℤ) (R : List Item),
      t.G 0 = ints xs ++ R → xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      (∀ x ∈ xs, zsz x ≤ w) →
      ∀ {L1 L2 L3 L4 L5 L6 : List Item},
      t.G sN = .int (vol (binShape Pre G Suf (2 ^ u)) : ℤ) :: L1 → t.G NLogN.KFW.sW = .int (w : ℤ) :: L2 →
      t.G NLogN.KFW.sP = .int (vol Pre : ℤ) :: L3 → t.G sG = .int (vol G : ℤ) :: L4 →
      t.G sS = .int ((vol Suf * (w + 1) : ℕ) : ℤ) :: L5 → t.G sU = .int (u : ℤ) :: L6 →
      ∃ c : ℕ, IRuns I l12prog (swWU q) t
        (t.upd 0 (ints (pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
          (swapPos Pre.length (Pre.length + 1 + G.length)) 0 xs) ++ R)) c ∧
        (c : ℝ) ≤ K * ((w : ℝ) + 1) * ((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) *
          (u : ℝ) ^ τS

Context. The lemma belongs to the part KFW: uniform Lemma 12 on integer arrays (parameters in registers).

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.