[{"type":"thinking","thinking":"The norm-summability of the digamma series: `Summable.of_norm_bounded_eventually (g := fun n => 2*‖z‖*(((n:ℝ)+1)^2)⁻¹) ...` inside — so `Summable (fun n => ‖1/((n:ℂ)+1) − 1/(z+n+1)‖)` follows from Summable.of_norm_bounded_eventually's conclusion... wait — Summable.of_norm_bounded_eventually (g summable) (h : ∀ᶠ n, ‖f n‖ ≤ g n) : Summable (fun n => ‖f n‖)? — NO: Summable.of_norm_bounded_eventually proves Summable f from ‖f‖ ≤ g. Hmm — so from summable_digamma_series I get Summable (term) but NOT directly Summable (‖term‖). For norm_tsum_le_tsum_norm I need Summable (fun n => ‖a_n‖). Get it by re-running the comparison: `Summable.of_norm_bounded_eventually (g := the 2‖z‖/(n+1)² one) (its summability) (the eventual bound)` — the g's summability is `h1.mul_left _`. So in my file: Summable (fun n => ‖a_n‖) := Summable.of_norm_bounded_eventually (g := fun n => 2*‖w‖*(((n:ℝ)+1)^2)⁻¹) (h1.mul_left _) (the same eventual bound). Hmm — but for MY tighter bound I need a different comparison (the A-split). My plan: ∑' ‖a_n‖ ≤ my bound — via tsum_le_tsum (my majorant) — needs my majorant summable AND ‖a_n‖ ≤ my majorant pointwise. My majorant: g n := ‖w‖ / ((n+1)·(re w + n + 1)) — summable? ≤ ‖w‖/(n+1)²·... for re w ≥ 2: (re w + n + 1) ≥ (n+1)·... no: re w + n + 1 ≥ n + 3 ≥ (n+1)·1: 1/((n+1)(re w+n+1)) ≤ 1/(n+1)² ✓ — so g n ≤ ‖w‖·(n+1)⁻² which is summable (the h1.mul_left pattern above) ⟹ g summable via Summable.of_nonneg_of_le. ✓ So:\n- Summable (fun n => ‖a n‖) via comparison with ‖w‖·(n+1)⁻² (using ‖a_n‖ ≤ ‖w‖/((n+1)(A+n+1)) ≤ ‖w‖/(n+1)² — wait: 1/((n+1)(A+n+1)) ≤ 1/(n+1)² ⟺ (n+1)² ≤ (n+1)(A+n+1) ⟺ n+1 ≤ A+n+1 ⟺ 0 ≤ A ✓ (A = re w ≥ 2 > 0)). \n- Then ∑' ‖a_n‖ ≤ ∑' g_n (tsum_le_tsum with both summable) and ∑' g_n = ‖w‖·Σ' 1/((n+1)(A+n+1)) (tsum_mul_left) and the Σ' of the kernel ≤ (1 + log N)/A + 1/N·... my split bound.\n\nFor the split-sum bound Σ'_n 1/((n+1)(A+n+1)) ≤ (1 + log N)/A + 1/N with N := ⌈A⌉₊:\nThe series terms are all ≥ 0 (A ≥ 2): Σ' = lim of partial sums... The cleanest Lean packaging: \nΣ'_n f_n = Σ_{n<N} f_n + Σ'_{n} f_{n+N} (tsum_eq_sum + tsum shift: `(tsum_eq_sum_add_tsum_nat_add`? there's `tsum_eq_sum_add_tsum_nat_add (k) (hf : Summable f) : ∑' n, f n = ∑ i ∈ range k, f i + ∑' n, f (n + k)` ✓ exists I believe).\n- head: Σ_{n=0}^{N−1} 1/((n+1)(A+n+1)) ≤ Σ 1/(A(n+1)) = H_N/A ≤ (1 + log N)/A (harmonic_le_one_add_log ✓).\n- tail: Σ'_n f_{n+N}: f_{n+N} = 1/((n+N+1)(A+n+N+1)) ≤ 1/(n+N+1)² hmm wait ≤ 1/((n+N)(n+N+1)) = telescope (1/(n+N) − 1/(n+N+1)): Σ' = 1/N. The telescope tsum: HasSum (fun n => 1/(n+N) − 1/(n+N+1)) (1/N) — via partial sums (Finset.sum_range_sub') + tendsto. Then Σ' f_{n+N} ≤ Σ' telescope = 1/N (tsum_le_tsum with summability from the telescope's HasSum ✓ and f's summability from... f_{n+N} ≤ telescope ⟹ summable via of_nonneg_of_le with the telescope summable (HasSum.summable)). And the ≤ of tsums: `tsum_le_tsum (h : ∀ n, f n ≤ g n) (hf : Summable f) (hg : Summable g)` ✓.\n- total: (1+log N)/A + 1/N with N = ⌈A⌉₊: 1/N ≤ 1/A (N ≥ A); log N ≤ log(A+1) (N ≤ A+1): so ≤ (2 + log(A+1))/A.\n\nThen ‖Σ' a_n‖ ≤ Σ' ‖a_n‖ ≤ ‖w‖·(2 + log(A+1))/A and ‖w‖/A ≤ ... for the FULL bound on ψ: ψ(w) = −γ − 1/w + Σ' a_n: ‖ψ(w)‖ ≤ γ + ‖w‖⁻¹ + ‖w‖/A·(2 + log(A+1)). With ‖w‖/A = ‖w‖/re w ≤ √(1 + (im w/re w)²) — for |im w| ≤ 5, re w ≥ 2: ≤ √(1+25/4) = √(29/4) < 3. So ‖ψ‖ ≤ γ + 1/2 + 3·(2 + log(A+1)) ≤ 1 + 0.5 + 6 + 3 log(‖w‖+1) ≤ 8 + 3·log(‖w‖+1). Fold to C·log(2+‖w‖): need γ + 0.5 + 6 + 3 log(‖w‖+1) ≤ C log(2+‖w‖): log(‖w‖+1) ≤ log(2+‖w‖) ✓; the constant 7.5 + eulerMascheroniConstant (γ < 1: is there a Mathlib bound on eulerMascheroniConstant? `Real.eulerMascheroniConstant_lt_one`? or lt_d9? check — there might be bounds: `Real.eulerMascheroniConstant_pos`? For safety: γ < 1 via some bound — grep at build) ≤ C log(2+‖w‖): take C := 20: need γ + 1/2 + 6 + 3 log(‖w‖+1) ≤ 20 log(2+‖w‖): since log(2+‖w‖) ≥ log 4 (‖w‖ ≥ re w ≥ 2) > 1.38: 7.6 ≤ 5.5·1.38·... 7.6/1.38 ≈ 5.5: so 7.6 ≤ 6·log(2+‖w‖) when log ≥ 7.6/6 = 1.27: log 4 = 1.386 ✓: so ≤ 6 log(2+‖w‖) + 3 log(‖w‖+1)·... ≤ 6 log(2+‖w‖) + 3 log(2+‖w‖)·... hmm 3 log(‖w‖+1) ≤ 3 log(2+‖w‖)·(log(‖w‖+1) ≤ log(2+‖w‖) ✓ direct). So total ≤ (6+3)·... wait: γ + 1/2 + 6 + 3 log(‖w‖+1) ≤ 6·log(2+‖w‖) + 3·log(2+‖w‖)?? the constant 7.6 ≤ 6·1.27 = 7.6 ✓ hmm tight: use 10 for the constant part: γ + 6.5 ≤ 10·log(4)/1.386·... 10·1.386 = 13.86 ≥ 7.6 ✓ comfortable: ‖ψ‖ ≤ 10 log(2+‖w‖) + 3 log(2+‖w‖) = 13 log(2+‖w‖)... let me just take C := 20 and verify: γ + 6.5 + 3 log(‖w‖+1) ≤ 20 log(2+‖w‖): γ + 6.5 ≤ 20·1.38 = 27.6 − 3·log(‖w‖+1) — at ‖w‖ = 2: 27.6 − 3.3 = 24.3 ≥ 7.6 ✓; and the difference grows (20 log(2+x) − 3 log(1+x) → increasing for x ≥ ...: derivative 20/(2+x) − 3/(1+x) > 0 ⟺ 20(1+x) > 3(2+x) ⟺ 17x > −14 ✓). So C = 20 works. State: re w ≥ 2 ∧ |im w| ≤ 5 ⟹ ‖ψ w‖ ≤ 20·log(2+‖w‖). Hmm — actually wait: I should double-check whether 5e-v wants |im| ≤ 5 exactly — |t| < 10 ⟹ |im w'| = |t|/2 < 5 ✓. OK scope: |im w| < 5·... make it ≤ 5.\n\nActually — hold on. For (B) let me ALSO reconsider the super-cheap alternative ONE more time, because the Weierstrass route needs the γ constant bound + telescope + harmonic + tsum splits (~150 lines). The alternative: the EM-comparison route (5d's §6 variant) with the 1/a integral bound: ψ(w) − log w = [ψ(v) − log v] + [log v − log w − Σ 1/(w+j)], v = w + 1 (single step!): ψ(w) = ψ(w+1) − 1/w: so ψ(w) − log w = [ψ(w+1) − log(w+1)] + [log(w+1) − log w − 1/w] + ... — the single-step EM: log(w+1) − log w − 1/w = −[1/w − log(1+1/w)]: ‖·‖ ≤ ‖1/w‖²·2 (norm_log_one_add_sub_self_le: ‖log(1+z)−z‖ ≤ ‖z‖²(1−‖z‖)⁻¹/2 with ‖z‖ = ‖1/w‖ ≤ 1/2 ✓: ≤ ‖1/w‖²·(1/2)⁻¹/2 = ‖1/w‖² ≤ 1/4). And ψ(w+1) − log(w+1) — SAME problem at w+1. NO GAIN. The recurrence never helps going right. OK — Weierstrass for (B). Confirmed final.\n\nHmm — actually wait, ONE more: for (B), is there a slicker bound via the CONJUGATE and digamma_stirling at shifted im... no. And is there really no Mathlib bound for digamma on reals? Real.digamma? Mathlib has Real.digamma? no — only Complex.digamma I believe (there's Real.Gamma but Real.digamma? there IS `Real.digamma`? Hmm — I don't think so). Weierstrass. FINAL.\n\nLet me now also pin (A)'s statement: for the 5e-v application: w = s/2 with s on the circle's near-axis left part: re w ≤ 2 case — but (A) as stated for re w ≤ 2 AND dist ≥ 1/4. The 5e-i circle gives dist(R/2, ℤ) ≥ 1/4 for the CENTER crossing; the circle points nearby: s with |s − (−R)| ≤ 10-ish (|im s| < 10): s/2 + R/2 = (s+R)/2: |s + R| ≤ ... on the circle |s| = R with |im s| ≤ 10: |s + R|² = |s|² + 2R·re s + R²... hmm: |s+R| for s = Re^{iθ} near θ = π: s = −R + iε·...: |s + R| ≈ √(ε² + (R − √(R²−ε²))²) ≈ √(ε² + (ε²/2R)²) ≈ ε for small ε. So dist(s/2, −ℕ) ≥ dist(R/2, ℕ... the −ℕ for s/2 negative... |s/2 − (−m)| = |s/2 + m|: with R/2 ∈ [2k+1.25, 2k+1.5]: s/2 + m for m = 2k+1: ≈ (s+R)/2 − (R/2 − (2k+1)) — |s/2 + (2k+1)| ≥ |R/2 − (2k+1)| − |s+R|/2 ≥ 1/4 − |s+R|/2 — and |s+R| ≤ ~10: 1/4 − 5 < 0!! The dist condition FAILS for circle points that wander along the circle. Hmm!! Wait — s on the circle with |im s| < 10: s/2 + m where the nearest −ℕ point to s/2: s/2 ≈ −R/2 + i·(t/2): |s/2 + m|² = (re s/2 + m)² + (t/2)²: re(s/2) = −√(R²−t²)/2 ∈ [−R/2, −√(R²−100)/2] ⊂ [−R/2, −R/2 + 25/R·...]: √(R²−100) = R√(1−100/R²) ≥ R(1 − 50/R²·...) = R − 50/R: so re(s/2) ∈ [−R/2, −R/2 + 25/R]: re(s/2) + (2k+1) ∈ [−R/2 + 2k+1, −R/2 + 2k+1 + 25/R] = [2k+1 − R/2, ...] with R/2 ∈ [2k+1.25, 2k+1.5]: 2k+1 − R/2 ∈ [−0.5, −0.25]: so re(s/2)+(2k+1) ∈ [−0.5, −0.25 + 25/R]: |re(s/2)+(2k+1)| ≥ 0.25 − 25/R ≥ 1/8 for R ≥ 200 ✓. And for other m: |re(s/2)+m| ≥ 0.75 − 25/R ≥ 1/2 ✓. So dist(s/2, −ℕ) ≥ min(1/8, |t|/2·...) hmm also the im part: |s/2 + m| ≥ |re-part| ≥ 1/8 for ALL m ✓ (as long as R ≥ 200). So on the circle: dist(s/2, −ℕ) ≥ 1/8 for the near-axis part — GOOD, the condition holds with 1/8 (not 1/4) after the circle wiggle. So (A)'s hypothesis should be dist ≥ c with c ANY positive constant — state with (hw : ∀ m : ℕ, c ≤ ‖w + m‖) for a positive real c, conclusion ‖ψ w‖ ≤ C(c)·log(2+‖w‖)... the constant depends on c (the separated-sum's small-j term ≤ 1/c). To keep it simple: state with c as a parameter: ∀ (c : ℝ) (hc : 0 < c), (∀ m : ℕ, c ≤ ‖w + (m:ℂ)‖) → ‖ψ w‖ ≤ (something with 1/c)·log(2+‖w‖). The \"1/c\" enters the small-j terms (≤ 2/c of them? at most 2 j's with |re(w+j)| < c: term ≤ 1/c each: 2/c total) and the rest ≤ 2(4 + H_m) hmm — let me redo the (C) bound with general δ := c: term_j ≤ max(1/|re(w+j)|, 1/c) hmm — term_j ≤ 1/c always (dist condition) and ≤ 1/|re(w+j)| when...: the V-split: right side: j₀ term ≤ 1/c; j > j₀: ≤ 1/(j−j₀): Σ ≤ H_m: right ≤ 1/c + H_m; left ≤ 1/c + H_m: total ≤ 2/c + 2H_m ≤ 2/c + 2(1 + log m). So Σ ‖w+j‖⁻¹ ≤ 2/c + 2 + 2 log m. Fine — state with c.\n\nLet me now write the file. Three theorems + helpers:\n\n```\nNguyenRH1/LiDigammaLeft.lean — ii′-5e-ii (D-068 §1 C2):\n* `digamma_recip_sum_le` (C): the separated reciprocal sum bound:\n    for w with ∀ m : ℕ, c ≤ ‖w + ↑m‖ (c > 0) and j₀ = ⌈−re w⌉₊ < m:\n    Σ_{j<m} ‖w + ↑j‖⁻¹ ≤ 2/c + 2 + 2·log m.\n    [V-split at j₀; each side ≤ 1/c + H_m via the AP structure.]\n* `norm_digamma_le_of_dist` (A): re w ≤ 2 + the dist condition ⟹\n    ∃-free explicit C: ‖ψ w‖ ≤ C·log(2+‖w‖) — hmm the compactness constant D is existential! So (A)'s form: obtain D from compactness ONCE (a standalone lemma ∃ D, ∀ v ∈ K, ‖ψ v‖ ≤ D) then the main theorem with C depending on D... The final statement: ∃ C : ℝ, ∀ w, (re w ≤ 2 → (∀ m, c ≤ ‖w + ↑m‖) → ‖ψ w‖ ≤ C * log (2 + ‖w‖))·... hmm — with c fixed (say 1/8) and C existential: `∃ C : ℝ, 0 < C ∧ ∀ w : ℂ, w.re ≤ 2 → (∀ m : ℕ, (1/8:ℝ) ≤ ‖w + m‖) → ‖Complex.digamma w‖ ≤ C * Real.log (2 + ‖w‖)`. The existential C absorbs D ✓.\n* `norm_digamma_le_of_two_le_re` (B): explicit C = 20: 2 ≤ re w → |im w| ≤ 5 → ‖ψ w‖ ≤ 20·log(2+‖w‖).\n```\n\nHmm wait — for (A), do I want the C existential or explicit-with-D? For 5e-v's use: ∃ C is fine (the o(R) argument unfolds the existential once). But actually — hmm, can I AVOID the compactness-existential by bounding ψ on K = [3,4]×[−1/2,1/2] EXPLICITLY via the Weierstrass series?? ψ(v) for re v ∈ [3,4]: the series: ψ(v) = −γ − 1/v + Σ'_n a_n with ‖a_n‖ ≤ ‖v‖/((n+1)(re v + n + 1)) — re v ≥ 3: the (B)-type bound applies to v!! ‖ψ v‖ ≤ 20·log(2+‖v‖) — (B) at v (re v ≥ 3 ≥ 2 ✓, |im v| ≤ 1/2 ≤ 5 ✓). SO: (A)'s landing-zone bound can use (B) at v whenever |im w| < 1/2... and digamma_stirling when |im w| ≥ 1/2. NO COMPACTNESS NEEDED — fully explicit constant!! Order: (B) first (Weierstrass), then (A) using (B) at the shifted point for |im| < 1/2 and StirlingVert for |im| ≥ 1/2. \n\n(B) at v: needs |im v| ≤ 5: |im v| = |im w| < 1/2 ✓ ≤ 5 ✓. And re v ∈ [3, 4) ✓ ≥ 2 ✓.\n\nStirlingVert at v (|im v| ≥ 1/2): ‖ψ(v)‖ ≤ ‖log v‖ + 3/(im v)² + 1/(2‖v‖) ≤ (log‖v‖ + π) + 3/(1/4) + 1/4·... ‖v‖ ≥ re v ≥ 3: 1/(2‖v‖) ≤ 1/6: ≤ log‖v‖ + π + 12.2 ≤ log‖v‖ + 16: and log‖v‖ ≤ log(2+‖v‖) ≤ log(2 + ‖w‖ + m) ≤ log(2+‖w‖) + log(m+2)-ish... fold.\n\nSo revised plan:\n- (T) the telescope tail: `tsum_one_div_sub_self (N : ℕ) (hN : 1 ≤ N) : ∑' n : ℕ, ((1:ℝ)/(n+N) − 1/(n+N+1)) = 1/N` — via Finset.sum_range_sub' + tendsto.\n- (H) harmonic bound: harmonic_le_one_add_log ✓ Mathlib has it.\n- (B) `norm_digamma_le_of_two_le_re {w} (hwre : 2 ≤ w.re) (hwim : |w.im| ≤ 5) : ‖Complex.digamma w‖ ≤ 20 * Real.log (2 + ‖w‖)`.\n- (C) `digamma_recip_sum_le {w} {c} (hc : 0 < c) (hdist : ∀ m : ℕ, c ≤ ‖w + m‖) (m : ℕ) (hj₀ : ⌈−w.re⌉₊ < m)`: Σ_{j ∈ range m} ‖(w + ↑j)⁻¹‖ ≤ 2/c + 2 + 2*log m. Hmm — the j₀ condition: for the V-split I need to handle j₀ := ⌈−w.re⌉₊ possibly > m (re w very negative with small m?) — in (A) m is chosen large so j₀ < m ✓. For (C) standalone take the hypothesis hj₀ : ⌈−w.re⌉₊ ≤ m or < m — compute at use. Hmm — actually for re w ≥ 0: j₀ = ⌈−re w⌉₊ = 0 (Nat.ceil of a nonpositive is 0) ✓ then no left side. OK state (C) with j₀ := ⌈−w.re⌉₊ and hypothesis (hj₀ : j₀ ≤ m) — with the split range m = range j₀ ∪ Ico j₀ m (Finset.range_eq_Ico + sum_Ico_consecutive...: ∑ range m = ∑ range j₀ + ∑ Ico j₀ m via `Finset.sum_range_add_sum_Ico`? or range_eq_Ico + Ico_union_Ico_eq_Ico + sum_union disjoint: `Finset.sum_Ico_consecutive`? the simplest: Finset.range_eq_Ico : range n = Ico 0 n; Ico 0 m = Ico 0 j₀ ∪ Ico j₀ m (Ico_union_Ico_eq_Ico (h : a ≤ b) (h2 : b ≤ c)); sum over union disjoint (Ico_disjoint_Ico_consecutive). Then left sum = ∑ range j₀ and right = ∑ Ico j₀ m ✓.\n- (A) `norm_digamma_le_of_dist_nat` (explicit C): re w ≤ 2 → (∀ m, c ≤ ‖w+↑m‖) → ‖ψ w‖ ≤ C·log(2+‖w‖) with C := something like 12/c + 30 (explicit!): assemble from (C) + landing-zone bound ((B) or stirling). Let me compute the constant: ‖ψ w‖ ≤ ‖ψ v‖ + Σ ≤ [LZ] + 2/c + 2 + 2 log m where [LZ] = the landing-zone bound: |im| ≥ 1/2: ‖log v‖ + 16.2: ‖log v‖ ≤ log‖v‖ + π ≤ log‖v‖ + 4: [LZ] ≤ log‖v‖ + 21; |im| < 1/2: [LZ] ≤ 20 log(2+‖v‖) (B). Unified: [LZ] ≤ 21·log(2+‖v‖) (for the stirling case: log‖v‖ + 21 ≤ 21·log(2+‖v‖)? log‖v‖ ≤ log(2+‖v‖) ✓ and 21 ≤ 21·log(2+‖v‖) ⟸ log(2+‖v‖) ≥ 1 ⟸ ‖v‖ ≥ e − 1 ≈ 1.72: ‖v‖ ≥ re v ≥ 3 ✓). So [LZ] ≤ 21 log(2+‖v‖).\n  ‖v‖ ≤ ‖w‖ + m; m = ⌈2 − re w⌉₊ + 1 ≤ (2 − re w) + 2 = 4 − re w ≤ 4 + ‖w‖ (for re w ≤ 2: 2 − re w ≥ 0 ✓ Nat.ceil ≤ x+1 via Nat.ceil_lt_add_one (0 ≤ 2 − re w): ⌈2−re w⌉₊ < 2−re w+1 ⟹ m < 3 − re w + 1 = 4 − re w ✓); so ‖v‖ ≤ ‖w‖ + 4 + ‖w‖·... ‖v‖ = ‖w + m‖ ≤ ‖w‖ + m ≤ ‖w‖ + 4 + ‖w‖ = 2‖w‖ + 4: log(2+‖v‖) ≤ log(6+2‖w‖) = log 2 + log(3+‖w‖) ≤ 1 + (1 + log(2+‖w‖)) = 2 + log(2+‖w‖) (log(3+‖w‖) = log((2+‖w‖)·(3+‖w‖)/(2+‖w‖)) = log(2+‖w‖) + log((3+‖w‖)/(2+‖w‖)) ≤ log(2+‖w‖) + log(3/2) ≤ log(2+‖w‖) + 1 ✓ hmm log(3/2) ≤ 1/2). Let me just: 6+2‖w‖ = 2(3+‖w‖) and 3+‖w‖ ≤ 2(2+‖w‖) ⟹ 6+2‖w‖ ≤ 4(2+‖w‖) ⟹ log(2+‖v‖) ≤ log 4 + log(2+‖w‖) ≤ 2 + log(2+‖w‖) (log 4 < 1.39 < 2). And log m ≤ log(4+‖w‖) ≤ log(2(2+‖w‖)) = log 2 + log(2+‖w‖) ≤ 1 + log(2+‖w‖).\n  Assemble: ‖ψ w‖ ≤ 21·(2 + log(2+‖w‖)) + 2/c + 2 + 2·(1 + log(2+‖w‖)) = 42 + 21 log(2+‖w‖) + 2/c + 4 + 2 log(2+‖w‖) = (46 + 2/c) + 23 log(2+‖w‖). Fold into C·log(2+‖w‖): need (46 + 2/c) ≤ C₀·log(2+‖w‖): ‖w‖ ≥ c (dist condition at m=0: ‖w‖ ≥ c) ⟹ log(2+‖w‖) ≥ log(2+c) — hmm for tiny c that's log 2 ≈ 0.69: (46 + 2/c) ≤ C₀·log(2+c) with c = 1/8: 46+16 = 62 ≤ C₀·log(2.125) = C₀·0.754 ⟹ C₀ ≥ 82.2: take C₀ := 70/c·... 62/0.754 ≈ 82.2 ≤ 84/c? 84/(1/8)... let me just take the final constant as an expression: C := 46 + 2/c + 23/log(2+c)... ugly. ALTERNATIVE: state the conclusion as ‖ψ w‖ ≤ (46 + 2/c) + 23·log(2+‖w‖) — the affine form! For 5e-v's use (‖ψ(s/2)‖ ≤ C log R for large R): the affine form ≤ (46+2c⁻¹+23)·log(2+‖w‖) for ‖w‖ ≥ ... any fixed lower bound on ‖w‖ gives the fold; in 5e-v ‖w‖ ≈ R/2 large ✓. But cleaner to just deliver the affine form and let 5e-v fold. Hmm — or deliver BOTH: the affine theorem + a folded corollary with explicit C(c) := (46 + 2/c + 23)/log(2+c)·... Let me deliver the affine form:\n  `norm_digamma_le_of_dist_nat {c : ℝ} (hc : 0 < c) {w : ℂ} (hwre : w.re ≤ 2) (hdist : ∀ m : ℕ, c ≤ ‖w + (m:ℂ)‖) : ‖Complex.digamma w‖ ≤ (46 + 2/c) + 23 * Real.log (2 + ‖w‖)`.\n  Hmm wait — actually for 5e-v I realize I should double check the constant needs... 5e-v: |F| ≤ ... + ½|ψ(s/2)| + ... on the circle: ½[(46+2/c) + 23 log(2+‖w‖)] with ‖w‖ ≤ R: ≤ ½(46+16) + 11.5·log(2+R) = O(log R) ✓ the o(R) conclusion unaffected by any of these constants ✓. Affine form it is.\n\nNow — the (C) V-split details in Lean:\n```\ntheorem digamma_recip_sum_le {c : ℝ} (hc : 0 < c) {w : ℂ}\n    (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) {m : ℕ} (hm : ⌈-w.re⌉₊ + 1 ≤ m) :\n    ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2 / c + 2 + 2 * Real.log m := by\n  set j₀ := ⌈-w.re⌉₊ with hj₀\n  -- split: range m = range j₀ ∪ Ico j₀ m\n  rw [Finset.range_eq_Ico j₀?...] hmm: ∑ range m = ∑ Ico 0 j₀ + ∑ Ico j₀ m: Finset.sum_Ico_consecutive (f) (h1 : 0 ≤ j₀) (h2 : j₀ ≤ m)? — `Finset.sum_Ico_consecutive (f : ℕ → M) (h₁ : a ≤ b) (h₂ : b ≤ c) : ∑ i ∈ Ico a b, f i + ∑ i ∈ Ico b c, f i = ∑ i ∈ Ico a c, f i` ✓ exists. With range_eq_Ico: range m = Ico 0 m: \n  rw [Finset.range_eq_Ico, ← Finset.sum_Ico_consecutive _ (Nat.zero_le _) (Nat.lt_succ_iff.mp hm?)]\n```\nhm : j₀ + 1 ≤ m ⟹ j₀ ≤ m via (Nat.lt_succ_iff.mp hm).le... j₀ + 1 ≤ m ⟹ j₀ ≤ m ✓ omega-ish (Nat.le_of_lt_succ? j₀ < m from j₀+1 ≤ m: Nat.lt_of_succ_le hm : j₀ < m then .le). OK.\n\nThen:\n```\n  -- right side: ∑ Ico j₀ m\n  have hright : ∑ j ∈ Finset.Ico j₀ m, ‖(w + (j:ℂ))⁻¹‖ ≤ 1 / c + (1 + Real.log m) := by\n    -- first term ≤ 1/c (dist); rest ≤ 1/(j − j₀)\n    -- decompose: Ico j₀ m = {j₀} ∪ Ico (j₀+1) m (Finset.Ico_eq_cons? `Finset.Ico_succ_left`? there's `Finset.Ico_succ_left_eq_erase`? or Ico_insert... for naturals: Ico j₀ m = insert j₀ (Ico (j₀+1) m): `Finset.Ico_succ_left : Ico a (a+1)...` hmm: `Finset.Ico_succ_left_eq_insert_Ico`? I recall `Finset.Ico_insert_succ_left (h : a < b) : insert a (Ico (a+1) b) = Ico a b`? something. Or handle: ∑ Ico j₀ m f = f j₀ + ∑ Ico (j₀+1) m f via `Finset.sum_Ico_succ_top`? no that's the top. There's `Finset.sum_Ico_eq_sum_range`? and... Let me use: Finset.Ico_eq_cons? Hmm — the safest: Ico j₀ m = Ico j₀ (j₀+1) ∪ Ico (j₀+1) m via Ico_union_Ico_eq_Ico (le_refl) (j₀+1 ≤ m): sum split: ∑ Ico j₀ (j₀+1) = f j₀ (Ico_singleton: Ico a a+1 = {a}: `Finset.Ico_self_singleton`? `Finset.Ico_singleton : Ico a (a+1) = {a}`? I think `Finset.Ico_succ_singleton : Ico a (a+1) = {a}` ✓ something like that).\n    ...\n```\nThis is going to be fiddly. The individual term bounds:\n- j = j₀: ‖(w+↑j₀)⁻¹‖ = ‖w+↑j₀‖⁻¹ ≤ 1/c (hdist j₀ + inv_le_inv₀... 1/‖·‖ ≤ 1/c from ‖·‖ ≥ c: `inv_le_inv₀ (hc) (hdist...)`? inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a: so ‖w+j₀‖⁻¹ ≤ c⁻¹ ⟺ c ≤ ‖w+j₀‖ ✓ hdist: (inv_le_inv₀ (by positivity on ‖·‖: c ≤ ‖·‖ ⟹ 0 < c ≤ ‖·‖) hc).mpr (hdist j₀) ✓.\n- j ∈ Ico (j₀+1) m: ‖(w+↑j)⁻¹‖ ≤ 1/(j − j₀): ‖w+↑j‖ ≥ |re(w+↑j)| = re w + j (≥ 0 for j ≥ j₀: re w + j₀ ≥ 0 by ceil: j₀ = ⌈−re w⌉₊ ≥ −re w ⟹ re w + j₀ ≥ 0 ✓; for j ≥ j₀: re w + j ≥ 0 ✓): so ‖w+↑j‖ ≥ re w + j ≥ (j − j₀)·1... re w + j = (re w + j₀) + (j − j₀) ≥ j − j₀ ≥ 1 (j > j₀): and ≥ 0: so ‖(w+↑j)⁻¹‖ ≤ 1/(re w + j) ≤ 1/(j − j₀) — the last: re w + j ≥ j − j₀ ⟺ re w + j₀ ≥ 0 ✓: so 1/(re w + j) ≤ 1/(j−j₀) via one_div_le_one_div_of_le (0 < j−j₀) (re w + j ≥ j − j₀)·... careful with ℕ-vs-ℝ: (j − j₀ : ℕ) cast to ℝ: j ≥ j₀+1 ⟹ j − j₀ ≥ 1 ✓.\n  Then Σ_{j ∈ Ico (j₀+1) m} 1/(j−j₀): reindex i = j − j₀: Ico (j₀+1) m → Ico 1 (m − j₀): `Finset.sum_Ico_eq_sum_range`? : ∑ i ∈ Ico a b, f i = ∑ i ∈ range (b−a), f (a+i)?? `Finset.sum_Ico_eq_sum_range : ∑ i ∈ Finset.Ico m n, f i = ∑ i ∈ Finset.range (n - m), f (m + i)` ✓ exists. So the sum = Σ_{i ∈ range (m − j₀ − 1)} 1/((i + 1) − ...): j = j₀+1+i: j − j₀ = i+1: = Σ_{i < m−j₀−1} 1/(i+1) = harmonic(m−j₀−1) ≤ 1 + log(m−j₀−1) ≤ 1 + log m (harmonic_le_one_add_log + mono) ✓.\n- left side similar with j₀−1−j.\n\nThe cast juggling with ℕ subtraction j − j₀ (Nat) → ℝ: ((j − j₀ : ℕ) : ℝ) = j − j₀ via Nat.cast_sub (j₀ ≤ j) ✓.\n\nThis is all standard but lengthy. Total file estimate: (T) telescope ~40, (B) ~150, (C) ~120, (A) ~120. ~430 lines. That's a big chunk for the remaining session — but the pacing directive says continue. Let me write it in pieces: (T) + (B) first (self-contained), compile; then (C) + (A), compile. Then build/audit/commit.\n\nLet me write (T) and (B) now.\n\nFor (T):\n```\n/-- The telescoping tail: ∑'_{n} (1/(n+N) − 1/(n+N+1)) = 1/N. -/\ntheorem tsum_one_div_sub_telescope (N : ℕ) (hN : 1 ≤ N) :\n    ∑' n : ℕ, ((1 : ℝ) / (n + N) − 1 / (n + N + 1)) = 1 / N := by\n  have hNR : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN  -- 0 < N\n  -- partial sums telescope\n  have hpartial : ∀ M : ℕ, ∑ n ∈ Finset.range M, ((1 : ℝ) / (n + N) − 1 / (n + N + 1))\n      = 1 / N - 1 / (M + N) := by\n    intro M\n    -- Finset.sum_range_sub' : ∑ i ∈ range n, (f i − f (i+1)) = f 0 − f n\n    have h := Finset.sum_range_sub' (fun n : ℕ => (1 : ℝ) / (n + N)) M\n    -- h : ∑ i ∈ range M, (f i − f (i+1)) = f 0 − f M\n    rw [h]  -- hmm the forms: f i − f(i+1) = 1/(i+N) − 1/((i+1)+N): (i+1)+N vs my i+N+1: i+N+1 = (i+1)+N by ring — the summand forms must match for rw... convert:\n    -- my sum: 1/(↑n + ↑N) − 1/(↑n + ↑N + 1): sum_range_sub' gives 1/(↑i + ↑N) − 1/(↑(i+1) + ↑N): ↑(i+1) + ↑N = ↑i + 1 + ↑N = (↑i + ↑N) + 1 ✓ push_cast/ring-equal — handle via a show-bridge:\n    ...\n```\nLet me structure hpartial via sum_range_sub' directly with f n := (1:ℝ)/(n + N) (n : ℕ cast): f (i+1) = 1/((i+1:ℕ) + N): the summand in my target: 1/(i+N) − 1/(i+N+1): note ((i+1 : ℕ) : ℝ) + N = (i:ℝ) + N + 1 by push_cast ✓. So:\n```\n  have hpartial : ∀ M : ℕ, ∑ n ∈ Finset.range M, ((1 : ℝ) / ((n : ℝ) + N) − 1 / ((n : ℝ) + N + 1))\n      = 1 / (N : ℝ) - 1 / ((M : ℝ) + N) := by\n    intro M\n    have h := Finset.sum_range_sub' (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N)) M\n    simp only at h  -- beta\n    rw [show ((0:ℕ) : ℝ) + (N:ℝ) = (N:ℝ) by simp] at h  -- f 0 = 1/(0 + N) = 1/N\n    -- h : ∑ i ∈ range M, (1/(↑i+↑N) − 1/(↑(i+1)+↑N)) = 1/↑N − 1/(↑M+↑N)\n    convert h using 2  -- hmm: the summand forms: mine 1/(↑n+↑N) − 1/(↑n+↑N+1) vs h's 1/(↑n+↑N) − 1/(↑(n+1)+↑N): ↑(n+1)+↑N = ↑n+↑N+1: congr per term:\n    · -- sum equality: congr 1: funext / sum_congr: the second terms' denominators equal:\n      apply Finset.sum_congr rfl\n      intro n _\n      push_cast\n      ring_nf  -- 1/(↑n+↑N+1) = 1/(↑(n+1)+↑N): both = 1/(↑n+↑N+1): congr 1; push_cast; ring\n      ...\n```\nHmm — convert/sum_congr per-term: 1/(↑n+↑N+1) = 1/(↑(n+1)+↑N): congr 1 then push_cast; ring: ↑(n+1) + ↑N = ↑n + ↑N + 1: push_cast [Nat.cast_add_one?]... `push_cast` handles: ↑(n+1) → ↑n + 1 then ring: ↑n + 1 + ↑N = ↑n + ↑N + 1 ✓. So per-term: `congr 1; push_cast; ring`. OK.\n\nThen the limit: HasSum via partial sums: HasSum f a := Tendsto (fun s : Finset ℕ => ∑ i in s, f i) atTop (𝓝 a) — use `hasSum_iff_tendsto_nat_of_nonneg`? : for f ≥ 0: HasSum f a ↔ Tendsto (fun n => ∑ i ∈ range n, f i) atTop (𝓝 a) ✓ exists I believe (`hasSum_iff_tendsto_nat_of_nonneg (hf : ∀ i, 0 ≤ f i)`). The nonneg: 1/(n+N) − 1/(n+N+1) ≥ 0: 1/(n+N+1) ≤ 1/(n+N) ⟺ n+N ≤ n+N+1 ✓ (one_div_le_one_div_of_le (pos) ...). Tendsto of 1/N − 1/(M+N) → 1/N − 0 = 1/N: Tendsto (fun M => 1/(M+N)) atTop (𝓝 0): `tendsto_one_div_add_atTop_nhds_zero_nat`? there are lemmas: `tendsto_one_div_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => 1/n) atTop (𝓝 0)` ✓ exists I think; for the shifted: 1/(M+N) ≤ 1/M → squeeze: `tendsto_of_tendsto_of_...`? squeeze_zero: `tendsto_of_tendsto_of_le_of_le`? or `squeeze_zero (hf : ∀ n, 0 ≤ f n) (hfg : ∀ n, f n ≤ g n) (hg : Tendsto g atTop (𝓝 0))`: with g := 1/M: tendsto_one_div_atTop_nhds_zero_nat — hmm exact name: `tendsto_one_div_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => 1 / n) atTop (𝓝 0)` — in Mathlib.Topology.Algebra.Order...? I'll find. Then Tendsto (1/N − 1/(M+N)) → 1/N − 0: tendsto_const_sub? `Tendsto.const_sub` ✓. Then sub_self... 1/N − 0 = 1/N: `sub_zero`.\nSo:\n```\n  have hnonneg : ∀ n : ℕ, (0:ℝ) ≤ 1 / ((n : ℝ) + N) − 1 / ((n : ℝ) + N + 1) := by\n    intro n\n    have h1 : (0:ℝ) < (n:ℝ) + N := by positivity  -- n + N > 0 since N ≥ 1: positivity with hNR in context? (n:ℝ) + ↑N: Nat.cast_nonneg + hNR: linarith [hNR, Nat.cast_nonneg n]... positivity might not see hNR: use: by have := Nat.cast_nonneg n; have := hNR; linarith — as a term: show (0:ℝ) < (n:ℝ) + N: by positivity fails without hNR visible? positivity uses context? no it doesn't use hypotheses. Use: by nlinarith? no: `by have h2 := hNR; have h3 := Nat.cast_nonneg (n : ℕ); linarith` — hmm in term: I'll write (by positivity) and fix to linarith-based if it fails.\n    have h2 : (n:ℝ) + N ≤ (n:ℝ) + N + 1 := by linarith\n    have h3 : 1 / ((n:ℝ) + N + 1) ≤ 1 / ((n:ℝ) + N) := one_div_le_one_div_of_le h1 h2\n    linarith [h3]\n  rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg |>.tsum_eq?]...\n```\nHmm — the final: I want ∑' = 1/N. Route: show HasSum f (1/N) then HasSum.tsum_eq. HasSum via hasSum_iff_tendsto_nat_of_nonneg hnonneg |>.mpr: goal Tendsto (fun M => ∑ n ∈ range M, f n) atTop (𝓝 (1/N)): rw the partial sums (hpartial): Tendsto (fun M => 1/N − 1/(M+N)) → 1/N − 0: Tendsto.sub_const? `Filter.Tendsto.sub_const (c) (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => f x − c) l (𝓝 (a − c))`? I want const − f: `Tendsto.const_sub (c) (h : Tendsto f l (𝓝 a)) : Tendsto (fun x => c − f x) l (𝓝 (c − a))` ✓ exists. Then the limit value c − 0 = 1/N: rewrite via sub_zero... assemble:\n```\n  have hlim0 : Tendsto (fun M : ℕ => (1 : ℝ) / ((M : ℝ) + N)) atTop (𝓝 0) := by\n    -- squeeze against 1/M\n    have h1 : Tendsto (fun M : ℕ => (1 : ℝ) / M) atTop (𝓝 0) := tendsto_one_div_atTop_nhds_zero_nat\n    have h2 : ∀ M : ℕ, (0:ℝ) ≤ 1 / ((M : ℝ) + N) := fun M => by positivity\n    have h3 : ∀ M : ℕ, 1 / ((M : ℝ) + N) ≤ 1 / M := by\n      intro M\n      by_cases hM : M = 0\n      · subst hM; simp [hNR...]  -- 1/(0+N) ≤ 1/0 = 0: 1/0 = 0 junk: 1/N ≤ 0?? FALSE! 1/0 = 0 in Lean (div by zero = 0): so 1/N ≤ 1/0 = 0 would need 1/N ≤ 0 — FALSE. Handle M = 0 separately: 1/(0+N) = 1/N and 1/0 = 0: the inequality 1/N ≤ 0 is FALSE — so my h3 is wrong at M = 0! Fix: use 1/(M+1) as the comparator: 1/(M+N) ≤ 1/(M+1) ⟺ M+1 ≤ M+N ⟺ 1 ≤ N ✓: and Tendsto 1/(M+1) → 0: the shifted one_div: `Tendsto (fun M => 1/(M+1)) atTop (𝓝 0)`: from tendsto_one_div_atTop_nhds_zero_nat.comp (tendsto_atTop_add_const_right?...): `tendsto_atTop_add_const_right atTop 1`? there's `tendsto_add_atTop_nat`? or: (tendsto_one_div_atTop_nhds_zero_nat).comp (tendsto_id...)... simpler: `tendsto_one_div_add_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => 1 / (n + c)) atTop (𝓝 0)`?? — I recall `tendsto_one_div_add_atTop_nhds_zero_nat` EXISTS (used for such shifts)! Let me assume and check.\n    exact squeeze_zero h2 h3 h1  -- squeeze_zero (hf : ∀ n, 0 ≤ f n) (hfg : ∀ n, f n ≤ g n) (hg : Tendsto g atTop (𝓝 0)) : Tendsto f atTop (𝓝 0) ✓ exists\n```\nWith the comparator 1/(M+1) and its known limit. Let me write h1 := tendsto_one_div_add_atTop_nhds_zero_nat (c := 1)? signature: maybe `tendsto_one_div_add_atTop_nhds_zero_nat : Tendsto (fun n : ℕ => 1 / (n + c)) atTop (𝓝 0)` — I'll check at build; fallback squeeze via 1/(M+1) ≤ ... whatever.\n\nThen:\n```\n  have hlim : Tendsto (fun M : ℕ => (1 : ℝ) / (N : ℝ) - 1 / ((M : ℝ) + N)) atTop (𝓝 (1 / (N : ℝ))) := by\n    have h := hlim0.const_sub (1 / (N : ℝ))  -- Tendsto (c − f) → c − 0\n    rwa [sub_zero] at h\n  have hHasSum : HasSum (fun n : ℕ => (1 : ℝ) / ((n : ℝ) + N) - 1 / ((n : ℝ) + N + 1)) (1 / (N : ℝ)) := by\n    rw [hasSum_iff_tendsto_nat_of_nonneg hnonneg]\n    -- goal Tendsto (fun M => ∑ range M f) (𝓝 (1/↑N))\n    convert hlim using 1  -- partial sums = the difference\n    ext M\n    exact hpartial M\n  exact hHasSum.tsum_eq\n```\n`hasSum_iff_tendsto_nat_of_nonneg` signature: `(hf : ∀ i, 0 ≤ f i) : HasSum f a ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)` ✓ I believe.\n\nNow (B):\n```\n/-- The Weierstrass-series digamma bound on the right half-plane:\n‖ψ(w)‖ ≤ 20·log(2+‖w‖) for re w ≥ 2, |im w| ≤ 5. (The re ≥ 2 split\nΣ'_n 1/((n+1)(A+n+1)) ≤ (1+log N)/A + 1/N with N = ⌈re w⌉₊: head by\nthe harmonic bound, tail by the telescope.) -/\ntheorem norm_digamma_le_of_two_le_re {w : ℂ} (hwre : 2 ≤ w.re) (hwim : |w.im| ≤ 5) :\n    ‖Complex.digamma w‖ ≤ 20 * Real.log (2 + ‖w‖) := by\n  -- w off the nonpositive integers (re ≥ 2)\n  have hcomp : w ∈ Complex.integerComplement := by\n    -- def: ∀ n : ℤ, w ≠ ↑n? or Nat: check the def — from the Zeta23 usage: integerComplement_add_ne_zero hz ((n:ℤ)+1) — so membership gives z + m ≠ 0 for m : ℤ-ish. The def: `Complex.integerComplement := {z | ∀ n : ℤ, z ≠ n}`? Let me handle via: intro pattern...\n    rw [Complex.integerComplement] -- def unfold? It's a def: {z : ℂ | ∀ n : ℤ, z ≠ n}? check\n    ...\n```\nHmm — need the integerComplement def. From the Series.lean usage: `Complex.integerComplement_add_ne_zero hz ((n : ℤ) + 1)` : z + (↑n + 1) ≠ 0 — so integerComplement membership unfolds to ∀ m : ℤ, z ≠ −m or z + m ≠ 0... Let me grep the def quickly when writing. Also note `digamma_series` is in namespace Zeta23.DigammaSeries — with `open Zeta23` it's DigammaSeries.digamma_series.\n\nThen:\n```\n  rw [DigammaSeries.digamma_series hcomp]  -- ψ w = −γ − 1/w + ∑' a_n\n  -- bound: ‖−γ − 1/w + Σ'‖ ≤ γ + ‖1/w‖ + ‖Σ'‖\n  ...\n```\nwith a_n := fun n : ℕ => 1/((n:ℂ)+1) − 1/(w+n+1).\n\nThe norm-summability of ‖a_n‖: via comparison with g₁ n := ‖w‖ * ((n+1:ℝ)²)⁻¹ hmm — or directly my split majorant. Let me define the majorant:\ng n := ‖w‖ / ((n:ℝ)+1) / ((w.re:ℝ) + n + 1) : ℝ — hmm let me use real division: g n := ‖w‖ / (((n:ℝ)+1) * (w.re + (n:ℝ) + 1)).\nFacts: 0 ≤ g n ✓; ‖a_n‖ ≤ g n:\n‖a_n‖ = ‖w/((n+1)(w+n+1))‖ [the identity: 1/(n+1) − 1/(w+n+1) = w/((n+1)(w+n+1)): field_simp needs (n+1:ℂ) ≠ 0 (Nat.cast_add_one_ne_zero ✓) and w+n+1 ≠ 0 (re(w+n+1) ≥ 3 > 0 ✓)] = ‖w‖/((n+1)·‖w+n+1‖) [norm_div, norm_mul, norm_natCast_add_one — the Zeta23 helper norm_natCast_add_one : ‖((n:ℂ)+1)‖ = (n:ℝ)+1 ✓ exists in Series.lean] ≤ ‖w‖/((n+1)·(re w + n + 1)) [‖w+n+1‖ ≥ re(w+n+1) = re w + n + 1: `Complex.abs_re_le_norm`? — the name: `Complex.abs_re_le_norm (z) : |z.re| ≤ ‖z‖` ✓ exists (RCLike.abs_re_le_norm). re(w+n+1) = w.re + n + 1: simp [add_re, natCast_re, one_re]. Then div_le_div_of_nonneg_left? hmm: ‖w‖/((n+1)‖w+n+1‖) ≤ ‖w‖/((n+1)(re w+n+1)) ⟺ denominator ↓: need (n+1)(re w+n+1) ≤ (n+1)‖w+n+1‖ and positivity: via `div_le_div_of_nonneg_left (ha : 0 ≤ ‖w‖) (hb : 0 < (n+1)(re w+n+1)) (h : (n+1)(re w+n+1) ≤ (n+1)‖w+n+1‖)`: div_le_div_of_nonneg_left (ha hb hbc : b ≤ c) : a/c ≤ a/b ✓ (from 5d usage). h: mul_le_mul_of_nonneg_left (re(w+n+1) ≤ ‖w+n+1‖: (abs_re_le_norm _) with re ≥ 0: abs_of_nonneg) ((n:ℝ)+1 ≥ 0) ✓.\nSummable g: g n ≤ ‖w‖·(n+1)⁻²: ((n+1)(A+n+1)) ≥ (n+1)² ⟹ g ≤ ‖w‖/(n+1)²: div_le_div_of_nonneg_left with (n+1)² ≤ (n+1)(A+n+1) ⟺ n+1 ≤ A+n+1 ⟺ 0 ≤ A ✓. Summable (‖w‖·(n+1)⁻²) := (the h1 from Zeta23's proof — rebuild: Real.summable_nat_rpow_inv.mpr (1 < 2) + the rpow_natCast bridge + summable_nat_add_iff 1 — clone ~8 lines from their proof). Then Summable g via Summable.of_nonneg_of_le (g ≥ 0) (g ≤ the summable) (its summability) ✓.\nSummable (fun n => ‖a_n‖) via Summable.of_nonneg_of_le (norm_nonneg) (‖a_n‖ ≤ g n) (Summable g) ✓.\nThen:\n‖∑' a_n‖ ≤ ∑' ‖a_n‖ (norm_tsum_le_tsum_norm hsummable_norm) ≤ ∑' g n (tsum_le_tsum (pointwise) hsummable_norm hgsummable).\n∑' g n = ‖w‖ * ∑' n, 1/((n+1)(A+n+1)) (tsum_mul_left? g n = ‖w‖ * kernel n: tsum_mul_left : ∑' (c * f) = c * ∑' f ✓).\nAnd the kernel bound: ∑' n, 1/((n+1)(A+n+1)) ≤ (1 + log N)/A + 1/N with N := ⌈A⌉₊:\n- summable kernel: ≤ 1/(n+1)² chain ✓ (same comparison).\n- split: ∑' n, kernel n = ∑_{n<N} kernel n + ∑' n, kernel (n+N) — `tsum_eq_sum_add_tsum_nat_add (k := N) (hf : Summable kernel)`? hmm — `tsum_eq_sum_add_tsum_nat_add (f) (k) (hf : Summable f) : ∑' n, f n = ∑ i ∈ range k, f i + ∑' n, f (n + k)`? I think it's `tsum_eq_sum_add_tsum_nat_add` with args (f k hf)... let me check at build; fallback Summable.sum_add_tsum_nat_add.\n- head: ∑_{n<N} 1/((n+1)(A+n+1)) ≤ ∑_{n<N} 1/(A·(n+1)) = (1/A)·H_N ≤ (1+A... (1/A)(1 + log N) [harmonic_le_one_add_log : harmonic N ≤ 1 + log N; harmonic N = ∑_{k ∈ range N} (k+1)⁻¹: my sum ∑_{n ∈ range N} 1/(A(n+1)) = (1/A)·∑ 1/(n+1): the harmonic def: harmonic N := ∑ i ∈ range N, (i+1)⁻¹? — the form (i+1)⁻¹ vs 1/(i+1): one_div... bridge via simp [one_div] or the def unfold. And per-term: 1/((n+1)(A+n+1)) ≤ 1/(A(n+1)) ⟺ A(n+1) ≤ (n+1)(A+n+1) ⟺ A ≤ A+n+1 ⟺ 0 ≤ n+1 ✓: one_div_le_one_div_of_le (pos) ...: careful the forms: 1/((n+1)*(A+n+1)) ≤ 1/(A*(n+1)): one_div_le_one_div_of_le (h1 : 0 < A*(n+1)) (h2 : A*(n+1) ≤ (n+1)*(A+n+1)) ✓.\n- tail: ∑' n, kernel (n+N) ≤ ∑' n, (1/(n+N) − 1/(n+N+1)) = 1/N: kernel (n+N) = 1/((n+N+1)(A+n+N+1)) ≤ 1/((n+N)(n+N+1)) = 1/(n+N) − 1/(n+N+1) [the telescope identity: 1/a − 1/(a+1) = 1/(a(a+1)): field_simp/ring with a ≠ 0, a+1 ≠ 0]: one_div_le_one_div_of_le: (n+N+1)(A+n+N+1) ≥ (n+N)(n+N+1) ⟺ n+N ≤ A+n+N ⟺ 0 ≤ A ✓. tsum_le_tsum with summability: telescope summable (HasSum from (T)) and kernel-shift summable (from summable kernel + summable_nat_add_iff). Then = 1/N via (T).\n- total: (1+log N)/A + 1/N; N = ⌈A⌉₊: A ≤ N (Nat.le_ceil) ⟹ 1/N ≤ 1/A (one_div_le_one_div_of_le); N ≤ A+1 (Nat.ceil_lt_add_one (0 ≤ A): ⌈A⌉₊ < A+1 ⟹ ≤ as reals: (N:ℝ) ≤ A+1) ⟹ log N ≤ log(A+1) (Real.log_le_log (0 < N) (N ≤ A+1)) ⟹ (1+log N)/A ≤ (1 + log(A+1))/A. So kernel tsum ≤ (1 + log(A+1))/A + 1/A = (2 + log(A+1))/A.\nThen: ‖∑' a_n‖ ≤ ‖w‖·(2 + log(A+1))/A = (‖w‖/A)·(2 + log(A+1)) with ‖w‖/A ≤ 3:\n‖w‖/re w: ‖w‖² = re² + im² ≤ re² + 25: (‖w‖/re)² ≤ 1 + 25/re² ≤ 1 + 25/4 = 29/4 ≤ 9 = 3²: so ‖w‖/re ≤ 3: via sq: (‖w‖ ≤ 3·re)²... prove ‖w‖ ≤ 3·w.re: ‖w‖² ≤ 9 re² ⟸ re²+25 ≤ 9re² ⟺ 25 ≤ 8re² ⟸ re ≥ 2: 8·4 = 32 ≥ 25 ✓: nlinarith [hnsq-ish]: ‖w‖^2 = w.re^2 + w.im^2 (normSq route as before); w.im² ≤ 25 (|im| ≤ 5 ⟹ im² ≤ 25: sq_abs + pow_le_pow_left₀); then ‖w‖ ≤ 3·re via le_of_pow_le_pow_left₀ (two_ne_zero) (by positivity: 0 ≤ 3·re) ((‖w‖^2 ≤ (3 re)^2)): (3re)² = 9re² ✓ nlinarith.\nSo ‖∑' a_n‖ ≤ 3·(2 + log(A+1)) = 6 + 3 log(A+1) ≤ 6 + 3 log(‖w‖+1) (A = re w ≤ ‖w‖: abs_re_le_norm + |re| = re (≥2>0): re ≤ ‖w‖ ✓: log(A+1) ≤ log(‖w‖+1) ✓ Real.log_le_log (0 < A+1) (A+1 ≤ ‖w‖+1)).\nAnd ‖ψ w‖ = ‖−γ − 1/w + Σ'‖ ≤ γ + ‖1/w‖ + ‖∑'‖: γ = eulerMascheroniConstant: need γ ≤ 1: Mathlib: `Real.eulerMascheroniConstant_lt_one`? grep at build; if missing use a coarse bound (there might be eulerMascheroniConstant_lt_...?). ‖1/w‖ = ‖w‖⁻¹ ≤ 1/2 (‖w‖ ≥ re ≥ 2).\nSo ‖ψ‖ ≤ 1 + 1/2 + 6 + 3 log(‖w‖+1) = 7.5 + 3 log(‖w‖+1) ≤ 20·log(2+‖w‖): the final fold: 7.5 + 3 log(‖w‖+1) ≤ 20 log(2+‖w‖): since log(‖w‖+1) ≤ log(2+‖w‖) ⟹ 3 log(‖w‖+1) ≤ 3 log(2+‖w‖): suffices 7.5 ≤ 17·log(2+‖w‖): log(2+‖w‖) ≥ log 4 (‖w‖ ≥ 2): log 4 = 2 log 2 ≥ 2·0.693 = 1.386 (log_two_gt_d9? `Real.log_two_gt_d9 : 0.6931471803 < log 2`? — there are gt/lt d9 lemmas: Real.log_two_gt_d9? or log_two_lt_d9 used earlier (lt). Is there log_two_gt_d9? I recall both exist: Real.log_two_gt_d9 : 0.6931471803 < Real.log 2 hmm — actually the pair: log_two_lt_d9 : log 2 < 0.6931471808 and log_two_gt_d9 : 0.6931471803 < log 2 — I'll check. Then 17·log(2+‖w‖) ≥ 17·2·log 2 ≥ 17·1.386 = 23.5 ≥ 7.5 ✓. So: 7.5 + 3 log(‖w‖+1) ≤ 3·2.5 + 3 log(2+‖w‖)?? just: 7.5 ≤ 17 log(2+‖w‖) from 17·1.386 ≥ 23.5 ≥ 7.5 ✓ linarith with the log facts; and 3 log(‖w‖+1) ≤ 3 log(2+‖w‖) ✓; total ≤ 20 log(2+‖w‖) ✓.\n\nHmm wait — eulerMascheroniConstant bound: if no Mathlib lemma, note the digamma_series has −(γ : ℂ): I need ‖(γ:ℂ)‖ = γ (norm_real; γ > 0? `Real.eulerMascheroniConstant_pos`?) and γ ≤ 1. If no bound exists in Mathlib — hmm — Zeta23's LiDigamma or others may have it. Grep both at build. Worst case: derive γ < 1 from... the series definition (hard). Surely Mathlib has bounds — I recall `Real.eulerMascheroniConstant_lt_one : eulerMascheroniConstant < 1`? or in the EulerMascheroni file with decimal bounds. Will check.\n\nThis is a LOT. Given the session length, let me write (T) + (B) first, compile, and if energy remains do (C) + (A). Actually — for 5e-v, both (A) and (B) are needed. Let me push through both but commit (T)+(B) at a green boundary first.\n\nActually, wait — let me reconsider the (C)+(A) necessity once more. In 5e-v, on the circle |s| = R_k:\n- logDeriv ΓR(s) for re s ∈ [−5/2·...]: hmm — actually what does the F-bound need at LEFT points with |t| ≥ 10? 5d's capstone handles re s ∈ [−5/2, 1/2] — but the circle's left part at |t| ≥ 10 has re s ∈ [−5/2·...]: the circle |s| = R with |t| ≥ 10: re s ∈ [−√(R²−t²)...]: for |t| ≥ 10, re s ranges over [−R, −√(R²−t²)]∪... no: |t| ≥ 10 with |s| = R: re s ∈ [−√(R²−10²)... hmm the circle point (σ, t) with σ² + t² = R²: for |t| ≥ 10: σ ∈ [−√(R²−100), √(R²−100)] — the full range including deep-left σ ≈ −√(R²−100) ≈ −R + 50/R. So the circle's points with |t| ≥ 10 include re s ≈ −R!! The 5d bound only covers re s ∈ [−5/2, 1/2]. For re s ∈ [−R, −5/2] with |t| ≥ 10: the FE-reflection (logDeriv_zeta_fe) directly: ζ′/ζ(s) = −ζ′/ζ(1−s) − bracket: 1−s has re ∈ [7/2, 1+R]: for re(1−s) ∈ [7/2, ...]: beyond 5c's range (re ≤ 7/2)!! Hmm — 5c covers re(1−s) ∈ [1/2, 7/2]: re(1−s) > 7/2 needs the Dirichlet bound (re > 2 fine ✓ 5e-vi in D-068). So for re s ∈ [−R, −5/2], |t| ≥ 10: ζ′/ζ(s) = −ζ′/ζ(1−s) − [logDeriv ΓR(1−s) + logDeriv ΓR(s)]: ζ′/ζ(1−s): re(1−s) ≥ 7/2: Dirichlet O(1) (re(1−s) ≥ 7/2 > 2 ✓). logDeriv ΓR(1−s): re > 0: RvM.logDeriv_Gammaℝ + digamma_stirling (|im(1−s)/2| = |t|/2 ≥ 5 ✓): O(log R) ✓. logDeriv ΓR(s): re s ∈ [−R, −5/2], |im s| ≥ 10: w = s/2: |im w| ≥ 5 ≥ 2 ⟹ **5d's left-plane bound applies** (‖ψ(w) − log w‖ ≤ 3)!! — but wait: 5d's bound is about ψ(w) − log w; the logDeriv ΓR(s) for re s ≤ 0 needs the identity logDeriv ΓR s = −(logπ)/2 + ½ψ(s/2) — 5d proved this only via the +4 shift for re s ∈ [−5/2, 1/2] (shift to re+4 ∈ [3/2, ...]). For re s ∈ [−R, −5/2]: s+4 has re ≤ 3/2 possibly ≤ 0 — the +4 shift doesn't reach re > 0!! Hmm!! So for re s ∈ [−R, −5/2] I need logDeriv ΓR(s) = −(logπ)/2 + ½ψ(s/2) at general re — i.e., the GENERAL identity logDeriv ΓR s = −(logπ)/2 + ½ψ(s/2) for s ∉ {0,−2,−4,...} (any negative re). Do I have that? 5d's logDeriv_Gammaℝ_shift : logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) for im ≠ 0. Iterate the shift m times? The general form: logDeriv ΓR s = logDeriv ΓR (s + 2m) − Σ... via ΓR(s+2m)/ΓR(s) = ∏... — the m-fold recurrence: from gamma_mul_prod (session 026!): Γ(s/2)·_{j<m}(s/2+j) = Γ(s/2+m) ⟹ ΓR(s)·...: ΓR(s+2m) = π^{−(s+2m)/2}Γ(s/2+m) = π^{−m}·π^{−s/2}·Γ(s/2)·∏_{j<m}(s/2+j)·... = π^{−m}·ΓR(s)·∏_{j<m}(s/2+j): so ΓR(s+2m) = π^{−m}·ΓR(s)·∏_{j<m}(s/2+j) for s/2 avoiding {0,...,−(m−1)}. Then logDeriv ΓR s = logDeriv ΓR (s+2m) − Σ_{j<m} (1/2)/(s/2+j)·... logDeriv of the product: logDeriv (∏_{j<m}(s/2+j)) s = Σ_j (1/2)/(s/2+j) = Σ_j 1/(s+2j). So logDeriv ΓR s = logDeriv ΓR (s+2m) − Σ_{j<m} 1/(s+2j)·... wait sign: ΓR(s) = π^m·ΓR(s+2m)/∏_j(s/2+j): logDeriv ΓR s = logDeriv ΓR(s+2m) − Σ_j (1/2)/(s/2+j) = −(logπ)/2 + ½ψ(s/2+m) − Σ_j 1/(s+2j) [logDeriv_Gammaℝ at s+2m with re(s+2m) = re s + 2m > 0 for m > −re s/2 ✓]. And ½ψ(s/2+m) − Σ_j 1/(s+2j) = ½[ψ(s/2) + Σ_j 1/(s/2+j)] − Σ_j 1/(s+2j)·... via digamma_add_natCast: ψ(s/2+m) = ψ(s/2) + Σ_{j<m} (s/2+j)⁻¹: ½ψ(s/2+m) − Σ 1/(s+2j): (s/2+j)⁻¹ = 2/(s+2j): ½Σ (s/2+j)⁻¹ = Σ 1/(s+2j) ✓ CANCELS EXACTLY: so logDeriv ΓR s = −(logπ)/2 + ½ψ(s/2) — the UNRESTRICTED identity (for s off the poles, im s ≠ 0 suffices). GOOD — so the general identity comes from: the m-fold ΓR product recurrence (gamma_mul_prod-based) + digamma_add_natCast + logDeriv_Gammaℝ at the shifted point. A small build (~80 lines, the m-fold version of 5d's logDeriv_Gammaℝ_shift — call it `logDeriv_Gammaℝ_eq_digamma` valid for im s ≠ 0, choosing m := ⌈max 0 (−re s/2)⌉₊ + 1 to land re(s+2m) > 0).\n   THEN: for re s ∈ [−R, −5/2], |im s| ≥ 10: logDeriv ΓR(s) = −(logπ)/2 + ½ψ(s/2) with |im(s/2)| ≥ 5 ≥ 2 ⟹ 5d's bound ‖ψ(w) − log w‖ ≤ 3 applies DIRECTLY (no (A) needed!) ⟹ ‖logDeriv ΓR s‖ ≤ log π + ½(3 + ‖log(s/2)‖) = O(log R) ✓✓.\n   And for |im s| < 10, re s ≈ −R (the near-axis left point): w = s/2 with |im w| < 5, re w ≈ −R/2: the near-axis case (A) — NEEDED (5d's bound needs |im w| ≥ 2; |im w| ∈ [2,5) is covered by 5d; |im w| < 2 needs (A)). Hmm — |im s| < 10 ⟹ |im w| < 5: split: |im w| ≥ 2 (i.e. |t| ∈ [4, 10)): 5d ✓; |im w| < 2 (|t| < 4): (A) needed. So (A) IS needed (for |t| < 4). And (B): logDeriv ΓR(1−s) at re(1−s) ≈ 1+R with |im(1−s)| = |t| < 10: w' = (1−s)/2: |im w'| < 5: |im w'| ≥ 1/2 ⟺ |t| ≥ 1: digamma_stirling ✓; |t| < 1: (B) needed. So both (A) and (B) confirmed needed, PLUS the general logDeriv ΓR identity (the m-fold shift — call it (G)).\n\nOK so 5e-ii = (G) + (B) + (C) + (A). Four pieces. (G) first (it's needed to EVALUATE logDeriv ΓR before any ψ-bound applies). Actually — (G) is needed at 5e-v's use sites; the (A)/(B) bounds are about ψ directly. Let me write (T) + (B) now, then (C) + (A), then (G). That's the full 5e-ii. This is a big session; keep going per the pacing rule, commit at green boundaries.\n\nLet me write (T) + (B) into LiDigammaLeft.lean now. Check eulerMascheroniConstant bounds + integerComplement def + one more name (tsum_eq_sum_add_tsum_nat_add) first.","signature":""},{"type":"text","text":"5e-ii needs four pieces: (G) the general logDeriv ΓR identity (m-fold shift), (B) the right-half Weierstrass bound, (C) the separated reciprocal sum, (A) the near-axis bound. Checking the last few signatures."},{"type":"tool_use","id":"Bash_245","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"eulerMascheroniConstant_lt\\|eulerMascheroniConstant_pos\\|eulerMascheroniConstant_le\" Mathlib/ 2>/dev/null | head -4; grep -rn \"def integerComplement\\|integerComplement =\" Mathlib/Analysis/SpecialFunctions/Complex/*.lean Mathlib/Analysis/SpecialFunctions/Gamma/*.lean 2>/dev/null | head -3; grep -rn \"tsum_eq_sum_add_tsum_nat_add\\|theorem sum_add_tsum_nat_add\" Mathlib/Topology/Algebra/InfiniteSum/ 2>/dev/null -r | head -3","description":"Check eulerMascheroni bounds, integerComplement, tsum split"},"extra_content":null}]