HvdH machine lemma pAttachP_cost (Permuting a list of records by a list of target indices)

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

theorem NLogN.pAttachP_cost (d n : ℕ) (Kl : List ℕ) (D : List (List ℤ)) (Rest RK : List Item)
    (s : IState HS) (hKl : Kl.length = n) (hK : ∀ k ∈ Kl, k < n) (hD : D.length = n)
    (hDw : ∀ r ∈ D, r.length = d)
    (L1 : List Item) (h0 : s.G 0 = ints D.flatten ++ Rest) (h1 : s.G 1 = .int n :: L1)
    (h3 : s.G 3 = natInts Kl ++ RK) (X : ℕ)
    (hDB : ∀ r ∈ D, Bnd X r) (hX2 : zsz ((n * (d + 1) : ℕ) : ℤ) ≤ X)
    (hXd : zsz ((d + 1 : ℕ) : ℤ) ≤ X) :
    (pAttachP d).cost s ≤ 100000 * (n + 1) * (d + 1) * (X + 2)

Context. The lemma belongs to the part Permuting a list of records by a list of target indices: Stack 0 holds n records of d integers, n is on 1, the number of key bits kb (n ≤ 2^kb) on 2, and stack 3 holds the target indices Kl (a permutation of 0, …, n-1). permP d moves record p to position Kl[p]; the index list on 3 is restored. Scratch: 40, 41, 43, 45, 51, 54 and those of sortP.

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