Round-six lemma `n1`
ProvedJ6Seg.Side.n1An 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.n1 :
(axwd6 P n src k ap + 1) * (axpre6 P n D k * axnc6 P n k * 2 ^ axfC6 P n * axpost6 P n D k + 1) *
(axfC6 P n + 1) +
(Nat.size (axpre6 P n D k * axnc6 P n k * 2 ^ axfC6 P n * axpost6 P n D k) +
axwd6 P n src k ap + axfC6 P n + 4) ^ 2 ≤
7 * (Wc ap + 9) ^ 2 * (TP6 P n * pP6 P n * (Nat.log 2 (bP6 n) + 1))
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.n1 :
(axwd6 P n src k ap + 1) * (axpre6 P n D k * axnc6 P n k * 2 ^ axfC6 P n * axpost6 P n D k + 1) *
(axfC6 P n + 1) +
(Nat.size (axpre6 P n D k * axnc6 P n k * 2 ^ axfC6 P n * axpost6 P n D k) +
axwd6 P n src k ap + axfC6 P n + 4) ^ 2 ≤
7 * (Wc ap + 9) ^ 2 * (TP6 P n * pP6 P n * (Nat.log 2 (bP6 n) + 1)) := by sorry