Round-six lemma `n2`
ProvedJ6Seg.Side.n2An 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.J6SegSideCost4):
theorem J6Seg.Side.n2 :
dP6 P n * ((axwd6 P n src k ap + 1) *
(axpre6 P n D k * 1 * 2 ^ axfJ6 P n src k * axpost6 P n D k + 1) * (axfJ6 P n src k + 1) +
(Nat.size (axpre6 P n D k * 1 * 2 ^ axfJ6 P n src k * axpost6 P n D k) +
axwd6 P n src k ap + axfJ6 P n src k + 4) ^ 2) ≤
101 * (Wc ap + 12) ^ 2 * (TP6 P n * pP6 P n * (dP6 P n + ℓP6 P n))
Context. Side costs 4: the eight side costs of one axis, as natural-number polynomials
With W = 3 wA + wC (so wd ≤ W p), T = TP6, p = pP6, β = log₂ lg n, on an axis with
AxNum:
n1: chunk fine exposure≤ 7 (W+9)² · T p (β+1);n2:d ·(Jfine exposure)≤ 101 (W+12)² · T p (d + ℓ);n3–n5: the selection and the two identity slab passes≤ 10^10 (W+1) · T p;n6: the output slab pass≤ 10^11 (W+11) · T p + 10^7 · T · fmB(2Z),Z = wd + 2p + 8;n7,n8: the copy and the swap≤ 10^9 (W+5)² · T p.
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.Side
open IntMul NLogN IntMul.Kappa.R6 J6Seg
variable {P : Prm} {n : ℕ} {src : ℕ → ℕ} {D k : ℕ} (ap : AxPlan6) (h : AxNum P n src D k)
include h
theorem J6Seg.Side.n2 :
dP6 P n * ((axwd6 P n src k ap + 1) *
(axpre6 P n D k * 1 * 2 ^ axfJ6 P n src k * axpost6 P n D k + 1) * (axfJ6 P n src k + 1) +
(Nat.size (axpre6 P n D k * 1 * 2 ^ axfJ6 P n src k * axpost6 P n D k) +
axwd6 P n src k ap + axfJ6 P n src k + 4) ^ 2) ≤
101 * (Wc ap + 12) ^ 2 * (TP6 P n * pP6 P n * (dP6 P n + ℓP6 P n)) := by sorry