The body proper (round six, `bodyCoreQ`)

The body proper (the frozen bodyQ with the round-six C-layer).

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

theorem IntMul.Kappa.R6.IL3H.bodyCoreQ {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K S r H P D ρ q0 Bp qB Zl Z Zr G Mb Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r Zl Zr H G CB 1) (hρ : ρ < K) (hS : 1 ≤ S) (hP : 1 ≤ P)
    (hr : 1 ≤ r) (hD : 1 ≤ D) (hqq : q0 + qB ≤ D)
    (hZl : zsz ((32 * c.Wr * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Zl)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z) (hHZ : zsz (H : ℤ) ≤ Z)
    (hV1 : zsz ((VbH c K (K * D) S r H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr) (hH1 : 1 ≤ H)
    (hMb : zsz (Mb : ℤ) ≤ Bz) (hM : K * D + P + D + S + 10 ≤ Mb)
    (pre : q0 + qB < D → MidPre c Isym tbl jL rowC CB K S r H P D ρ q0 Bp qB Zl Z Zr G)
    (hEZ : zsz ((Etot c D q0 qB : ℕ) : ℤ) ≤ Z)
    {σ : 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) : ℕ) : ℤ))
    (h13 : σ 13 = some ((Etot c D q0 qB : ℕ) : ℤ))
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)) (p w : ℕ)
    (hC0 : Clean0 f) (h0 : f 0 = gflat zs ++ l) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (hb : GB w zs)
    (hH : w + (dwCL c D q0 qB + 2) ≤ H)
    (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1) :
    ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs) ∧
      RunQ Isym tbl σ (bodyCore jK jL) f (Function.update f 0 (gflat zs' ++ l))
        (cBodyC c CB K S r H P D q0 qB Bp Z Zr Bz w)

Context. Round six, item language (I3): the layer body of the uniform Proposition 14

On a core assignment (CoreR at k = 0, G on vG), bodyCH c jK jL pushes

• 14 qB = min(D - q₀, ⌈⌊D/m⌋ G / K⌉) (two natural frames bF1, bF2),
• 15 Gs D'' (D'' = D - q₀ - qB; frame bF3),
• 13 E = q₀ + (qB + Gs D'') + (⌊D/2⌋ + D mod 2) (frame bF4),

then runs S_D ; C ; S_D ; b^D ; Q_p (the frozen sdC, mdC, truncU, and the round-six C-layer clCH). bodyCoreQ: the output is prop14Proc … (tens Cm) with the frozen guarantees; bodyQH: the run of bodyCH as a RunQ.

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*).