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

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

theorem NLogN.GL.loop11 (M : MulSpec) (b : RM) (A B c dA dB : Fin HS) (e : α → List Item)
    (d : β → List Item) (f : α → β) (s : IState HS) (L : List α) (R : List Item)
    (C N Bc : ℕ) (n : Ex HS)
    (hd : [A, dA, B, dB, c].Nodup) (h1 : s.G A = L.flatMap e ++ R) (hl : L.length = N)
    (hn : n.eval s = N) (hw : c ∉ b.writes)
    (hb : ∀ x ∈ L, ∀ (t : IState HS) (r o : List Item),
      (∀ j, j ∉ [A, dA, B, dB, c] → t.G j = s.G j) →
      t.G A = e x ++ r → t.G B = o ++ s.G B →
      b.run t = (t.upd A r).upd B ((d (f x)).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 A R).upd B (((L.map f).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|$.