The middle part (round six, `midQ`)

The middle part.

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

theorem IntMul.Kappa.R6.IL3H.midQ {c : IntMul.Kappa.R6.IL3H.Cfg} (jL : Fin Pp) (rowC : IStmt HS Pp)
    (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp qB Z Zf Zr G : ℕ} {CB : ℕ → ℝ}
    (LV : LvH c Isym tbl jL rowC K r Z Zr H G CB (D - q0 - qB))
    (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r) (hlt : q0 + qB < D)
    (hBpP : P * 2 ^ (K * q0) ≤ Bp) (hBp2 : Bp ≤ 2 * (P * 2 ^ (K * q0)))
    (hdvd : c.W ^ dep c.m (D - q0 - qB) * 2 ^ (2 * (((D - q0 - qB) / c.m - 1) * G)) ∣ Bp)
    (hSd : ((D - q0 - qB) / c.m - 1) * G ≤ K * qB)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hZf : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zf)
    (hHf : zsz (H : ℤ) ≤ Zf) (hGH : c.G (D - q0 - qB) ≤ H)
    (hV : zsz ((VbH c K (K * (D - q0 - qB)) (S * 2 ^ (K * qB)) r H (D - q0 - qB)
      (ρ + K * (D - q0 - qB - 1)) Bp : ℕ) : ℤ) ≤ Zr)
    {σ : Fin HS → Option ℤ} (hC : CoreR σ K S r H P D ρ 0 q0 Bp) (hG : σ vG = some (G : ℤ))
    (h14 : σ 14 = some (qB : ℤ)) (h15 : σ 15 = some ((c.G (D - q0 - qB) : ℕ) : ℤ)) :
    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 q0 ≤ x.val ∧ x.val < q0 + (D - q0 - qB) then Cm else 1)
      (midPart jL) (c.G (D - q0 - qB)) ((c.Wr + 4) * c.G (D - q0 - qB))
      (IntMul.Kappa.R6.IL3H.cMid (P * 2 ^ (K * D) * S) (Bp * 2 ^ (K * (D - q0)) * S) r Zf
        ((c.Wr + 4) * c.G (D - q0 - qB))
        ⌊CB (D - q0 - qB) * ((Bp * 2 ^ (K * (D - q0)) * S * Yu r Zr H : ℕ) : ℝ)⌋₊)

Context. Round six, item language (I3): the middle part of the C-layer

With the core registers (q₀ on 28, D - q₀ on 29, B' on 20), qB on 14 and Gs D'' on 15 (D'' = D - q₀ - qB ≥ 1), midPart jL pads the layer from P 2^{K q₀} to B' blocks (padCU with the frozen frame padE) and runs the level procedure on the D'' bits q₀ ≤ x < q₀ + D'' of the padded layout (level frame midE: t = K D'', S₀ = S 2^{K qB}, E = D'', e = ρ + K (D'' - 1), B = B', Gs D'').

midQ: midPart jL implements tens Cm on those bits, scale Gs D'', width (W'+4) Gs D''.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).