The truncation pass on a record array: from numerators at scale p + Δ to Q_p at scale p, in place on stack…

The truncation pass on a record array: from numerators at scale p + Δ to Q_p at scale p, in place on stack 0; widths do not grow. Cost O(|zs| (w + Δ)) + O(Z).

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

theorem NLogN.KFH.truncP_rec (s : IState HS) {r p Δ w : ℕ} (f : Fin HS → List ℤ) (zs : List GI)
    (xs : List (Fin r → ℂ)) (l : List ℤ) (hx : RecRep r (p + Δ) zs xs)
    (h0 : f 0 = gflat zs ++ l) (hC : Cl f) (hb : NLogN.KFB.GB w zs) (Z : ℕ)
    (hZ : zsz ((2 * zs.length : ℕ) : ℤ) ≤ Z) :
    RecRep r p (zs.map (gtr Δ)) (Butterfly.QpArr p xs) ∧ NLogN.KFB.GB w (zs.map (gtr Δ)) ∧
      FSp (truncP Δ (2 * zs.length)) (encK s f)
        (encK s (Function.update f 0 (gflat (zs.map (gtr Δ)) ++ l)))
        (cTrunc w Δ (2 * zs.length) Z)

Context. The lemma belongs to the part KFH: fixed-point record arrays and the Q_p truncation pass.

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.