LiContour.lean

Declarations

Source

/-
NguyenRH1/LiContour.lean — tier ii′ sub-stage ii′-4 (D-064 §5 graph L3+L1,
D-036 §2–3): the zero-avoiding ordinate T (pigeonhole on the perimeter
unit-window count bound) and the Lagarias-kernel norm bounds.

L3 (D-036 §2): in a unit ordinate window [a, a+1] (a ≥ 2) with at most
Ĉ₀(a+1) zero ordinates, one of the k+1 equally spaced midpoints
T_j = a + (2j+1)/(2(k+1)) has distance ≥ 1/(2(k+1)) ≥ 1/(3·Ĉ₀(a+1)) from
every zero ordinate in the window (each zero lies within < 1/(2(k+1)) of
at most one midpoint — adjacent midpoints are 1/(k+1) apart — so at most
k of the k+1 midpoints are blocked). The count input is the perimeter
hypothesis `ZeroCountProp` (Trudgian 2014 N(T)/S(T), D-062 §4; Ĉ₀ =
`C0hat` is D-056 §2's majorant, already in LiSkeleton). [Session-035
erratum: ZeroCountProp strengthened to the mult-weighted form — see the
def's docstring; `one_le_zeroMult` gives card ≤ Σ mult.]

L1 (D-036 §3): the kernel kFun n s = (s/(s−1))ⁿ − 1 satisfies
  * ‖kFun n s‖ ≤ 2                     (re s ≤ 1/2: here |s/(s−1)| ≤ 1)
  * ‖kFun n (s+1)‖ ≤ e⁴ + 1            (re s ≤ 3, n ≤ (im s)²: the
    horizontals, |1+1/s| ≤ 1 + (σ+1)/(σ²+T²) ≤ 1 + 4/n)
  * ‖kFun n (s+1)‖ ≤ e^{√n/2} + 1      (2√n ≤ re s: the right vertical,
    |1+1/s| ≤ 1 + 1/|s| ≤ 1 + 1/(2√n))
  * kFun n (−2) = (2/3)ⁿ − 1, hence ‖kFun n (−2)‖ ≤ 1 (trivial-zero term).

Also the deferred trivial-zero simplicity (ii′-1b(iii) NOTE): zeroMult(−2) = 1,
via ζ(s) = (s+2)·G(s) near −2 with G(s) = Λ(s)/H(s),
H(s) = 4·π^{−s/2}·Γ(s/2+2)/s (= (s+2)·ΓR(s) off s ∈ {−2, 0}), H(−2) = −2π ≠ 0,
Λ(−2) = Λ(3) = ΓR(3)·ζ(3) ≠ 0.

Archive references: D-036 §2–3, D-056 §2, D-064 §5 (L3/L1), D-066 §6.
-/
import Mathlib
import Zeta23.Statement
import Zeta23.RvM.CountByIntegral
import NguyenRH1.LiSides
import NguyenRH1.LiSkeleton

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The unit ordinate window and the perimeter count hypothesis -/

/-- The nontrivial zeros with ordinate in the unit window [a, a+1]. -/
def zeroWindow (a : ℝ) : Set ℂ :=
  {ρ | IsNontrivialZero ρ ∧ a ≤ ρ.im ∧ ρ.im ≤ a + 1}

/-- Finiteness of the unit ordinate window (via Zeta23 `zerosIn_finite`). -/
theorem zeroWindow_finite (a : ℝ) : (zeroWindow a).Finite := by
  apply Set.Finite.subset (zerosIn_finite (a - 1) (a + 1))
  intro ρ hρ
  refine ⟨hρ.1, ?_, hρ.2.2⟩
  linarith [hρ.2.1]

/-- A nontrivial zero has multiplicity ≥ 1 (zeroMult is the analytic
order). Bridges the mult-weighted perimeter count to the plain window
cardinality (card ≤ Σ mult). -/
theorem one_le_zeroMult {ρ : ℂ} (hρ : IsNontrivialZero ρ) : 1 ≤ zeroMult ρ := by
  have hρ1 : ρ ≠ 1 := by
    rintro rfl
    have h := hρ.2.2
    rw [Complex.one_re] at h
    exact (lt_irrefl (1 : ℝ)) h
  have htop := zeta_order_ne_top_of_ne hρ1
  have hne : analyticOrderAt riemannZeta ρ ≠ 0 :=
    (analyticAt_riemannZeta hρ1).analyticOrderAt_ne_zero.mpr hρ.1
  exact ENat.toNat_pos hne htop

/-- [PERIMETER — Trudgian 2014 N(T)/S(T), D-062 §4] The unit-window
zero-count bound: the multiplicity-weighted count of nontrivial zeros
with ordinates in [t, t+1] is at most Ĉ₀(t+1) (t ≥ 2). Declared
counting input for the L3 pigeonhole and the tight R-bound; Ĉ₀ =
`C0hat` is D-056 §2's honest majorant (LiSkeleton).
[Erratum 2026-08-23 (session 035): strengthened from the unweighted
set-card form `(Nat.card (zeroWindow t) : ℝ) ≤ Ĉ₀(t+1)` to the
mult-weighted form — Trudgian's N(T) counts zeros with multiplicity,
and the mult-weighted form is what the 5f/ii′-6 near sums
(zeroMult-weighted, from `seriesFun`) consume; the set-card encoding
under-captured the declared source (a second ii′-1a-class encoding
defect, found at the point of consumption). The set-card bound follows
from this form via `one_le_zeroMult` (card ≤ Σ mult); the two
consumers (exists_zero_avoiding_T, exists_gapCircle_radius) adapted.] -/
def ZeroCountProp : Prop :=
  ∀ t : ℝ, 2 ≤ t →
    (((zeroWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤ C0hat (t + 1)

/-- The two-unit ordinate window: nontrivial zeros with |γ − t| ≤ 1. -/
def zeroAbsWindow (t : ℝ) : Set ℂ :=
  {ρ | IsNontrivialZero ρ ∧ |ρ.im - t| ≤ 1}

/-- Finiteness of the two-unit ordinate window (via Zeta23
`zerosIn_finite`). -/
theorem zeroAbsWindow_finite (t : ℝ) : (zeroAbsWindow t).Finite := by
  apply Set.Finite.subset (zerosIn_finite (t - 2) (t + 1))
  intro ρ hρ
  refine ⟨hρ.1, ?_, ?_⟩
  · have := hρ.2; linarith [abs_le.mp this]
  · have := hρ.2; linarith [abs_le.mp this]

/-- [PERIMETER — Trudgian 2014 N(T)/S(T), the two-unit specialization,
D-069 §2] The two-unit window count: the multiplicity-weighted count of
nontrivial zeros with |γ − t| ≤ 1 is at most 0.6·log(t+2) +
0.886·log log(t+2) + 2.7 (t ≥ 10). This is N(t+1) − N(t−1) bounded by
the F-difference + S_b-pair: F(t+1)−F(t−1) ≤ (1/π)·log((t+1)/2π) ≤
0.31831·log(t+2) − 0.585 and S_b(t+1)+S_b(t−1) ≤ 0.274·log(t+2) +
0.886·log log(t+2) + 3.176, totaling 0.59231·log(t+2) +
0.886·log log(t+2) + 2.591 — the closed form has 0.008·log(t+2) + 0.11
slack. NOT derivable from the per-unit `ZeroCountProp` (the crude double
2·Ĉ₀ has log-coefficient 0.866 > 0.6); declared under the same
Trudgian-2014 source (D-062 §4 class). [Added session 035 — 5f's piece 2
consumes exactly this form; D-069 Finding 1.] -/
def ZeroCountProp2 : Prop :=
  ∀ t : ℝ, 10 ≤ t →
    (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤
      0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7

/-- [PERIMETER — Platt-class zero-location certificate, D-069 §2] There
are no nontrivial zeros with |γ| ≤ 14: the first nontrivial zero is at
γ = 14.134725…. This is the zero-LOCATION content of the
Platt–Trudgian-class Turing-method certificate (the same computation
that verifies RH to height 3×10¹² locates the zeros); it is not implied
by `RHUpTo` (an on-line statement) nor by the Trudgian count bounds
(the S_b slack is too large at low height). Declared in the
Platt–Trudgian trust class. [Added session 035 — 5f's piece 3
(far-difference sum) consumes this for the intervals below height 14;
D-069 Finding/need (P2).] -/
def NoLowZeros : Prop :=
  ∀ ρ : ℂ, IsNontrivialZero ρ → 14 ≤ |ρ.im|

/-- The global ordinate window: nontrivial zeros with 0 < γ ≤ T. -/
def zeroGlobalWindow (T : ℝ) : Set ℂ :=
  {ρ | IsNontrivialZero ρ ∧ 0 < ρ.im ∧ ρ.im ≤ T}

/-- Finiteness of the global ordinate window (via Zeta23
`zerosIn_finite`). -/
theorem zeroGlobalWindow_finite (T : ℝ) : (zeroGlobalWindow T).Finite := by
  apply Set.Finite.subset (zerosIn_finite 0 T)
  intro ρ hρ
  refine ⟨hρ.1, by linarith [hρ.2.1], hρ.2.2⟩

/-- [PERIMETER — Trudgian 2014 N(T) GLOBAL form, D-062 §4 / D-071 §3,
user-approved session 038] The global zero-count bound: the
multiplicity-weighted count of nontrivial zeros with 0 < γ ≤ T is at
most FAlt T (T ≥ 2). This is the un-specialized form of the declared
Trudgian source (`ZeroCountProp` is its unit-window corollary); the
unit form does NOT imply the global form at the FAlt level (summing
unit windows gives 0.433·T·log T > (1/2π)·T·log T). Used by the ii′-6
bridge (the both-signs count is 2× the one-sign count by conj
symmetry, `isNontrivialZero_conj` + `zeroMult_conj`). -/
def ZeroCountGlobalProp : Prop :=
  ∀ T : ℝ, 2 ≤ T →
    (((zeroGlobalWindow_finite T).toFinset.sum fun ρ => zeroMult ρ) : ℝ) ≤ FAlt T

/-- [PERIMETER — M₀ interval certificate, D-062 §4 L6 / D-071 §3,
user-approved session 038] ‖ζ′/ζ(−5/2 + it)‖ ≤ 1.3352 for |t| ≤ 10
(E-023 grid + sampled-Lipschitz ×2 safety; E-023b acb box-cover upgrade
optional). The same trust class as the Platt–Trudgian certificate
(interval-arithmetic computation). Used by the I_III short piece
(|t| ≤ 10 of the left vertical). -/
def MZeroProp : Prop :=
  ∀ t : ℝ, |t| ≤ 10 →
    ‖logDeriv riemannZeta ((-5 / 2 : ℂ) + (t : ℝ) * Complex.I)‖ ≤ 1.3352

/-- Ĉ₀(t) ≥ 2 for t ≥ 1 (indeed ≥ 3.33: log(t+2) ≥ 1 as t + 2 ≥ 3 > e,
so log log(t+2) ≥ 0 and the constant 2.9 remains). -/
theorem two_le_C0hat {t : ℝ} (ht : 1 ≤ t) : 2 ≤ C0hat t := by
  have h3 : (3 : ℝ) ≤ t + 2 := by linarith
  have hlog : 1 ≤ Real.log (t + 2) := by
    rw [Real.le_log_iff_exp_le (by positivity : (0:ℝ) < t + 2)]
    have he := Real.exp_one_lt_d9.le
    linarith
  have hloglog : 0 ≤ Real.log (Real.log (t + 2)) := Real.log_nonneg hlog
  have h1 : (0:ℝ) ≤ 0.433 * Real.log (t + 2) := by positivity
  have h2 : (0:ℝ) ≤ 0.886 * Real.log (Real.log (t + 2)) := by positivity
  unfold C0hat
  linarith

/-! ## 2. The midpoint pigeonhole (pure combinatorics) -/

/-- **Midpoint pigeonhole**: a finset S of reals with card S ≤ k admits one
of the k+1 midpoints a + (2j+1)/(2(k+1)) (j < k+1) at distance
≥ 1/(2(k+1)) from every point of S. (Each x ∈ S lies within < 1/(2(k+1))
of at most one midpoint — adjacent midpoints are 1/(k+1) apart — so at
most card S ≤ k of the k+1 midpoints are blocked.) -/
theorem exists_avoiding_midpoint {k : ℕ} (a : ℝ) (S : Finset ℝ)
    (hcard : S.card ≤ k) :
    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧
      ∀ x ∈ S, 1 / (2 * ((k : ℝ) + 1)) ≤ |x - T| := by
  classical
  set w : ℝ := 1 / (2 * ((k : ℝ) + 1)) with hw_def
  have hk1 : (0:ℝ) < 2 * ((k : ℝ) + 1) := by positivity
  have hw : 0 < w := one_div_pos.mpr hk1
  set c : ℕ → ℝ := fun j => a + (2 * (j : ℝ) + 1) * w with hc_def
  -- candidate spread: c i − c j = 2(i − j)·w
  have hcd : ∀ i j : ℕ, c i - c j = 2 * ((i : ℝ) - (j : ℝ)) * w := fun i j => by
    simp only [hc_def]; ring
  -- each candidate lies in [a, a+1]
  have hc_mem : ∀ j < k + 1, a ≤ c j ∧ c j ≤ a + 1 := by
    intro j hj
    have hjl : (0:ℝ) ≤ 2 * (j : ℝ) + 1 := by positivity
    have hju : 2 * (j : ℝ) + 1 ≤ 2 * ((k : ℝ) + 1) := by
      have hjk : j ≤ k := Nat.lt_succ_iff.mp hj
      have : (j : ℝ) ≤ k := by exact_mod_cast hjk
      linarith
    have h1 : (0:ℝ) ≤ (2 * (j : ℝ) + 1) * w := mul_nonneg hjl hw.le
    have h2 : (2 * (j : ℝ) + 1) * w ≤ 1 := by
      rw [hw_def, mul_one_div, div_le_one hk1]
      exact hju
    constructor <;> simp only [hc_def] <;> linarith
  -- the bad candidates: those within < w of some point of S
  set Bad : Finset ℕ := (Finset.range (k + 1)).filter
    (fun j => ∃ x ∈ S, |x - c j| < w) with hBad_def
  have hbad_wit : ∀ j ∈ Bad, ∃ x ∈ S, |x - c j| < w := fun j hj =>
    (Finset.mem_filter.mp hj).2
  choose! f hfS hfw using hbad_wit
  -- distinct bad candidates need distinct witnesses: f is injective on Bad
  have hinj : Set.InjOn f Bad := by
    intro i hi j hj hij
    by_contra hne
    have h1 : |f i - c i| < w := hfw i hi
    have h2 : |f j - c j| < w := hfw j hj
    have hlt : |c i - c j| < 2 * w := by
      have h3 : |c i - c j| ≤ |c i - f i| + |f i - c j| :=
        abs_sub_le (c i) (f i) (c j)
      rw [abs_sub_comm (c i) (f i)] at h3
      rw [hij] at h1 h3
      linarith
    rw [hcd i j] at hlt
    have hne1 : (1:ℝ) ≤ |(i : ℝ) - (j : ℝ)| := by
      rcases lt_or_gt_of_ne hne with h | h
      · have h4 : (i : ℝ) + 1 ≤ j := by
          exact_mod_cast Nat.add_one_le_of_lt h
        rw [abs_of_nonpos (by linarith)]
        linarith
      · have h4 : (j : ℝ) + 1 ≤ i := by
          exact_mod_cast Nat.add_one_le_of_lt h
        rw [abs_of_nonneg (by linarith)]
        linarith
    have hge : 2 * w ≤ |2 * ((i : ℝ) - (j : ℝ)) * w| := by
      rw [abs_mul, abs_mul, abs_of_pos hw, abs_of_pos (by norm_num : (0:ℝ) < 2)]
      nlinarith [hne1, hw]
    linarith
  have hcardBad : Bad.card ≤ S.card :=
    Finset.card_le_card_of_injOn f (fun j hj => hfS j hj) hinj
  -- some candidate is not bad
  have hlt2 : Bad.card < (Finset.range (k + 1)).card := by
    rw [Finset.card_range]
    exact Nat.lt_succ_of_le (hcardBad.trans hcard)
  obtain ⟨j, hj, hjB⟩ : ∃ j ∈ Finset.range (k + 1), j ∉ Bad := by
    by_contra hcon
    push Not at hcon
    have hsub : Finset.range (k + 1) ⊆ Bad := fun x hx => hcon x hx
    have := Finset.card_le_card hsub
    omega
  have hjk : j < k + 1 := Finset.mem_range.mp hj
  refine ⟨c j, (hc_mem j hjk).1, (hc_mem j hjk).2, fun x hx => ?_⟩
  have hnot : ¬ |x - c j| < w := by
    intro hlt
    exact hjB (Finset.mem_filter.mpr ⟨hj, ⟨x, hx, hlt⟩⟩)
  have : w ≤ |x - c j| := not_lt.mp hnot
  rwa [hw_def] at this

/-! ## 3. L3: the zero-avoiding ordinate -/

/-- **L3** (D-036 §2): given the perimeter count bound `ZeroCountProp`,
every unit window [a, a+1] with a ≥ 2 contains an ordinate T at distance
≥ 1/(3·Ĉ₀(a+1)) from every zero ordinate in the window. -/
theorem exists_zero_avoiding_T (hZC : ZeroCountProp) {a : ℝ} (ha : 2 ≤ a) :
    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧
      ∀ ρ : ℂ, IsNontrivialZero ρ → a ≤ ρ.im → ρ.im ≤ a + 1 →
        1 / (3 * C0hat (a + 1)) ≤ |ρ.im - T| := by
  classical
  have hfin := zeroWindow_finite a
  set WF : Finset ℂ := hfin.toFinset with hWF_def
  have hWFmem : ∀ ρ : ℂ, ρ ∈ WF ↔ ρ ∈ zeroWindow a :=
    fun ρ => Set.Finite.mem_toFinset hfin
  set S : Finset ℝ := WF.image Complex.im with hS_def
  have hScard : S.card ≤ WF.card := Finset.card_image_le
  have hWFcard : (WF.card : ℝ) ≤ C0hat (a + 1) := by
    have h1 := hZC a ha
    -- h1 : (∑ ρ ∈ WF, (zeroMult ρ : ℝ)) ≤ C0hat (a + 1); card ≤ Σ mult
    have h2 : (WF.card : ℝ) ≤ ∑ ρ ∈ WF, (zeroMult ρ : ℝ) := by
      rw [show (WF.card : ℝ) = ∑ _ρ ∈ WF, (1 : ℝ) by simp]
      apply Finset.sum_le_sum
      intro ρ hρ
      exact_mod_cast one_le_zeroMult ((hWFmem ρ).mp hρ).1
    exact h2.trans h1
  obtain ⟨T, hT1, hT2, hT3⟩ := exists_avoiding_midpoint a S hScard
  refine ⟨T, hT1, hT2, fun ρ hρ hρa hρa1 => ?_⟩
  have hρmem : ρ ∈ WF := (hWFmem ρ).mpr ⟨hρ, hρa, hρa1⟩
  have himmem : ρ.im ∈ S := Finset.mem_image.mpr ⟨ρ, hρmem, rfl⟩
  have h1 := hT3 ρ.im himmem
  have hC : 2 ≤ C0hat (a + 1) := two_le_C0hat (by linarith)
  have hpos : (0:ℝ) < 2 * ((WF.card : ℝ) + 1) := by positivity
  have hle : 2 * ((WF.card : ℝ) + 1) ≤ 3 * C0hat (a + 1) := by
    linarith [hWFcard]
  exact le_trans (one_div_le_one_div_of_le hpos hle) h1

/-! ## 3b. The wide zero-avoiding ordinate (D-071 Finding-2 repair) -/

/-- The wide ordinate window: nontrivial zeros with ordinate in
[a−1, a+2] (the 3-unit window for the Finding-2-extended pigeonhole —
zeros just outside [a, a+1] can sit at distance < 1/(3Ĉ₀) from T). -/
def zeroWindowWide (a : ℝ) : Set ℂ :=
  {ρ | IsNontrivialZero ρ ∧ a - 1 ≤ ρ.im ∧ ρ.im ≤ a + 2}

/-- Finiteness of the wide window (union of the three unit windows). -/
theorem zeroWindowWide_finite (a : ℝ) : (zeroWindowWide a).Finite := by
  apply Set.Finite.subset ((zeroWindow_finite (a - 1)).union
    ((zeroWindow_finite a).union (zeroWindow_finite (a + 1))))
  intro ρ hρ
  obtain ⟨hz, hlo, hhi⟩ := hρ
  by_cases h1 : ρ.im ≤ a
  · exact Or.inl ⟨hz, hlo, by linarith⟩
  · by_cases h2 : ρ.im ≤ a + 1
    · exact Or.inr (Or.inl ⟨hz, by linarith, h2⟩)
    · exact Or.inr (Or.inr ⟨hz, by linarith, by linarith⟩)

/-- The wide window's cardinality ≤ 3·Ĉ₀(a+2) (three unit windows via
the perimeter + `C0hat_mono`). -/
theorem zeroWindowWide_card_le (hZC : ZeroCountProp) {a : ℝ} (ha : 3 ≤ a) :
    ((zeroWindowWide_finite a).toFinset.card : ℝ) ≤ 3 * C0hat (a + 2) := by
  have hsub : (zeroWindowWide_finite a).toFinset ⊆
      (zeroWindow_finite (a - 1)).toFinset ∪
        ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset) := by
    intro ρ hρ
    have hmem : ρ ∈ zeroWindowWide a := (zeroWindowWide_finite a).mem_toFinset.mp hρ
    obtain ⟨hz, hlo, hhi⟩ := hmem
    by_cases h1 : ρ.im ≤ a
    · exact Finset.mem_union.mpr (Or.inl
        ((zeroWindow_finite (a - 1)).mem_toFinset.mpr ⟨hz, hlo, by linarith⟩))
    · by_cases h2 : ρ.im ≤ a + 1
      · exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inl
          ((zeroWindow_finite a).mem_toFinset.mpr ⟨hz, by linarith, h2⟩))))
      · exact Finset.mem_union.mpr (Or.inr (Finset.mem_union.mpr (Or.inr
          ((zeroWindow_finite (a + 1)).mem_toFinset.mpr ⟨hz, by linarith, by linarith⟩))))
  have hsum1 : (∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ)) ≤
      ∑ ρ ∈ ((zeroWindow_finite (a - 1)).toFinset ∪
        ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)),
        (zeroMult ρ : ℝ) :=
    Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ _ => Nat.cast_nonneg _)
  have hsum2 : (∑ ρ ∈ ((zeroWindow_finite (a - 1)).toFinset ∪
        ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)),
        (zeroMult ρ : ℝ)) ≤
      (∑ ρ ∈ (zeroWindow_finite (a - 1)).toFinset, (zeroMult ρ : ℝ)) +
        ((∑ ρ ∈ (zeroWindow_finite a).toFinset, (zeroMult ρ : ℝ)) +
          (∑ ρ ∈ (zeroWindow_finite (a + 1)).toFinset, (zeroMult ρ : ℝ))) := by
    have hu1 := Finset.sum_union_inter (s₁ := (zeroWindow_finite (a - 1)).toFinset)
      (s₂ := (zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset)
      (f := fun ρ => (zeroMult ρ : ℝ))
    have hnn : (0 : ℝ) ≤ ∑ ρ ∈ (zeroWindow_finite (a - 1)).toFinset ∩
        ((zeroWindow_finite a).toFinset ∪ (zeroWindow_finite (a + 1)).toFinset),
        (zeroMult ρ : ℝ) :=
      Finset.sum_nonneg (fun ρ _ => Nat.cast_nonneg _)
    have hu2 := Finset.sum_union_inter (s₁ := (zeroWindow_finite a).toFinset)
      (s₂ := (zeroWindow_finite (a + 1)).toFinset) (f := fun ρ => (zeroMult ρ : ℝ))
    have hnn2 : (0 : ℝ) ≤ ∑ ρ ∈ (zeroWindow_finite a).toFinset ∩
        (zeroWindow_finite (a + 1)).toFinset, (zeroMult ρ : ℝ) :=
      Finset.sum_nonneg (fun ρ _ => Nat.cast_nonneg _)
    linarith
  have h1 : (∑ ρ ∈ (zeroWindow_finite (a - 1)).toFinset, (zeroMult ρ : ℝ)) ≤
      C0hat a := by
    have h := hZC (a - 1) (by linarith)
    rwa [show a - 1 + 1 = a from by ring] at h
  have h2 := hZC a (by linarith)
  have h3 : (∑ ρ ∈ (zeroWindow_finite (a + 1)).toFinset, (zeroMult ρ : ℝ)) ≤
      C0hat (a + 2) := by
    have h := hZC (a + 1) (by linarith)
    rwa [show a + 1 + 1 = a + 2 from by ring] at h
  have hlog1 : Real.log (a + 2) ≤ Real.log (a + 2 + 2) :=
    Real.log_le_log (by positivity) (by linarith)
  have hlog2 : Real.log (Real.log (a + 2)) ≤ Real.log (Real.log (a + 2 + 2)) :=
    Real.log_le_log (Real.log_pos (by linarith)) hlog1
  have hmono1 : C0hat a ≤ C0hat (a + 2) := by
    unfold C0hat
    linarith [hlog1, hlog2]
  have hmono2 : C0hat (a + 1) ≤ C0hat (a + 2) := by
    unfold C0hat
    have h1' : Real.log (a + 1 + 2) ≤ Real.log (a + 2 + 2) :=
      Real.log_le_log (by positivity) (by linarith)
    have h2' : Real.log (Real.log (a + 1 + 2)) ≤ Real.log (Real.log (a + 2 + 2)) :=
      Real.log_le_log (Real.log_pos (by linarith)) h1'
    linarith [h1', h2']
  have hcard_le_sum : ((zeroWindowWide_finite a).toFinset.card : ℝ) ≤
      ∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ) := by
    rw [show ((zeroWindowWide_finite a).toFinset.card : ℝ) =
      ∑ _ρ ∈ (zeroWindowWide_finite a).toFinset, (1 : ℝ) by simp]
    apply Finset.sum_le_sum
    intro ρ hρ
    exact_mod_cast one_le_zeroMult (((zeroWindowWide_finite a).mem_toFinset.mp hρ).1)
  calc ((zeroWindowWide_finite a).toFinset.card : ℝ)
      ≤ ∑ ρ ∈ (zeroWindowWide_finite a).toFinset, (zeroMult ρ : ℝ) := hcard_le_sum
    _ ≤ C0hat a + C0hat (a + 1) + C0hat (a + 2) := by linarith [hsum1, hsum2, h1, h2, h3]
    _ ≤ 3 * C0hat (a + 2) := by linarith [hmono1, hmono2]

