Main theorem, sparse and fully instantiated (round six, `segInvFullS_err`)

Main theorem, sparse and fully instantiated.

The following holds (Lean statement, in the scope of module Solutions.J6SegSparse):

theorem J6Seg.segInvFullS_err {R w : ℕ} {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,
      |((segInvFullS 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 ∧
      |((segInvFullS 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 (segInvFullS 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 sparse algorithm

segInvS P lam T B U is segInv with the capacitance solved by geSolveS on the pattern bandS (λ + w) (s - λ - w): a band of half-width λ + w (blocks of length ≤ λ, coupling width w) plus the border of positions ≥ s - λ - w (the cyclic wrap). Per row of the capacitance at most 2(λ+w)+1 band entries plus the border are touched.

• capI_band: the capacitance vanishes off the pattern;
• segInvS_eq: under the hypotheses of segInv_err, segInvS = segInv;
• segInvFullS_err: the fully instantiated sparse algorithm satisfies the bound of segInvFull_err.

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*).