LiMoments.lean

Declarations

Source

/-
LiMoments.lean — tier ii′-3b: the contour moments (M) via the 5e
partial-fraction identity (D-070 route revision; D-066 §3's rectangle
plan superseded).

Target (D-066 §2 piece (M)): for all k ≥ 1,
  sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)!,
where gFun = logDeriv xiL and xiL = (s(s−1)/2)·completedRiemannZeta is
the entire ξ. The whole argument is the identity

  (G)  gFun s = B + seriesFun s

at every good point (ζ s ≠ 0, s ≠ 0, s ≠ 1, s ≠ −2n for n ≥ 1) — pure
logDeriv algebra from 5e's `partialFraction_identity` — plus termwise
series calculus: k ≥ 2 by iterated derivation of the absolutely
summable zero series at 0 (the LiDigamma §7–8 `iteratedDerivWithin_tsum`
pattern), k = 1 by the conj/reflect reindex V = Σ mult·(1/ρ̄ − 1/(1−ρ))
= −V = 0 (zeroMult_conj + zeroMult_one_sub).

§1: xiL (entire closed form via completedRiemannZeta₀) + basic facts +
    the two zero-subtype equivs.
§2: the good-set lemmas + (G) (`gFun_eq_momentB`).
§3: evaluation at 0 and 1 (punctured-continuity bridges) + the FE sign
    (`gFun_one_eq_neg`).
§4: summability budget + the k = 1 rearrangement (`two_mul_sigmaP_one`).
§5: the per-term derivative machine + termwise iterated derivation at 0
    (`iteratedDeriv_seriesFun_zero`).
§6: the capstone `sigmaP_eq_neg_iteratedDeriv_gFun_div`.

