The Kronecker stage

The Kronecker stage.

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

theorem NLogN.KFV.kronS_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {p ℓ n BK φ : ℕ}
    (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)
    (sB : IState HS) (hp : RT sB gPp p) (hl : RT sB gLl ℓ) (hn : RT sB gNn n)
    {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) (hdf : Disk xf) (hdg : Disk xg) :
    IRuns I iprog (kronS pM) (encK sB (o0 (gflat zf ++ (gflat zg ++ l))))
      (encK sB (o0 (gflat (kmulN (2 ^ ℓ) p ℓ (2 ^ n) zf zg) ++ l))) (cKronS p ℓ n BK φ)

Context. The lemma belongs to the part KFV §49: the Kronecker stage with its parameters (kronS): kronS pM = kPushS ; kronU pM ; kPopS. From the registers p (gPp), ℓ (gLl) and n (gNn) of the base, kPushS pushes the record-product parameters of kronU (b = 2p + ℓ + 3, r = 2^ℓ, ρ = ℓ) on 50 … 55, N = 2^n on vRH, 2 N r on vT and 0 on vZ; kPopS removes them. kronS_runs: on N records zf over zg (both disk records at scale 2^p), the stage leaves kmulN r p ℓ N zf zg, which stores zipWith (ppq r p) xf xg (again disk records, p + 1-bit).

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.