[{"type":"thinking","thinking":"Committed. Now §4 (A) + §5 (G) — the rest of 5e-ii. Let me write them carefully. I'll append to LiDigammaLeft.lean.\n\nFirst (A): `norm_digamma_le_of_dist_nat`. I need the digamma recurrence with pole-avoidance hypothesis (not im ≠ 0). Let me write a local `digamma_add_natCast'` with the weaker hypothesis, then (A), then (G).\n\nLet me draft the code carefully, watching all the gotchas banked this session:\n- Ascribe Nat.cast_nonneg haves.\n- Swapped add_le_add convention.\n- Pin nat-sub casts.\n- No bare `set` for things I need to compute with; explicit haves.\n- h3 : 0 ≤ ... needs explicit positivity ascriptions.\n\n**digamma_add_natCast'**: \n```\n/-- The digamma recurrence over a natural shift, pole-avoidance form. -/\ntheorem digamma_add_natCast' {w : ℂ} (hw : ∀ k : ℕ, w ≠ -(k : ℂ)) (n : ℕ) :\n    Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + (j : ℂ))⁻¹ := by\n  induction n with\n  | zero => simp\n  | succ k ih =>\n    have hne : ∀ m : ℕ, w + (k : ℂ) ≠ -(m : ℂ) := by\n      intro m h\n      -- w + ↑k = −↑m ⟹ w = −(↑k+↑m) = −↑(k+m): excluded by hw (k+m)\n      have h2 : w = -((k : ℂ) + (m : ℂ)) := by\n        have := h  -- w + ↑k = −↑m\n        -- w = −↑m − ↑k = −(↑k + ↑m)\n        have h3 := congrArg (· - (k : ℂ)) h  -- w = −↑m − ↑k\n        rwa [add_sub_cancel_right] at h3  -- h3 : w = −↑m − ↑k — wait: (w + ↑k) − ↑k = w: add_sub_cancel_right ✓: h3 : w = -↑m - ↑k\n        -- need −↑m − ↑k = −(↑k + ↑m): ring\n      ... \n```\nHmm: h : w + ↑k = −↑m: so w = −↑m − ↑k = −(↑k + ↑m) — and ↑(k+m) = ↑k + ↑m (Nat.cast_add): hw (k+m) : w ≠ −↑(k+m): apply hw (k+m); convert h2-form: goal w = −↑(k+m): from h: w = −↑m − ↑k = −(↑m + ↑k) = −(↑k + ↑m) = −↑(k+m): \n```\n      intro m h\n      apply hw (k + m)\n      -- goal: w = -↑(k+m)\n      have h3 : w = -(m : ℂ) - (k : ℂ) := by\n        have h4 := congrArg (· - (k : ℂ)) h\n        rwa [add_sub_cancel_right] at h4\n      rw [h3]\n      push_cast\n      ring\n```\n✓ (goal after rw [h3]: −↑m − ↑k = −↑(k+m): push_cast: ↑(k+m) → ↑k+↑m: −↑m − ↑k = −(↑k+↑m): ring ✓).\n\nThen:\n```\n  | succ k ih =>\n    have hne : ∀ m : ℕ, w + (k : ℂ) ≠ -(m : ℂ) := ...\n    have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) hne\n    rw [show w + ((k + 1 : ℕ) : ℂ) = (w + (k : ℂ)) + 1 by push_cast; ring, h1, ih,\n      Finset.sum_range_succ]\n    ring\n```\n(mirror of LiReflect's digamma_add_natCast which compiled ✓).\n\n**(A) norm_digamma_le_of_dist_nat**:\n```\n/-- **The near-axis left-plane digamma bound (A)**: for re w ≤ 2 and\ndist(w, −ℕ) ≥ c > 0, ‖ψ(w)‖ ≤ (46 + 2/c) + 23·log(2+‖w‖). Recurrence\nto re ∈ [3,4] + §3's sum bound + §2/StirlingVert at the landing point. -/\ntheorem norm_digamma_le_of_dist_nat {c : ℝ} (hc : 0 < c) {w : ℂ}\n    (hwre : w.re ≤ 2) (hdist : ∀ m : ℕ, c ≤ ‖w + (m : ℂ)‖) :\n    ‖Complex.digamma w‖ ≤ (46 + 2 / c) + 23 * Real.log (2 + ‖w‖) := by\n  -- pole-avoidance from the dist condition\n  have hpoles : ∀ k : ℕ, w ≠ -(k : ℂ) := by\n    intro k h\n    have h1 := hdist k\n    rw [h] at h1  -- ‖−↑k + ↑k‖ = 0: \n    simp at h1  -- ‖0‖ ≥ c contra c > 0: h1 : c ≤ ‖(-↑k : ℂ) + ↑k‖ = ‖0‖ = 0: simp: (−↑k + ↑k) = 0: neg_add_cancel? simp knows: add_neg... hmm (−(↑k) + ↑k) = 0: `neg_add_cancel`? or add_neg... let me: rw [h] at h1; simp at h1 — simp should reduce ‖(−(↑k:ℂ) + ↑k)‖ to 0 via add_neg_cancel? the form: (−↑k : ℂ) + ↑k: `neg_add_cancel`? that's −a + a = 0 ✓ simp lemma? neg_add_cancel is simp? maybe not. Robust: rw [h] at h1; rw [show (-(k:ℂ)) + (k:ℂ) = 0 by ring] at h1; simp at h1 (norm_zero) then linarith [hc, h1]?? h1 : c ≤ 0: linarith [hc, h1] ✓.\n  -- the shift count\n  set m := ⌈2 - w.re⌉₊ + 1 with hm_def\n  have hm_ge : (2 : ℝ) - w.re ≤ (m : ℝ) := by\n    have h := Nat.le_ceil (2 - w.re)\n    have h2 : ((⌈2 - w.re⌉₊ : ℕ) : ℝ) ≤ (m : ℝ) := by rw [hm_def]; push_cast; linarith [h]?? hmm: m = ⌈⌉₊ + 1: (↑m : ℝ) = ↑⌈⌉₊ + 1 ≥ (2−re w) + 1 ≥ (2−re w) ✓: \n    rw [hm_def]\n    push_cast\n    linarith [h]\n  have hm_lt : (m : ℝ) < (2 - w.re) + 2 := by\n    have h := Nat.ceil_lt_add_one (show (0:ℝ) ≤ 2 - w.re by linarith [hwre])  -- ⌈2−re⌉₊ < (2−re) + 1\n    have h2 : ((⌈2 - w.re⌉₊ : ℕ) : ℝ) < (2 - w.re) + 1 := by exact_mod_cast h\n    rw [hm_def]\n    push_cast\n    linarith [h2]\n  set v := w + (m : ℂ) with hv_def\n  have hvre : 3 ≤ v.re ∧ v.re < 4 := by\n    have h1 : v.re = w.re + (m : ℝ) := by\n      rw [hv_def]; simp [Complex.add_re, Complex.natCast_re]\n    rw [h1]\n    constructor <;> linarith [hm_ge, hm_lt]\n  have hvim : v.im = w.im := by\n    rw [hv_def]; simp [Complex.add_im, Complex.natCast_im]\n  -- j₀ for the sum bound\n  set j₀ := ⌈-w.re⌉₊ with hj₀\n  have hj₀m : j₀ + 1 ≤ m := by\n    -- j₀ ≤ max(0, −re w + 1): cases\n    by_cases hre : 0 ≤ -w.re\n    · have h1 : ((⌈-w.re⌉₊ : ℕ) : ℝ) < -w.re + 1 := by\n        have h := Nat.ceil_lt_add_one hre\n        exact_mod_cast h\n      -- j₀ + 1 ≤ m ⟸ −re w + 2 ≤ m: from hm_ge: m ≥ 2 − re w: hmm need m ≥ −re w + 2: hm_ge gives (m:ℝ) ≥ 2 − w.re: so (m:ℝ) ≥ 2 − re w and j₀ < −re w + 1 ⟹ j₀ + 1 < −re w + 2 ≤ m + 0·...: (j₀:ℝ) + 1 < (−re w + 1) + 1 = 2 − re w ≤ ↑m: so (j₀:ℝ)+1 < ↑m ⟹ j₀+1 ≤ m (nats): \n      have h2 : (j₀ : ℝ) + 1 < (m : ℝ) := by linarith [h1, hm_ge]\n      have h3 : j₀ + 1 < m := by  -- hmm strict in ℕ from real strict: exact_mod_cast h2 gives (↑(j₀+1):ℝ) < ↑m: j₀+1 < m: \n        have h4 : ((j₀ + 1 : ℕ) : ℝ) < (m : ℝ) := by\n          rw [Nat.cast_add_one]\n          linarith [h2]\n        exact_mod_cast h4\n      omega\n    · push Not at hre  -- −re w < 0: j₀ = 0\n      have h1 : ⌈-w.re⌉₊ = 0 := Nat.ceil_eq_zero.mpr (by linarith [hre])\n      rw [hj₀, h1]  -- goal 0 + 1 ≤ m: m ≥ 1: from hm_def: m = ⌈⌉₊ + 1 ≥ 1 ✓\n      omega\n  -- the recurrence\n  have hshift : Complex.digamma v = Complex.digamma w + ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹ := by\n    rw [hv_def]\n    exact digamma_add_natCast' hpoles m\n  -- the sum bound\n  have hsum := digamma_recip_sum_le hc hdist hj₀m  -- hmm digamma_recip_sum_le's hm : ⌈−w.re⌉₊ + 1 ≤ m: hj₀m is about j₀ = the set-var: the set j₀ := ⌈−re w⌉₊ makes them the same term ✓ — digamma_recip_sum_le hc hdist (hm := hj₀m)? the {m} implicit: our m ✓ the hypothesis (hm : ⌈-w.re⌉₊ + 1 ≤ m): hj₀m : j₀ + 1 ≤ m with j₀ set-to ⌈−re w⌉₊ — the set makes j₀ a local def equal to it; the expected form ⌈-w.re⌉₊ + 1 ≤ m vs hj₀m's j₀ + 1 ≤ m — defeq via hj₀ — hmm `set` replaces occurrences in goal/context but the NEW application digamma_recip_sum_le hc hdist hj₀m — the argument hj₀m : j₀ + 1 ≤ m must match the expected ⌈-w.re⌉₊ + 1 ≤ m — j₀ is a let-bound local def: isDefEq j₀ =?= ⌈-w.re⌉₊ — `set` introduces j₀ as a local definition with hj₀ : j₀ = ⌈-w.re⌉₊ — the defeq unfolds the local def? `set` introduces an fvar with a let-value — isDefEq CAN unfold it ✓ generally works. If not: rw [hj₀] at hj₀m first.\n  -- the landing-zone bound\n  have hLZ : ‖Complex.digamma v‖ ≤ 21 * Real.log (2 + ‖v‖) := by\n    by_cases him : 1 / 2 ≤ |v.im|\n    · -- StirlingVert\n      have hst := StirlingVert.digamma_stirling (by linarith [hvre.1] : (0:ℝ) < v.re) him\n      -- ‖ψ v‖ ≤ 3/(im v)² + ‖log v‖ + 1/(2‖v‖)\n      have hvnorm3 : 3 ≤ ‖v‖ := by\n        have h1 := Complex.abs_re_le_norm v\n        have h2 : |v.re| = v.re := abs_of_nonneg (by linarith [hvre.1])\n        rw [h2] at h1\n        linarith [hvre.1, h1]\n      calc ‖Complex.digamma v‖\n          = ‖(Complex.digamma v - Complex.log v + (1/2 : ℂ)/v) + Complex.log v - (1/2 : ℂ)/v‖ := by\n            congr 1; ring\n        _ ≤ ‖Complex.digamma v - Complex.log v + (1/2 : ℂ)/v‖ + ‖Complex.log v‖ + ‖(1/2 : ℂ)/v‖ := by\n            refine (norm_sub_le _ _).trans ?_\n            exact add_le_add_left (norm_add_le _ _) _  -- swapped convention\n        _ ≤ 3 / v.im^2 + (Real.log ‖v‖ + Real.pi) + (1/2)/‖v‖ := by\n            gcongr ... — explicit:\n            refine add_le_add (add_le_add hst (norm_log_le_of_one_le (by linarith [hvnorm3]))) ?_\n            rw [norm_div]\n            have h12 : ‖(1/2 : ℂ)‖ = 1/2 := by ... (the pattern from LiReflect)\n            rw [h12]\n        _ ≤ 21 * Real.log (2 + ‖v‖) := by\n            -- 3/(im v)² ≤ 3/(1/4) = 12; (1/2)/‖v‖ ≤ 1/6; log‖v‖ + π ≤ log(2+‖v‖) + 4: total ≤ log(2+‖v‖) + 16.2 + ... ≤ 21 log(2+‖v‖) ⟸ log(2+‖v‖) ≥ log 5 > 1.6 (‖v‖ ≥ 3): 21·1.6 = 33.6 ≥ 1·log + 16.2 ⟸ log(2+‖v‖)·20 ≥ 16.2 ⟸ 20·1.6 = 32 ≥ 16.2 ✓:\n            have him2 : v.im^2 ≥ 1/4 := by\n              calc v.im^2 = |v.im|^2 := by rw [sq_abs]\n                _ ≥ (1/2)^2 := pow_le_pow_left₀ (abs_nonneg _) him _\n                _ = 1/4 := by norm_num\n            have hlogv : Real.log ‖v‖ ≤ Real.log (2 + ‖v‖) := Real.log_le_log (by linarith [hvnorm3]) (by linarith)\n            have hlog5 : (0 : ℝ) ≤ Real.log (2 + ‖v‖) := Real.log_nonneg (by linarith [hvnorm3])\n            have hpi : Real.pi ≤ 4 := Real.pi_lt_d2.le.trans (by norm_num)\n            have h1 : 3 / v.im^2 ≤ 12 := by\n              rw [div_le_iff₀ (by linarith [him2] : (0:ℝ) < v.im^2)]\n              nlinarith [him2]\n            have h2 : (1/2 : ℝ) / ‖v‖ ≤ 1 := by\n              rw [div_le_one (by linarith [hvnorm3] : (0:ℝ) < ‖v‖)]\n              linarith [hvnorm3]\n            nlinarith [h1, h2, hlogv, hpi, hlog5, Real.log_nonneg (show (1:ℝ) ≤ 2 + ‖v‖ by linarith [hvnorm3])]\n    · -- |im v| < 1/2: the §2 bound\n      push Not at him\n      rw [hvim] at him  -- |w.im| < 1/2 ≤ 5: §2 needs |im v| ≤ 5: |v.im| < 1/2 ⟹ ≤ 5 ✓ via him: but (B) is stated with |w.im| ≤ 5 for the ARGUMENT v: |v.im| ≤ 5: from him : |v.im| < 1/2: .le.trans: \n      exact (norm_digamma_le_of_two_le_re (by linarith [hvre.1] : (2:ℝ) ≤ v.re)\n        (by linarith [him.le] : |v.im| ≤ 5)).trans (by\n        -- 20 log(2+‖v‖) ≤ 21 log(2+‖v‖): log ≥ 0 (‖v‖ ≥ 3)\n        have h : (0:ℝ) ≤ Real.log (2 + ‖v‖) := Real.log_nonneg (by linarith [hvre.1, Complex.abs_re_le_norm v] : (1:ℝ) ≤ 2 + ‖v‖)\n        nlinarith [h])\n  -- assemble\n  have hwnorm : ‖w‖ ≥ ... — need: m ≤ 4 + ‖w‖ and ‖v‖ ≤ 2‖w‖ + 4 and the log inequalities:\n  have hwm : (m : ℝ) ≤ 4 + ‖w‖ := by\n    have h1 : (m : ℝ) ≤ (2 - w.re) + 2 := hm_lt.le\n    have h2 : -w.re ≤ ‖w‖ := by\n      have h3 := Complex.abs_re_le_norm w\n      rwa [abs_le] at h3?? no: −re w ≤ |re w| ≤ ‖w‖: neg_le_abs (w.re) : −w.re ≤ |w.re| ✓ then trans with abs_re_le_norm:\n      exact (neg_le_abs w.re).trans (Complex.abs_re_le_norm w)\n    linarith [h1, h2]\n  have hvnorm : ‖v‖ ≤ 2 * ‖w‖ + 4 := by\n    rw [hv_def]\n    calc ‖w + (m : ℂ)‖ ≤ ‖w‖ + ‖(m : ℂ)‖ := norm_add_le _ _\n      _ = ‖w‖ + (m : ℝ) := by rw [RCLike.norm_natCast]\n      _ ≤ 2 * ‖w‖ + 4 := by linarith [hwm]\n  have hlogv_le : Real.log (2 + ‖v‖) ≤ 2 + Real.log (2 + ‖w‖) := by\n    -- 2 + ‖v‖ ≤ 6 + 2‖w‖ = 2(3+‖w‖) ≤ 4(2+‖w‖): log ≤ log 4 + log(2+‖w‖) ≤ 2 + log(2+‖w‖)\n    have h1 : 2 + ‖v‖ ≤ 4 * (2 + ‖w‖) := by linarith [hvnorm]\n    have h2 : Real.log (2 + ‖v‖) ≤ Real.log (4 * (2 + ‖w‖)) :=\n      Real.log_le_log (by linarith [hvre.1, ...] : (0:ℝ) < 2 + ‖v‖) h1\n    have h3 : Real.log (4 * (2 + ‖w‖)) = Real.log 4 + Real.log (2 + ‖w‖) :=\n      Real.log_mul (by norm_num : (4:ℝ) ≠ 0) (by positivity : (2 + ‖w‖) ≠ 0)\n    have h4 : Real.log 4 ≤ 2 := by\n      have h5 := Real.log_two_lt_d9.le  -- log 2 < 0.6932\n      have h6 : Real.log 4 = 2 * Real.log 2 := by\n        rw [show (4:ℝ) = 2^2 by norm_num, Real.log_pow]; push_cast; ring\n      linarith [h5, h6]\n    linarith [h2, h3, h4]\n  -- the sum bound form: 2/c + 2 + 2 log m ≤ ...: log m ≤ log(4+‖w‖) ≤ 1 + log(2+‖w‖):\n  have hlogm : Real.log m ≤ 1 + Real.log (2 + ‖w‖) := by\n    have h1 : (m : ℝ) ≤ 2 * (2 + ‖w‖) := by linarith [hwm]\n    have h2 : Real.log (m : ℝ) ≤ Real.log (2 * (2 + ‖w‖)) := by\n      apply Real.log_le_log (by positivity : (0:ℝ) < (m:ℝ)) h1\n      -- hmm 0 < ↑m: m ≥ 1 ✓: by exact_mod_cast (by omega : 1 ≤ m)?? m = ⌈⌉₊+1 ≥ 1: have hm1 : 1 ≤ m := by omega (from hm_def) — add\n    have h3 : Real.log (2 * (2 + ‖w‖)) = Real.log 2 + Real.log (2 + ‖w‖) :=\n      Real.log_mul (by norm_num) (by positivity)\n    have h4 : Real.log 2 ≤ 1 := Real.log_two_lt_d9.le.trans (by norm_num)\n    linarith [h2, h3, h4]\n  -- final assembly\n  rw [← hshift]  -- hmm: goal ‖ψ w‖: hshift : ψ v = ψ w + Σ: ‖ψ w‖ = ‖ψ v − Σ‖ ≤ ‖ψ v‖ + ‖Σ‖:\n  -- directly: ‖ψ w‖ = ‖ψ v − Σ‖: from hshift: ψ w = ψ v − Σ (by linear_combination hshift):\n  have hpsi : Complex.digamma w = Complex.digamma v - ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹ := by\n    linear_combination hshift\n  rw [hpsi]\n  calc ‖Complex.digamma v - ∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹‖\n      ≤ ‖Complex.digamma v‖ + ‖∑ j ∈ Finset.range m, (w + (j : ℂ))⁻¹‖ := norm_sub_le _ _\n    _ ≤ 21 * Real.log (2 + ‖v‖) + (2 / c + 2 + 2 * Real.log m) := add_le_add hLZ (hsum.trans' ...)...\n```\nwait hsum : ∑ ‖(w+↑j)⁻¹‖ ≤ 2/c + 2 + 2 log m (the SUM of norms) and I need ‖Σ (w+↑j)⁻¹‖ ≤ Σ ‖·‖⁻¹ (norm_sum_le) then hsum: ‖Σ‖ ≤ Σ‖·‖ ≤ 2/c+2+2 log m: `norm_sum_le` : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ ✓ exists. So:\n```\n    _ ≤ 21 * Real.log (2 + ‖v‖) + (2 / c + 2 + 2 * Real.log m) :=\n        add_le_add hLZ ((norm_sum_le _ _).trans hsum)\n    _ ≤ (46 + 2/c) + 23 * Real.log (2 + ‖w‖) := by\n        -- 21(2 + L) + 2/c + 2 + 2(1 + L) = 42 + 21L + 2/c + 2 + 2 + 2L = 46 + 2/c + 23L ✓ with L := log(2+‖w‖):\n        nlinarith [hlogv_le, hlogm, hc]  -- hlogv_le : log(2+‖v‖) ≤ 2 + L; hlogm : log m ≤ 1 + L: 21·log(2+‖v‖) ≤ 21(2+L) (mul by 21: monotone — nlinarith with the product 21·(...) linear ✓); 2 log m ≤ 2(1+L) ✓: total: 21(2+L) + 2/c + 2 + 2(1+L) = 46 + 2/c + 23L ✓ nlinarith closes (linear in the atoms log(2+‖v‖), log m, L, 1/c... 2/c as atom: the target has 2/c as written — the LHS has 2/c too ✓ same atom)\n```\nThe nlinarith: LHS = 21·log(2+‖v‖) + (2/c + 2 + 2·log m): with log(2+‖v‖) ≤ 2 + L and log m ≤ 1 + L: nlinarith multiplies hypotheses by constants? nlinarith can use them linearly: 21·log(2+‖v‖) ≤ 21·(2+L) requires multiplying hlogv_le by 21 — nlinarith/linarith: linarith does that ✓ (constant multiples of hypotheses) — but the RHS target: 46 + 2/c + 23·L — with 2/c written differently? The LHS's (2/c) and the goal's (2 / c) — same ✓. So linarith [hlogv_le, hlogm] should close: 21·logv + 2/c + 2 + 2·logm ≤ 21(2+L) + 2/c + 2 + 2(1+L) = 46 + 2/c + 23L ✓ linear ✓.\n\nHmm — one concern: `hsum` is about ∑ j ∈ range m, ‖(w + ↑j)‖⁻¹ — wait digamma_recip_sum_le's conclusion: ∑ j ∈ Finset.range m, ‖(w + (j : ℂ))⁻¹‖ ≤ 2/c + 2 + 2·log ↑m ✓ matches.\n\nAnd the hypothesis alignment: digamma_recip_sum_le {c} (hc) {w} (hdist) {m} (hm : ⌈-w.re⌉₊ + 1 ≤ m) — my call: digamma_recip_sum_le hc hdist (show ⌈-w.re⌉₊ + 1 ≤ m from ...) — the j₀ set-var issue: give the proof directly with the ceil form (not the j₀ alias) — since j₀ is `set`, the term ⌈-w.re⌉₊ displays as j₀ in context but the term I pass must have the literal form... `set j₀ := ⌈-w.re⌉₊ with hj₀` REPLACES occurrences — so writing ⌈-w.re⌉₊ in a new term still elaborates to the same underlying expression; set's fold is only presentational for the GOAL at set-time. The expected type of the (hm :) argument is ⌈-w.re⌉₊ + 1 ≤ m — passing hj₀m : j₀ + 1 ≤ m where j₀ is the set-local-def: isDefEq j₀ ≡ ⌈-w.re⌉₊ — set introduces j₀ as a new free variable with hj₀ : j₀ = ⌈-w.re⌉₊ — NOT a let-value (set uses `fvar` + the equation). So isDefEq does NOT automatically unfold j₀!! I need `rw [hj₀] at hj₀m` to convert hj₀m to the literal form, OR write the have with the literal form. Hmm — actually `set` in Lean4 Mathlib: introduces a local variable j₀ and hj₀ : j₀ = value, and replaces occurrences — the new fvar j₀ is opaque (not defeq to the value). So I DO need rw [hj₀] at hj₀m to get ⌈-w.re⌉₊ + 1 ≤ m for passing. Note: after rw [hj₀] at hj₀m, hj₀m : ⌈-w.re⌉₊ + 1 ≤ m ✓. Fine — handle.\n\nWait — actually in §3's proof I used `set j₀ := ⌈-w.re⌉₊ with hj₀` and then `recip_norm_le_right hdist hj₀ ...` passing hj₀ : j₀ = ⌈-w.re⌉₊ as the (hj₀ : j₀ = ⌈-w.re⌉₊) argument — matching ✓ (the lemma's hj₀ hypothesis is the equation j₀ = ⌈⌉₊ ✓). And it compiled ✓. OK so the same patterns work.\n\nNow (G). Let me draft it fully:\n\n```\n/-! ## 5. The general logDeriv ΓR identity (G) -/\n\n/-- logDeriv of a finite product of linear factors. -/\ntheorem logDeriv_prod_range_linear {s : ℂ} (hs : s.im ≠ 0) (m : ℕ) :\n    logDeriv (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s\n      = ∑ j ∈ Finset.range m, (1 / 2 : ℂ) / (s / 2 + (j : ℂ)) := by\n  induction m with\n  | zero => simp [logDeriv_const]  -- ∏ ∅ = 1: logDeriv (fun _ => 1) = 0; ∑ ∅ = 0: simp [logDeriv_const]: logDeriv_const : logDeriv (fun _ => a) = 0 — after simp the goal 0 = 0?? the goal: logDeriv (fun z => ∏ j ∈ range 0, ...) s = ∑ range 0 ...: range_zero, prod_empty, sum_empty: logDeriv (fun z => 1) s = 0: logDeriv_const is about logDeriv (fun _ => a) as a FUNCTION... its statement: logDeriv_const (a) : logDeriv (fun _ => a) = 0 — pointwise free: logDeriv (fun z => 1) s = (logDeriv (fun _ => 1)) s = 0 s = 0 — via congr_fun (logDeriv_const 1) s? simp [logDeriv_const] should handle ✓\n  | succ k ih =>\n    have hne : ∀ j : ℕ, (s / 2 + (j : ℂ)) ≠ 0 := by\n      intro j h\n      apply hs\n      have h2 : (s / 2).im = 0 := by\n        have h3 := congrArg Complex.im (congrArg (· / 2)?...)... \n```\nhmm — s/2 + ↑j = 0 ⟹ (s/2).im = 0 (since ↑j real): (s/2 + ↑j).im = (s/2).im + 0 = 0 ⟹ (s/2).im = 0 ⟹ s.im/2 = 0 ⟹ s.im = 0 contra hs:\n```\n    have hne : ∀ j : ℕ, (s / 2 + (j : ℂ)) ≠ 0 := by\n      intro j h\n      apply hs\n      have h1 : (s / 2 + (j : ℂ)).im = 0 := by rw [h]; simp\n      have h2 : (s / 2 + (j : ℂ)).im = s.im / 2 := by\n        simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im]\n      rw [h2] at h1\n      linarith [h1]  -- s.im/2 = 0 ⟹ s.im = 0 ✓ linarith: goal s.im = 0: from s.im/2 = 0: linarith closes (linear: s.im = 2·(s.im/2) = 0) ✓\n    have hprod_ne : (∏ j ∈ Finset.range k, (s / 2 + (j : ℂ))) ≠ 0 :=\n      Finset.prod_ne_zero_iff.mpr fun j _ => hne j\n    rw [Finset.prod_range_succ]\n    rw [logDeriv_mul s (Finset.prod_ne_zero_iff.mpr fun j _ => hne j) (hne k)\n      (by fun_prop : DifferentiableAt ℂ (fun z : ℂ => ∏ j ∈ Finset.range k, (z / 2 + (j : ℂ))) s)\n      (by fun_prop : DifferentiableAt ℂ (fun z : ℂ => z / 2 + (k : ℂ)) s)]\n    rw [ih]\n    -- logDeriv (fun z => z/2 + ↑k) s = (1/2)/(s/2+↑k):\n    have hfac : logDeriv (fun z : ℂ => z / 2 + (k : ℂ)) s = (1 / 2 : ℂ) / (s / 2 + (k : ℂ)) := by\n      have h1 : HasDerivAt (fun z : ℂ => z / 2 + (k : ℂ)) (1 / 2 : ℂ) s := by\n        have h2 := (hasDerivAt_id' s).div_const (2 : ℂ)\n        exact h2.add_const (k : ℂ)\n      rw [logDeriv_apply, h1.deriv]\n    rw [hfac, Finset.sum_range_succ]\n```\nHmm — logDeriv_mul : logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x — after rw [Finset.prod_range_succ] the goal's function is fun z => (∏ j ∈ range k, (z/2+↑j)) * (z/2+↑k) — logDeriv_mul's pattern fun z => f z * g z ✓ matches. Then the goal: logDeriv (∏-part) s + logDeriv (single) s = ∑ range (k+1): rw [ih] (the IH : logDeriv (∏-part) s = ∑ range k): goal ∑ range k + logDeriv single = ∑ range (k+1): rw [hfac, Finset.sum_range_succ]: RHS becomes ∑ range k + (1/2)/(s/2+↑k): both sides: [∑ range k] + (1/2)/(s/2+↑k) = [∑ range k] + (1/2)/(s/2+↑k) ✓ rfl-close by rw ✓.\n\nThe fun_prop for the product differentiability: DifferentiableAt ℂ (fun z => ∏ j ∈ range k, (z/2+↑j)) s — fun_prop should handle (div, add, const, prod) ✓.\n\nThen (G) main:\n```\n/-- **(G) the general logDeriv ΓR identity**: for im s ≠ 0,\nlogDeriv ΓR s = −(log π)/2 + ½ψ(s/2) — the m-fold shift landing re > 0\n(`gamma_mul_prod` + `digamma_add_natCast` + 5d's EventuallyEq machinery). -/\ntheorem logDeriv_Gammaℝ_eq {s : ℂ} (hs : s.im ≠ 0) :\n    logDeriv Complex.Gammaℝ s\n      = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma (s / 2) := by\n  set m := ⌈max 0 (-(s.re / 2))⌉₊ + 1 with hm_def\n  have hmge : (2 : ℝ) ≤ s.re + 2 * (m : ℝ) := by\n    have h1 : max 0 (-(s.re / 2)) ≤ (⌈max 0 (-(s.re / 2))⌉₊ : ℝ) := Nat.le_ceil _\n    have h2 : -(s.re / 2) ≤ max 0 (-(s.re / 2)) := le_max_right _ _\n    rw [hm_def]\n    push_cast\n    linarith [h1, h2]\n  have hres2 : 0 < (s + 2 * (m : ℂ)).re := by\n    have h1 : (s + 2 * (m : ℂ)).re = s.re + 2 * (m : ℝ) := by\n      simp [Complex.add_re, Complex.mul_re, Complex.natCast_re]  -- (2*↑m : ℂ).re = 2*↑m: mul_re: 2.re*↑m.re − 2.im*↑m.im: numerals simp ✓\n    rw [h1]\n    linarith [hmge]\n  -- the pointwise identity on U = {im ≠ 0}\n  have hU : IsOpen {z : ℂ | z.im ≠ 0} := isOpen_ne_fun Complex.continuous_im continuous_const\n  have hpt : ∀ z : ℂ, z.im ≠ 0 → Complex.Gammaℝ z\n      = (Real.pi : ℂ) ^ (m : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))\n        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by\n    intro z hz\n    -- recurrence side conditions\n    have hside : ∀ k : ℕ, k < m → z / 2 ≠ -(k : ℂ) := by\n      intro k _ h\n      apply hz\n      have h1 : (z / 2).im = 0 := by\n        have h2 := congrArg Complex.im h\n        -- h2 : (z/2).im = (−↑k).im = 0\n        simpa [Complex.neg_im, Complex.natCast_im] using h2\n      simp [Complex.div_ofNat_im] at h1  -- (z/2).im = z.im/2: h1 : z.im/2 = 0\n      linarith [h1]\n    have hrec := gamma_mul_prod (z / 2) m hside\n    -- ΓR(z+2m) = π^{−(z+2m)/2} Γ((z+2m)/2) = π^{−z/2}·π^{−m}·Γ(z/2+m)\n    have hG1 : Complex.Gammaℝ (z + 2 * (m : ℂ))\n        = (Real.pi : ℂ) ^ (-(z + 2 * (m : ℂ)) / 2) * Complex.Gamma ((z + 2 * (m : ℂ)) / 2) :=\n      Complex.Gammaℝ_def _\n    have harg1 : (-(z + 2 * (m : ℂ)) / 2) = -z / 2 - (m : ℂ) := by ring\n    have harg2 : (z + 2 * (m : ℂ)) / 2 = z / 2 + (m : ℂ) := by ring\n    -- the cpow split: π^{−z/2 − m} = π^{−z/2} · π^{−m}\n    have hpi : (Real.pi : ℂ) ^ (-z / 2 - (m : ℂ))\n        = (Real.pi : ℂ) ^ (-z / 2) * (((Real.pi ^ m : ℝ)) : ℂ)⁻¹ := by\n      have hlog : Complex.log (Real.pi : ℂ) = (Real.log Real.pi : ℂ) :=\n        (Complex.ofReal_log Real.pi_nonneg).symm\n      rw [Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,\n        Complex.cpow_def_of_ne_zero (by exact_mod_cast Real.pi_ne_zero : (Real.pi : ℂ) ≠ 0) _,\n        hlog]\n      have harg : (Real.log Real.pi : ℂ) * (-z / 2 - (m : ℂ))\n          = (Real.log Real.pi : ℂ) * (-z / 2) + ((-(m : ℝ) * Real.log Real.pi : ℝ) : ℂ) := by\n        push_cast\n        ring\n      rw [harg, Complex.exp_add, ← Complex.ofReal_exp]\n      -- Real.exp (−m·log π) = (π^m)⁻¹\n      have hexp : Real.exp (-(m : ℝ) * Real.log Real.pi) = (Real.pi ^ m)⁻¹ := by\n        have h1 : (-(m : ℝ) * Real.log Real.pi) = Real.log ((Real.pi ^ m)⁻¹) := by\n          rw [Real.log_inv, Real.log_pow]\n          ring\n        rw [h1, Real.exp_log (by positivity)]\n      rw [hexp]\n      push_cast\n      ring  -- hmm: ↑(π^m)⁻¹ vs ((↑π)^m)⁻¹: ofReal_pow/inv: push_cast normalizes ↑(π^m) → (↑π)^m: the goal: exp-form LHS already rewritten... let me end with: rw [hexp]; push_cast; ring — the goal at that point: (π:ℂ)^(−z/2) * ↑(Real.exp (−m log π)) = (π:ℂ)^(−z/2) * ↑((π^m)⁻¹): after rw [hexp]: RHS ↑( (π^m)⁻¹ ): push_cast turns it into ((↑π)^m)⁻¹: goal: π^(−z/2) * ((↑π)^m)⁻¹ = π^(−z/2) * ((↑π)^m)⁻¹ ✓ rfl — ring closes or the rw [hexp] + push_cast leaves syntactically equal sides ⟹ ring closes.\n    -- assemble ΓR(z+2m) = (π^m)⁻¹ · ΓR z · ∏\n    have hG2 : Complex.Gammaℝ (z + 2 * (m : ℂ))\n        = (((Real.pi ^ m : ℝ) : ℂ))⁻¹ * Complex.Gammaℝ z * ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by\n      rw [hG1, harg1, harg2, hpi, Complex.Gammaℝ_def]\n      -- ΓR z = π^{−z/2} Γ(z/2): unfold; hrec : Γ(z/2) * ∏ = Γ(z/2 + ↑m): substitute Γ(z/2+m) = Γ(z/2)·∏ via hrec.symm? hrec : Γ(z/2) * ∏ j ∈ range m, (z/2+↑j) = Γ(z/2+↑m): I need Γ(z/2+↑m) = Γ(z/2)·∏: rw [← hrec]:\n      rw [← hrec]\n      ring\n    -- solve for ΓR z: ΓR z = π^m · ΓR(z+2m) / ∏\n    have hPne : (∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) ≠ 0 := by\n      apply Finset.prod_ne_zero_iff.mpr\n      intro j _\n      intro h\n      apply hz\n      have h1 : (z / 2 + (j : ℂ)).im = 0 := by rw [h]; simp\n      simp [Complex.add_im, Complex.natCast_im, Complex.div_ofNat_im] at h1\n      linarith [h1]\n    have hπne : ((Real.pi ^ m : ℝ) : ℂ) ≠ 0 := by\n      exact_mod_cast pow_ne_zero m Real.pi_ne_zero\n    rw [eq_div_iff hPne]  -- goal: ΓR z * ∏ = π^m * ΓR(z+2m)\n    rw [hG2]\n    -- goal: ΓR z * ∏ = π^m * ((π^m)⁻¹ * ΓR z * ∏) = (π^m · (π^m)⁻¹)·(ΓR z · ∏) = ΓR z * ∏: \n    rw [show (Real.pi : ℂ) ^ (m : ℂ) = ((Real.pi ^ m : ℝ) : ℂ) by\n      rw [Complex.cpow_natCast]; push_cast; ring]  -- hmm (π:ℂ)^(↑m) = ↑(π^m): cpow_natCast: x^(↑n) = x^n: then ↑(π^m) vs (π:ℂ)^m: push_cast: ↑(π^m) → (↑π)^m ✓ then ring? the two sides (↑π)^m and ↑(π^m): push_cast turns ↑(π^m) into (↑π)^m: rfl — hmm the show's LHS is cpow (π:ℂ)^(↑m:ℂ) and RHS ↑(π^m): rw [Complex.cpow_natCast] turns LHS into (π:ℂ)^m: goal (π:ℂ)^m = ↑(π^m): push_cast turns RHS ↑(π^m) into (↑π)^m: rfl — so `by rw [Complex.cpow_natCast]; push_cast` — push_cast closes rfl? if both sides identical after push_cast — push_cast closes rfl goals? no — need exact/rfl: `by rw [Complex.cpow_natCast]; exact_mod_cast rfl`?? — simplest: by rw [Complex.cpow_natCast, ← Complex.ofReal_pow]?? — ↑(π^m) = (↑π)^m via `Complex.ofReal_pow : ↑(x^n) = (↑x)^n` ✓: so: rw [Complex.cpow_natCast, Complex.ofReal_pow] — LHS (π:ℂ)^m, RHS ↑(π^m) → after rw [Complex.ofReal_pow] the RHS becomes (↑π)^m: both sides (π:ℂ)^m ✓ rfl-close ✓. Wait direction: ofReal_pow : (↑(x^n) : ℂ) = (↑x)^n: rw [← Complex.ofReal_pow] turns (↑π)^m into ↑(π^m)... my show's equation: (π:ℂ)^(m:ℂ) = ↑(π^m): rw [Complex.cpow_natCast] : LHS (π:ℂ)^(↑m) → (π:ℂ)^m: goal (π:ℂ)^m = ↑(π^m): rw [← Complex.ofReal_pow]: pattern (↑x)^n: LHS (π:ℂ)^m matches with x := π: → ↑(π^m): goal ↑(π^m) = ↑(π^m) rfl ✓. So the show: by rw [Complex.cpow_natCast, ← Complex.ofReal_pow].\n    -- now the goal: ΓR z * ∏ = ↑(π^m) * ((↑(π^m))⁻¹ * ΓR z * ∏): ring with the inverse: need ↑(π^m) ≠ 0 to cancel — field_simp [hπne]? or:\n    field_simp [hπne]\n    ring\n```\nHmm — the field_simp after rw [hG2] and the show-rewrite: goal ΓR z * ∏ = ↑(π^m) * ((↑(π^m))⁻¹ * ΓR z * ∏): field_simp [hπne] clears the ⁻¹: ΓR z * ∏ * ↑(π^m) = ↑(π^m) * (ΓR z * ∏)·... then ring ✓. Or simply: the RHS = ↑(π^m) * (↑(π^m))⁻¹ * ΓR z * ∏ = ΓR z * ∏ by mul_inv_cancel₀ + one_mul: rw [mul_inv_cancel₀ hπne]?? the form: ↑(π^m) * (↑(π^m))⁻¹ * (ΓR z * ∏) — assoc: (↑(π^m) * (↑(π^m))⁻¹) * (ΓR z * ∏): mul_inv_cancel₀ : a * a⁻¹ = 1 for a ≠ 0 ✓: the exact form in the goal: ↑(π^m) * ((↑(π^m))⁻¹ * ΓR z * ∏) — regroup: = (↑(π^m) * (↑(π^m))⁻¹) * (ΓR z * ∏) [ring_nf? no — just: `field_simp [hπne]` then `ring` — iterate at build.\n\nThen:\n```\n  -- the EventuallyEq and the logDeriv computation\n  have hEv : Complex.Gammaℝ =ᶠ[𝓝 s]\n      fun z => (Real.pi : ℂ) ^ (m : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))\n        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ)) := by\n    filter_upwards [hU.mem_nhds hs] with z hz using hpt z hz\n  have hG2m : Complex.Gammaℝ (s + 2 * (m : ℂ)) ≠ 0 :=\n    Complex.Gammaℝ_ne_zero_of_re_pos hres2\n  have hPne : (∏ j ∈ Finset.range m, (s / 2 + (j : ℂ))) ≠ 0 := ... (as hpt's)\n  have hdG2m : DifferentiableAt ℂ (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s := by\n    apply DifferentiableAt.comp\n    · exact differentiableAt_Gammaℝ (by linarith [hres2] : (0:ℝ) < (s + 2*(m:ℂ)).re)?? \n```\nhmm — Zeta23's `differentiableAt_Gammaℝ (hs : 0 < s.re)` (WeilEF/XiLogDeriv.lean) — namespace? from the earlier grep: `Zeta23/WeilEF/XiLogDeriv.lean:30:lemma differentiableAt_Gammaℝ {s : ℂ} (hs : 0 < s.re)` — namespace inside? probably Zeta23 or plain. With open Zeta23 — accessible as differentiableAt_Gammaℝ (if root Zeta23 namespace) — but my LiReflect has differentiableAt_Gammaℝ_of_im_ne_zero' (mine). For re > 0: use whichever — check the namespace at build: try `Zeta23.differentiableAt_Gammaℝ` — hmm the file XiLogDeriv.lean's namespace: let me just use my own via... my ' variant needs im ≠ 0: (s+2m).im = s.im ≠ 0 ✓: differentiableAt_Gammaℝ_of_im_ne_zero' (by simp [Complex.add_im, ...]; exact hs). Then comp with (z + 2↑m): differentiableAt_id.add_const ✓:\n```\n  have hdG2m : DifferentiableAt ℂ (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s := by\n    have h1 : (s + 2 * (m : ℂ)).im ≠ 0 := by\n      have h2 : (s + 2 * (m : ℂ)).im = s.im := by\n        simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]\n      rw [h2]; exact hs\n    exact (differentiableAt_Gammaℝ_of_im_ne_zero' h1).comp s (differentiableAt_id.add_const _)\n  have hdP : DifferentiableAt ℂ (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s := by fun_prop\n  -- the big computation\n  rw [logDeriv_congr hEv]\n  have hstep1 : logDeriv (fun z : ℂ => (Real.pi : ℂ) ^ (m : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))\n        / ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s\n      = logDeriv (fun z : ℂ => (Real.pi : ℂ) ^ (m : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))) s\n        - logDeriv (fun z : ℂ => ∏ j ∈ Finset.range m, (z / 2 + (j : ℂ))) s :=\n    logDeriv_div s (mul_ne_zero (pow_ne_zero _ (by exact_mod_cast Real.pi_ne_zero)) hG2m) hPne\n      ((differentiableAt_const _).mul hdG2m) hdP\n  have hstep2 : logDeriv (fun z : ℂ => (Real.pi : ℂ) ^ (m : ℂ) * Complex.Gammaℝ (z + 2 * (m : ℂ))) s\n      = logDeriv Complex.Gammaℝ (s + 2 * (m : ℂ)) := by\n    rw [logDeriv_const_mul s _ (pow_ne_zero _ (by exact_mod_cast Real.pi_ne_zero : (Real.pi:ℂ) ≠ 0))]\n    -- logDeriv (ΓR(·+2m)) s = logDeriv ΓR (s+2m): the comp deriv\n    have hder : deriv (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s\n        = deriv Complex.Gammaℝ (s + 2 * (m : ℂ)) := by\n      have h1 := ((differentiableAt_Gammaℝ_of_im_ne_zero' (by\n          have h2 : (s + 2 * (m : ℂ)).im = s.im := by\n            simp [Complex.add_im, Complex.mul_im, Complex.natCast_im]\n          rw [h2]; exact hs)).hasDerivAt).comp s ((hasDerivAt_id' s).add_const (2 * (m : ℂ)))\n      have h2 : deriv (fun z : ℂ => Complex.Gammaℝ (z + 2 * (m : ℂ))) s\n          = deriv Complex.Gammaℝ (s + 2 * (m : ℂ)) * 1 := h1.deriv\n      rwa [mul_one] at h2\n    simp only [logDeriv_apply, hder]\n  rw [hstep1, hstep2]\n  -- logDeriv ΓR (s+2m) via logDeriv_Gammaℝ (re > 0)\n  have hev : logDeriv Complex.Gammaℝ (s + 2 * (m : ℂ))\n      = -(Real.log Real.pi : ℂ) / 2 + (1 / 2 : ℂ) * Complex.digamma ((s + 2 * (m : ℂ)) / 2) :=\n    RvM.logDeriv_Gammaℝ hres2\n  rw [hev]\n  -- the product logDeriv + the digamma shift + the cancellation\n  rw [logDeriv_prod_range_linear hs m]\n  -- (s+2m)/2 = s/2 + m; ψ(s/2 + m) = ψ(s/2) + Σ (s/2+↑j)⁻¹ (digamma_add_natCast, im(s/2) ≠ 0)\n  have him2 : (s / 2).im ≠ 0 := by\n    simp [Complex.div_ofNat_im]\n    exact hs  -- hmm: (s/2).im = s.im/2 ≠ 0 from hs: after simp [div_ofNat_im]: goal s.im/2 ≠ 0: div_ne_zero hs two_ne_zero ✓: `simp [Complex.div_ofNat_im]; exact div_ne_zero hs (by norm_num)`? careful — let me: have : (s/2).im = s.im / 2 := by simp [Complex.div_ofNat_im]; rw [this]; exact div_ne_zero hs (by norm_num : (2:ℝ) ≠ 0)\n  have harg : (s + 2 * (m : ℂ)) / 2 = s / 2 + (m : ℂ) := by ring\n  rw [harg, digamma_add_natCast him2 m]\n  -- the per-term form: (1/2)/(s/2+↑j) = (1/2)·(s/2+↑j)⁻¹: and Σ forms match\n  have hterm : ∀ j : ℕ, (1 / 2 : ℂ) / (s / 2 + (j : ℂ)) = (1 / 2 : ℂ) * (s / 2 + (j : ℂ))⁻¹ := by\n    intro j\n    rw [div_eq_mul_inv]\n  rw [Finset.sum_congr rfl (fun j _ => hterm j)]  -- hmm rw with sum_congr result — messy; better:\n  -- the goal: −(logπ)/2 + ½(ψ(s/2) + Σ (s/2+↑j)⁻¹) − Σ (1/2)/(s/2+↑j) = −(logπ)/2 + ½ψ(s/2)\n  -- via: Σ (1/2)/(s/2+↑j) = ½ Σ (s/2+↑j)⁻¹: Finset.mul_sum\n  have hsumform : ∑ j ∈ Finset.range m, (1 / 2 : ℂ) / (s / 2 + (j : ℂ))\n      = (1 / 2 : ℂ) * ∑ j ∈ Finset.range m, (s / 2 + (j : ℂ))⁻¹ := by\n    rw [Finset.mul_sum]\n    apply Finset.sum_congr rfl\n    intro j _\n    rw [div_eq_mul_inv]\n  rw [hsumform]\n  ring\n```\nCheck the algebra at the end: goal: −(logπ)/2 + ½·(ψ + Σ) − ½·Σ = −(logπ)/2 + ½·ψ — after rw [digamma_add_natCast him2 m]: the term digamma (s/2 + ↑m) becomes ψ(s/2) + Σ: the goal: −(logπ)/2 + ½·(ψ(s/2) + Σ (s/2+↑j)⁻¹) − Σ (1/2)/(s/2+↑j) = −(logπ)/2 + ½ ψ(s/2): rw [hsumform]: the Σ (1/2)/(...) → ½·Σ(...)⁻¹: goal: −(logπ)/2 + ½·(ψ + Σ) − ½·Σ = ...: ring ✓ (treating ψ, Σ as atoms: ½ψ + ½Σ − ½Σ = ½ψ ✓).\n\nOne concern: `digamma_add_natCast him2 m` — its statement (LiReflect): digamma (w + ↑n) = digamma w + Σ j ∈ range n, (w + ↑j)⁻¹ with w := s/2: after rw [harg] the term is digamma (s/2 + ↑m) ✓ rw [digamma_add_natCast him2 m] rewrites it to digamma (s/2) + Σ ✓.\n\nAlso hpt's form vs the EventuallyEq: the function fun z => (π:ℂ)^(↑m) * ΓR(z+2↑m) / ∏ ... — and hpt gives ΓR z = that ✓ filter_upwards ✓.\n\nThe hstep1's logDeriv_div: signature logDeriv_div (x) (hf : f x ≠ 0) (hg : g x ≠ 0) (hdf) (hdg) ✓.\n\n`pow_ne_zero _ (hpi : (π:ℂ) ≠ 0) : (π:ℂ)^? ≠ 0` — the exponent (m:ℂ) is a cpow! pow_ne_zero is for ^ℕ — for the cpow (π:ℂ)^(↑m:ℂ): need cpow-ne-zero: `Complex.cpow_ne_zero`? hmm — for x ≠ 0: x^y ≠ 0 — hmm is that even true for cpow? x^y = exp(y log x) ≠ 0 (exp_ne_zero) for x ≠ 0 ✓: `Complex.cpow_ne_zero (hx : x ≠ 0) (y : ℂ) : x ^ y ≠ 0`? hmm — not sure of the name; maybe `Complex.cpow_ne_zero_iff`? Let me handle: (π:ℂ)^(↑m) = (π:ℂ)^m via cpow_natCast (hmm — is the exponent ↑m : ℂ with m : ℕ — cpow_natCast : x ^ (↑n : ℂ) = x ^ n — so rewrite to (π:ℂ)^m then pow_ne_zero m ✓. To avoid the issue entirely: define the EventuallyEq's constant factor as ((Real.pi ^ m : ℝ) : ℂ) (the real-pow cast) instead of the cpow — from the show-rewrite: (π:ℂ)^(↑m:ℂ) = ↑(π^m) — use ↑(π^m) EVERYWHERE (cleaner: no cpow-ne-zero issues: ↑(π^m) ≠ 0 via cast of pow_ne_zero ✓). Let me use ((Real.pi ^ m : ℝ) : ℂ) as the constant in hpt/hEv/steps.\n\nOK — I have full drafts. Write §4+§5 as the append now. This is long; let me be careful to paste ONLY Lean. I'll write §4 ((A) + digamma_add_natCast') and §5 (G) in one Edit, then compile-iterate.","signature":""},{"type":"text","text":"Build green, audit clean, committed. Now §4 (A) + §5 (G) — the rest of 5e-ii. Appending them (Lean only this time)."},{"type":"tool_use","id":"Bash_438","name":"Bash","input":{"command":"tail -3 /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiDigammaLeft.lean","description":"Check file tail before appending"},"extra_content":null}]