The uniform level step computes the template step on the level layout

The uniform level step computes the template step on the level layout.

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

theorem NLogN.KIL.stepU_spec {N : ℕ} [NeZero N] (A B Cs : Shape) (P L : ℕ) (T : TSh m) (rX : Fin HS)
    (hrX : 38 ≤ rX.val ∧ rX.val < 56)
    (hpos : ∀ a ∈ P :: L :: hdShape A B Cs m N, 1 ≤ a)
    (t : IState HS) (xs : List ℤ) (Bb : ℕ) (R : List Item) (hT : TOK T N Bb)
    (hlen : xs.length = vol (P :: L :: hdShape A B Cs m N)) (hb : Bnd Bb xs)
    (hV : zsz ((vol (P :: L :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb) (h0 : t.G 0 = ints xs ++ R)
    {LN LQ LX LB LC : List Item} (hNQ : t.G sNQ = .int (-(N : ℤ)) :: LN)
    (hQQ : t.G sQQ = .int (N : ℤ) :: LQ)
    (hX : t.G rX = .int ((vol (P :: L :: A) : ℕ) : ℤ) :: LX)
    (hB : t.G rVB = .int ((vol B : ℕ) : ℤ) :: LB)
    (hC : t.G rVC = .int ((vol Cs : ℕ) : ℤ) :: LC) :
    Sp (stepU m rX T) t
      (t.upd 0 (ints ((T.eval N).arr ((hdLayout A B Cs m N).cons2 P L) 0 xs) ++ R))
      (cStepG T.k T.d (stgT rX T).length (vol (P :: L :: hdShape A B Cs m N)) Bb (paT rX T)
        (pcT T) (stgT rX T))

Context. The lemma belongs to the part KIL4: the uniform level step stepU: A shift template TSh m fixes the active field i, the fraction k/d of the unit, its sign and the rational controls cs j = (p_j, q_j) (control j is p_j · q_j⁻¹ mod N). The template does not mention the modulus N, the level or any volume.

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.