Perimeter: `ZeroCountProp` only (inherited from 5e's gap circles).
Archive references: D-066 §2, D-068 §5, D-070.
-/
import Mathlib
import NguyenRH1.LiTightR
import NguyenRH1.LiSwaps
import NguyenRH1.LiResidue
import NguyenRH1.LiDigamma
import NguyenRH1.LiReflect

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The entire ξ and the zero-subtype equivs -/

/-- The entire ξ in closed form: (s(s−1)/2)·Λ₀(s) − (s−1)/2 + s/2 with
Λ₀ = `completedRiemannZeta₀` entire (Mathlib `differentiable_completedZeta₀`).
Equals (s(s−1)/2)·Λ(s) off {0, 1} (`xiL_eq_mul`); xiL(0) = xiL(1) = 1/2. -/
def xiL (s : ℂ) : ℂ :=
  (s * (s - 1) / 2) * completedRiemannZeta₀ s - (s - 1) / 2 + s / 2

lemma differentiable_xiL : Differentiable ℂ xiL := by
  have h1 : Differentiable ℂ (fun s : ℂ => s * (s - 1) / 2) :=
    (differentiable_id.mul (differentiable_id.sub_const 1)).div_const 2
  have h2 : Differentiable ℂ (fun s : ℂ => (s - 1) / 2) :=
    (differentiable_id.sub_const 1).div_const 2
  have h3 : Differentiable ℂ (fun s : ℂ => s / 2) := differentiable_id.div_const 2
  exact ((h1.mul differentiable_completedZeta₀).sub h2).add h3

lemma analyticAt_xiL (s : ℂ) : AnalyticAt ℂ xiL s :=
  (differentiable_xiL.differentiableOn.analyticOnNhd isOpen_univ) s (Set.mem_univ s)

/-- The defining equation off {0, 1}: xiL s = (s(s−1)/2)·Λ(s). -/
lemma xiL_eq_mul {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) :
    xiL s = (s * (s - 1) / 2) * completedRiemannZeta s := by
  rw [xiL, completedRiemannZeta_eq]
  have h1s : (1 : ℂ) - s ≠ 0 := sub_ne_zero.mpr (Ne.symm h1)
  field_simp
  ring

lemma xiL_zero : xiL 0 = 1 / 2 := by norm_num [xiL]

lemma xiL_one : xiL 1 = 1 / 2 := by norm_num [xiL]

/-- The functional equation xiL(1−s) = xiL(s), all s. -/
lemma xiL_one_sub (s : ℂ) : xiL (1 - s) = xiL s := by
  by_cases h0 : s = 0
  · subst h0
    show xiL (1 - 0) = xiL 0
    rw [sub_zero, xiL_one, xiL_zero]
  by_cases h1 : s = 1
  · subst h1
    show xiL (1 - 1) = xiL 1
    rw [sub_self, xiL_zero, xiL_one]
  · have h10 : (1 : ℂ) - s ≠ 0 := sub_ne_zero.mpr (Ne.symm h1)
    have h11 : (1 : ℂ) - s ≠ 1 := by
      intro h
      apply h0
      have h2 := congrArg (fun t : ℂ => (1 : ℂ) - t) h
      simp at h2
      exact h2
    rw [xiL_eq_mul h10 h11, xiL_eq_mul h0 h1, completedRiemannZeta_one_sub]
    congr 1
    ring

/-- xiL vanishes nowhere off {0, 1} where ζ ≠ 0. -/
lemma xiL_ne_zero {s : ℂ} (h0 : s ≠ 0) (h1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) :
    xiL s ≠ 0 := by
  rw [xiL_eq_mul h0 h1]
  apply mul_ne_zero
  · exact div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero
  · intro hΛ
    rw [RvM.completedRiemannZeta_eq_zero_iff] at hΛ
    exact hζ hΛ.1

lemma not_isNontrivialZero_zero : ¬ IsNontrivialZero (0 : ℂ) := by
  intro h
  have h2 := h.2.1
  rw [Complex.zero_re] at h2
  exact lt_irrefl 0 h2

lemma not_isNontrivialZero_one : ¬ IsNontrivialZero (1 : ℂ) := by
  intro h
  have h2 := h.2.2
  rw [Complex.one_re] at h2
  exact lt_irrefl 1 h2

/-- Reflection of a nontrivial zero: 1 − ρ is a nontrivial zero
(conj then Zeta23 reflect). -/
lemma isNontrivialZero_one_sub {ρ : ℂ} (hρ : IsNontrivialZero ρ) :
    IsNontrivialZero (1 - ρ) := by
  have h := zeta_reflect_zero ((starRingEnd ℂ) ρ) (isNontrivialZero_conj hρ)
  have e : Zeta23.reflect ((starRingEnd ℂ) ρ) = 1 - ρ := by
    simp [Zeta23.reflect]
  rwa [e] at h

/-- The conjugation involution on the nontrivial-zero subtype. -/
def conjZeroEquiv : {ρ : ℂ // IsNontrivialZero ρ} ≃ {ρ : ℂ // IsNontrivialZero ρ} where
  toFun ρ := ⟨(starRingEnd ℂ) ρ, isNontrivialZero_conj ρ.2⟩
  invFun ρ := ⟨(starRingEnd ℂ) ρ, isNontrivialZero_conj ρ.2⟩
  left_inv ρ := Subtype.ext (by simp)
  right_inv ρ := Subtype.ext (by simp)

/-- The reflection involution ρ ↦ 1 − ρ on the nontrivial-zero subtype. -/
def oneSubZeroEquiv : {ρ : ℂ // IsNontrivialZero ρ} ≃ {ρ : ℂ // IsNontrivialZero ρ} where
  toFun ρ := ⟨1 - ρ, isNontrivialZero_one_sub ρ.2⟩
  invFun ρ := ⟨1 - ρ, isNontrivialZero_one_sub ρ.2⟩
  left_inv ρ := Subtype.ext (by simp)
  right_inv ρ := Subtype.ext (by simp)

/-! ## 2. The good set and the identity (G) -/

/-- The chosen constant from the 5e partial-fraction identity. -/
noncomputable def momentB (hZC : ZeroCountProp) : ℂ :=
  Classical.choose (partialFraction_identity hZC)

lemma momentB_spec (hZC : ZeroCountProp) (s : ℂ) (hζ : riemannZeta s ≠ 0)
    (h0 : s ≠ 0) (h1 : s ≠ 1) (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :
    logDeriv riemannZeta s = momentB hZC + seriesFun s - 1 / s - 1 / (s - 1) +
      (Real.log Real.pi : ℂ) / 2 - Complex.digamma (s / 2) / 2 :=
  Classical.choose_spec (partialFraction_identity hZC) s hζ h0 h1 hn

/-- The log-derivative of ξ. -/
noncomputable def gFun (s : ℂ) : ℂ := logDeriv xiL s

/-- The good-set half-shift condition for the ΓR identity: s/2 ∉ −ℕ. -/
lemma good_half_ne_neg_nat {s : ℂ} (h0 : s ≠ 0)
    (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :
    ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := by
  intro m hm
  rcases Nat.eq_zero_or_pos m with hm0 | hm0
  · subst hm0
    simp only [Nat.cast_zero, neg_zero] at hm
    apply h0
    have h2 : s = 2 * (s / 2) := by ring
    rw [h2, hm, mul_zero]
  · apply hn m hm0
    linear_combination 2 * hm

/-- **The identity (G)**: off the excluded set, gFun = B + seriesFun.
Pure logDeriv algebra: logDeriv of xiL = (s(s−1)/2)·Λ splits as
1/s + 1/(s−1) + [−(log π)/2 + ψ(s/2)/2] + ζ′/ζ, and 5e's
partial-fraction identity collapses everything to B + seriesFun. -/
theorem gFun_eq_momentB (hZC : ZeroCountProp) {s : ℂ} (hζ : riemannZeta s ≠ 0)
    (h0 : s ≠ 0) (h1 : s ≠ 1) (hn : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) :
    gFun s = momentB hZC + seriesFun s := by
  have hhalf : ∀ m : ℕ, s / 2 ≠ -(m : ℂ) := good_half_ne_neg_nat h0 hn
  have hΓ0 : Complex.Gammaℝ s ≠ 0 := by
    rw [Ne, Complex.Gammaℝ_eq_zero_iff]
    rintro ⟨m, hm⟩
    rcases Nat.eq_zero_or_pos m with hm0 | hm0
    · subst hm0
      simp only [Nat.cast_zero, mul_zero, neg_zero] at hm
      exact h0 hm
    · exact hn m hm0 (by linear_combination hm)
  have hΓdiff : DifferentiableAt ℂ Complex.Gammaℝ s :=
    differentiableAt_Gammaℝ_of_not_neg_nat hhalf
  -- xiL agrees with the product form on a neighbourhood of s
  have hopen : IsOpen ({0}ᶜ ∩ {1}ᶜ : Set ℂ) :=
    isOpen_compl_singleton.inter isOpen_compl_singleton
  have hexp : xiL =ᶠ[𝓝 s]
      (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) := by
    filter_upwards [hopen.mem_nhds ⟨h0, h1⟩] with t ht
    exact xiL_eq_mul ht.1 ht.2
  -- Λ agrees with ΓR·ζ on a neighbourhood of s
  have hΛeq : completedRiemannZeta =ᶠ[𝓝 s]
      (fun t => Complex.Gammaℝ t * riemannZeta t) := by
    filter_upwards [hΓdiff.continuousAt.eventually_ne hΓ0, eventually_ne_nhds h0]
      with t htΓ ht0
    rw [riemannZeta_def_of_ne_zero ht0]
    field_simp [htΓ]
  have hlog : logDeriv xiL s =
      logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) s := by
    rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]
  rw [gFun, hlog]
  have hP : DifferentiableAt ℂ (fun t : ℂ => t * (t - 1) / 2) s :=
    (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2
  have hΛ : DifferentiableAt ℂ completedRiemannZeta s := differentiableAt_completedZeta h0 h1
  have hP0 : s * (s - 1) / 2 ≠ 0 :=
    div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero
  have hΛ0 : completedRiemannZeta s ≠ 0 := by
    rw [Ne, RvM.completedRiemannZeta_eq_zero_iff]
    rintro h
    exact hζ h.1
  rw [logDeriv_mul (f := fun t : ℂ => t * (t - 1) / 2) (g := completedRiemannZeta) _
    hP0 hΛ0 hP hΛ]
  have hPlog : logDeriv (fun t : ℂ => t * (t - 1) / 2) s = 1 / s + 1 / (s - 1) := by
    rw [logDeriv_apply]
    have hderiv : deriv (fun t : ℂ => t * (t - 1) / 2) s = s - 1 / 2 := by
      have h2' : HasDerivAt (fun t : ℂ => t * (t - 1) / 2) ((1 * (s - 1) + s * 1) / 2) s :=
        ((hasDerivAt_id' s).mul ((hasDerivAt_id' s).sub_const 1)).div_const 2
      rw [h2'.deriv]
      ring
    rw [hderiv]
    have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr h1
    field_simp [h0, hs1]
    ring
  rw [hPlog]
  have hlogΛ : logDeriv completedRiemannZeta s =
      logDeriv Complex.Gammaℝ s + logDeriv riemannZeta s := by
    have heq : logDeriv completedRiemannZeta s =
        logDeriv (fun t => Complex.Gammaℝ t * riemannZeta t) s := by
      rw [logDeriv_apply, logDeriv_apply, hΛeq.deriv_eq, hΛeq.eq_of_nhds]
    rw [heq, logDeriv_mul (f := Complex.Gammaℝ) (g := riemannZeta) _ hΓ0 hζ
      (differentiableAt_Gammaℝ_of_not_neg_nat hhalf) (differentiableAt_riemannZeta h1)]
  rw [hlogΛ, logDeriv_Gammaℝ_eq_of_not_neg_nat hhalf, momentB_spec hZC s hζ h0 h1 hn]
  ring

/-! ## 3. Evaluation at 0 and 1 -/

/-- Functions continuous at s₀ that agree on the punctured neighbourhood
agree at s₀. -/
lemma eq_of_eventuallyEq_nhd_ne {F G : ℂ → ℂ} {s₀ : ℂ} (hF : ContinuousAt F s₀)
    (hG : ContinuousAt G s₀) (h : F =ᶠ[𝓝[≠] s₀] G) : F s₀ = G s₀ :=
  tendsto_nhds_unique (hF.tendsto.mono_left nhdsWithin_le_nhds)
    ((hG.tendsto.mono_left nhdsWithin_le_nhds).congr' h.symm)

/-- gFun is continuous wherever xiL ≠ 0. -/
lemma gFun_continuousAt (s : ℂ) (hs : xiL s ≠ 0) : ContinuousAt gFun s :=
  (((analyticAt_xiL s).deriv).div (analyticAt_xiL s) hs).continuousAt

/-- The series value at 0 is 0 (termwise: 1/(0−ρ) + 1/ρ = 0). -/
lemma seriesFun_zero : seriesFun 0 = 0 := by
  rw [seriesFun]
  have h : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTerm 0 ρ = 0 := by
    intro ρ
    have hρ0 : (ρ : ℂ) ≠ 0 := by
      intro h0
      have h2 := ρ.2.2.1
      rw [h0, Complex.zero_re] at h2
      exact lt_irrefl 0 h2
    rw [seriesTerm, zero_sub, div_neg, neg_add_cancel, mul_zero]
  rw [tsum_congr h]
  exact tsum_zero

/-- The series value at 1: Σ mult/(ρ(1−ρ)) (termwise partial fractions). -/
lemma seriesFun_one : seriesFun 1 =
    ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ)))) := by
  rw [seriesFun]
  apply tsum_congr
  intro ρ
  have hρ0 : (ρ : ℂ) ≠ 0 := by
    intro h0
    have h2 := ρ.2.2.1
    rw [h0, Complex.zero_re] at h2
    exact lt_irrefl 0 h2
  have h1ρ : (1 : ℂ) - (ρ : ℂ) ≠ 0 := by
    intro h
    have h3 : (1 : ℂ) = (ρ : ℂ) := sub_eq_zero.mp h
    have h4 := ρ.2.2.2
    rw [← h3, Complex.one_re] at h4
    exact lt_irrefl 1 h4
  rw [seriesTerm, one_div_sub_add_one_div hρ0 h1ρ]

/-- The good conditions hold eventually in the punctured neighbourhood of 0. -/
lemma good_eventually_zero :
    ∀ᶠ s in 𝓝[≠] (0 : ℂ), riemannZeta s ≠ 0 ∧ s ≠ 1 ∧
      (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by
  have hζ : ∀ᶠ s in 𝓝 (0 : ℂ), riemannZeta s ≠ 0 :=
    (analyticAt_riemannZeta (by norm_num : (0 : ℂ) ≠ 1)).continuousAt.eventually_ne
      (by rw [riemannZeta_zero]; norm_num)
  have h1 : ∀ᶠ s in 𝓝 (0 : ℂ), s ≠ 1 := eventually_ne_nhds (by norm_num : (0 : ℂ) ≠ 1)
  have hnorm : ∀ᶠ s in 𝓝 (0 : ℂ), ‖s‖ < 2 := by
    have h : Metric.ball (0 : ℂ) 2 ∈ 𝓝 (0 : ℂ) := Metric.ball_mem_nhds _ (by norm_num)
    filter_upwards [h] with s hs
    rw [Metric.mem_ball, dist_zero_right] at hs
    exact hs
  filter_upwards [hζ.filter_mono nhdsWithin_le_nhds, h1.filter_mono nhdsWithin_le_nhds,
    hnorm.filter_mono nhdsWithin_le_nhds] with s hζs h1s hsn
  refine ⟨hζs, h1s, fun n hn1 habs => ?_⟩
  rw [habs] at hsn
  have h2 : ‖(-2 : ℂ)‖ = 2 := by
    rw [show (-2 : ℂ) = ((-2 : ℝ) : ℂ) by push_cast; ring, Complex.norm_real,
      Real.norm_eq_abs, abs_neg]
    norm_num
  have hbig : (2 : ℝ) ≤ ‖(-2 : ℂ) * (n : ℂ)‖ := by
    rw [norm_mul, h2, RCLike.norm_natCast]
    have hn1' : (1 : ℝ) ≤ (n : ℝ) := Nat.one_le_cast.mpr hn1
    linarith
  linarith

/-- The good conditions hold eventually in the punctured neighbourhood of 1. -/
lemma good_eventually_one :
    ∀ᶠ s in 𝓝[≠] (1 : ℂ), riemannZeta s ≠ 0 ∧ s ≠ 0 ∧
      (∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ)) := by
  have hA : ∀ᶠ s in 𝓝 (1 : ℂ), zetaA s ≠ 0 := zetaA_ne_zero_near_one
  have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), s ≠ 0 := eventually_ne_nhds (by norm_num : (1 : ℂ) ≠ 0)
  have hnorm : ∀ᶠ s in 𝓝 (1 : ℂ), ‖s - 1‖ < 1 := by
    have h : Metric.ball (1 : ℂ) 1 ∈ 𝓝 (1 : ℂ) := Metric.ball_mem_nhds _ (by norm_num)
    filter_upwards [h] with s hs
    rw [Metric.mem_ball, dist_eq_norm] at hs
    exact hs
  filter_upwards [hA.filter_mono nhdsWithin_le_nhds, self_mem_nhdsWithin,
    h0.filter_mono nhdsWithin_le_nhds, hnorm.filter_mono nhdsWithin_le_nhds]
    with s hAs hs1 h0s hsn
  refine ⟨?_, h0s, fun n hn1 habs => ?_⟩
  · intro hζ
    rw [zetaA_apply hs1, hζ, mul_zero] at hAs
    exact hAs rfl
  · rw [habs] at hsn
    have hnorm2 : ‖(-2 : ℂ) * (n : ℂ) - 1‖ = 2 * (n : ℝ) + 1 := by
      have e : (-2 : ℂ) * (n : ℂ) - 1 = ((- (2 * (n : ℝ) + 1) : ℝ) : ℂ) := by
        push_cast
        ring
      rw [e, Complex.norm_real, Real.norm_eq_abs, abs_neg, abs_of_nonneg (by
        have hn0 : (0 : ℝ) ≤ (n : ℝ) := Nat.cast_nonneg _
        linarith)]
    rw [hnorm2] at hsn
    have hn1' : (1 : ℝ) ≤ (n : ℝ) := Nat.one_le_cast.mpr hn1
    linarith