/-- **L3-wide** (D-071 Finding-2 repair): given the perimeter count
bound, every unit window [a, a+1] with a ≥ 3 contains an ordinate T at
distance ≥ 1/(9·Ĉ₀(a+2)) from EVERY zero ordinate in the 3-unit window
(a−1, a+2) — covering the zeros just outside [a, a+1] that the plain
L3 clearance misses. -/
theorem exists_zero_avoiding_T_wide (hZC : ZeroCountProp) {a : ℝ} (ha : 3 ≤ a) :
    ∃ T : ℝ, a ≤ T ∧ T ≤ a + 1 ∧
      ∀ ρ : ℂ, IsNontrivialZero ρ → a - 1 < ρ.im → ρ.im < a + 2 →
        1 / (9 * C0hat (a + 2)) ≤ |ρ.im - T| := by
  classical
  have hfin := zeroWindowWide_finite a
  set WF : Finset ℂ := hfin.toFinset with hWF_def
  have hWFmem : ∀ ρ : ℂ, ρ ∈ WF ↔ ρ ∈ zeroWindowWide a :=
    fun ρ => Set.Finite.mem_toFinset hfin
  set S : Finset ℝ := WF.image Complex.im with hS_def
  have hScard : S.card ≤ WF.card := Finset.card_image_le
  have hWFcard : (WF.card : ℝ) ≤ 3 * C0hat (a + 2) := zeroWindowWide_card_le hZC ha
  obtain ⟨T, hT1, hT2, hT3⟩ := exists_avoiding_midpoint a S hScard
  refine ⟨T, hT1, hT2, fun ρ hρ hρlo hρhi => ?_⟩
  have hρmem : ρ ∈ WF := (hWFmem ρ).mpr ⟨hρ, by linarith, by linarith⟩
  have himmem : ρ.im ∈ S := Finset.mem_image.mpr ⟨ρ, hρmem, rfl⟩
  have h1 := hT3 ρ.im himmem
  have hC : 2 ≤ C0hat (a + 2) := two_le_C0hat (by linarith)
  have hpos : (0:ℝ) < 2 * ((WF.card : ℝ) + 1) := by positivity
  have hle : 2 * ((WF.card : ℝ) + 1) ≤ 9 * C0hat (a + 2) := by
    linarith [hWFcard, hC]
  exact le_trans (one_div_le_one_div_of_le hpos hle) h1

