The chunk kernel is a `RowBody6` row kernel (round six, `chunk2_rowBody6`)

The chunk kernel is a RowBody6 row kernel (abstract tables).

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

theorem J6Seg.KR.chunk2_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 lam : ℕ) (hlam : 1 ≤ lam) (di gi gam dd : List ℤ)
    (ds : ℕ → List (ℕ × List ℤ × List ℤ)) {Kt X : ℤ} (hKt : 0 ≤ Kt) (hX : 0 ≤ X)
    (hdi : di.length = lam) (hgi : gi.length = lam) (hga : gam.length = lam)
    (hdd : dd.length = lam)
    (tdi : TB (2 ^ P * Kt) di) (tgi : TB (2 ^ P * Kt) gi) (tga : TB (2 ^ P * Kt) gam)
    (tdd : TB (2 ^ P * Kt) dd) (hKpk : 2 ^ P * Kt ≤ 2 ^ pk)
    (hpk : Xs ((lam + 1) * Kt + 1) X 7 ≤ 2 ^ pk)
    (hds : ∀ q, ∀ d ∈ ds q, 1 ≤ d.1 ∧ d.2.1.length = d.1 ∧ d.2.2.length = d.1 ∧ d.1 ≤ lam ∧
        TB (2 ^ P * Kt) d.2.1 ∧ TB (2 ^ P * Kt) d.2.2 ∧
        2 * (2 * d.1) * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧
        zsz ((2 * d.1 : ℕ) : ℤ) ≤ B ∧ (∀ v ∈ blkHdr2 d.1 b, zsz v ≤ BH))
    (hsum : ∀ q, J6Seg.KR.sumN (ds q) ≤ lam)
    (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 di gi gam dd (ds q), zsz v ≤ BH)
    (C : ℝ) (hC : ∀ q, ((cKer2 pk b lam φD φT B BH (ds q) + 2 : ℕ) : ℝ) ≤ C) :
    RowBody6 Isym tbl e J6Seg.KR.dT (fun q => tabK2 P pk b lam di gi gam dd (ds q))
      (fun x => x.length = lam ∧ AB X x) (fun q => chunkG2 P di gi gam dd (ds q)) C

Context. B3′, part 6: chunk2_rowBody6 (the new chunk kernel as a RowBody6 row kernel, abstract tables).

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