The cost of `fwWrap`

The cost of fwWrap. -/ def fwWCost (q : Ref.Params) (kb Φm : ℕ) : ℕ := fwCost q kb Φm + 10 ^ 6 * (2 ^ q.logOuter * q.r + 1) * (fwW2 q kb + 2) + 10 ^ 6 * (q.K + 1) * (fwW q kb + 2) /-! ## The main specification

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

theorem NLogN.FWW.fwWrap_spec (M : MulSpec) {Φm : ℕ} (q : Ref.Params) (kb : ℕ)
    (hMB : MulBnd M (q.fn + 1) Φm)
    (hP : 1 ≤ q.P) (hK : q.K ≤ q.fn) (hlo : q.logOuter ≤ q.fn) (hkb : q.logOuter ≤ kb)
    (s : IState HS) (hC : FwCtx q kb s) (U V : List (ℤ × ℤ)) (R1 R2 : List Item)
    (hPre : FwPre q U V) (hU : s.G wI1 = gints U ++ R1) (hV : s.G wI2 = gints V ++ R2) :
    Spec M fwWrap s (((s.upd wI1 R1).upd wI2 R2).upd wO (gints (Ref.fermatW q U V) ++ s.G wO))
      (fwWCost q kb Φm)

Context. The lemma belongs to the part Wrapping the Fermat convolution fwP as an abstract LProg2 (part 1).

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