Error of the computed chirp transform

Error of the computed chirp transform. If M̃C is within Ec·hp of the bilinear contraction MC with output norm ≤ 1 (grid inputs, first of norm ≤ 1, second ≤ 7/10), and ã is a grid approximation of the unit phases a, then for ‖x‖ ≤ 6/10: ‖C̃(x) - a · MC(a, a · x)‖ ≤ (Ec + 10)hp and ‖C̃(x)‖ ≤ 1.

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

theorem NLogN.KFM.chirp_err (p : ℕ) {MC MCt : (ι → ℂ) → (ι → ℂ) → (ι → ℂ)} (hMC : BilC MC) (Ec : ℝ)
    (hMCt : ∀ f g, Grid p f → Grid p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 7 / 10 →
      ‖MCt f g - MC f g‖ ≤ Ec * hp p ∧ ‖MCt f g‖ ≤ 1)
    {a at' b bt : ι → ℂ} (ha : Phases p a at') (hb' : Phases p b bt) (hbg : Grid p bt)
    {x : ι → ℂ} (hx : ‖x‖ ≤ 6 / 10) :
    ‖chirpT p MCt bt at' x - a * MC b (a * x)‖ ≤ (Ec + 10) * hp p ∧
      ‖chirpT p MCt bt at' x‖ ≤ 1

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.