One line on the geometry: the rotation step with P = N0·Q·N1·Q·N2, B = S2, d0 = N2·Q·N1, d1 = N2 is rixT g…

One line on the geometry: the rotation step with P = N0·Q·N1·Q·N2, B = S2, d0 = N2·Q·N1, d1 = N2 is rixT g (rot2 Q (amt K ρ f l)).

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

theorem NLogN.KFL.rotStep_geo {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
    {K ρ f : ℕ} (hK : 1 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) (g : Geo) (hg : g.Pos)
    (hQe : g.Q = 2 ^ (f * K)) (l : Line) (hs : l.sgn = 1 ∨ l.sgn = -1)
    (hb : l.b = 0 ∨ l.b = 1) {Bb : ℕ} (hB2 : 2 ≤ Bb) (hbig : 4 * 2 ^ (f * K) < 2 ^ Bb)
    (zV : zsz (g.V : ℤ) ≤ Bb) (w : ℕ)
    (t : IState HS) (xs : List ℤ) (R : List Item) (hlen : xs.length = g.V) (hbw : Bnd w xs)
    (h0 : t.G 0 = ints xs ++ R) :
    IRuns I iprog (NLogN.KFL.rotStep K ρ f (g.N2 * g.Q * g.N1) g.N2 g.Q
        (g.N0 * g.Q * g.N1 * g.Q * g.N2) g.S2 l.sgn l.b) t
      (t.upd 0 (ints (rixT g (rot2 g.Q (amt K ρ f l)) xs) ++ R))
      (NLogN.KFL.cRot K f l.b (g.N0 * g.Q * g.N1 * g.Q * g.N2) g.Q g.S2 w Bb)

Context. The lemma belongs to the part KFL §6: one line (22) as an item program: rotStep … l pushes P, Q, B on stacks 1, 2, 4, generates the table of line l (tabGen, stack 14) and runs the fine block rotation KFC.rotF (which consumes the table). rotStep_runs: the result is the rotation pull pull [P,Q,B] [P,Q,B] (rotAddr Q (tabA …)). rotStep_geo: on the 8-axis geometry with d0 = N2·Q·N1, d1 = N2, this is rixT g (rot2 Q (amt K ρ f l)), i.e. the line acting on the third slot z with controls (x, y) (canonical slots).

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.