HvdH machine lemma Rsp.cDelP_all (Table builders for `bapP`)

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

theorem NLogN.Rsp.cDelP_all (s0 : IState HS) (s t Bq : ℕ) (LS LT : List Item) (hs : 0 < s)
    (hS : s0.G TS = .int (s : ℤ) :: LS) (hT : s0.G NLogN.Rsp.TT = .int (t : ℤ) :: LT)
    (hBq : 4 * (s + t + 2) ^ 2 < 2 ^ Bq) :
    cDelP.ok s0 ∧
      cDelP.run s0 = s0.upd D1 (ints ((cDel s t).map (Nat.cast : ℕ → ℤ)) ++ s0.G D1) ∧
      cDelP.cost s0 ≤ tabCost 1 s ((cDelE.size + 1) * 10 ^ 7 * (Bq + 2) ^ 2) + 10 ^ 9

Context. The lemma belongs to the part Table builders for bapP: One-row tables built by row1P T RK wP (TRI := 1 pushed, tabP, popped), with a single-push weight program push T e:

• cTabP : ints (cTab s).flatten (all ones) on W1;
• eDelP : ints (eDel s) on BD;
• cDelP : ints (cDel s t) on D1;
• psKeysP : natInts (psKeys s t) on KS;
• ptKeysP : natInts (ptKeys s t) on 3 (needs TU = (s⁻¹ mod t)). Scalars: TS = s, TT = t, TU; 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|$.