HvdH machine lemma Rsp.sWP_wspec (Building the `S` weight table and the step table)

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

theorem NLogN.Rsp.sWP_wspec (s0 : IState HS) (p s t m K2 NI Bq : ℕ) (beta : ℤ)
    (LP LS LT LM LB LK : List Item) (ht : 0 < t) (hNI : NI = 2 * m + 1)
    (hP : s0.G TP = .int (p : ℤ) :: LP) (hS : s0.G TS = .int (s : ℤ) :: LS)
    (hT : s0.G NLogN.Rsp.TT = .int (t : ℤ) :: LT) (hM : s0.G TM = .int (m : ℤ) :: LM)
    (hB : s0.G TBe = .int beta :: LB) (hK : s0.G TK2 = .int (K2 : ℤ) :: LK)
    (hBq : 4 * (s + t + 2 * m + 2) ^ 4 < 2 ^ Bq) (hpB : zsz (p : ℤ) ≤ Bq)
    (hKB : zsz (K2 : ℤ) ≤ Bq) (hbB : zsz beta ≤ Bq)
    (hwB : ∀ j, zsz (beta * HvdH.expNeg p K2 j) ≤ Bq) (hEB : ∀ j, zsz (HvdH.expNeg p K2 j) ≤ Bq) :
    WSpec sWP NLogN.Rsp.BW TCI TCK s0 NI t (sWf p s t m beta K2) (sWCost p Bq)

Context. The lemma belongs to the part Building the S weight table and the step table: sTabP pushes ints (sTab p s t α).flatten on BW; sDelP pushes ints (sDel s t) on BD. Scalar parameters (registers): TP = p, TS = s, TT = t, TM = m = sWidth p α, TBe = betaT p α, TK2 = α² t², TRI = 2m+1; counters TCI, TCK.

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