HvdH machine lemma BD.Bq_size (Crude magnitude bounds, part 3: the parameters `mkParams K N`)

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

theorem NLogN.BD.Bq_size (K N : ℕ) (hK : 20 ≤ K) (hN : 2 ^ (2 ^ (8 * K) + 1) ≤ N) :
    Nat.size (Bq (mkParams K N)) ≤ (mkParams K N).p + (mkParams K N).p / 8

Context. The lemma belongs to the part Crude magnitude bounds, part 3: the parameters mkParams K N: * copS_upper: 4K sᵢ ≤ (4K-1) tᵢ for the source lengths of mkParams (direct from copS).

• jIter_le: then jIter ≤ 4Kp/α² + 1 = Jm q, i.e. HJ (mkParams K N).
• Bq q = 2 · max(2^p, BW q) · cSq q ^ K, and for K ≥ 20, N ≥ 2^(2^(8K)+1): Bq_size: Nat.size (Bq q) ≤ p + p/8 and Bq_lt: Bq q < 2^P.
• refStep_LB_mkParams: every intermediate list of refStep (mkParams K N) x y is bounded by Bq, except the raw fermatW outputs which are bounded by 2^P (structurally).

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