LiDisc.lean

Declarations

Source

/-
NguyenRH1/LiDisc.lean — tier ii′ sub-stage ii′-5c (D-067 §3 + §6 revision):
the LOOSE Davenport-disc R-bound on σ ∈ [1/2, 7/2], |t| ≥ 10 — the
GROWTH INPUT for the partial-fraction identity (ii′-5e). Its constants
are deliberately loose (D-067 §6: no disc-only constant can reach the
baked A = 10.5, B₀ = 48; tightness comes from the identity stage).

Structure (all on the disc B(2+it, R), R ∈ [2.4, 2.5] chosen in a gap of
the zero-distance values):
* §1 the zero collection + count (perimeter ZeroCountProp, ii′-4);
* §2 the R-gap selection (scaled midpoint pigeonhole from ii′-4);
* §3 g := ζ/∏(s−ρₖ)^{mₖ} analytic + nonvanishing on the closed disc;
* §4 the bounds: |g| on the outer circle (ii′-5b's |ζ|-bound +
  clearance), the center lower bound (1/ζ = Σ μ(n)n^{−s}), then
  LogOfAnalyticFunction + BorelCaratheodoryDeriv (StrongPNTPrefix)
  giving ‖(log g)′‖ ≪ (log|t|)², hence the loose R-bound.

Archive references: D-067, D-064 §4 R3, journal-022.
-/
import Mathlib
import Zeta23.FromPNTPlus.StrongPNTPrefix
import NguyenRH1.LiRBound
import NguyenRH1.LiContour

open Zeta23 Complex Filter Topology MeasureTheory
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. The zero collection and its count -/

/-- The disc center s₀ = 2 + it. -/
def discCenter (t : ℝ) : ℂ := 2 + t * Complex.I