/-- gFun(0) = B (punctured continuity; seriesFun(0) = 0). -/
lemma gFun_zero (hZC : ZeroCountProp) : gFun 0 = momentB hZC := by
  have hgood : ∀ᶠ s in 𝓝[≠] (0 : ℂ), gFun s = momentB hZC + seriesFun s := by
    filter_upwards [good_eventually_zero, self_mem_nhdsWithin] with s ⟨hζ, h1, hn⟩ h0
    exact gFun_eq_momentB hZC hζ h0 h1 hn
  have hF : ContinuousAt gFun 0 := gFun_continuousAt 0 (by rw [xiL_zero]; norm_num)
  have hG0 : ContinuousAt ((fun _ => momentB hZC) + seriesFun) 0 :=
    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_zero).continuousAt
  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 0 := hG0
  have h := eq_of_eventuallyEq_nhd_ne hF hG hgood
  rwa [seriesFun_zero, add_zero] at h

/-- gFun(1) = B + seriesFun(1) (punctured continuity). -/
lemma gFun_one (hZC : ZeroCountProp) : gFun 1 = momentB hZC + seriesFun 1 := by
  have hgood : ∀ᶠ s in 𝓝[≠] (1 : ℂ), gFun s = momentB hZC + seriesFun s := by
    filter_upwards [good_eventually_one, self_mem_nhdsWithin] with s ⟨hζ, h0, hn⟩ h1
    exact gFun_eq_momentB hZC hζ h0 h1 hn
  have hF : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)
  have hG0 : ContinuousAt ((fun _ => momentB hZC) + seriesFun) 1 :=
    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_one).continuousAt
  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 1 := hG0
  exact eq_of_eventuallyEq_nhd_ne hF hG hgood

