The whole chain

The whole chain. All hypotheses are the per-procedure guarantees of §9.4–9.7 and the exact identities; the conclusion is the final < 1/2 bound before rounding.

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

theorem NLogN.KFM.chain_close (p b γ : ℕ) (S : ℝ) (hS0 : 0 ≤ S)
    -- exact maps
    {A : (κ → ℂ) → (ι → ℂ)} {QF : (ι → ℂ) → (ι → ℂ)} {B0 : (ι → ℂ) → (κ → ℂ)}
    {Mr : (ι → ℂ) → (ι → ℂ) → (ι → ℂ)} {θ θi a ck : ι → ℂ}
    (hA : LinC A) (hQF : LinC QF) (hB : LinC B0) (hMr : BilC Mr)
    (hQFa : ∀ x, a * (θi * Mr (θ * ck) (θ * (a * x))) = QF x)
    (hFc : ∀ w, ‖(2 : ℂ) ^ γ • B0 (QF (A w))‖ ≤ ‖w‖)
    -- computed procedures
    {At : (κ → ℂ) → (ι → ℂ)} {B0t : (ι → ℂ) → (κ → ℂ)} {Mrt : (ι → ℂ) → (ι → ℂ) → (ι → ℂ)}
    {θt θit at' bt : ι → ℂ} (εA εB Er : ℝ)
    (hAt : ∀ u, Grid p u → ‖u‖ ≤ 1 / 2 → ‖At u - A u‖ ≤ εA * hp p ∧ Grid p (At u))
    (hBt : ∀ y, Grid p y → ‖y‖ ≤ 1 → ‖B0t y - B0 y‖ ≤ εB * hp p)
    (hMrt : ∀ f g, Grid p f → Grid p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 → ‖Mrt f g - Mr f g‖ ≤ Er * hp p)
    (hθ : Phases p θ θt) (hθi : Phases p θi θit) (ha : Phases p a at') (hb' : Phases p ck bt)
    (hbg : Grid p bt)
    (hθg : Grid p θit)
    -- sizes
    (hεA : εA * hp p ≤ 1 / 10) (hEr : Er * hp p ≤ 1 / 10)
    (hEs : (2 : ℝ) ^ γ * ((εA + (Er + 22) + εB) * hp p) ≤ 1 / 100)
    (hB2 : 2 * (2 : ℝ) ^ (2 * b + 4) * S ^ 2 *
      (3 * ((2 : ℝ) ^ γ * (εA + (Er + 22) + εB)) + 2) * hp p < 1)
    -- data
    {u v : κ → ℂ} (hu : Grid p u) (hv : Grid p v) (hu1 : ‖u‖ ≤ 1 / 4) (hv1 : ‖v‖ ≤ 1 / 4)
    {c : κ → ℂ}
    (hc : ∀ j, (2 : ℂ) ^ (2 * b + 4) * S * (S * cnj ((fun w => (2 : ℂ) ^ γ • B0 (QF (A w)))
      (cnj ((2 : ℂ) ^ γ • B0 (QF (A u)) * (2 : ℂ) ^ γ • B0 (QF (A v))))) j) = c j) :
    let Ft : (κ → ℂ) → (κ → ℂ) := fun w =>
      (2 : ℂ) ^ γ • B0t (chirpT p (mcT p Mrt θt θit) bt at' (At w))
    ∀ j, ‖(2 : ℂ) ^ (2 * b + 4) * S * (S * plusT Ft (QA p (Ft u * Ft v)) j) - c j‖ < 1 / 2

Context. The lemma belongs to the part KFM 14: the whole error chain and exact recovery (§9.7), abstract form.

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.