LiAssembly.lean

Declarations

Source

/-
LiAssembly.lean — tier ii′-6-b: the sides identity and the bridge
(D-071 §4.1–4.3).

§1 (`sf_abs_le_rectInt_add_zeroSum`): the rectangle residue theorem
`rectInt'_Jlag` (ii′-1b) on the D-036 variant-B rectangle
(z = −5/2 − iT, w = 2√n + iT, T zero-avoiding-wide from ii′-6's L3-wide)
plus the crux `sf_eq_resW1` (ii′-3c):
  |Sf n| = |(ResW1 n).re| ≤ ‖RectInt‖ + ‖Σ_{Sz} mult·(1−(ρ/(ρ−1))ⁿ)‖.

§2 (`zeroSum_norm_le_four_FAlt_add_one`): the bridge — under RHUpTo
3×10¹² every zero in Sz is on the line (|ρ/(ρ−1)| = 1), so each term
≤ 2·mult, and the both-signs mult-count is 2× the one-sign count
(conj symmetry + `zeroMult_conj` + the perimeter `ZeroCountGlobalProp`)
⟹ ‖Σ‖ ≤ 4·FAlt T + 1 (the +1 is the trivial-zero term at −2).

Perimeter used: ZeroCountProp (the crux), RHUpTo, ZeroCountGlobalProp,
NoLowZeros.
-/
import Mathlib
import NguyenRH1.LiSides
import NguyenRH1.LiCrux
import NguyenRH1.LiContour
import NguyenRH1.LiTightR
import NguyenRH1.LiFEntire
import NguyenRH1.LiCircleBound

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 0. The both-signs ordinate window -/

/-- The nontrivial zeros with |γ| ≤ T (the rectangle's zero content,
minus the trivial zero −2 which is handled separately). -/
def zeroBothWindow (T : ℝ) : Set ℂ :=
  {ρ | IsNontrivialZero ρ ∧ |ρ.im| ≤ T}

/-- Finiteness of the both-signs window (via Zeta23 `zerosIn_finite`). -/
theorem zeroBothWindow_finite (T : ℝ) : (zeroBothWindow T).Finite := by
  apply Set.Finite.subset (zerosIn_finite (-T - 1) T)
  intro ρ hρ
  refine ⟨hρ.1, ?_, ?_⟩
  · linarith [abs_le.mp hρ.2 |>.1]
  · exact abs_le.mp hρ.2 |>.2

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

/-- Finiteness of the negative window. -/
theorem zeroGlobalWindowNeg_finite (T : ℝ) : (zeroGlobalWindowNeg T).Finite := by
  apply Set.Finite.subset (zerosIn_finite (-T - 1) 0)
  intro ρ hρ
  refine ⟨hρ.1, by linarith [hρ.2.1], by linarith [hρ.2.2]⟩

/-! ## 1. The sides identity -/

/-- The rectangle for the L0 assembly (D-036 variant B): z = −5/2 − iT,
w = 2√n + iT. -/
abbrev rectZ (T : ℝ) : ℂ := ((-5 / 2 : ℝ) : ℂ) - (T : ℝ) * Complex.I
abbrev rectW (n : ℕ) (T : ℝ) : ℂ := ((2 * Real.sqrt n : ℝ) : ℂ) + (T : ℝ) * Complex.I

lemma rectZ_re (T : ℝ) : (rectZ T).re = -5 / 2 := by simp [rectZ]
lemma rectZ_im (T : ℝ) : (rectZ T).im = -T := by simp [rectZ]
lemma rectW_re (n : ℕ) (T : ℝ) : (rectW n T).re = 2 * Real.sqrt n := by simp [rectW]
lemma rectW_im (n : ℕ) (T : ℝ) : (rectW n T).im = T := by simp [rectW]

/-- **The sides identity** (D-071 §4.1): on the variant-B rectangle with
the wide zero-avoiding ordinate,
|Sf n| ≤ ‖RectangleIntegral' (Jlag n) z w‖ + ‖Σ_{Sz} mult·(1−(ρ/(ρ−1))ⁿ)‖,
Sz = {nontrivial zeros, |γ| ≤ T} ∪ {−2}. -/
theorem sf_abs_le_rectInt_add_zeroSum (hZC : ZeroCountProp) {n : ℕ} (hn : 1 ≤ n)
    {T : ℝ} (hT1 : 1 ≤ T) (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1)
    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →
      ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|) :
    |Sf n| ≤ ‖RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)‖ +
      ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
        (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := by
  set z := rectZ T
  set w := rectW n T
  have hn1sqrt : (1 : ℝ) ≤ Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)
  have hre : z.re ≤ w.re := by
    rw [rectZ_re, rectW_re]
    have h := Real.sqrt_nonneg (n : ℝ)
    linarith
  have him : z.im ≤ w.im := by
    rw [rectZ_im, rectW_im]
    linarith
  -- 1 is interior
  have h1mem : (1 : ℂ) ∈ Rectangle z w := by
    have hr : (1 : ℂ).re ∈ Set.uIcc z.re w.re := by
      rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Complex.one_re, Set.mem_Icc]
      constructor <;> [linarith; linarith [Real.sqrt_nonneg (n : ℝ)]]
    have hi : (1 : ℂ).im ∈ Set.uIcc z.im w.im := by
      rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Complex.one_im, Set.mem_Icc]
      constructor <;> linarith
    exact ⟨hr, hi⟩
  have h1notb : (1 : ℂ) ∉ RectangleBorder z w := by
    intro hb
    have h2n : (1 : ℝ) < 2 * Real.sqrt n := by
      linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]
    have key : (1 : ℂ).im = z.im ∨ (1 : ℂ).re = z.re ∨ (1 : ℂ).im = w.im ∨
        (1 : ℂ).re = w.re := by
      rw [RectangleBorder] at hb
      simp only [Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff] at hb
      tauto
    rcases key with him | hre | him2 | hre2
    · rw [rectZ_im, Complex.one_im] at him
      exact absurd him (by linarith [hT1] : (0 : ℝ) ≠ -T)
    · rw [rectZ_re, Complex.one_re] at hre
      norm_num at hre
    · rw [rectW_im, Complex.one_im] at him2
      exact absurd him2 (by linarith [hT1] : (0 : ℝ) ≠ T)
    · rw [rectW_re, Complex.one_re] at hre2
      exact absurd hre2 (by linarith [h2n] : (1 : ℝ) ≠ 2 * Real.sqrt n)
  have h1int : Rectangle z w ∈ 𝓝 (1 : ℂ) :=
    rectangle_mem_nhds_of_mem_not_border hre him h1mem h1notb
  -- the border is zero-free
  have hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0 := by
    intro s hs hζ
    have key : s.im = z.im ∨ s.re = z.re ∨ s.im = w.im ∨ s.re = w.re := by
      rw [RectangleBorder] at hs
      simp only [Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff] at hs
      tauto
    rcases zeta_zero_classification hζ with hnt | h0 | hn2
    · -- nontrivial: re ∈ (0,1); border pieces with re in (0,1) are top/bottom
      rcases key with him | hre | him2 | hre2
      · -- bottom: im = −T; conj ρ has im = T in the window — pigeonhole contradiction
        rw [rectZ_im] at him
        have hconj := hTwide ((starRingEnd ℂ) s) (isNontrivialZero_conj hnt)
          (by rw [Complex.conj_im, him]; linarith [hTn])
          (by rw [Complex.conj_im, him]; linarith [hTn1])
        have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) := by
          have h := two_le_C0hat (by linarith [hn1sqrt] : (1 : ℝ) ≤ Real.sqrt n + 2)
          exact one_div_pos.mpr (by linarith)
        have hzero : |((starRingEnd ℂ) s).im - T| = 0 := by
          rw [Complex.conj_im, him, neg_neg, sub_self, abs_zero]
        linarith [hconj, hpos, hzero]
      · -- left: re = −5/2, not in (0,1)
        rw [rectZ_re] at hre
        have h21 : (0 : ℝ) < -5 / 2 := hre ▸ hnt.2.1
        norm_num at h21
      · -- top: im = T; pigeonhole contradiction directly
        rw [rectW_im] at him2
        have hdir := hTwide s hnt (by rw [him2]; linarith [hTn]) (by rw [him2]; linarith [hTn1])
        have hpos : (0 : ℝ) < 1 / (9 * C0hat (Real.sqrt n + 2)) := by
          have h := two_le_C0hat (by linarith [hn1sqrt] : (1 : ℝ) ≤ Real.sqrt n + 2)
          exact one_div_pos.mpr (by linarith)
        have hzero : |s.im - T| = 0 := by rw [him2, sub_self, abs_zero]
        linarith [hdir, hpos, hzero]
      · -- right: re = 2√n ≥ 2 > 1
        rw [rectW_re] at hre2
        have h1re : (1 : ℝ) ≤ s.re := by
          rw [hre2]
          linarith [Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]
        exact riemannZeta_ne_zero_of_one_le_re h1re hζ
    · -- s = 0: not on the border (im 0 = ±T needs T = 0; re 0 = −5/2 / 2√n false)
      rw [h0] at hs
      rw [h0] at key
      rcases key with him | hre | him2 | hre2
      · rw [rectZ_im, Complex.zero_im] at him
        exact absurd him (by linarith [hT1] : (0 : ℝ) ≠ -T)
      · rw [rectZ_re, Complex.zero_re] at hre
        norm_num at hre
      · rw [rectW_im, Complex.zero_im] at him2
        exact absurd him2 (by linarith [hT1] : (0 : ℝ) ≠ T)
      · rw [rectW_re, Complex.zero_re] at hre2
        have h0' : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _
        linarith [hre2, h0']
    · -- s = −2n, n ≥ 1: re = −2n; border re-pieces are −5/2 and 2√n; im = 0 ≠ ±T
      obtain ⟨m, hm1, rfl⟩ := hn2
      have him0 : ((-2 : ℂ) * (m : ℂ)).im = 0 := by
        simp [Complex.mul_im]
      have hre0 : ((-2 : ℂ) * (m : ℂ)).re = -2 * (m : ℝ) := by
        simp [Complex.mul_re]
      rcases key with him | hre | him2 | hre2
      · rw [rectZ_im, him0] at him
        exact absurd him (by linarith [hT1] : (0 : ℝ) ≠ -T)
      · rw [rectZ_re, hre0] at hre
        have hm : (m : ℝ) = 5 / 4 := by linarith
        have hm5 : m = 1 := by
          have h6 : (m : ℝ) < 2 := by linarith
          have h7 : m < 2 := by exact_mod_cast h6
          exact le_antisymm (Nat.lt_succ_iff.mp h7) hm1
        rw [hm5] at hm
        norm_num at hm
      · rw [rectW_im, him0] at him2
        exact absurd him2 (by linarith [hT1] : (0 : ℝ) ≠ T)
      · rw [rectW_re, hre0] at hre2
        have hpos : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _
        have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _
        nlinarith [hre2, hpos, hm0]
  -- Sz and its characterization
  set Sz : Finset ℂ := (zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)} with hSz_def
  have hSz : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0 := by
    intro s
    constructor
    · intro hs
      rw [hSz_def, Finset.mem_union, Finset.mem_singleton] at hs
      rcases hs with hs | rfl
      · have hmem : s ∈ zeroBothWindow T := (zeroBothWindow_finite T).mem_toFinset.mp hs
        obtain ⟨hnt, himT⟩ := hmem
        have hs1 : s ≠ 1 := by
          intro h
          have h22 : (1 : ℂ).re < 1 := h ▸ hnt.2.2
          rw [Complex.one_re] at h22
          exact lt_irrefl 1 h22
        refine ⟨⟨?_, ?_⟩, ?_⟩
        · have hr : s.re ∈ Set.uIcc z.re w.re := by
            rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]
            exact ⟨by linarith [hnt.2.1], by linarith [hnt.2.2, Real.one_le_sqrt.mpr (by exact_mod_cast hn : (1 : ℝ) ≤ n)]⟩
          exact hr
        · have hi : s.im ∈ Set.uIcc z.im w.im := by
            rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]
            exact abs_le.mp himT
          exact hi
        · rw [zetaA_apply hs1, hnt.1, mul_zero]
      · refine ⟨⟨?_, ?_⟩, ?_⟩
        · have hr : (-2 : ℂ).re ∈ Set.uIcc z.re w.re := by
            rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc]
            have h2re : (-2 : ℂ).re = -2 := by simp
            rw [h2re]
            constructor
            · norm_num
            · have h0' : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg _
              linarith
          exact hr
        · have hi : (-2 : ℂ).im ∈ Set.uIcc z.im w.im := by
            rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc]
            have h2im : (-2 : ℂ).im = 0 := by simp
            rw [h2im]
            constructor <;> linarith [hT1]
          exact hi
        · have h2ne : (-2 : ℂ) ≠ 1 := by norm_num
          rw [zetaA_apply h2ne]
          have hζ2 : riemannZeta (-2 : ℂ) = 0 := by
            have h := riemannZeta_neg_two_mul (n := 1) le_rfl
            rw [show (-2 : ℂ) * ((1 : ℕ) : ℂ) = -2 by push_cast; ring] at h
            exact h
          rw [hζ2, mul_zero]
    · intro ⟨hmem, hzA⟩
      have hs1 : s ≠ 1 := by
        intro h
        rw [h, zetaA_one] at hzA
        exact one_ne_zero hzA
      have hζ : riemannZeta s = 0 := by
        have e := zetaA_apply hs1
        rw [e, mul_eq_zero] at hzA
        rcases hzA with h | h
        · exact absurd (sub_eq_zero.mp h) hs1
        · exact h
      rcases zeta_zero_classification hζ with hnt | h0 | hn2
      · rw [hSz_def, Finset.mem_union]
        left
        apply (zeroBothWindow_finite T).mem_toFinset.mpr
        refine ⟨hnt, ?_⟩
        have hi : s.im ∈ Set.uIcc z.im w.im := hmem.2
        rw [Set.uIcc_of_le him, rectZ_im, rectW_im, Set.mem_Icc] at hi
        exact abs_le.mpr hi
      · have h00 : zetaA 0 = 0 := by rwa [h0] at hzA
        rw [zetaA_apply (by norm_num : (0 : ℂ) ≠ 1), riemannZeta_zero] at h00
        norm_num at h00
      · obtain ⟨m, hm1, rfl⟩ := hn2
        rw [hSz_def, Finset.mem_union]
        have hr : ((-2 : ℂ) * (m : ℂ)).re ∈ Set.uIcc z.re w.re := hmem.1
        rw [Set.uIcc_of_le hre, rectZ_re, rectW_re, Set.mem_Icc] at hr
        have hre2 : ((-2 : ℂ) * (m : ℂ)).re = -2 * (m : ℝ) := by
          simp [Complex.mul_re, Complex.neg_re]
        rw [hre2] at hr
        have hm1' : m = 1 := by
          have h1 : (m : ℝ) ≤ 5 / 4 := by
            have := hr.1
            have hm0 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg _
            nlinarith [this, hm0]
          have h2 : (m : ℝ) ≥ 1 := by exact_mod_cast hm1
          have hm2 : m ≤ 1 := by
            have h6 : (m : ℝ) < 2 := by linarith
            exact_mod_cast Nat.lt_succ_iff.mp (by exact_mod_cast h6 : m < 2)
          exact le_antisymm hm2 hm1
        rw [hm1']
        right
        rw [show ((-2 : ℂ) * ((1 : ℕ) : ℂ)) = -2 by push_cast; ring]
        exact Finset.mem_singleton_self (-2 : ℂ)
  -- the identity
  have hid := rectInt'_Jlag n hre him h1int hborder Sz hSz
  have hcrux := sf_eq_resW1 hZC hn
  rw [← hcrux]
  refine le_trans (abs_re_le_norm _) ?_
  have e : ResW1 n = RectangleIntegral' (Jlag n) z w -
      ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by
    rw [hid]
    ring
  rw [e]
  exact norm_sub_le _ _

/-! ## 2. The bridge -/

/-- On the line re ρ = 1/2: |ρ/(ρ−1)| = 1, so each zero term has norm
≤ 2·mult. -/
lemma zeroTerm_norm_le_two {ρ : ℂ} (_hρ : IsNontrivialZero ρ) (hre : ρ.re = 1 / 2)
    (n : ℕ) :
    ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 2 * (zeroMult ρ : ℝ) := by
  have hρ1 : ρ - 1 ≠ 0 := by
    intro h
    have h2 : ρ = 1 := sub_eq_zero.mp h
    rw [h2, Complex.one_re] at hre
    norm_num at hre
  have hnorm : ‖ρ‖ = ‖ρ - 1‖ := by
    have h : ‖ρ‖ ^ 2 = ‖ρ - 1‖ ^ 2 := by
      rw [← Complex.normSq_eq_norm_sq, ← Complex.normSq_eq_norm_sq]
      rw [Complex.normSq_apply ρ, Complex.normSq_apply (ρ - 1)]
      simp only [sub_re, one_re, sub_im, one_im, sub_zero]
      rw [hre]
      ring
    exact (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp h
  have hnorm_ratio : ‖ρ / (ρ - 1)‖ = 1 := by
    rw [norm_div, hnorm, div_self (ne_of_gt (norm_pos_iff.mpr hρ1))]
  calc ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖
      = (zeroMult ρ : ℝ) * ‖1 - (ρ / (ρ - 1)) ^ n‖ := by
        rw [norm_mul, RCLike.norm_natCast]
    _ ≤ (zeroMult ρ : ℝ) * 2 := by
        apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
        calc ‖1 - (ρ / (ρ - 1)) ^ n‖
            ≤ ‖(1 : ℂ)‖ + ‖(ρ / (ρ - 1)) ^ n‖ := norm_sub_le _ _
          _ = 1 + 1 := by rw [norm_one, norm_pow, hnorm_ratio, one_pow]
          _ = 2 := by norm_num
    _ = 2 * (zeroMult ρ : ℝ) := by ring

/-- The nontrivial part of the zero sum: ‖Σ‖ ≤ 2·Σ mult (each term ≤ 2
on the line via `RHUpTo`). -/
lemma zeroSum_nontriv_norm_le (hRH : RHUpTo (3 * 10 ^ 12)) {n : ℕ} {T : ℝ}
    (hTle : T ≤ 3 * 10 ^ 12) :
    ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
      (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤
      2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
  calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
        (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖
      ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
        ‖(zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ := norm_sum_le _ _
    _ ≤ ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, 2 * (zeroMult ρ : ℝ) := by
        apply Finset.sum_le_sum
        intro ρ hρ
        have hnt : IsNontrivialZero ρ := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).1
        have him : |ρ.im| ≤ T := ((zeroBothWindow_finite T).mem_toFinset.mp hρ).2
        have hre : ρ.re = 1 / 2 := hRH ρ hnt (by linarith [him, hTle] : |ρ.im| ≤ 3 * 10 ^ 12)
        exact zeroTerm_norm_le_two hnt hre n
    _ = 2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
        rw [Finset.mul_sum]

/-- The both-signs mult count is 2× the one-sign count (NoLowZeros gives
im ≠ 0; the conj bijection with `zeroMult_conj` identifies the two
halves). -/
lemma zeroBothWindow_sum_eq_two_mul (hNLZ : NoLowZeros) (T : ℝ) :
    ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ) =
      2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ) := by
  classical
  set P := (zeroGlobalWindow_finite T).toFinset with hP
  set N := (zeroGlobalWindowNeg_finite T).toFinset with hN
  have hW : (zeroBothWindow_finite T).toFinset = P ∪ N := by
    ext ρ
    rw [Finset.mem_union, (zeroBothWindow_finite T).mem_toFinset,
      (zeroGlobalWindow_finite T).mem_toFinset, (zeroGlobalWindowNeg_finite T).mem_toFinset]
    constructor
    · intro ⟨hnt, himT⟩
      have him0 : ρ.im ≠ 0 := by
        have h14 := hNLZ ρ hnt
        intro h
        rw [h, abs_zero] at h14
        exact (by norm_num : ¬ (14 : ℝ) ≤ 0) h14
      rcases lt_or_gt_of_ne him0 with hneg | hpos
      · exact Or.inr ⟨hnt, by linarith [abs_le.mp himT |>.1], hneg⟩
      · exact Or.inl ⟨hnt, hpos, by linarith [abs_le.mp himT |>.2]⟩
    · intro h
      rcases h with ⟨hnt, hpos, himT⟩ | ⟨hnt, himT, hneg⟩
      · have habs : |ρ.im| ≤ T := by rw [abs_of_pos hpos]; exact himT
        exact ⟨hnt, habs⟩
      · have habs : |ρ.im| ≤ T := by rw [abs_of_neg hneg]; linarith
        exact ⟨hnt, habs⟩
  have hdisj : Disjoint P N := by
    rw [Finset.disjoint_left]
    intro ρ hρP hρN
    have h1 : 0 < ρ.im := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρP).2.1
    have h2 : ρ.im < 0 := ((zeroGlobalWindowNeg_finite T).mem_toFinset.mp hρN).2.2
    linarith
  have hNeq : N = P.image (starRingEnd ℂ) := by
    rw [hN, hP]
    ext ρ
    simp only [(zeroGlobalWindowNeg_finite T).mem_toFinset,
      (zeroGlobalWindow_finite T).mem_toFinset, Finset.mem_image]
    constructor
    · intro ⟨hnt, himT, hneg⟩
      refine ⟨(starRingEnd ℂ) ρ, ?_, ?_⟩
      · exact ⟨isNontrivialZero_conj hnt, by rw [Complex.conj_im]; exact neg_pos.mpr hneg,
          by rw [Complex.conj_im]; linarith⟩
      · rw [starRingEnd_apply, starRingEnd_apply, star_star]
    · rintro ⟨σ, hσmem, rfl⟩
      obtain ⟨hσnt, hσpos, hσT⟩ := hσmem
      refine ⟨isNontrivialZero_conj hσnt, ?_, ?_⟩
      · rw [Complex.conj_im]
        linarith
      · rw [Complex.conj_im]
        linarith
  have hNsum : (∑ ρ ∈ N, (zeroMult ρ : ℝ)) = ∑ ρ ∈ P, (zeroMult ρ : ℝ) := by
    rw [hNeq, Finset.sum_image (fun ρ _ σ _ h => (starRingEnd ℂ).injective h)]
    apply Finset.sum_congr rfl
    intro ρ hρ
    have hnt : IsNontrivialZero ρ := ((zeroGlobalWindow_finite T).mem_toFinset.mp hρ).1
    have h := zeroMult_conj hnt
    rw [h]
  rw [hW, Finset.sum_union hdisj, hNsum]
  ring

/-- The trivial-zero term at −2: |1 − (2/3)ⁿ| ≤ 1. -/
lemma trivTerm_norm_le_one (n : ℕ) :
    ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ ≤ 1 := by
  have hm : (zeroMult (-2 : ℂ) : ℂ) = 1 := by
    rw [zeroMult_neg_two]
    norm_num
  rw [hm, one_mul]
  have h1 : (0 : ℝ) ≤ (2 / 3 : ℝ) := by norm_num
  have h2 : (2 / 3 : ℝ) ≤ 1 := by norm_num
  have hpow1 : (2 / 3 : ℝ) ^ n ≤ 1 := pow_le_one₀ h1 h2
  have hnorm : ‖(1 : ℂ) - ((-2 : ℂ) / (-2 - 1)) ^ n‖ = 1 - (2 / 3 : ℝ) ^ n := by
    have e : (-2 : ℂ) / (-2 - 1) = ((2 / 3 : ℝ) : ℂ) := by
      have h3 : (-2 : ℂ) - 1 = -3 := by norm_num
      rw [h3]
      rw [div_eq_iff (by norm_num : (-3 : ℂ) ≠ 0)]
      push_cast
      ring
    rw [e, ← ofReal_pow, ← ofReal_one, ← ofReal_sub, Complex.norm_real, Real.norm_eq_abs,
      abs_of_nonneg (by linarith : (0 : ℝ) ≤ 1 - (2 / 3 : ℝ) ^ n)]
  rw [hnorm]
  linarith [pow_nonneg h1 n]

/-- **The bridge** (D-071 §4.2): ‖Σ zero terms‖ ≤ 4·FAlt T + 1. The +1
is the trivial-zero term at −2; the 4·FAlt is the both-signs count
(2·mult per term × 2× one-sign count ≤ FAlt via the perimeter
`ZeroCountGlobalProp`). -/
theorem zeroSum_norm_le_four_FAlt_add_one (hRH : RHUpTo (3 * 10 ^ 12))
    (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros) {n : ℕ} {T : ℝ}
    (hTle : T ≤ 3 * 10 ^ 12 - 1) (hT2 : 2 ≤ T) :
    ‖∑ ρ ∈ ((zeroBothWindow_finite T).toFinset ∪ {(-2 : ℂ)}),
      (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ ≤ 4 * FAlt T + 1 := by
  have h2not : (-2 : ℂ) ∉ (zeroBothWindow_finite T).toFinset := by
    intro h
    have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1
    have h21 : (0 : ℝ) < (-2 : ℂ).re := hnt.2.1
    norm_num at h21
  have hdisj2 : Disjoint (zeroBothWindow_finite T).toFinset {(-2 : ℂ)} := by
    rw [Finset.disjoint_left]
    intro ρ hρ hρ2
    rw [Finset.mem_singleton] at hρ2
    exact h2not (hρ2 ▸ hρ)
  rw [Finset.sum_union hdisj2, Finset.sum_singleton]
  have htriv := trivTerm_norm_le_one n
  have hbridge := zeroSum_nontriv_norm_le hRH (n := n) (T := T) (by linarith [hTle])
  have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T
  have hZ := hZCG T hT2
  calc ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
        (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) +
        (zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖
      ≤ ‖∑ ρ ∈ (zeroBothWindow_finite T).toFinset,
        (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)‖ +
        ‖(zeroMult (-2 : ℂ) : ℂ) * (1 - ((-2 : ℂ) / (-2 - 1)) ^ n)‖ := norm_add_le _ _
    _ ≤ (2 * ∑ ρ ∈ (zeroBothWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by
        linarith [hbridge, htriv]
    _ = 2 * (2 * ∑ ρ ∈ (zeroGlobalWindow_finite T).toFinset, (zeroMult ρ : ℝ)) + 1 := by
        rw [hcount]
    _ ≤ 4 * FAlt T + 1 := by linarith [hZ]

end NguyenRH1