Error bound for the segmented inverse of the resampling system (complex form)

Let $s\le t$ be lengths with $s>0$, let $\alpha\ge 2$ be the Gaussian parameter and assume $x=\alpha^2\theta=\alpha^2(t-s)/s\ge 3$ (xθ s t α). Let $B$ be a valid block structure (BlocksOK s t B: wrap-free runs partitioning $[0,s)$ with coupling width $w=B.w$) whose blocks all have length at most $\lambda$, and let $T$ be precomputed fixed-point tables of precision $P$ accurate to $E\ge 0$ ulps with per-block constants bounded by $D_m$ (TabOK P s t α B T E Dm). Put $G=D_m\,((\lambda+1)E+1)\,(B_u+1)\,(\lambda+1)\,(2w+1)\,(|J|+1)^2$ (segG), where $|J|$ is the number of near-boundary positions of the block structure. Let $U:\mathbb N\to\mathbb Z\times\mathbb Z$ be a fixed-point complex input whose real and imaginary parts satisfy $|U_i^{re}/2^P|,|U_i^{im}/2^P|\le B_u$ ($B_u\ge 0$), and let $v,w:\mathbb N\to\mathbb C$ satisfy $\|w_i\|\le W_m$, the system $w_i+(E w)_i=v_i$ with the exact coupling operator Eexact s t α for $i<s$, and $|U_i^{re}/2^P-\operatorname{Re}v_i|\le\varepsilon_{in}$, $|U_i^{im}/2^P-\operatorname{Im}v_i|\le\varepsilon_{in}$. Write $\delta=\frac{60G}{2^P}+3\cdot4e^{-\pi\alpha^2w(w+1)}(B_u+1)+\frac87\varepsilon_{in}$. If $1000\,G\le2^P$, then for every $i<s$ the complex segmented inverse segInvC P T B U has real and imaginary parts each within $\delta$ of $\operatorname{Re}w_i$, $\operatorname{Im}w_i$, and $\|\mathrm{segInvC}(U)_i/2^P-w_i\|\le 2\delta$ (as a complex number via toC).

In Lean:

theorem J6Seg.segInvC_err {P lam : ℕ} {B : Blocks} {T : Tables} {E Dm Bu εin Wm : ℝ}
    (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α) (hx : 3 ≤ xθ s t α)
    (hB : BlocksOK s t B) (hlam : ∀ i < s, B.len i ≤ lam)
    (hT : TabOK P s t α B T E Dm) (hE : 0 ≤ E)
    (U : ℕ → ℤ × ℤ) (hBu : 0 ≤ Bu)
    (hU : ∀ i < s, |((U i).1 : ℝ) / 2 ^ P| ≤ Bu ∧ |((U i).2 : ℝ) / 2 ^ P| ≤ Bu)
    (v w : ℕ → ℂ) (hw : ∀ i < s, ‖w i‖ ≤ Wm)
    (hsys : ∀ i < s, w i + Eexact s t α w 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 * segG B lam E Dm Bu ≤ 2 ^ P) :
    ∀ i < s,
      |((segInvC P T B U i).1 : ℝ) / 2 ^ P - (w i).re| ≤ 60 * segG B lam E Dm Bu / 2 ^ P +
          3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (B.w * (B.w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
      |((segInvC P T B U i).2 : ℝ) / 2 ^ P - (w i).im| ≤ 60 * segG B lam E Dm Bu / 2 ^ P +
          3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (B.w * (B.w + 1))))) * (Bu + 1) + 8 / 7 * εin ∧
      ‖toC (segInvC P T B U i) / 2 ^ P - w i‖ ≤ 2 * (60 * segG B lam E Dm Bu / 2 ^ P +
          3 * (4 * exp (-(π * (α : ℝ) ^ 2 * (B.w * (B.w + 1))))) * (Bu + 1) + 8 / 7 * εin)

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