transU_runs (KFUU §11b: the uniform axis rotation `transU`)

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

theorem NLogN.KFUU.transU_runs {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) {eSw : Fin P} {sdS : Fin HS} {K : ℝ}
    (hK : SwOKU I iprog eSw sdS K) (hdS : sdS ≠ 0) {Dsc : Fin HS} (hD : Dsc = 18 ∨ Dsc = 19)
    (hDd : Dsc ≠ sdS) (w h : ℕ) (b0 : Bool) (bt : List Bool) (hh : 1 ≤ h)
    (s : IState HS) (f : Fin HS → List ℤ) (l : List ℤ) (hf : ∀ j, j ≠ 0 → j ≠ dP → f j = [])
    (hfd : f dP = KFM.descTr w h (b0 :: bt)) (zs : List GI) (h0 : f 0 = gflat zs ++ l)
    (hlen : zs.length = vol (shP h (b0 :: bt))) (hgb : NLogN.KFB.GB w zs)
    (B Z : ℕ) (hwB : zsz (w : ℤ) ≤ B) (hhB : h + 1 ≤ B)
    (h2B : zsz ((2 * 2 ^ (h + if b0 then 1 else 0) : ℕ) : ℤ) ≤ B)
    (h2hB : zsz ((2 ^ h * 2 : ℕ) : ℤ) ≤ B)
    (hkB : zsz ((3 + (b0 :: bt).length : ℕ) : ℤ) ≤ B)
    (hZ3 : 3 ≤ Z) (hZV : zsz ((vol (shP h (b0 :: bt)) * 2 : ℕ) : ℤ) ≤ Z) (hwZ : zsz (w : ℤ) ≤ Z)
    (hUZ : zsz ((2 ^ h : ℕ) : ℤ) ≤ Z) :
    IRuns I iprog (transU pM eSw sdS Dsc) (NLogN.KIL.encK s f)
      (NLogN.KIL.encK s (Function.update f 0 (gflat (IntMul.HvdH.Ref.transposeL
        ((shP h (b0 :: bt)).headD 1) (vol (shP h (b0 :: bt)).tail) zs) ++ l)))
      (cTr K w h (b0 :: bt) B Z)

Context. The lemma belongs to the part KFUU §11b: the uniform axis rotation transU: readT reads descTr w h bs = [w, h, k, b_0, …] from dP (restored); mkT builds 2^h, the sizes t_j = 2^{h+b_j} (on pTK and xB), nR = k, rCZ = 2; the first revU reverses all k axes; midT sets rCZ = 2 t_0, the sizes t_{k-1}, …, t_1 on pTR, nR = k - 1; the second revU reverses the first k - 1 axes (inner block 2 t_0); cleanT clears. transU_runs: the result is gflat (transposeL t_0 (V / t_0) zs).

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.