[{"type":"thinking","thinking":"I accidentally wrote `sorry` placeholders into the file (I was drafting the structure and left them). I must NOT leave sorries — let me complete the hbound proof and the digamma_diff_le proof properly before compiling. Let me think through the remaining pieces:\n\n**hbound**: ‖(z y)⁻¹ * ((c:ℝ):ℂ)‖ ≤ 5/t. \n‖(z y)⁻¹ * ((c:ℝ):ℂ)‖ = ‖(z y)⁻¹‖ * ‖((c:ℝ):ℂ)‖ = ‖z y‖⁻¹ * |c| (norm_inv, and ‖((c:ℝ):ℂ)‖ = |c| via Complex.norm_real).\n≤ (t/2)⁻¹ · (5/2) = (2/t)·(5/2) = 5/t: via mul_le_mul (inv_le: ‖z y‖⁻¹ ≤ (t/2)⁻¹ from hznorm: t/2 ≤ ‖z y‖ ⟹ ‖z y‖⁻¹ ≤ (t/2)⁻¹ via inv_le_inv₀ (norm_pos (z y ≠ 0 from hznorm > 0) (t/2 > 0)) — inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a — hmm direction: ‖z y‖⁻¹ ≤ (t/2)⁻¹ ⟺ t/2 ≤ ‖z y‖ ✓ hznorm. So:\n```lean\n  have hbound : ∀ y ∈ Set.uIoc (0 : ℝ) 1,\n      ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n    intro y _\n    have hzy : (0 : ℝ) < ‖z y‖ := by\n      have h := hznorm y\n      positivity\n    have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n      rw [norm_mul, norm_inv]\n      rw [show ((c : ℝ) : ℂ) = (((|c| : ℝ)) : ℂ) ...] -- no\n```\nHmm — ‖((c:ℝ):ℂ)‖ = |c|: `Complex.norm_real : ‖(x : ℂ)‖ = |x|`? — wait Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = |x|? Actually it's `Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = ‖x‖`? — hmm: `Complex.norm_real : ‖(x : ℂ)‖ = |x|`? Let me recall: `Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = |x|`? — hmm, actually I believe `Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = |x|`? — wait, actually in Mathlib it's `Complex.norm_real (x : ℝ) : ‖(↑x : ℂ)‖ = |x|`? Hmm — I've seen `Complex.norm_real : ‖(x : ℂ)‖ = |x|`? hmm. Actually: `Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = |x|` hmm — hold on, actually it's stated as `Complex.norm_real (x : ℝ) : ‖(x : ℂ)‖ = |x|`? — hmm I recall `Complex.norm_real : ‖(x : ℂ)‖ = |x|`? Let me just say: the codebase used `Complex.norm_real` at line 3866 (session-033 Fexpr): `rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]; norm_num` — so Complex.norm_real : ‖((x:ℝ):ℂ)‖ = |x| ✓ and then abs handling. So:\n```lean\n    have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n      rw [norm_mul, norm_inv, Complex.norm_real]\n```\nWait — the term is ((c : ℝ) : ℂ) — the Real-cast ✓ norm_real applies ✓.\n```lean\n    rw [h1]\n    have h2 : ‖z y‖⁻¹ ≤ (t / 2)⁻¹ := by\n      rw [inv_le_inv₀ hzy (by positivity)]\n      exact hznorm y\n    calc ‖z y‖⁻¹ * |c| ≤ (t / 2)⁻¹ * (5 / 2) :=\n        mul_le_mul h2 hcnorm (abs_nonneg _) (by positivity)\n      _ = 5 / t := by field_simp; ring\n```\nHmm — inv_le_inv₀ signature: `inv_le_inv₀ (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a` ✓. So h2 : ‖z y‖⁻¹ ≤ (t/2)⁻¹ via (inv_le_inv₀ hzy ht2pos).mpr (hznorm y) — hznorm : t/2 ≤ ‖z y‖ ✓ matches b ≤ a with a := ‖z y‖, b := t/2: a⁻¹ ≤ b⁻¹ ⟺ b ≤ a ✓.\nmul_le_mul (h2 : ‖z y‖⁻¹ ≤ (t/2)⁻¹) (hcnorm : |c| ≤ 5/2) (0 ≤ |c|) (0 ≤ (t/2)⁻¹): gives ‖z y‖⁻¹·|c| ≤ (t/2)⁻¹·(5/2) ✓. (t/2)⁻¹·(5/2) = 5/t: field_simp; ring — hmm: (t/2)⁻¹ = 2/t: (2/t)·(5/2) = 5/t ✓ field_simp with t ≠ 0 (ht0.ne') in context? field_simp [ht0.ne'] then ring.\n\nThen the final: ‖∫₀¹ ...‖ ≤ (5/t)·|1 − 0| = 5/t via intervalIntegral.norm_integral_le_of_norm_le_const hbound : ‖∫ y in 0..1, f y‖ ≤ (5/t)·|1−0| = 5/t ✓:\n```lean\n  calc ‖∫ y in (0:ℝ)..(1:ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)‖\n      ≤ (5 / t) * |1 - 0| := intervalIntegral.norm_integral_le_of_norm_le_const hbound\n    _ = 5 / t := by norm_num [abs_one]  -- |1 − 0| = 1: abs_of... |1-0| = 1: rw [abs_of_nonneg (by norm_num)]; norm_num\n```\nHmm — `intervalIntegral.norm_integral_le_of_norm_le_const (h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f‖ ≤ C * |b − a|` — the Ι a b is uIoc — my hbound is over Set.uIoc 0 1 — Ι = uIoc ✓ same thing (Set.uIoc = Ι? Ι a b := uIoc a b ∪ uIoc b a — intervaloc). The lemma's h is over Ι a b = uIoc a b ∪ uIoc b a. My hbound : ∀ y ∈ Set.uIoc 0 1 — since 0 ≤ 1, Ι 0 1 = uIoc 0 1 ✓ but syntactically Ι vs uIoc differ — `Set.uIoc_eq...`? Ι is notation for Set.uIoc?? No — Ι a b is `Set.uIoc a b ∪ Set.uIoc b a`? No: Ι a b = uIoc (min a b) (max a b). Hmm — `Set.uIoc` vs `Ι`: Ι a b := Set.uIoc (min a b) (max a b). For a ≤ b: Ι a b = uIoc a b (min_eq_left, max_eq_right). The membership conversion: hbound : ∀ y ∈ Set.uIoc 0 1, ... and I need ∀ y ∈ Ι 0 1: rw [show Ι (0:ℝ) 1 = Set.uIoc 0 1 from by rw [Set.uIoc...]]... ugh. Actually — from LiReflect's usage and HasPrimitives.lean:245: `intervalIntegral.norm_integral_le_of_norm_le_const hw` where hw presumably over Ι. Let me just provide the h over Ι: intro y hy — hy : y ∈ Ι 0 1 — convert to uIoc membership: `Set.mem_uIoc`... the Ι is `Set.uIoc a b ∪ Set.uIoc b a`?? Actually Ι a b is DEFINED as Set.uIoc (min...) hmm no: in Mathlib, `Ι a b := Set.uIoc a b ∪ Set.uIoc b a`? Let me recall — Ι is the \"unordered interval\": `Set.Ι a b := uIoc (min a b) (max a b)`? and there's `Set.uIoc_eq_Ι`? Hmm — actually `Ι a b = uIoc a b ∪ uIoc b a`?? No wait: I recall `Set.Ι a b := uIoc (min a b) (max a b)` and lemmas `Set.mem_Ι`... This is a rabbit hole; simplest: state hbound over `Set.Ι (0:ℝ) 1` directly and convert membership: hy : y ∈ Ι 0 1 — get bounds: y ∈ (0, 1]: `Set.mem_Ι`? or since my proof only uses hznorm (true for ALL y), the membership is unused! Look at hbound's proof: intro y _ — the membership is UNUSED (the bound holds for all y). So I can state hbound over ANY set: `∀ y ∈ Set.Ι (0:ℝ) 1, ...` with intro y _ and never use the membership ✓. Let me state it over Ι directly. The name: `Set.Ι` — in Lean: `Set.Ι` or `uIoc`? The lemma statement shows `Ι a b` — that's `Set.Ι`. In my code: `Set.Ι (0:ℝ) 1`? The Ι is notation for `Set.Ι`... Let me just use `Set.uIoc` and hope Ι = uIoc is defeq — NO. Let me check: from HasPrimitives usage: `intervalIntegral.norm_integral_le_of_norm_le_const hw` — let me look at hw's statement there to see the set form.\n\nActually — the simplest robust: use the uIoc form and if the set mismatch bites, bridge via `Set.uIoc_of_le (by norm_num : (0:ℝ) ≤ 1)`? There's `Set.uIoc_of_le (h : a ≤ b) : uIoc a b = Ι a b`? or the reverse `Set.Ι_of_le`: `Set.Ι_of_le (h : a ≤ b) : Ι a b = uIoc a b`? I recall `Set.Ι_of_le (h : a ≤ b) : Ι a b = uIoc a b` ✓ plausible. So:\n```lean\n  have hbound : ∀ y ∈ Set.Ι (0 : ℝ) 1, ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n    intro y _\n    ...\n```\nwith the membership unused ✓ (works regardless of Ι's definition).\n\n**digamma_diff_le**: \n```lean\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n      ≤ 6 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w : ℂ := s / 2 with hw\n  set w₀ : ℂ := (2 + t * Complex.I) / 2 with hw₀\n  have hw₀eq : w₀ = 1 + (t / 2) * Complex.I := by rw [hw₀]; ring\n  have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n  have hw₀im : w₀.im = t / 2 := by rw [hw₀eq]; simp\n  have himw : w.im ≠ 0 := by rw [hwim]; positivity\n  -- the recurrence: ψ(w + 2) = ψ(w) + w⁻¹ + (w+1)⁻¹\n  have hrec : Complex.digamma (w + 2) = Complex.digamma w + (w⁻¹ + (w + 1)⁻¹) := by\n    have h := digamma_add_natCast himw 2\n    rw [show w + ((2 : ℕ) : ℂ) = w + 2 by push_cast; ring] at h\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n    simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add] at h\n    exact h\n```\nHmm — the sum form after the range rws: ((0 + w⁻¹) + (w+1)⁻¹)? The sum: ∑ j ∈ range 2, (w + (j:ℂ))⁻¹ = (w + 0)⁻¹ + (w + 1)⁻¹ after the two sum_range_succ from range 0: (((∑ range 0) + f 0) + f 1) = ((0 + f 0) + f 1): simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add]: f 0 = (w + (0:ℕ))⁻¹ → (w + 0)⁻¹ → w⁻¹ (cast_zero + add_zero ✓); f 1 = (w + (1:ℕ))⁻¹ → (w + 1)⁻¹ (cast_one ✓); the (0 + w⁻¹) → w⁻¹ via zero_add ✓. So h : digamma (w+2) = digamma w + (w⁻¹ + (w+1)⁻¹) ✓.\n\nWait — digamma_add_natCast's signature: (hw : w.im ≠ 0) (n : ℕ) : digamma (w + ↑n) = digamma w + ∑ j ∈ range n, (w + ↑j)⁻¹ — the w + ↑(2:ℕ): my show `w + ((2:ℕ):ℂ) = w + 2` by push_cast; ring ✓.\n\n- Stirling at w+2 and w₀:\n```lean\n  have hvre : (0 : ℝ) < (w + 2).re := by\n    have hwre : w.re = s.re / 2 := by rw [hw]; simp\n    have h : (w + 2).re = w.re + 2 := by simp\n    rw [h, hwre]\n    linarith [hσlo]\n  have hvim : (w + 2).im = t / 2 := by\n    have h : (w + 2).im = w.im := by simp\n    rw [h, hwim]\n  have hStir1 := StirlingVert.digamma_stirling hvre (by\n    rw [hvim, abs_of_nonneg (by linarith : (0:ℝ) ≤ t/2)]\n    linarith : (1/2 : ℝ) ≤ |(w + 2).im|)\n```\nHmm the second arg: 1/2 ≤ |(w+2).im|: rw [hvim]: |(t/2)| — abs_of_nonneg → t/2: linarith (t/2 ≥ 5 ≥ 1/2 ✓). Let me write: `(by rw [hvim]; rw [abs_of_nonneg (by linarith)]; linarith)`. Hmm — the term after rw [hvim] is |t/2|: rw [abs_of_nonneg (show (0:ℝ) ≤ t/2 by linarith)] : t/2: goal 1/2 ≤ t/2 ✓ linarith.\n\nThe (w+2).re computation: (w+2).re = w.re + (2:ℂ).re = w.re + 2: `by simp` should evaluate (2:ℂ).re = 2 ✓ (Complex.add_re simp lemma + OfNat re — my piece-2 code did `hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp` which needed (2 + t·I).re = 2 — worked ✓). So `have h : (w + 2).re = w.re + 2 := by simp` ✓. Similarly im: (w+2).im = w.im ✓ by simp.\n\n- Stirling at w₀: \n```lean\n  have hw₀re : (0 : ℝ) < w₀.re := by rw [hw₀eq]; simp\n```\nw₀.re = (1 + (t/2)I).re = 1 + 0 = 1 > 0 ✓ by simp then... `rw [hw₀eq]; simp` — the goal (0:ℝ) < w₀.re → (1 + (t/2)·I).re = 1: simp gives 0 < 1 ✓ closes. \n```lean\n  have hStir2 := StirlingVert.digamma_stirling hw₀re (by\n    rw [hw₀im, abs_of_nonneg (by linarith : (0:ℝ) ≤ t/2)]; linarith)\n```\n\n- Set the remainders:\n```lean\n  set r1 : ℂ := Complex.digamma (w + 2) - Complex.log (w + 2) + (1 / 2) / (w + 2) with hr1\n  set r0 : ℂ := Complex.digamma w₀ - Complex.log w₀ + (1 / 2) / w₀ with hr0\n  have hr1le : ‖r1‖ ≤ 3 / (t / 2) ^ 2 := by rw [hr1]; rw [hvim] at hStir1; exact hStir1\n```\nhmm — hStir1 : ‖digamma (w+2) − log (w+2) + (1/2)/(w+2)‖ ≤ 3/(w+2).im² — rw [hvim] at hStir1 changes (w+2).im → t/2 ✓ then hr1le : ‖r1‖ ≤ 3/(t/2)² = hStir1 (r1 is set to exactly that expression ✓ defeq via set).\n\n- the assembly:\nψ(w) − ψ(w₀) = [log(w+2) − log w₀] + [(1/2)/w₀ − (1/2)/(w+2)] − w⁻¹ − (w+1)⁻¹ + [r1 − r0].\nCheck: ψ(w) = ψ(w+2) − w⁻¹ − (w+1)⁻¹ (from hrec) and ψ(w+2) = log(w+2) − (1/2)/(w+2) + r1 (from hr1: r1 = ψ(w+2) − log(w+2) + (1/2)/(w+2) ⟹ ψ(w+2) = log(w+2) − (1/2)/(w+2) + r1 ✓ linear) and ψ(w₀) = log w₀ − (1/2)/w₀ + r0 ✓.\nSo ψ(w) − ψ(w₀) = log(w+2) − (1/2)/(w+2) + r1 − w⁻¹ − (w+1)⁻¹ − log w₀ + (1/2)/w₀ − r0 ✓.\nThe identity as a have:\n```lean\n  have hdecomp : Complex.digamma w - Complex.digamma w₀\n      = (Complex.log (w + 2) - Complex.log w₀)\n        + ((1 / 2) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0) := by\n    rw [hr1, hr0]  -- hmm — unfold r1/r0\n    linear_combination hrec\n```\nHmm — with set r1 := expr1, hr1 : r1 = expr1. To unfold: rw [hr1] replaces r1 with expr1? hr1 : r1 = expr1 — rw [hr1] rewrites r1 → expr1 in the goal ✓ (and r0). Then the goal is a linear identity in the atoms with hrec: linear_combination hrec:\ngoal: ψw − ψw₀ = (log(w+2) − log w₀) + ((1/2)/w₀ − (1/2)/(w+2)) − w⁻¹ − (w+1)⁻¹ + ((ψ(w+2) − log(w+2) + (1/2)/(w+2)) − (ψ w₀ − log w₀ + (1/2)/w₀)).\nhrec: ψ(w+2) = ψ w + (w⁻¹ + (w+1)⁻¹).\ngoal − hrec: ψw − ψw₀ − ψ(w+2) + ψw + w⁻¹ + (w+1)⁻¹ vs the RHS expression... let me verify: RHS = log(w+2) − log w₀ + (1/2)/w₀ − (1/2)/(w+2) − w⁻¹ − (w+1)⁻¹ + ψ(w+2) − log(w+2) + (1/2)/(w+2) − ψ w₀ + log w₀ − (1/2)/w₀ = ψ(w+2) − w⁻¹ − (w+1)⁻¹ − ψ w₀. So goal: ψw − ψw₀ = ψ(w+2) − w⁻¹ − (w+1)⁻¹ − ψ w₀ ⟺ ψw = ψ(w+2) − w⁻¹ − (w+1)⁻¹ ⟺ hrec rearranged ✓. linear_combination hrec: goal_diff − (hrec_diff) = (ψw − ψw₀ − [ψ(w+2) − w⁻¹ − (w+1)⁻¹ − ψ w₀]) − (ψ(w+2) − [ψw + w⁻¹ + (w+1)⁻¹]) = ψw − ψ(w+2) + ψw + w⁻¹ + (w+1)⁻¹ − ψ(w+2) + ψw... let me just trust linear_combination hrec (sign maybe −hrec; fix at build).\n\n- the norm chain:\n```lean\n  have hnorm : ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ 5 / t + 5 / t ^ 2 + 2 / t + 2 / t + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := by\n    rw [hdecomp]\n    -- five-part norm chain via norm haves + linarith\n    have hL : ‖Complex.log (w + 2) - Complex.log w₀‖ ≤ 5 / t := by\n      rw [hw₀eq]  -- log w₀ = log (1 + (t/2)I)\n      -- and w = s/2: log (w + 2) = log (s/2 + 2)\n      rw [hw]\n      exact log_diff_le ht hσlo hσhi him\n    have h12 : ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ ≤ 5 / t ^ 2 := by\n      -- (1/2)/w₀ − (1/2)/(w+2) = (1/2)·(w+2−w₀)/(w₀(w+2)): norm ≤ (1/2)·|c|/(‖w₀‖‖w+2‖)\n      ...\n```\nThe (1/2)/w₀ − (1/2)/(w+2): = (1/2)·(1/w₀ − 1/(w+2)) = (1/2)·(w+2−w₀)/(w₀·(w+2)). And w+2 − w₀ = c' = ((c:ℝ):ℂ) (from htarget: w₀ + c' = s/2 + 2 = w + 2 ⟹ w + 2 − w₀ = c' ✓). ‖·‖ = (1/2)·|c|/(‖w₀‖‖w+2‖) ≤ (1/2)·(5/2)/((t/2)(t/2)) = (5/4)·(4/t²) = 5/t² ✓.\nIn Lean:\n```lean\n    have h12 : ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ ≤ 5 / t ^ 2 := by\n      have hw₀0 : w₀ ≠ 0 := by\n        intro h\n        have := hznorm... -- hmm w₀ = z 0: ‖w₀‖ ≥ t/2 > 0\n      have hw2 : w + 2 ≠ 0 := by ...\n      have h1 : (1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)\n          = (1 / 2) * ((w + 2 - w₀) / (w₀ * (w + 2))) := by\n        field_simp\n        ring\n      rw [h1, norm_mul, norm_div]\n      ...\n```\nfield_simp with hw₀0, hw2: (1/2)/w₀ − (1/2)/(w+2) = (1/2)(w+2−w₀)/(w₀(w+2)): field_simp [hw₀0, hw2] then ring — the identity: LHS·(w₀(w+2)) = (1/2)(w+2) − (1/2)w₀ = (1/2)(w+2−w₀) ✓. Then norm: (1/2)·‖w+2−w₀‖/(‖w₀‖‖w+2‖). ‖w+2−w₀‖ = |c| (htarget rearranged: w+2−w₀ = c' — from htarget : w₀ + ↑c = w + 2: w + 2 − w₀ = ↑c: by linear_combination htarget? or: have : w + 2 − w₀ = ((c:ℝ):ℂ) := by linear_combination htarget — hmm htarget : w₀ + ↑c = w + 2: w + 2 − w₀ = ↑c ⟺ htarget: linear_combination htarget ✓). ‖↑c‖ = |c| ≤ 5/2. ‖w₀‖ ≥ t/2 (hznorm 0: z 0 = w₀ + 0 = w₀: rw [hz] at hznorm 0: z 0 = w₀ + ((0·c:ℝ):ℂ) = w₀: simp). ‖w+2‖ ≥ t/2 (im = t/2 via hvim + abs_im_le_norm). So the product ≥ t²/4: 1/(product) ≤ 4/t². Then (1/2)·(5/2)·(4/t²) = 5/t² ✓.\nThe ≠ 0's: w₀ ≠ 0 (‖w₀‖ ≥ t/2 ≥ 5 > 0); w+2 ≠ 0 (‖w+2‖ ≥ t/2 > 0); w ≠ 0 (‖w‖ ≥ t/2); w+1 ≠ 0 (im(w+1) = t/2 ≠ 0 or ‖w+1‖ ≥ t/2).\n```lean\n    have hw1 : ‖(w⁻¹ : ℂ)‖ ≤ 2 / t := by\n      rw [norm_inv]\n      have h : t / 2 ≤ ‖w‖ := by\n        have h1 := abs_im_le_norm w\n        rw [hwim, abs_of_nonneg (by linarith : (0:ℝ) ≤ t/2)] at h1\n        exact h1\n      rw [inv_le...] hmm: ‖w⁻¹‖ = ‖w‖⁻¹ ≤ (t/2)⁻¹ = 2/t: \n      have h2 : ‖w‖⁻¹ ≤ (t / 2)⁻¹ := by\n        rw [inv_le_inv₀ (by positivity ... ‖w‖ > 0) (by positivity : (0:ℝ) < t/2)]\n        exact h\n      rw [h2]  -- hmm ‖w⁻¹‖ = ‖w‖⁻¹ already from norm_inv\n      field_simp?  (t/2)⁻¹ = 2/t: \n```\n‖w⁻¹‖ = ‖w‖⁻¹ ≤ (t/2)⁻¹ = 2/t: the last: (t/2)⁻¹ = 2/t: `by field_simp`? (t/2)⁻¹ = 2/t ⟺ 1/(t/2) = 2/t ⟺ t = 2·(t/2) ✓ field_simp with t ≠ 0. So:\n```lean\n    have hw1 : ‖(w : ℂ)⁻¹‖ ≤ 2 / t := by\n      have hwn : t / 2 ≤ ‖w‖ := by\n        have h1 := abs_im_le_norm w\n        rw [hwim, abs_of_nonneg (by linarith : (0:ℝ) ≤ t/2)] at h1\n        exact h1\n      have hpos : (0 : ℝ) < ‖w‖ := by positivity\n      rw [norm_inv]\n      calc ‖w‖⁻¹ ≤ (t / 2)⁻¹ := by\n            rw [inv_le_inv₀ hpos (by positivity : (0:ℝ) < t/2)]\n            exact hwn\n        _ = 2 / t := by field_simp\n```\nHmm — (t/2)⁻¹ = 2/t: field_simp needs t ≠ 0: ht0.ne' in context ✓ — `by field_simp` should find ht0.ne'? field_simp looks for ne hyps in context ✓ or `by rw [inv_div]...`: (t/2)⁻¹ = 2/t: inv_div: (a/b)⁻¹ = b/a ✓ `rw [inv_div]` — wait inv_div : (a/b)⁻¹ = b/a ✓. So `(t/2)⁻¹ = 2/t` by rw [inv_div] — hmm inv_div on (t/2)⁻¹ gives 2/t ✓ directly. Let me use that (no field_simp): `_ = 2 / t := by rw [inv_div]`. ✓\n\nSimilarly hw1' : ‖(w+1)⁻¹‖ ≤ 2/t: im(w+1) = w.im = t/2 ✓ same.\n\n- the r bounds: hr1le : ‖r1‖ ≤ 3/(t/2)², hr0le similarly.\n\n- the chain: ‖ψw − ψw₀‖ ≤ hL + h12 + hw1 + hw1' + (hr1le + hr0le) via the norm haves + linarith pattern (banked):\n```lean\n  have hnorm : ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ (5 / t) + (5 / t ^ 2) + (2 / t) + (2 / t) + (3 / (t / 2) ^ 2) + (3 / (t / 2) ^ 2) := by\n    rw [hdecomp]\n    have hc1 : ‖(Complex.log (w + 2) - Complex.log w₀)\n        + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0)‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n        + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖ + ‖r1 - r0‖ :=\n      norm_add_le _ _\n    ... (the per-step haves + linarith pattern)\n```\nThen the final fold: 5/t + 5/t² + 2/t + 2/t + 3/(t/2)² + 3/(t/2)² = 9/t + 5/t² + 24/t² = 9/t + 29/t². And ‖(ψw − ψw₀)/2‖ = ½‖ψw − ψw₀‖ ≤ (9/t + 29/t²)/2. Target 6/t: need (9/t + 29/t²)/2 ≤ 6/t ⟺ 9/t + 29/t² ≤ 12/t ⟺ 29/t² ≤ 3/t ⟺ 29 ≤ 3t ⟺ t ≥ 29/3 = 9.67 ✓ t ≥ 10. \n\nThe norm of /2: ‖x/2‖ = ‖x‖/2 (norm_div with ‖(2:ℂ)‖ = 2 — from my one_div_diff_le's hψnorm pattern: `rw [norm_div]; have h1 : ‖(2:ℂ)‖ = 2 := by rw [show (2:ℂ) = ((2:ℝ):ℂ) by push_cast; ring, Complex.norm_real]; norm_num; rw [h1]` ✓ reuse).\n\nThe final assembly:\n```lean\n  rw [hw, hw₀]  -- the goal's digamma args back to w, w₀? — w := s/2 IS the arg\n  -- goal: ‖(digamma w − digamma w₀)/2‖ ≤ 6/t\n  rw [norm_div]  -- hmm the /2 norm\n  have h2norm : ‖(2 : ℂ)‖ = 2 := by\n    rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n    norm_num\n  rw [h2norm]\n  rw [div_le_iff₀ (by norm_num : (0:ℝ) < 2)]\n  -- goal: ‖digamma w − digamma w₀‖ ≤ 6/t * 2\n  have hfold : (5 / t) + (5 / t ^ 2) + (2 / t) + (2 / t) + (3 / (t / 2) ^ 2) + (3 / (t / 2) ^ 2)\n      ≤ 6 / t * 2 := by\n    rw [div_le_iff₀...] hmm — 3/(t/2)² = 12/t²: \n    have h1 : (3 : ℝ) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n      field_simp\n      ring\n    rw [h1]\n    -- 5/t + 5/t² + 2/t + 2/t + 12/t² + 12/t² = 9/t + 29/t² ≤ 12/t\n    rw [div_le_iff₀ ht0]  -- hmm the t's — let me just clear denominators\n    have ht2 : (0 : ℝ) < t ^ 2 := by positivity\n    rw [div_le_iff₀ ht2]?? — the terms have different denominators — messy. Better: multiply through: show (9/t + 29/t²) ≤ 12/t: div_le_div... Let me: \n    have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n      rw [div_le_div_iff ht0 ht0]?? no — different denoms.\n```\nCleaner: 9/t + 29/t² ≤ 12/t ⟺ (multiply by t² > 0): 9t + 29 ≤ 12t ⟺ 29 ≤ 3t ✓ t ≥ 10. In Lean: \n```lean\n    have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n      have h1 : (9 / t + 29 / t ^ 2) * t ^ 2 ≤ (12 / t) * t ^ 2 := by\n        rw [div_le_iff₀... no — mul_le_mul_of_nonneg_right (h : a ≤ b) (hc : 0 ≤ c) — I need the forward: prove a·t² ≤ b·t² then conclude a ≤ b via (mul_le_mul_right ht2).mp. Let me:\n      suffices h : (9 / t + 29 / t ^ 2) * t ^ 2 ≤ (12 / t) * t ^ 2 by\n        exact (mul_le_mul_right ht2).mp h\n      rw [div_mul_cancel₀ ... ] -- messy division forms\n```\nHmm — div_mul forms: (9/t)·t² = 9t: `div_mul_cancel₀`? 9/t·t² = 9·t: rw [div_mul_eq_mul_div, ...]. Ugh. Cleanest: field_simp [ht0.ne'] on the SUFFICES goal then nlinarith:\n```lean\n    have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n      rw [div_le_iff₀ ht0]  -- (9/t + 29/t²) ≤ 12/t ⟺ ... hmm div_le_iff₀ is a/c ≤ b ↔ a ≤ b·c — the LHS here isn't a single division.\n```\nLet me use the positive-multiplier trick:\n```lean\n    have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n      rw [show (12 : ℝ) / t = 12 * t / t ^ 2 by field_simp]\n      rw [show 9 / t + 29 / t ^ 2 = (9 * t + 29) / t ^ 2 by field_simp]\n      exact div_le_div_of_nonneg_right ... no — same denominator: div_le_div_of_nonneg_right (h : a ≤ b) (c ≥ 0) : a/c ≤ b/c ✓:\n      apply div_le_div_of_nonneg_right _ (by positivity : (0:ℝ) ≤ t^2)  -- hmm direction\n      nlinarith [ht]\n```\n(9t + 29)/t² ≤ 12t/t² ⟸ 9t + 29 ≤ 12t ⟸ 29 ≤ 3t ✓ (t ≥ 10: 3t ≥ 30 ≥ 29 ✓ nlinarith [ht] — wait ht : 10 ≤ t: 3t ≥ 30 > 29 ✓ linarith). div_le_div_of_nonneg_right (hab : 9*t+29 ≤ 12*t) (hc : 0 ≤ t^2) : (9t+29)/t² ≤ 12t/t² ✓. The show-forms: 12/t = 12t/t²: field_simp (t≠0) ✓; 9/t + 29/t² = (9t+29)/t²: field_simp ✓. Then the total: 5/t + 5/t² + 2/t + 2/t + 12/t² + 12/t² = 9/t + 29/t²: by ring (same-denominator normalization ✓ ring handles). So:\n```lean\n  have hfold : (5 : ℝ) / t + 5 / t ^ 2 + 2 / t + 2 / t + 3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2\n      ≤ 6 / t * 2 := by\n    have h1 : (3 : ℝ) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n      field_simp [ht0.ne']\n      ring\n    rw [h1]\n    have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by ...\n    have hsum : (5 : ℝ) / t + 5 / t ^ 2 + 2 / t + 2 / t + 12 / t ^ 2 + 12 / t ^ 2\n        = 9 / t + 29 / t ^ 2 := by ring\n    rw [hsum]\n    linarith [hkey, ht0]  -- 9/t + 29/t² ≤ 12/t and 12/t = 6/t·2: hmm 6/t*2 = 12/t by ring — linarith sees 12/t and 6/t*2 as different atoms? (6/t)*2 vs 12/t: linarith treats 6/t*2 as (6/t)*2 — atom 6/t scaled — and 12/t is a DIFFERENT atom. Bridge: have : (6:ℝ)/t*2 = 12/t := by ring; rw [this]... let me restructure the goal as ≤ 12/t directly.\n```\nLet me simplify: make the final bound 12/t and note 6/t*2... — actually the goal after div_le_iff₀ (0<2): ‖ψw − ψw₀‖ ≤ (6/t)·2: 6/t·2 = 12/t: have h6 : (6:ℝ)/t * 2 = 12 / t := by ring. rw [h6]. Then the chain: hnorm gives ≤ 5/t + 5/t² + 2/t + 2/t + 3/(t/2)² + 3/(t/2)²; show that's ≤ 12/t via h1 + hsum + hkey. OK.\n\nLet me now also double check the hdecomp + hnorm chain plumbing. This is a LOT of fiddly code. Let me write it all out and compile. Writing the complete piece 6 now (replacing the sorry draft).","signature":""},{"type":"text","text":"I left `sorry` placeholders in the draft — let me write the complete piece 6 properly (no sorries)."},{"type":"tool_use","id":"Edit_222","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"/-! ## 8. Piece 6: the digamma difference -/\n\n/-- The log difference along the constant-imaginary segment: for\ns = σ + it with σ ∈ [−5/2, 3] and t ≥ 10: ‖log (s/2 + 2) − log (1 +\n(t/2)·I)‖ ≤ 5/t. The segment FTC: every point of the segment has\nim = t/2 (so norm ≥ t/2) and re ≥ 3/4 (slit plane); the scalar\ndifference c = σ/2 + 1 ∈ [−1/4, 5/2]. -/\ntheorem log_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖Complex.log (s / 2 + 2) - Complex.log (1 + (t / 2) * Complex.I)‖ ≤ 5 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w₀ : ℂ := 1 + (t / 2) * Complex.I with hw₀\n  set c : ℝ := s.re / 2 + 1 with hc\n  have hcle : |c| ≤ 5 / 2 := by\n    rw [hc, abs_le]\n    constructor <;> linarith\n  -- the segment z(y) = w₀ + (y·c : ℂ), y ∈ [0,1]\n  set z : ℝ → ℂ := fun y => w₀ + ((y * c : ℝ) : ℂ) with hz\n  have hzim : ∀ y : ℝ, (z y).im = t / 2 := by\n    intro y\n    rw [hz, hw₀]\n    simp [Complex.add_im, Complex.ofReal_im]\n  have hznorm : ∀ y : ℝ, t / 2 ≤ ‖z y‖ := by\n    intro y\n    have h := abs_im_le_norm (z y)\n    rw [hzim y, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h\n    exact h\n  have hzslit : ∀ y : ℝ, z y ∈ Complex.slitPlane := by\n    intro y\n    rw [Complex.mem_slitPlane_iff]\n    right\n    rw [hzim y]\n    positivity\n  -- the endpoint: w₀ + c' = s/2 + 2\n  have htarget : w₀ + ((c : ℝ) : ℂ) = s / 2 + 2 := by\n    rw [hw₀, hc]\n    rw [Complex.ext_iff]\n    constructor\n    · have h1 : (s / 2 + 2).re = s.re / 2 + 2 := by simp\n      rw [h1]\n      simp [Complex.add_re, Complex.ofReal_re]\n      ring_nf\n    · have h1 : (s / 2 + 2).im = t / 2 := by simp [him]\n      rw [h1]\n      simp [Complex.add_im, Complex.ofReal_im]\n      ring_nf\n  -- the FTC derivative family\n  have hanti : ∀ y ∈ Set.uIcc (0 : ℝ) 1,\n      HasDerivAt (fun x : ℝ => Complex.log (z x)) (((z y)⁻¹) * ((c : ℝ) : ℂ)) y := by\n    intro y _\n    have h1 : HasDerivAt (fun u : ℂ => Complex.log (w₀ + u * ((c : ℝ) : ℂ)))\n        (((z y)⁻¹) * ((c : ℝ) : ℂ)) ((y : ℝ) : ℂ) := by\n      have h2 := (Complex.hasDerivAt_log (hzslit y)).comp ((y : ℝ) : ℂ)\n        (((hasDerivAt_id' ((y : ℝ) : ℂ)).mul_const ((c : ℝ) : ℂ)).const_add w₀)\n      simpa [hz, Function.comp_def, mul_comm] using h2\n    exact h1.comp_ofReal\n  have hconti : IntervalIntegrable\n      (fun y : ℝ => ((z y)⁻¹) * ((c : ℝ) : ℂ)) volume 0 1 := by\n    apply ContinuousOn.intervalIntegrable\n    apply Continuous.continuousOn\n    apply Continuous.mul continuous_const\n    apply Continuous.inv₀ _ (fun y => by\n      have h := hznorm y\n      positivity)\n    rw [hz]\n    exact (continuous_const.add (Complex.continuous_ofReal.mul continuous_const))\n  -- the integral identity and bound\n  have hint : ∫ y in (0 : ℝ)..(1 : ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)\n      = Complex.log (s / 2 + 2) - Complex.log w₀ := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]\n    rw [hz]\n    simp only [Nat.cast_one, one_mul, Nat.cast_zero, zero_mul, add_zero]\n    rw [htarget]\n  rw [← hint]\n  have hbound : ∀ y ∈ Set.Ι (0 : ℝ) 1,\n      ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n    intro y _\n    have hzy : (0 : ℝ) < ‖z y‖ := by\n      have h := hznorm y\n      positivity\n    have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n      rw [norm_mul, norm_inv, Complex.norm_real]\n    rw [h1]\n    have h2 : ‖z y‖⁻¹ ≤ (t / 2)⁻¹ := by\n      rw [inv_le_inv₀ hzy (by positivity : (0 : ℝ) < t / 2)]\n      exact hznorm y\n    calc ‖z y‖⁻¹ * |c| ≤ (t / 2)⁻¹ * (5 / 2) :=\n        mul_le_mul h2 hcle (abs_nonneg _) (by positivity)\n      _ = 5 / t := by field_simp\n  calc ‖∫ y in (0 : ℝ)..(1 : ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)‖\n      ≤ (5 / t) * |1 - 0| := intervalIntegral.norm_integral_le_of_norm_le_const hbound\n    _ = 5 / t := by norm_num [abs_one]\n\n/-- **Piece 6** (D-069 §3): the digamma difference\n½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 6/t. Via the +2 shift (re(w+2) ≥ 3/4), Zeta23's\ndigamma_stirling at w+2 and w₀, the recurrence ψ(w) = ψ(w+2) − w⁻¹ −\n(w+1)⁻¹, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n      ≤ 6 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w : ℂ := s / 2 with hw\n  set w₀ : ℂ := (2 + t * Complex.I) / 2 with hw₀\n  have hw₀eq : w₀ = 1 + (t / 2) * Complex.I := by rw [hw₀]; ring\n  have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n  have hw₀im : w₀.im = t / 2 := by rw [hw₀eq]; simp\n  have himw : w.im ≠ 0 := by rw [hwim]; positivity\n  have hwre : w.re = s.re / 2 := by rw [hw]; simp\n  have hw₀re : (0 : ℝ) < w₀.re := by rw [hw₀eq]; simp\n  -- the recurrence: ψ(w + 2) = ψ(w) + w⁻¹ + (w+1)⁻¹\n  have hrec : Complex.digamma (w + 2) = Complex.digamma w + (w⁻¹ + (w + 1)⁻¹) := by\n    have h := digamma_add_natCast himw 2\n    rw [show w + ((2 : ℕ) : ℂ) = w + 2 by push_cast; ring] at h\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n    simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add] at h\n    exact h\n  -- the Stirling bounds at w + 2 and w₀\n  have hvre : (0 : ℝ) < (w + 2).re := by\n    have h : (w + 2).re = w.re + 2 := by simp\n    rw [h, hwre]\n    linarith [hσlo]\n  have hvim : (w + 2).im = t / 2 := by\n    have h : (w + 2).im = w.im := by simp\n    rw [h, hwim]\n  have hStir1 := StirlingVert.digamma_stirling hvre (by\n    rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n  have hStir2 := StirlingVert.digamma_stirling hw₀re (by\n    rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n  -- the remainders\n  set r1 : ℂ := Complex.digamma (w + 2) - Complex.log (w + 2) + (1 / 2) / (w + 2) with hr1\n  set r0 : ℂ := Complex.digamma w₀ - Complex.log w₀ + (1 / 2) / w₀ with hr0\n  have hr1le : ‖r1‖ ≤ 3 / (t / 2) ^ 2 := by\n    have h := hStir1\n    rw [hvim] at h\n    exact h\n  have hr0le : ‖r0‖ ≤ 3 / (t / 2) ^ 2 := by\n    have h := hStir2\n    rw [hw₀im] at h\n    exact h\n  -- the decomposition\n  have hdecomp : Complex.digamma w - Complex.digamma w₀\n      = (Complex.log (w + 2) - Complex.log w₀)\n        + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0) := by\n    rw [hr1, hr0]\n    linear_combination hrec\n  -- the pieces\n  have hL : ‖Complex.log (w + 2) - Complex.log w₀‖ ≤ 5 / t := by\n    rw [hw, hw₀eq]\n    exact log_diff_le ht hσlo hσhi him\n  have hw0norm : t / 2 ≤ ‖w₀‖ := by\n    have h1 := abs_im_le_norm w₀\n    rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw2norm : t / 2 ≤ ‖w + 2‖ := by\n    have h1 := abs_im_le_norm (w + 2)\n    rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hwnorm : t / 2 ≤ ‖w‖ := by\n    have h1 := abs_im_le_norm w\n    rw [hwim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw1norm : t / 2 ≤ ‖w + 1‖ := by\n    have h1 := abs_im_le_norm (w + 1)\n    have h2 : (w + 1).im = t / 2 := by simp [hwim]\n    rw [h2, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw₀0 : w₀ ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw0norm\n    linarith\n  have hw2 : w + 2 ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw2norm\n    linarith\n  have hw0 : w ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hwnorm\n    linarith\n  have hw1 : w + 1 ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw1norm\n    linarith\n  have h12 : ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ ≤ 5 / t ^ 2 := by\n    have h1 : (1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)\n        = (1 / 2) * ((w + 2 - w₀) / (w₀ * (w + 2))) := by\n      field_simp\n      ring\n    have hsub : w + 2 - w₀ = ((s.re / 2 + 1 : ℝ) : ℂ) := by\n      have ht1 : w₀ + ((s.re / 2 + 1 : ℝ) : ℂ) = w + 2 := by\n        rw [hw, hw₀eq]\n        rw [Complex.ext_iff]\n        constructor\n        · simp [hwre]\n          ring_nf\n        · simp [hw₀im]\n          rw [hwim]\n      linear_combination ht1\n    rw [h1, hsub, norm_mul, norm_div, Complex.norm_real]\n    have hc : |s.re / 2 + 1| ≤ 5 / 2 := by\n      rw [abs_le]\n      constructor <;> linarith\n    have h12n : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by\n      rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n      norm_num\n    rw [h12n]\n    have hprod : (t / 2) * (t / 2) ≤ ‖w₀‖ * ‖w + 2‖ :=\n      mul_le_mul hw0norm hw2norm (by positivity) (by positivity)\n    calc (1 / 2) * (|s.re / 2 + 1| / (‖w₀‖ * ‖w + 2‖))\n        ≤ (1 / 2) * ((5 / 2) / (‖w₀‖ * ‖w + 2‖)) := by\n          apply mul_le_mul_of_nonneg_left _ (by norm_num)\n          exact div_le_div_of_nonneg_right hc (by positivity)\n      _ ≤ (1 / 2) * ((5 / 2) / ((t / 2) * (t / 2))) := by\n          apply mul_le_mul_of_nonneg_left _ (by norm_num)\n          exact div_le_div_of_nonneg_left (by norm_num) (by positivity) hprod\n      _ = 5 / t ^ 2 := by field_simp; ring\n  have hw1b : ‖(w : ℂ)⁻¹‖ ≤ 2 / t := by\n    rw [norm_inv]\n    have hpos : (0 : ℝ) < ‖w‖ := by positivity\n    calc ‖w‖⁻¹ ≤ (t / 2)⁻¹ := by\n          rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n          exact hwnorm\n      _ = 2 / t := by rw [inv_div]\n  have hw1'b : ‖(w + 1 : ℂ)⁻¹‖ ≤ 2 / t := by\n    rw [norm_inv]\n    have hpos : (0 : ℝ) < ‖w + 1‖ := by positivity\n    calc ‖w + 1‖⁻¹ ≤ (t / 2)⁻¹ := by\n          rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n          exact hw1norm\n      _ = 2 / t := by rw [inv_div]\n  -- the norm chain\n  have hnorm : ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := by\n    rw [hdecomp]\n    have hc1 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0)‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖ + ‖r1 - r0‖ :=\n      norm_add_le _ _\n    have hc2 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖ + ‖(w + 1)⁻¹‖ :=\n      norm_sub_le _ _\n    have hc3 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖ + ‖w⁻¹‖ :=\n      norm_sub_le _ _\n    have hc4 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖\n        ≤ ‖Complex.log (w + 2) - Complex.log w₀‖\n          + ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ :=\n      norm_add_le _ _\n    have hc5 : ‖r1 - r0‖ ≤ ‖r1‖ + ‖r0‖ := norm_sub_le _ _\n    linarith [hc1, hc2, hc3, hc4, hc5, hL, h12, hw1b, hw1'b, hr1le, hr0le]\n  -- the fold to 6/t\n  have h2norm : ‖(2 : ℂ)‖ = 2 := by\n    rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n    norm_num\n  rw [hw, hw₀, norm_div, h2norm]\n  rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]\n  have h1 : (3 : ℝ) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n    field_simp\n    ring\n  have hsum : 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (12 / t ^ 2 + 12 / t ^ 2)\n      = 9 / t + 29 / t ^ 2 := by\n    field_simp\n    ring\n  have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n    rw [show (12 : ℝ) / t = 12 * t / t ^ 2 by field_simp; ring]\n    rw [show 9 / t + 29 / t ^ 2 = (9 * t + 29) / t ^ 2 by field_simp; ring]\n    apply div_le_div_of_nonneg_right _ (by positivity : (0 : ℝ) ≤ t ^ 2)\n    nlinarith [ht]\n  calc ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := hnorm\n    _ = 9 / t + 29 / t ^ 2 := by rw [h1]; rw [hsum]\n    _ ≤ 12 / t := hkey\n    _ = 6 / t * 2 := by ring\n\nend NguyenRH1\n\nend","new_string":"      _ ≤ 4.5 / 100 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) hprods1\n      _ = 0.045 := by norm_num\n\n/-! ## 8. Piece 6: the digamma difference -/\n\n/-- The log difference along the constant-imaginary segment: for\ns = σ + it with σ ∈ [−5/2, 3] and t ≥ 10: ‖log (s/2 + 2) − log (1 +\n(t/2)·I)‖ ≤ 5/t. The segment FTC: every point of the segment has\nim = t/2 (so norm ≥ t/2) and re ≥ 3/4 (slit plane); the scalar\ndifference c = σ/2 + 1 ∈ [−1/4, 5/2]. -/\ntheorem log_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖Complex.log (s / 2 + 2) - Complex.log (1 + (t / 2) * Complex.I)‖ ≤ 5 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w₀ : ℂ := 1 + (t / 2) * Complex.I with hw₀\n  set c : ℝ := s.re / 2 + 1 with hc\n  have hcle : |c| ≤ 5 / 2 := by\n    rw [hc, abs_le]\n    constructor <;> linarith\n  -- the segment z(y) = w₀ + (y·c : ℂ), y ∈ [0,1]\n  set z : ℝ → ℂ := fun y => w₀ + ((y * c : ℝ) : ℂ) with hz\n  have hzim : ∀ y : ℝ, (z y).im = t / 2 := by\n    intro y\n    rw [hz, hw₀]\n    simp [Complex.add_im, Complex.ofReal_im]\n  have hznorm : ∀ y : ℝ, t / 2 ≤ ‖z y‖ := by\n    intro y\n    have h := abs_im_le_norm (z y)\n    rw [hzim y, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h\n    exact h\n  have hzslit : ∀ y : ℝ, z y ∈ Complex.slitPlane := by\n    intro y\n    rw [Complex.mem_slitPlane_iff]\n    right\n    rw [hzim y]\n    positivity\n  -- the endpoint: w₀ + c' = s/2 + 2\n  have htarget : w₀ + ((c : ℝ) : ℂ) = s / 2 + 2 := by\n    rw [hw₀, hc]\n    rw [Complex.ext_iff]\n    constructor\n    · have h1 : (s / 2 + 2).re = s.re / 2 + 2 := by simp\n      rw [h1]\n      simp [Complex.add_re, Complex.ofReal_re]\n      ring_nf\n    · have h1 : (s / 2 + 2).im = t / 2 := by simp [him]\n      rw [h1]\n      simp [Complex.add_im, Complex.ofReal_im]\n      ring_nf\n  -- the FTC derivative family\n  have hanti : ∀ y ∈ Set.uIcc (0 : ℝ) 1,\n      HasDerivAt (fun x : ℝ => Complex.log (z x)) (((z y)⁻¹) * ((c : ℝ) : ℂ)) y := by\n    intro y _\n    have h1 : HasDerivAt (fun u : ℂ => Complex.log (w₀ + u * ((c : ℝ) : ℂ)))\n        (((z y)⁻¹) * ((c : ℝ) : ℂ)) ((y : ℝ) : ℂ) := by\n      have h2 := (Complex.hasDerivAt_log (hzslit y)).comp ((y : ℝ) : ℂ)\n        (((hasDerivAt_id' ((y : ℝ) : ℂ)).mul_const ((c : ℝ) : ℂ)).const_add w₀)\n      simpa [hz, Function.comp_def, mul_comm] using h2\n    exact h1.comp_ofReal\n  have hconti : IntervalIntegrable\n      (fun y : ℝ => ((z y)⁻¹) * ((c : ℝ) : ℂ)) volume 0 1 := by\n    apply ContinuousOn.intervalIntegrable\n    apply Continuous.continuousOn\n    apply Continuous.mul continuous_const\n    apply Continuous.inv₀ _ (fun y => by\n      have h := hznorm y\n      positivity)\n    rw [hz]\n    exact (continuous_const.add (Complex.continuous_ofReal.mul continuous_const))\n  -- the integral identity and bound\n  have hint : ∫ y in (0 : ℝ)..(1 : ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)\n      = Complex.log (s / 2 + 2) - Complex.log w₀ := by\n    rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hanti hconti]\n    rw [hz]\n    simp only [Nat.cast_one, one_mul, Nat.cast_zero, zero_mul, add_zero]\n    rw [htarget]\n  rw [← hint]\n  have hbound : ∀ y ∈ Set.Ι (0 : ℝ) 1,\n      ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ ≤ 5 / t := by\n    intro y _\n    have hzy : (0 : ℝ) < ‖z y‖ := by\n      have h := hznorm y\n      positivity\n    have h1 : ‖((z y)⁻¹) * ((c : ℝ) : ℂ)‖ = ‖z y‖⁻¹ * |c| := by\n      rw [norm_mul, norm_inv, Complex.norm_real]\n    rw [h1]\n    have h2 : ‖z y‖⁻¹ ≤ (t / 2)⁻¹ := by\n      rw [inv_le_inv₀ hzy (by positivity : (0 : ℝ) < t / 2)]\n      exact hznorm y\n    calc ‖z y‖⁻¹ * |c| ≤ (t / 2)⁻¹ * (5 / 2) :=\n        mul_le_mul h2 hcle (abs_nonneg _) (by positivity)\n      _ = 5 / t := by field_simp\n  calc ‖∫ y in (0 : ℝ)..(1 : ℝ), ((z y)⁻¹) * ((c : ℝ) : ℂ)‖\n      ≤ (5 / t) * |1 - 0| := intervalIntegral.norm_integral_le_of_norm_le_const hbound\n    _ = 5 / t := by norm_num [abs_one]\n\n/-- **Piece 6** (D-069 §3): the digamma difference\n½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 6/t. Via the +2 shift (re(w+2) ≥ 3/4), Zeta23's\ndigamma_stirling at w+2 and w₀, the recurrence ψ(w) = ψ(w+2) − w⁻¹ −\n(w+1)⁻¹, and the segment-FTC log bound. -/\ntheorem digamma_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) :\n    ‖(Complex.digamma (s / 2) - Complex.digamma ((2 + t * Complex.I) / 2)) / 2‖\n      ≤ 6 / t := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  set w : ℂ := s / 2 with hw\n  set w₀ : ℂ := (2 + t * Complex.I) / 2 with hw₀\n  have hw₀eq : w₀ = 1 + (t / 2) * Complex.I := by rw [hw₀]; ring\n  have hwim : w.im = t / 2 := by rw [hw]; simp [him]\n  have hw₀im : w₀.im = t / 2 := by rw [hw₀eq]; simp\n  have himw : w.im ≠ 0 := by rw [hwim]; positivity\n  have hwre : w.re = s.re / 2 := by rw [hw]; simp\n  have hw₀re : (0 : ℝ) < w₀.re := by rw [hw₀eq]; simp\n  -- the recurrence: ψ(w + 2) = ψ(w) + w⁻¹ + (w+1)⁻¹\n  have hrec : Complex.digamma (w + 2) = Complex.digamma w + (w⁻¹ + (w + 1)⁻¹) := by\n    have h := digamma_add_natCast himw 2\n    rw [show w + ((2 : ℕ) : ℂ) = w + 2 by push_cast; ring] at h\n    rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero] at h\n    simp only [Nat.cast_zero, add_zero, Nat.cast_one, zero_add] at h\n    exact h\n  -- the Stirling bounds at w + 2 and w₀\n  have hvre : (0 : ℝ) < (w + 2).re := by\n    have h : (w + 2).re = w.re + 2 := by simp\n    rw [h, hwre]\n    linarith [hσlo]\n  have hvim : (w + 2).im = t / 2 := by\n    have h : (w + 2).im = w.im := by simp\n    rw [h, hwim]\n  have hStir1 := StirlingVert.digamma_stirling hvre (by\n    rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n  have hStir2 := StirlingVert.digamma_stirling hw₀re (by\n    rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)]; linarith)\n  -- the remainders\n  set r1 : ℂ := Complex.digamma (w + 2) - Complex.log (w + 2) + (1 / 2) / (w + 2) with hr1\n  set r0 : ℂ := Complex.digamma w₀ - Complex.log w₀ + (1 / 2) / w₀ with hr0\n  have hr1le : ‖r1‖ ≤ 3 / (t / 2) ^ 2 := by\n    have h := hStir1\n    rw [hvim] at h\n    exact h\n  have hr0le : ‖r0‖ ≤ 3 / (t / 2) ^ 2 := by\n    have h := hStir2\n    rw [hw₀im] at h\n    exact h\n  -- the decomposition\n  have hdecomp : Complex.digamma w - Complex.digamma w₀\n      = (Complex.log (w + 2) - Complex.log w₀)\n        + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0) := by\n    rw [hr1, hr0]\n    linear_combination hrec\n  -- the pieces\n  have hL : ‖Complex.log (w + 2) - Complex.log w₀‖ ≤ 5 / t := by\n    rw [hw, hw₀eq]\n    exact log_diff_le ht hσlo hσhi him\n  have hw0norm : t / 2 ≤ ‖w₀‖ := by\n    have h1 := abs_im_le_norm w₀\n    rw [hw₀im, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw2norm : t / 2 ≤ ‖w + 2‖ := by\n    have h1 := abs_im_le_norm (w + 2)\n    rw [hvim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hwnorm : t / 2 ≤ ‖w‖ := by\n    have h1 := abs_im_le_norm w\n    rw [hwim, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw1norm : t / 2 ≤ ‖w + 1‖ := by\n    have h1 := abs_im_le_norm (w + 1)\n    have h2 : (w + 1).im = t / 2 := by simp [hwim]\n    rw [h2, abs_of_nonneg (by linarith : (0 : ℝ) ≤ t / 2)] at h1\n    exact h1\n  have hw₀0 : w₀ ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw0norm\n    linarith\n  have hw2 : w + 2 ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw2norm\n    linarith\n  have hw0 : w ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hwnorm\n    linarith\n  have hw1 : w + 1 ≠ 0 := by\n    intro h\n    rw [h, norm_zero] at hw1norm\n    linarith\n  have h12 : ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ ≤ 5 / t ^ 2 := by\n    have h1 : (1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)\n        = (1 / 2) * ((w + 2 - w₀) / (w₀ * (w + 2))) := by\n      field_simp\n      ring\n    have hsub : w + 2 - w₀ = ((s.re / 2 + 1 : ℝ) : ℂ) := by\n      have ht1 : w₀ + ((s.re / 2 + 1 : ℝ) : ℂ) = w + 2 := by\n        rw [hw, hw₀eq]\n        rw [Complex.ext_iff]\n        constructor\n        · simp [hwre]\n          ring_nf\n        · simp [hw₀im]\n          rw [hwim]\n      linear_combination ht1\n    rw [h1, hsub, norm_mul, norm_div, Complex.norm_real]\n    have hc : |s.re / 2 + 1| ≤ 5 / 2 := by\n      rw [abs_le]\n      constructor <;> linarith\n    have h12n : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by\n      rw [show (1 / 2 : ℂ) = ((1 / 2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n      norm_num\n    rw [h12n]\n    have hprod : (t / 2) * (t / 2) ≤ ‖w₀‖ * ‖w + 2‖ :=\n      mul_le_mul hw0norm hw2norm (by positivity) (by positivity)\n    calc (1 / 2) * (|s.re / 2 + 1| / (‖w₀‖ * ‖w + 2‖))\n        ≤ (1 / 2) * ((5 / 2) / (‖w₀‖ * ‖w + 2‖)) := by\n          apply mul_le_mul_of_nonneg_left _ (by norm_num)\n          exact div_le_div_of_nonneg_right hc (by positivity)\n      _ ≤ (1 / 2) * ((5 / 2) / ((t / 2) * (t / 2))) := by\n          apply mul_le_mul_of_nonneg_left _ (by norm_num)\n          exact div_le_div_of_nonneg_left (by norm_num) (by positivity) hprod\n      _ = 5 / t ^ 2 := by field_simp; ring\n  have hw1b : ‖(w : ℂ)⁻¹‖ ≤ 2 / t := by\n    rw [norm_inv]\n    have hpos : (0 : ℝ) < ‖w‖ := by positivity\n    calc ‖w‖⁻¹ ≤ (t / 2)⁻¹ := by\n          rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n          exact hwnorm\n      _ = 2 / t := by rw [inv_div]\n  have hw1'b : ‖(w + 1 : ℂ)⁻¹‖ ≤ 2 / t := by\n    rw [norm_inv]\n    have hpos : (0 : ℝ) < ‖w + 1‖ := by positivity\n    calc ‖w + 1‖⁻¹ ≤ (t / 2)⁻¹ := by\n          rw [inv_le_inv₀ hpos (by positivity : (0 : ℝ) < t / 2)]\n          exact hw1norm\n      _ = 2 / t := by rw [inv_div]\n  -- the norm chain\n  have hnorm : ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := by\n    rw [hdecomp]\n    have hc1 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹ + (r1 - r0)‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖ + ‖r1 - r0‖ :=\n      norm_add_le _ _\n    have hc2 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹ - (w + 1)⁻¹‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖ + ‖(w + 1)⁻¹‖ :=\n      norm_sub_le _ _\n    have hc3 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)) - w⁻¹‖\n        ≤ ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖ + ‖w⁻¹‖ :=\n      norm_sub_le _ _\n    have hc4 : ‖(Complex.log (w + 2) - Complex.log w₀)\n          + ((1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2))‖\n        ≤ ‖Complex.log (w + 2) - Complex.log w₀‖\n          + ‖(1 / 2 : ℂ) / w₀ - (1 / 2) / (w + 2)‖ :=\n      norm_add_le _ _\n    have hc5 : ‖r1 - r0‖ ≤ ‖r1‖ + ‖r0‖ := norm_sub_le _ _\n    linarith [hc1, hc2, hc3, hc4, hc5, hL, h12, hw1b, hw1'b, hr1le, hr0le]\n  -- the fold to 6/t\n  have h2norm : ‖(2 : ℂ)‖ = 2 := by\n    rw [show (2 : ℂ) = ((2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real]\n    norm_num\n  rw [hw, hw₀, norm_div, h2norm]\n  rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 2)]\n  have h1 : (3 : ℝ) / (t / 2) ^ 2 = 12 / t ^ 2 := by\n    field_simp\n    ring\n  have hsum : 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (12 / t ^ 2 + 12 / t ^ 2)\n      = 9 / t + 29 / t ^ 2 := by\n    field_simp\n    ring\n  have hkey : 9 / t + 29 / t ^ 2 ≤ 12 / t := by\n    rw [show (12 : ℝ) / t = 12 * t / t ^ 2 by field_simp; ring]\n    rw [show 9 / t + 29 / t ^ 2 = (9 * t + 29) / t ^ 2 by field_simp; ring]\n    apply div_le_div_of_nonneg_right _ (by positivity : (0 : ℝ) ≤ t ^ 2)\n    nlinarith [ht]\n  calc ‖Complex.digamma w - Complex.digamma w₀‖\n      ≤ 5 / t + 5 / t ^ 2 + (2 / t + 2 / t) + (3 / (t / 2) ^ 2 + 3 / (t / 2) ^ 2) := hnorm\n    _ = 9 / t + 29 / t ^ 2 := by rw [h1]; rw [hsum]\n    _ ≤ 12 / t := hkey\n    _ = 6 / t * 2 := by ring\n\nend NguyenRH1\n\nend"},"extra_content":null}]