A fixed template list computes the denoted steps on the level layout

A fixed template list computes the denoted steps on the level layout.

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

theorem NLogN.KFD.stepsU_fspec {N : ℕ} [NeZero N] (A B Cs : Shape) (P L : ℕ) (rX : Fin HS)
    (hrX : 38 ≤ rX.val ∧ rX.val < 56)
    (hpos : ∀ a ∈ P :: L :: hdShape A B Cs m N, 1 ≤ a) (w Bb : ℕ) (R : List Item)
    (hV : zsz ((vol (P :: L :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb)
    {LN LQ LX LB LC : List Item} (t : IState HS) (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) :
    ∀ (Ts : List (TSh m)) (xs : List ℤ), (∀ T ∈ Ts, TOK T N Bb) →
      xs.length = vol (P :: L :: hdShape A B Cs m N) → Bnd w xs → t.G 0 = ints xs ++ R →
      FSp (stepsU m rX Ts) t
        (t.upd 0 (ints (AModel.runArr ((hdLayout A B Cs m N).cons2 P L) 0 (Ts.map (·.eval N)) xs) ++ R))
        (cStepsUF rX (vol (P :: L :: hdShape A B Cs m N)) w Bb Ts)

Context. The lemma belongs to the part KFD: the fine uniform level step: stepG_fspec / stepU_fspec: the KIL4 step programs (unchanged) with fine cost cStepGF; the data bound w and the global bound Bb are separate. cStepGF_le: cStepGF ≤ tKF·(10^13 (V+1)(w+2) + 10^10 (Bb+2)²).

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.