extI_runs (KFV §10: packing, the four ring products, and the extraction of one record produ)

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

theorem NLogN.KFV.extI_runs {e : Ex HS} {O : Fin HS} (hO : O = vOR ∨ O = vOI) {b r Δ Bz Bb : ℕ}
    (hb : 1 ≤ b) (s : IState HS) (f : Fin HS → List ℤ) (d : ℤ) (h : ℕ → ℤ)
    (hec : e.Clean) (hel : e.Lin) (heo : e.ok (NLogN.KIL.encK s f)) (hev : e.eval (NLogN.KIL.encK s f) = d)
    (heb : e.Bnd (NLogN.KIL.encK s f) Bz)
    (hhb : ∀ j < 2 * r, -(2 : ℤ) ^ (b - 1) ≤ h j ∧ h j < 2 ^ (b - 1))
    (hd : d = ∑ j ∈ Finset.range (2 * r), h j * (2 ^ b : ℤ) ^ j)
    (hBz : b * (2 * r) + 2 ≤ Bz) (hBb : zsz ((2 * r : ℕ) : ℤ) ≤ Bb)
    (fZ : f vZ = []) (fX : f tX = []) (fR : f vRH = []) (fT : f NLogN.KFV.vT = []) (fT2 : f vT2 = [])
    (fT4 : f vT4 = []) (fL : f NLogN.KFV.vL = []) :
    IRuns I iprog (extI e O b r Δ) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update f O (((List.range r).map fun j => fdt Δ (h j) (h (j + r))) ++ f O)))
      (cExt e.size r b Δ Bz Bb)

Context. The lemma belongs to the part KFV §10: packing, the four ring products, and the extraction of one record product.

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.