/-- The FE sign: gFun(1) = −gFun(0) (xiL(1−s) = xiL(s), chain rule). -/
lemma gFun_one_eq_neg : gFun 1 = -gFun 0 := by
  have hfun : (fun s : ℂ => xiL (1 - s)) = xiL := funext xiL_one_sub
  have hderiv : deriv (fun s : ℂ => xiL (1 - s)) 0 = -deriv xiL 1 := by
    have h1 : DifferentiableAt ℂ xiL ((fun s : ℂ => 1 - s) 0) := by
      simpa using differentiable_xiL 1
    have h2 : DifferentiableAt ℂ (fun s : ℂ => 1 - s) 0 :=
      (differentiableAt_const (1 : ℂ)).sub differentiableAt_id
    have hcomp : deriv (xiL ∘ fun s : ℂ => 1 - s) 0 =
        deriv xiL ((fun s : ℂ => 1 - s) 0) * deriv (fun s : ℂ => 1 - s) 0 :=
      deriv_comp 0 h1 h2
    have heq : (xiL ∘ fun s : ℂ => 1 - s) = fun s : ℂ => xiL (1 - s) := rfl
    rw [heq] at hcomp
    have hinner : deriv (fun s : ℂ => 1 - s) 0 = -1 := by
      have h0' : HasDerivAt (fun s : ℂ => 1 - s) (0 - 1) 0 :=
        (hasDerivAt_const (0 : ℂ) (1 : ℂ)).sub (hasDerivAt_id' 0)
      rw [h0'.deriv]
      norm_num
    rw [hinner] at hcomp
    simp at hcomp
    exact hcomp
  have h0 : deriv xiL 0 = -deriv xiL 1 := by
    have hcongr : deriv xiL 0 = deriv (fun s : ℂ => xiL (1 - s)) 0 :=
      (Filter.EventuallyEq.of_eq hfun.symm).deriv_eq
    rw [hcongr, hderiv]
  rw [gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_zero, xiL_one, h0]
  field_simp

/-! ## 4. The summability budget and the k = 1 rearrangement -/

lemma nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (ρ : ℂ) ≠ 0 := by
  intro h0
  have h2 := ρ.2.2.1
  rw [h0, Complex.zero_re] at h2
  exact lt_irrefl 0 h2

lemma one_sub_nontrivialZero_ne_zero (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
    (1 : ℂ) - (ρ : ℂ) ≠ 0 := by
  intro h
  have h3 : (1 : ℂ) = (ρ : ℂ) := sub_eq_zero.mp h
  have h4 := ρ.2.2.2
  rw [← h3, Complex.one_re] at h4
  exact lt_irrefl 1 h4

lemma norm_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) < ‖(ρ : ℂ)‖ :=
  norm_pos_iff.mpr (nontrivialZero_ne_zero ρ)

lemma norm_one_sub_nontrivialZero_pos (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
    (0 : ℝ) < ‖(1 : ℂ) - (ρ : ℂ)‖ :=
  norm_pos_iff.mpr (one_sub_nontrivialZero_ne_zero ρ)

/-- **Master summability**: Σ mult/‖ρ‖² over the zeros (the ii′-2
finite-ball + (9/4)-comparison skeleton). -/
lemma summable_mult_div_norm_sq :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2) := by
  have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) :=
    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left (9 / 4)
  set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
    if (2 : ℝ) ≤ ‖(ρ : ℂ)‖ then
      (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))
    else (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 with hDdef
  have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}.Finite := by
    have hcomp : IsCompact (Metric.closedBall (0 : ℂ) 2) := isCompact_closedBall _ _
    have hzeros : (Metric.closedBall (0 : ℂ) 2) ∩ {ρ : ℂ | IsNontrivialZero ρ}
        ⊆ (Metric.closedBall (0 : ℂ) 2) ∩ riemannZetaZeros := by
      intro z hz
      exact ⟨hz.1, hz.2.1⟩
    have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros
    have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |
        ¬ ((2 : ℝ) ≤ ‖(ρ : ℂ)‖)}).Finite := by
      apply hfin2.subset
      rintro z ⟨ρ, hρ, rfl⟩
      refine ⟨?_, ρ.2⟩
      simp only [Metric.mem_closedBall, dist_zero_right]
      exact le_of_lt (lt_of_not_ge hρ)
    exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)
  have hE : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by
    apply summable_of_hasFiniteSupport
    apply hfin.subset
    intro ρ hρ
    simp only [Function.mem_support, ne_eq] at hρ
    by_contra hball
    apply hρ
    have hball' : (2 : ℝ) ≤ ‖(ρ : ℂ)‖ := not_not.mp hball
    simp only [D, if_pos hball']
    ring
  have hD : Summable D := by
    have hsum := hbase.add hE
    have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
        (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +
          (D ρ - (9 / 4) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))))) = D := by
      funext ρ
      ring
    rw [heq] at hsum
    exact hsum
  refine Summable.of_norm_bounded hD (fun ρ => ?_)
  by_cases hρ : (2 : ℝ) ≤ ‖(ρ : ℂ)‖
  · simp only [D, if_pos hρ]
    have hz := ρ.2
    have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by norm_num) hρ
    have hgpos : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by
      have hnn := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
      linarith
    have hcomp : 1 + Complex.normSq (gammaOf (ρ : ℂ)) ≤ 9 / 4 * ‖(ρ : ℂ)‖ ^ 2 :=
      normSq_gammaOf_le_mul_norm_sq (n := 1) le_rfl hz.2.1.le hz.2.2.le (by simpa using hρ)
    have key : (zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 ≤
        (9 / 4) * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)) := by
      rw [div_le_div_iff₀ (pow_pos hρpos 2) hgpos]
      calc (zeroMult ρ : ℝ) * (1 + Complex.normSq (gammaOf ρ))
          ≤ (zeroMult ρ : ℝ) * (9 / 4 * ‖(ρ : ℂ)‖ ^ 2) :=
            mul_le_mul_of_nonneg_left hcomp (Nat.cast_nonneg _)
        _ = (9 / 4 * (zeroMult ρ : ℝ)) * ‖(ρ : ℂ)‖ ^ 2 := by ring
    rw [Real.norm_of_nonneg (by positivity)]
    exact key
  · simp only [D, if_neg hρ]
    rw [Real.norm_of_nonneg (by positivity)]

/-- The avoiding-ball lower bound: every zero has δ ≤ ‖ρ‖. -/
lemma exists_norm_lower_bound :
    ∃ δ : ℝ, 0 < δ ∧ ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, δ ≤ ‖(ρ : ℂ)‖ := by
  obtain ⟨δ, hδ, hball⟩ := exists_ball_avoid_nontrivialZeros 0 not_isNontrivialZero_zero
  refine ⟨δ, hδ, fun ρ => ?_⟩
  by_contra h
  exact hball ρ (by rw [Metric.mem_ball, dist_zero_right]; exact lt_of_not_ge h)

/-- Σ mult·ρ^{−k} is absolutely summable for k ≥ 2. -/
lemma summable_mult_inv_pow {k : ℕ} (hk : 2 ≤ k) :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k) := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le hk
  obtain ⟨δ, hδ, hδle⟩ := exists_norm_lower_bound
  apply Summable.of_norm_bounded (summable_mult_div_norm_sq.mul_left ((1 / δ) ^ m))
  intro ρ
  have hρδ := hδle ρ
  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le hδ hρδ
  rw [norm_mul, norm_pow, norm_div, norm_one, RCLike.norm_natCast, div_pow, one_pow]
  calc (zeroMult ρ : ℝ) * (1 / ‖(ρ : ℂ)‖ ^ (2 + m))
      = (zeroMult ρ : ℝ) * ((1 / ‖(ρ : ℂ)‖ ^ 2) * (1 / ‖(ρ : ℂ)‖ ^ m)) := by
        rw [pow_add, ← one_div_mul_one_div]
    _ ≤ (zeroMult ρ : ℝ) * ((1 / ‖(ρ : ℂ)‖ ^ 2) * (1 / δ ^ m)) := by
        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
        apply mul_le_mul_of_nonneg_left _ (by positivity : (0 : ℝ) ≤ 1 / ‖(ρ : ℂ)‖ ^ 2)
        exact one_div_le_one_div_of_le (pow_pos hδ m) (pow_le_pow_left₀ hδ.le hρδ m)
    _ = (1 / δ) ^ m * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2) := by
        rw [div_pow, one_pow]
        ring

/-- The conjugation reindex: Σ mult·ρ̄^{−k} = Σ mult·ρ^{−k}. -/
lemma tsum_mult_inv_pow_conj (k : ℕ) :
    (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k := by
  have h := Equiv.tsum_eq conjZeroEquiv
    (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℂ) * (1 / (σ : ℂ)) ^ k)
  rw [← h]
  apply tsum_congr
  intro ρ
  have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=
    rfl
  show (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k =
    (zeroMult ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) : ℂ) *
      (1 / ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ)) ^ k
  rw [e1, zeroMult_conj ρ.2]

/-- The conj-summability transfer. -/
lemma summable_mult_inv_pow_conj {k : ℕ} (hk : 2 ≤ k) :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) := by
  have e : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) =
      (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℂ) * (1 / (σ : ℂ)) ^ k) ∘
        conjZeroEquiv := by
    funext ρ
    have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=
      rfl
    show (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k =
      (zeroMult ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) : ℂ) *
        (1 / ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ)) ^ k
    rw [e1, zeroMult_conj ρ.2]
  rw [e]
  exact (Equiv.summable_iff conjZeroEquiv).mpr (summable_mult_inv_pow hk)

