The correction: flR recs M ↦ flR (recs ∘ corrR) M

The correction: flR recs M ↦ flR (recs ∘ corrR) M.

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

theorem NLogN.KFL.corrRS_fsp {K ρ f : ℕ} (hK : 1 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) {g : Geo} (hg : g.Pos)
    (hQe : g.Q = 2 ^ (f * K)) (recs : ℕ → List ℤ) (hlen : ∀ m, (recs m).length = g.B)
    (hbits : ∀ m, Bnd 1 (recs m)) (s : IState HS) :
    FSp (corrRS K ρ f g (zsz (g.V : ℤ))) (NLogN.KIL.encK s (Function.update (fun _ => []) 0 (flR recs g.recG.V)))
      (NLogN.KIL.encK s (Function.update (fun _ => []) 0 (flR (fun d => recs (corrR K ρ f g d)) g.recG.V)))
      (cCorr K f g (zsz (g.V : ℤ)) (nMv (keyR K ρ f g) g.recG.V) (zsz (g.V : ℤ) + 3))

Context. The lemma belongs to the part KFL §14: the correction, pass 3 (merge) and the whole correction: Pass 3 rebuilds stack 0 from the bottom: for d = M-1, …, 0 it pops the flag of d and moves the top record of sKB (a moved destination: the sorted entries are in decreasing destination order) or of sT (an unmoved record) to stack 0.

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.