Round-six lemma `Ut_le_X`
ProvedJ6Seg.Side.Ut_le_XUt p α ≤ CUt · X^10 when p ≤ X, α² ≤ p.
The following holds (Lean statement, in the scope of module Solutions.J6SegSlabCost1):
theorem J6Seg.Side.Ut_le_X {p α X : ℕ} (hX : 1 ≤ X) (hp : p ≤ X) (hα : α ^ 2 ≤ p) :
J6Seg.Src.uC (4 * p) J6Seg.Src.DD + J6Seg.Src.ePC (4 * p) p α + NLogN.KFUU.cU (4 * p + 1) +
20000 ≤ CUt * X ^ 10
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.Ut_le_X {p α X : ℕ} (hX : 1 ≤ X) (hp : p ≤ X) (hα : α ^ 2 ≤ p) :
J6Seg.Src.uC (4 * p) J6Seg.Src.DD + J6Seg.Src.ePC (4 * p) p α + NLogN.KFUU.cU (4 * p + 1) +
20000 ≤ CUt * X ^ 10 := by sorry