dropR_sp (KFUU §8e: clearing registers and lists)

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

theorem NLogN.KFUU.dropR_sp {X C : Fin HS} (hXC : X ≠ C) (hX5 : X.val < 56) (hC5 : C.val < 56)
    (s : IState HS) (f : Fin HS → List ℤ) (L l : List ℤ) (hfX : f X = L ++ l) (hfC : f C = [])
    (n : Ex HS) (hnc : n.Clean) (hno : n.ok (NLogN.KIL.encK s f)) (hnl : n.Lin) (Bb : ℕ)
    (hnb : n.Bnd (NLogN.KIL.encK s f) Bb) (hn : n.eval (NLogN.KIL.encK s f) = L.length) (hL : Bnd Bb L) :
    Sp (dropR X C n) (NLogN.KIL.encK s f) (NLogN.KIL.encK s (Function.update f X l))
      ((n.size + 1) * 2000 * (Bb + 2) + L.length * ((2 * Bb + 2) + 8000 * (Bb + 2) + 30) + 32)

Context. The lemma belongs to the part KFUU §8e: clearing registers and lists.

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.