natCost_le (KFUU §9d: absorbing the costs of `Φ` into `cPhiU`)

The following holds (Lean statement, in the scope of module Solutions.KFUUAbs):

theorem NLogN.KFUU.natCost_le (w h d VT VS PM : ℕ) (hd : 2 ^ (d + 1) ≤ VT) (hST : VS ≤ VT) (hS2 : 2 ≤ VS)
    (hP1 : 1 ≤ PM) (hPS : PM ≤ VS) (hd0 : d = 0 → PM = 1) :
    natCost w d VT VS PM (w + h + 3 * d + zsz (VS : ℤ) + 3) (zsz (VT : ℤ) + w + h + 3)
        (zsz ((2 * VS : ℕ) : ℤ) + d) (zsz ((2 * VS : ℕ) : ℤ)) ≤
      C1 * ((d + 1) * cScan VT w + (d + 1) * (h + w + Nat.size VS + 1) ^ 2 +
        d * cRb d w VS PM (zsz ((2 * VS : ℕ) : ℤ)))

Context. The lemma belongs to the part KFUU §9d: absorbing the costs of Φ into cPhiU: With L = size V_T (V_T ≥ 2^{d+1}, so d + 2 ≤ L and L^4 ≤ 64 V_T), every bit-size quantity of the setup, the table and the multiplications is polylogarithmic in V_T, or is covered by the descriptor term (d+1)(h + w + size V_S + 1)^2.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.