D-039 — Proof of the digamma remainder bound (upgrades R-004's H2 to proved)

Date: 2026-08-19 | Session: 008 | Task: R-004 hardening (D-037 follow-up) Status: ERRATUM (2026-08-19, D-054 task 4.3b): proof BROKEN, bound TRUE. (i) §1's Binet tail split at t = 1 bounds ∫₁^∞ by a constant (~4e-5), so the assembly fails for |W| ≳ 35; repair: split at t ~ |V|/2 (|W²+t²| ≥ V²/2 below, exponential tail above). (ii) §2's Cauchy estimate yields 0.45 ABSOLUTE on |u| ≤ 0.2, not 0.45·|u|⁴; repair: sharper Cauchy circle or direct series majorant (true max ~0.01). The bound |r(w)| ≤ 1/|w|² itself stands (asymptotic 1/12; grid max 0.084). Repair = task 4.5a. Original text preserved below. Status was: complete. Claim (D-036 §1, used in the R-bound assembly): ψ(w) = log w − 1/(2w) + r(w), |r(w)| ≤ 1/|w|² for Re w ≥ −3/2, |w| ≥ 5 (|Im w| ≥ 5 in the contour application). Proved below with margin (we get 0.36/|w|²). Numerical spot-check: max |r|·|w|² ≈ 0.084 over a sample grid (asymptotic value 1/12).

1. Binet piece (Re W > 0)

Binet's second formula for ψ: for Re W > 0, r(W) = −2 ∫₀^∞ t / ((t² + W²)(e^{2πt} − 1)) dt. For W = U + iV and real t: |W² + t²|² = |W|⁴ + 2t²(U²−V²) + t⁴ ≥ (|W|² − t²)² (both sign cases), and also |W² + t²| ≥ 2U|V| (drop the first square). Split at t = 1, assuming |W| ≥ 5 and U ≥ 1/2, |V| ≥ 5:

• ∫₀¹: |W²+t²| ≥ |W|²−1 ≥ 0.96|W|², and ∫₀¹ t/(e^{2πt}−1)dt < 1/24 (∫₀^∞ = Γ(2)ζ(2)/(2π)² = 1/24).
• ∫₁^∞: |W²+t²| ≥ 2U|V| ≥ |V| ≥ 5, and ∫₁^∞ t/(e^{2πt}−1)dt ≤ 2e^{−2π}/(2π) ≤ 1e-3·... ≤ 2e-4. Assemble: |r(W)| ≤ 2[1/(24(|W|²−1)) + 2e-4] ≤ 0.097/|W|², |W| ≥ 5, Re W ≥ 1/2.

2. Recurrence piece

ψ(w) = ψ(w+2) − 1/w − 1/(w+1) gives, with W = w + 2, r(w) = r(w+2) + E(w), E(w) := log(1 + 2/w) − 1/(2(w+2)) − 1/(2w) − 1/(w+1). E(w) = f(1/w) with f(u) = log(1+2u) − u/2 − u/(2(1+2u)) − u/(1+u) analytic on |u| ≤ 0.4 (nearest singularity u = −1/2), and f(u) = −u³/3 + O(u⁴) (coefficients through u² vanish exactly; c₃ = −1/3). On |u| = 0.4: |f + u³/3| ≤ 3.62 (termwise: |log(1+2u)| ≤ −log 0.2 = 1.61, |u|/2 = 0.2, |u/(2(1+2u))| ≤ 0.4/(2·0.2) = 1, |u/(1+u)| ≤ 0.78, plus 0.4³/3 ≤ 0.022). Cauchy: |f(u) + u³/3| ≤ 3.62·(|u|/0.4)⁴/(1−|u|/0.4); for |u| ≤ 0.2 (i.e. |w| ≥ 5): ≤ 0.45·|u|⁴·... precisely 3.62·(0.5)⁴/0.5 = 0.45. Hence |E(w)| ≤ 1/(3|w|³) + 0.45/|w|⁴ ≤ 0.0847/|w|², |w| ≥ 5.

3. Assembly

For Re w ≥ −3/2, |w| ≥ 5: W = w+2 has Re W ≥ 1/2 and |W| ≥ |w|−2; for the contour application |Im w| ≥ 5 so |V| ≥ 5 and |W| ≥ 5 hold; |w+2| ≥ (3/5)|w|. Therefore |r(w)| ≤ 0.097·(5/3)²/|w|² + 0.0847/|w|² = (0.269 + 0.085)/|w|² ≤ 0.36/|w|² < 1/|w|². ∎

4. Consequences

• D-036 §1's R-bound assembly is now FULLY traced: every piece is proved (Trudgian N(T)/S(T) [literature], σ₂ exact, the digamma remainder above, elementary kernel bounds). The R-bound |R(s)| ≤ 2 log(|t|+2) + 2 with A = 2.0, B₀ = 2.0 is [PROVED].
• R-004's input inventory: H2 is no longer heuristic. The theorem's remaining non-proved inputs: Platt–Trudgian (computational), Misguich–Voros (computational literature), M₀ = 1.3352 (E-023 S1, grid + Lipschitz safety — upgradeable to interval-rigorous via an acb box cover, E-023b, optional; M₀ enters only an additive constant 40·M₀ ≈ 53).
• Tag update: R-004 → [PROVED-CONDITIONAL(computational RH-to-T₀; computational finite verification)] — the digamma caveat removed.