The chirp call

The chirp call.

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

theorem NLogN.KFM.chirp_phase [∀ i, NeZero (tBD n D i)] {eC : Fin (7 + P')} {dS : Fin HS} {C₀ : ℝ} {A : ℕ}
    {θt θit at' bt : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ} (hd0 : dS ≠ 0)
    (hC : chirpGN Isym ext eC dS C₀ A n D θt θit at' bt) (Bd : ℕ)
    (hBd : ∀ x ∈ descChirpN n, zsz x ≤ Bd)
    (t : IState HS) (hR : BaseOK t n) (xs : List GI) (x : ((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ)
    (R0 : List Item) (h0 : t.G 0 = ints (gflat xs) ++ R0)
    (hx : RepFull (pP n) (tBD n D) xs x) (hx1 : ‖x‖ ≤ 6 / 10) :
    ∃ (Mrt : (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ) →
          (((i : Fin (D + 1)) → ZMod (tBD n D i)) → ℂ)),
      (∀ f g, Grid (pP n) f → Grid (pP n) g → ‖f‖ ≤ 1 → ‖g‖ ≤ 1 →
        ‖Mrt f g - mrX (tBD n D) f g‖ ≤ ErC n D * hp (pP n)) ∧
    ∃ (ys : List GI) (c : ℕ),
      IRuns Isym iprog (callW (descChirpP (bX dS)) (bX dS) (bY dS) dS (g eC)) t
        (t.upd 0 (ints (gflat ys) ++ R0)) c ∧
      RepFull (pP n) (tBD n D) ys (chirpT (pP n) (mcT (pP n) Mrt θt θit) bt at' x) ∧
      NLogN.KFB.GB (pP n + 2) ys ∧ (c : ℝ) ≤ kChirp n Bd C₀ A

Context. The lemma belongs to the part KFM Big2: the interface calls of bigE: Every interface call is callW bld X Y dS e (KFMCall) with the descriptor builder bld (KFMSB, KFMSF) on the builder stack X = bX dS and the scratch Y = bY dS (both differ from the interface's descriptor stack dS). A run of the interface in its own table kTable ext is a run in the merged table (IRuns.relabel).

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.