The line's chunk kernel is a `RowBody6` row kernel (round six, `chunkK2_rowBody6`)

The line's chunk kernel is a RowBody6 row kernel.

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

theorem J6Seg.KR.chunkK2_rowBody6 {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp} {e : Fin Pp}
    {M : MulSpec} {pM : Fin Pp} (htbl : tbl e = chunkI2 pM) (hM : MulOK Isym tbl pM M)
    (hdom : ∀ x y, M.dom x y)
    {b pk φD B BH : ℕ} {φT : ℕ → ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ n, ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT n)
    (hb : 1 ≤ b) (P R s t lam α : ℕ) (hlam : 1 ≤ lam) {Kt X : ℤ} (hKt : 0 ≤ Kt) (hX : 0 ≤ X)
    (hT : ∀ u < lam, |(TT P R s t α).di u| ≤ 2 ^ P * Kt ∧ |(TT P R s t α).gi u| ≤ 2 ^ P * Kt ∧
      |(TT P R s t α).gam u| ≤ 2 ^ P * Kt ∧ |(TT P R s t α).dd u| ≤ 2 ^ P * Kt ∧
      ∀ c, |(TT P R s t α).am c u| ≤ 2 ^ P * Kt ∧ |(TT P R s t α).ap c u| ≤ 2 ^ P * Kt)
    (hKpk : 2 ^ P * Kt ≤ 2 ^ pk) (hpk : Xs ((lam + 1) * Kt + 1) X 7 ≤ 2 ^ pk)
    (hbig : 4 * lam * 2 ^ (2 * pk) < 2 ^ (b - 1))
    (hhdr : ∀ n, 1 ≤ n → n ≤ lam → ∀ v ∈ blkHdr2 n b, zsz v ≤ BH)
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B) (hlB : zsz ((2 * lam : ℕ) : ℤ) ≤ B)
    (hBBH : B ≤ BH)
    (hBH : ∀ q, ∀ v ∈ tabK2 P pk b lam (diL P R s t lam α) (giL P R s t lam α) (gamL P R s t lam α)
      (ddL P R s t lam α) (descsOf s t lam (TT P R s t α) q), zsz v ≤ BH)
    (C : ℝ) (hC : ∀ q, ((cKer2 pk b lam φD φT B BH (descsOf s t lam (TT P R s t α) q) + 2 : ℕ) : ℝ) ≤ C) :
    RowBody6 Isym tbl e J6Seg.KR.dT
      (fun q => tabK2 P pk b lam (diL P R s t lam α) (giL P R s t lam α) (gamL P R s t lam α)
        (ddL P R s t lam α) (descsOf s t lam (TT P R s t α) q))
      (fun x => x.length = lam ∧ AB X x) (fun q => liftG (chunkK P R s t lam α q)) C

Context. B3′, part 7: chunkK2_rowBody6 — the line's chunk kernel with tables tabK2 … (descsOf … q).

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