sort_moved (KFL §11: the list model of the radix sort)

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

theorem NLogN.KFL.sort_moved (hγκ : ∀ m, γ (κ m) = m) (hκγ : ∀ m, κ (γ m) = m)
    (hκ : ∀ m < M, κ m < M) (hγ : ∀ m < M, γ m < M) {A : ℕ} (hA : M ≤ 2 ^ A)
    (recs : ℕ → List ℤ) : rsort A (ent0 κ M recs) = ent1 κ γ M recs

Context. The lemma belongs to the part KFL §11: the list model of the radix sort: Entries are pairs (key, record). rpass i is one stable LSD pass on bit i, ones first (this is what two stacks give: the 0-bucket is moved back first, the 1-bucket on top of it); rsort A runs the passes 0, …, A-1. rsort_eq: with keys below 2^A and distinct, the result is the unique list sorted by strictly decreasing key.

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.