rotStep_runs (KFL §6: one line (22) as an item program)

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

theorem NLogN.KFL.rotStep_runs {K ρ f : ℕ} (hK : 1 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) {d0 d1 Q : ℕ}
    (hd0 : 0 < d0) (hd1 : 0 < d1) (hQe : 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)
    (zd0 : zsz (d0 : ℤ) ≤ Bb) (zd1 : zsz (d1 : ℤ) ≤ Bb)
    (P B w : ℕ) (zP : zsz (P : ℤ) ≤ Bb) (zB : zsz (B : ℤ) ≤ Bb)
    (t : IState HS) (xs : List ℤ) (R : List Item) (hlen : xs.length = P * Q * B) (hbw : Bnd w xs)
    (h0 : t.G 0 = ints xs ++ R) :
    IRuns I iprog (NLogN.KFL.rotStep K ρ f d0 d1 Q P B l.sgn l.b) t
      (t.upd 0 (ints (AModel.pull [P, Q, B] [P, Q, B] (KIL.rotAddr Q (tabA K ρ f d0 d1 Q l)) 0 xs) ++ R))
      (NLogN.KFL.cRot K f l.b P Q B 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.