topQ (KFW C-layer 5: core registers, level frames, the top kernels)

The following holds (Lean statement, in the scope of module Solutions.KFWC5):

theorem NLogN.KFW.topQ (jT jL : Fin Pp) (rowC : IStmt HS Pp) (hT : tbl jT = NLogN.KFW.topC jT jL)
    (hL : tbl jL = levC jL rowC) {K S r H P D ρ k q0 Bp Z Zr : ℕ} {c0 : ℝ}
    (L0 : LvQ Isym tbl jL rowC K r Z Zr H 0 c0) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hq : q0 ≤ D) (hZ16 : zsz ((16 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hV : zsz ((Vb K (K * D) S r H 0 P : ℕ) : ℤ) ≤ Zr)
    (Mb Bz : ℕ) (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + 2 ≤ Mb) :
    ∀ (d i : ℕ) (σ : Fin HS → Option ℤ), CoreR σ K S r H P D ρ k q0 Bp → σ 11 = some (i : ℤ) →
      i + d = q0 →
      SImplQ Isym tbl (fun s => Agree σ s) 0 H r (fun x : Fin D => KFH.stT K D S ρ x)
        (P * 2 ^ (K * D) * S)
        (tensF fun x : Fin D => if i ≤ x.val ∧ x.val < q0 then Cm else 1) (.call jT) d (2 * d)
        (fun _ => d * (⌊c0 * ((P * 2 ^ (K * D) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ + cTopO Bz) +
          cTopE Bz)

Context. The lemma belongs to the part KFW C-layer 5: core registers, level frames, the top kernels.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.