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

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

theorem NLogN.Rsp.row1P_all (T RK : Fin HS) (hd : TDist T TCI TCK TRI RK) (hTR : T ≠ TRI) (hRR : RK ≠ TRI)
    (wP : RS) (s0 : IState HS) (NK : ℕ) (wf : ℕ → ℕ → ℤ) (Cw : ℕ)
    (hw : WSpec wP T TCI TCK (s0.upd TRI (.int 1 :: s0.G TRI)) 1 NK wf Cw) (LK : List Item)
    (hRK : s0.G RK = .int (NK : ℤ) :: LK) :
    (row1P T RK wP).ok s0 ∧
      (row1P T RK wP).run s0 = s0.upd T (ints ((List.range NK).map (wf 0)) ++ s0.G T) ∧
      (row1P T RK wP).cost s0 ≤ tabCost 1 NK Cw + 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|$.