The Φ (forward) and Φ⁻¹ calls. fwd = true calls eF on PhiD, else eB

The Φ (forward) and Φ⁻¹ calls. fwd = true calls eF on PhiD, else eB.

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

theorem NLogN.KFM.phi_phase {eF eB : Fin (7 + P')} {dS : Fin HS} {C₀ : ℝ} (hd0 : dS ≠ 0)
    (hP : phiG Isym ext eF eB dS C₀ (pP n + 2) (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n) (muN n))
    (Bd : ℕ) (hBd : ∀ x ∈ descPhiN n, zsz x ≤ Bd)
    (t : IState HS) (hR : BaseOK t n) (xs : List ℤ) (R0 : List Item)
    (h0 : t.G 0 = ints xs ++ R0) (hxw : Bnd (pP n + 2) xs) :
    (xs.length = vol (KFU.shK (IntMul.OpenAI.Glue.dP n) (KFU.sP (IntMul.OpenAI.Glue.dP n) (srcN n))) →
      ∃ c : ℕ, IRuns Isym iprog (callW (descPhiP (bX dS) rPw) (bX dS) (bY dS) dS (g eF)) t
        (t.upd 0 (ints (KFU.PhiD (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n) (muN n) xs) ++ R0)) c ∧
        (c : ℝ) ≤ kPhi n Bd C₀) ∧
    (xs.length = vol (KFU.shR (IntMul.OpenAI.Glue.dP n) (KFU.tP (IntMul.OpenAI.Glue.dP n) (ℓP n - 1) (bLn n))) →
      ∃ c : ℕ, IRuns Isym iprog (callW (descPhiP (bX dS) rPw) (bX dS) (bY dS) dS (g eB)) t
        (t.upd 0 (ints (KFU.PhiInvD (ℓP n - 1) (IntMul.OpenAI.Glue.dP n) (bLn n) (srcN n) (muN n) xs) ++ R0)) c ∧
        (c : ℝ) ≤ kPhi n Bd C₀)

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.