Error of the computed source transform F̃ u = 2^γ B̃₀(C̃(Ã u)) against F u = 2^γ B₀(QF(A u)), for grid u…

Error of the computed source transform F̃ u = 2^γ B̃₀(C̃(Ã u)) against F u = 2^γ B₀(QF(A u)), for grid u of norm ≤ 1/2.

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

theorem NLogN.KFM.source_err (p : ℕ) (γ : ℕ) {A : (κ → ℂ) → (ι → ℂ)} {QF : (ι → ℂ) → (ι → ℂ)}
    {B0 : (ι → ℂ) → (κ → ℂ)} (hA : LinC A) (hQF : LinC QF) (hB : LinC B0)
    {At : (κ → ℂ) → (ι → ℂ)} {Ct : (ι → ℂ) → (ι → ℂ)} {B0t : (ι → ℂ) → (κ → ℂ)}
    (εA Ec εB : ℝ)
    (hAt : ∀ u, Grid p u → ‖u‖ ≤ 1 / 2 → ‖At u - A u‖ ≤ εA * hp p ∧ Grid p (At u))
    (hCt : ∀ x, Grid p x → ‖x‖ ≤ 6 / 10 → ‖Ct x - QF x‖ ≤ Ec * hp p ∧ ‖Ct x‖ ≤ 1 ∧ Grid p (Ct x))
    (hBt : ∀ y, Grid p y → ‖y‖ ≤ 1 → ‖B0t y - B0 y‖ ≤ εB * hp p)
    (hεA : εA * hp p ≤ 1 / 10)
    {u : κ → ℂ} (hu : Grid p u) (hu1 : ‖u‖ ≤ 1 / 2) :
    ‖(2 : ℂ) ^ γ • B0t (Ct (At u)) - (2 : ℂ) ^ γ • B0 (QF (A u))‖ ≤
      2 ^ γ * ((εA + Ec + εB) * hp p)

Context. The lemma belongs to the part KFM 14: the error chain of the computed pipeline (§9.7.1), abstract form: Arrays are functions ι → ℂ with the sup norm; hp = 2^{-p}. Every computed procedure is an arbitrary function with an error bound on grid inputs (Grid p f: Q_p f = f), so the IL denotations (and P18IL) plug in later.

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_Defs20.