Round-six lemma `rotU_runs`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem NLogN.KFX.rotU_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
    {K ρ f : ℕ} (hK : 1 ≤ K) (hρK : ρ < K) (hf : 1 ≤ f) {d0 d1 : ℕ}
    (hd0 : 0 < d0) (hd1 : 0 < d1) (l : Line) (hs : l.sgn = 1 ∨ l.sgn = -1)
    (hb : l.b = 0 ∨ l.b = 1) {Bb : ℕ} (hB2 : 2 ≤ Bb) (hbig : 4 * 2 ^ (f * K) < 2 ^ Bb)
    (zd0 : zsz (d0 : ℤ) ≤ Bb) (zd1 : zsz (d1 : ℤ) ≤ Bb)
    (P B w : ℕ) (zP : zsz (P : ℤ) ≤ Bb)
    (t : IState HS) (xs : List ℤ) (R : List Item) (hlen : xs.length = P * 2 ^ (f * K) * B)
    (hbw : Bnd w xs) (h0 : t.G 0 = ints xs ++ R)
    {eP eQ eB ed0 ed1 er ef eK : Ex HS}
    (hsz : ((rotPl eP eQ eB ed0 ed1 er ef eK).map fun p => p.2.size + 1).sum ≤ 100)
    (n1 : NoLow eP) (n2 : NoLow eQ) (n3 : NoLow eB) (n4 : NoLow ed0) (n5 : NoLow ed1)
    (n6 : NoLow er) (n7 : NoLow ef) (n8 : NoLow eK)
    (E1 : ESp eP t Bb (P : ℤ)) (E2 : ESp eQ t Bb ((2 ^ (f * K) : ℕ) : ℤ)) (E3 : ESp eB t Bb (B : ℤ))
    (E4 : ESp ed0 t Bb (d0 : ℤ)) (E5 : ESp ed1 t Bb (d1 : ℤ)) (E6 : ESp er t Bb ((2 : ℤ) ^ ρ))
    (E7 : ESp ef t Bb ((f - 1 : ℕ) : ℤ)) (E8 : ESp eK t Bb ((2 : ℤ) ^ K)) :
    IRuns I iprog (rotU l.sgn l.b eP eQ eB ed0 ed1 er ef eK) t
      (t.upd 0 (ints (pull [P, 2 ^ (f * K), B] [P, 2 ^ (f * K), B]
        (KIL.rotAddr (2 ^ (f * K)) (tabA K ρ f d0 d1 (2 ^ (f * K)) l)) 0 xs) ++ R))
      (cRotU K f l.b P (2 ^ (f * K)) B w Bb)

Context. KFX §2: register-driven table rotations (the lines (22) and the last bit)

• pushSt_G_mem, pushOK_of: pushed parameter lists built from KFL.ESp facts.
• tabRot_runs: a generic withPushI pl (fcode U ; rotF) where U pushes the rotation table.
• tabGenU sgn b: KFL.tabGen with the literals P, Q, d0, d1, 2^ρ, f-1, 2^K read from the registers 1, 2, 3, 5, 6, 7, 8 (tabGenU_sub: the literal instance is RS.sub).
• rotU_geo: one line rixT g (rot2 Q (amt K ρ f l)) with parameters from expressions.
• xorGenU, xorU_geo: the last-bit step rixT g (XLc K ρ f).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).