B1: `SlabNeed6 P` for every `P.Ok` (round six, `slabNeed6`)
ProvedJ6Seg.Src.slabNeed6B1: SlabNeed6 P for every P.Ok.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSrc24):
theorem J6Seg.Src.slabNeed6 (P : Prm) (hP : P.Ok) : SlabNeed6 P
Context. B-line IL, source-table producers, part 24: SlabNeed6 P (B1)
slabNeed6 P hP : SlabNeed6 P for every P.Ok. The family USf dA (8 procedures, uniform in the
table): upF dA Z Z1 Cm body{1,3,5,7} and dn0 Cm / dn7 Cm, with parking registers
Z, Z1, Cm ∈ {49, 50, 51, 54} \ {dA}. The procedure index map: e1u = 0, e1d = 1, e3u = 2, …, e7d = 7. Constants: Cs = 1, A = 0 (every set-up / tear-down costs ≤ B0 + 2 ≤ cU6 P n 0 / (D+1),
via J6Seg.Side.slabCost6_all with K = Kb + 10000).
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.Src open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg IntMul.Kappa.R6 open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg open J6Seg.Slab (argO) open J6Seg.PJ (rg dsc) open J6Seg.Ax (ρS sZ slabV SetupS Fam SlabNeed6 SlabFree slabV1 slabV3 slabV5 slabV7 ctl1 ctl3 ctl5 ctl7 AxReg)
theorem J6Seg.Src.slabNeed6 (P : Prm) (hP : P.Ok) : SlabNeed6 P := by sorry