[{"type":"thinking","thinking":"`Complex.div_ofNat_im (z : ℂ) (n : ℕ) [n.AtLeastTwo] : (z / ofNat n).im = z.im / n` — exactly what I need (line 784). And div_ofNat_re similarly. These are probably @[simp]. So `(s/2).im = s.im/2` via `Complex.div_ofNat_im` or plain `simp`. \n\nNow I have everything I need. Time to write the file. Let me write §1–§5 (the main theorem) first, then §6 (left-plane digamma). Actually, given the size, let me write §0–§5 first and iterate on compile errors, then add §6.\n\nPlan of declarations:\n\n§0 helpers:\n- `im_div_two` — via div_ofNat_im (may be simp; still useful to have).\n- `Gammaℝ_ne_zero_of_im_ne_zero'` (NguyenRH1 namespace) : s.im ≠ 0 → Gammaℝ s ≠ 0.\n- `differentiableAt_Gammaℝ_of_im_ne_zero'` : s.im ≠ 0 → DifferentiableAt ℂ Gammaℝ s.\n- `logDeriv_congr`.\n\n§1 ΓR shift:\n- `gammaR_shift {s} (hs : s.im ≠ 0) : Gammaℝ s = (π:ℂ)^2 * Gammaℝ (s+4) / ((s/2)*(s/2+1))`\n- `logDeriv_Gammaℝ_shift {s} (hs : s.im ≠ 0) : logDeriv Gammaℝ s = logDeriv Gammaℝ (s+4) − 2*(s+1)/(s*(s+2))`\n\n§2 FE:\n- `completedZeta_eq_mul_eventually {s} (hs0 : s ≠ 0) (hG : Gammaℝ s ≠ 0) (hd : DifferentiableAt ℂ Gammaℝ s) : completedRiemannZeta =ᶠ[𝓝 s] fun z => Gammaℝ z * riemannZeta z`\n- `logDeriv_completedZeta_eq_add {s} (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hG : Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0) (hd : DifferentiableAt ℂ Gammaℝ s) : logDeriv completedRiemannZeta s = logDeriv Gammaℝ s + logDeriv riemannZeta s`\n- `logDeriv_completedZeta_neg_one_sub {s} (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1) : logDeriv completedRiemannZeta s = -logDeriv completedRiemannZeta (1 - s)`\n- `riemannZeta_one_sub_ne_zero {s} (hs0 : s ≠ 0) (hG : Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0) (h1s0 : 1 - s ≠ 0) (hG1 : Gammaℝ (1 - s) ≠ 0) : riemannZeta (1 - s) ≠ 0`\n- `logDeriv_zeta_fe {s} (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hG : Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0) (hd : DifferentiableAt ℂ Gammaℝ s) (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1) (hG1 : Gammaℝ (1-s) ≠ 0) (hζ1 : riemannZeta (1-s) ≠ 0) (hd1 : DifferentiableAt ℂ Gammaℝ (1-s)) : logDeriv riemannZeta s = -logDeriv riemannZeta (1-s) - (logDeriv Gammaℝ s + logDeriv Gammaℝ (1-s))`\n\n§3 reflection:\n- `riemannZeta_one_sub_eq_zero_of_nontrivial {ρ} (hρ : IsNontrivialZero ρ) : riemannZeta (1 - ρ) = 0`\n- `one_sub_mem_nearZeros_neg {t} {ρ} (hρ : ρ ∈ nearZeros t) : 1 - ρ ∈ nearZeros (-t)`\n- `nearZeros_neg_eq_image (t : ℝ) : nearZeros (-t) = (nearZeros t).image (fun ρ => 1 - ρ)`\n- `zeroMult_one_sub {ρ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) : zeroMult (1 - ρ) = zeroMult ρ`\n- `sum_nearZeros_neg_reflect (t : ℝ) (s : ℂ) : ∑ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ) / (1 - s - ρ') = -∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)`\n\n§4 bracket:\n- `norm_log_le_of_one_le {w : ℂ} (hw : 1 ≤ ‖w‖) : ‖Complex.log w‖ ≤ Real.log ‖w‖ + Real.pi`\n- `norm_digamma_le_log_of {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} (hwre : 0 < w.re) (hwim : |w.im| = |t| / 2) (hwn : ‖w‖ ≤ 2 * |t|) : ‖Complex.digamma w‖ ≤ Real.log |t| + 5`\n- `gammaR_bracket_norm_le {t} (ht) {s} (hsim : s.im = t) (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 1/2) : ‖logDeriv Gammaℝ (1-s) + logDeriv Gammaℝ s‖ ≤ 4 * (Real.log |t|)^2`\n\n§5 capstone:\n- `logDeriv_riemannZeta_sub_nearZeros_le_left {t} (ht : 10 ≤ |t|) {s} (hsim : s.im = t) (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 1/2) (hs0 : riemannZeta s ≠ 0) : ‖logDeriv riemannZeta s − ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ)/(s − ρ)‖ ≤ 200000 * (Real.log |t|)^2`\n\n§6 left-plane digamma:\n- `digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) : Complex.digamma (w + n) = Complex.digamma w + ∑ j ∈ Finset.range n, (w + j)⁻¹`\n- `em_sum_inv_eq ...`? maybe inline.\n- `norm_digamma_sub_log_le_of_two_le_abs_im {w : ℂ} (hw : 2 ≤ |w.im|) : ‖Complex.digamma w − Complex.log w‖ ≤ 3`\n\nNow — write it. I'll write §0–§5 first (§6 in a second pass since it's independent).\n\nSome more care on §3's C2 ball computation. I need: ‖(1 − ρ) − discCenter (−t)‖ ≤ 5/2.\n\n(1 − ρ) − discCenter (−t) = 1 − ρ − (2 + (−t)·I) = −1 − ρ + t·I.\nLet u := ρ − discCenter t: u.re = ρ.re − 2, u.im = ρ.im − t.\n−1 − ρ + t·I: re = −1 − ρ.re; im = −ρ.im + t = −(ρ.im − t).\n‖·‖² = (1 + ρ.re)² + (ρ.im − t)² [squaring kills the signs].\n0 < ρ.re < 1 ⟹ 1 < 1 + ρ.re < 2 ⟹ (1+ρ.re)² ≤ 4.\n|ρ.im − t| < 1 ⟹ (ρ.im−t)² ≤ 1.\nTotal ≤ 5 ≤ 25/4 ⟹ ‖·‖ ≤ 5/2 (via le_of_pow_le_pow or sqrt route — mirror LiDisc's hnorm1 approach at line 1004).\n\nIn Lean, following nearZeros_subset_image's pattern:\n```\nhave hnorm : ‖(1 - ρ) - discCenter (-t)‖ ≤ Real.sqrt 5 := by\n  have hsq : Complex.normSq ((1 - ρ) - discCenter (-t)) ≤ 5 := by\n    rw [Complex.normSq_apply]\n    have hre : ((1 - ρ) - discCenter (-t)).re = -(1 + ρ.re) := by\n      simp [discCenter, sub_re, add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im, neg_re, neg_im]\n      ring\n    have him : ((1 - ρ) - discCenter (-t)).im = -(ρ.im - t) := by\n      simp [discCenter, sub_im, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, neg_re, neg_im]\n      ring\n    have h1 : (1 + ρ.re) ^ 2 ≤ 4 := by\n      have : |1 + ρ.re| ≤ 2 := by rw [abs_le]; constructor <;> linarith [hρnt.2.1, hρnt.2.2]\n      calc (1 + ρ.re)^2 = |1 + ρ.re|^2 := (sq_abs _).symm\n        _ ≤ 2^2 := pow_le_pow_left₀ (abs_nonneg _) this _\n        _ = 4 := by norm_num\n    have h2 : (ρ.im - t)^2 ≤ 1 := ...\n    rw [hre, him, neg_sq, neg_sq]  -- (-(1+ρ.re))² = (1+ρ.re)² \n    nlinarith [h1, h2]\n  ...same sqrt finish...\n```\nneg_sq : (-a)^2 = a^2 ✓ exists.\n\nHmm wait: hre as I wrote says re = −(1 + ρ.re): re(−1 − ρ + tI) = −1 − ρ.re + 0 = −(1 + ρ.re) ✓.\n\nThe simp call: (1 − ρ − discCenter (−t)).re where discCenter (−t) = 2 + (−t)*I: 1 − ρ − (2 + (−t)*I) = −1 − ρ − (−t)*I: re = 1 − ρ.re − 2 − 0 = −1 − ρ.re ✓. simp [sub_re, neg_re, add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im, neg_im, one_re, one_im] then ring. I'll trust the LiDisc pattern with extended simp set and `ring` after (the LiDisc one didn't need ring since no negation... let me include ring_nf fallbacks: `simp [...]; ring`).\n\nFor the membership in zeroDiscFinset(−t): mem_zeroDiscFinset.mpr ⟨ball, zero⟩ where ball : (1−ρ) ∈ Metric.closedBall (discCenter (−t)) (5/2): Metric.mem_closedBall: dist (1−ρ) (discCenter (−t)) ≤ 5/2: dist_eq_norm: Complex.dist_eq : dist x y = ‖x − y‖ ✓; then ‖·‖ ≤ √5 ≤ 5/2 via Real.sqrt 5 ≤ 5/2: (5/2)² = 25/4 ≥ 5: Real.sqrt_le_iff? `Real.sqrt_le_left (hb : 0 ≤ b) : sqrt a ≤ b ↔ a ≤ b^2`? or `Real.sqrt_le_iff : sqrt a ≤ b ↔ 0 ≤ b ∧ a ≤ b^2`? hmm. LiDisc used: `Real.sqrt 5 ≤ Real.sqrt ((23/10)^2)` then sqrt_sq. I'll do: Real.sqrt 5 ≤ 5/2: `Real.sqrt_le_iff.mpr ⟨by norm_num, by norm_num⟩`? or via sqrt_le_sqrt of 5 ≤ (5/2)² = 25/4: Real.sqrt ((5/2)^2) = 5/2 (Real.sqrt_sq (by norm_num)) ✓ copy that pattern.\n\nThen C3's ext argument:\n```\ntheorem nearZeros_neg_eq_image (t : ℝ) :\n    nearZeros (-t) = (nearZeros t).image (fun ρ => 1 - ρ) := by\n  classical\n  ext ρ'\n  constructor\n  · intro h\n    rw [Finset.mem_image]\n    exact ⟨1 - ρ', one_sub_mem_nearZeros_neg' h, by ring⟩  -- ρ' = 1 - (1 - ρ')\n  · intro h\n    rw [Finset.mem_image] at h\n    obtain ⟨ρ, hρ, rfl⟩ := h\n    exact one_sub_mem_nearZeros_neg hρ\n```\nwhere I need BOTH directions of the membership transport. So make ONE bidirectional lemma:\n```\ntheorem one_sub_mem_nearZeros_neg_iff {t : ℝ} {ρ : ℂ} :\n    (1 - ρ) ∈ nearZeros (-t) ↔ ρ ∈ nearZeros t\n```\nHmm — from h : ρ' ∈ nearZeros (−t) I want 1 − ρ' ∈ nearZeros t. If I prove `one_sub_mem_nearZeros_neg : ρ ∈ nearZeros t → 1 − ρ ∈ nearZeros (−t)` then the other direction is the same lemma at −t applied to 1−ρ: 1 − (1−ρ) = ρ ∈ nearZeros (−(−t)) = nearZeros t: needs −(−t) = t (neg_neg) and 1 − (1−ρ) = ρ (sub_sub_self? `sub_sub_self : a − (a − b) = b`? for 1 − (1 − ρ): sub_sub_self : 1 − (1 − ρ) = ρ ✓). \n\nSo:\n```\ntheorem mem_nearZeros_neg_of_one_sub {t} {ρ'} (h : ρ' ∈ nearZeros (-t)) : 1 - ρ' ∈ nearZeros t := by\n  have := one_sub_mem_nearZeros_neg h  -- : 1 - ρ' ∈ nearZeros (-(-t))\n  rwa [neg_neg] at this\n```\n✓.\n\nThen sum_nearZeros_neg_reflect:\n```\ntheorem sum_nearZeros_neg_reflect (t : ℝ) (s : ℂ) :\n    ∑ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ) / (1 - s - ρ')\n      = - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ) := by\n  classical\n  rw [nearZeros_neg_eq_image, Finset.sum_image]\n  · rw [Finset.sum_neg_distrib]  -- if exists; else manual\n    apply Finset.sum_congr rfl\n    intro ρ hρ\n    have hnt := zeroDisc_isNontrivial ((mem_nearZeros.mp hρ).1)\n    rw [zeroMult_one_sub hnt.2.1 hnt.2.2]\n    -- (zeroMult ρ)/(1 − s − (1−ρ)) = −((zeroMult ρ)/(s−ρ))\n    have : (1 : ℂ) - s - (1 - ρ) = -(s - ρ) := by ring\n    rw [this, div_neg]  -- hmm: m/(−(s−ρ)) = −(m/(s−ρ)): `div_neg : a / −b = −(a/b)` ✓\n  · exact fun a _ b _ hab => sub_left_inj.mp hab  -- Set.InjOn (fun ρ => 1 − ρ) _\n```\nCareful: Finset.sum_image (h : Set.InjOn f ↑s) : ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x) — signature `Finset.sum_image {g : β → α} (h : Set.InjOn f s) : ∑ x ∈ s.image f, g x = ∑ x ∈ s, g (f x)` ✓ (journal: takes Set.InjOn). After rw, goal: ∑ ρ ∈ nearZeros t, (zeroMult (1−ρ) : ℂ)/(1 − s − (1−ρ)) = −∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ)/(s − ρ). Then rw [Finset.sum_neg_distrib]: turns RHS −∑ f into ∑ (−f): goal becomes ∑ lhs-form = ∑ ρ, −((zeroMult ρ)/(s−ρ)): sum_congr: per-term: zeroMult (1−ρ) = zeroMult ρ (needs 0 < ρ.re < 1 from nontrivial ✓); denominator 1 − s − (1 − ρ) = −(s − ρ) ✓ ring; div_neg : a / −b = −(a / b) ✓.\n\nIf Finset.sum_neg_distrib doesn't exist: use `Finset.sum_congr` first to show LHS sum = ∑ ρ, −((zeroMult ρ:ℂ)/(s−ρ)), then `Finset.sum_neg_distrib`/`neg_sum`... alternatives: `Finset.sum_neg_distrib` hmm. There IS `Finset.sum_neg_distrib` in Mathlib (Algebra/BigOperators/Group/Finset/Basic?): I'm not sure. Safe: `(Finset.sum_sub_distrib (s := ..) (f := fun _ => 0) ..)`... Actually simplest bulletproof: `neg_eq_of_add_eq_zero_left`? Or use map: `Finset.sum_neg_distrib` — let me just plan on:\n```\n  rw [← Finset.sum_neg_distrib]  -- goal RHS direction\n```\nIf that fails, fallback: have : ∀ x, -(f x) = (0 - f x) := fun x => (zero_sub _).symm... then ∑ (0 − f) = 0 − ∑ f by Finset.sum_sub_distrib + Finset.sum_const_zero... `Finset.sum_const_zero : ∑ x ∈ s, 0 = 0` ✓ simp. I'll adapt at compile time.\n\nAlso for C5 I should double check zeroMult: `Zeta23.zeroMult ρ = (analyticOrderAt riemannZeta ρ).toNat`. zeroMult_one_sub: \n```\ntheorem zeroMult_one_sub {ρ : ℂ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) :\n    zeroMult (1 - ρ) = zeroMult ρ := by\n  unfold zeroMult  -- hmm zeroMult is Zeta23.zeroMult: `Zeta23.zeroMult` def — unfold works if equation lemma: rw [Zeta23.zeroMult]? use `show (analyticOrderAt riemannZeta (1-ρ)).toNat = ...` — the def: `def zeroMult (ρ : ℂ) : ℕ := (analyticOrderAt riemannZeta ρ).toNat` — so zeroMult (1−ρ) = (analyticOrderAt ζ (1−ρ)).toNat definitionally: `show ((analyticOrderAt riemannZeta (1 - ρ)).toNat = (analyticOrderAt riemannZeta ρ).toNat` might work via rfl-unfold; safer: `simp only [zeroMult, analyticOrderAt_zeta_one_sub h0 h1]`? simp only with the def: `rw [show zeroMult (1-ρ) = (analyticOrderAt riemannZeta (1-ρ)).toNat from rfl, analyticOrderAt_zeta_one_sub h0 h1]` — since def unfolds by rfl ✓.\n```\n\nC1: riemannZeta (1−ρ) = 0 from IsNontrivialZero ρ:\n```\ntheorem riemannZeta_one_sub_eq_zero_of_nontrivial {ρ : ℂ} (hρ : IsNontrivialZero ρ) :\n    riemannZeta (1 - ρ) = 0 := by\n  have h0 : ρ ≠ 0 := fun h => by rw [h] at hρ; simp at hρ -- hρ.2.1 : 0 < (0:ℂ).re = false... cleaner: hρ.2.1 : 0 < ρ.re; if ρ = 0 then re = 0: fun h => by rw [h, Complex.zero_re] at hρ; exact lt_irrefl 0 hρ.2.1\n  have hG : Complex.Gammaℝ ρ ≠ 0 := Complex.Gammaℝ_ne_zero_of_re_pos hρ.2.1\n  have h1ρ0 : (1 : ℂ) - ρ ≠ 0 := fun h => by ... re(1−ρ) = 1 − ρ.re > 0 ⟹ ≠ 0: fun h => by have := congrArg Complex.re h; simp [sub_re, one_re] at this; linarith [hρ.2.2]\n  have hG1 : Complex.Gammaℝ (1 - ρ) ≠ 0 := Complex.Gammaℝ_ne_zero_of_re_pos (by simp [sub_re]; linarith [hρ.2.2] : 0 < (1-ρ).re)\n  have hΛ1 : completedRiemannZeta (1 - ρ) = 0 := by\n    rw [completedRiemannZeta_one_sub, RvM.completedRiemannZeta_eq_Gammaℝ_mul h0 hG, hρ.1, mul_zero]\n  rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul h1ρ0 hG1] at hΛ1\n  exact (mul_eq_zero.mp hΛ1).resolve_left hG1  -- hmm: mul_eq_zero.mp : a*b = 0 → a = 0 ∨ b = 0; resolve_left hG1 : b = 0 ✓\n```\nIsNontrivialZero ρ structure: ⟨hz : riemannZeta ρ = 0, h1 : 0 < ρ.re, h2 : ρ.re < 1⟩ — from completedRiemannZeta_eq_zero_iff usage: `.2.1` and `.2.2` and `.1` ✓ (as in zeroDisc_isNontrivial: hρnt.1, hρnt.2.1, hρnt.2.2 ✓).\n\n§2 details:\n\nB1:\n```\ntheorem completedZeta_eventuallyEq {s : ℂ} (hs0 : s ≠ 0) (hG : Complex.Gammaℝ s ≠ 0)\n    (hd : DifferentiableAt ℂ Complex.Gammaℝ s) :\n    completedRiemannZeta =ᶠ[𝓝 s] fun z => Complex.Gammaℝ z * riemannZeta z := by\n  have h1 : ∀ᶠ z in 𝓝 s, z ≠ 0 := isOpen_compl_singleton.mem_nhds hs0\n  have h2 : ∀ᶠ z in 𝓝 s, Complex.Gammaℝ z ≠ 0 := hd.continuousAt.eventually_ne hG\n  filter_upwards [h1, h2] with z hz0 hzG\n  exact RvM.completedRiemannZeta_eq_Gammaℝ_mul hz0 hzG\n```\n✓.\n\nB2:\n```\ntheorem logDeriv_completedZeta_eq_add {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1)\n    (hG : Complex.Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0)\n    (hd : DifferentiableAt ℂ Complex.Gammaℝ s) :\n    logDeriv completedRiemannZeta s = logDeriv Complex.Gammaℝ s + logDeriv riemannZeta s := by\n  rw [logDeriv_congr (completedZeta_eventuallyEq hs0 hG hd)]\n  exact logDeriv_mul s hG hζ hd (differentiableAt_riemannZeta hs1)\n```\n✓.\n\nB3:\n```\ntheorem logDeriv_completedZeta_neg_one_sub {s : ℂ} (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1) :\n    logDeriv completedRiemannZeta s = -logDeriv completedRiemannZeta (1 - s) := by\n  have hfe : (fun z : ℂ => completedRiemannZeta (1 - z)) = completedRiemannZeta :=\n    funext fun z => completedRiemannZeta_one_sub z\n  have hd1 : DifferentiableAt ℂ completedRiemannZeta (1 - s) :=\n    differentiableAt_completedZeta h1s0 h1s1\n  have hder : deriv (fun z : ℂ => completedRiemannZeta (1 - z)) s = - deriv completedRiemannZeta (1 - s) := by\n    have h1 : HasDerivAt (fun z : ℂ => 1 - z) (-1 : ℂ) s := by\n      have := (hasDerivAt_id' s).const_sub (1 : ℂ)  -- HasDerivAt.const_sub (c) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c - f x) (-f') x\n      simpa using this\n    have h2 := hd1.hasDerivAt.comp s h1  -- HasDerivAt (Λ ∘ (1−·)) (deriv Λ (1−s) * −1) s\n    rw [h2.deriv]\n    simp [Function.comp_def]  -- deriv Λ (1−s) * −1 = − deriv Λ (1−s): mul_neg_one\n  -- logDeriv Λ s: rewrite via hfe\n  have h3 : logDeriv completedRiemannZeta s = logDeriv (fun z : ℂ => completedRiemannZeta (1 - z)) s := by rw [hfe]\n  rw [h3, logDeriv_apply, logDeriv_apply, hder]\n  -- goal: −deriv Λ (1−s) / Λ(1−s) = −(deriv Λ (1−s) / Λ(1−s)): neg_div\n  rw [neg_div]\n```\nCareful with the rw [hfe] direction: hfe : (fun z => Λ (1−z)) = Λ; goal h3 : logDeriv Λ s = logDeriv (fun z => Λ (1−z)) s — rw [hfe] rewrites LHS occurrences of the lambda with Λ — the lambda appears on RHS: rw [hfe] turns RHS into logDeriv Λ s making goal rfl ✓ (rw rewrites all occurrences of the lambda pattern).\n\nHmm wait — in h3, after `rw [hfe]`, both sides identical ⟹ closed by rfl automatically? rw closes rfl goals ✓.\n\nB5:\n```\ntheorem riemannZeta_one_sub_ne_zero {s : ℂ} (hs0 : s ≠ 0) (hG : Complex.Gammaℝ s ≠ 0)\n    (hζ : riemannZeta s ≠ 0) (h1s0 : 1 - s ≠ 0) (hG1 : Complex.Gammaℝ (1 - s) ≠ 0) :\n    riemannZeta (1 - s) ≠ 0 := by\n  intro h\n  have hΛ : completedRiemannZeta (1 - s) = 0 := by\n    rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul h1s0 hG1, h, mul_zero]\n  rw [completedRiemannZeta_one_sub] at hΛ\n  rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hG] at hΛ\n  exact mul_ne_zero hG hζ hΛ\n```\n✓.\n\nB4:\n```\ntheorem logDeriv_zeta_fe {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1)\n    (hG : Complex.Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0)\n    (hd : DifferentiableAt ℂ Complex.Gammaℝ s)\n    (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1)\n    (hG1 : Complex.Gammaℝ (1 - s) ≠ 0) (hζ1 : riemannZeta (1 - s) ≠ 0)\n    (hd1 : DifferentiableAt ℂ Complex.Gammaℝ (1 - s)) :\n    logDeriv riemannZeta s\n      = - logDeriv riemannZeta (1 - s) - (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1 - s)) := by\n  have h1 := logDeriv_completedZeta_eq_add hs0 hs1 hG hζ hd\n  have h2 := logDeriv_completedZeta_eq_add h1s0 h1s1 hG1 hζ1 hd1\n  have h3 := logDeriv_completedZeta_neg_one_sub h1s0 h1s1\n  -- h1: logDeriv Λ s = logDeriv ΓR s + logDeriv ζ s\n  -- h2: logDeriv Λ (1−s) = logDeriv ΓR (1−s) + logDeriv ζ (1−s)\n  -- h3: logDeriv Λ s = −logDeriv Λ (1−s)\n  linear_combination h1 + h2 + h3\n```\nCheck: goal: ζs = −ζ1 − (Γs + Γ1). h1 + h2 + h3: (Λs = Γs + ζs) + (Λ1 = Γ1 + ζ1) + (Λs = −Λ1) — sum of LHS: 2Λs + Λ1; sum of RHS: Γs + ζs + Γ1 + ζ1 − Λ1. linear_combination proves goal LHS − goal RHS = combination: ζs + ζ1 + Γs + Γ1 =? (h1+h2+h3: LHS−RHS = 2Λs + Λ1 − Γs − ζs − Γ1 − ζ1 + Λ1 = 2Λs + 2Λ1 − Γs − ζs − Γ1 − ζ1). goal: ζs + ζ1 + Γs + Γ1 = 0 ⟸ from h3: Λs + Λ1 = 0 and h1+h2: Λs + Λ1 = Γs+ζs+Γ1+ζ1 ⟹ Γs+ζs+Γ1+ζ1 = 0 ✓. linear_combination h1 + h2 + h3: goal_eq − (h1_eq + h2_eq + h3_eq) = [ζs + ζ1 + Γs + Γ1] − [Λs − Γs − ζs + Λ1 − Γ1 − ζ1 + Λs + Λ1] = ζs + ζ1 + Γs + Γ1 − 2Λs − 2Λ1 + Γs + ζs + Γ1 + ζ1 = 2(Γs+ζs+Γ1+ζ1) − 2(Λs+Λ1)... hmm let me just verify: linear_combination h1+h2+h3 checks: (goal.lhs − goal.rhs) = 1·(h1.lhs − h1.rhs) + 1·(h2.lhs − h2.rhs) + 1·(h3.lhs − h3.rhs) after normalization:\ngoal.lhs − goal.rhs = ζs − (−ζ1 − (Γs+Γ1)) = ζs + ζ1 + Γs + Γ1.\nh1.l−r = Λs − Γs − ζs. h2.l−r = Λ1 − Γ1 − ζ1. h3.l−r = Λs + Λ1.\nSum: 2Λs + 2Λ1 − Γs − ζs − Γ1 − ζ1. Is ζs+ζ1+Γs+Γ1 = 2Λs+2Λ1−Γs−ζs−Γ1−ζ1? That would need 2(Γs+ζs+Γ1+ζ1) = 2(Λs+Λ1) — NOT a ring identity. So coefficients wrong. Solve: want a·h1 + b·h2 + c·h3 with: goal: ζs + ζ1 + Γs + Γ1. a·(Λs−Γs−ζs) + b·(Λ1−Γ1−ζ1) + c·(Λs+Λ1) = (a+c)Λs + (b+c)Λ1 − aΓs − aζs − bΓ1 − bζ1. Match: −a = 1 (Γs), −b = 1 (Γ1): a = −1, b = −1; then Λs coeff: −1 + c = 0 ⟹ c = 1 ✓ Λ1: −1 + 1 = 0 ✓. So linear_combination -h1 - h2 + h3 ⟹ check: −h1−h2+h3 LHS−RHS = −(Λs−Γs−ζs) −(Λ1−Γ1−ζ1) + (Λs+Λ1) = Γs+ζs+Γ1+ζ1 ✓ = goal ✓. So: `linear_combination -h1 - h2 + h3`. (linear_combination syntax: `linear_combination -h1 - h2 + h3` — the tactic supports negation ✓.)\n\n§4 details:\n\nnorm_log_le_of_one_le:\n```\ntheorem norm_log_le_of_one_le {w : ℂ} (hw : 1 ≤ ‖w‖) :\n    ‖Complex.log w‖ ≤ Real.log ‖w‖ + Real.pi := by\n  calc ‖Complex.log w‖ ≤ |(Complex.log w).re| + |(Complex.log w).im| := norm_le_abs_re_add_abs_im' _\n    _ = |Real.log ‖w‖| + |Complex.arg w| := by rw [Complex.log_re, Complex.log_im]\n    _ = Real.log ‖w‖ + |Complex.arg w| := by rw [abs_of_nonneg (Real.log_nonneg hw)]\n    _ ≤ Real.log ‖w‖ + Real.pi := by gcongr; exact Complex.abs_arg_le_pi _\n```\n(gcongr for the ≤ with the arg bound: add_le_add_left (Complex.abs_arg_le_pi w) _ ✓ simpler: `exact add_le_add_left (Complex.abs_arg_le_pi w) _` hmm the order: Real.log ‖w‖ + |arg w| ≤ Real.log ‖w‖ + π: add_le_add_left (abs_arg_le_pi w) _ ✓.)\n\nnorm_digamma_le_log_of:\n```\ntheorem norm_digamma_le_log_of {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}\n    (hwre : 0 < w.re) (hwim : |w.im| = |t| / 2) (hwn : ‖w‖ ≤ 2 * |t|) :\n    ‖Complex.digamma w‖ ≤ Real.log |t| + 5 := by\n  have ht0 : (0:ℝ) < |t| := by positivity... |t| ≥ 10 > 0: lt_of_lt_of_le (by norm_num) ht\n  have hwim5 : 5 ≤ |w.im| := by rw [hwim]; linarith [ht]  -- |t|/2 ≥ 5 ✓\n  have hwnorm5 : 5 ≤ ‖w‖ := hwim5.trans (by rw [← hwim]; exact Complex.abs_im_le_norm w)  -- hmm: |w.im| ≤ ‖w‖ so 5 ≤ |w.im| ≤ ‖w‖ ✓: hwim5 : 5 ≤ |w.im|; (Complex.abs_im_le_norm w) : |w.im| ≤ ‖w‖: le_trans ✓\n  have hst := StirlingVert.digamma_stirling hwre (by rw [hwim]; linarith [ht])  -- 1/2 ≤ |w.im|: |t|/2 ≥ 5 ≥ 1/2 ✓\n  -- decompose ψ = (ψ − log + 1/(2w)) + log − 1/(2w)\n  calc ‖Complex.digamma w‖ \n      = ‖(Complex.digamma w - Complex.log w + (1/2 : ℂ)/w) + Complex.log w - (1/2:ℂ)/w‖ := by ring_nf  -- congr: a = (a−b+c)+b−c: by ring_nf? for norm arg: congr 1; ring\n    _ ≤ ‖Complex.digamma w - Complex.log w + (1/2 : ℂ)/w‖ + ‖Complex.log w‖ + ‖(1/2:ℂ)/w‖ := by\n        exact (norm_add_le _ _).trans (add_le_add_left (norm_sub_le _ _) _)... hmm careful: ‖A + B − C‖ ≤ ‖A‖ + ‖B − C‖ ≤ ‖A‖ + ‖B‖ + ‖−C‖ = ... Let me: ‖(A + B) − C‖ ≤ ‖A + B‖ + ‖C‖ ≤ ‖A‖ + ‖B‖ + ‖C‖: norm_sub_le (A+B) C : ‖A+B−C‖ ≤ ‖A+B‖ + ‖C‖; norm_add_le A B. So: (norm_sub_le _ _).trans (add_le_add_right (norm_add_le _ _) _) ✓.\n    _ ≤ 3 / w.im^2 + (Real.log ‖w‖ + Real.pi) + (1/2)/‖w‖ := by\n        gcongr -- three components: hst; norm_log_le_of_one_le (1 ≤ ‖w‖ from 5 ≤ ‖w‖); ‖(1/2)/w‖ = (1/2)/‖w‖: norm_div, norm_one... ‖(1/2 : ℂ)‖ = 1/2: hmm (1/2 : ℂ) norm: via show (1/2:ℂ) = ((1/2:ℝ):ℂ) by norm_num; norm_real... pattern from LiDisc line 1034-1036 ✓ copy.\n    _ ≤ Real.log |t| + 5 := by\n        have h1 : 3 / w.im^2 ≤ 1 := by -- w.im² ≥ 25: 3/25 ≤ 1: rw [hwim]?? careful: w.im^2 = |w.im|^2 via sq_abs; |w.im| = |t|/2 ≥ 5 ⟹ w.im^2 ≥ 25 ⟹ 3/w.im² ≤ 3/25 ≤ 1: div_le_one_of_le₀? `div_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b)`? form: div_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b) : a / b ≤ 1? hmm maybe (h : a ≤ b) (hb : 0 ≤ b)... check at build. or: rw [div_le_one (by positivity : (0:ℝ) < w.im^2)]; nlinarith [...]. \n        have h2 : Real.log ‖w‖ ≤ Real.log |t| + 1 := by\n          -- log ‖w‖ ≤ log (2|t|) = log 2 + log |t| ≤ 1 + log|t|\n          have := Real.log_le_log (by linarith [hwnorm5] : (0:ℝ) < ‖w‖) hwn  -- log ‖w‖ ≤ log (2|t|)\n          rw [Real.log_mul (two_ne_zero) (ne_of_gt ht0... |t| ≠ 0)] at this  -- log (2*|t|) = log 2 + log |t|\n          -- Real.log 2 ≤ 1: Real.log_two_lt_d9 : log 2 < 0.6931... ≤ 1: linarith\n          linarith [Real.log_two_lt_d9.le]  -- Real.log_two_lt_d9 : Real.log 2 < 0.6931471803\n        have h3 : (1/2 : ℝ)/‖w‖ ≤ 1 := by -- ‖w‖ ≥ 5 ≥ 1/2: (1/2)/5 = 0.1 ≤ 1: div_le_one... nlinarith route with div_le_iff\n        have h4 : Real.pi ≤ 4 := Real.pi_lt_315.le.trans (by norm_num)  -- Real.pi_lt_315 : π < 3.15\n        linarith [h1, h2, h3, h4]\n```\nWait — issue: Real.log_mul : log (a*b) = log a + log b needs a ≠ 0, b ≠ 0: Real.log_mul (ha : a ≠ 0) (hb : b ≠ 0) ✓. 2*|t|: fine.\nHmm h2: log (2 * |t|) — hwn : ‖w‖ ≤ 2 * |t| ✓. But careful — Real.log_le_log (hx : 0 < x) (h : x ≤ y) : log x ≤ log y ✓ banked journal-024.\n\nAnd the calc step 1: ‖A + B − C‖ decomposition — the congr: digamma w = (digamma w − log w + (1/2)/w) + log w − (1/2)/w: ring in ℂ ✓: congr 1 then ring. Write: `congr 1; ring`.\n\ngammaR_bracket_norm_le:\n```\ntheorem gammaR_bracket_norm_le {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}\n    (hsim : s.im = t) (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 1 / 2) :\n    ‖logDeriv Complex.Gammaℝ (1 - s) + logDeriv Complex.Gammaℝ s‖ ≤ 4 * (Real.log |t|) ^ 2 := by\n  have ht0 : (0:ℝ) < |t| := lt_of_lt_of_le (by norm_num) ht\n  have htim : s.im ≠ 0 := by rw [hsim]; exact fun h => by rw [h, abs_zero] at ht; norm_num at ht\n  -- wait: t ≠ 0 from |t| ≥ 10: fun h : t = 0 => ... ht : 10 ≤ |0| = 0 false: \n  --   rw [hsim]; intro h; rw [h, abs_zero] at ht; norm_num at ht ✓\n  -- the two digamma point facts\n  set w1 := (1 - s) / 2 with hw1\n  set w2 := (s + 4) / 2 with hw2\n  have hw1re : 0 < w1.re := by rw [hw1]; simp [Complex.div_ofNat_re, sub_re, one_re]; linarith [hσhi]\n  -- (1−s).re = 1 − s.re ≥ 1/2 > 0; (w1).re = (1−s.re)/2 ✓\n  have hw1im : |w1.im| = |t| / 2 := by\n    rw [hw1]; simp [Complex.div_ofNat_im, sub_im, one_im, hsim]  -- ((1−s).im)/2 = (−t)/2\n    rw [abs_div, abs_neg, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 2)]  -- |−t/2| = |t|/2\n  have hw1n : ‖w1‖ ≤ 2 * |t| := by\n    have hsn : ‖s‖ ≤ |s.re| + |t| := (norm_le_abs_re_add_abs_im' s).trans (by rw [hsim] : ...)  \n```\nhmm — norm_le_abs_re_add_abs_im' s : ‖s‖ ≤ |s.re| + |s.im|; |s.im| = |t| (rw [hsim]); |s.re| ≤ 5/2 (abs_le: −5/2 ≤ re ≤ 1/2 ≤ 5/2 ⟹ |re| ≤ 5/2: abs_le.mpr ⟨hσlo, hσhi.trans (by norm_num)⟩). So ‖s‖ ≤ 5/2 + |t|.\n‖w1‖ = ‖(1−s)/2‖ = ‖1−s‖/2 ≤ (1 + ‖s‖)/2 ≤ (1 + 5/2 + |t|)/2 = 7/4 + |t|/2 ≤ |t| (since 7/4 ≤ |t|/2 ⟺ 7/2 ≤ |t| ✓ from |t| ≥ 10) ≤ 2|t| ✓.\nIn Lean: ‖(1−s)/2‖: norm_div... ‖(1−s)/2‖ = ‖1−s‖/‖(2:ℂ)‖ = ‖1−s‖/2: norm_div, then ‖(2:ℂ)‖ = 2: `Complex.norm_ofNat`? or show (2:ℂ) = ((2:ℝ):ℂ); norm_real; Real.norm_eq_abs; abs_of_nonneg — LiDisc pattern (h25 at line 1034) ✓ copy: they wrote `rw [show (2/5:ℂ) = ((2/5:ℝ):ℂ) by norm_num, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg ...]` — hmm Complex.norm_real : ‖(r : ℂ)‖ = |r|? `Complex.norm_real (r : ℝ) : ‖(r : ℂ)‖ = ‖r‖`? then Real.norm_eq_abs. OK copy pattern.\n‖1 − s‖ ≤ ‖(1:ℂ)‖ + ‖s‖ = 1 + ‖s‖: norm_sub_le? ‖1 − s‖ ≤ ‖1‖ + ‖s‖ via norm_sub_le (1) s : ‖1−s‖ ≤ ‖1‖ + ‖s‖ hmm norm_sub_le : ‖a − b‖ ≤ ‖a‖ + ‖b‖ ✓; norm_one ✓.\nThen arithmetic via nlinarith with ht.\n\n  have hw2re : 0 < w2.re := by rw [hw2]; simp [Complex.div_ofNat_re, add_re, ...]; -- (s+4).re = s.re + 4 ≥ 3/2 > 0\n  have hw2im : |w2.im| = |t| / 2 := by rw [hw2]; simp [Complex.div_ofNat_im, add_im, hsim]; -- (t+0)/2: abs_div as before\n  have hw2n : ‖w2‖ ≤ 2 * |t| := ... ‖(s+4)/2‖ = ‖s+4‖/2 ≤ (‖s‖+4)/2 ≤ (5/2+|t|+4)/2 = 13/4 + |t|/2 ≤ |t| (13/4 ≤ 5 = |t|/2 ✓) ≤ 2|t|.\n  have hd1 := norm_digamma_le_log_of ht hw1re hw1im hw1n\n  have hd2 := norm_digamma_le_log_of ht hw2re hw2im hw2n\n  -- the logDeriv evaluations\n  have hev1 : logDeriv Complex.Gammaℝ (1 - s) = -(Real.log Real.pi : ℂ)/2 + (1/2 : ℂ) * Complex.digamma ((1-s)/2) :=\n    RvM.logDeriv_Gammaℝ (by simp [sub_re, one_re]; linarith [hσhi] : 0 < (1-s).re)\n  have hev2 : logDeriv Complex.Gammaℝ (s + 4) = -(Real.log Real.pi : ℂ)/2 + (1/2 : ℂ) * Complex.digamma ((s+4)/2) :=\n    RvM.logDeriv_Gammaℝ (by simp [add_re]; linarith [hσlo] : 0 < (s+4).re)\n  have hshift := logDeriv_Gammaℝ_shift htim\n  -- bracket algebra\n  have hbr : logDeriv Complex.Gammaℝ (1 - s) + logDeriv Complex.Gammaℝ s\n      = -(Real.log Real.pi : ℂ) + (1/2:ℂ)*Complex.digamma ((1-s)/2) + (1/2:ℂ)*Complex.digamma ((s+4)/2) - 2*(s+1)/(s*(s+2)) := by\n    rw [hshift, hev1, hev2]; ring\n  rw [hbr]\n  -- norm bound\n  have hlogpi : Real.log Real.pi ≤ 2 := by\n    rw [Real.log_le_iff_le_exp Real.pi_pos]  -- banked journal-024: Real.log_le_iff_le_exp (h : 0 < x) : log x ≤ y ↔ x ≤ exp y — CHECK signature: maybe (hx : 0 < x) : Real.log x ≤ y ↔ x ≤ Real.exp y ✓\n    -- π ≤ e²: e > 2.718 ⟹ e² > 7.38 > π\n    have he : Real.exp 2 > 7 := by\n      have h := Real.exp_one_gt_d9  -- e > 2.7182818283\n      rw [show (2:ℝ) = 1 + 1 by ring, Real.exp_add]... hmm exp 2 = (exp 1)^2: Real.exp_nat_mul? journal-024 banked Real.exp_nat_mul : exp (n*x) = (exp x)^n: exp 2 = exp (2*1) = (exp 1)^2 ✓: rw [← Real.exp_nat_mul 1 2]?? direction: Real.exp_nat_mul (x n) : Real.exp (n*x) = (Real.exp x)^n: so exp 2: show (2:ℝ) = 2*1 by ring ▸ ... messy; simpler: have h2 : Real.exp 2 = Real.exp 1 ^ 2 := by rw [← Real.exp_nat_mul]; norm_num — Real.exp_nat_mul (x : ℝ) (n : ℕ) : Real.exp (n * x) = Real.exp x ^ n — so Real.exp 2 = Real.exp (2*1): `show Real.exp (↑(2:ℕ) * 1) = _` hmm the coercion: 2*1 with 2 : ℕ cast... `norm_num` might handle: rw [show (2:ℝ) = (2:ℕ) * 1 by norm_num, Real.exp_nat_mul]; ... then (exp 1)^2 > 2.718^2 > 7.3 > π: nlinarith [h, Real.pi_lt_315.le, Real.exp_pos 1]... \n```\nLet me simplify: hlogpi : Real.log π ≤ 2 via: Real.log π ≤ Real.log (exp 2) [Real.log_le_log pi_pos (le of π ≤ e²)] = 2 [Real.log_exp] — with π ≤ exp 2 from: exp 2 ≥ 2.7182² ≥ 7.38 ≥ π. Compute exp 1 > 2.718281828459045 (Real.exp_one_gt_d9 : 2.718281828459045 < exp 1 — the d9 name: Real.exp_one_gt_d9 : 2.718281828 < Real.exp 1? something). Then exp 2 = (exp 1)² > 2.718² = 7.38... > 3.15 > π: \n```\nhave he2 : Real.pi ≤ Real.exp 2 := by\n  have h1 := Real.exp_one_gt_d9  -- check actual: Real.exp_one_gt_d9 : 2.7182818283 < Real.exp 1 (10 digits)\n  have h2 : Real.exp 2 = Real.exp 1 * Real.exp 1 := by rw [← Real.exp_add]; norm_num  -- exp 2 = exp (1+1) = exp 1 * exp 1: rw [← Real.exp_add]; norm_num: goal exp (1+1) = exp 1 * exp 1: Real.exp_add: exp(1+1) = exp 1 * exp 1 ✓ then 1+1 = 2 norm_num — careful direction: goal Real.exp 2 = Real.exp 1 * Real.exp 1: rw [← Real.exp_add] gives Real.exp (1+1) = ... then norm_num closes (1+1=2)? rw [← Real.exp_add] turns RHS exp 1 * exp 1 into exp (1+1); goal: exp 2 = exp (1+1): norm_num ✓.\n  rw [h2]\n  nlinarith [h1, Real.pi_lt_315, Real.exp_pos 1]\n```\nnlinarith: exp1 > 2.7182818283, π < 3.15 ⟹ exp1 * exp1 > 2.718² ≈ 7.39 > 3.15 ✓ nlinarith [h1, pi_lt_315, exp_pos 1] should manage (products of the bound: needs (exp1)^2 > 2.7182^2: nlinarith can do: (exp1 − 2.7182818283) > 0, exp1 > 0 ⟹ exp1² > 2.7182818283² hmm nlinarith with mul_self... I'll feed: nlinarith [h1, Real.pi_lt_315, Real.exp_pos 1, sq_nonneg (Real.exp 1 − 2.7)] — will iterate at build.\n\nThen the final norm assembly:\n```\n  calc ‖-(Real.log Real.pi : ℂ) + (1/2:ℂ)*Complex.digamma w1 + (1/2:ℂ)*Complex.digamma w2 - 2*(s+1)/(s*(s+2))‖\n      ≤ Real.log Real.pi + (1/2)‖digamma w1‖ + (1/2)‖digamma w2‖ + ‖2*(s+1)/(s*(s+2))‖ := by\n        -- triangle chain + norm_neg + norm_const_mul + Complex.norm_real for (log π : ℂ)\n        ...\n    _ ≤ 2 + (1/2)(Real.log |t| + 5) + (1/2)(Real.log |t| + 5) + 1 := by gcongr [...]\n    _ = Real.log |t| + 8 := by ring\n    _ ≤ 4 * (Real.log |t|)^2 := by nlinarith [two_le_log_abs_t ht, sq_nonneg (Real.log |t| - 2)]... \n```\nWait — two_le_log_abs_t from LiDisc: check its exact statement: journal says `two_le_log_abs_t (e² ≤ 2.7183² < 10)` presumably `theorem two_le_log_abs_t {t : ℝ} (ht : 10 ≤ |t|) : 2 ≤ Real.log |t|`. It's in LiDisc.lean namespace NguyenRH1 — same namespace, accessible ✓ (need to confirm exact name at build: grep LiDisc for \"two_le_log_abs_t\").\n\nThe triangle chain: ‖A + B + C − D‖ ≤ ‖A‖ + ‖B‖ + ‖C‖ + ‖D‖: via norm_add_le thrice + norm_sub_le: ‖((A+B)+C)−D‖ ≤ ‖A+B+C‖ + ‖D‖ ≤ ... write carefully with calc/trans. Components:\n‖−(log π : ℂ)‖ = |log π| = log π (log π ≥ 0: Real.log_nonneg (one_le... π ≥ 1: Real.pi_gt_three.le.trans (by norm_num)) — norm_neg then Complex.norm_real? ‖(r:ℂ)‖ = |r|: `Complex.norm_real`? hmm — earlier: `Complex.norm_real (r : ℝ) : ‖(r:ℂ)‖ = |r|`? or `RCLike.norm_real`? LiDisc line 1035 used `Complex.norm_real` then `Real.norm_eq_abs` — hmm that gave ‖(r:ℂ)‖ = ‖r‖_ℝ = |r|. OK so: ‖−(Real.log π : ℂ)‖ = |Real.log π| = Real.log π (abs_of_nonneg (Real.log_nonneg ...)).\n‖(1/2) * digamma w‖ = (1/2)‖digamma w‖: norm_mul + ‖(1/2:ℂ)‖ = 1/2 (norm_real pattern).\n‖2*(s+1)/(s*(s+2))‖: = 2*‖s+1‖/(‖s‖*‖s+2‖) [norm_div, norm_mul, norm_real for 2] ≤ 1: 2‖s+1‖ ≤ ‖s‖‖s+2‖: 2(5/2+|t|+1)... wait ‖s+1‖ ≤ ‖s‖ + 1 ≤ 5/2+|t|+1: 2(7/2+|t|) = 7 + 2|t| ≤ |t|² (|t| ≥ 10: |t|² ≥ 10|t| = 2|t| + 8|t| ≥ 2|t| + 80 > 2|t| + 7 ✓): nlinarith [ht, hsn, ...] after div_le_iff (‖s‖*‖s+2‖ > 0: ‖s‖ ≥ |im s| = |t| > 0 ✓, ‖s+2‖ ≥ |im(s+2)| = |t| > 0 ✓ positivity).\n\nOK. And §5 capstone as planned. \n\nFor §5, the 5c application:\n```\n  have h5c := logDeriv_riemannZeta_sub_nearZeros_le (t := -t) (by rw [abs_neg]; exact ht) (s := 1 - s)\n    (by simp [sub_im, one_im, hsim])  -- (1-s).im = -t\n    (by simp [sub_re, one_re]; linarith [hσhi])  -- 1/2 ≤ (1-s).re\n    (by simp [sub_re, one_re]; linarith [hσlo])  -- (1-s).re ≤ 7/2\n    hζ1\n  rw [abs_neg] at h5c  -- log |−t| → log |t|\n```\nHmm — h5c's statement will have Real.log |−t|: the rw [abs_neg] at h5c rewrites |−t| to |t| inside ✓ (abs_neg : |−a| = |a| ✓).\n\n(1−s).im = −t: sub_im: (1−s).im = (1:ℂ).im − s.im = 0 − t = −t: simp [sub_im, one_im, hsim] ✓ probably: goal (1−s).im = −t: rw [Complex.sub_im, Complex.one_im, hsim]; ring ✓ bulletproof.\n\nThe final algebra:\n```\n  -- X := logDeriv ζ s − Σ_t\n  have hkey : logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ)/(s - ρ)\n      = -(logDeriv riemannZeta (1-s) - ∑ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ)/(1 - s - ρ'))\n        - (logDeriv Complex.Gammaℝ (1-s) + logDeriv Complex.Gammaℝ s) := by\n    rw [hfe, hrefl]  -- hfe: logDeriv ζ s = −logDeriv ζ(1−s) − (Γs + Γ1); hrefl: Σ_{−t} (1−s−ρ') = −Σ_t\n    ring\n```\ncheck: LHS after hfe: −ζ1 − (Γs + Γ1) − Σt. hrefl : Σ_{−t} = −Σ_t ⟹ Σ_t = −Σ_{−t}: so LHS = −ζ1 − (Γs+Γ1) + Σ_{−t}. RHS: −(ζ1 − Σ_{−t}) − (Γ1 + Γs) = −ζ1 + Σ_{−t} − Γ1 − Γs ✓ ring closes.\nHmm — hrefl rewrites Σ_{−t} into −Σ_t; but RHS of hkey contains Σ_{−t} which gets rewritten to −Σ_t: RHS = −(ζ1 − (−Σ_t)) − bracket = −ζ1 − Σ_t − bracket... wait: −(ζ1 − (−Σ_t)) = −ζ1 + Σ_t... let me redo: after rw [hrefl] the term ∑ ρ' ∈ nearZeros (−t), ... becomes −∑ ρ ∈ nearZeros t, ... EVERYWHERE including RHS of hkey. Then goal: LHS − Σ_t = −(ζ1 − (−Σ_t)) − bracket ⟹ −ζ1 − bracket − Σ_t = −ζ1 + Σ_t − bracket?? ✗ MISMATCH. Let me recompute: I want X = −(ζ1 − Σ_{−t}) − bracket. X = ζs − Σ_t = [−ζ1 − bracket] − Σ_t. And Σ_t = −Σ_{−t} (from hrefl). So X = −ζ1 − bracket + Σ_{−t} = −(ζ1 − Σ_{−t}) − bracket ✓. After rw [hfe, hrefl]: hfe rewrites ζs → −ζ1 − (Γs+Γ1) (in LHS of hkey). hrefl rewrites Σ_{−t} → −Σ_t: LHS has no Σ_{−t}; RHS's Σ_{−t} becomes −Σ_t. Goal becomes: (−ζ1 − bracket) − Σ_t = −(ζ1 − (−Σ_t)) − bracket = −ζ1 + Σ_t − bracket·... −(ζ1 + Σ_t)... wait −(ζ1 − (−Σ_t)) = −(ζ1 + Σ_t) = −ζ1 − Σ_t ✓. So RHS = −ζ1 − Σ_t − bracket; LHS = −ζ1 − bracket − Σ_t ✓ ring closes. \n\nThen:\n```\n  rw [hkey]\n  calc ‖-(...) − (...)‖ ≤ ‖logDeriv riemannZeta (1-s) − Σ_{−t}...‖ + ‖logDeriv ΓR (1−s) + logDeriv ΓR s‖ := (norm_sub_le _ _).trans (add_le_add_left (norm_neg _ ▸ le_rfl) _)?? \n```\n‖−A − B‖ ≤ ‖−A‖ + ‖B‖ = ‖A‖ + ‖B‖: norm_sub_le (−A) B : ‖−A − B‖ ≤ ‖−A‖ + ‖B‖; norm_neg ▸ : ‖−A‖ = ‖A‖. So:\n```\n  refine (norm_sub_le _ _).trans ?_\n  rw [norm_neg]\n  refine add_le_add h5c hbr |>.trans ?_  -- h5c : ‖ζ1 − Σ_{−t}‖ ≤ 100000 L²; hbr : ‖bracket‖ ≤ 4 L²\n  nlinarith [sq_nonneg (Real.log |t|), two_le_log_abs_t ht]\n```\n100000L² + 4L² = 100004L² ≤ 200000L² ✓ (L² ≥ 0).\n\nNow §6. Let me draft:\n\n```\n/-! ## 6. The left-plane uniform digamma bound (ii′-5e input) -/\n\n/-- The digamma recurrence iterated over a natural shift. -/\ntheorem digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (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 hwj : ∀ j : ℕ, w + (j : ℂ) ≠ 0 := by\n      intro j h\n      apply hw\n      have := congrArg Complex.im h\n      simp [Complex.add_im, Complex.natCast_im] at this  -- (w + ↑j).im = w.im + 0: simp\n      exact this\n    have hne : ∀ m : ℕ, w + (k : ℂ) ≠ -(m : ℂ) := by\n      intro m h\n      exact hwj ... hmm: w + ↑k = −↑m: im: (w+↑k).im = w.im = (−↑m).im = 0: \n      apply hw\n      have := congrArg Complex.im h\n      simp [Complex.add_im, Complex.natCast_im, Complex.neg_im] at this\n      exact this\n    have h1 := Complex.digamma_apply_add_one (w + (k : ℂ)) hne\n    -- h1 : digamma (w + ↑k + 1) = digamma (w + ↑k) + (w + ↑k)⁻¹\n    rw [show w + ((k+1 : ℕ) : ℂ) = (w + (k:ℂ)) + 1 by push_cast; ring, h1, ih, Finset.sum_range_succ]\n```\npush_cast: ((k+1 : ℕ) : ℂ) = ↑k + 1 ✓.\n\nThen the EM application. Let me define within the proof:\n```\ntheorem norm_digamma_sub_log_le_of_two_le_abs_im {w : ℂ} (hw : 2 ≤ |w.im|) :\n    ‖Complex.digamma w - Complex.log w‖ ≤ 3 := by\n  set a := w.re; set c := |w.im|\n  have hc : 2 ≤ c := hw\n  have hc0 : (0:ℝ) < c := by linarith\n  have him : w.im ≠ 0 := fun h => by rw [h, abs_zero] at hw; norm_num at hw\n  -- the shift count\n  set n := ⌈|w.re|⌉₊ + 2 with hn\n  have hnv : 0 < w.re + n := by\n    have := Nat.le_ceil |w.re|  -- |w.re| ≤ ⌈|w.re|⌉₊\n    have : (2:ℝ) ≤ (n : ℝ) := by rw [hn]; push_cast; linarith [Nat.cast_nonneg ⌈|w.re|⌉₊]  -- hmm n = ceil + 2: (n:ℝ) = ↑ceil + 2\n    -- w.re + n ≥ w.re + |w.re| + 2 ≥ 2 > 0... need (n:ℝ) ≥ |w.re| + 2: from Nat.le_ceil: |w.re| ≤ ↑⌈⌉₊: (n:ℝ) = ↑⌈|w.re|⌉₊ + 2 ≥ |w.re| + 2 ✓\n    have hcast : (n : ℝ) = (⌈|w.re|⌉₊ : ℝ) + 2 := by rw [hn]; push_cast; ring\n    have hceil : |w.re| ≤ (⌈|w.re|⌉₊ : ℝ) := Nat.le_ceil _\n    -- w.re + ↑n ≥ w.re + |w.re| + 2 ≥ 2\n    have h1 : w.re + |w.re| ≥ 0 := by ... abs: −|x| ≤ x: neg_abs_le... w.re + |w.re| ≥ 0: `neg_abs_le w.re` : −|w.re| ≤ w.re ⟹ w.re + |w.re| ≥ 0 ✓\n    linarith [hceil, h1]  -- w.re + n = w.re + ceil + 2 ≥ −|re| + |re| + 2 = 2 > 0\n  set v := w + (n : ℂ) with hv\n  have hvre : 0 < v.re := by rw [hv]; simp [Complex.add_re, Complex.natCast_re]; linarith [hnv]  -- v.re = w.re + ↑n > 0 ✓ hmm simp then linarith: v.re = w.re + (n:ℝ): exact: (w + ↑n).re = w.re + ↑n: Complex.add_re, natCast_re ✓ then 0 < that = hnv ✓ directly: after simp, goal 0 < w.re + ↑n — that's hnv ✓.\n  have hvim : v.im = w.im := by rw [hv]; simp [Complex.add_im, Complex.natCast_im]\n  -- the digamma shift\n  have hshift := digamma_add_natCast him n  -- digamma v = digamma w + Σ_{j<n} (w+↑j)⁻¹\n  -- EM for f x = (w + ↑x)⁻¹\n  set f : ℝ → ℂ := fun x => (w + (x : ℂ))⁻¹ with hf\n  have hdiff : ∀ x : ℝ, HasDerivAt f (-(w + (x:ℂ))⁻¹ ^ 2)?? \n```\nhmm — deriv f x = −(w+↑x)^{−2}: HasDerivAt.inv form: `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt f⁻¹ (−f' / f x ^ 2) x`? Let me check exact: `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun x => (f x)⁻¹) (-f' / f x ^ 2) x`? I believe the value is `-(f x ^ 2)⁻¹ * f'`? In Mathlib: `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt f⁻¹ (-f' / f x ^ 2) x`. Hmm not sure of exact form. For g x = w + ↑x with g' = 1: inv gives HasDerivAt g⁻¹ (−1/(w+↑x)^2) x. Let me use comp_ofReal again: e z := (w + z)⁻¹: HasDerivAt e (−(w+z)^2)⁻¹... hasDerivAt_inv? `hasDerivAt_inv (x : ℂ) (hx : x ≠ 0) : HasDerivAt (·⁻¹) (-(x⁻¹^2)) x`? hmm: hasDerivAt_inv (hx : x ≠ 0) : HasDerivAt Inv.inv (-(x^2))⁻¹ x? I recall `hasDerivAt_inv (hx : x ≠ 0) : HasDerivAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) x`. Compose: e = Inv.inv ∘ (w + ·): (hasDerivAt_inv hnez).comp z ((hasDerivAt_id' z).const_add w): HasDerivAt (Inv.inv ∘ (w+·)) ((-(w+z)^2)⁻¹ * 1) z = (−(w+z)^2)⁻¹. Then comp_ofReal: HasDerivAt (fun y : ℝ => e ↑y) (−(w+↑y)^2)⁻¹ y. And f = fun y => (w + ↑y)⁻¹ = e ∘ ofReal ✓ defeq: (fun y => e ↑y) = fun y => (w + ↑y)⁻¹: rfl? e ↑y = (w + ↑y)⁻¹ by rfl ✓ (e defined as such). So:\n```\n  have hder : ∀ x : ℝ, HasDerivAt f (-((w + (x:ℂ)) ^ 2)⁻¹) x := by\n    intro x\n    have hne : w + (x:ℂ) ≠ 0 := by\n      intro h; apply him\n      have := congrArg Complex.im h\n      simpa [Complex.add_im, Complex.ofReal_im] using this\n    have h1 : HasDerivAt (fun z : ℂ => (w + z)⁻¹) (-((w + (x:ℂ)) ^ 2)⁻¹) (x : ℂ) := by\n      have := (hasDerivAt_inv hne).comp (x:ℂ) ((hasDerivAt_id' (x:ℂ)).const_add w)\n      -- this : HasDerivAt (Inv.inv ∘ (w + ·)) (−((w + ↑x)^2)⁻¹ * 1) ↑x\n      simpa [Function.comp_def] using this\n    have h2 := h1.comp_ofReal\n    -- h2 : HasDerivAt (fun y : ℝ => (fun z => (w+z)⁻¹) ↑y) (−((w+↑x)^2)⁻¹) x\n    exact h2  -- defeq with f\n```\nWatch: hasDerivAt_inv signature: `hasDerivAt_inv (hx : x ≠ 0) : HasDerivAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) x`? or `HasDerivAt Inv.inv (-x ^ 2)⁻¹ x`? hmm — I think: `hasDerivAt_inv (hx : x ≠ 0) : HasDerivAt (fun x => x⁻¹) (-x⁻¹ ^ 2) x`?? not sure. There's definitely `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun x => (f x)⁻¹) (-f' / (f x) ^ 2) x`. Use that with hf = (hasDerivAt_id' z).const_add w : HasDerivAt (fun z => w + z) 1 z: .inv hne : HasDerivAt (fun z => (w+z)⁻¹) (−1/(w+z)^2) z. −1/(w+z)² = −((w+z)²)⁻¹: neg_div... one_mul: −1/(w+z)^2 = −((w+z)^2)⁻¹ by rw [div_eq_mul_inv, neg_one_mul]?? −1/u = −(1 * u⁻¹) = −u⁻¹ ✓: `neg_one_mul`? −1/u = (−1) * u⁻¹ = −u⁻¹: div_eq_mul_inv: 1/u = 1 * u⁻¹ hmm: −1/u = −(1/u) = −(1 * u⁻¹) = −u⁻¹: `neg_div`, `one_mul` ✓. Then .comp_ofReal. Whatever exact form — adaptable at build.\n\n  Then: hf_diff : ∀ t ∈ Set.Icc 0 n, DifferentiableAt ℝ f t := fun t _ => (hder t).differentiableAt\n  h_cont : ContinuousOn (deriv f) [[0, n]]: deriv f = fun x => −((w+↑x)^2)⁻¹: funext x: (hder x).deriv; ContinuousOn: the function x ↦ −(w+↑x)²⁻¹ is continuous (denominator ≠ 0 everywhere: hne for all x ✓): Continuous.div... : Continuous fun x => ((w + ↑x)^2)⁻¹: continuous_inv₀ (fun x => pow_ne_zero 2 (hne x)) ∘ (continuous_const.add continuous_ofReal...). `Complex.continuous_ofReal : Continuous Complex.ofReal` ✓. continuous_const.add Complex.continuous_ofReal : Continuous (fun x => w + ↑x) ✓ .pow 2, .inv₀. Then neg. So:\n```\n  have hcontfun : Continuous fun x : ℝ => -(((w + (x:ℂ)) ^ 2)⁻¹) := by\n    apply Continuous.neg\n    apply Continuous.inv₀ _ (fun x => pow_ne_zero 2 (hne x))  -- hne needs ∀ x factored out\n    exact (continuous_const.add Complex.continuous_ofReal).pow 2\n  have hderiv_eq : deriv f = fun x : ℝ => -(((w + (x:ℂ)) ^ 2)⁻¹) := funext fun x => (hder x).deriv\n  have hcont : ContinuousOn (deriv f) (Set.uIcc 0 (n:ℝ)) := by rw [hderiv_eq]; exact hcontfun.continuousOn\n```\nEM: `sum_eq_integral_add_integral_deriv (ha : 0 ≤ a) (hab : a ≤ b) (hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t) (h_cont : ContinuousOn (deriv f) [[a,b]])` — with a = 0, b = ↑n: ∑ k ∈ Ioc ⌊0⌋₊ ⌊↑n⌋₊, f ↑k = f 0 * B1 0 − f ↑n * B1 ↑n + ∫₀ⁿ f + ∫₀ⁿ deriv f * B1.\n⌊(0:ℝ)⌋₊ = 0 (Nat.floor_zero), ⌊(n:ℝ)⌋₊ = n (Nat.floor_natCast ✓).\nB1 0 = −1/2: B1 def: x − ⌊x⌋₊ − 1/2: B1 0 = 0 − 0 − 1/2 ✓: `show B1 0 = -1/2` by unfold B1; simp. B1 ↑n = ↑n − ↑n − 1/2 = −1/2: unfold B1; rw [Nat.floor_natCast]; simp.\nSum: ∑ k ∈ Ioc 0 n, f ↑k = ∑ j ∈ range n, f ↑(j+1) — via my earlier plan:\n```\n  have hIoc : Finset.Ioc 0 n = (Finset.range (n+1)).erase 0 := by\n    ext x; simp [Finset.mem_Ioc, Finset.mem_erase, Finset.mem_range]; omega\n  -- Σ_{Ioc 0 n} f k = Σ_{range (n+1)} f − f 0 = Σ_{range n} f + f n − f 0\n```\nThen algebra: Σ_{j ∈ range n} f j = Σ_{Ioc} f − f n + f 0 = [f 0·B1 0 − f n·B1 n + ∫f + ∫f'B1] − f n + f 0 = ∫f + ∫f'B1 + (f 0 − f n)/2 ·... f 0·(−1/2) − f n·(−1/2) − f n + f 0 = f 0/2 − f n/2 = (f 0 − f n)/2 ✓.\nSo:\n```\n  have hsum : ∑ j ∈ Finset.range n, f (j : ℝ) = (∫ x in 0..(n:ℝ), f x) + (f 0 - f n)/2 + ∫ x in 0..(n:ℝ), deriv f x * (B1 x : ℂ) := by\n    ...algebra from EM + hIoc + B1 values...\n```\nNote the EM integrand: deriv f t * B1 t — with the RCLike coe: deriv f t * ((B1 t : ℝ) : ℂ)? In the lemma statement `∫ t in a..b, deriv f t * B1 t` with 𝕜 := ℂ and B1 : ℝ → ℝ: there's a coercion ℝ → ℂ inserted: deriv f t * ↑(B1 t). OK.\n\nAlso note: f j for j : ℕ in the range sum vs f ↑k with k ∈ Ioc: same function f applied to casts. And the digamma shift's sum: ∑ j ∈ range n, (w + (j:ℂ))⁻¹ = ∑ j ∈ range n, f ↑j ✓ same.\n\nThe integral ∫₀ⁿ f = log v − log w:\n```\n  have hint : ∫ x in (0:ℝ)..(n:ℝ), f x = Complex.log v - Complex.log w := by\n    have hanti : ∀ x ∈ Set.uIcc 0 (n:ℝ), HasDerivAt (fun y : ℝ => Complex.log (w + (y:ℂ))) ((w + (x:ℂ))⁻¹) x := by\n      intro x _\n      have hne : w + (x:ℂ) ≠ 0 := ...\n      have hslit : w + (x:ℂ) ∈ Complex.slitPlane := by\n        rw [Complex.mem_slitPlane_iff]; right  -- im ≠ 0\n        simp [Complex.add_im, Complex.ofReal_im]; exact him  -- (w+↑x).im = w.im ≠ 0\n      have h1 : HasDerivAt (fun z : ℂ => Complex.log (w + z)) (w + (x:ℂ))⁻¹ (x:ℂ) := by\n        have := (Complex.hasDerivAt_log hslit).comp (x:ℂ) ((hasDerivAt_id' (x:ℂ)).const_add w)\n        simpa [Function.comp_def] using this  -- ((w+↑x)⁻¹ * 1)\n      exact h1.comp_ofReal\n    have hconti : IntervalIntegrable (fun x : ℝ => (w + (x:ℂ))⁻¹) volume 0 (n:ℝ) := by\n      apply ContinuousOn.intervalIntegrable\n      -- continuous since denominators nonzero\n      ...\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]\n    -- log (w + ↑n) − log (w + ↑0): w + ↑n = v (defeq: v = w + ↑n ✓ rfl); w + ↑(0:ℝ) = w: simp\n    simp [hv]  -- hmm: f's FTC gives Complex.log (w + ↑(↑n : ℝ)) − Complex.log (w + ↑(0:ℝ)): (↑(↑n:ℝ) : ℂ) = (↑n : ℂ) ✓ defeq; ↑0 = 0, w + 0 = w simp\n```\nintervalIntegral.integral_eq_sub_of_hasDerivAt signature: `(hf : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b − f a` ✓. Note the uIcc membership: `Set.mem_uIcc`... fine.\n\nThe remainder bound:\n```\n  have hrem : ‖∫ x in (0:ℝ)..(n:ℝ), deriv f x * (B1 x : ℂ)‖ ≤ (1/2) * (Real.pi / c) := by\n    calc ‖∫ x in 0..↑n, deriv f x * ↑(B1 x)‖\n        ≤ ∫ x in 0..↑n, ‖deriv f x * ↑(B1 x)‖ := intervalIntegral.norm_integral_le_integral_norm (Nat.cast_nonneg'...)  -- hmm: needs a ≤ b: 0 ≤ ↑n ✓ (Nat.cast_nonneg)\n      _ ≤ ∫ x in 0..↑n, (1/2) * (((x + a)^2 + c^2)⁻¹) := by\n          apply intervalIntegral.integral_mono_on (le_refl... 0 ≤ ↑n) hint1 hint2 _\n          intro x hx\n          -- ‖deriv f x * ↑(B1 x)‖ = ‖deriv f x‖ * |B1 x| ≤ ‖w+↑x‖⁻² * (1/2) = (1/2) * ((x+a)²+c²)⁻¹\n          rw [hderiv_eq]  -- pointwise? deriv f x value via hderiv_eq: deriv f x = −((w+↑x)²)⁻¹ by rw [hderiv_eq]\n          have hB : |B1 x| ≤ 1/2 := abs_B1_le_half (le_trans (Nat.cast_nonneg ...) hx.1)  -- hx : x ∈ Icc 0 ↑n: 0 ≤ x\n          have hnorm : ‖-(((w + (x:ℂ)) ^ 2)⁻¹) * ↑(B1 x)‖ = ‖w + (x:ℂ)‖⁻¹^2 * |B1 x| := by\n            rw [norm_mul, norm_neg, norm_inv, norm_pow, Complex.norm_real, Real.norm_eq_abs]\n            ring  -- hmm ‖(w+↑x)²‖ = ‖w+↑x‖²: norm_pow ✓; ⁻¹: norm_inv ✓\n          -- ‖w + ↑x‖⁻² = ((x + a)² + c²)⁻¹\n          have hnsq : ‖w + (x:ℂ)‖ ^ 2 = (x + a)^2 + c^2 := by\n            rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n            simp [Complex.add_re, Complex.ofReal_re, Complex.add_im, Complex.ofReal_im]\n            -- (w.re + x)² + w.im² = (x+a)² + c²: a = w.re, c = |w.im|, c² = w.im² (sq_abs)\n            rw [sq_abs]  -- hmm c = |w.im|: c^2 = |w.im|^2 = w.im^2: sq_abs w.im : |w.im|^2 = w.im^2\n            ring\n          rw [hnorm]  -- goal: ‖w+↑x‖⁻¹^2 * |B1 x| ≤ (1/2)*((x+a)²+c²)⁻¹\n          rw [← hnsq]  -- hmm getting messy; instead: (1/2) * ((x+a)²+c²)⁻¹ = (1/2) * (‖w+↑x‖^2)⁻¹\n          ...\n```\nThis pointwise chain is fiddly but standard. Then:\n```\n      _ = (1/2) * ∫ x in 0..↑n, ((x + a)^2 + c^2)⁻¹ := intervalIntegral.integral_mul_const _ _ |>.symm... \n      _ ≤ (1/2) * (Real.pi / c) := by gcongr (need ∫₀ⁿ ≤ π/c — the arctan FTC bound)\n```\nThe arctan bound:\n```\n  have harctan : ∫ x in (0:ℝ)..(n:ℝ), ((x + a)^2 + c^2)⁻¹ ≤ Real.pi / c := by\n    have hanti : ∀ x ∈ Set.uIcc 0 (n:ℝ), HasDerivAt (fun y : ℝ => (1/c) * Real.arctan ((y + a)/c)) (((x + a)^2 + c^2)⁻¹) x := by\n      intro x _\n      have h1 : HasDerivAt (fun y : ℝ => (y + a)/c) (1/c) x := ((hasDerivAt_id x).add_const a).div_const c\n      have h2 := h1.arctan  -- Real.HasDerivAt.arctan: HasDerivAt (arctan ∘ ·) (1/(1+((x+a)/c)^2) * (1/c)) x — check name: `Real.HasDerivAt.arctan (hf : HasDerivAt f f' x) : HasDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x` ✓\n      have h3 := h2.const_mul (1/c)  -- HasDerivAt.const_mul (c') (hf) : HasDerivAt (fun x => c' * f x) (c' * f') x ✓\n      convert h3 using 1  -- derivative value: (1/c) * (1/(1+((x+a)/c)^2) * (1/c)) = ((x+a)^2+c^2)⁻¹\n      field_simp [hc0.ne']\n      ring\n    have hconti : IntervalIntegrable (fun x : ℝ => ((x + a)^2 + c^2)⁻¹) volume 0 (n:ℝ) := by\n      apply ContinuousOn.intervalIntegrable\n      apply Continuous.inv₀ _ (fun x => by positivity... (x+a)^2 + c^2 ≠ 0: c > 0: nlinarith [sq_nonneg (x+a), hc0])  -- ContinuousOn from Continuous\n      · continuity: (continuous_id.add continuous_const).pow 2 |>.add continuous_const: Continuous fun x => (x+a)^2 + c^2\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]\n    -- = (1/c)(arctan((↑n + a)/c) − arctan((0+a)/c)) ≤ π/c\n    have h1 : Real.arctan ((↑n + a)/c) - Real.arctan ((0 + a)/c) ≤ Real.pi := by\n      have hu := Real.arctan_lt_pi_div_two ((↑n + a)/c)\n      have hv := Real.neg_pi_div_two_lt_arctan ((0 + a)/c)\n      linarith [Real.pi_pos]\n    rw [...]  -- massage: (1/c)*u − (1/c)*v = (1/c)*(u−v) ≤ (1/c)*π = π/c (c > 0)\n    rw [div_le_iff... \n```\n`Real.neg_pi_div_two_lt_arctan` — need to confirm exists; fallback: −arctan: arctan (a/c) < π/2 ⟹ −π/2 < −arctan... use Real.arctan_neg: arctan(−x) = −arctan x: −(π/2) < arctan v ⟺ arctan (−v) < π/2 ✓: have := Real.arctan_lt_pi_div_two (−((0+a)/c)); rw [Real.arctan_neg] at this; linarith. Robust.\n\nThen final assembly:\n```\n  -- ψ v − log v bound (v = w + n)\n  have hv1 : ‖Complex.digamma v - Complex.log v‖ ≤ 1 := by\n    have hst := StirlingVert.digamma_stirling hvre (by rw [hvim]; linarith [hc] : 1/2 ≤ |v.im|)\n    calc ‖Complex.digamma v - Complex.log v‖ \n        = ‖(Complex.digamma v - Complex.log v + (1/2:ℂ)/v) - (1/2:ℂ)/v‖ := by congr 1; ring\n      _ ≤ ‖...‖ + ‖(1/2:ℂ)/v‖ := norm_sub_le _ _\n      _ ≤ 3 / v.im^2 + (1/2)/‖v‖ := ...\n      _ ≤ 3/4 + 1/4 := ...  -- |v.im| = |w.im| = c ≥ 2: v.im^2 = c² ≥ 4: 3/v.im² ≤ 3/4; ‖v‖ ≥ |v.im| = c ≥ 2: (1/2)/‖v‖ ≤ (1/2)/2 = 1/4\n      _ ≤ 1 := by norm_num\n  -- the difference [Σ f − (log v − log w)]\n  have hmid : ‖∑ j ∈ Finset.range n, f (j:ℝ) - (Complex.log v - Complex.log w)‖ ≤ 1/2 + (1/2) * (Real.pi / c) := by\n    rw [hsum, hint]  -- Σ f = ∫f + (f0 − fn)/2 + ∫f'B1 = (log v − log w) + (f0 − fn)/2 + ∫f'B1\n    -- (log v − log w) + (f0−fn)/2 + rem − (log v − log w) = (f0−fn)/2 + rem\n    have : (∫... ) ... — algebra: ring_nf to cancel\n    calc ‖((Complex.log v - Complex.log w) + (f 0 - f ↑n)/2 + ∫ f'B1) - (Complex.log v - Complex.log w)‖\n        = ‖(f 0 - f ↑n)/2 + ∫ f'B1‖ := by congr 1; ring\n      _ ≤ ‖(f 0 - f ↑n)/2‖ + ‖∫ f'B1‖ := norm_add_le _ _\n      _ ≤ 1/2 + (1/2)*(Real.pi/c) := add_le_add hboundary hrem\n  hboundary : ‖(f 0 - f ↑n)/2‖ ≤ 1/2: ‖(f 0 − f n)/2‖ ≤ (‖f 0‖ + ‖f n‖)/2 ≤ (1/2 + 1/2)/2 = 1/2: ‖f 0‖ = ‖(w+0)⁻¹‖ = ‖w‖⁻¹ ≤ 1/2 (‖w‖ ≥ c ≥ 2); ‖f ↑n‖ = ‖v‖⁻¹ ≤ 1/2 (‖v‖ ≥ |v.im| = |w.im| = c ≥ 2). norm_div: ‖X/2‖ = ‖X‖/2: ‖(2:ℂ)‖ = 2 pattern. ‖f 0 − f ↑n‖ ≤ ‖f 0‖ + ‖f ↑n‖ (norm_sub_le) ≤ 1/2+1/2 = 1 ⟹ /2 ≤ 1/2 ✓.\n  -- final:\n  calc ‖Complex.digamma w - Complex.log w‖\n      = ‖(Complex.digamma v - Complex.log v) - (∑ j ∈ range n, f (j:ℝ) - (Complex.log v - Complex.log w))‖ := by\n        congr 1\n        -- digamma w = digamma v − Σ f [hshift]; expand: digamma v − Σf − log w = (digamma v − log v) − (Σf − (log v − log w)) ✓ ring\n        rw [hshift]; ring\n    _ ≤ ‖digamma v − log v‖ + ‖Σf − (log v − log w)‖ := norm_sub_le _ _\n    _ ≤ 1 + (1/2 + (1/2)*(Real.pi/c)) := add_le_add hv1 hmid\n    _ ≤ 3 := by\n        -- π/c ≤ π/2 (c ≥ 2): (1/2)(π/2) = π/4 ≤ 1: total ≤ 1 + 1/2 + 1 = 2.5 ≤ 3\n        have hpc : Real.pi / c ≤ Real.pi / 2 := by gcongr (div_le_div_of_nonneg_left pi_nonneg hc0 hc : π/c ≤ π/2: div_le_div_of_nonneg_left (Real.pi_nonneg) hc0 hw : a/b ≤ a/c form: `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c') : a / c' ≤ a / b`? direction: c ≥ 2 ⟹ π/c ≤ π/2: div_le_div_of_nonneg_left Real.pi_nonneg (by norm_num : (0:ℝ) < 2) hw — check signature at build: `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (hbc : b ≤ c) : a / c ≤ a / b` hmm it's `div_le_div_of_nonneg_left` in older Mathlib / renamed `div_le_div_iff_of_pos...` journal-024 mentioned renames: \"pow_le_pow_left₀ / div_le_div_iff_of_pos_right/left (renames)\". I'll try div_le_div_of_nonneg_left and fallbacks.)\n        nlinarith [hpc, Real.pi_lt_315.le]\n```\n1 + (1/2 + (1/2)(π/c)) ≤ 1 + 1/2 + (1/2)(3.15/2) = 1.5 + 0.7875 = 2.2875 ≤ 3 ✓.\n\nWait — I need to double check the hsum algebra once more. EM: Σ_{k ∈ Ioc 0 n} f k = f 0·B1 0 − f n·B1 n + ∫f + ∫f'B1 with B1 0 = B1 n = −1/2:\n= −f(0)/2 + f(n)/2 + ∫f + ∫f'B1.\nΣ_{range n} f j = Σ_{Ioc 0 n} f k + f 0 − f n [since range n = {0..n−1}, Ioc 0 n = {1..n}].\n= −f0/2 + fn/2 + ∫f + ∫f'B1 + f0 − fn = ∫f + ∫f'B1 + f0/2 − fn/2 = ∫f + (f0 − fn)/2 + ∫f'B1 ✓ matches hsum. Good.\n\nIn Lean:\n```\n  have hEM := sum_eq_integral_add_integral_deriv (f := f) (a := 0) (b := (n:ℝ)) le_rfl (Nat.cast_nonneg n) hf_diff hcont\n  -- hEM : ∑ k ∈ Finset.Ioc ⌊(0:ℝ)⌋₊ ⌊(n:ℝ)⌋₊, f ↑k = f 0 * ↑(B1 0) − f ↑n * ↑(B1 ↑n) + ∫ + ∫\n  rw [Nat.floor_zero, Nat.floor_natCast] at hEM\n  have hB10 : B1 0 = -1/2 := by unfold B1; simp  -- B1 0 = 0 − ⌊0⌋₊ − 1/2: Nat.floor_zero... unfold B1: (0:ℝ) − ⌊(0:ℝ)⌋₊ − 1/2: simp [Nat.floor_zero]\n  have hB1n : B1 (n:ℝ) = -1/2 := by unfold B1; rw [Nat.floor_natCast]; simp\n  rw [hB10, hB1n] at hEM\n  -- sum conversion\n  have hconv : ∑ k ∈ Finset.Ioc 0 n, f (k:ℝ) = ∑ j ∈ Finset.range n, f (j:ℝ) - f 0 + f ↑n := by\n    rw [hIoc]  -- Ioc 0 n = (range (n+1)).erase 0\n    rw [Finset.sum_erase ...]  -- needs 0 ∈ range (n+1) ✓ (n+1 > 0): sum_erase (h : a ∈ s) : ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x — form: `Finset.sum_erase (s) (h : a ∈ s) : ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x − f a`? The statement: sum_erase : ∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x for a ∈ s? I recall `Finset.sum_erase (hs : a ∈ s) : ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a`? hmm there's `Finset.sum_erase_add`? and `Finset.add_sum_erase (s) (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x` ✓ that one I'm confident about: add_sum_erase.\n    -- range (n+1) sum: sum_range_succ: ∑ j ∈ range (n+1) f = ∑ j ∈ range n f + f n\n    ...\n```\nLet me structure: Σ_{erase 0 (range (n+1))} f = Σ_{range (n+1)} f − f 0 [via add_sum_erase: f 0 + Σ_{erase} = Σ_{range(n+1)} ⟹ Σ_{erase} = Σ_{range(n+1)} − f 0: `eq_sub_of_add_eq (Finset.add_sum_erase ...)`]; Σ_{range (n+1)} f = Σ_{range n} f + f n [Finset.sum_range_succ]. So Σ_{Ioc} = Σ_{range n} + f n − f 0 ⟹ Σ_{range n} = Σ_{Ioc} − f n + f 0 ✓ hconv. (add_sum_erase signature: `Finset.add_sum_erase (s : Finset α) (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x` — with f implicit — fine.)\n\nCasts: f ↑k where the Ioc sum has f (↑k : ℝ)... f : ℝ → ℂ, applied to (↑k : ℝ) ✓. And range sums f (↑j : ℝ) ✓. The digamma shift sum: (w + (↑j : ℂ))⁻¹ = f ↑j — (↑j : ℝ) then ofReal to ℂ vs (↑j : ℂ) directly: `Complex.ofReal_natCast`? : ((↑j : ℝ) : ℂ) = (↑j : ℂ): `Complex.ofReal_natCast (j : ℕ) : ((j:ℝ):ℂ) = (j:ℂ)`? hmm name: probably `Complex.ofReal_natCast` ✓ simp. So need simp bridge: f (↑j : ℝ) = (w + ↑(↑j : ℝ))⁻¹ = (w + (↑j:ℂ))⁻¹: by simp [hf, Complex.ofReal_natCast]? or norm_num1: `by simp only [hf]; rw [Complex.ofReal_natCast]`... I'll handle at build with push_cast/simp.\n\nOK. Also `Nat.cast_nonneg` variants and `Nat.le_ceil : a ≤ ⌈a⌉₊`? for ℝ: `Nat.le_ceil (a : ℝ) : a ≤ ⌈a⌉₊`? The statement: Nat.le_ceil : a ≤ ↑(Nat.ceil a)? I think `Nat.le_ceil : x ≤ ⌈x⌉₊` as `(x : ℝ) ≤ ↑(⌈x⌉₊)` hmm — Nat.ceil : ℝ → ℕ; Nat.le_ceil : a ≤ ⌈a⌉₊ where the RHS is coerced. I believe `Nat.le_ceil (a : α) : a ≤ ⌈a⌉₊` with the cast inserted ✓.\n\nOne more piece: intervalIntegral.norm_integral_le_integral_norm: `intervalIntegral.norm_integral_le_integral_norm (hab : a ≤ b) : ‖∫ x in a..b, f x‖ ≤ ∫ x in a..b, ‖f x‖` ✓ exists.\n\nintegral_mono_on: `intervalIntegral.integral_mono_on (h : a ≤ b) (hf : IntervalIntegrable f volume a b) (hg : IntervalIntegrable g volume a b) (hfg : ∀ x ∈ Set.Icc a b, f x ≤ g x) : ∫ x in a..b, f x ≤ ∫ x in a..b, g x`? — signature approximately; there's also integral_mono_ae. Adapt at build. The integrability of both sides: norm of (deriv f * B1): continuous on Icc ⟹ integrable ✓ (ContinuousOn.intervalIntegrable); the (1/2)((x+a)²+c²)⁻¹ continuous ✓.\n\nAlso for harctan bound — I evaluate ∫₀ⁿ = F(n) − F(0) then bound. Fine.\n\nLength estimate: §0–§5 ~500 lines, §6 ~400 lines. That's a full session. Let me get started. I'll write §0–§5 first, compile with `lake env lean NguyenRH1/LiReflect.lean`, iterate, then add §6.\n\nOne more check — `RvM.logDeriv_Gammaℝ` exact namespace: file Zeta23/RvM/GammaSide.lean — does it sit in `namespace Zeta23.RvM`? D-067 §4 says \"Zeta23 `RvM.logDeriv_Gammaℝ`\". LiDisc used `RvM.completedRiemannZeta_eq_Gammaℝ_mul` and `RvM.zeta_lower_bound_two` with `open Zeta23`. So RvM is Zeta23.RvM ✓. logDeriv_Gammaℝ at GammaSide.lean:65 — check its namespace quickly. Also `StirlingVert.digamma_stirling` = Zeta23.StirlingVert.digamma_stirling ✓ (namespace Zeta23, namespace StirlingVert seen). And `analyticOrderAt_zeta_one_sub` is in namespace Zeta23 (ZetaReflect.lean has `namespace Zeta23`) — with open Zeta23 it's just analyticOrderAt_zeta_one_sub ✓.\n\nLet me check GammaSide's namespace and LiContour's imports (to know what's already available transitively) and grep LiDisc for two_le_log_abs_t's exact statement.","signature":""},{"type":"text","text":"All APIs verified. Checking the last namespace details, then writing the file."},{"type":"tool_use","id":"Bash_37","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean && grep -n \"namespace\" Zeta23/RvM/GammaSide.lean | head -3 && grep -n \"two_le_log_abs_t\" /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiDisc.lean | head -3 && grep -n \"^import\" /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiContour.lean","description":"Check GammaSide namespace, two_le_log_abs_t, LiContour imports"},"extra_content":null}]