The product

The product.

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

theorem NLogN.KFM.mul_phase (C : BigCtx ix Isym extM n D) (t : IState HS) (hR : BaseOK t n) (x y : ℕ)
    (hx : x < 2 ^ n) (hy : y < 2 ^ n) (hA : t.G ARGM = [.int (y : ℤ), .int (x : ℤ)])
    (h0 : t.G 0 = []) (hW : t.G pW = []) :
    ∃ (zsZ : List GI) (Z Ux Uy : ((i : Fin (D + 1)) → ZMod (sBD n D i)) → ℂ) (c : ℕ),
      IRuns Isym (kTable extM) (mulP ix) t (((t.upd ARGM []).upd pW []).upd 0 (ints (gflat zsZ)))
        c ∧
      RepPad (pP n) (sBD n D) (tBD n D) zsZ Z ∧ NLogN.KFB.GB (NLogN.KFM.wU n D) zsZ ∧
      ‖Z - Rperm (sBD n D) (tBD n D) (dftM (sBD n D) (cnj (QA (pP n) (Ux * Uy))))‖ ≤
        EsN n D * hp (pP n) ∧
      ‖Ux - Rperm (sBD n D) (tBD n D)
        (dftM (sBD n D) (fun k => (2 : ℂ)⁻¹ ^ (bP n + 2) * ubar C x k))‖ ≤ EsN n D * hp (pP n) ∧
      ‖Uy - Rperm (sBD n D) (tBD n D)
        (dftM (sBD n D) (fun k => (2 : ℂ)⁻¹ ^ (bP n + 2) * ubar C y k))‖ ≤ EsN n D * hp (pP n) ∧
      (c : ℝ) ≤ kMul C

Context. The lemma belongs to the part KFM Big7: the product Z: mulP = inP; mv² 0 → pW; inP; gmul; conj; F̃. From ARGM = [y, x] it leaves on stack 0 an array Z with ‖Z − R F_s(cnj Q_p(U_x U_y))‖ ≤ Es hp, where U_x, U_y are the transforms of the two inputs (inP_phase).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.