/-! ## 4. L1: kernel norm bounds (D-036 §3) -/

/-- On re s ≤ 1/2 the ratio satisfies ‖s/(s−1)‖ ≤ 1 (i.e. ‖s‖ ≤ ‖s−1‖:
re s ≤ 1/2 ⟺ 0 ≤ 1 − 2·re s ⟺ re s² + im s² ≤ (re s − 1)² + im s²). -/
theorem norm_div_sub_one_le_one {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖s / (s - 1)‖ ≤ 1 := by
  have hs1 : s ≠ 1 := by
    rintro h
    rw [h] at hs
    simp only [Complex.one_re] at hs
    norm_num at hs
  have hnorm : ‖s‖ ≤ ‖s - 1‖ := by
    have h : ‖s‖ ^ 2 ≤ ‖s - 1‖ ^ 2 := by
      rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]
      rw [Complex.normSq_apply s, Complex.normSq_apply (s - 1)]
      simp only [sub_re, one_re, sub_im, one_im, sub_zero]
      nlinarith [hs]
    exact (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h
  have hpos : (0:ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)
  rw [norm_div]
  exact (div_le_one hpos).mpr hnorm

/-- **L1 (left side)**: ‖kFun n s‖ ≤ 2 for re s ≤ 1/2 (D-036 §3 (III)). -/
theorem kFun_norm_le_two {n : ℕ} {s : ℂ} (hs : s.re ≤ 1 / 2) : ‖kFun n s‖ ≤ 2 := by
  have h1 := norm_div_sub_one_le_one hs
  have h2 : ‖(s / (s - 1)) ^ n‖ ≤ 1 := by
    rw [norm_pow]
    exact pow_le_one₀ (norm_nonneg _) h1
  calc ‖kFun n s‖ = ‖(s / (s - 1)) ^ n - 1‖ := rfl
    _ ≤ ‖(s / (s - 1)) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _
    _ ≤ 1 + 1 := by rw [norm_one]; linarith [h2]
    _ = 2 := by norm_num

/-- kFun at the shifted point: kFun n (s+1) = (1 + 1/s)ⁿ − 1 (s ≠ 0). -/
theorem kFun_add_one {n : ℕ} {s : ℂ} (hs : s ≠ 0) :
    kFun n (s + 1) = (1 + 1 / s) ^ n - 1 := by
  have e : (s + 1) / (s + 1 - 1) = 1 + 1 / s := by
    rw [show s + 1 - 1 = s by ring]
    field_simp
  unfold kFun
  rw [e]

/-- The horizontal core estimate: ‖1 + 1/s‖ ≤ 1 + (re s + 1)/normSq s.
From ‖1+1/s‖² = 1 + (2σ+1)/D ≤ (1+(σ+1)/D)² with D = normSq s = σ² + T². -/
theorem norm_one_add_one_div_le {s : ℂ} (hs : s ≠ 0) :
    ‖1 + 1 / s‖ ≤ 1 + (s.re + 1) / Complex.normSq s := by
  set D := Complex.normSq s with hD_def
  have hD : (0:ℝ) < D := Complex.normSq_pos.mpr hs
  have hD_rel : D = s.re * s.re + s.im * s.im := by rw [hD_def, Complex.normSq_apply s]
  have h1 : (1 + 1 / s).re = 1 + s.re / D := by
    simp [Complex.add_re, Complex.one_re, hD_def]
  have h2 : (1 + 1 / s).im = -s.im / D := by
    simp [Complex.add_im, Complex.one_im, hD_def]
  have hsq : Complex.normSq (1 + 1 / s) = 1 + (2 * s.re + 1) / D := by
    rw [Complex.normSq_apply (1 + 1 / s), h1, h2]
    field_simp [hD.ne']
    nlinarith [hD_rel]
  have hRHS : (0:ℝ) ≤ 1 + (s.re + 1) / D := by
    have hsum : (0:ℝ) < D + (s.re + 1) := by
      nlinarith [sq_nonneg (s.re + 1 / 2), sq_nonneg s.im, hD_rel]
    have e : 1 + (s.re + 1) / D = (D + (s.re + 1)) / D := by field_simp [hD.ne']
    rw [e]
    exact div_nonneg hsum.le hD.le
  have hcmp : ‖1 + 1 / s‖ ^ 2 ≤ (1 + (s.re + 1) / D) ^ 2 := by
    rw [← Complex.normSq_eq_norm_sq, hsq]
    have e : (1 + (s.re + 1) / D) ^ 2
        = 1 + (2 * s.re + 1) / D + (1 / D + ((s.re + 1) / D) ^ 2) := by
      field_simp [hD.ne']
      ring
    rw [e]
    have hpos : (0:ℝ) ≤ 1 / D + ((s.re + 1) / D) ^ 2 := by positivity
    linarith
  exact (sq_le_sq₀ (norm_nonneg _) hRHS).mp hcmp

/-- **L1 (horizontals)**: ‖kFun n (s+1)‖ ≤ e⁴ + 1 for re s ≤ 3 and
n ≤ (im s)² (D-036 §3 (II),(IV)): then |1+1/s| ≤ 1 + 4/n, and
(1 + 4/n)ⁿ ≤ (e^{4/n})ⁿ = e⁴. -/
theorem kFun_shift_norm_le_exp_four_add_one {n : ℕ} {s : ℂ}
    (hσ : s.re ≤ 3) (hT : (n : ℝ) ≤ s.im ^ 2) :
    ‖kFun n (s + 1)‖ ≤ Real.exp 4 + 1 := by
  rcases Nat.eq_zero_or_pos n with hn | hn
  · subst hn
    simp only [kFun, pow_zero, sub_self, norm_zero]
    positivity
  · have hnR : (1:ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have hTim : 0 < s.im ^ 2 := by nlinarith [hT, hnR]
    have hs0 : s ≠ 0 := by
      rintro h
      rw [h, Complex.zero_im] at hTim
      norm_num at hTim
    have hD : (0:ℝ) < Complex.normSq s := Complex.normSq_pos.mpr hs0
    have hDn : (n:ℝ) ≤ Complex.normSq s := by
      rw [Complex.normSq_apply s]
      nlinarith [hT, sq_nonneg s.re]
    have hle : ‖1 + 1 / s‖ ≤ 1 + 4 / (n : ℝ) := by
      refine (norm_one_add_one_div_le hs0).trans ?_
      have hσ4 : s.re + 1 ≤ 4 := by linarith
      have h4 : (s.re + 1) / Complex.normSq s ≤ 4 / (n : ℝ) := by
        by_cases hσp : 0 ≤ s.re + 1
        · calc (s.re + 1) / Complex.normSq s ≤ 4 / Complex.normSq s :=
              (div_le_div_iff_of_pos_right hD).mpr hσ4
            _ ≤ 4 / (n : ℝ) :=
              (div_le_div_iff_of_pos_left (by norm_num) hD (by positivity)).mpr hDn
        · have hneg : (s.re + 1) / Complex.normSq s ≤ 0 :=
            div_nonpos_of_nonpos_of_nonneg (not_le.mp hσp).le hD.le
          have hpos4 : (0:ℝ) ≤ 4 / (n : ℝ) := by positivity
          linarith
      linarith [h4]
    have hpow : ‖1 + 1 / s‖ ^ n ≤ Real.exp 4 := by
      calc ‖1 + 1 / s‖ ^ n ≤ (1 + 4 / (n : ℝ)) ^ n :=
            pow_le_pow_left₀ (norm_nonneg _) hle n
        _ ≤ (Real.exp (4 / (n : ℝ))) ^ n := by
            have h := Real.add_one_le_exp (4 / (n : ℝ))
            exact pow_le_pow_left₀ (by positivity) (by linarith) n
        _ = Real.exp 4 := by
            rw [← Real.exp_nat_mul]
            congr 1
            have hn0 : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'
            field_simp [hn0]
    rw [kFun_add_one hs0]
    calc ‖(1 + 1 / s) ^ n - 1‖ ≤ ‖(1 + 1 / s) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _
      _ = ‖1 + 1 / s‖ ^ n + 1 := by rw [norm_pow, norm_one]
      _ ≤ Real.exp 4 + 1 := by linarith [hpow]

/-- **L1 (right vertical)**: ‖kFun n (s+1)‖ ≤ e^{√n/2} + 1 for 0 < n and
2√n ≤ re s (D-036 §3 (I)): then |1+1/s| ≤ 1 + 1/(2√n), whose n-th power
is ≤ e^{n/(2√n)} = e^{√n/2}. -/
theorem kFun_shift_norm_le_exp_sqrt_half_add_one {n : ℕ} {s : ℂ}
    (hn : 0 < n) (hσ : 2 * Real.sqrt (n : ℝ) ≤ s.re) :
    ‖kFun n (s + 1)‖ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by
  have hnR : (0:ℝ) < (n : ℝ) := by exact_mod_cast hn
  have hsqrt : 0 < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr hnR
  have hre0 : (0:ℝ) ≤ s.re := by linarith [hsqrt.le]
  have hnorm_s : 2 * Real.sqrt (n : ℝ) ≤ ‖s‖ :=
    hσ.trans (abs_of_nonneg hre0 ▸ Complex.abs_re_le_norm s)
  have hs0 : s ≠ 0 := by
    rintro h
    rw [h, norm_zero] at hnorm_s
    linarith [hsqrt]
  have hnorm_pos : (0:ℝ) < ‖s‖ := by linarith [hsqrt]
  have h1 : ‖1 + 1 / s‖ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by
    calc ‖1 + 1 / s‖ ≤ ‖(1 : ℂ)‖ + ‖1 / s‖ := norm_add_le _ _
      _ = 1 + 1 / ‖s‖ := by rw [norm_one, norm_div, norm_one]
      _ ≤ 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by
          have h := (div_le_div_iff_of_pos_left one_pos hnorm_pos
            (by positivity : (0:ℝ) < 2 * Real.sqrt (n : ℝ))).mpr hnorm_s
          linarith [h]
  have hpow : ‖1 + 1 / s‖ ^ n ≤ Real.exp (Real.sqrt (n : ℝ) / 2) := by
    calc ‖1 + 1 / s‖ ^ n ≤ (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n :=
          pow_le_pow_left₀ (norm_nonneg _) h1 n
      _ ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ)))) ^ n := by
          have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : ℝ)))
          exact pow_le_pow_left₀ (by positivity) (by linarith) n
      _ = Real.exp (Real.sqrt (n : ℝ) / 2) := by
          rw [← Real.exp_nat_mul]
          congr 1
          rw [mul_one_div, div_eq_div_iff (by positivity : (2 * Real.sqrt (n : ℝ)) ≠ 0)
            (by norm_num : (2 : ℝ) ≠ 0)]
          nlinarith [Real.mul_self_sqrt hnR.le]
  rw [kFun_add_one hs0]
  calc ‖(1 + 1 / s) ^ n - 1‖ ≤ ‖(1 + 1 / s) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _
    _ = ‖1 + 1 / s‖ ^ n + 1 := by rw [norm_pow, norm_one]
    _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by linarith [hpow]

