phiInv_spec (KFU §9: the runs of `Φ` and `Φ⁻¹`)

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

theorem NLogN.KFU.phiInv_spec {q' : ℕ} {K : ℝ} (hK : SwOK q' K) (hK0 : 0 ≤ K) (w h d : ℕ) (hh : 1 ≤ h)
    (bL : ℕ → Bool) (sF μ : ℕ → ℕ) (hs : ∀ j < d, 1 ≤ sF j) (hst : ∀ j < d, sF j ≤ 2 ^ h)
    (Bb : ℕ) (hBb : zsz ((2 * vol (shR d (sP d sF)) : ℕ) : ℤ) ≤ Bb)
    (I : List Sym) (ys : List ℤ) (hlen : ys.length = vol (shR d (NLogN.KFU.tP d h bL))) (hb : Bnd w ys)
    (t : IState HS) (R : List Item) (h0 : t.G 0 = ints ys ++ R) :
    ∃ c : ℕ, IRuns I KFL.l12prog (phiInvC q' w h d bL sF μ) t
      (t.upd 0 (ints (PhiInvD h d bL sF μ ys) ++ R)) c ∧
      (c : ℝ) ≤ cPhi d w (vol (shR d (NLogN.KFU.tP d h bL))) (vol (shR d (sP d sF)))
        (vol ((List.range (d - 1)).map sF)) Bb K h

Context. The lemma belongs to the part KFU §9: the runs of Φ and Φ⁻¹: phiC (stack 0: ints xs ++ R, xs on S_k = shK (sP)):

1. pad S_k → T_k (d+1 scans),
2. reverse the axes on T_k → T_r (revC, Lemma 12 swaps + bit moves),
3. delete the padding T_r → S_r,
4. the shifts i = d-1, …, 0 (forward coefficients csF),
5. pad S_r → T_r.

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.