`PartD` for the streams of a line (round six, `partD_line`)
ProvedJ6Seg.JK.partD_linePartD for the streams of a line.
The following holds (Lean statement, in the scope of module Solutions.J6SegJPre7):
theorem J6Seg.JK.partD_line (h : SegReg P R s t lam w α)
(hK : K ≤ (LJ s t lam w).length) (hG : (LJ s t lam w).length ≤ G)
(hXb : Xb0 P w Bv ≤ Xb) (hBc : Bc0 s K G ≤ Bc) (hk : 2 * Xb + 2 * P + Bc + 6 ≤ k)
(v : List ℤ) (hv : v.length = G) (hvb : Bnd Bv v) :
PartD P k K G Xb Bc (jFs P R s t lam w α) (jBs P R s t lam w α)
(jCc P R s t lam w α K) v
Context. J kernel precondition (JPre), part 7: PartD and JPre for the streams of a line
partD_line: in the regime SegReg P R s t λ w α, with K ≤ |LJ| ≤ G, for every gathered
row part v of length G with Bnd Bv v, the streams jFs, jBs, jCc of the line satisfy
PartD P k K G Xb Bc … v for every Xb ≥ Xb0 P w Bv, Bc ≥ Bc0 s K G and
k ≥ 2 Xb + 2 P + Bc + 6.
jPre_line: the same for both parts of a GI row, i.e. JPre.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs67
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.JK
open Finset
open IntMul NLogN NLogN.KIL NLogN.KFB Function
variable {P R s t lam w α K G Bv Xb Bc k : ℕ}
theorem J6Seg.JK.partD_line (h : SegReg P R s t lam w α)
(hK : K ≤ (LJ s t lam w).length) (hG : (LJ s t lam w).length ≤ G)
(hXb : Xb0 P w Bv ≤ Xb) (hBc : Bc0 s K G ≤ Bc) (hk : 2 * Xb + 2 * P + Bc + 6 ≤ k)
(v : List ℤ) (hv : v.length = G) (hvb : Bnd Bv v) :
PartD P k K G Xb Bc (jFs P R s t lam w α) (jBs P R s t lam w α)
(jCc P R s t lam w α K) v := by sorry