/-- **L1 (trivial-zero term)**: kFun n (−2) = (2/3)ⁿ − 1. -/
theorem kFun_neg_two (n : ℕ) : kFun n (-2) = (2 / 3 : ℂ) ^ n - 1 := by
  unfold kFun
  norm_num

/-- The trivial-zero contribution is harmless: ‖kFun n (−2)‖ ≤ 1
(it equals 1 − (2/3)ⁿ as a real absolute value). -/
theorem norm_kFun_neg_two_le_one (n : ℕ) : ‖kFun n (-2)‖ ≤ 1 := by
  rw [kFun_neg_two]
  have h23 : (2 / 3 : ℂ) = ((2 / 3 : ℝ) : ℂ) := by norm_num
  rw [h23]
  have h : (((2 / 3 : ℝ) : ℂ) ^ n - 1) = (((2 / 3 : ℝ) ^ n - 1 : ℝ) : ℂ) := by
    push_cast
    ring
  rw [h, Complex.norm_real, Real.norm_eq_abs]
  have h01 : (0:ℝ) ≤ (2 / 3 : ℝ) ^ n := by positivity
  have h1le : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
  rw [abs_of_nonpos (by linarith)]
  linarith

/-! ## 5. Trivial-zero simplicity: zeroMult (−2) = 1 -/