/-- **The unpaired form** (k ≥ 2): the paired sum collapses to the
unpaired sum by conj-invariance: sigmaP k = ½(S + S) = S. -/
lemma sigmaP_eq_unpaired {k : ℕ} (hk : 2 ≤ k) :
    sigmaP k = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k := by
  have hs1 := summable_mult_inv_pow hk
  have hs2 := summable_mult_inv_pow_conj hk
  have step : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, sigmaSlice k ρ) =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, (1 / 2 : ℂ) *
        ((zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ k +
          (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ k) := by
    apply tsum_congr
    intro ρ
    rw [sigmaSlice]
    ring
  rw [sigmaP, step, tsum_mul_left, Summable.tsum_add hs1 hs2, tsum_mult_inv_pow_conj k]
  ring

/-- The reflected master summability: Σ mult/‖1−ρ‖² (reindex transfer). -/
lemma summable_mult_div_norm_sq_one_sub :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by
  have e : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) =
      (fun σ : {σ : ℂ // IsNontrivialZero σ} => (zeroMult σ : ℝ) / ‖(σ : ℂ)‖ ^ 2) ∘
        oneSubZeroEquiv := by
    funext ρ
    have e1 : ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = 1 - (ρ : ℂ) := rfl
    show (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2 =
      (zeroMult ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) : ℝ) /
        ‖((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ)‖ ^ 2
    rw [e1, zeroMult_one_sub ρ.2.2.1 ρ.2.2.2]
  rw [e]
  exact (Equiv.summable_iff oneSubZeroEquiv).mpr summable_mult_div_norm_sq

/-- The AM-GM bound: mult·(1/(‖ρ‖‖1−ρ‖)) ≤ ½(mult/‖ρ‖² + mult/‖1−ρ‖²). -/
lemma mult_div_norm_mul_norm_le (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
    (zeroMult ρ : ℝ) * (1 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) ≤
      (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +
        (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by
  have hρ0 := norm_nontrivialZero_pos ρ
  have h1ρ0 := norm_one_sub_nontrivialZero_pos ρ
  have key : 2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) ≤
      1 / ‖(ρ : ℂ)‖ ^ 2 + 1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2 := by
    have h1 : (0 : ℝ) ≤ (1 / ‖(ρ : ℂ)‖ - 1 / ‖(1 : ℂ) - (ρ : ℂ)‖) ^ 2 := sq_nonneg _
    have hexp : (1 / ‖(ρ : ℂ)‖ - 1 / ‖(1 : ℂ) - (ρ : ℂ)‖) ^ 2 =
        1 / ‖(ρ : ℂ)‖ ^ 2 - 2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) +
          1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2 := by
      have hm : (2 : ℝ) * (1 / ‖(ρ : ℂ)‖) * (1 / ‖(1 : ℂ) - (ρ : ℂ)‖) =
          2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖) := by
        rw [mul_assoc, one_div_mul_one_div, mul_one_div]
      rw [sub_sq, div_pow, div_pow, one_pow, hm]
    rw [hexp] at h1
    linarith
  calc (zeroMult ρ : ℝ) * (1 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖))
      = (zeroMult ρ : ℝ) / 2 * (2 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) := by ring
    _ ≤ (zeroMult ρ : ℝ) / 2 * (1 / ‖(ρ : ℂ)‖ ^ 2 + 1 / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) :=
        mul_le_mul_of_nonneg_left key (div_nonneg (Nat.cast_nonneg _) (by norm_num))
    _ = (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +
        (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := by ring

/-- The mixed family Σ mult/(ρ(1−ρ)) is absolutely summable. -/
lemma summable_mult_one_div_mul_one_sub :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ))))) := by
  have hsum := summable_mult_div_norm_sq.add summable_mult_div_norm_sq_one_sub
  apply Summable.of_norm_bounded (hsum.mul_left (1 / 2))
  intro ρ
  rw [norm_mul, norm_div, norm_one, RCLike.norm_natCast, norm_mul]
  show (zeroMult ρ : ℝ) * (1 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) ≤ _
  exact mult_div_norm_mul_norm_le ρ

/-- The V-family is absolutely summable (1/ρ̄ − 1/(1−ρ) = O(‖ρ‖⁻¹‖1−ρ‖⁻¹)). -/
lemma summable_mult_vTerm :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)))) := by
  have hsum := summable_mult_div_norm_sq.add summable_mult_div_norm_sq_one_sub
  apply Summable.of_norm_bounded (hsum.mul_left (1 / 2))
  intro ρ
  have hρ0 := norm_nontrivialZero_pos ρ
  have h1ρ0 := norm_one_sub_nontrivialZero_pos ρ
  have hconj : ‖((starRingEnd ℂ) (ρ : ℂ))‖ = ‖(ρ : ℂ)‖ := Complex.norm_conj _
  have hid : 1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)) =
      ((1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)) /
        (((starRingEnd ℂ) (ρ : ℂ)) * (1 - (ρ : ℂ))) := by
    have hc0 : ((starRingEnd ℂ) (ρ : ℂ)) ≠ 0 := by
      have h1 : (0 : ℝ) < ‖((starRingEnd ℂ) (ρ : ℂ))‖ := by
        rw [Complex.norm_conj]
        exact norm_nontrivialZero_pos ρ
      exact norm_pos_iff.mp h1
    have h1ρ0' : (1 : ℂ) - (ρ : ℂ) ≠ 0 := one_sub_nontrivialZero_ne_zero ρ
    field_simp [hc0, h1ρ0']
  have hnum : ‖(1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)‖ ≤ 1 := by
    have e : (1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ) = ((1 - 2 * (ρ : ℂ).re : ℝ) : ℂ) := by
      rw [sub_sub, Complex.add_conj]
      push_cast
      ring
    rw [e, Complex.norm_real, Real.norm_eq_abs, abs_le]
    have hre0 := ρ.2.2.1
    have hre1 := ρ.2.2.2
    constructor <;> linarith
  rw [norm_mul, hid, norm_div, norm_mul, hconj, RCLike.norm_natCast]
  calc (zeroMult ρ : ℝ) * (‖(1 : ℂ) - (ρ : ℂ) - (starRingEnd ℂ) (ρ : ℂ)‖ /
        (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖))
      ≤ (zeroMult ρ : ℝ) * (1 / (‖(ρ : ℂ)‖ * ‖(1 : ℂ) - (ρ : ℂ)‖)) :=
        mul_le_mul_of_nonneg_left (div_le_div_of_nonneg_right hnum (mul_pos hρ0 h1ρ0).le)
          (Nat.cast_nonneg _)
    _ ≤ (1 / 2) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2 +
          (zeroMult ρ : ℝ) / ‖(1 : ℂ) - (ρ : ℂ)‖ ^ 2) := mult_div_norm_mul_norm_le ρ

