The uniform record product (recI_runs with the sizes read from kc … kD)

The uniform record product (recI_runs with the sizes read from kc … kD).

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

theorem NLogN.KFV.recU_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b r p ρ φ : ℕ} (hΦ : ∀ x y : ℤ, zsz x ≤ b * r + 2 → zsz y ≤ b * r + 2 → M.Φ x y ≤ φ)
    (hb : 1 ≤ b) (hr : 1 ≤ r) (hbig : 2 * r * 2 ^ (2 * p) < 2 ^ (b - 1))
    (s : IState HS) (f : Fin HS → List ℤ) (zx zy : List GI) (lx ly : List ℤ)
    (hX : f NLogN.KFV.vX = gflat zx ++ lx) (hY : f NLogN.KFV.vY = gflat zy ++ ly) (hlx : zx.length = r)
    (hly : zy.length = r)
    (hzx : ∀ z ∈ zx, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p) (hzy : ∀ z ∈ zy, |z.1| ≤ 2 ^ p ∧ |z.2| ≤ 2 ^ p)
    (hT : Tmp f)
    (hP : PV (πr (2 ^ p) (kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ (p + ρ))) s)
    (hF : PZ (πr (2 ^ p) (kG b r (2 ^ p)) b r ((2 ^ b) ^ (2 * r)) (2 ^ (p + ρ))) f) :
    IRuns I iprog (recU pM) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update (Function.update (Function.update f NLogN.KFV.vX lx) NLogN.KFV.vY ly) vO
        ((gflat (kmul r p ρ zx zy)).reverse ++ f vO)))
      (2000 * cRec r p b (p + ρ) φ)

Context. The lemma belongs to the part KFV §14: the uniform record product recU.

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.