The radix sort: A passes

The radix sort: A passes.

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

theorem NLogN.KFL.radix_fsp {B Bb W A : ℕ} (hB2 : 2 ≤ Bb) (hW : ∀ n : ℕ, n ≤ W → zsz (n : ℤ) ≤ Bb)
    (hA : A ≤ W) (s : IState HS) (G : Fin HS → List ℤ) (E : List Ent)
    (hE : ∀ e ∈ E, e.2.length = B ∧ Bnd 1 e.2 ∧ e.1 ≤ W) (hEW : (E.length + 1) * (B + 1) ≤ W)
    {kk0 kb0 lnb : List ℤ} (hK : G sKK = E.map (kh 0) ++ kk0) (hB : G sKB = E.flatMap Prod.snd ++ kb0)
    (h1K : G sZ1K = []) (h1B : G sZ1B = []) (h0K : G sZ0K = []) (h0B : G sZ0B = [])
    (hc3 : G c3 = []) (hc2 : G c2 = []) (hN : G rNB = (E.length : ℤ) :: lnb) :
    FSp (radixProg B A) (encK s G) (encK s (Function.update (Function.update G
      sKK ((rsort A E).map (kh A) ++ kk0)) sKB ((rsort A E).flatMap Prod.snd ++ kb0)))
      (cLp A (cPass B E.length Bb) Bb)

Context. The lemma belongs to the part KFL §13: the correction, the radix sort on the stacks: The extracted entries E (keys on sKK, records on sKB, entry 0 on top) are sorted by A LSD passes. A pass pops every entry and pushes it on the bucket of its low key bit (sZ0K/sZ0B or sZ1K/sZ1B, the key halved), then moves bucket 0 and then bucket 1 back: the result is rpass i E (passB_fsp). radix_fsp: A passes give rsort A E. All per-entry work is linear in the word size (Sp.push, Sp.asg on linear expressions).

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.