The three swaps on the 8-axis geometry (Q = 2^u): axes 1↔3, 3↔5, 1↔5 are rixT g sw01, rixT g sw12, rixT g…

The three swaps on the 8-axis geometry (Q = 2^u): axes 1↔3, 3↔5, 1↔5 are rixT g sw01, rixT g sw12, rixT g sw02, each at cost ≤ K (V + 1) u^τ.

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

theorem NLogN.KFL.swI_geo :
    ∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (g : Geo), g.Pos → ∀ u : ℕ, 1 ≤ u → g.Q = 2 ^ u →
      ∀ (I : List Sym) (t : IState HS) (zs : List ℤ) (R : List Item),
      Bits zs → t.G 0 = ints zs ++ R → zs.length = g.V →
      (∃ c : ℕ, IRuns I l12prog (swI q g.N0 g.N1 (vol [g.N2, g.Q, g.N3, g.B]) u) t
          (t.upd 0 (ints (rixT g sw01 zs) ++ R)) c ∧
          (c : ℝ) ≤ K * ((g.V : ℝ) + 1) * (u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)) ∧
      (∃ c : ℕ, IRuns I l12prog (swI q (vol [g.N0, g.Q, g.N1]) g.N2 (vol [g.N3, g.B]) u) t
          (t.upd 0 (ints (rixT g sw12 zs) ++ R)) c ∧
          (c : ℝ) ≤ K * ((g.V : ℝ) + 1) * (u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50)) ∧
      (∃ c : ℕ, IRuns I l12prog (swI q g.N0 (vol [g.N1, g.Q, g.N2]) (vol [g.N3, g.B]) u) t
          (t.upd 0 (ints (rixT g sw02 zs) ++ R)) c ∧
          (c : ℝ) ≤ K * ((g.V : ℝ) + 1) * (u : ℝ) ^ (1 - (2 : ℝ)⁻¹ ^ 50))

Context. The lemma belongs to the part KFL §4: the Lemma 12 swap wrapper: swI q vP vG vS u pushes the four Lemma 12 parameters (kP, kG, kS, aU), runs the fine Lemma 12 program l12F, and pops them. swI_spec: on any state whose stack 0 is enc2 xs ++ R (arbitrary tail R, no other hypothesis) it interchanges the two [2^u] fields of binShape Pre G Suf (2^u) at cost ≤ K (V + 1) u^τ, τ = 1 - 2^-50.

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.