unzP_fsp (KFV §10: the four register loops of one Kronecker record product)

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

theorem NLogN.KFV.unzP_fsp {X SA SB C : Fin HS} (h1 : X ≠ SA) (h2 : X ≠ SB) (h3 : X ≠ C) (h4 : SA ≠ SB)
    (h5 : SA ≠ C) (h6 : SB ≠ C) (hX5 : X.val < 56) (hA5 : SA.val < 56) (hB5 : SB.val < 56)
    (hC5 : C.val < 56) (s : IState HS) (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (c : ℤ)
    (w Bb : ℕ) (hX : f X = gflat zs ++ l) (hC : f C = [])
    (hw : ∀ z ∈ zs, zsz z.1 ≤ w ∧ zsz z.2 ≤ w ∧ zsz (z.1 + c) ≤ w ∧ zsz (z.2 + c) ≤ w)
    (hc : zsz c ≤ w) (hn : zsz (zs.length : ℤ) ≤ Bb) :
    FSp (unzP X SA SB C c zs.length) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update (Function.update (Function.update f X l) SA
        ((gflat (zs.map (offG c))).reverse ++ f SA)) SB
        ((gflat (zs.map (fun z => offG c z.swap))).reverse ++ f SB)))
      (cLp zs.length (30000 * (w + 2)) Bb)

Context. The lemma belongs to the part KFV §10: the four register loops of one Kronecker 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.