/-- The local factor of ΓR at −2: Hfun s = 4·π^{−s/2}·Γ(s/2+2)/s. Equals
(s+2)·ΓR(s) off {−2, 0} (by `Gamma_add_one` twice); analytic at −2 with
Hfun(−2) = −2π ≠ 0. This is the nonvanishing cofactor in the local
factorization ζ(s) = (s+2)·(Λ(s)/Hfun(s)) proving zeroMult(−2) = 1. -/
def Hfun (s : ℂ) : ℂ := 4 * (Real.pi : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2 + 2) / s

/-- Hfun is analytic at −2: on ball(−2, 1) the point s/2+2 avoids the
Gamma poles {0, −1, −2, …} (it lies in ball(1, 1/2)). -/
theorem Hfun_analyticAt_neg_two : AnalyticAt ℂ Hfun (-2) := by
  have hcpi : AnalyticAt ℂ (fun s : ℂ => (Real.pi : ℂ) ^ (-s / 2)) (-2) := by
    have hexp : AnalyticAt ℂ
        (fun s : ℂ => Complex.exp ((Complex.log (Real.pi : ℂ) * (-1 / 2)) * s)) (-2) :=
      (analyticAt_const.mul analyticAt_id).cexp
    apply hexp.congr
    filter_upwards with s
    rw [Complex.cpow_def_of_ne_zero (by norm_num : (Real.pi : ℂ) ≠ 0)]
    ring_nf
  have hGamma : AnalyticAt ℂ (fun s : ℂ => Complex.Gamma (s / 2 + 2)) (-2) := by
    have hd : DifferentiableOn ℂ (fun s : ℂ => Complex.Gamma (s / 2 + 2))
        (Metric.ball (-2 : ℂ) (1 : ℝ)) := by
      intro s hs
      have hg : DifferentiableAt ℂ Complex.Gamma (s / 2 + 2) := by
        apply Complex.differentiableAt_Gamma
        intro m hm
        have hs_eq : s = -2 * (m : ℂ) - 4 := by linear_combination 2 * hm
        rw [hs_eq, Metric.mem_ball, dist_eq_norm] at hs
        have h1 : ((-2 : ℂ) * (m : ℂ) - 4) - -2
            = -(((2 : ℝ) * m + 2 : ℝ) : ℂ) := by push_cast; ring
        rw [h1, norm_neg, Complex.norm_real, Real.norm_eq_abs] at hs
        rw [abs_of_nonneg (by positivity : (0:ℝ) ≤ 2 * (m : ℝ) + 2)] at hs
        have hge : (2:ℝ) ≤ 2 * (m : ℝ) + 2 := by
          have hm0 : (0:ℝ) ≤ (m : ℝ) := by positivity
          linarith
        linarith
      exact (hg.comp s
        (show DifferentiableAt ℂ (fun s : ℂ => s / 2 + 2) s from by fun_prop)).differentiableWithinAt
    have hball : (-2 : ℂ) ∈ Metric.ball (-2 : ℂ) (1 : ℝ) :=
      Metric.mem_ball_self (zero_lt_one : (0:ℝ) < 1)
    exact (hd.analyticOnNhd Metric.isOpen_ball) _ hball
  show AnalyticAt ℂ (fun s : ℂ => 4 * (Real.pi : ℂ) ^ (-s / 2) *
    Complex.Gamma (s / 2 + 2) / s) (-2)
  exact ((analyticAt_const.mul hcpi).mul hGamma).div analyticAt_id (by norm_num)

