Round-six lemma `segInvFull_err`
ProvedJ6Seg.segInvFull_errAn 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.J6SegFull):
theorem J6Seg.segInvFull_err {P R lam w s t α : ℕ} {Bu εin Wm : ℝ}
(hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hx : 3 ≤ xθ s t α) (hl : 1 ≤ lam) (hw : w ≤ s)
(hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R)
(U : ℕ → ℤ × ℤ) (hBu : 0 ≤ Bu)
(hU : ∀ i < s, |((U i).1 : ℝ) / 2 ^ P| ≤ Bu ∧ |((U i).2 : ℝ) / 2 ^ P| ≤ Bu)
(v ww : ℕ → ℂ) (hww : ∀ i < s, ‖ww i‖ ≤ Wm)
(hsys : ∀ i < s, ww i + Eexact s t α ww i = v i)
(hin : ∀ i < s, |((U i).1 : ℝ) / 2 ^ P - (v i).re| ≤ εin ∧
|((U i).2 : ℝ) / 2 ^ P - (v i).im| ≤ εin)
(hP : 1000 * fullG lam w s t α Bu ≤ 2 ^ P) :
∀ i < s,
|((segInvFull P R lam w s t α U i).1 : ℝ) / 2 ^ P - (ww i).re| ≤
60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
|((segInvFull P R lam w s t α U i).2 : ℝ) / 2 ^ P - (ww i).im| ≤
60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
‖toC (segInvFull P R lam w s t α U i) / 2 ^ P - ww i‖ ≤
2 * (60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin)
Context. Segmented inverse (S2): the fully instantiated algorithm
segInvFull P R lam w s t α U = segInvC P (mkTables P R s t α) (mkBlocks s t lam w) U: everything
(blocks, tables, elimination) is computed from (P, R, λ, w, s, t, α).
segInvFull_err: for s ≤ t, α ≥ 2, α²θ ≥ 3, 1 ≤ λ, w ≤ s, D_{λ-1} ≤ 2^R, and
1000 G ≤ 2^P with G = D_{λ-1} ((λ+1)(3λ+3)+1)(Bu+1)(λ+1)(2w+1)(s+1)², the output is within
60 G/2^P + 12 e^{-πα² w(w+1)} (Bu+1) + (8/7) ε_in of 2^P w in both parts (twice that in norm),
where w + Eexact w = v.
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_Defs61 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg open Finset Real open IntMul.HvdH IntMul.HvdH.JPf J6QLU
theorem J6Seg.segInvFull_err {P R lam w s t α : ℕ} {Bu εin Wm : ℝ}
(hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hx : 3 ≤ xθ s t α) (hl : 1 ≤ lam) (hw : w ≤ s)
(hR : ddR (α : ℝ) ((t : ℝ) / s) (lam - 1) ≤ 2 ^ R)
(U : ℕ → ℤ × ℤ) (hBu : 0 ≤ Bu)
(hU : ∀ i < s, |((U i).1 : ℝ) / 2 ^ P| ≤ Bu ∧ |((U i).2 : ℝ) / 2 ^ P| ≤ Bu)
(v ww : ℕ → ℂ) (hww : ∀ i < s, ‖ww i‖ ≤ Wm)
(hsys : ∀ i < s, ww i + Eexact s t α ww i = v i)
(hin : ∀ i < s, |((U i).1 : ℝ) / 2 ^ P - (v i).re| ≤ εin ∧
|((U i).2 : ℝ) / 2 ^ P - (v i).im| ≤ εin)
(hP : 1000 * fullG lam w s t α Bu ≤ 2 ^ P) :
∀ i < s,
|((segInvFull P R lam w s t α U i).1 : ℝ) / 2 ^ P - (ww i).re| ≤
60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
|((segInvFull P R lam w s t α U i).2 : ℝ) / 2 ^ P - (ww i).im| ≤
60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
‖toC (segInvFull P R lam w s t α U i) / 2 ^ P - ww i‖ ≤
2 * (60 * fullG lam w s t α Bu / 2 ^ P +
3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (w * (w + 1))))) * (Bu + 1) + 8 / 7 * εin) := by sorry