HvdH machine lemma GL.loop21 (Generic element-stream loops (Gaussian list primitives, part 1))

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

theorem NLogN.GL.loop21 (M : MulSpec) (b : RM) (A1 A2 B c dB : Fin HS) (e1 : α → List Item)
    (e2 : α2 → List Item) (d : β → List Item) (f : α → α2 → β) (s : IState HS) (L1 : List α)
    (L2 : List α2) (R1 R2 : List Item) (C N Bc : ℕ) (n : Ex HS)
    (hd : [A1, A2, B, dB, c].Nodup) (h1 : s.G A1 = L1.flatMap e1 ++ R1)
    (h2 : s.G A2 = L2.flatMap e2 ++ R2) (hl1 : L1.length = N) (hl2 : L2.length = N)
    (hn : n.eval s = N) (hw : c ∉ b.writes)
    (hb : ∀ x ∈ L1, ∀ y ∈ L2, ∀ (t : IState HS) (r1 r2 o : List Item),
      (∀ j, j ∉ [A1, A2, B, dB, c] → t.G j = s.G j) →
      t.G A1 = e1 x ++ r1 → t.G A2 = e2 y ++ r2 → t.G B = o ++ s.G B →
      b.run t = ((t.upd A1 r1).upd A2 r2).upd B ((d (f x y)).reverse ++ t.G B) ∧ b.ok M t ∧
        b.cost M t ≤ C)
    (hc56 : c.val < 56) (hnc : n.Clean) (hno : n.ok s) (hnl : n.Lin) (hnB : n.Bnd s Bc) :
    (RM.rep c n b).run s = ((s.upd A1 R1).upd A2 R2).upd B
      (((List.zipWith f L1 L2).flatMap d).reverse ++ s.G B) ∧
    (RM.rep c n b).ok M s ∧
    (RM.rep c n b).cost M s ≤ (n.size + 1) * 2000 * (Bc + 2) +
      N * (C + 8000 * (Bc + 2) + 30) + 32

Context. The lemma belongs to the part Generic element-stream loops (Gaussian list primitives, part 1): RM.rep c n b where the body b pops one element from each of the input stacks A1, A2 and pushes the (reversed) encodings of two results onto B1, B2. After N rounds the outputs are the reversed flattened encodings of the zipWith lists. The wrappers loop11, loop21, loop12 are the one/two-input, one/two-output special cases.

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