[{"type":"thinking","thinking":"`Zeta23.GammaFacts.StirlingVert.digamma_stirling (hw : 0 < w.re) (ht : 1/2 ≤ |w.im|) : ‖digamma w − log w + (1/2)/w‖ ≤ 3 / w.im²`.\n\nSo ψ(w) − log w + 1/(2w) ≤ 3/(im w)² for re w > 0, |im w| ≥ 1/2. That's the sharp remainder with constant 3 (vs Lemma D's 1.2/|w|²) — MORE than enough for our budget.\n\nOur w = s/2 has re w = σ/2 ∈ [−5/4, 3/2] — can be ≤ 0 (for σ ∈ [−5/2, 0])! So digamma_stirling applies directly only when σ > 0. For σ ≤ 0, shift: w ↦ w+2 (re w+2 = σ/2 + 2 ≥ 3/4 > 0 ✓): ψ(w+2) − log(w+2) + 1/(2(w+2)) ≤ 3/(im)². And ψ(w+2) = ψ(w) + 1/w + 1/(w+1) (digamma_add_natCast with n = 2). So ψ(w) = ψ(w+2) − 1/w − 1/(w+1).\n\nThe ψ-difference: ψ(w) − ψ(w₀) — with w₀ = s₀/2 = 1 + it/2: re w₀ = 1 > 0 ✓ direct. For w with re w = σ/2:\n- If σ/2 > 0 (σ ∈ (0, 3]): direct digamma_stirling on both.\n- If σ ≤ 0: shift w by 2.\n\nHmm — case split on σ. Cleaner: apply the shift for ALL w? For re w > 0 the direct is fine; for re w ≤ 0 shift by 2. The difference bound:\n\nCase A (re w > 0): |ψ(w) − ψ(w₀)| = |[log w − 1/(2w) + r(w)] − [log w₀ − 1/(2w₀) + r(w₀)]| ≤ |log w − log w₀| + (1/2)|1/w − 1/w₀| + 3/(im w)² + 3/(im w₀)². With im w = im w₀ = t/2 ≥ 5: ≤ |log diff| + (1/2)·2.25/25 + 6/25 = |log diff| + 0.045 + 0.24.\n\nCase B (re w ≤ 0): ψ(w) = ψ(w+2) − 1/w − 1/(w+1); ψ(w+2) = log(w+2) − 1/(2(w+2)) + r(w+2). So ψ(w) = log(w+2) − 1/(2(w+2)) − 1/w − 1/(w+1) + r(w+2). And ψ(w₀) = log w₀ − 1/(2w₀) + r(w₀). The difference: [log(w+2) − log w₀] − (1/2)[1/(w+2) − 1/w₀] − [1/w + 1/(w+1)] + [r(w+2) − r(w₀)]. Bounds: |1/w| ≤ 1/|im w| = 2/t ≤ 0.2; |1/(w+1)|: im(w+1) = t/2 ⟹ ≤ 2/t ≤ 0.2. |log(w+2) − log w₀|: w+2 = (σ/2+2) + it/2, w₀ = 1 + it/2: |(w+2) − w₀| = |σ/2 + 1| ≤ 5/4 + 1 = 2.25 (σ ∈ [−5/2, 0]: σ/2 + 1 ∈ [−1/4, 1]: |σ/2+1| ≤ 1 hmm wait σ/2 ∈ [−5/4, 0] so σ/2 + 1 ∈ [−1/4, 1], |·| ≤ 1 — even better; but let me keep 2.25 for safety — no: |σ/2 + 1| ≤ max(|−1/4|, 1) = 1). |log(w+2) − log w₀| ≤ 2·|(w+2−w₀)/w₀| ≤ 2·1/5 = 0.2·2 = 0.4 (|w₀| ≥ 5). Actually |log(1+u)| ≤ 2|u| for |u| ≤ 1/2: |u| = |(w+2−w₀)/w₀| ≤ 1/5 = 0.2: ≤ 0.4 ✓.\n\nHmm — the case split makes it messy. Let me simplify: is there a UNIFORM form? Actually — simpler: apply digamma_stirling at w+2 and w₀+2?? No wait — the cleanest uniform approach: the difference ψ(w) − ψ(w₀) where BOTH get shifted: no. \n\nAlternative uniform approach: use the RECURRENCE relation differently. Actually, let me reconsider: our w = s/2 with σ ∈ [−5/2, 3]. The digamma difference bound — the cleanest uniform statement:\n\nFor ANY w with |im w| ≥ 5 and re w ≥ −5/4 (our range), and w₀ = 1 + it/2:\nUse the shifted form for w only when needed. OR: uniformly shift w by 2: ψ(w) = ψ(w+2) − 1/w − 1/(w+1) (valid for im w ≠ 0 ✓ digamma_add_natCast n=2 needs im ≠ 0 ✓). And ψ(w+2) = log(w+2) − 1/(2(w+2)) + r(w+2) with re(w+2) = σ/2+2 ≥ 3/4 > 0 ✓ ALWAYS (σ ≥ −5/2). So uniformly:\nψ(w) = log(w+2) − 1/(2(w+2)) − 1/w − 1/(w+1) + r(w+2), ‖r(w+2)‖ ≤ 3/(t/2)² = 12/t².\nψ(w₀) = log w₀ − 1/(2w₀) + r(w₀), ‖r(w₀)‖ ≤ 12/t².\n\nDifference: ψ(w) − ψ(w₀) = [log(w+2) − log w₀] − (1/2)[1/(w+2) − 1/w₀] − 1/w − 1/(w+1) + [r(w+2) − r(w₀)].\n\nHmm — the −1/w − 1/(w+1) extra terms: |1/w| ≤ 2/t, |1/(w+1)| ≤ 2/t. These are the price of the uniform shift: ≤ 4/t ≤ 0.4. And log(w+2) − log w₀: |(w+2) − w₀| = |σ/2 + 1| ≤ 2.25 (uniform σ range): |u| ≤ 2.25/5 = 0.45: |log diff| ≤ 2·0.45 = 0.9. (1/2)|1/(w+2) − 1/w₀| ≤ (1/2)·|(w+2)−w₀|/(|w+2||w₀|) ≤ (1/2)·2.25/(5·5) = 0.045. r-difference ≤ 24/t² ≤ 0.24.\n\nTotal: 0.9 + 0.045 + 0.4 + 0.24 = 1.585. ½·1.585 = 0.7925 ≤ 2.185 ✓✓ FITS with huge margin. And it's UNIFORM (no case split). \n\nWait — actually, hmm: ψ(w) = ψ(w+2) − 1/w − 1/(w+1) — digamma_add_natCast (w) (2): ψ(w+2) = ψ(w) + Σ_{j<2} (w+j)⁻¹ = ψ(w) + w⁻¹ + (w+1)⁻¹ ✓ so ψ(w) = ψ(w+2) − w⁻¹ − (w+1)⁻¹ ✓. digamma_add_natCast needs hw : w.im ≠ 0 ✓ (im w = t/2 ≥ 5).\n\nSo piece 6's Lean proof:\n1. `digamma_stirling` at w+2 and at w₀ (both re > 0, |im| = t/2 ≥ 5 ≥ 1/2 ✓): ‖ψ(v) − log v + (1/2)/v‖ ≤ 3/(im v)².\n2. ψ(w) via the recurrence.\n3. The log difference |log(w+2) − log w₀| ≤ 2·(|(w+2)−w₀|/|w₀|): the |log(1+u)| ≤ 2|u| bound — Mathlib lemma? `Complex.norm_log_one_add_le`? Let me search: there's `Complex.abs_log_one_add_le`? or `Complex.norm_log_one_add_le (h : ‖z‖ ≤ 1/2) : ‖log (1+z)‖ ≤ 2‖z‖`? I recall something like `Complex.norm_log_one_add_le (hz : ‖z‖ < 1) : ‖log (1 + z)‖ ≤ -Real.log (1 - ‖z‖)`? and then −log(1−x) ≤ 2x for x ≤ 1/2 via Real.log... Let me check what exists.\n   Actually the log DIFFERENCE: log(w+2) − log w₀ = log((w+2)/w₀)? — needs the arg care (Complex.log of a ratio: log a − log b = log(a/b) requires... Complex.log_sub? no — log(a/b) = log a − log b when... in ℂ this needs the arguments to not cross the slit. The safe form: log(w+2) − log w₀ = log(1 + u) where u = (w+2−w₀)/w₀ — the identity log(1+u) = log(w+2) − log(w₀) holds when...? Complex.log(1+u) = log(w+2) − log w₀ where 1+u = (w+2)/w₀: Complex.log_div? Hmm — Complex.log (a/b) = log a − log b requires re b ≠ 0 or... there's `Complex.log_div (ha : a ≠ 0) (hb : b ≠ 0)`? — not always true in ℂ (the arg wrap). BUT for our case: w+2 and w₀ both have im > 0 and re > 0 — they're in the right half-plane, both args in (−π/2, π/2), so the ratio's arg is in (−π, π) — no slit crossing: log(w+2) − log w₀ = log((w+2)/w₀) ✓ valid. Mathlib: `Complex.log_div (ha : a.re > 0)?`... there's `Complex.log_div_of...`? Hmm — or via log_mul_of... For safety: Complex.log_div_of_real? Let me search for what's available. Alternatively avoid the ratio: bound ‖log(w+2) − log w₀‖ directly via the FTC: log(w+2) − log w₀ = ∫_{w₀}^{w+2} dz/z along the straight segment (both in the right half-plane, segment stays in re ≥ 3/4... re(w+2) ≥ 3/4, re w₀ = 1: segment re ≥ 3/4 > 0 ✓): |∫ dz/z| ≤ |segment|·max|1/z| = 2.25·(1/(min re... |z| ≥ re z ≥ 3/4 along the segment): ≤ 2.25/(3/4) = 3?? too big — hmm: |1/z| ≤ 1/|z| ≤ 1/(t/2 − ...)|: |z| ≥ |im z| = t/2 ≥ 5 along the segment (im constant t/2!) — the segment from w₀ to w+2 has constant im = t/2 ✓ so |z| ≥ t/2 ≥ 5 ⟹ |∫| ≤ 2.25/5 = 0.45!! Clean — the FTC-along-the-segment bound: |log(w+2) − log w₀| = |∫_{segment} dz/z| ≤ |w+2−w₀|·sup|1/z| ≤ 2.25·(2/t) = 4.5/t ≤ 0.45 at t=10 ✓. The FTC: Complex integral along a segment of 1/z — Mathlib: `Complex...`? Hmm — path integrals in Lean are painful. Alternative: the identity via HasDerivAt + the fundamental theorem for line integrals... Mathlib has `Complex.integral_...`? Actually — simpler: use the real-parameter FTC: define g(y) = Complex.log(w₀ + y·(w+2−w₀)) for y ∈ [0,1] (real parameter): g' = (w+2−w₀)/(w₀ + y(w+2−w₀)) (chain rule, Complex.log differentiable off the slit — the segment has re ≥ 3/4 > 0 so all points in slitPlane ✓). Then log(w+2) − log w₀ = g(1) − g(0) = ∫₀¹ g'(y) dy (real FTC for ℂ-valued — intervalIntegral with complex integrand ✓ used in 5d: sum_eq_integral_add_integral_deriv is ℂ-valued ✓). Bound: ‖g'(y)‖ ≤ |w+2−w₀|/|w₀+y(w+2−w₀)| ≤ 2.25/(t/2) (im of the point = t/2 ✓ constant). ∫ ≤ 2.25·(2/t)·1 = 4.5/t. This is exactly the 5d pattern (the log FTC at LiReflect:724-729: `HasDerivAt (fun y : ℝ => Complex.log (w + y)) ((w+x)⁻¹)` ✓ SAME form). \n\nSo piece 6's log bound: ‖log(w+2) − log w₀‖ ≤ 4.5/t via the segment FTC (the 5d pattern, ~60 lines given the machinery exists).\n\nTotal piece 6 target: ‖(digamma (s/2) − digamma (s₀/2))/2‖ ≤ C₆ with C₆ = ½·(0.45 + 0.045 + 0.4 + 0.24)·... let me recompute with the /2: ½·1.585 = 0.7925. Set the target ≤ 1 (round). Actually — hold on, let me reconsider whether to include the shift terms for ALL w or to keep them only when needed... The uniform-shift form has the extra −1/w − 1/(w+1) terms costing 0.4 — fine (budget 2.185).\n\nHmm wait — actually, let me simplify FURTHER: apply digamma_stirling at v := w + 2 and v₀ := w₀ (direct, re w₀ = 1 > 0):\nψ(w) − ψ(w₀) = [ψ(w+2) − 1/w − 1/(w+1)] − ψ(w₀)\n = [log(w+2) − 1/(2(w+2)) + r_v] − 1/w − 1/(w+1) − [log w₀ − 1/(2w₀) + r₀]\n = [log(w+2) − log w₀] + [1/(2w₀) − 1/(2(w+2))] − 1/w − 1/(w+1) + [r_v − r₀].\n\nBounds (all with |·| ≥ t/2 on every point involved):\n- ‖log(w+2) − log w₀‖ ≤ 4.5/t.\n- ‖1/(2w₀) − 1/(2(w+2))‖ = ½·‖(w+2 − w₀)/(w₀(w+2))‖ ≤ ½·2.25/((t/2)(t/2)) = ½·2.25·4/t² = 4.5/t².\n- ‖1/w‖ ≤ 2/t; ‖1/(w+1)‖ ≤ 2/t.\n- ‖r_v‖ ≤ 3/(t/2)² = 12/t²; ‖r₀‖ ≤ 12/t².\n\nTotal: 4.5/t + 4.5/t² + 4/t + 24/t² ≤ (at t ≥ 10, t² ≥ 10t): 4.5/t + 0.45/t + 4/t + 2.4/t = 11.35/t ≤ 1.135 at t = 10. So ‖ψ(w)−ψ(w₀)‖ ≤ 11.35/t; half: 5.675/t ≤ 0.5675. TARGET: ‖(digamma (s/2) − digamma (s₀/2))/2‖ ≤ 6/t — hmm let me set: ≤ 5.7/t ≤ 0.57. Or just ≤ 1 for roundness. The assembly uses a specific constant; let me use ≤ 0.6 (safe) — hmm, actually let me just target ‖(ψ-diff)/2‖ ≤ 6/t (then 6/t ≤ 0.6 for t ≥ 10). Simpler: prove ‖(digamma (s/2) − digamma (s₀/2))/2‖ ≤ 6/t.\n\nHmm — one subtlety: digamma_stirling needs 0 < re: v = w+2: re v = σ/2 + 2 ≥ 3/4 ✓ (σ ≥ −5/2). v₀ = w₀: re = 1 ✓. And the |im| ≥ 1/2: t/2 ≥ 5 ✓.\n\nAlso the r_v bound: digamma_stirling gives ‖digamma v − log v + (1/2)/v‖ ≤ 3/(v.im)² = 3/(t/2)² = 12/t² ✓.\n\nLet me now write piece 6. Structure:\n\n```lean\n/-- Piece 6 (digamma difference): for σ ∈ [−5/2, 3], s = σ + it, t ≥ 10,\ns₀ = 2 + it: ‖(ψ(s/2) − ψ(s₀/2))/2‖ ≤ 6/t. Via the +2 shift into the\nright half-plane (re(w+2) ≥ 3/4), Zeta23's digamma_stirling at w+2 and\nw₀, the recurrence ψ(w) = ψ(w+2) − 1/w − 1/(w+1), and the segment-FTC\nlog bound (im constant t/2 ⟹ |∫ dz/z| ≤ 2.25·(2/t)). -/\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n      ≤ 6 / t := by\n  ...\n```\n\nComponents:\n(a) w := s/2, w₀ := (2+tI)/2 = 1 + (t/2)I. w₀'s form: (2 + tI)/2 = 1 + (t/2)I: by ring-ish. Let me define w₀ := 1 + (t/2)*I and show (2+t*I)/2 = w₀ by ring (field_simp): (2+tI)/2 = 1 + (t/2)I ✓ ring (char 0 field) ✓.\n(b) w.im = t/2 (s.im = t: (s/2).im = s.im/2 = t/2 ✓ simp [him]).\n(c) ‖w‖ ≥ t/2: |im w| = t/2 ≤ ‖w‖ (abs_im_le_norm).\n(d) The recurrence: digamma w = digamma (w+2) − w⁻¹ − (w+1)⁻¹ — from digamma_add_natCast (w) (hw : w.im ≠ 0) (2): digamma (w+2) = digamma w + Σ_{j<2} (w+j)⁻¹ = digamma w + w⁻¹ + (w+1)⁻¹. Need w.im ≠ 0 ✓ (t/2 ≥ 5). The sum: Finset.range 2 = {0,1}: (w+0)⁻¹ + (w+1)⁻¹ = w⁻¹ + (w+1)⁻¹ ✓ (Finset.sum_range_two? or sum_range_succ twice).\n(e) digamma_stirling at v = w+2: ‖digamma v − log v + (1/2)/v‖ ≤ 3/(v.im)² = 3/(t/2)²; re v = σ/2 + 2 ≥ 3/4 > 0 ✓; |im v| = t/2 ≥ 5 ≥ 1/2 ✓.\n(f) digamma_stirling at w₀: re = 1 > 0 ✓; ‖digamma w₀ − log w₀ + (1/2)/w₀‖ ≤ 3/(t/2)².\n(g) the log difference: ‖log(w+2) − log w₀‖ ≤ 4.5/t via segment FTC. This is the meaty part:\n```lean\n  have hseg : ∀ y : ℝ, y ∈ Set.uIcc (0:ℝ) 1 → (w₀ + y * ((w + 2) - w₀)).re ≥ 3/4 ∧ ...\n```\nHmm — w₀ + y·((w+2) − w₀): re = 1 + y·(σ/2 + 1) ∈ [1 − ...]: σ/2 + 1 ∈ [−1/4, 2]: re = 1 + y·(σ/2+1) ≥ 1 − 1/4 = 3/4 ✓ (y ∈ [0,1], σ/2+1 ≥ −1/4: re ≥ 1 − 1/4 = 3/4 ✓). im = t/2 (constant: im(y·(w+2−w₀)) = y·im(w+2−w₀) = y·0 = 0 since im(w+2) = im w₀ = t/2 ✓). So the segment point z(y) = w₀ + y·δ (δ := w+2−w₀) has re ≥ 3/4 (so ∈ slitPlane, z ≠ 0) and im = t/2 (so ‖z‖ ≥ t/2).\nThen log(w+2) − log w₀ = ∫₀¹ δ·z(y)⁻¹ dy (the chain-rule FTC): \ng(y) := Complex.log(z(y)): HasDerivAt g (δ·z(y)⁻¹) y: Complex.log's deriv: hasDerivAt_log (z ≠ 0, slitPlane membership): Complex.hasDerivAt_log (hz : z ∈ slitPlane)? The name: `Complex.hasDerivAt_log (hz : z ≠ 0)?` — hmm: Complex.log is differentiable on slitPlane: `Complex.hasDerivAt_log (hx : x ∈ slitPlane) : HasDerivAt log x⁻¹ x`? or `Complex.hasDerivAt_log (hx : x ≠ 0)`? For the slitPlane: I think there's `Complex.hasDerivAt_log_of_mem_slitPlane`? or log is analytic off (−∞, 0]. From 5d (LiReflect:725): `HasDerivAt (fun y : ℝ => Complex.log (w + y)) ((w+x)⁻¹) x` — they used `hslit : w + (x:ℂ) ∈ Complex.slitPlane` and presumably Complex.hasDerivAt_log. Let me check the exact name used there.\nThen the FTC: ∫₀¹ g' = g(1) − g(0) via intervalIntegral.integral_deriv_eq_sub (g cont, g' = ...) — for ℂ-valued: `intervalIntegral.integral_deriv_eq_sub (f cont...) (hderiv : ∀ x ∈ uIcc, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f')`: f(1) − f(0) = ∫₀¹ f' — name check: intervalIntegral.integral_deriv_eq_sub (hf : ContinuousOn f uIcc?) (hderiv : ∀ x ∈ interior, HasDerivWithinAt...) — 5d used `sum_eq_integral_add_integral_deriv` which is built on it. The direct: `intervalIntegral.integral_deriv_eq_sub (f f' a b) (hcont : ContinuousOn f (uIcc a b)) (hderiv : ∀ x ∈ uIoo a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' ...) : ∫ x in a..b, f' x = f b − f a` ✓ standard.\nThen ‖∫₀¹ δ·z⁻¹‖ ≤ ∫₀¹ ‖δ·z⁻¹‖ ≤ ∫₀¹ ‖δ‖·(2/t) = (2.25)·(2/t) = 4.5/t — via intervalIntegral.norm_integral_le_of_norm_le_const? `intervalIntegral.norm_integral_le_of_norm_le_const (h : ∀ x ∈ uIoc, ‖f x‖ ≤ C) : ‖∫ a..b f‖ ≤ C·|b−a|`? something like that (used in 5d presumably).\nThen ‖δ‖ = ‖w+2 − w₀‖ = ‖(s/2 + 2) − (1 + (t/2)I)‖ = ‖(σ/2 + 1) + 0·I‖·... = |σ/2 + 1| ≤ 2.25 (σ/2 ∈ [−1.25, 1.5]: σ/2+1 ∈ [−0.25, 2.5]: |·| ≤ 2.5 hmm: σ/2 ∈ [−5/4, 3/2]: σ/2 + 1 ∈ [−1/4, 5/2]: |σ/2+1| ≤ 5/2 = 2.5). So ‖δ‖ ≤ 2.5: ∫ ≤ 2.5·2/t = 5/t. Hmm — 2.5 not 2.25 (σ/2 up to 3/2 gives σ/2+1 up to 5/2). Fine: 5/t.\nLet me redo the totals with 5/t: log diff ≤ 5/t; 1/(2·) diff ≤ ½·‖δ‖·(2/t)² = ½·2.5·4/t² = 5/t²; 1/w + 1/(w+1) ≤ 2/t + 2/t = 4/t; r-pieces ≤ 24/t². Total: 5/t + 5/t² + 4/t + 24/t² ≤ 5/t + 0.5/t + 4/t + 2.4/t = 11.9/t (at t ≥ 10). Half: ≤ 5.95/t. Target: ‖(ψ-diff)/2‖ ≤ 6/t ✓.\n\n(h) The final assembly: ψ(w) − ψ(w₀) = [log(w+2) − log w₀] + [1/(2w₀) − 1/(2(w+2))] − w⁻¹ − (w+1)⁻¹ + [r_v − r₀] — via linear_combination with the recurrence + the two Stirling haves. Then the norm chain (norm_add_le etc.) + the per-piece bounds + t ≥ 10 arithmetic.\n\nThe algebra: from (d): ψ(w) = ψ(w+2) − w⁻¹ − (w+1)⁻¹. From (e): ψ(w+2) = log(w+2) − (1/2)/(w+2) + r_v where r_v := digamma v − log v + (1/2)/v (so digamma v = log v − (1/2)/v + r_v — wait: ‖digamma v − log v + (1/2)/v‖ ≤ 3/(im)²: set r_v := digamma v − Complex.log v + (1/2)/v: then digamma v = log v − (1/2)/v + r_v ✓ linear). Similarly r₀ := digamma w₀ − log w₀ + (1/2)/w₀. Then:\nψ(w) − ψ(w₀) = ψ(v) − w⁻¹ − (w+1)⁻¹ − ψ(w₀)\n = [log v − (1/2)/v + r_v] − w⁻¹ − (w+1)⁻¹ − [log w₀ − (1/2)/w₀ + r₀]\n = [log v − log w₀] − (1/2)/v + (1/2)/w₀ − w⁻¹ − (w+1)⁻¹ + r_v − r₀ ✓.\n\nNorm chain: ‖ψ(w) − ψ(w₀)‖ ≤ ‖log v − log w₀‖ + ½‖1/v − 1/w₀‖ hmm the (1/2)/v − (1/2)/w₀ = (1/2)·(1/v − 1/w₀): ‖·‖ ≤ ½·‖1/v − 1/w₀‖ = ½·‖(w₀−v)/(v·w₀)‖ = ½·‖w₀−v‖/(‖v‖‖w₀‖). w₀ − v = w₀ − (w+2) = −δ: ‖·‖ = ‖δ‖ ≤ 2.5. ‖v‖ ≥ t/2 (im v = t/2 ✓), ‖w₀‖ ≥ t/2 ✓. So ≤ ½·2.5/((t/2)²) = ½·2.5·4/t² = 5/t² ✓.\n‖w⁻¹‖ = 1/‖w‖ ≤ 2/t; ‖(w+1)⁻¹‖ ≤ 2/t (im(w+1) = t/2 ✓).\n‖r_v‖ ≤ 3/(t/2)² = 12/t²; ‖r₀‖ ≤ 12/t².\n\nThen the /2: ‖(ψ(w)−ψ(w₀))/2‖ = ½‖ψ(w)−ψ(w₀)‖.\n\nAnd the fold to 6/t: 5/t + 5/t² + 2/t + 2/t + 12/t² + 12/t² = 9/t + 29/t² ≤ 9/t + 29/(10t) = 9/t + 2.9/t = 11.9/t. Half: 5.95/t ≤ 6/t ✓.\n\nThis is a solid ~200-line build. Given the time (2:20 AM), let me go for it — it's mechanical given the pieces. Actually — one more check: Complex.hasDerivAt_log's exact form for the segment FTC. From LiReflect:725-729, they have `HasDerivAt (fun y : ℝ => Complex.log (w + (y:ℂ))) ((w + (x:ℂ))⁻¹) x` — let me read that part to copy the exact pattern.","signature":""},{"type":"text","text":"`digamma_stirling` gives ‖ψ(v) − log v + (1/2)/v‖ ≤ 3/(im v)² — piece 6 has a comfortable route. Checking the 5d segment-FTC pattern to copy for the log difference."},{"type":"tool_use","id":"Read_215","name":"Read","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiReflect.lean","offset":723,"limit":75},"extra_content":null}]