Truncation on records: Q_p of the array is represented by the truncated numerators
ProvedNLogN.KFH.truncP_repTruncation on records: Q_p of the array is represented by the truncated numerators.
The following holds (Lean statement, in the scope of module Solutions.KFHRec):
theorem NLogN.KFH.truncP_rep {r p Δ : ℕ} {zs : List GI} {xs : List (Fin r → ℂ)}
(h : RecRep r (p + Δ) zs xs) : RecRep r p (zs.map (gtr Δ)) (Butterfly.QpArr p xs)
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 (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine -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.
-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_K_Defs18 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 set_option linter.unusedSimpArgs false set_option linter.unusedVariables false open NLogN open NLogN.KFH open IntMul RS AModel KIL KFD KFB Complex
theorem NLogN.KFH.truncP_rep {r p Δ : ℕ} {zs : List GI} {xs : List (Fin r → ℂ)}
(h : RecRep r (p + Δ) zs xs) : RecRep r p (zs.map (gtr Δ)) (Butterfly.QpArr p xs) := by sorry