packI_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.packI_runs {S P : Fin HS} (hS0 : S ≠ 0) (hSL : S ≠ NLogN.KFV.vL) (hP0 : P ≠ 0) (hPS : P ≠ S)
    (hS5 : S.val < 56) (hP5 : P.val < 56) {b r w Bp : ℕ} (hb : 1 ≤ b) (KG : ℤ)
    (s : IState HS) (f : Fin HS → List ℤ) (zA : List GI) (lS : List ℤ)
    (hlen : zA.length = r) (hS : f S = (gflat zA).reverse ++ lS) (hL : f NLogN.KFV.vL = [])
    (hre : ∀ z ∈ zA, 0 ≤ z.1) (hw : NLogN.KFB.GB w zA)
    (hB1 : zsz (carOut b zA : ℤ) ≤ Bp) (hB2 : zsz KG ≤ Bp) (hB3 : zsz ((carOut b zA : ℤ) - KG) ≤ Bp)
    (hn : zsz ((2 * r : ℕ) : ℤ) ≤ Bp) (hfok : NLogN.KFD.fok (NLogN.mvK S 0 NLogN.KFV.vL (.lit ((2 * r : ℕ) : ℤ))) = true) :
    IRuns I iprog (packI S P b r KG) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update (Function.update f S lS) P (((carOut b zA : ℤ) - KG) :: f P)))
      (cPack r w b Bp)

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.