HvdH machine lemma Rsp.bandP_okc (Banded multiply–accumulate: rounds and the whole program (ok and cost))

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

theorem NLogN.Rsp.bandP_okc (M : MulSpec) (m Φ B sh dmax : ℕ) (hM : MulBnd M m Φ) (s : IState HS) (R : ℤ)
    (Xl : List ℤ) (Dl : List ℕ) (Ws : List (List ℤ))
    (acc : List ℤ) (RX RW RD RA LR LN LNR LNW : List Item) (n NR : ℕ)
    (hWs : Ws.length = NR) (hWr : ∀ W ∈ Ws, W.length = n) (hDl : Dl.length = n)
    (hal : acc.length = n) (hXl : NLogN.Rsp.pre Dl n + NR ≤ Xl.length)
    (hR : s.G BR = .int R :: LR) (hN : s.G BN = .int n :: LN) (hNR : s.G BNR = .int NR :: LNR)
    (hNW : s.G BNW = .int (n * NR : ℕ) :: LNW)
    (hX : s.G NLogN.Rsp.BX = ints Xl ++ RX) (hW : s.G NLogN.Rsp.BW = ints Ws.flatten ++ RW)
    (hD : s.G BD = ints (Dl.map (Nat.cast : ℕ → ℤ)) ++ RD) (hA : s.G BA = ints acc ++ RA)
    (hRsh : R = 2 ^ sh)
    (hXB : ∀ y ∈ Xl, zsz y ≤ m) (hWB : ∀ W ∈ Ws, ∀ y ∈ W, zsz y ≤ m)
    (hAB : ∀ j ≤ NR, ∀ y ∈ bandF R Dl (Ws.take j) Xl acc, zsz y ≤ B)
    (hmB : 2 * m ≤ B) (hLB : zsz (Xl.length : ℤ) ≤ B) (hsh : sh + 1 ≤ B)
    (hnB : zsz ((n * NR : ℕ) : ℤ) ≤ B) (hn1 : zsz (n : ℤ) ≤ B) (hdm : ∀ d ∈ Dl, d ≤ dmax) :
    bandP.ok M s ∧ bandP.cost M s ≤ bandCost n NR m Φ B dmax Xl.length

Context. The lemma belongs to the part Banded multiply–accumulate: rounds and the whole program (ok and cost).

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|$.