Lemma 12 on w-bit integer arrays, any two axes

Lemma 12 on w-bit integer arrays, any two axes. For p < q < |sh| with sh[p] = sh[q] = 2^u, swAx realises pull sh sh (swapPos p q) at cost ≤ K (w+1) (V+1) u^τ.

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

theorem NLogN.KFS.swAx_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) (t : IState HS) (xs : List ℤ) (R : List Item),
      t.G 0 = ints xs ++ R → xs.length = vol sh → (∀ x ∈ xs, zsz x ≤ w) →
      ∃ c : ℕ, IRuns I l12prog (swAx q' w sh p q u) t
        (t.upd 0 (ints (AModel.pull sh sh (swapPos p q) 0 xs) ++ R)) c ∧
        (c : ℝ) ≤ K * ((w : ℝ) + 1) * ((vol sh : ℝ) + 1) * (u : ℝ) ^ τS

Context. The lemma belongs to the part KFS §2: Lemma 12 on arrays of w-bit integers and of Gaussian records: Route (b) of MACHINE-PLAN.md §3 item 2(iii): convert the items to bits (KFL.toBitsI, sign plus w magnitude bits per integer), so that the item axis becomes an innermost bit axis of size w + 1, interchange the two 2^u fields with the fine Lemma 12 wrapper KFL.swI, and convert back (KFL.fromBitsI).

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.