rev_spec (KFU §6: the axis reversal)

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

theorem NLogN.KFU.rev_spec {q' : ℕ} {K : ℝ} (hK : SwOK q' K) (hK0 : 0 ≤ K) (mz : ℕ → ℕ) (bg : ℕ → Bool)
    (hmz : ∀ j, 1 ≤ mz j) (u : ℕ) (hu : 1 ≤ u) (L : List ℕ) (cid : ℕ)
    (hL : ∀ j ∈ L, mz j = 2 ^ u) (hcid : bg cid = false) (hnd : (L ++ [cid]).Nodup)
    (w : ℕ) (xs0 : List ℤ) (hx : Bnd w xs0) (hxs : xs0.length = vol ((L ++ [cid]).map (tz mz bg)))
    (I : List Sym) (t : IState HS) (R : List Item) (h0 : t.G 0 = ints xs0 ++ R) :
    ∃ c : ℕ, IRuns I KFL.l12prog (revC q' w u mz bg L cid) t
      (t.upd 0 (ints (AModel.pull ((L ++ [cid]).map (tz mz bg)) ((L.reverse ++ [cid]).map (tz mz bg))
        (revH L.length) 0 xs0) ++ R)) c ∧
      (c : ℝ) ≤ 3 * (L.length + 1) * (NLogN.KFU.cMv (vol ((L ++ [cid]).map (tz mz bg))) w + 1 +
        K * ((w : ℝ) + 1) * ((vol ((L ++ [cid]).map (tz mz bg)) : ℝ) + 1) * (u : ℝ) ^ KFS.τS)

Context. The lemma belongs to the part KFU §6: the axis reversal.

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.