HvdH machine lemma GL.scaleP_all (Gaussian list primitives, part 4: scaling, `tdiv`, rounding, copying)

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

theorem NLogN.GL.scaleP_all (M : MulSpec) (cN : Fin HS) (hcN : IsCnt cN) (k m Q N : ℕ) (s : IState HS)
    (u : List ℤ) (R LN LS : List Item) (hU : s.G gD = ints u ++ R) (hl : u.length = N)
    (hN : s.G cN = .int N :: LN) (hS : s.G gPS = .int (2 ^ k) :: LS)
    (hub : ∀ x ∈ u, zsz x ≤ m) (hQ : m + k + 1 ≤ Q) (hNQ : zsz ((2 * N : ℕ) : ℤ) ≤ Q) :
    (scaleP cN).run s = s.upd gD (gints (u.map (scaleF k)) ++ R) ∧
    (scaleP cN).ok M s ∧
    (scaleP cN).cost M s ≤ N * 100000 * (Q + 2) + 20000 * (Q + 2)

Context. The lemma belongs to the part Gaussian list primitives, part 4: scaling, tdiv, rounding, copying: * scaleP cN: gD : ints u ++ R ↦ gints (u.map (a ↦ (a·2^k, 0))) ++ R (gPS = 2^k).

• tdivP cN: gD : gints W ++ R ↦ gints (W.map (z ↦ (z₁ tdiv 2^k, z₂ tdiv 2^k))) ++ R (gPT = 2^k).
• roundP cN: gD : gints Y ++ R ↦ ints (Y.map rnd) ++ R with rnd z = (S²·z₁·2^(c+1) + 2^p) / 2^(p+1) (floor division; gPQ = S², gPC = 2^(c+1), gPP = 2^p, gPR = 2^(p+1)); one multiplication call per element.
• copyP cN: gCH : gints A ++ R ↦ gints A ++ R and gZA : X ↦ gints A ++ X.

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