§9.6 exactness in the form of chain_close

§9.6 exactness in the form of chain_close.

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

theorem NLogN.KFM.final_exact (s t : Fin d → ℕ) [∀ i, NeZero (s i)] (hcop : ∀ i, Nat.Coprime (s i) (t i))
    (b : ℕ) (ubar vbar : ((i : Fin d) → ZMod (s i)) → ℂ) (j : (i : Fin d) → ZMod (s i)) :
    (2 : ℂ) ^ (2 * b + 4) * (∏ i, (s i : ℂ)) * ((∏ i, (s i : ℂ)) *
      cnj (Rperm s t (dftM s (cnj (Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * ubar k)) *
        Rperm s t (dftM s (fun k => (2 : ℂ)⁻¹ ^ (b + 2) * vbar k)))))) j) = cconv s ubar vbar j

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.