The whole set-up product, as a polynomial in `p, t, b` (`slab_poly`)
ProvedJ6Seg.Side.slab_polyThe whole set-up product, as a polynomial in p, t, b.
The following holds (Lean statement, in the scope of module Solutions.J6SegSlabCost1):
theorem J6Seg.Side.slab_poly {K d s p t α b : ℕ} (hp : 1 ≤ p) (ht : 1 ≤ t) (hb : 1 ≤ b) (hd : d ≤ p)
(hs : s ≤ t) (hα : α ^ 2 ≤ p) :
K * (NF d s + p + t + 1) *
(J6Seg.Src.uC (4 * p) J6Seg.Src.DD + J6Seg.Src.ePC (4 * p) p α +
NLogN.KFUU.cU (4 * p + 1) + 20000) + 2 ≤
((K * (CN + 1) * CUt + 2) * 3 ^ 19) * b ^ 20 * t ^ 20 * p ^ 20
Context. Slab set-up cost (the asymptotic half of SlabNeed6)
slabCost6_all K: eventually, on every axis,
K · (NF d s + p + t + 1) · Ut p α + 2 ≤ cU6 P n 0 / (D + 1), where
Ut p α = uC (4p) DD + ePC (4p) p α + cU (4p+1) + 20000 (inlined).
Everything is a polynomial in X = p + t + 1 of degree ≤ 19; we close with budget_ev (e = 20).
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_Defs70 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Side set_option maxRecDepth 20000 open IntMul NLogN IntMul.Kappa.R6 J6Seg
theorem J6Seg.Side.slab_poly {K d s p t α b : ℕ} (hp : 1 ≤ p) (ht : 1 ≤ t) (hb : 1 ≤ b) (hd : d ≤ p)
(hs : s ≤ t) (hα : α ^ 2 ≤ p) :
K * (NF d s + p + t + 1) *
(J6Seg.Src.uC (4 * p) J6Seg.Src.DD + J6Seg.Src.ePC (4 * p) p α +
NLogN.KFUU.cU (4 * p + 1) + 20000) + 2 ≤
((K * (CN + 1) * CUt + 2) * 3 ^ 19) * b ^ 20 * t ^ 20 * p ^ 20 := by sorry