/-- Hfun(−2) = −2π (via Γ(1) = 1 and π^1 = π). -/
theorem Hfun_neg_two : Hfun (-2) = -2 * (Real.pi : ℂ) := by
  unfold Hfun
  rw [show (-(-2 : ℂ) / 2) = 1 by norm_num, Complex.cpow_one,
    show ((-2 : ℂ) / 2 + 2) = 1 by norm_num, Complex.Gamma_one, mul_one]
  field_simp
  ring

/-- Hfun(−2) ≠ 0. -/
theorem Hfun_neg_two_ne_zero : Hfun (-2) ≠ 0 := by
  rw [Hfun_neg_two]
  norm_num [Real.pi_ne_zero]

/-- The punctured identity: (s+2)·ΓR(s) = Hfun s for s ∉ {−2, 0}
(Gamma_add_one applied twice: Γ(s/2) = Γ(s/2+2)/((s/2)(s/2+1))). -/
theorem Hfun_eq (s : ℂ) (hs2 : s ≠ -2) (hs0 : s ≠ 0) :
    (s + 2) * Complex.Gammaℝ s = Hfun s := by
  have h2ne : s / 2 ≠ 0 := div_ne_zero hs0 (by norm_num)
  have h21ne : s / 2 + 1 ≠ 0 := by
    intro h
    apply hs2
    linear_combination 2 * h
  have h1 := Complex.Gamma_add_one (s / 2) h2ne
  have h2 : Complex.Gamma (s / 2 + 2) = (s / 2 + 1) * Complex.Gamma (s / 2 + 1) := by
    rw [show s / 2 + 2 = (s / 2 + 1) + 1 by ring]
    exact Complex.Gamma_add_one _ h21ne
  have hG : Complex.Gamma (s / 2)
      = Complex.Gamma (s / 2 + 2) / ((s / 2) * (s / 2 + 1)) := by
    have h12 : Complex.Gamma (s / 2 + 2)
        = (s / 2 + 1) * (s / 2) * Complex.Gamma (s / 2) := by
      rw [h2, h1]; ring
    rw [h12, mul_comm (s / 2 + 1) (s / 2)]
    exact (mul_div_cancel_left₀ _ (mul_ne_zero h2ne h21ne)).symm
  rw [Complex.Gammaℝ_def, hG]
  unfold Hfun
  have hs2' : s + 2 ≠ 0 := by
    rw [ne_eq, add_eq_zero_iff_eq_neg]
    exact hs2
  field_simp [hs0, hs2', mul_ne_zero h2ne h21ne]
  ring

/-- **Trivial-zero simplicity** (deferred from ii′-1b(iii), route D-066 §6):
zeroMult(−2) = 1. The local factorization ζ(s) = (s+2)·G(s) holds near −2
with G(s) = Λ(s)/Hfun(s) analytic and G(−2) = Λ(−2)/(−2π) ≠ 0, since
Λ(−2) = Λ(3) = ΓR(3)·ζ(3) ≠ 0 (functional equation + ΓR(3) ≠ 0 via
`Gammaℝ_eq_zero_iff` + `riemannZeta_ne_zero_of_one_lt_re`). -/
theorem zeroMult_neg_two : zeroMult (-2) = 1 := by
  have hHfun_an : AnalyticAt ℂ Hfun (-2) := Hfun_analyticAt_neg_two
  have hHfun_ne : Hfun (-2) ≠ 0 := Hfun_neg_two_ne_zero
  have hΛ_an : AnalyticAt ℂ completedRiemannZeta (-2) := by
    have hd : DifferentiableOn ℂ completedRiemannZeta (Metric.ball (-2) 1) := by
      intro s hs
      have hs0 : s ≠ 0 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs
        have e : ((0 : ℂ) - -2) = ((2 : ℝ) : ℂ) := by norm_num
        rw [e, Complex.norm_real, Real.norm_eq_abs] at hs
        norm_num at hs
      have hs1 : s ≠ 1 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs
        have e : ((1 : ℂ) - -2) = ((3 : ℝ) : ℂ) := by norm_num
        rw [e, Complex.norm_real, Real.norm_eq_abs] at hs
        norm_num at hs
      exact (differentiableAt_completedZeta hs0 hs1).differentiableWithinAt
    exact (hd.analyticOnNhd Metric.isOpen_ball) (-2) (Metric.mem_ball_self zero_lt_one)
  have hΛ_ne : completedRiemannZeta (-2) ≠ 0 := by
    have hΓR3 : Complex.Gammaℝ 3 ≠ 0 := by
      rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]
      rintro ⟨m, hm⟩
      have hre := congrArg Complex.re hm
      norm_num [Complex.neg_re, Complex.mul_re] at hre
      have hm0 : (0:ℝ) ≤ (m : ℝ) := by positivity
      linarith
    have hζ3 : riemannZeta 3 ≠ 0 :=
      riemannZeta_ne_zero_of_one_lt_re (by norm_num)
    have hΛ3 : completedRiemannZeta 3 ≠ 0 := by
      rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul (by norm_num) hΓR3]
      exact mul_ne_zero hΓR3 hζ3
    have hfe : completedRiemannZeta (-2) = completedRiemannZeta 3 := by
      have h := completedRiemannZeta_one_sub (-2 : ℂ)
      norm_num at h
      exact h.symm
    rw [hfe]
    exact hΛ3
  have hG_an : AnalyticAt ℂ (fun s => completedRiemannZeta s / Hfun s) (-2) :=
    hΛ_an.div hHfun_an hHfun_ne
  have hG_ne : completedRiemannZeta (-2) / Hfun (-2) ≠ 0 :=
    div_ne_zero hΛ_ne hHfun_ne
  have hEv : ∀ᶠ s in 𝓝 (-2 : ℂ),
      riemannZeta s = (s - -2) ^ 1 • (completedRiemannZeta s / Hfun s) := by
    have hHne_ev : ∀ᶠ s in 𝓝 (-2 : ℂ), Hfun s ≠ 0 :=
      hHfun_an.continuousAt.eventually_ne hHfun_ne
    filter_upwards [Metric.ball_mem_nhds (-2) (zero_lt_one : (0:ℝ) < 1), hHne_ev]
      with s hs1 hHne
    by_cases hs : s = -2
    · subst hs
      have hz0 : riemannZeta (-2) = 0 := by
        have h := riemannZeta_neg_two_mul_nat_add_one 0
        norm_num at h
        exact h
      rw [hz0]
      simp
    · have hs0 : s ≠ 0 := by
        rintro h
        rw [h, Metric.mem_ball, dist_eq_norm] at hs1
        have e : ((0 : ℂ) - -2) = ((2 : ℝ) : ℂ) := by norm_num
        rw [e, Complex.norm_real, Real.norm_eq_abs] at hs1
        norm_num at hs1
      have hΓR : Complex.Gammaℝ s ≠ 0 := by
        rw [ne_eq, Complex.Gammaℝ_eq_zero_iff]
        rintro ⟨m, hm⟩
        rcases Nat.eq_zero_or_pos m with hm0 | hmpos
        · subst hm0
          norm_num at hm
          exact hs0 hm
        · rcases eq_or_ne m 1 with hm1 | hm1
          · subst hm1
            norm_num at hm
            exact hs hm
          · have hm2 : 2 ≤ m := by omega
            rw [hm, Metric.mem_ball, dist_eq_norm] at hs1
            have h1 : (-(2 * (m : ℂ))) - -2 = (((2 : ℝ) - 2 * m : ℝ) : ℂ) := by
              push_cast
              ring
            rw [h1, Complex.norm_real, Real.norm_eq_abs] at hs1
            have hle : (2:ℝ) - 2 * (m : ℝ) ≤ 0 := by
              have hmR : (2:ℝ) ≤ (m : ℝ) := by exact_mod_cast hm2
              linarith
            rw [abs_of_nonpos hle] at hs1
            have hmR : (2:ℝ) ≤ (m : ℝ) := by exact_mod_cast hm2
            nlinarith
      have hΛ := RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hΓR
      have hH : (s + 2) * Complex.Gammaℝ s = Hfun s := Hfun_eq s hs hs0
      rw [pow_one, smul_eq_mul, show s - -2 = s + 2 by ring]
      have hz : riemannZeta s = completedRiemannZeta s / Complex.Gammaℝ s := by
        rw [hΛ, mul_div_cancel_left₀ _ hΓR]
      rw [hz, ← mul_div_assoc, div_eq_div_iff hΓR hHne, ← hH]
      ring
  have hRHS_an : AnalyticAt ℂ
      (fun s => (s - -2) ^ 1 • (completedRiemannZeta s / Hfun s)) (-2) :=
    ((analyticAt_id.sub analyticAt_const).pow 1).smul hG_an
  have hzeta_an : AnalyticAt ℂ riemannZeta (-2) := hRHS_an.congr (EventuallyEq.symm hEv)
  have horder : analyticOrderAt riemannZeta (-2) = 1 :=
    (hzeta_an.analyticOrderAt_eq_natCast).mpr
      ⟨fun s => completedRiemannZeta s / Hfun s, hG_an, hG_ne, hEv⟩
  rw [zeroMult, horder]
  exact ENat.toNat_one

end NguyenRH1

end