HvdH machine lemma ST.midP_spec (The recursive step, part 8: `csP`, the descriptor bounds, `innerP`)

The following holds (Lean statement, in the scope of module NLogN.HSt8):

theorem NLogN.ST.midP_spec (M : MulSpec) {kb Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu : ℕ} {BS BB : ℕ → ℕ}
    (q : Params) (u v : List ℤ)
    (hA : ExArgs M q kb Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu BS BB u v) (t : IState HS)
    (R1 R41 L17 L37 L5 L6 L7 L9 L39 L26 : List Item) (h1 : t.G 1 = .int (q.S : ℤ) :: R1)
    (h17 : t.G 17 = .int (q.p : ℤ) :: L17) (h37 : t.G 37 = .int (q.logT : ℤ) :: L37)
    (h5 : t.G 5 = .int ((2 ^ q.e : ℕ) : ℤ) :: L5) (h6 : t.G 6 = .int ((2 ^ (q.e - 1) : ℕ) : ℤ) :: L6)
    (h7 : t.G 7 = .int ((q.K - q.dh : ℕ) : ℤ) :: L7) (h9 : t.G 9 = .int (EX.TT q : ℤ) :: L9)
    (h39 : t.G 39 = .int (q.logOuter : ℤ) :: L39) (h26 : t.G 26 = .int (q.fn : ℤ) :: L26)
    (h31 : ∃ L, t.G 31 = .int ((2 ^ q.b : ℕ) : ℤ) :: L) (h42 : ∃ L, t.G 42 = .int (q.α : ℤ) :: L)
    (h2 : ∃ L, t.G 2 = .int (kb : ℤ) :: L) (h44 : ∃ L, t.G 44 = .int (q.P : ℤ) :: L)
    (h41 : t.G 41 = ints (EX.sl q).reverse ++ R41)
    (R RV : List Item) (hu : t.G 0 = ints u ++ R) (hv : t.G 30 = ints v ++ RV)
    (hch : ∃ RC, t.G 28 = gints (chirpL q) ++ RC)
    (he : 2 ≤ q.e) (hdh : q.dh < q.K) (B : ℕ)
    (hB : 2 * q.fn + q.logOuter + q.e + 2 * q.K + 4 ≤ B) (hpB : q.p * q.p + q.p + 2 < 2 ^ B)
    (hKB : 8 * q.K < 2 ^ B) (hSB : zsz (q.S : ℤ) ≤ B) (hslB : Bnd B (EX.sl q))
    (hTB : EX.TT q < 2 ^ B) (hlTB : q.logT + 1 ≤ B) :
    Spec M (midP q.K) t (((t.upd 30 RV).upd 0 (ints (exactConvL q u v) ++ R)).upd 41 R41)
      (midPCost q kb Bs CS CB Bx Q Φf Φm B)

Context. The lemma belongs to the part The recursive step, part 8: csP, the descriptor bounds, innerP.

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.