Error bound for the segmented inverse of the resampling system (real 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$ be a fixed-point input with $|U_i/2^P|\le B_u$ ($B_u\ge0$) for $i<s$, and let $v,w:\mathbb N\to\mathbb R$ satisfy $|w_i|\le W_m$, the resampling system $N w = v$ (NxR s t α w i = v i) for $i<s$, and $|U_i/2^P - v_i|\le\varepsilon_{in}$. If $1000\,G\le 2^P$, then for every $i<s$ the output of the segmented inverse segInv P T B U satisfies

In Lean:

theorem J6Seg.segInv_err {P s t α 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 : ℝ) / 2 ^ P| ≤ Bu)
    (v w : ℕ → ℝ) (hw : ∀ i < s, |w i| ≤ Wm) (hsys : ∀ i < s, NxR s t α w i = v i)
    (hin : ∀ i < s, |(U i : ℝ) / 2 ^ P - v i| ≤ εin)
    (hP : 1000 * segG B lam E Dm Bu ≤ 2 ^ P) :
    ∀ i < s, |(segInv P T B U i : ℝ) / 2 ^ P - w i| ≤
      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*).