The entry procedure

The entry procedure.

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

theorem NLogN.KFW.p14Q (jG jE jT jL jW : Fin Pp) (rowC : IStmt HS Pp)
    (hG : tbl jG = logC jG (coreC jE)) (hEc : tbl jE = eaccC jE (NLogN.KFW.bodyC jT jW))
    (hT : tbl jT = NLogN.KFW.topC jT jL) (hW : tbl jW = lowC jW jL) (hL : tbl jL = levC jL rowC)
    {K r Z Zr P D S ρ p w k q0 Bp H Mb Bz : ℕ} {Kc : ℝ}
    (hk : k = Nat.log mC D) (hq : q0 = q0f D k)
    (hBp : Bp = padB (P * 2 ^ (K * q0)) (P8Lift.Wc ^ k)) (hH : H = w + KFM.EwB NLogN.KFW.A0 D)
    (LV : ∀ j, LvQ Isym tbl jL rowC K r Z Zr H j (cbW Kc K j))
    (hρ : ρ < K) (hK : 1 ≤ K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hVt : zsz ((Vb K (K * D) S r H 0 P : ℕ) : ℤ) ≤ Zr)
    (hVl : ∀ j ≤ k, zsz ((Vb K (K * (D - q0)) S r H j Bp : ℕ) : ℤ) ≤ Zr)
    (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : MbB K P D w k q0 Bp ≤ Mb)
    (hEZ : zsz (((q0 + lowF ES k (D - q0) + (D / 2 + D % 2)) : ℕ) : ℤ) ≤ Z)
    (hp : zsz (p : ℤ) ≤ Z) (hwZ : w < 2 ^ Z)
    (st : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ)
    (xs : List (Fin r → ℂ)) (hx : RecRep r p zs xs)
    (hl : xs.length = AModel.vol (Butterfly.layerShape P K D S)) (h0 : f 0 = gflat zs ++ l)
    (h36 : f 36 = [(P : ℤ), (K : ℤ), (D : ℤ), (S : ℤ), (ρ : ℤ), (r : ℤ), (p : ℤ), (w : ℤ), (Z : ℤ)])
    (hfree : ∀ j : Fin HS, j ≠ 0 → j ≠ 36 → j.val < 50 → f j = [])
    (hb : NLogN.KFB.GB w zs) (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1)
    (hex : ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)) :
    IRuns Isym tbl (p14C jG) (NLogN.KIL.encK st f)
      (NLogN.KIL.encK st (Function.update f 0 (gflat (Classical.choose hex) ++ l)))
      (8 * (2 * moveCost Z + 19) + (cChain Kc K S r H P D k q0 Bp Z Zr Bz w +
        8 * (2 * moveCost Z + 19)))

Context. The lemma belongs to the part KFW C-layer 16: the run of the entry procedure.

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.