LiCrux.lean

Declarations

Source

/-
LiCrux.lean — tier ii′-3c: the (4.10-a) assembly and the crux identity
Sf(n) = Res₁(n) (D-066 §2; the assembly algebra verified numerically in
D-064 §3).

The chain (all k ≥ 1, m := k−1):
- (M)   sigmaP k = −gFun^{(m)}(0)/m!                    [ii′-3b capstone]
- (FE)  gFun^{(m)}(0) = (−1)^{m+1}·gFun^{(m)}(1)        [xiL_one_sub]
- (exp) gFun^{(m)}(1) = (−1)^m·m! − m!·lcoeff m
        + (−1)^{m+1}·m!·a_{m+1}                          [shift expansion:
        1/(1+s) + hLiExt + ΓR′/ΓR(1+s); pieces (A)/(B) ii′-3a]
⟹ (4.10-a): lcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}
⟹ the crux: ResW1 n = SInfty n + 1 − liCoeff n (ℂ), i.e.
   (ResW1 n).re = Sf n, for n ≥ 1.

Perimeter: ZeroCountProp only (inherited via ii′-3b's capstone).
-/
import Mathlib
import NguyenRH1.LiMoments
import NguyenRH1.LiArchimedean
import NguyenRH1.LiZetaCoeff
import NguyenRH1.LiSkeleton

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The FE relation: gFun^{(m)}(0) = (−1)^{m+1}·gFun^{(m)}(1) -/

/-- The functional equation as a function identity: gFun(1−s) = −gFun(s)
everywhere (xiL is entire; xiL(1−s) = xiL(s) + chain rule). -/
lemma gFun_one_sub_fun : (fun s : ℂ => gFun (1 - s)) = -gFun := by
  have hderiv : ∀ s : ℂ, deriv xiL (1 - s) = -deriv xiL s := by
    intro s
    have hfun : (fun s : ℂ => xiL (1 - s)) = xiL := funext xiL_one_sub
    have h2 : deriv (fun s : ℂ => xiL (1 - s)) s = deriv xiL s := by rw [hfun]
    have h1 : DifferentiableAt ℂ xiL ((fun s : ℂ => 1 - s) s) := differentiable_xiL _
    have h2' : DifferentiableAt ℂ (fun s : ℂ => 1 - s) s :=
      (differentiableAt_const (1 : ℂ)).sub differentiableAt_id
    have hcomp : deriv (xiL ∘ fun s : ℂ => 1 - s) s =
        deriv xiL ((fun s : ℂ => 1 - s) s) * deriv (fun s : ℂ => 1 - s) s :=
      deriv_comp s 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) s = -1 := by
      have h0' : HasDerivAt (fun s : ℂ => 1 - s) (0 - 1) s :=
        (hasDerivAt_const s (1 : ℂ)).sub (hasDerivAt_id' s)
      rw [h0'.deriv]
      norm_num
    rw [hinner] at hcomp
    simp at hcomp
    rw [hcomp] at h2
    linear_combination -h2
  funext s
  rw [Pi.neg_apply, gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_one_sub, hderiv s,
    neg_div]

/-- The FE derivative relation (D-066 §2): gFun^{(m)}(0) =
(−1)^{m+1}·gFun^{(m)}(1), via the unconditional
`iteratedDeriv_comp_const_sub` + `iteratedDeriv_neg`. -/
lemma iteratedDeriv_gFun_zero (m : ℕ) :
    iteratedDeriv m gFun 0 = ((-1 : ℂ)) ^ (m + 1) * iteratedDeriv m gFun 1 := by
  have h1 := congr_fun (iteratedDeriv_comp_const_sub m gFun (1 : ℂ)) 0
  rw [sub_zero, smul_eq_mul] at h1
  rw [gFun_one_sub_fun, iteratedDeriv_neg] at h1
  linear_combination -h1

/-! ## 2. The shift expansion: gFun(1+s) = 1/(1+s) + hLiExt s + ΓR′/ΓR(1+s) -/

/-- The punctured form of the shift expansion (pure logDeriv algebra at
1+s, mirroring `gFun_eq_momentB`; no perimeter needed). -/
lemma gFun_one_add_punctured :
    ∀ᶠ s in 𝓝[≠] (0 : ℂ), gFun (1 + s) =
      1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s) := by
  -- eventually facts on 𝓝 0
  have hZA : ∀ᶠ s in 𝓝 (0 : ℂ), zetaA (1 + s) ≠ 0 := by
    have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 + (0 : ℂ))) :=
      (continuousAt_const.add continuousAt_id).tendsto
    rw [add_zero] at h1
    exact h1.eventually zetaA_ne_zero_near_one
  have hΓ1 : ∀ m : ℕ, (1 : ℂ) / 2 ≠ -(m : ℂ) := by
    intro m hm
    have e := congrArg Complex.re hm
    have e2 : (-(m : ℂ)).re = -(m : ℝ) := by simp
    have e3 : ((1 : ℂ) / 2).re = 1 / 2 := by norm_num
    rw [e3, e2] at e
    have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
    linarith
  have hΓcont : ContinuousAt Complex.Gammaℝ 1 :=
    (differentiableAt_Gammaℝ_of_not_neg_nat hΓ1).continuousAt
  have hΓ : ∀ᶠ s in 𝓝 (0 : ℂ), Complex.Gammaℝ (1 + s) ≠ 0 := by
    have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 + (0 : ℂ))) :=
      (continuousAt_const.add continuousAt_id).tendsto
    rw [add_zero] at h1
    exact h1.eventually ((hΓcont.tendsto).eventually_ne (by
      rw [Complex.Gammaℝ_one]; norm_num))
  have hpole : ∀ᶠ s in 𝓝 (0 : ℂ), ∀ m : ℕ, (1 + s) / 2 ≠ -(m : ℂ) := by
    have hopen : IsOpen {s : ℂ | 0 < (((1 + s) / 2).re)} := by
      have hcont : Continuous (fun s : ℂ => (((1 + s) / 2).re)) :=
        Complex.continuous_re.comp ((continuous_const.add continuous_id).div_const 2)
      exact isOpen_Ioi.preimage hcont
    have hmem : (0 : ℂ) ∈ {s : ℂ | 0 < (((1 + s) / 2).re)} := by
      show 0 < (((1 + (0 : ℂ)) / 2).re)
      have e : (1 + (0 : ℂ)) / 2 = 1 / 2 := by ring
      rw [e]
      simp
    filter_upwards [hopen.mem_nhds hmem] with s hs
    intro m hmeq
    rw [hmeq] at hs
    simp at hs
    have hm : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m
    linarith
  filter_upwards [self_mem_nhdsWithin, hZA.filter_mono nhdsWithin_le_nhds,
    hΓ.filter_mono nhdsWithin_le_nhds, hpole.filter_mono nhdsWithin_le_nhds,
    (eventually_ne_nhds (show (0 : ℂ) ≠ -1 by norm_num)).filter_mono nhdsWithin_le_nhds]
    with s hs0 hZAs hΓs hpols hs1
  -- point hypotheses
  have hs1' : (1 : ℂ) + s ≠ 1 := by
    intro h
    exact hs0 (show s = 0 by linear_combination h)
  have hs0' : (1 : ℂ) + s ≠ 0 := by
    intro h
    apply hs1
    linear_combination h
  have hζs : riemannZeta (1 + s) ≠ 0 := by
    intro hζ
    have e := zetaA_apply hs1'
    rw [hζ, mul_zero] at e
    exact hZAs e
  have hΓdiff : DifferentiableAt ℂ Complex.Gammaℝ (1 + s) :=
    differentiableAt_Gammaℝ_of_not_neg_nat hpols
  -- the logDeriv algebra at 1+s (the gFun_eq_momentB pattern)
  have hopen : IsOpen ({0}ᶜ ∩ {1}ᶜ : Set ℂ) :=
    isOpen_compl_singleton.inter isOpen_compl_singleton
  have hexp : xiL =ᶠ[𝓝 (1 + s)]
      (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) := by
    filter_upwards [hopen.mem_nhds ⟨hs0', hs1'⟩] with t ht
    exact xiL_eq_mul ht.1 ht.2
  have hΛeq : completedRiemannZeta =ᶠ[𝓝 (1 + s)]
      (fun t => Complex.Gammaℝ t * riemannZeta t) := by
    filter_upwards [hΓdiff.continuousAt.eventually_ne hΓs, eventually_ne_nhds hs0']
      with t htΓ ht0
    rw [riemannZeta_def_of_ne_zero ht0]
    field_simp [htΓ]
  have hlog : logDeriv xiL (1 + s) =
      logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) (1 + s) := by
    rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]
  show logDeriv xiL (1 + s) = _
  rw [hlog]
  have hP : DifferentiableAt ℂ (fun t : ℂ => t * (t - 1) / 2) (1 + s) :=
    (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2
  have hΛ : DifferentiableAt ℂ completedRiemannZeta (1 + s) :=
    differentiableAt_completedZeta hs0' hs1'
  have hP0 : (1 + s) * ((1 + s) - 1) / 2 ≠ 0 :=
    div_ne_zero (mul_ne_zero hs0' (sub_ne_zero.mpr hs1')) two_ne_zero
  have hΛ0 : completedRiemannZeta (1 + s) ≠ 0 := by
    rw [Ne, RvM.completedRiemannZeta_eq_zero_iff]
    rintro h
    exact hζs 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) (1 + s) =
      1 / (1 + s) + 1 / s := by
    rw [logDeriv_apply]
    have hderiv : deriv (fun t : ℂ => t * (t - 1) / 2) (1 + s) = (1 + s) - 1 / 2 := by
      have h2' : HasDerivAt (fun t : ℂ => t * (t - 1) / 2)
          ((1 * ((1 + s) - 1) + (1 + s) * 1) / 2) (1 + s) :=
        ((hasDerivAt_id' (1 + s)).mul ((hasDerivAt_id' (1 + s)).sub_const 1)).div_const 2
      rw [h2'.deriv]
      ring
    rw [hderiv, show ((1 : ℂ) + s) - 1 = s by ring,
      div_add_div 1 1 hs0' hs0, div_eq_div_iff
        (div_ne_zero (mul_ne_zero hs0' hs0) two_ne_zero) (mul_ne_zero hs0' hs0)]
    ring
  have hlogΛ : logDeriv completedRiemannZeta (1 + s) =
      logDeriv Complex.Gammaℝ (1 + s) + logDeriv riemannZeta (1 + s) := by
    have heq : logDeriv completedRiemannZeta (1 + s) =
        logDeriv (fun t => Complex.Gammaℝ t * riemannZeta t) (1 + 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Γs hζs hΓdiff
      (differentiableAt_riemannZeta hs1')]
  rw [hPlog, hlogΛ]
  -- the hLiExt identity: hLiExt s = 1/s + ζ′/ζ(1+s)
  have hE : hLiExt s = 1 / s + logDeriv riemannZeta (1 + s) := by
    rw [hLiExt_of_ne hs0]
    have hh : hLi (1 + s) = 1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by
      rw [hLi]
      ring_nf
    rw [hh]
    have hX : (1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s)))) / s =
        deriv zetaA (1 + s) / zetaA (1 + s) := by
      have e : 1 - (1 - s * (deriv zetaA (1 + s) / zetaA (1 + s))) =
          s * (deriv zetaA (1 + s) / zetaA (1 + s)) := by ring
      rw [e, mul_div_cancel_left₀ _ hs0]
    rw [hX]
    have hzeq : (fun w : ℂ => (w - 1) * riemannZeta w) =ᶠ[𝓝 (1 + s)] zetaA := by
      filter_upwards [eventually_ne_nhds hs1'] with z hz
      exact (zetaA_apply hz).symm
    have hderiv_zetaA : deriv zetaA (1 + s) =
        riemannZeta (1 + s) + s * deriv riemannZeta (1 + s) := by
      rw [← hzeq.deriv_eq]
      have hsplit : (fun w : ℂ => (w - 1) * riemannZeta w) =
          (fun w : ℂ => w - 1) * riemannZeta := rfl
      have hf : DifferentiableAt ℂ (fun w : ℂ => w - 1) (1 + s) := differentiableAt_id.sub_const 1
      rw [hsplit, deriv_mul hf (differentiableAt_riemannZeta hs1')]
      have h1 : deriv (fun w : ℂ => w - 1) (1 + s) = 1 :=
        ((hasDerivAt_id' (1 + s)).sub_const 1).deriv
      rw [h1]
      ring
    rw [hderiv_zetaA, zetaA_apply hs1', show ((1 : ℂ) + s) - 1 = s by ring, logDeriv_apply,
      div_add_div 1 (deriv riemannZeta (1 + s)) hs0 hζs,
      div_eq_div_iff (mul_ne_zero hs0 hζs) (mul_ne_zero hs0 hζs)]
    ring
  rw [hE]
  ring

/-- The shift expansion on a full neighbourhood of 0 (both sides are
continuous at 0; the point value comes from `eq_of_eventuallyEq_nhd_ne`). -/
lemma gFun_one_add_eventuallyEq :
    (fun s : ℂ => gFun (1 + s)) =ᶠ[𝓝 (0 : ℂ)]
      fun s => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s) := by
  have hp := gFun_one_add_punctured
  have hFcont : ContinuousAt (fun s : ℂ => gFun (1 + s)) 0 := by
    have hg : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)
    rw [show (1 : ℂ) = 1 + 0 from (add_zero 1).symm] at hg
    have h1 : Tendsto (fun s : ℂ => 1 + s) (𝓝 0) (𝓝 (1 + (0 : ℂ))) :=
      (continuousAt_const.add continuousAt_id).tendsto
    have hcomp : ContinuousAt (gFun ∘ fun s : ℂ => 1 + s) 0 := hg.tendsto.comp h1
    have heq : (gFun ∘ fun s : ℂ => 1 + s) = fun s : ℂ => gFun (1 + s) := rfl
    rw [heq] at hcomp
    exact hcomp
  have hG3 : ContDiffAt ℂ 1 (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 := by
    obtain ⟨hG, hpole⟩ := eventually_Gamma_ne_zero_and_pole_free
    have hev : (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) =ᶠ[𝓝 (0 : ℂ)]
        (fun s => -(Real.log Real.pi : ℂ) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2)) := by
      filter_upwards [hG, hpole] with s h1 h2
      exact logDeriv_Gammaℝ_one_add h1 h2
    have hcd0 : ContDiffAt ℂ 1 (fun s => Complex.digamma ((1 + s) / 2)) 0 := by
      have h1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=
        digamma_analyticOn _ dpsiDomain_half
      have h2 : AnalyticAt ℂ (fun s : ℂ => (1 + s) / 2) 0 :=
        (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)
      have h3 := AnalyticAt.comp_of_eq h1 h2 (by show (1 + (0 : ℂ)) / 2 = 1 / 2; ring)
      have heq : (Complex.digamma ∘ (fun s : ℂ => (1 + s) / 2)) =
          fun s => Complex.digamma ((1 + s) / 2) := rfl
      rw [heq] at h3
      exact h3.contDiffAt
    have hcd : ContDiffAt ℂ 1 (fun s : ℂ => -(Real.log Real.pi : ℂ) / 2 +
        (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=
      contDiff_const.contDiffAt.add ((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)
    exact hcd.congr_of_eventuallyEq hev
  have hGcont : ContinuousAt (fun s : ℂ =>
      1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s)) 0 := by
    have hc1 : ContinuousAt (fun s : ℂ => 1 / (1 + s)) 0 :=
      ContinuousAt.div continuousAt_const (continuousAt_const.add continuousAt_id) (by norm_num)
    have hc2 : ContinuousAt hLiExt 0 := hLiExt_analyticAt_zero.continuousAt
    have hc3 : ContinuousAt (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 :=
      hG3.continuousAt
    exact (hc1.add hc2).add hc3
  have hpt := eq_of_eventuallyEq_nhd_ne hFcont hGcont hp
  rw [eventually_nhdsWithin_iff] at hp
  filter_upwards [hp] with s hs
  by_cases h0 : s = 0
  · subst h0
    exact hpt
  · exact hs h0

/-! ## 3. The coefficient extraction at 1 -/

/-- The m-th derivative of the 1/(1+s) piece: (−1)^m·m!. -/
lemma iteratedDeriv_one_div_one_add (m : ℕ) :
    iteratedDeriv m (fun s : ℂ => 1 / (1 + s)) 0 = ((-1 : ℂ)) ^ m * (m ! : ℂ) := by
  have e : (fun s : ℂ => 1 / (1 + s)) = fun s : ℂ => (s + 1) ^ (-1 : ℤ) := by
    funext s
    rw [zpow_neg_one, one_div]
    congr 1
    ring
  rw [e, iteratedDeriv_zpow_neg_one m 1 (by norm_num : (0 : ℂ) + 1 ≠ 0), zero_add, one_zpow,
    mul_one]

/-- **The shift coefficient extraction**: gFun^{(m)}(1) =
(−1)^m·m! − m!·lcoeff m + (−1)^{m+1}·m!·a_{m+1}. -/
lemma iteratedDeriv_gFun_one (m : ℕ) :
    iteratedDeriv m gFun 1 =
      ((-1 : ℂ)) ^ m * (m ! : ℂ) - (m ! : ℂ) * lcoeff m +
        ((-1 : ℂ)) ^ (m + 1) * (m ! : ℂ) * (lagariasA (m + 1) : ℝ) := by
  have hcomp := congr_fun (iteratedDeriv_comp_add_const m gFun (1 : ℂ)) 0
  rw [zero_add] at hcomp
  rw [← hcomp]
  have e0 : (fun z : ℂ => gFun (z + 1)) = fun s : ℂ => gFun (1 + s) :=
    funext fun s => by rw [add_comm]
  rw [e0, iteratedDeriv_congr_of_eventuallyEq gFun_one_add_eventuallyEq m]
  have h1 : ContDiffAt ℂ m (fun s : ℂ => 1 / (1 + s)) 0 :=
    (analyticAt_const.div (analyticAt_const.add analyticAt_id) (by norm_num)).contDiffAt
  have h2 : ContDiffAt ℂ m hLiExt 0 := hLiExt_analyticAt_zero.contDiffAt
  have h3 : ContDiffAt ℂ m (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) 0 := by
    obtain ⟨hG, hpole⟩ := eventually_Gamma_ne_zero_and_pole_free
    have hev : (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) =ᶠ[𝓝 (0 : ℂ)]
        (fun s => -(Real.log Real.pi : ℂ) / 2 + (1 / 2) * Complex.digamma ((1 + s) / 2)) := by
      filter_upwards [hG, hpole] with s hs1 hs2
      exact logDeriv_Gammaℝ_one_add hs1 hs2
    have hcd0 : ContDiffAt ℂ m (fun s => Complex.digamma ((1 + s) / 2)) 0 := by
      have ha1 : AnalyticAt ℂ Complex.digamma ((1 : ℂ) / 2) :=
        digamma_analyticOn _ dpsiDomain_half
      have ha2 : AnalyticAt ℂ (fun s : ℂ => (1 + s) / 2) 0 :=
        (analyticAt_const.add analyticAt_id).div analyticAt_const (by norm_num)
      have ha3 := AnalyticAt.comp_of_eq ha1 ha2 (by show (1 + (0 : ℂ)) / 2 = 1 / 2; ring)
      have heq : (Complex.digamma ∘ (fun s : ℂ => (1 + s) / 2)) =
          fun s => Complex.digamma ((1 + s) / 2) := rfl
      rw [heq] at ha3
      exact ha3.contDiffAt
    have hcd : ContDiffAt ℂ m (fun s : ℂ => -(Real.log Real.pi : ℂ) / 2 +
        (1 / 2) * Complex.digamma ((1 + s) / 2)) 0 :=
      contDiff_const.contDiffAt.add ((contDiff_const (𝕜 := ℂ) (c := (1 / 2 : ℂ))).contDiffAt.mul hcd0)
    exact hcd.congr_of_eventuallyEq hev
  have hsplit1 : (fun s : ℂ => 1 / (1 + s) + hLiExt s + logDeriv Complex.Gammaℝ (1 + s)) =
      (fun s : ℂ => 1 / (1 + s) + hLiExt s) + (fun s : ℂ => logDeriv Complex.Gammaℝ (1 + s)) :=
    rfl
  have hsplit2 : (fun s : ℂ => 1 / (1 + s) + hLiExt s) =
      (fun s : ℂ => 1 / (1 + s)) + hLiExt := rfl
  have h12 : ContDiffAt ℂ m (fun s : ℂ => 1 / (1 + s) + hLiExt s) 0 := h1.add h2
  rw [hsplit1, iteratedDeriv_add h12 h3, hsplit2, iteratedDeriv_add h1 h2,
    iteratedDeriv_one_div_one_add, iteratedDeriv_hLiExt m, iteratedDeriv_logDeriv_Gammaℝ m]
  ring

/-! ## 4. The (4.10-a) assembly -/

/-- **Lagarias (4.10), a-form (D-066 §0)**: for all k ≥ 1,
lcoeff (k−1) = (−1)^k·(lagariasA k + sigmaP k) + (−1)^{k−1}.
The assembly algebra of D-066 §2 with the multiplied-out
linear_combination (the (m! : ℂ) ≠ 0 clear + the (−1)^{m+1}-square
sign relation). Perimeter: ZeroCountProp only. -/
theorem lagarias_4_10_a (hZC : ZeroCountProp) {k : ℕ} (hk : 1 ≤ k) :
    lcoeff (k - 1) =
      ((-1 : ℂ)) ^ k * ((lagariasA k : ℝ) + sigmaP k) + ((-1 : ℂ)) ^ (k - 1) := by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : k ≠ 0)
  rw [Nat.succ_eq_add_one, Nat.add_sub_cancel]
  have hF : ((m ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero m)
  have hM := sigmaP_eq_neg_iteratedDeriv_gFun_div hZC (by omega : 1 ≤ m + 1)
  rw [Nat.add_sub_cancel] at hM
  have hM2 : (m ! : ℂ) * sigmaP (m + 1) = -iteratedDeriv m gFun 0 := by
    rw [hM]
    field_simp [hF]
  have hFE := iteratedDeriv_gFun_zero m
  have hExp := iteratedDeriv_gFun_one m
  have ht_sq : ((-1 : ℂ)) ^ (m + 1) * ((-1 : ℂ)) ^ (m + 1) = 1 := by
    rw [← pow_add, show (m + 1) + (m + 1) = 2 * (m + 1) by ring, pow_mul,
      show ((-1 : ℂ)) ^ 2 = 1 by norm_num, one_pow]
  have hgoal : (m ! : ℂ) * lcoeff m =
      (m ! : ℂ) * (((-1 : ℂ)) ^ (m + 1) * ((lagariasA (m + 1) : ℝ)) +
        ((-1 : ℂ)) ^ (m + 1) * sigmaP (m + 1) + ((-1 : ℂ)) ^ m) := by
    linear_combination
      (-((-1 : ℂ)) ^ (m + 1)) * hM2 + ((-1 : ℂ)) ^ (m + 1) * hFE +
      ((-1 : ℂ)) ^ (m + 1) * ((-1 : ℂ)) ^ (m + 1) * hExp +
      (-(m ! : ℂ) * lcoeff m + ((-1 : ℂ)) ^ (m + 1) * (m ! : ℂ) * (lagariasA (m + 1) : ℝ) +
        ((-1 : ℂ)) ^ m * (m ! : ℂ)) * ht_sq
  have hgoal2 : (m ! : ℂ) * lcoeff m =
      (m ! : ℂ) * (((-1 : ℂ)) ^ (m + 1) * (((lagariasA (m + 1) : ℝ)) + sigmaP (m + 1)) +
        ((-1 : ℂ)) ^ m) := by
    linear_combination hgoal
  exact mul_left_cancel₀ hF hgoal2

/-! ## 5. The crux: Sf(n) = Res₁(n) -/

/-- **The crux identity** (D-064 §3, D-066 §5): for n ≥ 1,
ResW1 n = SInfty n + 1 − liCoeff n (as ℂ), i.e. (ResW1 n).re = Sf n.
Via ResW1_eq_sum + (4.10-a) + the two ii′-2 swaps + the binomial sum
Σ_{j=1}^n (−1)^{j−1}C(n,j) = 1. -/
theorem sf_eq_resW1 (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n) :
    (ResW1 n).re = Sf n := by
  -- the binomial sums
  have hsign : ∀ j : ℕ, 1 ≤ j → ((-1 : ℂ)) ^ (j - 1) = -((-1 : ℂ)) ^ j := by
    intro j hj
    have e : j - 1 + 1 = j := by omega
    calc ((-1 : ℂ)) ^ (j - 1) = -(((-1 : ℂ)) ^ (j - 1) * (-1 : ℂ)) := by ring
      _ = -((-1 : ℂ)) ^ (j - 1 + 1) := by rw [pow_succ]
      _ = -((-1 : ℂ)) ^ j := by rw [e]
  have hbinom : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ)) = -1 := by
    have h := add_pow (-1 : ℂ) 1 n
    rw [neg_add_cancel, zero_pow (by omega : n ≠ 0)] at h
    rw [Finset.sum_congr rfl (fun j _ => by rw [one_pow, mul_one] :
        ∀ j ∈ Finset.range (n + 1), (-1 : ℂ) ^ j * 1 ^ (n - j) * (n.choose j : ℂ) =
          (-1 : ℂ) ^ j * (n.choose j : ℂ))] at h
    rw [show Finset.range (n + 1) = insert 0 (Finset.Icc 1 n) from by
      ext j
      simp [Finset.mem_range, Finset.mem_Icc]
      omega] at h
    rw [Finset.sum_insert (show (0 : ℕ) ∉ Finset.Icc 1 n from by
      intro hmem
      rw [Finset.mem_Icc] at hmem
      omega)] at h
    rw [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at h
    linear_combination -h
  have hS3 : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ)) = 1 := by
    have e : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ)) =
        ∑ j ∈ Finset.Icc 1 n, -((-1 : ℂ) ^ j * (n.choose j : ℂ)) :=
      Finset.sum_congr rfl (fun j hj => by rw [hsign j (Finset.mem_Icc.mp hj).1, neg_mul])
    rw [e, Finset.sum_neg_distrib, hbinom, neg_neg]
  have hS : ((SInfty n : ℝ) : ℂ) =
      ∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * (lagariasA j : ℝ) := by
    have h := sInfty_eq_sum n hn
    have h2 : ((SInfty n : ℝ) : ℂ) =
        ((∑ j ∈ Finset.Icc 1 n, (-1 : ℝ) ^ j * (n.choose j : ℝ) * lagariasA j : ℝ) : ℂ) := by
      rw [h]
    push_cast at h2
    exact h2
  have hL : (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * sigmaP j) =
      -liCoeff n := by
    rw [liCoeff_eq_sum_sigma, ← Finset.sum_neg_distrib]
    apply Finset.sum_congr rfl
    intro j _
    ring
  -- the ℂ identity
  have hid : ResW1 n = ((SInfty n : ℝ) : ℂ) + 1 - liCoeff n := by
    rw [ResW1_eq_sum]
    have hterms : (∑ j ∈ Finset.Icc 1 n, (n.choose j : ℂ) * lcoeff (j - 1)) =
        (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * (lagariasA j : ℝ)) +
          ((∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ j * (n.choose j : ℂ) * sigmaP j) +
            (∑ j ∈ Finset.Icc 1 n, (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ))) := by
      rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
      apply Finset.sum_congr rfl
      intro j hj
      have hj1 : 1 ≤ j := (Finset.mem_Icc.mp hj).1
      rw [lagarias_4_10_a hZC hj1]
      show (n.choose j : ℂ) * ((-1 : ℂ) ^ j * ((lagariasA j : ℝ) + sigmaP j) + (-1 : ℂ) ^ (j - 1)) =
        (-1 : ℂ) ^ j * (n.choose j : ℂ) * (lagariasA j : ℝ) +
          ((-1 : ℂ) ^ j * (n.choose j : ℂ) * sigmaP j + (-1 : ℂ) ^ (j - 1) * (n.choose j : ℂ))
      ring
    rw [hterms, ← hS, hL, hS3]
    ring
  rw [hid, Sf]
  simp only [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.one_re]

end NguyenRH1