[{"type":"thinking","thinking":"§0–§4 compile clean (zero errors, zero warnings). Now §5–§9. Let me write the remaining sections:\n\n§5: digammaSeriesPart + analyticity on ball(0, 1/2) + the s=0 witness.\n§6: digammaSeriesPartSub + analyticity on ball(−n, 1/2) + the split + the −2n witness.\n§7: nontrivial-zero witness.\n§8: generic analyticity + badPoint-free balls.\n§9: Gentire + capstone.\n\nLet me draft these carefully.\n\n§5:\n```lean\n/-! ## 5. The digamma series part and the witness at s = 0 -/\n\n/-- The series part of the digamma partial-fraction expansion:\nΣ'_j (1/(j+1) − 1/(w+j+1)); analytic on ball(0, 1/2). -/\ndef digammaSeriesPart (w : ℂ) : ℂ :=\n  ∑' j : ℕ, (1 / ((j : ℂ) + 1) - 1 / (w + j + 1))\n\nlemma digammaSeriesTerm_eq {w : ℂ} {j : ℕ} (hj : (j : ℂ) + 1 ≠ 0) (hw : w + j + 1 ≠ 0) :\n    1 / ((j : ℂ) + 1) - 1 / (w + j + 1) = w / (((j : ℂ) + 1) * (w + j + 1)) := by\n  field_simp\n  ring\n```\nHmm: 1/a − 1/b = (b − a)/(ab): b − a = w+j+1 − (j+1) = w ✓: field_simp + ring ✓ (banked pattern).\n\n```lean\nlemma digammaSeriesPart_analyticOn :\n    AnalyticOnNhd ℂ digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n  have hsum : Summable (fun j : ℕ => (1 : ℝ) / ((j : ℝ) + 1) ^ 2) := summable_div_add_one_sq 1\n  have hu : HasSumUniformlyOn (fun j => fun w : ℂ => 1 / ((j : ℂ) + 1) - 1 / (w + j + 1))\n      digammaSeriesPart (Metric.ball 0 (1 / 2)) := by\n    apply HasSumUniformlyOn.of_norm_le_summable hsum\n    intro j w hw\n    -- w ∈ ball(0, 1/2): ‖w‖ < 1/2\n    have hwn : ‖w‖ < 1 / 2 := by\n      have := Metric.mem_ball.mp hw\n      rw [dist_zero_right] at this\n      exact this\n    have hj1 : (0 : ℝ) < (j : ℝ) + 1 := by positivity\n    have hwj : w + (j : ℂ) + 1 ≠ 0 := by\n      intro h\n      have : ‖w + (j : ℂ) + 1‖ = 0 := by rw [h]; exact norm_zero\n      have hge : (j : ℝ) + 1 - ‖w‖ ≤ ‖w + (j : ℂ) + 1‖ := by\n        have h1 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n          simp [Complex.add_re, Complex.one_re, Complex.natCast_re]  -- natCast_re: (↑j).re = j: `Complex.natCast_re : (↑n).re = n`? there's `Complex.natCast_re` ✓ or `RCLike.natCast_re`... hmm: (↑j : ℂ).re = (j : ℝ): `Complex.natCast_re : ((n : ℂ)).re = n`? I think `Complex.natCast_re` exists (or `RCLike.natCast_re`). Let me use `Complex.natCast_re` and adjust if error.\n        have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _\n        have h3 : w.re ≥ -‖w‖ := neg_norm_le_re w  -- `neg_norm_le_re : -‖z‖ ≤ z.re`? `Complex.neg_norm_le_re`? hmm: `neg_norm_le.re`? The lemma: `Complex.neg_norm_le_re (z : ℂ) : -‖z‖ ≤ z.re`? or `Complex.re_le_norm` + `Complex.neg_le_norm`? There's `Complex.neg_norm_le_re`? If unsure: from abs_re_le_norm: |w.re| ≤ ‖w‖ ⟹ −‖w‖ ≤ w.re via abs_le. \n        linarith [h1, h2, h3]  -- wait hge : (j:ℝ)+1 − ‖w‖ ≤ ‖w+j+1‖: from h2: w.re + j + 1 ≤ ‖·‖ and w.re ≥ −‖w‖: j + 1 − ‖w‖ ≤ w.re + j + 1 ≤ ‖·‖ ✓\n      rw [this] at hge\n      linarith [hwn, hj1]  -- (j+1) − ‖w‖ ≤ 0 with ‖w‖ < 1/2 ≤ j+1: contra ✓\n    have hj0 : ((j : ℂ) + 1) ≠ 0 := by\n      intro h\n      have := congrArg Complex.re h\n      simp at this  -- (j+1).re = j+1 = 0: j + 1 > 0: `Complex.add_re, natCast_re, one_re`: this : (j:ℝ) + 1 = 0: positivity false: linarith? simp at this leaves ↑j + 1 = 0: then `have : (0:ℝ) < (j:ℝ)+1 := by positivity; linarith`. Hmm simp at this might close the goal if it reduces to False: (↑(j)+1 : ℝ) = 0 — simp knows Nat.cast_nonneg? `simp at this` with positivity facts... safer:\n      have h1 : ((j : ℂ) + 1).re = 0 := by rw [h]; simp\n      simp [Complex.add_re] at h1  -- (j:ℝ) + 1 = 0\n      have h2 : (0 : ℝ) < (j : ℝ) + 1 := by positivity\n      linarith\n    rw [digammaSeriesTerm_eq hj0 hwj, norm_div, norm_mul]\n    -- ‖w‖ / ((j+1) * ‖w+j+1‖) ≤ 1 / (j+1)²\n    have hnorm_ge : ((j : ℝ) + 1) * ((j : ℝ) + 1) / 2 ≤ ‖((j : ℂ) + 1) * (w + j + 1)‖ := by\n      rw [norm_mul]\n      have h1 : ‖((j : ℂ) + 1 : ℂ)‖ = (j : ℝ) + 1 := by\n        rw [show ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) by push_cast; ring, Complex.norm_natCast]  -- hmm: (↑j + 1 : ℂ) = ↑(j+1): push_cast; ring ✓; Complex.norm_natCast : ‖↑(j+1)‖ = ↑(j+1) — wait Complex.norm_natCast vs RCLike.norm_natCast ∀-form (journal-028 gotcha: ∀-form — use rw)... in rw position fine.\n        -- then ↑(j+1) = ↑j + 1: push_cast\n      ...\n```\nThis is getting heavy. Simplify the norm estimates: ‖(j:ℂ)+1‖ = (j:ℝ)+1: \n```lean\n      have h1 : ‖(j : ℂ) + 1‖ = (j : ℝ) + 1 := by\n        have e : ((j : ℂ) + 1) = ((j + 1 : ℕ) : ℂ) := by push_cast; ring\n        rw [e, RCLike.norm_natCast]  -- ∀-form in rw ✓\n        push_cast  -- goal ↑(j+1) = ↑j + 1: push_cast closes? push_cast : ↑(j+1) = ↑j + 1 ✓ simp form: rw [Nat.cast_add, Nat.cast_one]\n        -- safer: rw [Nat.cast_add, Nat.cast_one]\n```\nand ‖w + j + 1‖ ≥ ((j:ℝ)+1)/2: from re: (w + j + 1).re = w.re + j + 1 ≥ −‖w‖ + j + 1 > −1/2 + j + 1 = (j+1)/2 + j/2 ≥ (j+1)/2 — and ‖·‖ ≥ re: so ‖w+j+1‖ ≥ re(...) ≥ (j+1) − ‖w‖ > (j+1) − 1/2 ≥ (j+1)/2 ✓.\nThen ‖w‖/((j+1)·‖w+j+1‖) ≤ (1/2)/((j+1)·(j+1)/2) = 1/(j+1)² via div_le_div_iff₀-style juggling: \n```lean\n    have hbig : ‖w‖ / (‖(j:ℂ)+1‖ * ‖w + j + 1‖) ≤ 1 / ((j:ℝ)+1)^2 := by\n      rw [h1]  -- denominator (j+1) * ‖w+j+1‖\n      have hwj2 : ((j : ℝ) + 1) / 2 ≤ ‖w + (j : ℂ) + 1‖ := by\n        have h2 : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _\n        have h3 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n          simp [Complex.add_re, Complex.one_re, Complex.natCast_re]  -- hmm the re of ↑j + ... : build explicitly:\n        ...\n```\nHonestly the re-computation: (w + ↑j + 1).re = w.re + (↑j).re + (1:ℂ).re = w.re + j + 1: `simp [Complex.add_re]` should give w.re + (↑j).re + 1 and (↑j).re: simp lemma `Complex.natCast_re : (↑n).re = ↑n`? I believe `Complex.natCast_re` exists as simp. To be safe: `have h3 : (w + (j:ℂ) + 1).re = w.re + j + 1 := by simp [Complex.add_re]` and if simp leaves (↑j).re, add Complex.natCast_re to the simp set. I'll write `simp [Complex.add_re, Complex.natCast_re, Complex.one_re]`.\n\nThen: −‖w‖ ≤ w.re: `neg_norm_le_re`? For ℂ: `Complex.neg_norm_le_re (z : ℂ) : -‖z‖ ≤ z.re`? — I used `abs_re_le_norm` earlier (LiDigamma used Complex.abs_re_le_norm ✓): from |w.re| ≤ ‖w‖: abs_le.mp gives both ✓: `(abs_le.mp (Complex.abs_re_le_norm w)).1 : -‖w‖ ≤ w.re` ✓.\n\nOK the estimates: let A := (j:ℝ)+1 > 0. ‖denom‖ = A·‖w+j+1‖ ≥ A·(A/2) = A²/2. ‖w‖/denom ≤ (1/2)/(A²/2) = 1/A²:\n```lean\n      rw [div_le_div_iff₀ hden0 hA20]  -- ‖w‖·A² ≤ 1·(A·‖w+j+1‖)\n      -- from ‖w‖ ≤ 1/2 (hwn.le) and A·‖w+j+1‖ ≥ A²/2: ‖w‖·A² ≤ (1/2)A² ≤ A·‖w+j+1‖?? need (1/2)A² ≤ A·‖w+j+1‖ ⟺ A/2 ≤ ‖w+j+1‖ ✓ hwj2 times A ≥ 0:\n      nlinarith [hwn.le, hwj2, hj1, ...]\n```\nLet me write: goal after div_le_div_iff₀: ‖w‖ * (A^2) ≤ 1 * (A * ‖w+j+1‖): nlinarith [hwn.le, hwj2, hj1]: from A/2 ≤ ‖w+j+1‖: A·‖w+j+1‖ ≥ A²/2 (nlinarith product A·(...) with A ≥ 0); ‖w‖·A² ≤ (1/2)·A² (product (1/2 − ‖w‖)≥0 · A² ≥ 0 — nlinarith needs A² ≥ 0: sq_nonneg): 1*(A*‖..‖) = A·‖..‖ ✓. So nlinarith [hwn.le, hwj2, hj1, sq_nonneg A]? pass the pieces: `nlinarith [hwn.le, hwj2, hj1.le, sq_nonneg ((j:ℝ)+1)]` — hmm nlinarith multiplies hypotheses pairwise automatically ✓.\n\nOK — and then TendstoLocallyUniformlyOn → differentiableOn (partial sums: each term 1/(j+1) − 1/(w+j+1) differentiable on the ball: w+j+1 ≠ 0 ✓ hwj-style for all w ∈ ball — note hwj above is per-w; inside the differentiability proof I need ∀ w ∈ ball, w + j + 1 ≠ 0 — same proof (extract a standalone lemma `add_nat_add_one_ne_zero_of_mem_ball`).\n\nLet me factor a helper:\n```lean\nlemma add_nat_add_one_ne_zero_of_mem_ball {w : ℂ} (hw : w ∈ Metric.ball 0 (1/2)) (j : ℕ) :\n    w + (j : ℂ) + 1 ≠ 0 := by\n  have hwn : ‖w‖ < 1 / 2 := by\n    have h := Metric.mem_ball.mp hw\n    rwa [dist_zero_right] at this\n  intro h\n  have hre : (w + (j : ℂ) + 1).re ≤ ‖w + (j : ℂ) + 1‖ := Complex.re_le_norm _\n  rw [h, norm_zero] at hre... \n```\nhmm: rw [h] at hre: (0:ℂ).re ≤ ‖0‖: hre : (0).re ≤ 0... then hre computes: need (w+↑j+1).re = w.re + j + 1: \n```lean\n  have h1 : (w + (j : ℂ) + 1).re = w.re + (j : ℝ) + 1 := by\n    simp [Complex.add_re, Complex.natCast_re, Complex.one_re]\n  rw [h] at h1  -- h1 : (0:ℂ).re = ... : simp: h1 : 0 = w.re + j + 1: hmm (0:ℂ).re simp to 0: `simp at h1` gives 0 = w.re + ↑j + 1\n  simp at h1  -- 0 = w.re + ↑j + 1\n  have h2 : -‖w‖ ≤ w.re := (abs_le.mp (Complex.abs_re_le_norm w)).1\n  have hj0 : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n  linarith  -- 0 = w.re + j + 1 ≥ −1/2 + 0 + 1 = 1/2 > 0 contra ✓\n```\n\nOK. Rather than fully elaborating every step in my head, let me write the sections and let the compiler guide. Write §5+§6 now (the digamma splits + the 0 and −2n witnesses), compile, then §7–§9.\n\nFor §6 the −n ball version: ball(−(n:ℂ), 1/2):\n- pole avoidance: w + j + 1 ≠ 0 for j ≠ n−1: w = −(j+1) ⟹ ‖w − (−n)‖ = |n − (j+1)| ≥ 1 (j+1 ≠ n) but ‖w+n‖ < 1/2 contra ✓:\n```lean\nlemma add_nat_add_one_ne_zero_of_mem_ball_neg {n : ℕ} (hn : 1 ≤ n) {w : ℂ}\n    (hw : w ∈ Metric.ball (-(n : ℂ)) (1/2)) {j : ℕ} (hj : j ≠ n - 1) :\n    w + (j : ℂ) + 1 ≠ 0 := by\n  intro h\n  -- w = −(j+1): then ‖(−n) − (−(j+1))‖ = |j+1−n| ≥ 1\n  have h1 : w = -((j : ℂ) + 1) := by linear_combination h  -- from h: w + j + 1 = 0\n  have h2 : dist w (-(n : ℂ)) < 1 / 2 := Metric.mem_ball.mp hw\n  rw [h1] at h2\n  -- dist (−(j+1)) (−n) = ‖(j+1) − n‖ = |((j:ℝ)+1) − n|\n  rw [Complex.dist_eq] at h2  -- ‖−(j+1) − −n‖ = ‖(n:ℂ) − (j+1)‖: \n  have h3 : (-((j : ℂ) + 1)) - (-(n : ℂ)) = ((n : ℂ) - ((j : ℂ) + 1)) := by ring\n  rw [h3] at h2  -- hmm rw at h2 with h3: the pattern (−(↑j+1)) − (−↑n) ✓\n  -- ‖(n:ℂ) − (↑j+1)‖ = |(n:ℝ) − (j+1)|: via norm of real cast: (n:ℂ) − (↑j+1) = ↑((n:ℝ) − (j+1)): ofReal_sub... \n  have h4 : ‖((n : ℂ) - ((j : ℂ) + 1))‖ = |(n : ℝ) - ((j : ℝ) + 1)| := by\n    rw [show (n : ℂ) - ((j : ℂ) + 1) = ((n - (j + 1) : ℕ) : ℂ)?? — no: n vs j+1 in ℕ-sub is wrong when j+1 > n. Use ℝ: ((n:ℝ) − ((j:ℝ)+1) : ℂ)? the ofReal cast: ((x : ℝ) : ℂ): `Complex.ofReal_sub`... (n:ℂ) − (↑j + 1) = ↑((n:ℝ) − (↑j + 1)): push_cast backwards: `by push_cast; ring`?? then norm of ofReal: `Complex.norm_ofReal`? `RCLike.norm_ofReal` ∀-form (LiSkeleton used RCLike.norm_ofReal ✓): rw [show ..., RCLike.norm_ofReal]: gives ‖(x:ℝ)‖ = |x|? RCLike.norm_ofReal : ‖(x : 𝕜)‖ = |x|?? For ℂ: ‖(x:ℂ-of-real)‖ = |x| — `Complex.norm_ofReal` : ‖(r : ℂ)‖ = |r| ✓ exists (or RCLike.norm_ofReal y = |y| ✓).\n    rw [show (n : ℂ) - ((j : ℂ) + 1) = (((n : ℝ) - ((j : ℝ) + 1)) : ℂ) by push_cast; ring, Complex.norm_ofReal]\n  rw [h4] at h2\n  -- |(n:ℝ) − (j+1)| ≥ 1 since n ≠ j+1 (integers)\n  have h5 : (1 : ℝ) ≤ |(n : ℝ) - ((j : ℝ) + 1)| := by\n    have hne : n ≠ j + 1 := by\n      intro hc\n      apply hj\n      omega  -- j ≠ n − 1 with n ≥ 1: j + 1 = n ⟺ j = n − 1 ✓ omega handles? hne goal: n ≠ j+1; hj : j ≠ n − 1; from hc : n = j + 1: j = n − 1 in ℕ: omega ✓ (with hn : 1 ≤ n in context? omega sees hn ✓ since hn is a hypothesis... hn : 1 ≤ n is in scope ✓).\n    -- |n − (j+1)| ≥ 1 for distinct naturals\n    rcases lt_or_gt_of_ne hne with hlt | hgt\n    · -- n < j+1: (j+1) − n ≥ 1\n      have h6 : (n : ℝ) + 1 ≤ (j : ℝ) + 1 := by exact_mod_cast Nat.succ_le_of_lt... hmm: n < j+1 ⟹ n+1 ≤ j+1: exact_mod_cast (Nat.succ_le_iff.mpr hlt)?? n+1 ≤ j+1 ⟺ n < j+1 ✓: `Nat.succ_le_of_lt hlt : n + 1 ≤ j + 1` — wait Nat.succ_le_of_lt : a < b → a+1 ≤ b: n < j+1 ⟹ n+1 ≤ j+1 ✓. Then (n:ℝ)+1 ≤ (j:ℝ)+1 via exact_mod_cast ✓. rw [abs_of_neg (by linarith : (n:ℝ) − (j+1) < 0)]; linarith.\n    · -- n > j+1\n      have h6 : (j : ℝ) + 1 + 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hgt  -- j+1+1 ≤ n\n      rw [abs_of_pos (by linarith : 0 < (n:ℝ) − (j+1))]; linarith\n  linarith\n```\nHmm wait — h3 rewrite direction: h2 : ‖−(↑j+1) − −↑n‖ < 1/2: rw [h3] at h2 ✓. But careful Complex.dist_eq : dist a b = ‖a − b‖ ✓.\n\nOK this is doable. The M-test for the sub-series: eventually-form with u j := 6n/(j+1)² for j ≥ 2n+1... wait earlier I computed with ‖w‖ ≤ 3n/2: hmm ‖w‖ ≤ ‖w+n‖... no: w ∈ ball(−n, 1/2): ‖w‖ ≤ ‖w − (−n)‖ + ‖−n‖ < 1/2 + n. So ‖w‖ < n + 1/2 ≤ 3n/2 (n ≥ 1 ✓). For j ≥ 2n+1 (so j+1 ≥ 2n+2): ‖w+j+1‖ ≥ (j+1) − ‖w‖ > (j+1) − (n+1/2) ≥ (j+1) − (j+1)/2 = (j+1)/2 ✓ ((j+1)/2 ≥ n+1 > n+1/2 ✓ since j+1 ≥ 2n+2 ⟹ (j+1)/2 ≥ n+1 ✓). So ‖term‖ = ‖w‖/((j+1)‖w+j+1‖) ≤ (n+1/2)·2/(j+1)² = (2n+1)/(j+1)² ✓. u j := (2n+1)/((j:ℝ)+1)^2 — summable via summable_div_add_one_sq (2n+1) ✓.\n\nThe cofinite eventuality: {j | ¬ (2n+1 ≤ j)} = {j | j < 2n+1} = finite (Finset.range / Set.finite_lt...): `Set.finite_lt_nat`? {j : ℕ | j < k}.Finite: `Set.finite_Iio`? or `Set.Finite.subset (Finset.finite_toSet (Finset.range ...))`: there's `Set.finite_lt_nat (k) : {j | j < k}.Finite`? I'll use `(Set.finite_lt_nat _)`. Hmm — safer: `Set.Finite.subset (Finset.finite_range ...)`: {j | j < 2n+1} = ↑(Finset.range (2n+1)): `Finset.coe_range : ↑(range k) = {j | j < k}`? `Finset.coe_range : ↑(Finset.range k) = Set.Iio k` ✓ and Set.Iio k finite: `Set.finite_Iio` ✓ exists for locally finite orders. So (Set.finite_Iio (2*n+1)).subset (fun j hj => hj) with membership defeq ✓. Then eventually_cofinite.mpr — wait direction: eventually_cofinite : (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.Finite: rw [eventually_cofinite]; apply (Set.finite_Iio ...).subset; intro j hj; show j < 2n+1?? — {j | ¬P j} ⊆ {j | j < 2n+1}: intro j hj (hj : ¬P j); goal j ∈ {j | j < 2n+1} defeq j < 2n+1: by_contra; push Not → 2n+1 ≤ j; then prove P j contra hj ✓.\n\nHmm wait — for the sub-series M-test I need: for j ≥ 2n+1: ∀ w ∈ ball, ‖subterm j w‖ ≤ u j. subterm j w = if j = n−1 then 0 else full-term. j ≥ 2n+1 ⟹ j ≠ n−1 (2n+1 > n−1 ⟺ n > −2 ✓) ⟹ = full term: bound ✓ as computed.\n\nBut also — pole avoidance hwj for ALL j ≠ n−1 on the ball (needed for differentiability of partial sums AND for the term algebra at each w): add_nat_add_one_ne_zero_of_mem_ball_neg ✓.\n\nAnd the summability of the sub-series at each w ∈ ball — from the uniform convergence (pointwise). How to extract pointwise HasSum from HasSumUniformlyOn? There should be `HasSumUniformlyOn.hasSum (h) (hw : w ∈ s)`? Let me not need it: for the SPLIT identity I need Summable (sub at w) — get it by comparison with the FULL series at w (‖sub‖ ≤ ‖full‖ pointwise via if-zero; full summable at w ∈ integerComplement via Zeta23 summable_digamma_series). ✓ no pointwise-extraction needed. But wait — the M-test conclusion gives HasSumUniformlyOn of sub → its limit = ∑' sub = digammaSeriesPartSub — fine, no pointwise summability needed from it.\n\nHmm, actually — is the eventual M-test (of_norm_le_summable_eventually) applicable with the if-term? The bound holds eventually ✓; the head terms unconstrained ✓. Conclusion: HasSumUniformlyOn sub (fun w => ∑' j, sub j w) ball ✓ = digammaSeriesPartSub ✓ (defeq).\n\nThen differentiability of partial sums of sub on the ball: term j: if j = n−1 then 0 else full-term: full-term differentiable at w ∈ ball: 1/(j+1) const ✓; 1/(w+j+1): w+j+1 ≠ 0 (pole avoidance, j ≠ n−1 ✓; for j = n−1 the if gives 0 ✓ const).\n\nThe single-split: for w ∈ ball(−n,1/2), w ≠ −n: \ndigammaSeriesPart w = digammaSeriesPartSub n w + (1/(n:ℂ) − 1/(w+n)):\n- pointwise: full j = sub j + single j where single j := if j = n−1 then (1/(j+1) − 1/(w+j+1)) else 0 ✓ by_cases simp.\n- Summable full at w: w ∈ integerComplement: w = (k:ℤ) with ‖w+n‖ < 1/2 ⟹ |k + n| < 1/2... k integer, n nat: |k+n| < 1/2 ⟹ k = −n ⟹ w = −n excluded ✓. So w ∈ integerComplement ⟹ summable_digamma_series gives Summable (fun j => 1/(j+1) − 1/(w+j+1)) — its exact summand form must match — check: `summable_digamma_series (hz : z ∈ integerComplement) : Summable fun n => ...` (line 298) — presumably exactly the digamma_series summand ✓.\n- Summable sub at w: of_norm_bounded (full.norm) (‖sub‖ ≤ ‖full‖ pointwise: if-zero ≤ ✓).\n- Summable single: finite support ✓.\n- tsum: full = sub + single via Summable.tsum_add (sub) (single) reversed: ∑' (sub + single) = ... with pointwise eq full = sub + single: tsum_congr.\n- single tsum = 1/n − 1/(w+n): tsum_eq_single (n−1): ∀ j ≠ n−1: single j = 0 ✓ if_neg; value at n−1: if_pos: 1/((n−1:ℂ)+1) − 1/(w+(n−1)+1) = 1/n − 1/(w+n): casts: (n−1 : ℕ) as ℂ + 1: (↑(n−1) : ℂ) + 1 = ↑n: Nat.cast_sub (hn : 1 ≤ n)... `(↑(n − 1) : ℂ) + 1 = ↑n`: Nat.cast_sub hn gives ↑(n−1) = ↑n − ↑1 = ↑n − 1: so LHS = ↑n − 1 + 1 = ↑n ✓ via push_cast/ring with the cast_sub rewrite: `rw [Nat.cast_sub hn]; push_cast; ring`? Nat.cast_sub (hn : 1 ≤ n) : ↑(n − 1) = ↑n − ↑1: then ring ✓. Handle carefully.\n\nThen H_n w := −γ − 1/w + digammaSeriesPartSub n w + 1/(n:ℂ): analytic at −n: pieces: const ✓; 1/w at −n ≠ 0 ✓ (n ≥ 1); digammaSeriesPartSub analytic on the ball (M-test) ⟹ at −n (center ✓); 1/n const ✓.\ndigamma w = −1/(w+n) + H_n w for w ∈ ball, w ≠ −n:\ndigamma w = −γ − 1/w + full w (digamma_series at w ∈ integerComplement ✓)\n        = −γ − 1/w + sub w + (1/n − 1/(w+n))  [the split]\n        = −1/(w+n) + H_n w ✓ ring.\n\nThen the −2n witness:\nW := fun s => Wtriv s − seriesFun s + 1/s + 1/(s−1) − c + H_n(s/2)/2\nwhere Wtriv from logDeriv_zeta_sub_mult_div_eventually at ρ₀ = −2n: (hζ : riemannZeta (−2n) = 0) — need! ζ(−2n) = 0 for n ≥ 1: from zeroMult_neg_two_mul: zeroMult(−2n) = (analyticOrderAt ζ (−2n)).toNat = 1: analyticOrderAt = some 1 ≠ 0 ⟹ ζ(−2n) = 0: analyticOrderAt_eq_zero ↔ f x ≠ 0 (hh.analyticOrderAt_eq_zero.mpr used earlier in LiSides: `(....analyticOrderAt_eq_zero).mpr (by rw [zetaA_one]; norm_num)` ✓ so analyticOrderAt_eq_zero : order = 0 ↔ f x ≠ 0 — the iff for analytic f: `AnalyticAt.analyticOrderAt_eq_zero : analyticOrderAt f x = 0 ↔ f x ≠ 0`? So contrapositive: order.toNat = 1 ≠ 0 ⟹ order ≠ 0 ⟹ ¬ f x ≠ 0 ⟹ f x = 0 ✓:\n```lean\n  have hζtriv : riemannZeta (-2 * (n : ℂ)) = 0 := by\n    by_contra h\n    have hord := zeroMult_neg_two_mul (n) hn  -- check signature: zeroMult_neg_two_mul {n : ℕ} (hn : 1 ≤ n) : zeroMult (-2 * n) = 1? — check LiTrivialZeros exact statement\n    -- zeroMult = (analyticOrderAt ζ _).toNat; analyticOrderAt ≠ 0 (toNat = 1)\n    have h0 : analyticOrderAt riemannZeta (-2 * (n : ℂ)) = 0 :=\n      (analyticAt_riemannZeta (by ... : -2*n ≠ 1)).analyticOrderAt_eq_zero.mpr h\n    rw [h0] at hord  -- zeroMult = (0).toNat = 0 ≠ 1\n    simp [zeroMult] at hord\n```\nCheck zeroMult_neg_two_mul's exact form/signature from LiTrivialZeros — need to grep. Also its s-form: `zeroMult (-2 * ↑n) = 1`?\n\n- Wtriv analytic at −2n ✓ from the lemma + punctured: logDeriv ζ s − zeroMult(−2n)/(s−(−2n)) = Wtriv s: with zeroMult = 1 and s − (−2n) = s + 2n.\n- Fexpr s = W s punctured: Fexpr s = logDerivζ s − series + 1/s + 1/(s−1) − c + ψ(s/2)/2; for s near −2n, s ≠ −2n: logDerivζ s = Wtriv s + 1/(s+2n) (from the witness + zeroMult = 1) and ψ(s/2)/2 = −1/(s+2n) + H_n(s/2)/2 (from the digamma split at w = s/2 — need s/2 ∈ ball(−n, 1/2) ⟺ s ∈ ball(−2n, 1) ✓ take the s-ball radius min(1, ...)/2 etc; and s/2 ≠ −n ⟺ s ≠ −2n ✓):\n  Fexpr s = [Wtriv s + 1/(s+2n)] − series + 1/s + 1/(s−1) − c + [−1/(s+2n) + H_n(s/2)/2] = Wtriv s − series + 1/s + 1/(s−1) − c + H_n(s/2)/2 ✓ ring.\n- W analytic at −2n: Wtriv ✓; seriesFun: ¬IsNontrivialZero (−2n): re = −2n < 0: `.2.1 : 0 < re` contra ✓; 1/s: −2n ≠ 0 (n ≥ 1) ✓; 1/(s−1): −2n − 1 ≠ 0 ✓; H_n(s/2)/2: H_n analytic at −n ✓ comp with s/2 (value at −2n is −n ✓) then /2 ✓.\n\n§7 nontrivial witness:\n```lean\nlemma Fexpr_eventually_zero_of_nontrivial {ρ₀ : ℂ} (hρ : IsNontrivialZero ρ₀) :\n    ∃ W, AnalyticAt ℂ W ρ₀ ∧ ∀ᶠ s in 𝓝[≠] ρ₀, Fexpr s = W s := by\n  obtain ⟨W0, hW0, hW0eq⟩ := logDeriv_zeta_sub_mult_div_eventually hρ.1 (by\n    intro h; rw [h] at hρ... : ρ₀ ≠ 1: re ρ₀ < 1: if ρ₀ = 1: re = 1 contra: `fun h => absurd (h ▸ hρ.2.2) (by simp)`? h : ρ₀ = 1: hρ.2.2 : ρ₀.re < 1: h ▸ : (1:ℂ).re < 1: simp ⟹ False: `exact fun h => by rw [h, Complex.one_re] at hρ; exact lt_irrefl 1 hρ.2.2` — careful: rw [h] at hρ rewrites everywhere incl hρ.2.2: then hρ.2.2 : (1:ℂ).re < 1?? hρ is a term of And-type: rw [h] at hρ rewrites ρ₀ → 1 in hρ's type ✓ then have hlt := hρ.2.2; rw [Complex.one_re] at hlt; exact lt_irrefl _ hlt ✓.)\n  -- series part\n  obtain ⟨ρ₀', rfl⟩?? — seriesFun_sub_polar_analyticAt takes ρ₀ : {ρ // IsNontrivialZero ρ} (subtype). Here ρ₀ : ℂ with hρ : IsNontrivialZero ρ₀: use ⟨ρ₀, hρ⟩ : the subtype. seriesFun_sub_polar_analyticAt ⟨ρ₀, hρ⟩ : AnalyticAt ℂ (fun s => seriesFun s − (zeroMult (⟨ρ₀,hρ⟩:ℂ)... hmm (zeroMult (↑⟨ρ₀,hρ⟩) : ℂ)/(s − ↑⟨ρ₀,hρ⟩)) ↑⟨ρ₀,hρ⟩ — coercions reduce: ↑⟨ρ₀, hρ⟩ = ρ₀ ✓ rfl. So: AnalyticAt ℂ (fun s => seriesFun s − (zeroMult ρ₀:ℂ)/(s − ρ₀)) ρ₀ ✓ after defeq coercion — may need `show` to manage the coe display.\n  W := fun s => W0 s − (seriesFun s − m/(s−ρ₀)) + 1/s + 1/(s−1) − c + ψ(s/2)/2 — wait the Fexpr assembly: Fexpr s = logDerivζ − series + elems; logDerivζ = W0 + m/(s−ρ₀) punctured; series = (series − m/(s−ρ₀)) + m/(s−ρ₀) — trivially: Fexpr s = W0 s + m/(s−ρ₀) − seriesFun s + 1/s + 1/(s−1) − c + ψ/2 = W0 s − (seriesFun s − m/(s−ρ₀)) + 1/s + 1/(s−1) − c + ψ/2 ✓ ring (punctured).\n  W := fun s => W0 s - (seriesFun s - (zeroMult ρ₀:ℂ)/(s - ρ₀)) + 1/s + 1/(s-1) - c + digamma(s/2)/2\n  analytic: W0 ✓; series-minus-polar ✓ (5e-iii); 1/s: ρ₀ ≠ 0 (re > 0 ✓); 1/(s−1): ρ₀ ≠ 1 ✓; digamma(s/2)/2: ∀ m, ρ₀/2 ≠ −↑m: re(ρ₀/2) = re ρ₀/2 > 0 ≥ ... −↑m's re = −m ≤ 0 contra ✓.\n  punctured: filter_upwards [hW0eq] with s hs; show-unfold Fexpr; rw [hs]; ring ✓ (m/(s−ρ₀) atoms cancel).\n```\n\n§8 generic + good balls:\n```lean\nlemma Fexpr_analyticAt_of_not_bad {s : ℂ} (hs : ¬ badPoint s) : AnalyticAt ℂ Fexpr s := by\n  -- ζ s ≠ 0\n  have hζ : riemannZeta s ≠ 0 := by\n    intro hz\n    apply hs\n    rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩\n    · exact Or.inl h\n    · exact Or.inr (Or.inl h)\n    · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))\n  have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n  have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))\n  have hlog : AnalyticAt ℂ (logDeriv riemannZeta) s :=\n    ((analyticAt_riemannZeta hs1).deriv).div (analyticAt_riemannZeta hs1) hζ\n  have hser : AnalyticAt ℂ seriesFun s := seriesFun_analyticAt (fun h => hs (Or.inl h))\n  have hinv : AnalyticAt ℂ (fun s : ℂ => 1 / s) s := analyticAt_const.div analyticAt_id hs0\n  have hinv1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) s :=\n    analyticAt_const.div (analyticAt_id.sub analyticAt_const) (sub_ne_zero.mpr hs1)  -- hmm: the g function: fun s => s − 1: analyticAt_id.sub analyticAt_const : AnalyticAt (id − const)... the lambda form again: (analyticAt_id.sub analyticAt_const) : AnalyticAt ℂ (id − fun _ => 1) s: Pi-sub vs fun s => s − 1: use apply AnalyticAt.div analyticAt_const _ ...: `apply AnalyticAt.div analyticAt_const _ (sub_ne_zero.mpr hs1)` leaves goal AnalyticAt ℂ (fun x => x − 1)?? the div unification: goal AnalyticAt (fun s => 1/(s−1)) s: apply AnalyticAt.div: pattern fun x => f x / g x: f := 1, g := fun s => s − 1 ✓ then hg0 : g s ≠ 0: (fun s => s−1) s ≠ 0 — beta: s − 1 ≠ 0 ✓ sub_ne_zero.mpr hs1 : s − 1 ≠ 0 — exact defeq ✓ might need show. Then remaining goal AnalyticAt ℂ (fun s => s − 1) s: analyticAt_id.sub analyticAt_const : AnalyticAt ℂ (id − fun _ => 1)?? — defeq id s − 1 = s − 1: exact should accept? Pi-sub again — risk. Use fun_prop? AnalyticAt fun_prop support: try `by fun_prop`. If fun_prop fails, the show-bridge. I'll write explicit term with apply and hope, else adjust.\n  have hdig : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by\n    apply analyticAt_digamma_div_two\n    intro m h\n    -- s/2 = −↑m ⟹ s = −2m: bad\n    apply hs\n    have h2 : s = -2 * (m : ℂ) := by linear_combination 2 * h  -- s/2 = −m ⟹ s = −2m: h : s/2 = −↑m: 2*h: s = −2↑m ✓ linear_combination 2*h? goal s = -2*↑m: linear_combination (2 * h): LHS−RHS − 2*(hLHS−hRHS) = 0: s − (−2↑m) − 2*(s/2 − (−↑m)) = s + 2↑m − s + ... let me verify: 2*(s/2 + ↑m) = s + 2↑m: goal s + 2↑m = 0?? goal is s = −2↑m i.e. s + 2↑m = 0 ✓ linear_combination 2*h: proves (s) − (−2↑m) = 2*(s/2 − (−↑m)) ✓: s + 2↑m = 2(s/2) + 2↑m = s + 2↑m ✓.\n    rcases Nat.eq_zero_or_pos m with hm0 | hm\n    · subst hm0; simp at h2; exact Or.inr (Or.inl h2)  -- s = 0: h2 : s = -2*↑0 = 0: simp at h2 : s = 0\n    · exact Or.inr (Or.inr (Or.inr ⟨m, hm, h2⟩))\n  have hconst : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) s := analyticAt_const\n  -- assemble: Fexpr = (((logDerivζ − series) + 1/s) + 1/(s−1) − c) + ψ/2 — the def order:\n  -- Fexpr s := logDeriv ζ s - seriesFun s + 1/s + 1/(s-1) - c + digamma(s/2)/2\n  show AnalyticAt ℂ (fun s => logDeriv riemannZeta s - seriesFun s + 1/s + 1/(s-1) - c + digamma(s/2)/2) s\n  exact ((((hlog.sub hser).add hinv).add hinv1).sub hconst).add hdig\n```\nThe show: Fexpr s unfolds ✓ defeq. The final assembly: the association order in Fexpr: ((((logDeriv − series) + 1/s) + 1/(s−1)) − c) + ψ/2 — my term: ((((hlog.sub hser).add hinv).add hinv1).sub hconst).add hdig : AnalyticAt ℂ (((((logDeriv ζ − seriesFun) + 1/s-lambda) + 1/(s−1)-lambda) − const) + dig-lambda) s — with Pi-ops vs the show-lambda: defeq ✓ hopefully exact accepts. If not: convert using 1 + funext simp [Pi...]. I'll handle if error.\n\n§9 the good-ball lemma:\n```lean\nlemma exists_ball_good_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :\n    ∃ δ : ℝ, 0 < δ ∧ ∀ y ∈ Metric.ball s δ, ¬ badPoint y := by\n  -- ζ ≠ 0 ball\n  have hζ : riemannZeta s ≠ 0 := ... (as in §8)\n  have hs1 : s ≠ 1 := ...\n  obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n    ((analyticAt_riemannZeta hs1).continuousAt.eventually_ne hζ)\n  -- avoid {0, 1}\n  have hs0 : s ≠ 0 := ...\n  set δ₀ := min (‖s‖ / 2) (‖s - 1‖ / 2)?? hmm — need δ₀ > 0 with ball(s, δ₀) avoiding {0,1}: δ₀ := min ‖s‖ ‖s−1‖ /2... ‖s‖ > 0 (s ≠ 0), ‖s−1‖ > 0 (s ≠ 1): δ₀ := min ‖s‖ ‖s−1‖ > 0... wait but if ‖s‖ huge it's fine. Take δ := min ε₁ (min ‖s‖ ‖s−1‖)/2... just δ := min ε₁ ((min ‖s‖ ‖s−1‖)/2) — positivity: min ‖s‖ ‖s−1‖ > 0 (both pos via norm_pos_iff) /2 ✓.\n  -- every y in ball: ζ y ≠ 0 ⟹ y not nontrivial (∈ zeros contra), not −2n (ζ(−2n) = 0), and ‖y‖ ≤ ‖s‖/... y ≠ 0: ‖y − s‖ < δ ≤ ‖s‖/2 ⟹ ‖y‖ ≥ ‖s‖/2 > 0 ✓; y ≠ 1: ‖y−s‖ < ‖s−1‖/2 ⟹ ‖y−1‖ ≥ ‖s−1‖/2 > 0 ✓.\n  ...\n  -- y badPoint cases: nontrivial: ζ y = 0 contra hball₁; y = 0: norm contra; y = 1: contra; y = −2n: ζ(−2n) = 0 contra hball₁ — needs ζ(−2n) = 0!\n```\nζ(−2n) = 0: as discussed from zeroMult_neg_two_mul — let me make a standalone lemma `riemannZeta_neg_two_mul (hn : 1 ≤ n) : riemannZeta (−2 * (n:ℂ)) = 0` (also used in §6's Wtriv).\n\nForm: what's the exact statement of zeroMult_neg_two_mul? Check LiTrivialZeros.","signature":""},{"type":"text","text":"§0–§4 compile clean. Before writing §5–§9, let me check `zeroMult_neg_two_mul`'s exact form and the `summable_digamma_series` summand shape."},{"type":"tool_use","id":"Bash_132","name":"Bash","input":{"command":"grep -n \"theorem zeroMult_neg_two_mul\\|lemma zeroMult_neg_two_mul\" -A 4 D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiTrivialZeros.lean | head -8; cd D:/Python/Quantum/zeta-23-lean && sed -n '296,320p' Zeta23/GammaFacts/Series.lean","description":"zeroMult_neg_two_mul signature and summable_digamma_series"},"extra_content":null}]