/-- **The V-sum vanishes**: the conj reindex gives V = W and the reflect
reindex gives W = −V. -/
lemma vTerm_tsum_eq_zero :
    (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ)))) = 0 := by
  set V := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ))) with hV
  have h1 : V = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) - 1 / (1 - (starRingEnd ℂ) (ρ : ℂ))) := by
    have h := Equiv.tsum_eq conjZeroEquiv (fun σ : {σ : ℂ // IsNontrivialZero σ} =>
      (zeroMult σ : ℂ) * (1 / ((starRingEnd ℂ) (σ : ℂ)) - 1 / (1 - (σ : ℂ))))
    rw [hV, ← h]
    apply tsum_congr
    intro ρ
    have e1 : ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = (starRingEnd ℂ) (ρ : ℂ) :=
      rfl
    have e2 : (starRingEnd ℂ) ((starRingEnd ℂ) (ρ : ℂ)) = (ρ : ℂ) := by
      rw [starRingEnd_apply, starRingEnd_apply, star_star]
    show (zeroMult ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) : ℂ) *
        (1 / ((starRingEnd ℂ) ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ)) -
          1 / (1 - ((conjZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ))) =
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) - 1 / (1 - (starRingEnd ℂ) (ρ : ℂ)))
    rw [e1, zeroMult_conj ρ.2, e2]
  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) - 1 / (1 - (starRingEnd ℂ) (ρ : ℂ)))) = -V := by
    have h := Equiv.tsum_eq oneSubZeroEquiv (fun σ : {σ : ℂ // IsNontrivialZero σ} =>
      (zeroMult σ : ℂ) * (1 / (σ : ℂ) - 1 / (1 - (starRingEnd ℂ) (σ : ℂ))))
    rw [← h]
    rw [hV, ← tsum_neg]
    apply tsum_congr
    intro ρ
    have e1 : ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) = 1 - (ρ : ℂ) := rfl
    have e2 : (1 : ℂ) - (starRingEnd ℂ) (1 - (ρ : ℂ)) = (starRingEnd ℂ) (ρ : ℂ) := by
      rw [map_sub, map_one, sub_sub_cancel]
    show (zeroMult ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) : ℂ) *
        (1 / ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ) -
          1 / (1 - (starRingEnd ℂ) ((oneSubZeroEquiv ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ))) =
      -((zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ))))
    rw [e1, zeroMult_one_sub ρ.2.2.1 ρ.2.2.2, e2]
    ring
  have h3 : V = -V := h1.trans h2
  have h4 : (2 : ℂ) * V = 0 := by linear_combination h3
  exact (mul_eq_zero.mp h4).resolve_left (by norm_num)

/-- The first family (1/ρ + 1/ρ̄) is summable (the sigmaSlice 1 form). -/
lemma summable_mult_fst :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) := by
  have h := (sigmaSlice_summable 1 le_rfl).mul_left (2 : ℂ)
  apply h.congr
  intro ρ
  rw [sigmaSlice, pow_one, pow_one]
  ring

/-- The second family (1/ρ + 1/(1−ρ)) is summable (the mixed form). -/
lemma summable_mult_snd :
    Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ)))) := by
  apply summable_mult_one_div_mul_one_sub.congr
  intro ρ
  have hρ0 := nontrivialZero_ne_zero ρ
  have h1ρ := one_sub_nontrivialZero_ne_zero ρ
  congr 1
  field_simp [hρ0, h1ρ]
  ring

/-- **Twice σ₁ is the mixed series**: 2·sigmaP 1 = Σ mult/(ρ(1−ρ)).
The two pairings differ by V = 0. -/
lemma two_mul_sigmaP_one :
    (2 : ℂ) * sigmaP 1 = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ)))) := by
  have h1 : (2 : ℂ) * sigmaP 1 = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ))) := by
    rw [sigmaP, ← tsum_mul_left]
    apply tsum_congr
    intro ρ
    rw [sigmaSlice, pow_one, pow_one]
    ring
  have h2 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / ((ρ : ℂ) * (1 - (ρ : ℂ))))) =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
        (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ))) := by
    apply tsum_congr
    intro ρ
    have hρ0 := nontrivialZero_ne_zero ρ
    have h1ρ := one_sub_nontrivialZero_ne_zero ρ
    congr 1
    field_simp [hρ0, h1ρ]
    ring
  have h3 : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) -
        (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
          (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ)))) =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
        (zeroMult ρ : ℂ) * (1 / ((starRingEnd ℂ) (ρ : ℂ)) - 1 / (1 - (ρ : ℂ))) := by
    rw [← Summable.tsum_sub summable_mult_fst summable_mult_snd]
    apply tsum_congr
    intro ρ
    ring
  have hFst : (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
      (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / ((starRingEnd ℂ) (ρ : ℂ)))) =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
        (zeroMult ρ : ℂ) * (1 / (ρ : ℂ) + 1 / (1 - (ρ : ℂ))) :=
    sub_eq_zero.mp (by rw [h3]; exact vTerm_tsum_eq_zero)
  rw [h1, hFst, ← h2]

/-- **(M) at k = 1**: σ₁ = −gFun(0). Via 2σ₁ = seriesFun(1) =
gFun(1) − B = −2·gFun(0). -/
lemma sigmaP_one_eq_neg_gFun_zero (hZC : ZeroCountProp) : sigmaP 1 = -gFun 0 := by
  have h2 := two_mul_sigmaP_one
  rw [← seriesFun_one] at h2
  have hg1 := gFun_one hZC
  have hg0 := gFun_zero hZC
  have hfe := gFun_one_eq_neg
  linear_combination (h2 - hg1 + hg0 + hfe) / 2

/-! ## 5. Termwise iterated derivation of the series at 0 -/

/-- The iterated derivative of s ↦ (s+c)⁻¹ (positive form, from
LiDigamma's negative form via `iteratedDeriv_neg`). -/
lemma iteratedDeriv_zpow_neg_one (k : ℕ) (c : ℂ) {s : ℂ} (hs : s + c ≠ 0) :
    iteratedDeriv k (fun s : ℂ => (s + c) ^ (-1 : ℤ)) s =
      ((-1 : ℂ)) ^ k * (k ! : ℂ) * (s + c) ^ (-(k : ℤ) - 1) := by
  have e : (fun s : ℂ => (s + c) ^ (-1 : ℤ)) = -fun s : ℂ => -((s + c) ^ (-1 : ℤ)) :=
    funext fun s => (neg_neg _).symm
  rw [e, iteratedDeriv_neg k _ s, iteratedDeriv_neg_zpow_neg_one_add k c hs]
  simp only [neg_mul, neg_neg]

/-- The k-th iterated derivative (k ≥ 1) of a series summand:
(d/ds)^k [mult·(1/(s−ρ) + 1/ρ)] = mult·(−1)^k·k!·(s−ρ)^{−k−1}. -/
lemma iteratedDeriv_seriesTerm {j : ℕ} (hj : 1 ≤ j) (ρ : {ρ : ℂ // IsNontrivialZero ρ})
    {s : ℂ} (hs : s - (ρ : ℂ) ≠ 0) :
    iteratedDeriv j (fun s : ℂ => seriesTerm s ρ) s =
      (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ j * (j ! : ℂ) * (s - (ρ : ℂ)) ^ (-(j : ℤ) - 1)) := by
  have hsp : s + -(ρ : ℂ) ≠ 0 := by
    rw [← sub_eq_add_neg]
    exact hs
  have e : (fun s : ℂ => seriesTerm s ρ) =
      fun s : ℂ => (zeroMult ρ : ℂ) * ((s + -(ρ : ℂ)) ^ (-1 : ℤ) + ((ρ : ℂ))⁻¹) := by
    funext t
    rw [seriesTerm]
    simp only [one_div, zpow_neg_one, sub_eq_add_neg]
  have hcf : ContDiffAt ℂ j (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ)) s := by
    have h1 : AnalyticAt ℂ (fun s : ℂ => s + -(ρ : ℂ)) s := analyticAt_id.add analyticAt_const
    have h2 : AnalyticAt ℂ (fun s : ℂ => 1 / (s + -(ρ : ℂ))) s := analyticAt_const.div h1 hsp
    have e2 : (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ)) = fun s => 1 / (s + -(ρ : ℂ)) :=
      funext fun t => by rw [zpow_neg_one, one_div]
    rw [e2]
    exact h2.contDiffAt
  have hcc : ContDiffAt ℂ j (fun _ : ℂ => ((ρ : ℂ))⁻¹) s := contDiff_const.contDiffAt
  have hinner : ContDiffAt ℂ j (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ) + ((ρ : ℂ))⁻¹) s :=
    hcf.add hcc
  rw [e, iteratedDeriv_const_mul _ hinner]
  congr 1
  have hsplit : (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ) + ((ρ : ℂ))⁻¹) =
      (fun s : ℂ => (s + -(ρ : ℂ)) ^ (-1 : ℤ)) + (fun _ : ℂ => ((ρ : ℂ))⁻¹) := rfl
  rw [hsplit, iteratedDeriv_add hcf hcc, iteratedDeriv_const, if_neg (show j ≠ 0 by omega),
    add_zero, sub_eq_add_neg]
  exact iteratedDeriv_zpow_neg_one j (-(ρ : ℂ)) hsp