/-- The zeros of ζ in the closed disc of radius 5/2 about 2+it, as a
finset (finiteness from Mathlib's discrete-zero-set machinery). -/
noncomputable def zeroDiscFinset (t : ℝ) : Finset ℂ :=
  ((isCompact_closedBall (discCenter t) (5 / 2)).inter_riemannZetaZeros_finite).toFinset

theorem mem_zeroDiscFinset {t : ℝ} {ρ : ℂ} :
    ρ ∈ zeroDiscFinset t ↔
      ρ ∈ Metric.closedBall (discCenter t) (5 / 2) ∧ riemannZeta ρ = 0 := by
  unfold zeroDiscFinset
  rw [Set.Finite.mem_toFinset]
  constructor
  · intro h
    exact ⟨h.1, h.2⟩
  · intro h
    exact ⟨h.1, mem_riemannZetaZeros.mpr h.2⟩

/-- Every zero of ζ in the disc is a nontrivial zero (re ≥ 1 excluded by
`riemannZeta_ne_zero_of_one_le_re`; re ≤ 0 excluded by the FE since the
disc avoids {−2n} and 0). -/
theorem zeroDisc_isNontrivial {t : ℝ} {ρ : ℂ} (hρ : ρ ∈ zeroDiscFinset t) :
    IsNontrivialZero ρ := by
  have h2 := (mem_zeroDiscFinset.mp hρ).2
  have hball := (mem_zeroDiscFinset.mp hρ).1
  -- ρ ∈ closedBall (2+it) (5/2) ⟹ re ρ ∈ [−1/2, 9/2]
  have hre : -1 / 2 ≤ ρ.re ∧ ρ.re ≤ 9 / 2 := by
    rw [Metric.mem_closedBall, Complex.dist_eq] at hball
    have h1 : |(ρ - discCenter t).re| ≤ 5 / 2 := (abs_re_le_norm _).trans hball
    have h2re : (ρ - discCenter t).re = ρ.re - 2 := by
      simp [discCenter, sub_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]
    rw [h2re] at h1
    have := abs_le.mp h1
    constructor <;> linarith [this.1, this.2]
  -- re ρ ≥ 1 excluded
  have hnot1 : ρ.re < 1 := by
    by_contra h
    push Not at h
    exact riemannZeta_ne_zero_of_one_le_re h h2
  -- re ρ ≤ 0 excluded (would force ρ ∈ {−2n} ∪ {0}, all outside the disc)
  have hpos : 0 < ρ.re := by
    by_contra h
    push Not at h
    by_cases hG : Complex.Gammaℝ ρ = 0
    · -- ΓR(ρ) = 0 ⟹ ρ = −2n: n = 0 gives ζ(0) = −1/2 ≠ 0; n ≥ 1 gives re ≤ −2
      rw [Complex.Gammaℝ_eq_zero_iff] at hG
      obtain ⟨n, hn⟩ := hG
      have hre' : ρ.re = -2 * (n : ℝ) := by
        rw [hn]
        simp [neg_re, mul_re]
      rcases Nat.eq_zero_or_pos n with hn0 | hnpos
      · subst hn0
        norm_num at hre'
        rw [hn] at h2
        norm_num at h2
        rw [riemannZeta_zero] at h2
        norm_num at h2
      · have hn1 : (1:ℝ) ≤ (n : ℝ) := by exact_mod_cast hnpos
        linarith [hre.1, hre']
    · have hρ0 : ρ ≠ 0 := by
        intro h0
        rw [h0, riemannZeta_zero] at h2
        norm_num at h2
      have hΛ : completedRiemannZeta ρ = 0 := by
        rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hρ0 hG, h2, mul_zero]
      exact absurd (RvM.completedRiemannZeta_eq_zero_iff.mp hΛ).2.1 (not_lt.mpr h)
  exact ⟨h2, hpos, hnot1⟩

/-! ## 2. The scaled function, the Jensen count, and the R-gap

The scaled function F(w) = ζ(s₀ + (5/2)w)/ζ(s₀) on the unit disc, to
which Zeta23's `ZerosBound` (Jensen) applies: F(0) = 1 (the center lower
bound ‖ζ(2+it)‖ ≥ 1/3 is Zeta23's `RvM.zeta_lower_bound_two`), and
‖F‖ ≤ (9/4)|t|² on the closed unit disc (ii′-5b's disc bound). -/

/-- The scaled function F(w) = ζ(s₀ + (5/2)·w)/ζ(s₀), s₀ = 2+it. -/
noncomputable def scaledZeta (t : ℝ) (w : ℂ) : ℂ :=
  riemannZeta (discCenter t + (5 / 2 : ℂ) * w) / riemannZeta (discCenter t)

theorem scaledZeta_zero (t : ℝ) : scaledZeta t 0 = 1 := by
  unfold scaledZeta
  simp only [mul_zero, add_zero]
  exact div_self (fun h0 => by
    have h := RvM.zeta_lower_bound_two t
    rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h
    norm_num at h)

/-- ζ is analytic on neighborhoods of every point ≠ 1. -/
theorem analyticAt_riemannZeta_of_ne_one {z : ℂ} (hz : z ≠ 1) :
    AnalyticAt ℂ riemannZeta z :=
  (HolomorphicOn_riemannZeta.analyticOnNhd isOpen_compl_singleton) z hz

/-- F is analytic on the closed unit disc (ζ is analytic on B(s₀, 5/2),
which avoids the pole at 1 since |t| ≥ 10 ⟹ |im| ≥ 15/2). -/
theorem scaledZeta_analytic {t : ℝ} (ht : 10 ≤ |t|) :
    AnalyticOnNhd ℂ (scaledZeta t) (Metric.closedBall 0 1) := by
  intro w hw
  rw [Metric.mem_closedBall, dist_zero_right] at hw
  have hw' : ‖(5 / 2 : ℂ) * w‖ ≤ 5 / 2 := by
    have hn : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by
      rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
        Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
    rw [norm_mul, hn]
    calc (5 / 2 : ℝ) * ‖w‖ ≤ (5 / 2) * 1 := mul_le_mul_of_nonneg_left hw (by norm_num)
      _ = 5 / 2 := by norm_num
  -- the evaluation point is not 1 (its imaginary part is large)
  have hne : discCenter t + (5 / 2 : ℂ) * w ≠ 1 := by
    intro h
    have hwim : |w.im| ≤ 1 := (abs_im_le_norm _).trans hw
    have him : (discCenter t + (5 / 2 : ℂ) * w).im = t + (5 / 2) * w.im := by
      simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
    have hbig : 15 / 2 ≤ |t + (5 / 2) * w.im| := by
      have h2 : |t| ≤ |t + (5 / 2) * w.im| + |(5 / 2) * w.im| := by
        have h3 := abs_add_le (t + (5 / 2) * w.im) (-((5 / 2) * w.im))
        rw [abs_neg, add_neg_cancel_right] at h3
        exact h3
      have h4 : |(5 / 2) * w.im| ≤ 5 / 2 := by
        rw [abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
        calc (5 / 2) * |w.im| ≤ (5 / 2) * 1 :=
              mul_le_mul_of_nonneg_left hwim (by norm_num)
          _ = 5 / 2 := by norm_num
      linarith [h2, h4, ht]
    rw [h] at him
    rw [Complex.one_im] at him
    rw [← him] at hbig
    norm_num at hbig
  have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w :=
    analyticAt_const.add (analyticAt_const.mul analyticAt_id)
  exact ((analyticAt_riemannZeta_of_ne_one hne).comp_of_eq haff rfl).div analyticAt_const
    (fun h0 => by
      have h := RvM.zeta_lower_bound_two t
      rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h
      norm_num at h)

/-- The order of ζ is invariant under the affine change of variable
w ↦ s₀ + (5/2)·w (nonzero slope), valid for ‖w₀‖ ≤ 1 (so the target
avoids the pole at 1). -/
theorem analyticOrderNatAt_riemannZeta_affine {t : ℝ} (ht : 10 ≤ |t|) {w₀ : ℂ}
    (hw₀ : ‖w₀‖ ≤ 1) :
    analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀
      = analyticOrderNatAt riemannZeta (discCenter t + (5 / 2 : ℂ) * w₀) := by
  set z₀ := discCenter t + (5 / 2 : ℂ) * w₀ with hz₀
  -- z₀ avoids 1 (its imaginary part is large)
  have hz₀ne : z₀ ≠ 1 := by
    intro h
    have hwim : |w₀.im| ≤ 1 := (abs_im_le_norm _).trans hw₀
    have him : z₀.im = t + (5 / 2) * w₀.im := by
      simp [hz₀, discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
    have hbig : 15 / 2 ≤ |t + (5 / 2) * w₀.im| := by
      have h3 := abs_add_le (t + (5 / 2) * w₀.im) (-((5 / 2) * w₀.im))
      rw [abs_neg, add_neg_cancel_right] at h3
      have h4 : |(5 / 2) * w₀.im| ≤ 5 / 2 := by
        rw [abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
        calc (5 / 2) * |w₀.im| ≤ (5 / 2) * 1 :=
              mul_le_mul_of_nonneg_left hwim (by norm_num)
          _ = 5 / 2 := by norm_num
      linarith [h3, h4, ht]
    rw [h] at him
    rw [Complex.one_im] at him
    rw [← him] at hbig
    norm_num at hbig
  obtain ⟨h', h1, h2, h3⟩ := (analyticAt_riemannZeta_of_ne_one hz₀ne).analyticOrderAt_ne_top.mp
    (zeta_order_ne_top_of_ne hz₀ne)
  -- transfer the factorization to the w-side
  have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ :=
    analyticAt_const.add (analyticAt_const.mul analyticAt_id)
  have haffT : Tendsto (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) (𝓝 w₀) (𝓝 z₀) :=
    haff.continuousAt
  have h3' := h3.comp_tendsto haffT
  -- h3' : ζ ∘ aff =ᶠ series ∘ aff; massage the form
  have hpt : ∀ w : ℂ,
      ((fun z => (z - z₀) ^ analyticOrderNatAt riemannZeta z₀ • h' z) ∘
        fun w => discCenter t + (5 / 2 : ℂ) * w) w
        = (w - w₀) ^ analyticOrderNatAt riemannZeta z₀ •
          (((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) *
            h' (discCenter t + (5 / 2 : ℂ) * w)) := by
    intro w
    simp only [Function.comp_apply]
    rw [show discCenter t + (5 / 2 : ℂ) * w - z₀ = (5 / 2 : ℂ) * (w - w₀) by rw [hz₀]; ring]
    rw [mul_pow, smul_eq_mul, smul_eq_mul]
    ring
  have hF : (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) =ᶠ[𝓝 w₀]
      fun w => (w - w₀) ^ analyticOrderNatAt riemannZeta z₀ •
        (((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) *
          h' (discCenter t + (5 / 2 : ℂ) * w)) :=
    h3'.trans (Filter.Eventually.of_forall hpt)
  have hcof : AnalyticAt ℂ (fun w => ((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) *
      h' (discCenter t + (5 / 2 : ℂ) * w)) w₀ :=
    analyticAt_const.mul (h1.comp_of_eq haff rfl)
  have hcof_ne : ((5 / 2 : ℂ) ^ analyticOrderNatAt riemannZeta z₀) * h' z₀ ≠ 0 :=
    mul_ne_zero (pow_ne_zero _ (by norm_num)) h2
  have hF_an : AnalyticAt ℂ (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀ :=
    analyticAt_riemannZeta_of_ne_one hz₀ne |>.comp_of_eq haff rfl
  have horder : analyticOrderAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀
      = (analyticOrderNatAt riemannZeta z₀ : ℕ∞) :=
    (hF_an.analyticOrderAt_eq_natCast).mpr ⟨_, hcof, hcof_ne, hF⟩
  have hF_top : analyticOrderAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀
      ≠ ⊤ := by
    rw [horder]
    exact ENat.natCast_ne_top _
  have h1c := Nat.cast_analyticOrderNatAt hF_top
  have h2c := Nat.cast_analyticOrderNatAt (zeta_order_ne_top_of_ne hz₀ne)
  have hcast : ((analyticOrderNatAt (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀
      : ℕ) : ℕ∞) = ((analyticOrderNatAt riemannZeta z₀ : ℕ) : ℕ∞) := by
    rw [h1c, h2c, horder]
    exact h2c
  exact Nat.cast_inj.mp hcast

/-! ## 3. The Jensen count and the R-gap -/

/-- Zeros of the scaled function F in the closed unit ball are finite. -/
theorem scaledZeta_zeros_finite {t : ℝ} :
    (SetOfZeros 1 (scaledZeta t)).Finite := by
  have hz0 : riemannZeta (discCenter t) ≠ 0 := by
    have h := RvM.zeta_lower_bound_two t
    intro h0
    rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h
    norm_num at h
  -- SetOfZeros 1 F = the affine preimage of the ζ-zeros in the 5/2-disc
  have hsub : SetOfZeros 1 (scaledZeta t) ⊆
      (fun w => discCenter t + (5 / 2 : ℂ) * w) ⁻¹'
        (Metric.closedBall (discCenter t) (5 / 2) ∩ riemannZetaZeros) := by
    intro w hw
    have hFw : riemannZeta (discCenter t + (5 / 2 : ℂ) * w) = 0 := by
      have := hw.2
      unfold scaledZeta at this
      exact (div_eq_zero_iff.mp this).resolve_right hz0
    constructor
    · rw [Metric.mem_closedBall, Complex.dist_eq]
      rw [add_sub_cancel_left]
      calc ‖(5 / 2 : ℂ) * w‖ ≤ (5 / 2) * ‖w‖ := by
            rw [norm_mul]
            have hn : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by
              rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
                Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
            rw [hn]
        _ ≤ (5 / 2) * 1 := mul_le_mul_of_nonneg_left hw.1 (by norm_num)
        _ = 5 / 2 := by norm_num
    · exact mem_riemannZetaZeros.mpr hFw
  have hfin : ((fun w => discCenter t + (5 / 2 : ℂ) * w) ⁻¹'
      (Metric.closedBall (discCenter t) (5 / 2) ∩ riemannZetaZeros)).Finite :=
    ((isCompact_closedBall _ _).inter_riemannZetaZeros_finite).preimage (fun a _ b _ hab =>
      (mul_left_cancel₀ (by norm_num : (5 / 2 : ℂ) ≠ 0) (add_left_cancel hab)))
  exact hfin.subset hsub

/-! ## 4. The Jensen count -/

/-- A nonzero constant factor does not change the analytic order. -/
theorem analyticOrderNatAt_const_mul {C : ℂ} (hC : C ≠ 0) {X : ℂ → ℂ} {w₀ : ℂ}
    (hX : AnalyticAt ℂ X w₀) :
    analyticOrderNatAt (fun w => C * X w) w₀ = analyticOrderNatAt X w₀ := by
  have hord : analyticOrderAt (fun w => C * X w) w₀ = analyticOrderAt X w₀ := by
    have h1 : analyticOrderAt ((fun _ : ℂ => C) • X) w₀
        = analyticOrderAt (fun _ : ℂ => C) w₀ + analyticOrderAt X w₀ :=
      analyticOrderAt_smul analyticAt_const hX
    have h2 : analyticOrderAt (fun _ : ℂ => C) w₀ = 0 :=
      (analyticAt_const (𝕜 := ℂ) (v := C)).analyticOrderAt_eq_zero.mpr hC
    have h3 : (fun w : ℂ => C * X w) = (fun _ : ℂ => C) • X :=
      funext fun w => by simp [smul_eq_mul]
    rw [h3, h1, h2]
    simp
  by_cases htop : analyticOrderAt X w₀ = ⊤
  · rw [htop] at hord
    show (analyticOrderAt (fun w => C * X w) w₀).toNat = (analyticOrderAt X w₀).toNat
    rw [hord, htop]
  · have h1c := Nat.cast_analyticOrderNatAt (f := fun w => C * X w) (z₀ := w₀)
      (by rw [hord]; exact htop)
    have h2c := Nat.cast_analyticOrderNatAt (f := X) (z₀ := w₀) htop
    have hcast : ((analyticOrderNatAt (fun w => C * X w) w₀ : ℕ) : ℕ∞)
        = ((analyticOrderNatAt X w₀ : ℕ) : ℕ∞) := by
      rw [h1c, h2c, hord]
    exact Nat.cast_inj.mp hcast

/-- The order of the scaled function at w₀ equals the order of ζ at the
affine image (for ‖w₀‖ ≤ 1, |t| ≥ 10). -/
theorem analyticOrderNatAt_scaledZeta {t : ℝ} (ht : 10 ≤ |t|) {w₀ : ℂ} (hw₀ : ‖w₀‖ ≤ 1) :
    analyticOrderNatAt (scaledZeta t) w₀
      = analyticOrderNatAt riemannZeta (discCenter t + (5 / 2 : ℂ) * w₀) := by
  have hζ0 : riemannZeta (discCenter t) ≠ 0 := by
    have h := RvM.zeta_lower_bound_two t
    intro h0
    rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h
    norm_num at h
  have haffine := analyticOrderNatAt_riemannZeta_affine ht hw₀
  have haff_an : AnalyticAt ℂ (fun w => riemannZeta (discCenter t + (5 / 2 : ℂ) * w)) w₀ := by
    have hne : discCenter t + (5 / 2 : ℂ) * w₀ ≠ 1 := by
      intro h
      have hwim : |w₀.im| ≤ 1 := (abs_im_le_norm _).trans hw₀
      have him : (discCenter t + (5 / 2 : ℂ) * w₀).im = t + (5 / 2) * w₀.im := by
        simp [discCenter, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
      have hbig : 15 / 2 ≤ |t + (5 / 2) * w₀.im| := by
        have h3 := abs_add_le (t + (5 / 2) * w₀.im) (-((5 / 2) * w₀.im))
        rw [abs_neg, add_neg_cancel_right] at h3
        have h4 : |(5 / 2) * w₀.im| ≤ 5 / 2 := by
          rw [abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
          calc (5 / 2) * |w₀.im| ≤ (5 / 2) * 1 :=
                mul_le_mul_of_nonneg_left hwim (by norm_num)
            _ = 5 / 2 := by norm_num
        linarith [h3, h4, ht]
      rw [h] at him
      rw [Complex.one_im] at him
      rw [← him] at hbig
      norm_num at hbig
    have haff : AnalyticAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ :=
      analyticAt_const.add (analyticAt_const.mul analyticAt_id)
    exact (analyticAt_riemannZeta_of_ne_one hne).comp_of_eq haff rfl
  have hconst := analyticOrderNatAt_const_mul (inv_ne_zero hζ0) haff_an
  -- scaledZeta t = fun w => (ζ(s₀))⁻¹ * ζ(aff w) pointwise
  have hpoint : scaledZeta t = fun w => (riemannZeta (discCenter t))⁻¹ *
      riemannZeta (discCenter t + (5 / 2 : ℂ) * w) :=
    funext fun w => by unfold scaledZeta; rw [div_eq_mul_inv, mul_comm]
  rw [hpoint, hconst]
  exact haffine

/-- **The Jensen count**: the mult-weighted count of zeros of the scaled
function F in the closed ball of radius 24/25, via Zeta23's `ZerosBound`
applied with B = (9/4)·|t|². -/
theorem scaledZeta_jensen_count {t : ℝ} (ht : 10 ≤ |t|) :
    ∑ ρ ∈ (finiteSetOfZeros_mono (f := scaledZeta t) (r := 24 / 25)
      (by norm_num) (scaledZeta_zeros_finite)).toFinset,
        analyticOrderNatAt (scaledZeta t) ρ
      ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
  have hB : ∀ z : ℂ, ‖z‖ ≤ 99 / 100 → ‖scaledZeta t z‖ ≤ (9 / 4) * |t| ^ 2 := by
    intro z hz
    have hcenter : (1 / 3 : ℝ) ≤ ‖riemannZeta (discCenter t)‖ := by
      have h := RvM.zeta_lower_bound_two t
      rwa [← show discCenter t = 2 + t * Complex.I from rfl] at h
    have hcenter_pos : (0:ℝ) < ‖riemannZeta (discCenter t)‖ := by linarith
    have htsq : (0:ℝ) < |t| ^ 2 := by
      have : (0:ℝ) < |t| := by linarith
      positivity
    have htop : ‖riemannZeta (discCenter t + (5 / 2 : ℂ) * z)‖ ≤ (3 / 4) * |t| ^ 2 := by
      apply norm_riemannZeta_le_disc ht
      rw [Metric.mem_closedBall, Complex.dist_eq,
        show discCenter t = 2 + t * Complex.I from rfl, add_sub_cancel_left]
      calc ‖(5 / 2 : ℂ) * z‖ ≤ (5 / 2) * ‖z‖ := by
            rw [norm_mul]
            have hn : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by
              rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
                Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
            rw [hn]
        _ ≤ (5 / 2) * (99 / 100) := mul_le_mul_of_nonneg_left hz (by norm_num)
        _ ≤ 5 / 2 := by norm_num
    unfold scaledZeta
    rw [norm_div]
    calc ‖riemannZeta (discCenter t + (5 / 2 : ℂ) * z)‖ / ‖riemannZeta (discCenter t)‖
        ≤ ((3 / 4) * |t| ^ 2) / ‖riemannZeta (discCenter t)‖ :=
          (div_le_div_iff_of_pos_right hcenter_pos).mpr htop
      _ ≤ ((3 / 4) * |t| ^ 2) / (1 / 3) :=
          (div_le_div_iff_of_pos_left (by positivity) hcenter_pos (by norm_num)).mpr hcenter
      _ = (9 / 4) * |t| ^ 2 := by ring
  have h := ZerosBound (f := scaledZeta t) (r := 24 / 25) (R := 99 / 100)
    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
    (scaledZeta_analytic ht) (scaledZeta_zero t) scaledZeta_zeros_finite hB
  refine h.trans_eq ?_
  rw [one_div, inv_mul_eq_div]
  have hratio : (99 / 100 : ℝ) / (24 / 25) = 33 / 32 := by norm_num
  rw [hratio]

/-! ## 5. The scaled norm bound as a standalone lemma; order helpers -/

/-- The ii′-5b disc bound transferred to the scaled function (the content
of the Jensen-count bound `hB`, extracted for reuse in the |g|
outer-circle estimate). -/
theorem norm_scaledZeta_le {t : ℝ} (ht : 10 ≤ |t|) {z : ℂ} (hz : ‖z‖ ≤ 99 / 100) :
    ‖scaledZeta t z‖ ≤ (9 / 4) * |t| ^ 2 := by
  have hcenter : (1 / 3 : ℝ) ≤ ‖riemannZeta (discCenter t)‖ := by
    have h := RvM.zeta_lower_bound_two t
    rwa [← show discCenter t = 2 + t * Complex.I from rfl] at h
  have hcenter_pos : (0:ℝ) < ‖riemannZeta (discCenter t)‖ := by linarith
  have htop : ‖riemannZeta (discCenter t + (5 / 2 : ℂ) * z)‖ ≤ (3 / 4) * |t| ^ 2 := by
    apply norm_riemannZeta_le_disc ht
    rw [Metric.mem_closedBall, Complex.dist_eq,
      show discCenter t = 2 + t * Complex.I from rfl, add_sub_cancel_left]
    calc ‖(5 / 2 : ℂ) * z‖ ≤ (5 / 2) * ‖z‖ := by
          rw [norm_mul]
          have hn : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by
            rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
              Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
          rw [hn]
      _ ≤ (5 / 2) * (99 / 100) := mul_le_mul_of_nonneg_left hz (by norm_num)
      _ ≤ 5 / 2 := by norm_num
  unfold scaledZeta
  rw [norm_div]
  calc ‖riemannZeta (discCenter t + (5 / 2 : ℂ) * z)‖ / ‖riemannZeta (discCenter t)‖
      ≤ ((3 / 4) * |t| ^ 2) / ‖riemannZeta (discCenter t)‖ :=
        (div_le_div_iff_of_pos_right hcenter_pos).mpr htop
    _ ≤ ((3 / 4) * |t| ^ 2) / (1 / 3) :=
        (div_le_div_iff_of_pos_left (by positivity) hcenter_pos (by norm_num)).mpr hcenter
    _ = (9 / 4) * |t| ^ 2 := by ring

/-- The scaled function has finite order at every point of the closed unit
disc (it is analytic there and not identically zero, since F(0) = 1). -/
theorem scaledZeta_order_ne_top {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} (hw : ‖w‖ ≤ 1) :
    analyticOrderAt (scaledZeta t) w ≠ ⊤ := by
  have hfAn := scaledZeta_analytic ht
  have h0mem : (0 : ℂ) ∈ Metric.closedBall 0 1 := by
    rw [Metric.mem_closedBall, dist_zero_right, norm_zero]
    norm_num
  have hwmem : w ∈ Metric.closedBall 0 1 := by
    rwa [Metric.mem_closedBall, dist_zero_right]
  have hord0 : analyticOrderAt (scaledZeta t) 0 = 0 := by
    rw [analyticOrderAt_eq_zero]
    exact Or.inr (by rw [scaledZeta_zero]; exact one_ne_zero)
  have h0top : analyticOrderAt (scaledZeta t) 0 ≠ ⊤ := by
    rw [hord0]
    exact WithTop.zero_ne_top
  exact hfAn.analyticOrderAt_ne_top_of_isPreconnected Metric.isPreconnected_closedBall
    h0mem hwmem h0top

/-- A zero of the scaled function in the closed unit disc has order ≥ 1. -/
theorem one_le_analyticOrderNatAt_scaledZeta {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : ‖w‖ ≤ 1) (hw0 : scaledZeta t w = 0) :
    1 ≤ analyticOrderNatAt (scaledZeta t) w := by
  have htop := scaledZeta_order_ne_top ht hw
  have han : AnalyticAt ℂ (scaledZeta t) w :=
    scaledZeta_analytic ht w (by rwa [Metric.mem_closedBall, dist_zero_right])
  have hne : analyticOrderAt (scaledZeta t) w ≠ 0 := han.analyticOrderAt_ne_zero.mpr hw0
  have h := ENat.toNat_pos hne htop
  exact h

/-! ## 6. The zero finsets (radius-parameterized) and their counts -/

/-- Zeros of the scaled function F with norm ≤ r, as a finset (r ≤ 1). -/
def scaledZeroFinset (t : ℝ) (r : ℝ) (hr : r ≤ 1) : Finset ℂ :=
  (scaledZeta_zeros_finite.subset (t := SetOfZeros r (scaledZeta t)) fun w hw => by
    obtain ⟨h1, h2⟩ := hw
    exact ⟨h1.trans hr, h2⟩).toFinset

theorem mem_scaledZeroFinset {t : ℝ} {r : ℝ} {hr : r ≤ 1} {w : ℂ} :
    w ∈ scaledZeroFinset t r hr ↔ ‖w‖ ≤ r ∧ scaledZeta t w = 0 := by
  unfold scaledZeroFinset
  rw [Set.Finite.mem_toFinset]
  exact Iff.rfl

theorem scaledZeroFinset_subset {t : ℝ} {r₁ r₂ : ℝ} {hr₁ : r₁ ≤ 1} {hr₂ : r₂ ≤ 1}
    (h : r₁ ≤ r₂) : scaledZeroFinset t r₁ hr₁ ⊆ scaledZeroFinset t r₂ hr₂ := by
  intro w hw
  rw [mem_scaledZeroFinset] at hw ⊢
  exact ⟨hw.1.trans h, hw.2⟩

/-- The 24/25-finset agrees with the Jensen finset of
`scaledZeta_jensen_count`. -/
theorem scaledZeroFinset_24_25_eq (t : ℝ) :
    scaledZeroFinset t (24 / 25) (by norm_num) =
      (finiteSetOfZeros_mono (f := scaledZeta t) (r := 24 / 25) (by norm_num)
        scaledZeta_zeros_finite).toFinset :=
  Set.Finite.toFinset_inj.mpr rfl

/-- The mult-weighted count over any radius ≤ 24/25 is bounded by the
Jensen count. -/
theorem scaledZeroFinset_sum_order_le {t : ℝ} (ht : 10 ≤ |t|) {r : ℝ}
    {hr : r ≤ 1} (hr24 : r ≤ 24 / 25) :
    (∑ ρ ∈ scaledZeroFinset t r hr, (analyticOrderNatAt (scaledZeta t) ρ : ℝ)) ≤
      Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
  have hsub : scaledZeroFinset t r hr ⊆ scaledZeroFinset t (24 / 25) (by norm_num) :=
    scaledZeroFinset_subset (hr₂ := by norm_num) hr24
  have hle : ∑ ρ ∈ scaledZeroFinset t r hr, analyticOrderNatAt (scaledZeta t) ρ ≤
      ∑ ρ ∈ scaledZeroFinset t (24 / 25) (by norm_num), analyticOrderNatAt (scaledZeta t) ρ :=
    Finset.sum_le_sum_of_subset_of_nonneg hsub (fun _ _ _ => Nat.zero_le _)
  rw [← Nat.cast_sum]
  refine (Nat.cast_le.mpr hle).trans ?_
  rw [scaledZeroFinset_24_25_eq]
  exact_mod_cast scaledZeta_jensen_count ht

/-- The cardinality of the zero finset is bounded by the mult-weighted
count (each zero has order ≥ 1). -/
theorem scaledZeroFinset_card_le_sum {t : ℝ} (ht : 10 ≤ |t|) {r : ℝ}
    {hr : r ≤ 1} :
    ((scaledZeroFinset t r hr).card : ℝ) ≤
      ∑ ρ ∈ scaledZeroFinset t r hr, (analyticOrderNatAt (scaledZeta t) ρ : ℝ) := by
  have h : (scaledZeroFinset t r hr).card ≤
      ∑ ρ ∈ scaledZeroFinset t r hr, analyticOrderNatAt (scaledZeta t) ρ := by
    rw [Finset.card_eq_sum_ones]
    apply Finset.sum_le_sum
    intro w hw
    rw [mem_scaledZeroFinset] at hw
    exact one_le_analyticOrderNatAt_scaledZeta ht (hw.1.trans hr) hw.2
  calc ((scaledZeroFinset t r hr).card : ℝ)
      ≤ ↑(∑ ρ ∈ scaledZeroFinset t r hr, analyticOrderNatAt (scaledZeta t) ρ) :=
        Nat.cast_le.mpr h
    _ = ∑ ρ ∈ scaledZeroFinset t r hr, (analyticOrderNatAt (scaledZeta t) ρ : ℝ) := by
        rw [Nat.cast_sum]

/-! ## 7. The R-gap selection (×10 rescale of the midpoint pigeonhole) -/

/-- The cardinality of the 24/25-finset. -/
noncomputable def card96 (t : ℝ) : ℕ :=
  (scaledZeroFinset t (24 / 25) (by norm_num)).card

theorem card96_cast (t : ℝ) :
    (card96 t : ℝ) = ((scaledZeroFinset t (24 / 25)
      (by norm_num : (24/25:ℝ) ≤ 1)).card : ℝ) := rfl

/-- The gap scale δw = 1/(50(k+1)), k = card96. -/
noncomputable def gapD (t : ℝ) : ℝ := 1 / (50 * ((card96 t : ℝ) + 1))

theorem gapD_pos (t : ℝ) : 0 < gapD t := by
  unfold gapD
  apply div_pos (by norm_num)
  exact mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)

theorem gapD_le (t : ℝ) : gapD t ≤ 1 / 50 := by
  unfold gapD
  have hb : (0:ℝ) < 50 * ((card96 t : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  apply (div_le_div_iff_of_pos_left (by norm_num : (0:ℝ) < 1) hb
    (by norm_num : (0:ℝ) < 50)).mpr
  have hk : (0:ℝ) ≤ (card96 t : ℝ) := Nat.cast_nonneg _
  linarith

/-- **The collection radius**: R_c ∈ [2.3, 2.4] at distance ≥ 1/(20(k+1))
from every (5/2)-scaled norm of a 24/25-zero, where k is the cardinality
of the 24/25 zero finset. (Obtained by applying the unit-window midpoint
pigeonhole `exists_avoiding_midpoint` at a = 23 to the ×10-rescaled norm
finset and dividing by 10.) -/
theorem exists_collection_radius {t : ℝ} (_ht : 10 ≤ |t|) :
    ∃ R_c : ℝ, 23 / 10 ≤ R_c ∧ R_c ≤ 24 / 10 ∧
      ∀ w ∈ scaledZeroFinset t (24 / 25) (by norm_num),
        1 / (20 * (((scaledZeroFinset t (24 / 25) (by norm_num)).card : ℝ) + 1)) ≤
          |(5 / 2) * ‖w‖ - R_c| := by
  classical
  set Z96 := scaledZeroFinset t (24 / 25) (by norm_num : (24/25:ℝ) ≤ 1) with hZ96
  set S := Z96.image fun w => (5 / 2) * ‖w‖ with hS
  set S10 := S.image fun x => x * 10 with hS10
  have hcard : S10.card ≤ Z96.card := Finset.card_image_le.trans Finset.card_image_le
  obtain ⟨T, hT1, hT2, hT3⟩ := exists_avoiding_midpoint 23 S10 hcard
  refine ⟨T / 10, by linarith, by linarith, fun w hw => ?_⟩
  have hwS : (5 / 2) * ‖w‖ ∈ S := Finset.mem_image.mpr ⟨w, hw, rfl⟩
  have hwS10 : (5 / 2) * ‖w‖ * 10 ∈ S10 := Finset.mem_image.mpr ⟨_, hwS, rfl⟩
  have h := hT3 ((5 / 2) * ‖w‖ * 10) hwS10
  have h10 : (10:ℝ) = |10| := (abs_of_pos (by norm_num)).symm
  have hscale : |(5 / 2) * ‖w‖ * 10 - T| = 10 * |(5 / 2) * ‖w‖ - T / 10| := by
    rw [h10, ← abs_mul]
    congr 1
    ring
  rw [hscale] at h
  have hpos2 : (0:ℝ) < 2 * ((Z96.card : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  have h1 := (div_le_iff₀ hpos2).mp h
  have h2 : 10 * |(5 / 2) * ‖w‖ - T / 10| * (2 * ((Z96.card : ℝ) + 1))
      = |(5 / 2) * ‖w‖ - T / 10| * (20 * ((Z96.card : ℝ) + 1)) := by ring
  rw [h2] at h1
  have hpos : (0:ℝ) < 20 * ((Z96.card : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  exact (div_le_iff₀ hpos).mpr h1

/-- The chosen collection radius. -/
noncomputable def collRadius {t : ℝ} (ht : 10 ≤ |t|) : ℝ :=
  (exists_collection_radius ht).choose

theorem collRadius_ge {t : ℝ} (ht : 10 ≤ |t|) : 23 / 10 ≤ collRadius ht :=
  ((exists_collection_radius ht).choose_spec).1

theorem collRadius_le {t : ℝ} (ht : 10 ≤ |t|) : collRadius ht ≤ 24 / 10 :=
  ((exists_collection_radius ht).choose_spec).2.1

theorem collRadius_gap {t : ℝ} (ht : 10 ≤ |t|)
    {w : ℂ} (hw : w ∈ scaledZeroFinset t (24 / 25) (by norm_num)) :
    1 / (20 * (((scaledZeroFinset t (24 / 25) (by norm_num)).card : ℝ) + 1)) ≤
      |(5 / 2) * ‖w‖ - collRadius ht| :=
  ((exists_collection_radius ht).choose_spec).2.2 w hw

/-- The scaled collection radius r_c = (2/5)·R_c ∈ [23/25, 24/25]. -/
noncomputable def rC {t : ℝ} (ht : 10 ≤ |t|) : ℝ := collRadius ht * (2 / 5)

theorem rC_ge {t : ℝ} (ht : 10 ≤ |t|) : 23 / 25 ≤ rC ht := by
  have h := collRadius_ge ht
  unfold rC
  linarith

theorem rC_le {t : ℝ} (ht : 10 ≤ |t|) : rC ht ≤ 24 / 25 := by
  have h := collRadius_le ht
  unfold rC
  linarith

theorem rC_pos {t : ℝ} (ht : 10 ≤ |t|) : 0 < rC ht :=
  (by norm_num : (0:ℝ) < 23 / 25).trans_le (rC_ge ht)

theorem rC_lt_one {t : ℝ} (ht : 10 ≤ |t|) : rC ht < 1 := (rC_le ht).trans_lt (by norm_num)

/-- The gap in the w-scale: every 24/25-zero has norm at distance ≥ gapD
from r_c. -/
theorem rC_gap {t : ℝ} (ht : 10 ≤ |t|)
    {w : ℂ} (hw : w ∈ scaledZeroFinset t (24 / 25) (by norm_num)) :
    gapD t ≤ |‖w‖ - rC ht| := by
  have h := collRadius_gap ht hw
  have hscale : (5 / 2) * ‖w‖ - collRadius ht = (5 / 2) * (‖w‖ - rC ht) := by
    unfold rC
    ring
  rw [hscale, abs_mul, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)] at h
  have hpos20 : (0:ℝ) < 20 * (((scaledZeroFinset t (24 / 25)
      (by norm_num : (24/25:ℝ) ≤ 1)).card : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  have h2 := (div_le_iff₀ hpos20).mp h
  have hcast := card96_cast t
  unfold gapD
  rw [hcast]
  have hpos50 : (0:ℝ) < 50 * (((scaledZeroFinset t (24 / 25)
      (by norm_num : (24/25:ℝ) ≤ 1)).card : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  rw [div_le_iff₀ hpos50]
  calc (1 : ℝ) ≤ (5 / 2) * |‖w‖ - rC ht| *
        (20 * (((scaledZeroFinset t (24 / 25) (by norm_num)).card : ℝ) + 1)) := h2
    _ = |‖w‖ - rC ht| *
        (50 * (((scaledZeroFinset t (24 / 25) (by norm_num)).card : ℝ) + 1)) := by ring

/-- The collected zeros: norm ≤ r_c. -/
noncomputable def collZeros {t : ℝ} (ht : 10 ≤ |t|) : Finset ℂ :=
  scaledZeroFinset t (rC ht) (rC_lt_one ht).le

theorem mem_collZeros {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} :
    w ∈ collZeros ht ↔ ‖w‖ ≤ rC ht ∧ scaledZeta t w = 0 :=
  mem_scaledZeroFinset

/-- Collected zeros lie strictly inside: ‖w‖ ≤ r_c − gapD. -/
theorem collZeros_norm_le {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} (hw : w ∈ collZeros ht) :
    ‖w‖ ≤ rC ht - gapD t := by
  have hmem := (mem_collZeros ht).mp hw
  have hw96 : w ∈ scaledZeroFinset t (24 / 25) (by norm_num) :=
    scaledZeroFinset_subset (hr₂ := by norm_num) (rC_le ht) hw
  have hgap := rC_gap ht hw96
  have hle : ‖w‖ ≤ rC ht := hmem.1
  have hX : ‖w‖ - rC ht ≤ 0 := sub_nonpos.mpr hle
  rw [abs_of_nonpos hX] at hgap
  have hδ := gapD_pos t
  linarith

/-- The mult-weighted count over the collected zeros, as a natural. -/
noncomputable def collMultSum {t : ℝ} (ht : 10 ≤ |t|) : ℕ :=
  ∑ ρ ∈ collZeros ht, analyticOrderNatAt (scaledZeta t) ρ

/-! ## 8. The Blaschke quotient g = Cf r_c F -/

/-- The product over the collected zeros, P(w) = ∏ (w−ρ)^{m_ρ}. -/
noncomputable def collProd {t : ℝ} (ht : 10 ≤ |t|) (w : ℂ) : ℂ :=
  ∏ ρ ∈ collZeros ht, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ

/-- Off the collected zero set, the Blaschke quotient Cf is F/P. -/
theorem Cf_eq_div_collProd {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : w ∉ SetOfZeros (rC ht) (scaledZeta t)) :
    Cf (rC ht) (scaledZeta t) w = scaledZeta t w / collProd ht w := by
  classical
  have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=
    scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by
      obtain ⟨h1, h2⟩ := hx
      exact ⟨h1.trans (rC_lt_one ht).le, h2⟩
  unfold Cf collProd
  simp only [hfin, ↓reduceDIte]
  rw [dif_neg hw]
  apply congrArg (fun X => scaledZeta t w / X)
  exact Finset.prod_congr (Set.Finite.toFinset_inj.mpr rfl) (fun _ _ => rfl)

/-- At a collected zero, Cf is the zero-factor cofactor over the remaining
product. -/
theorem Cf_eq_zeroFactor_div {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : w ∈ SetOfZeros (rC ht) (scaledZeta t)) :
    Cf (rC ht) (scaledZeta t) w = ZeroFactor (scaledZeta t) w /
      ∏ ρ ∈ collZeros ht \ {w}, (w - ρ) ^ analyticOrderNatAt (scaledZeta t) ρ := by
  classical
  have hfin : (SetOfZeros (rC ht) (scaledZeta t)).Finite :=
    scaledZeta_zeros_finite.subset (t := SetOfZeros (rC ht) (scaledZeta t)) fun x hx => by
      obtain ⟨h1, h2⟩ := hx
      exact ⟨h1.trans (rC_lt_one ht).le, h2⟩
  unfold Cf
  simp only [hfin, ↓reduceDIte]
  rw [dif_pos hw]
  apply congrArg (fun X => ZeroFactor (scaledZeta t) w / X)
  apply Finset.prod_congr _ (fun _ _ => rfl)
  congr 1

/-- g is analytic on a closed disc slightly larger than closedBall(0, r_c). -/
theorem Cf_collZeros_analytic {t : ℝ} (ht : 10 ≤ |t|) :
    AnalyticOnNhd ℂ (Cf (rC ht) (scaledZeta t))
      (Metric.closedBall 0 ((1 + rC ht) / 2)) := by
  apply CfAnalytic
  · have h1 := rC_lt_one ht
    linarith [rC_pos ht]
  · have h1 := rC_lt_one ht
    linarith
  · exact scaledZeta_analytic ht
  · rw [scaledZeta_zero]
    exact one_ne_zero

/-- g is nonvanishing on closedBall(0, r_c). -/
theorem Cf_collZeros_ne_zero {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : w ∈ Metric.closedBall 0 (rC ht)) :
    Cf (rC ht) (scaledZeta t) w ≠ 0 := by
  rw [Metric.mem_closedBall, dist_zero_right] at hw
  by_cases h0 : scaledZeta t w = 0
  · have hwS : w ∈ SetOfZeros (rC ht) (scaledZeta t) := ⟨hw, h0⟩
    rw [Cf_eq_zeroFactor_div ht hwS]
    apply div_ne_zero
    · obtain ⟨h_w, h_w_an, h_w_ne, hZF, _⟩ := ZeroFactorization (rC_lt_one ht)
        (scaledZeta_analytic ht) (by rw [scaledZeta_zero]; exact one_ne_zero) hwS
      rw [hZF]
      exact h_w_ne
    · apply Finset.prod_ne_zero_iff.mpr
      intro ρ hρ
      have hρne : ρ ≠ w := fun h => (Finset.mem_sdiff.mp hρ).2 (Finset.mem_singleton.mpr h)
      exact pow_ne_zero _ (sub_ne_zero.mpr hρne.symm)
  · have hwS : w ∉ SetOfZeros (rC ht) (scaledZeta t) := fun h => h0 h.2
    rw [Cf_eq_div_collProd ht hwS]
    apply div_ne_zero h0
    unfold collProd
    apply Finset.prod_ne_zero_iff.mpr
    intro ρ hρ
    have hρ0 : scaledZeta t ρ = 0 := ((mem_collZeros ht).mp hρ).2
    exact pow_ne_zero _ (sub_ne_zero.mpr (fun h => h0 (by rw [h]; exact hρ0)))

/-- At the center, log‖g(0)‖ ≥ 0 (since g(0) = 1/∏(−ρ)^{m_ρ} and each
‖ρ‖ ≤ r_c < 1). -/
theorem Cf_collZeros_log_norm_zero_nonneg {t : ℝ} (ht : 10 ≤ |t|) :
    0 ≤ Real.log ‖Cf (rC ht) (scaledZeta t) 0‖ := by
  have h0S : (0:ℂ) ∉ SetOfZeros (rC ht) (scaledZeta t) := by
    intro h
    have h2 := h.2
    rw [scaledZeta_zero] at h2
    exact one_ne_zero h2
  rw [Cf_eq_div_collProd ht h0S, scaledZeta_zero]
  have hprod_norm : ‖collProd ht 0‖
      = ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by
    unfold collProd
    rw [norm_prod]
    apply Finset.prod_congr rfl
    intro ρ hρ
    rw [zero_sub, norm_pow, norm_neg]
  have hfac : ∀ ρ ∈ collZeros ht,
      0 < ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by
    intro ρ hρ
    have hρ0 : scaledZeta t ρ = 0 := ((mem_collZeros ht).mp hρ).2
    have hne : ρ ≠ 0 := by
      intro h
      rw [h, scaledZeta_zero] at hρ0
      exact one_ne_zero hρ0
    exact pow_pos (norm_pos_iff.mpr hne) _
  have hprod_pos : 0 < ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ :=
    Finset.prod_pos hfac
  have hprod_le : ∏ ρ ∈ collZeros ht, ‖ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ ≤ 1 := by
    apply Finset.prod_le_one (fun ρ hρ => (hfac ρ hρ).le)
    intro ρ hρ
    have hnorm : ‖ρ‖ ≤ 1 :=
      (((mem_collZeros ht).mp hρ).1.trans (rC_le ht)).trans (by norm_num)
    exact pow_le_one₀ (norm_nonneg _) hnorm
  rw [norm_div, norm_one, hprod_norm,
    Real.log_div one_ne_zero (ne_of_gt hprod_pos), Real.log_one, zero_sub]
  exact neg_nonneg.mpr (Real.log_nonpos hprod_pos.le hprod_le)

/-- **The outer-circle bound**: on the sphere ‖w‖ = r_c (which carries no
zeros, by the gap), ‖g(w)‖ ≤ (9/4)|t|² · gapD^{−M_c}. -/
theorem Cf_collZeros_norm_le_sphere {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : ‖w‖ = rC ht) :
    ‖Cf (rC ht) (scaledZeta t) w‖ ≤
      (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by
  have hδ := gapD_pos t
  have hwS : w ∉ SetOfZeros (rC ht) (scaledZeta t) := by
    intro hmem
    have hmemZ : w ∈ collZeros ht := (mem_collZeros ht).mpr ⟨hmem.1, hmem.2⟩
    have hle := collZeros_norm_le ht hmemZ
    rw [hw] at hle
    linarith
  rw [Cf_eq_div_collProd ht hwS, norm_div]
  have hF : ‖scaledZeta t w‖ ≤ (9 / 4) * |t| ^ 2 :=
    norm_scaledZeta_le ht (by rw [hw]; exact (rC_le ht).trans (by norm_num))
  -- the product is ≥ gapD^{M_c}
  have hP : gapD t ^ collMultSum ht ≤ ‖collProd ht w‖ := by
    have hstep : ∏ ρ ∈ collZeros ht, gapD t ^ analyticOrderNatAt (scaledZeta t) ρ
        ≤ ∏ ρ ∈ collZeros ht, ‖w - ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := by
      apply Finset.prod_le_prod (fun ρ _ => pow_nonneg hδ.le _)
      intro ρ hρ
      have hρle := collZeros_norm_le ht hρ
      have hd : gapD t ≤ ‖w - ρ‖ := by
        have h1 : ‖w‖ - ‖ρ‖ ≤ ‖w - ρ‖ := norm_sub_norm_le w ρ
        rw [hw] at h1
        linarith
      exact pow_le_pow_left₀ hδ.le hd _
    rw [Finset.prod_pow_eq_pow_sum] at hstep
    calc gapD t ^ collMultSum ht
        = gapD t ^ (∑ ρ ∈ collZeros ht, analyticOrderNatAt (scaledZeta t) ρ) := rfl
      _ ≤ ∏ ρ ∈ collZeros ht, ‖w - ρ‖ ^ analyticOrderNatAt (scaledZeta t) ρ := hstep
      _ = ‖collProd ht w‖ := by
          unfold collProd
          rw [norm_prod]
          apply Finset.prod_congr rfl
          intro ρ hρ
          rw [norm_pow]
  have hPpos : 0 < gapD t ^ collMultSum ht := pow_pos hδ _
  have hXnn : (0:ℝ) ≤ (9 / 4) * |t| ^ 2 := by positivity
  have hnormP : 0 < ‖collProd ht w‖ := hPpos.trans_le hP
  rw [div_le_div_iff₀ hnormP hPpos]
  nlinarith [hF, hP, hPpos, hXnn, norm_nonneg (scaledZeta t w),
    mul_nonneg hXnn (sub_nonneg.mpr hP),
    mul_nonneg (sub_nonneg.mpr hF) hPpos.le]

/-- The bound propagates to the closed ball by the maximum principle. -/
theorem Cf_collZeros_norm_le_ball {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ}
    (hw : w ∈ Metric.closedBall 0 (rC ht)) :
    ‖Cf (rC ht) (scaledZeta t) w‖ ≤
      (9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht := by
  apply AnalyticOn.norm_le_of_norm_le_on_sphere (r := rC ht) (R := (1 + rC ht) / 2)
  · have h1 := rC_lt_one ht
    linarith [rC_pos ht]
  · exact (Cf_collZeros_analytic ht).analyticOn
  · intro z hz
    rw [mem_sphere_iff_norm, sub_zero] at hz
    exact Cf_collZeros_norm_le_sphere ht hz
  · exact hw

/-! ## 9. The elementary constant fold (real-analysis lemmas) -/

/-- log(9/4) ≤ 1 since 9/4 ≤ e. -/
theorem log_9_4_le_one : Real.log (9 / 4) ≤ 1 := by
  rw [Real.log_le_iff_le_exp (by norm_num : (0:ℝ) < 9 / 4)]
  calc (9 / 4 : ℝ) ≤ 2.7182818283 := by norm_num
    _ ≤ Real.exp 1 := Real.exp_one_gt_d9.le

/-- log(33/32) ≥ 1/33 (from log x ≥ 1 − 1/x). -/
theorem log_33_32_ge : (1 / 33 : ℝ) ≤ Real.log (33 / 32) := by
  have h := Real.one_sub_inv_le_log_of_pos (by norm_num : (0:ℝ) < 33 / 32)
  norm_num at h
  exact h

/-- 2 ≤ log|t| for |t| ≥ 10 (since e² < 2.719² < 10). -/
theorem two_le_log_abs_t {t : ℝ} (ht : 10 ≤ |t|) : (2:ℝ) ≤ Real.log |t| := by
  have h1 : Real.exp 2 ≤ 10 := by
    have he : Real.exp 1 ≤ 2.7182818286 := Real.exp_one_lt_d9.le
    have h2 : Real.exp 2 = Real.exp 1 ^ 2 := by
      rw [show (2:ℝ) = (2:ℕ) * 1 by norm_num, Real.exp_nat_mul]
    rw [h2]
    nlinarith [he, Real.exp_pos 1]
  rw [Real.le_log_iff_exp_le (by positivity : (0:ℝ) < |t|)]
  exact h1.trans ht

/-- The Jensen bound in elementary form. -/
theorem jensen_bound_elementary {t : ℝ} (ht : 10 ≤ |t|) :
    Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) ≤ 33 + 66 * Real.log |t| := by
  have hL := two_le_log_abs_t ht
  have hnum : Real.log ((9 / 4) * |t| ^ 2) ≤ 1 + 2 * Real.log |t| := by
    rw [Real.log_mul (by norm_num) (by positivity), Real.log_pow]
    linarith [log_9_4_le_one]
  have hnum0 : (0:ℝ) ≤ Real.log ((9 / 4) * |t| ^ 2) := by
    apply Real.log_nonneg
    have hsq : (10:ℝ) ^ 2 ≤ |t| ^ 2 := (sq_le_sq₀ (by norm_num) (abs_nonneg t)).mpr ht
    nlinarith
  have hden := log_33_32_ge
  have hden0 : (0:ℝ) < Real.log (33 / 32) := lt_of_lt_of_le (by norm_num) hden
  calc Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32)
      ≤ (1 + 2 * Real.log |t|) / (1 / 33) := by
        rw [div_le_div_iff₀ hden0 (by norm_num : (0:ℝ) < 1 / 33)]
        have h12 : (0:ℝ) ≤ 1 + 2 * Real.log |t| := by linarith
        have h1 := mul_le_mul_of_nonneg_right hnum (by norm_num : (0:ℝ) ≤ 1 / 33)
        have h2 := mul_le_mul_of_nonneg_left hden h12
        nlinarith [h1, h2]
      _ = 33 + 66 * Real.log |t| := by ring

/-- The 24/25 zero count is at most the elementary Jensen bound. -/
theorem card96_le {t : ℝ} (ht : 10 ≤ |t|) : (card96 t : ℝ) ≤ 33 + 66 * Real.log |t| :=
  ((scaledZeroFinset_card_le_sum (t := t) ht (r := 24 / 25) (hr := by norm_num)).trans
    (scaledZeroFinset_sum_order_le (t := t) ht (r := 24 / 25) (hr := by norm_num)
      (le_refl _))).trans (jensen_bound_elementary ht)

/-- The collected mult-weighted count is at most the elementary Jensen bound. -/
theorem collMultSum_le {t : ℝ} (ht : 10 ≤ |t|) :
    (collMultSum ht : ℝ) ≤ 33 + 66 * Real.log |t| := by
  have h1 := scaledZeroFinset_sum_order_le (t := t) ht (r := rC ht) (hr := (rC_lt_one ht).le)
    (rC_le ht)
  calc (collMultSum ht : ℝ)
      = ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℝ) := by
        unfold collMultSum
        rw [Nat.cast_sum]
    _ ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := h1
    _ ≤ 33 + 66 * Real.log |t| := jensen_bound_elementary ht

/-- log(50(k+1)) ≤ log|t| + 8 (since 50(k+1) ≤ 4150·log|t| and
log 4150 ≤ 9, log(log|t|) ≤ log|t| − 1). -/
theorem log_50_card_le {t : ℝ} (ht : 10 ≤ |t|) :
    Real.log (50 * ((card96 t : ℝ) + 1)) ≤ Real.log |t| + 8 := by
  have hL := two_le_log_abs_t ht
  have hJc := card96_le ht
  have h1 : 50 * ((card96 t : ℝ) + 1) ≤ 4150 * Real.log |t| := by nlinarith [hJc, hL]
  have hpos1 : (0:ℝ) < 50 * ((card96 t : ℝ) + 1) :=
    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)
  have h2 : Real.log (50 * ((card96 t : ℝ) + 1)) ≤ Real.log (4150 * Real.log |t|) :=
    Real.log_le_log hpos1 h1
  rw [Real.log_mul (by norm_num) (by linarith : (0:ℝ) < Real.log |t|).ne'] at h2
  have h3 : Real.log (4150 : ℝ) ≤ 9 := by
    rw [Real.log_le_iff_le_exp (by norm_num)]
    have he : (2.71:ℝ) ≤ Real.exp 1 :=
      (by norm_num : (2.71:ℝ) ≤ 2.7182818283).trans Real.exp_one_gt_d9.le
    have h9 : Real.exp 9 = Real.exp 1 ^ 9 := by
      rw [show (9:ℝ) = (9:ℕ) * 1 by norm_num, Real.exp_nat_mul]
    rw [h9]
    calc (4150:ℝ) ≤ 2.71 ^ 9 := by norm_num
      _ ≤ Real.exp 1 ^ 9 := pow_le_pow_left₀ (by norm_num) he 9
  have h4 : Real.log (Real.log |t|) ≤ Real.log |t| - 1 :=
    Real.log_le_sub_one_of_pos (by linarith : (0:ℝ) < Real.log |t|)
  linarith [h2, h3, h4]

/-- **The M-bound fold**: log of the |g|-bound ≤ 420·(log|t|)². -/
theorem Mbound_le {t : ℝ} (ht : 10 ≤ |t|) :
    Real.log ((9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht) ≤
      420 * (Real.log |t|) ^ 2 := by
  have hL := two_le_log_abs_t ht
  have hJM := collMultSum_le ht
  have hlogδ := log_50_card_le ht
  have hlog_expand : Real.log ((9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht)
      = Real.log ((9 / 4) * |t| ^ 2) +
        (collMultSum ht : ℝ) * Real.log (50 * ((card96 t : ℝ) + 1)) := by
    have hX : (9 / 4) * |t| ^ 2 ≠ 0 := by positivity
    have hδM : gapD t ^ collMultSum ht ≠ 0 := pow_ne_zero _ (gapD_pos t).ne'
    have hδe : Real.log (gapD t) = - Real.log (50 * ((card96 t : ℝ) + 1)) := by
      unfold gapD
      rw [Real.log_div one_ne_zero (mul_pos (by norm_num)
        (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)).ne']
      rw [Real.log_one, zero_sub]
    rw [Real.log_div hX hδM, Real.log_pow, hδe]
    ring
  rw [hlog_expand]
  have hnum : Real.log ((9 / 4) * |t| ^ 2) ≤ 1 + 2 * Real.log |t| := by
    rw [Real.log_mul (by norm_num) (by positivity), Real.log_pow]
    linarith [log_9_4_le_one]
  have hlogδ0 : (0:ℝ) ≤ Real.log (50 * ((card96 t : ℝ) + 1)) := by
    apply Real.log_nonneg
    have hk : (0:ℝ) ≤ (card96 t : ℝ) := Nat.cast_nonneg _
    nlinarith
  have hJ0 : (0:ℝ) ≤ 33 + 66 * Real.log |t| := by nlinarith [hL]
  have hstep := add_le_add hnum (mul_le_mul hJM hlogδ hlogδ0 hJ0)
  refine hstep.trans ?_
  have hprod : (0:ℝ) ≤ (Real.log |t| - 2) * (354 * Real.log |t| + 131) :=
    mul_nonneg (sub_nonneg.mpr hL) (by nlinarith [hL])
  nlinarith [hprod, hL]

/-! ## 10. The near-zero finset and the affine push-forward -/

/-- The nontrivial zeros in the open unit ordinate window about t. -/
def nearZeros (t : ℝ) : Finset ℂ :=
  (zeroDiscFinset t).filter fun ρ => |ρ.im - t| < 1

theorem mem_nearZeros {t : ℝ} {ρ : ℂ} :
    ρ ∈ nearZeros t ↔ ρ ∈ zeroDiscFinset t ∧ |ρ.im - t| < 1 := Finset.mem_filter

/-- The affine map is injective. -/
theorem affMap_injOn {t : ℝ} (s : Finset ℂ) :
    Set.InjOn (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) s :=
  fun a _ b _ hab => mul_left_cancel₀ (by norm_num : (5 / 2 : ℂ) ≠ 0) (add_left_cancel hab)

/-- zeroMult at the affine image equals the scaled order. -/
theorem zeroMult_affMap {t : ℝ} (ht : 10 ≤ |t|) {w : ℂ} (hw : w ∈ collZeros ht) :
    zeroMult (discCenter t + (5 / 2 : ℂ) * w) = analyticOrderNatAt (scaledZeta t) w := by
  have h := analyticOrderNatAt_scaledZeta ht
    (((mem_collZeros ht).mp hw).1.trans (rC_lt_one ht).le)
  rw [h]
  rfl

/-- The pushed-forward sum over the image equals the collected sum. -/
theorem sum_image_zeroMult_div {t : ℝ} (ht : 10 ≤ |t|) (g : ℂ → ℂ) :
    ∑ ρ ∈ (collZeros ht).image (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w), g ρ
      = ∑ w ∈ collZeros ht, g (discCenter t + (5 / 2 : ℂ) * w) :=
  Finset.sum_image (affMap_injOn _)

/-- Every near zero lies in the affine image of the collected zeros. -/
theorem nearZeros_subset_image {t : ℝ} (ht : 10 ≤ |t|) :
    nearZeros t ⊆ (collZeros ht).image (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) := by
  classical
  intro ρ hρ
  rw [mem_nearZeros] at hρ
  obtain ⟨hρdisc, hρim⟩ := hρ
  have hρnt : IsNontrivialZero ρ := zeroDisc_isNontrivial hρdisc
  have hρ0 : riemannZeta ρ = 0 := hρnt.1
  have hnorm1 : ‖ρ - discCenter t‖ ≤ Real.sqrt 5 := by
    have hsq : Complex.normSq (ρ - discCenter t) ≤ 5 := by
      rw [Complex.normSq_apply]
      have hre : (ρ - discCenter t).re = ρ.re - 2 := by
        simp [discCenter, sub_re, add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]
      have him : (ρ - discCenter t).im = ρ.im - t := by
        simp [discCenter, sub_im, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im]
      have h1 : (ρ.re - 2) ^ 2 ≤ 4 := by
        have h2 : |ρ.re - 2| ≤ 2 := by
          rw [abs_le]
          constructor <;> linarith [hρnt.2.1, hρnt.2.2]
        calc (ρ.re - 2) ^ 2 = |ρ.re - 2| ^ 2 := by rw [sq_abs]
          _ ≤ 2 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) h2 _
          _ = 4 := by norm_num
      have h2 : (ρ.im - t) ^ 2 ≤ 1 := by
        have h3 : |ρ.im - t| ≤ 1 := hρim.le
        calc (ρ.im - t) ^ 2 = |ρ.im - t| ^ 2 := by rw [sq_abs]
          _ ≤ 1 ^ 2 := pow_le_pow_left₀ (abs_nonneg _) h3 2
          _ = 1 := by norm_num
      rw [hre, him]
      nlinarith [h1, h2]
    have h4 : ‖ρ - discCenter t‖ ^ 2 ≤ 5 := by
      rw [← Complex.normSq_eq_norm_sq]
      exact hsq
    calc ‖ρ - discCenter t‖ = Real.sqrt (‖ρ - discCenter t‖ ^ 2) :=
          (Real.sqrt_sq (norm_nonneg _)).symm
      _ ≤ Real.sqrt 5 := Real.sqrt_le_sqrt h4
  have h52 : Real.sqrt 5 ≤ 23 / 10 := by
    have h1 : Real.sqrt 5 ≤ Real.sqrt ((23 / 10) ^ 2) := Real.sqrt_le_sqrt (by norm_num)
    rwa [Real.sqrt_sq (by norm_num)] at h1
  have h25 : ‖(2 / 5 : ℂ)‖ = 2 / 5 := by
    rw [show (2 / 5 : ℂ) = ((2 / 5 : ℝ) : ℂ) by norm_num, Complex.norm_real,
      Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 2 / 5)]
  refine Finset.mem_image.mpr ⟨(2 / 5 : ℂ) * (ρ - discCenter t), ?_, ?_⟩
  · rw [mem_collZeros ht]
    constructor
    · rw [norm_mul, h25]
      calc (2 / 5 : ℝ) * ‖ρ - discCenter t‖ ≤ (2 / 5) * (23 / 10) :=
            mul_le_mul_of_nonneg_left (hnorm1.trans h52) (by norm_num)
        _ = 23 / 25 := by norm_num
        _ ≤ rC ht := rC_ge ht
    · unfold scaledZeta
      rw [show discCenter t + (5 / 2 : ℂ) * ((2 / 5 : ℂ) * (ρ - discCenter t)) = ρ by ring,
        hρ0, zero_div]
  · ring

/-- The image-sum of zeroMult is the collected mult-weighted count. -/
theorem sum_image_zeroMult_le {t : ℝ} (ht : 10 ≤ |t|) :
    ∑ ρ ∈ (collZeros ht).image (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w),
        (zeroMult ρ : ℝ)
      ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
  classical
  rw [Finset.sum_image (affMap_injOn _)]
  calc ∑ w ∈ collZeros ht, (zeroMult (discCenter t + (5 / 2 : ℂ) * w) : ℝ)
      = ∑ w ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) w : ℝ) :=
        Finset.sum_congr rfl fun w hw => by rw [zeroMult_affMap ht hw]
    _ = (collMultSum ht : ℝ) := by
        unfold collMultSum
        rw [Nat.cast_sum]
    _ ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
        unfold collMultSum
        rw [Nat.cast_sum]
        exact scaledZeroFinset_sum_order_le (t := t) ht (r := rC ht)
          (hr := (rC_lt_one ht).le) (rC_le ht)

/-! ## 11. The loose R-bound (ii′-5c capstone) -/

/-- **The loose Davenport-disc R-bound** (ii′-5c, D-067 §6): on
σ ∈ [1/2, 7/2], |t| ≥ 10, the log-derivative of ζ minus its near-zero
sum is O((log|t|)²) with the deliberately loose constant 100000. This is
the GROWTH INPUT for the partial-fraction identity (ii′-5e); the tight
constants come from the identity's analysis (ii′-5f). -/
theorem logDeriv_riemannZeta_sub_nearZeros_le {t : ℝ} (ht : 10 ≤ |t|) {s : ℂ}
    (hsim : s.im = t) (hσlo : 1 / 2 ≤ s.re) (hσhi : s.re ≤ 7 / 2)
    (hs0 : riemannZeta s ≠ 0) :
    ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖
      ≤ 100000 * (Real.log |t|) ^ 2 := by
  classical
  set w₀ : ℂ := (2 / 5 : ℂ) * (s - discCenter t) with hw₀def
  have haff : discCenter t + (5 / 2 : ℂ) * w₀ = s := by rw [hw₀def]; ring
  have hw₀norm : ‖w₀‖ ≤ 3 / 5 := by
    have hsnorm : ‖s - discCenter t‖ = |s.re - 2| := by
      have heq : s - discCenter t = ((s.re - 2 : ℝ) : ℂ) := by
        apply Complex.ext_iff.mpr
        constructor
        · simp [discCenter, sub_re, add_re, mul_re, ofReal_re, ofReal_im, I_re, I_im]
        · simp [discCenter, sub_im, add_im, mul_im, ofReal_re, ofReal_im, I_re, I_im, hsim]
      rw [heq, Complex.norm_real, Real.norm_eq_abs]
    have h25 : ‖(2 / 5 : ℂ)‖ = 2 / 5 := by
      rw [show (2 / 5 : ℂ) = ((2 / 5 : ℝ) : ℂ) by norm_num, Complex.norm_real,
        Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 2 / 5)]
    rw [hw₀def, norm_mul, h25, hsnorm]
    have hσ : |s.re - 2| ≤ 3 / 2 := by
      rw [abs_le]
      constructor <;> linarith
    calc (2 / 5 : ℝ) * |s.re - 2| ≤ (2 / 5) * (3 / 2) :=
          mul_le_mul_of_nonneg_left hσ (by norm_num)
      _ = 3 / 5 := by norm_num
  have hζs0 : riemannZeta (discCenter t) ≠ 0 := by
    have h := RvM.zeta_lower_bound_two t
    intro h0
    rw [← show discCenter t = 2 + t * Complex.I from rfl, h0, norm_zero] at h
    norm_num at h
  have hFw₀ : scaledZeta t w₀ ≠ 0 := by
    unfold scaledZeta
    rw [haff]
    exact div_ne_zero hs0 hζs0
  have hw₀notmem : w₀ ∉ SetOfZeros (rC ht) (scaledZeta t) := fun h => hFw₀ h.2
  have hZclosed : IsClosed (SetOfZeros (rC ht) (scaledZeta t)) := by
    have hset : SetOfZeros (rC ht) (scaledZeta t) = ↑(collZeros ht) := by
      ext x
      rw [Finset.mem_coe, mem_collZeros ht]
      exact Iff.rfl
    rw [hset]
    exact (collZeros ht).finite_toSet.isClosed
  have hEv1 : ∀ᶠ w in 𝓝 w₀, w ∉ SetOfZeros (rC ht) (scaledZeta t) :=
    hZclosed.isOpen_compl.mem_nhds hw₀notmem
  have hB_eq : Cf (rC ht) (scaledZeta t) =ᶠ[𝓝 w₀]
      fun w => scaledZeta t w / collProd ht w := by
    filter_upwards [hEv1] with w hw1
    exact Cf_eq_div_collProd ht hw1
  have hF_an : AnalyticAt ℂ (scaledZeta t) w₀ :=
    scaledZeta_analytic ht w₀ (by
      rw [Metric.mem_closedBall, dist_zero_right]
      exact hw₀norm.trans (by norm_num))
  have hP_an : AnalyticAt ℂ (collProd ht) w₀ := analyticAt_finset_prod_sub_pow _ _ _
  have hP_ne : collProd ht w₀ ≠ 0 := by
    unfold collProd
    apply Finset.prod_ne_zero_iff.mpr
    intro ρ hρ
    have hρ0 : scaledZeta t ρ = 0 := ((mem_collZeros ht).mp hρ).2
    exact pow_ne_zero _ (sub_ne_zero.mpr (fun h => hFw₀ (by rw [h]; exact hρ0)))
  have hlogB : logDeriv (fun w => scaledZeta t w / collProd ht w) w₀
      = logDeriv (scaledZeta t) w₀ - logDeriv (collProd ht) w₀ :=
    logDeriv_div w₀ hFw₀ hP_ne hF_an.differentiableAt hP_an.differentiableAt
  have hsne1 : s ≠ 1 := by
    intro h1
    rw [h1, Complex.one_im] at hsim
    rw [← hsim, abs_zero] at ht
    norm_num at ht
  have hζs_diff : DifferentiableAt ℂ riemannZeta s :=
    (analyticAt_riemannZeta_of_ne_one hsne1).differentiableAt
  have hζs_diff' : DifferentiableAt ℂ riemannZeta (discCenter t + (5 / 2 : ℂ) * w₀) :=
    haff.symm ▸ hζs_diff
  have haff_diff : DifferentiableAt ℂ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ := by
    fun_prop
  have hderiv_aff : deriv (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ = 5 / 2 := by
    have h1 : (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w)
        = fun w => (5 / 2 : ℂ) * w + discCenter t := funext fun w => by ring
    rw [h1, deriv_add_const]
    show deriv (fun w : ℂ => (5 / 2 : ℂ) * id w) w₀ = 5 / 2
    rw [deriv_const_mul (5 / 2 : ℂ) differentiableAt_id, deriv_id']
    simp
  have hlogF : logDeriv (scaledZeta t) w₀ = (5 / 2 : ℂ) * logDeriv riemannZeta s := by
    have hFeq : scaledZeta t = fun w : ℂ =>
        (riemannZeta ∘ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w)) w /
          riemannZeta (discCenter t) := funext fun w => rfl
    rw [hFeq]
    have hga : (riemannZeta ∘ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w)) w₀ ≠ 0 := by
      rw [Function.comp_apply, haff]
      exact hs0
    rw [logDeriv_div w₀ hga hζs0 (hζs_diff'.comp w₀ haff_diff) (differentiableAt_const _)]
    have hlogconst : logDeriv (fun _ : ℂ => riemannZeta (discCenter t)) w₀ = 0 := by
      rw [logDeriv_apply, deriv_const, zero_div]
    have hlogcomp : logDeriv (riemannZeta ∘ (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w)) w₀
        = logDeriv riemannZeta ((fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀) *
          deriv (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) w₀ :=
      logDeriv_comp hζs_diff' haff_diff
    rw [hlogcomp, hlogconst, sub_zero, hderiv_aff]
    show logDeriv riemannZeta (discCenter t + (5 / 2 : ℂ) * w₀) * (5 / 2 : ℂ) = _
    rw [haff]
    ring
  have hlogP : logDeriv (collProd ht) w₀
      = ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℂ) / (w₀ - ρ) := by
    unfold collProd
    rw [logDeriv_prod (fun ρ hρ => pow_ne_zero _ (sub_ne_zero.mpr (fun h => hFw₀ (by
        rw [h]; exact ((mem_collZeros ht).mp hρ).2))))
      (fun ρ hρ => ((analyticAt_id.sub analyticAt_const).pow _).differentiableAt)]
    apply Finset.sum_congr rfl
    intro ρ hρ
    rw [logDeriv_fun_pow (differentiableAt_id.sub (differentiableAt_const _))]
    rw [logDeriv_apply]
    have hd : deriv (fun w : ℂ => w - ρ) w₀ = 1 := by
      rw [deriv_sub_const, deriv_id'']
    rw [hd, mul_one_div]
  obtain ⟨J_B, hJ_an, hJ0, hJderiv, hJre⟩ :=
    LogOfAnalyticFunction (r := 3 / 5) (R := rC ht) (B := Cf (rC ht) (scaledZeta t))
      (by norm_num) (by linarith [rC_ge ht])
      ((Cf_collZeros_analytic ht).mono (Metric.closedBall_subset_closedBall (by
        have h1 := rC_lt_one ht
        linarith [rC_pos ht])))
      (fun z hz => Cf_collZeros_ne_zero ht hz)
  set Mbound : ℝ := Real.log ((9 / 4) * |t| ^ 2 / gapD t ^ collMultSum ht) with hMdef
  have hMpos : 0 < Mbound := by
    rw [hMdef]
    apply Real.log_pos
    have hδM : gapD t ^ collMultSum ht ≤ 1 :=
      pow_le_one₀ (gapD_pos t).le ((gapD_le t).trans (by norm_num))
    have hδM0 : 0 < gapD t ^ collMultSum ht := pow_pos (gapD_pos t) _
    have hX1 : (1:ℝ) < (9 / 4) * |t| ^ 2 := by
      have hsq : (10:ℝ) ^ 2 ≤ |t| ^ 2 := (sq_le_sq₀ (by norm_num) (abs_nonneg t)).mpr ht
      nlinarith
    rw [lt_div_iff₀ hδM0, one_mul]
    exact hδM.trans_lt hX1
  have hReJ : ∀ z ∈ Metric.ball 0 (rC ht), (J_B z).re ≤ Mbound := by
    intro z hz
    have hzC : z ∈ Metric.closedBall 0 (rC ht) := Metric.ball_subset_closedBall hz
    have h1 := hJre z hz
    have hBz := Cf_collZeros_norm_le_ball ht hzC
    have hBz0 := Cf_collZeros_ne_zero ht hzC
    have hlogle : Real.log ‖Cf (rC ht) (scaledZeta t) z‖ ≤ Mbound :=
      Real.log_le_log (norm_pos_iff.mpr hBz0) hBz
    have hcen := Cf_collZeros_log_norm_zero_nonneg ht
    rw [← h1]
    linarith [hlogle, hcen]
  have hBC : ‖deriv J_B w₀‖ ≤ 16 * Mbound * (rC ht) ^ 2 / (rC ht - 3 / 5) ^ 3 :=
    BorelCaratheodoryDeriv hMpos (by norm_num) (by linarith [rC_ge ht])
      hJ_an.analyticOn hJ0 hReJ (by
        rw [Metric.mem_closedBall, dist_zero_right]
        exact hw₀norm)
  have h450 : 16 * Mbound * (rC ht) ^ 2 / (rC ht - 3 / 5) ^ 3 ≤ 450 * Mbound := by
    have hrc1 := rC_ge ht
    have hrc2 := rC_le ht
    have hrc0 := rC_pos ht
    have h1 : (rC ht) ^ 2 ≤ (24 / 25 : ℝ) ^ 2 :=
      (sq_le_sq₀ hrc0.le (by norm_num)).mpr hrc2
    have h2 : (8 / 25 : ℝ) ^ 3 ≤ (rC ht - 3 / 5) ^ 3 :=
      pow_le_pow_left₀ (by norm_num) (by linarith) 3
    rw [div_le_iff₀ (pow_pos (by linarith : (0:ℝ) < rC ht - 3 / 5) 3)]
    nlinarith [hMpos.le, h1, h2, mul_nonneg hMpos.le (sub_nonneg.mpr h1),
      mul_nonneg hMpos.le (sub_nonneg.mpr h2)]
  have hderivJ : deriv J_B w₀
      = deriv (Cf (rC ht) (scaledZeta t)) w₀ / Cf (rC ht) (scaledZeta t) w₀ :=
    hJderiv w₀ (by rw [Metric.mem_closedBall, dist_zero_right]; exact hw₀norm)
  have hderivB : deriv (Cf (rC ht) (scaledZeta t)) w₀
      = deriv (fun w => scaledZeta t w / collProd ht w) w₀ := hB_eq.deriv_eq
  have hBval : Cf (rC ht) (scaledZeta t) w₀ = scaledZeta t w₀ / collProd ht w₀ :=
    hB_eq.eq_of_nhds
  have hlogFP : logDeriv (fun w => scaledZeta t w / collProd ht w) w₀
      = (5 / 2 : ℂ) * logDeriv riemannZeta s
        - ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℂ) / (w₀ - ρ) := by
    rw [hlogB, hlogF, hlogP]
  have hkey : deriv J_B w₀ = (5 / 2 : ℂ) * logDeriv riemannZeta s
      - ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℂ) / (w₀ - ρ) := by
    rw [hderivJ, hderivB, hBval]
    exact hlogFP
  have hζeq : logDeriv riemannZeta s
      = (2 / 5 : ℂ) * deriv J_B w₀
        + ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℂ) /
            (s - (discCenter t + (5 / 2 : ℂ) * ρ)) := by
    have h1 : (5 / 2 : ℂ) * logDeriv riemannZeta s
        = deriv J_B w₀ + ∑ ρ ∈ collZeros ht,
            (analyticOrderNatAt (scaledZeta t) ρ : ℂ) / (w₀ - ρ) := by
      rw [hkey]
      ring
    calc logDeriv riemannZeta s
        = (2 / 5 : ℂ) * ((5 / 2 : ℂ) * logDeriv riemannZeta s) := by ring
      _ = (2 / 5 : ℂ) * (deriv J_B w₀ + ∑ ρ ∈ collZeros ht,
            (analyticOrderNatAt (scaledZeta t) ρ : ℂ) / (w₀ - ρ)) := by rw [h1]
      _ = (2 / 5 : ℂ) * deriv J_B w₀ + ∑ ρ ∈ collZeros ht,
            (analyticOrderNatAt (scaledZeta t) ρ : ℂ) /
              (s - (discCenter t + (5 / 2 : ℂ) * ρ)) := by
          rw [mul_add, Finset.mul_sum]
          apply congrArg ((2 / 5 : ℂ) * deriv J_B w₀ + ·)
          apply Finset.sum_congr rfl
          intro ρ hρ
          have hX : (w₀ - ρ) ≠ 0 :=
            sub_ne_zero.mpr (fun h => hFw₀ (by rw [h]; exact ((mem_collZeros ht).mp hρ).2))
          have hden : s - (discCenter t + (5 / 2 : ℂ) * ρ) = (5 / 2 : ℂ) * (w₀ - ρ) := by
            rw [hw₀def]; ring
          rw [← mul_div_assoc, hden]
          field_simp [hX, (by norm_num : (5 / 2 : ℂ) ≠ 0)]
  set img := (collZeros ht).image (fun w : ℂ => discCenter t + (5 / 2 : ℂ) * w) with himg
  have hsum_img : ∑ ρ ∈ img, (zeroMult ρ : ℂ) / (s - ρ)
      = ∑ ρ ∈ collZeros ht, (analyticOrderNatAt (scaledZeta t) ρ : ℂ) /
          (s - (discCenter t + (5 / 2 : ℂ) * ρ)) := by
    rw [himg, Finset.sum_image (affMap_injOn _)]
    apply Finset.sum_congr rfl
    intro ρ hρ
    rw [zeroMult_affMap ht hρ]
  have hsub : nearZeros t ⊆ img := by rw [himg]; exact nearZeros_subset_image ht
  have hsplit : ∑ ρ ∈ img, (zeroMult ρ : ℂ) / (s - ρ)
      = ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)
        + ∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ) := by
    have h := Finset.sum_sdiff hsub (f := fun ρ => (zeroMult ρ : ℂ) / (s - ρ))
    rw [add_comm] at h
    exact h.symm
  have hfinal : logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)
      = (2 / 5 : ℂ) * deriv J_B w₀ + ∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ) := by
    rw [hζeq, ← hsum_img, hsplit]
    ring
  rw [hfinal]
  have hextras : ‖∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖
      ≤ Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
    have h1 : ‖∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖
        ≤ ∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℝ) := by
      refine (norm_sum_le _ _).trans (Finset.sum_le_sum fun ρ hρ => ?_)
      have hρimg : ρ ∈ img := (Finset.mem_sdiff.mp hρ).1
      have hρnotnear : ρ ∉ nearZeros t := (Finset.mem_sdiff.mp hρ).2
      rw [himg] at hρimg
      obtain ⟨w, hw, rfl⟩ := Finset.mem_image.mp hρimg
      have hρdisc : discCenter t + (5 / 2 : ℂ) * w ∈ zeroDiscFinset t := by
        rw [mem_zeroDiscFinset]
        constructor
        · rw [Metric.mem_closedBall, Complex.dist_eq, add_sub_cancel_left, norm_mul]
          have h25 : ‖(5 / 2 : ℂ)‖ = 5 / 2 := by
            rw [show (5 / 2 : ℂ) = ((5 / 2 : ℝ) : ℂ) by norm_num, Complex.norm_real,
              Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 5 / 2)]
          rw [h25]
          have hwle := ((mem_collZeros ht).mp hw).1
          calc (5 / 2 : ℝ) * ‖w‖ ≤ (5 / 2) * rC ht :=
                mul_le_mul_of_nonneg_left hwle (by norm_num)
            _ = collRadius ht := by unfold rC; ring
            _ ≤ 5 / 2 := (collRadius_le ht).trans (by norm_num)
        · have hFw : scaledZeta t w = 0 := ((mem_collZeros ht).mp hw).2
          unfold scaledZeta at hFw
          exact (div_eq_zero_iff.mp hFw).resolve_right hζs0
      have himge : 1 ≤ |(discCenter t + (5 / 2 : ℂ) * w).im - t| := by
        by_contra h
        push Not at h
        exact hρnotnear (mem_nearZeros.mpr ⟨hρdisc, h⟩)
      have hsnorm : (1:ℝ) ≤ ‖s - (discCenter t + (5 / 2 : ℂ) * w)‖ := by
        have h1 := abs_im_le_norm (s - (discCenter t + (5 / 2 : ℂ) * w))
        rw [sub_im, hsim, abs_sub_comm] at h1
        linarith
      rw [norm_div, RCLike.norm_natCast, div_le_iff₀ (zero_lt_one.trans_le hsnorm)]
      have hm0 : (0:ℝ) ≤ (zeroMult (discCenter t + (5 / 2 : ℂ) * w) : ℝ) := Nat.cast_nonneg _
      nlinarith [hsnorm, hm0, mul_nonneg hm0 (sub_nonneg.mpr hsnorm)]
    refine h1.trans ?_
    refine (Finset.sum_le_sum_of_subset_of_nonneg Finset.sdiff_subset
      (fun i _ _ => Nat.cast_nonneg _)).trans ?_
    rw [himg]
    exact sum_image_zeroMult_le ht
  calc ‖(2 / 5 : ℂ) * deriv J_B w₀ + ∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖
      ≤ ‖(2 / 5 : ℂ) * deriv J_B w₀‖
        + ‖∑ ρ ∈ img \ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖ := norm_add_le _ _
    _ ≤ (2 / 5) * (450 * Mbound) + Real.log ((9 / 4) * |t| ^ 2) / Real.log (33 / 32) := by
        have h25 : ‖(2 / 5 : ℂ)‖ = 2 / 5 := by
          rw [show (2 / 5 : ℂ) = ((2 / 5 : ℝ) : ℂ) by norm_num, Complex.norm_real,
            Real.norm_eq_abs, abs_of_nonneg (by norm_num : (0:ℝ) ≤ 2 / 5)]
        rw [norm_mul, h25]
        exact add_le_add
          (mul_le_mul_of_nonneg_left (hBC.trans h450) (by norm_num : (0:ℝ) ≤ 2 / 5)) hextras
    _ ≤ 100000 * (Real.log |t|) ^ 2 := by
        have h1 : Mbound ≤ 420 * (Real.log |t|) ^ 2 := by
          rw [hMdef]
          exact Mbound_le ht
        have h2 := jensen_bound_elementary ht
        have hL := two_le_log_abs_t ht
        have h42 : 33 + 66 * Real.log |t| ≤ 42 * (Real.log |t|) ^ 2 := by
          have hprod : (0:ℝ) ≤ (Real.log |t| - 2) * (42 * Real.log |t| + 17) :=
            mul_nonneg (sub_nonneg.mpr hL) (by nlinarith [hL])
          nlinarith [hprod, hL]
        nlinarith [h1, h2, h42, hL, sq_nonneg (Real.log |t|)]

end NguyenRH1

end