The error chain of §9.7 with every exact map instantiated

The error chain of §9.7 with every exact map instantiated. The remaining hypotheses are the guarantees of the computed procedures: the line maps Ã, B̃₀ (against Lemma 19's tensor witnesses), the ring convolution M̃r (against mrX, i.e. Proposition 18), and the grid phase tables for the twist ζ^{j_D}, its inverse, the chirp a and its conjugate.

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

theorem NLogN.KFM.chain_concrete (p b α : ℕ) (s t : Fin (D + 1) → ℕ) [∀ i, NeZero (s i)] [∀ i, NeZero (t i)]
    (M : AxisMaps (d := D + 1) p α s t) (ht : ∀ i, Even (t i))
    (hcop : ∀ i, Nat.Coprime (s i) (t i)) (ζ : ℂ) (hζ : ζ ^ t (Fin.last D) = -1)
    {At : (((i : Fin (D + 1)) → ZMod (s i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (t i)) → ℂ)}
    {B0t : (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (s i)) → ℂ)}
    {Mrt : (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (t i)) → ℂ) →
      (((i : Fin (D + 1)) → ZMod (t i)) → ℂ)}
    {θt θit at' bt : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ} (εA εB Er : ℝ)
    (hAt : ∀ u, Grid p u → ‖u‖ ≤ 1 / 2 →
      ‖At u - tensCLM (kerA M.A) u‖ ≤ εA * hp p ∧ Grid p (At u))
    (hBt : ∀ y, Grid p y → ‖y‖ ≤ 1 → ‖B0t y - tensCLM (kerB M.B) y‖ ≤ εB * hp p)
    (hMrt : ∀ f g, Grid p f → Grid p g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 → ‖Mrt f g - mrX t f g‖ ≤ Er * hp p)
    (hθ : Phases p (twX t ζ) θt) (hθi : Phases p (fun j => (twX t ζ j)⁻¹) θit)
    (ha : Phases p (fun j => (starRingEnd ℂ) (chirp s t j)) at') (hb' : Phases p (chirp s t) bt)
    (hbg : Grid p bt) (hθg : Grid p θit)
    (hεA : εA * hp p ≤ 1 / 10) (hEr : Er * hp p ≤ 1 / 10)
    (hEs : (2 : ℝ) ^ (2 * (D + 1) * α ^ 2) * ((εA + (Er + 22) + εB) * hp p) ≤ 1 / 100)
    (hB2 : 2 * (2 : ℝ) ^ (2 * b + 4) * (∏ i, (s i : ℝ)) ^ 2 *
      (3 * ((2 : ℝ) ^ (2 * (D + 1) * α ^ 2) * (εA + (Er + 22) + εB)) + 2) * hp p < 1)
    {ubar vbar : ((i : Fin (D + 1)) → ZMod (s i)) → ℂ}
    (hu : Grid p (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k))
    (hv : Grid p (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k))
    (hu1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k)‖ ≤ 1 / 4)
    (hv1 : ‖(fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k)‖ ≤ 1 / 4) :
    let Ft : (((i : Fin (D + 1)) → ZMod (s i)) → ℂ) → (((i : Fin (D + 1)) → ZMod (s i)) → ℂ) :=
      fun w => (2 : ℂ) ^ (2 * (D + 1) * α ^ 2) • B0t (chirpT p (mcT p Mrt θt θit) bt at' (At w))
    ∀ j, ‖(2 : ℂ) ^ (2 * b + 4) * ((∏ i, (s i : ℝ) : ℝ) : ℂ) * (((∏ i, (s i : ℝ) : ℝ) : ℂ) *
      plusT Ft (QA p (Ft (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k) *
        Ft (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k))) j) - cconv s ubar vbar j‖ < 1 / 2

Context. The lemma belongs to the part KFM 14: the exact side of the error chain: The exact maps of §9.4–9.7 as LinC / BilC instances, and the identities chain_close needs.

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.