The core

The core.

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

theorem NLogN.KFV.core_runs {Ctx : IState HS → Prop} {cF cO : IStmt HS Pp}
    {ℓ p W n kF kO : ℕ} {TF TO : List (Fin (2 ^ ℓ) → ℂ) → List (Fin (2 ^ ℓ) → ℂ)}
    (s : IState HS) (fB : Fin HS → List ℤ) (hfT : fB NLogN.KFV.sT = [])
    (hC : ∀ X, Ctx (encK s (Function.update fB NLogN.KFV.sT X)))
    (HF : LayerU I iprog Ctx cF TF (2 ^ n) p W kF) (HO : LayerU I iprog Ctx cO TO (2 ^ n) p W kO)
    (hn : RT (encK s fB) gNn n) (hl : RT (encK s fB) gLl ℓ) (hp : RT (encK s fB) gPp p)
    {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y) {φ BK B : ℕ}
    (hΦ : ∀ x y : ℤ, zsz x ≤ NLogN.KFV.kb p ℓ * 2 ^ ℓ + 2 → zsz y ≤ NLogN.KFV.kb p ℓ * 2 ^ ℓ + 2 → M.Φ x y ≤ φ)
    (hBK : 2 * (NLogN.KFV.kb p ℓ * 2 ^ ℓ) + p + n + ℓ + 8 ≤ BK) (hB : W + n + ℓ + 4 ≤ B) (hpW : p + 1 ≤ W)
    {zf zg : List GI} (l : List ℤ) {xf xg : List (Fin (2 ^ ℓ) → ℂ)}
    (hxf : RecRep (2 ^ ℓ) p zf xf) (hxg : RecRep (2 ^ ℓ) p zg xg)
    (hlf : xf.length = 2 ^ n) (hlg : xg.length = 2 ^ n) (hbf : NLogN.KFB.GB W zf) (hbg : NLogN.KFB.GB W zg)
    (hdf : Disk xf) (hdg : Disk xg) :
    ∃ zh : List GI,
      RecRep (2 ^ ℓ) p zh ((TO (List.zipWith (ppq (2 ^ ℓ) p) (TF xf) (TF xg))).map
        fun x => ((2 : ℂ) ^ n) • x) ∧
      (TO (List.zipWith (ppq (2 ^ ℓ) p) (TF xf) (TF xg))).length = 2 ^ n ∧
      IRuns I iprog (core18 cF cO pM) (encK (encK s fB) (o0 (gflat zf ++ (gflat zg ++ l))))
        (encK (encK s fB) (o0 (gflat zh ++ l)))
        (kF + (cShut (2 * (2 ^ n * 2 ^ ℓ)) B + (kF + (cShut (2 * (2 ^ n * 2 ^ ℓ)) B +
          (cKronS p ℓ n BK φ + (kO + cScale (2 * (2 ^ n * 2 ^ ℓ)) B))))))

Context. The lemma belongs to the part KFV §52: the core of the Proposition 18 program (two arrays).

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.