HvdH machine lemma GL.roundP_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.roundP_all (M : MulSpec) {m Φm : ℕ} (hM : MulBnd M m Φm) (cN : Fin HS) (hcN : IsCnt cN)
    (S2 : ℤ) (c p Q N : ℕ) (s : IState HS) (Y : List (ℤ × ℤ)) (R LN LQ LC LP LR : List Item)
    (hY : s.G gD = gints Y ++ R) (hl : Y.length = N) (hN : s.G cN = .int N :: LN)
    (hQ' : s.G gPQ = .int S2 :: LQ) (hC : s.G gPC = .int (2 ^ (c + 1)) :: LC)
    (hP : s.G gPP = .int (2 ^ p) :: LP) (hR : s.G gPR = .int (2 ^ (p + 1)) :: LR)
    (hYb : GB m Y) (hS : zsz S2 ≤ m) (hBQ : 2 * m + c + p + 6 ≤ Q)
    (hNQ : zsz ((2 * N : ℕ) : ℤ) ≤ Q) :
    (roundP cN).run s = s.upd gD (ints (Y.map (rndF S2 c p)) ++ R) ∧
    (roundP cN).ok M s ∧
    (roundP cN).cost M s ≤ N * (Φm + 200000 * (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|$.