HvdH machine lemma GL.zipP_all (Gaussian list primitives, part 3: moves, transfers, the zip product pr)

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

theorem NLogN.GL.zipP_all (M : MulSpec) {m Φm : ℕ} (hM : MulBnd M m Φm) (σ : Sg) (cN : Fin HS)
    (hcN : IsCnt cN) (p Q N : ℕ) (s : IState HS) (A U : List (ℤ × ℤ)) (R1 R2 LN LP : List Item)
    (hA : s.G gZA = gints A ++ R1) (hU : s.G gD = gints U ++ R2) (hlA : A.length = N)
    (hlU : U.length = N) (hN : s.G cN = .int N :: LN) (hP : s.G gPP = .int (2 ^ p) :: LP)
    (hAb : GB m A) (hUb : GB m U) (hmQ : 2 * m + 1 ≤ Q) (hpQ : p + 1 ≤ Q)
    (hNQ : zsz ((2 * N : ℕ) : ℤ) ≤ Q) :
    (zipP σ cN).run s = (s.upd gZA R1).upd gD (gints (List.zipWith (gzF σ p) A U) ++ R2) ∧
    (zipP σ cN).ok M s ∧
    (zipP σ cN).cost M s ≤ N * (4 * Φm + 200000 * (Q + 2)) + 20000 * (Q + 2)

Context. The lemma belongs to the part Gaussian list primitives, part 3: moves, transfers, the zip product program: * mv_all: mvList as an RM step (run / ok / cost in one statement).

• xferP i j n: move n integers from i to j keeping their order (via gZT).
• zipP σ cN: gD := zipWith (gzF σ p) A U (A consumed from gZA), cN ∈ {gPN, gPM} holds the length.

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