Round-six lemma `cost_le_core`
ProvedJ6Seg.PreT.cost_le_coreAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPre28):
theorem J6Seg.PreT.cost_le_core {Q R A M lam nc t p b aA aC mA mC : ℕ} (hp : 1 ≤ p) (hb : 1 ≤ b) (ht : 1 ≤ t)
(hA : A ≤ aA * Q + aC) (hM : M ≤ mA * Q + mC) (hQ : Q ≤ 3 * p) (hR : R ≤ p)
(hlam : lam ≤ 4 * b ^ 2) (hnc : nc * lam ≤ t) (hl : 1 ≤ lam) :
cCS2 Q R A lam M nc ≤ cK aA aC mA mC * b ^ 4 * t * p ^ 10
Context. B-line IL, pre-tables (B5′), part 28: the chunk store is within the per-axis budget
chunkStore_cost_ev: for widths A ≤ aA·Q + aC, M ≤ mA·Q + mC (Q = Q6 p d s), eventually
cCS2 Q R A λ M nc ≤ cU6 P n A' / (D + 1) on every axis (Cp = 1, any A').
The ℕ core: cCS2 ≤ K b⁴ t p¹⁰ (cCS2_le, λ ≤ 4b², nc λ ≤ t), d ≤ b, and
K b⁵ p⁹ t ≤ T because t² ≤ 2T (ℓ ≤ (L+1)/2 for d ≥ 2) and 2 (K b⁵ p⁹)² ≤ T
(T b' ≥ 4n > 2^(b+1)).
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_Defs68 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.PreT open IntMul NLogN IntMul.Kappa.R6 J6Seg J6Seg.Side
theorem J6Seg.PreT.cost_le_core {Q R A M lam nc t p b aA aC mA mC : ℕ} (hp : 1 ≤ p) (hb : 1 ≤ b) (ht : 1 ≤ t)
(hA : A ≤ aA * Q + aC) (hM : M ≤ mA * Q + mC) (hQ : Q ≤ 3 * p) (hR : R ≤ p)
(hlam : lam ≤ 4 * b ^ 2) (hnc : nc * lam ≤ t) (hl : 1 ≤ lam) :
cCS2 Q R A lam M nc ≤ cK aA aC mA mC * b ^ 4 * t * p ^ 10 := by sorry