set_option maxHeartbeats 800000 in
/-- The k-th derivative family (k ≥ 1) is summable locally uniformly on
ball(0, δ/2) (the M-test; dominator C_j·mult/‖ρ‖² via ‖s−ρ‖ ≥ ‖ρ‖/2 and
1/‖ρ‖^{j−1} ≤ (1/δ)^{j−1}). -/
lemma seriesTerm_deriv_summableLocallyUniformlyOn {j : ℕ} (hj : 1 ≤ j)
    {δ : ℝ} (hδ : 0 < δ) (hδle : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, δ ≤ ‖(ρ : ℂ)‖) :
    SummableLocallyUniformlyOn
      (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
        iteratedDerivWithin j (fun s : ℂ => seriesTerm s ρ) (Metric.ball 0 (δ / 2)))
      (Metric.ball 0 (δ / 2)) := by
  apply SummableLocallyUniformlyOn_of_locally_bounded Metric.isOpen_ball
  intro K hK _
  refine ⟨fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
      ((j ! : ℝ) * 2 ^ (j + 1) * (1 / δ) ^ (j - 1)) * ((zeroMult ρ : ℝ) / ‖(ρ : ℂ)‖ ^ 2),
    summable_mult_div_norm_sq.mul_left _, fun ρ s hs => ?_⟩
  have hsb : s ∈ Metric.ball (0 : ℂ) (δ / 2) := hK hs
  have hsbn : ‖s‖ < δ / 2 := by
    simpa only [Metric.mem_ball, dist_zero_right] using hsb
  have hρge : δ ≤ ‖(ρ : ℂ)‖ := hδle ρ
  have hρpos : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le hδ hρge
  have hnorm1 : ‖(ρ : ℂ)‖ / 2 ≤ ‖s - (ρ : ℂ)‖ := by
    have h2 := norm_sub_norm_le (ρ : ℂ) s
    rw [norm_sub_rev]
    linarith
  have hsρ : s - (ρ : ℂ) ≠ 0 :=
    norm_pos_iff.mp (lt_of_lt_of_le (by linarith : (0 : ℝ) < ‖(ρ : ℂ)‖ / 2) hnorm1)
  rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) hsb, iteratedDeriv_seriesTerm hj ρ hsρ]
  rw [norm_mul, norm_mul, norm_mul, RCLike.norm_natCast]
  have hsign : ‖((-1 : ℂ)) ^ j‖ = 1 := by rw [norm_pow, norm_neg, norm_one, one_pow]
  rw [hsign, one_mul, RCLike.norm_natCast, norm_zpow]
  rw [show (-(j : ℤ) - 1 : ℤ) = -(((j + 1 : ℕ) : ℤ)) by push_cast; ring, zpow_neg, zpow_natCast]
  have hjeq : j + 1 = (j - 1) + 2 := by omega
  have h1 : (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹ ≤ ((‖(ρ : ℂ)‖ / 2) ^ (j + 1))⁻¹ := by
    rw [← one_div, ← one_div]
    exact one_div_le_one_div_of_le (pow_pos (by linarith : (0 : ℝ) < ‖(ρ : ℂ)‖ / 2) _)
      (pow_le_pow_left₀ (by linarith : (0 : ℝ) ≤ ‖(ρ : ℂ)‖ / 2) hnorm1 _)
  have h2 : ((‖(ρ : ℂ)‖ / 2) ^ (j + 1))⁻¹ = 2 ^ (j + 1) * (‖(ρ : ℂ)‖ ^ (j + 1))⁻¹ := by
    rw [div_pow, inv_div, div_eq_mul_inv]
  have h3 : (‖(ρ : ℂ)‖ ^ (j + 1))⁻¹ ≤ (δ ^ (j - 1))⁻¹ * (‖(ρ : ℂ)‖ ^ 2)⁻¹ := by
    rw [hjeq, pow_add, mul_inv]
    have h4 : (‖(ρ : ℂ)‖ ^ (j - 1))⁻¹ ≤ (δ ^ (j - 1))⁻¹ := by
      rw [← one_div, ← one_div]
      exact one_div_le_one_div_of_le (pow_pos hδ _) (pow_le_pow_left₀ hδ.le hρge _)
    exact mul_le_mul_of_nonneg_right h4 (by positivity)
  have hkey : (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹ ≤
      2 ^ (j + 1) * (1 / δ) ^ (j - 1) * (‖(ρ : ℂ)‖ ^ 2)⁻¹ := by
    calc (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹
        ≤ ((‖(ρ : ℂ)‖ / 2) ^ (j + 1))⁻¹ := h1
      _ = 2 ^ (j + 1) * (‖(ρ : ℂ)‖ ^ (j + 1))⁻¹ := h2
      _ ≤ 2 ^ (j + 1) * ((δ ^ (j - 1))⁻¹ * (‖(ρ : ℂ)‖ ^ 2)⁻¹) :=
          mul_le_mul_of_nonneg_left h3 (by positivity)
      _ = 2 ^ (j + 1) * (1 / δ) ^ (j - 1) * (‖(ρ : ℂ)‖ ^ 2)⁻¹ := by
          rw [div_pow, one_pow, one_div, mul_assoc]
  have hfac : (0 : ℝ) ≤ (zeroMult ρ : ℝ) * (j ! : ℝ) := by positivity
  calc (↑(zeroMult ρ)) * (↑j ! * (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹)
      = (↑(zeroMult ρ) * ↑j !) * (‖s - (ρ : ℂ)‖ ^ (j + 1))⁻¹ := by rw [mul_assoc]
    _ ≤ (↑(zeroMult ρ) * ↑j !) * (2 ^ (j + 1) * (1 / δ) ^ (j - 1) * (‖(ρ : ℂ)‖ ^ 2)⁻¹) :=
        mul_le_mul_of_nonneg_left hkey hfac
    _ = (↑j ! * 2 ^ (j + 1) * (1 / δ) ^ (j - 1)) * ((↑(zeroMult ρ)) / ‖(ρ : ℂ)‖ ^ 2) := by ring

/-- The j-th iterated derivative (j ≥ 1) of seriesFun at 0, termwise:
(d/ds)^j seriesFun (0) = Σ_ρ mult·(−1)^j·j!·(0−ρ)^{−j−1}
(the LiDigamma §8 `iteratedDerivWithin_tsum` pattern on ball(0, δ/2)). -/
lemma iteratedDeriv_seriesFun_zero {j : ℕ} (hj : 1 ≤ j) :
    iteratedDeriv j seriesFun 0 =
      ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},
        (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ j * (j ! : ℂ) * (0 - (ρ : ℂ)) ^ (-(j : ℤ) - 1)) := by
  obtain ⟨δ, hδ, hδle⟩ := exists_norm_lower_bound
  have h0mem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) (δ / 2) := by
    rw [Metric.mem_ball, dist_zero_right, norm_zero]
    positivity
  have pole_free : ∀ t : ℂ, t ∈ Metric.ball (0 : ℂ) (δ / 2) →
      ∀ σ : {σ : ℂ // IsNontrivialZero σ}, t - (σ : ℂ) ≠ 0 := by
    intro t ht σ
    rw [Metric.mem_ball, dist_zero_right] at ht
    have hσ := hδle σ
    have h1 : ‖(σ : ℂ)‖ - ‖t‖ ≤ ‖t - (σ : ℂ)‖ := by
      have h2 := norm_sub_norm_le (σ : ℂ) t
      rw [norm_sub_rev]
      exact h2
    have hpos : (0 : ℝ) < ‖t - (σ : ℂ)‖ := lt_of_lt_of_le (by linarith) h1
    exact norm_pos_iff.mp hpos
  show iteratedDeriv j (fun s : ℂ => ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, seriesTerm s ρ) 0 = _
  rw [← (iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem,
    iteratedDerivWithin_tsum j Metric.isOpen_ball h0mem
      (fun t _ => seriesSummable t)
      (fun k hk1 _ => seriesTerm_deriv_summableLocallyUniformlyOn hk1 hδ hδle)
      ?_]
  · apply tsum_congr
    intro ρ
    rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) h0mem]
    exact iteratedDeriv_seriesTerm hj ρ (pole_free 0 h0mem ρ)
  · intro σ k r _ hr
    rcases Nat.eq_zero_or_pos k with hk0 | hk0
    · subst hk0
      rw [iteratedDerivWithin_zero]
      have hrσ := pole_free r hr σ
      have h1 : AnalyticAt ℂ (fun z : ℂ => z - (σ : ℂ)) r := analyticAt_id.sub analyticAt_const
      have h2 : AnalyticAt ℂ (fun z : ℂ => 1 / (z - (σ : ℂ))) r := analyticAt_const.div h1 hrσ
      have h3 : AnalyticAt ℂ (fun z : ℂ =>
          (zeroMult σ : ℂ) * (1 / (z - (σ : ℂ)) + 1 / (σ : ℂ))) r :=
        analyticAt_const.mul (h2.add analyticAt_const)
      show DifferentiableAt ℂ (fun z : ℂ =>
        (zeroMult σ : ℂ) * (1 / (z - (σ : ℂ)) + 1 / (σ : ℂ))) r
      exact h3.differentiableAt
    · have h5 : (fun t => iteratedDerivWithin k (fun z : ℂ => seriesTerm z σ)
          (Metric.ball 0 (δ / 2)) t) =ᶠ[𝓝 r]
          fun t => (zeroMult σ : ℂ) * (((-1 : ℂ)) ^ k * (k ! : ℂ) *
            (t - (σ : ℂ)) ^ (-(k : ℤ) - 1)) := by
        filter_upwards [Metric.isOpen_ball.mem_nhds hr] with t ht
        rw [(iteratedDerivWithin_of_isOpen Metric.isOpen_ball) ht]
        exact iteratedDeriv_seriesTerm (by omega) σ (pole_free t ht σ)
      apply h5.differentiableAt_iff.mpr
      have hrσ := pole_free r hr σ
      have h4 : DifferentiableAt ℂ (fun t : ℂ => t - (σ : ℂ)) r :=
        differentiableAt_id.sub (differentiableAt_const _)
      have h6 : DifferentiableAt ℂ (fun t : ℂ => (t - (σ : ℂ)) ^ (-(k : ℤ) - 1)) r := by
        have h7 := ((hasDerivAt_zpow (-(k : ℤ) - 1) (r - (σ : ℂ))
          (Or.inl hrσ)).differentiableAt).comp r h4
        have heq : ((fun x : ℂ => x ^ (-(k : ℤ) - 1)) ∘ fun t : ℂ => t - (σ : ℂ)) =
            fun t : ℂ => (t - (σ : ℂ)) ^ (-(k : ℤ) - 1) := rfl
        rw [heq] at h7
        exact h7
      exact (differentiableAt_const _).mul ((differentiableAt_const _).mul h6)

/-! ## 6. The capstone -/

/-- The identity (G) on a full neighbourhood of 0 (the punctured version
upgraded by the point values gFun(0) = B, seriesFun(0) = 0). -/
lemma gFun_eventuallyEq_zero (hZC : ZeroCountProp) :
    gFun =ᶠ[𝓝 (0 : ℂ)] (fun s => momentB hZC + seriesFun s) := by
  have h := good_eventually_zero
  rw [eventually_nhdsWithin_iff] at h
  filter_upwards [h] with s hs
  by_cases h0 : s = 0
  · subst h0
    rw [gFun_zero hZC, seriesFun_zero, add_zero]
  · have ⟨hζ, h1, hn⟩ := hs h0
    exact gFun_eq_momentB hZC hζ h0 h1 hn

/-- **(M), the capstone of ii′-3b**: for all k ≥ 1,
sigmaP k = −(iteratedDeriv (k−1) gFun 0)/(k−1)!.
k = 1 by the conj/reflect reindex (§4); k ≥ 2 by (G) + termwise
derivation of the zero series at 0 (§5). Perimeter: ZeroCountProp only. -/
theorem sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC : ZeroCountProp) {k : ℕ} (hk : 1 ≤ k) :
    sigmaP k = -iteratedDeriv (k - 1) gFun 0 / ((k - 1)! : ℂ) := by
  rcases k with _ | k
  · omega
  · rw [Nat.add_sub_cancel]
    by_cases hk0 : k = 0
    · subst hk0
      have e : ((0 ! : ℕ) : ℂ) = 1 := by norm_num
      rw [iteratedDeriv_zero, e, div_one]
      exact sigmaP_one_eq_neg_gFun_zero hZC
    · have hk1 : 1 ≤ k := Nat.one_le_iff_ne_zero.mpr hk0
      have hev := gFun_eventuallyEq_zero hZC
      rw [iteratedDeriv_congr_of_eventuallyEq hev k]
      have hcf : ContDiffAt ℂ k (fun _ : ℂ => momentB hZC) 0 := contDiff_const.contDiffAt
      have hcg : ContDiffAt ℂ k seriesFun 0 :=
        (seriesFun_analyticAt not_isNontrivialZero_zero).contDiffAt
      have hsplit : (fun s : ℂ => momentB hZC + seriesFun s) =
          (fun _ : ℂ => momentB hZC) + seriesFun := rfl
      rw [hsplit, iteratedDeriv_add hcf hcg, iteratedDeriv_const, if_neg hk0, zero_add,
        iteratedDeriv_seriesFun_zero hk1]
      have hterm : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ},
          (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ k * (k ! : ℂ) * (0 - (ρ : ℂ)) ^ (-(k : ℤ) - 1)) =
          -((k ! : ℂ) * ((zeroMult ρ : ℂ) * (1 / (ρ : ℂ)) ^ (k + 1))) := by
        intro ρ
        have e1 : (0 - (ρ : ℂ)) ^ (-(k : ℤ) - 1) =
            ((-1 : ℂ)) ^ (k + 1) * (1 / (ρ : ℂ)) ^ (k + 1) := by
          rw [zero_sub,
            show (-(k : ℤ) - 1 : ℤ) = -(((k + 1 : ℕ) : ℤ)) by push_cast; ring,
            zpow_neg, zpow_natCast, neg_pow, mul_inv]
          congr 1
          · apply inv_eq_of_mul_eq_one_right
            rw [← pow_add, show (k + 1) + (k + 1) = 2 * (k + 1) by ring, pow_mul,
              show ((-1 : ℂ)) ^ 2 = 1 by norm_num, one_pow]
          · rw [← inv_pow, one_div]
        rw [e1]
        have hsign : ((-1 : ℂ)) ^ k * ((-1 : ℂ)) ^ (k + 1) = -1 := by
          rw [← pow_add, show k + (k + 1) = 2 * k + 1 by ring, pow_add, pow_mul,
            show ((-1 : ℂ)) ^ 2 = 1 by norm_num, one_pow, pow_one, one_mul]
        have e2 : (zeroMult ρ : ℂ) * (((-1 : ℂ)) ^ k * (k ! : ℂ) *
            (((-1 : ℂ)) ^ (k + 1) * (1 / (ρ : ℂ)) ^ (k + 1))) =
            ((zeroMult ρ : ℂ) * (k ! : ℂ) * (1 / (ρ : ℂ)) ^ (k + 1)) *
              (((-1 : ℂ)) ^ k * ((-1 : ℂ)) ^ (k + 1)) := by ring
        rw [e2, hsign]
        ring
      rw [tsum_congr hterm, tsum_neg, neg_neg, tsum_mul_left,
        ← sigmaP_eq_unpaired (show 2 ≤ k + 1 by omega)]
      have hfact : ((k ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero k)
      field_simp [hfact]

end NguyenRH1