{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-057-convexity-proof.md",
  "old_string": "## 5. Caveats\n- The proof is for the margin\u0303 majorant; the substitution \u0108\u2080 \u2265 C\u2080 is\n  the D-056 closed-form bound (proved there).\n- E-029 provides the symbolic-expression check (sympy table matches\n  the hand-derived \u03c8\u1d62 to machine precision) and the grid verifications;\n  the sign arguments of \u00a72\u20133 are hand-provable as written.",
  "new_string": "## 5. Caveats\n- The proof is for the margin\u0303 majorant; the substitution \u0108\u2080 \u2265 C\u2080 is\n  the D-056 closed-form bound (proved there).\n- E-029 provides the symbolic-expression check (sympy table matches\n  the hand-derived \u03c8\u1d62 to machine precision) and the grid verifications;\n  the sign arguments of \u00a72\u20133 are hand-provable as written.\n\n## 6. Lean formalization note (session 011): 11 conditions \u2192 8 blocks\nThe Lean proof of `marginTilde_convex` (NguyenRH1, session 011) diverges\nfrom this file's presentation by design:\n- This file's table has 11 rows. Rows #1\u2013#4 (T log T, T, log T,\n  log log T) exist to expand the Trudgian N(T)/S(T) majorants F and\n  S_b into elementary pieces. The Lean theorem is **parameterized over\n  F** (the majorant and its \u03c8-condition h\u03c8 are hypotheses, discharged\n  elsewhere for the explicit Trudgian majorant), so those rows never\n  appear: the 2F(T) term is handled atomically via h\u03c8.\n- The remaining rows collapse to **8 block types**: id (#2), T\u00b7L1 (#5),\n  T\u00b7L2 (#6), L1\u00b2 (#7), L1\u00b7L2 (#8), L2\u00b2 (#9), L1 (#10), L2 (#11) \u2014\n  exactly the blocks generated by the closed-form \u0108\u2080/H\u0302 terms.\n- B\u0303\u2084 (the I_I term) is **not concave**, so it is excluded from the\n  \u03c8-machinery and bounded directly: IIMaj is rewritten as\n  \u03c8\u0303(s) = 4.56(s+1)(e^{\u2212as}+e^{\u2212bs}) and the analytic factor-monotone\n  bound \u03c8\u0303\u2033(s) \u2212 \u03c8\u0303\u2032(s)/s \u2264 1.316 < 2 (iimaj_bracket_bound) replaces\n  this file's \u00a73 grid-plus-decay argument (E-029's measured\n  max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 \u2014 the measured-to-traced conversion also\n  highlighted in draft.tex's Formal verification appendix)."
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
  "oldString": "    calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by\n          rw [norm_div, Nat.cast_nonneg, ...]  -- placeholder\n      _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by",
  "newString": "    calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) :=\n          norm_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)\n      _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by",
  "originalFile": "/-\nNguyenRH1/LiCircleBound.lean \u2014 tier ii\u2032 sub-stage ii\u2032-5e-v (D-068 \u00a75):\nthe circle bound for the partial-fraction difference and the squeeze to\nthe capstone identity.\n\n\u00a70: conjugate symmetry of the nontrivial zeros (for the lower-half\n    circle arcs).\n\u00a71: the mult-weighted ordinate-window count bridges from Zeta23's RvM\n    local count (`zeta_local_zero_count`: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3)\n    with multiplicity, ALL t \u2014 no perimeter): `A0count` + the dyadic\n    interval count `Ncount_le_of_interval`.\n\u00a72: the Dirichlet bound `norm_logDeriv_zeta_le_dirichlet` (\u2016\u03b6\u2032/\u03b6 s\u2016 \u2264\n    dirichletC2 for re s \u2265 2; \u2212\u03b6\u2032/\u03b6 = LSeries \u039b, termwise \u2264 the s = 2\n    majorant) \u2014 the right near-axis arc input.\n\u00a73+: (this file, subsequent sub-stages) the series bound, the logDeriv\n    assembly, the Fexpr circle bound, the Schwarz squeeze, and the\n    capstone `partialFraction_identity`.\n\nArchive references: D-068 \u00a75, journal-029.\n-/\nimport Mathlib\nimport Zeta23.RvM.LocalCount\nimport NguyenRH1.LiFEntire\nimport NguyenRH1.LiGapCircles\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. Conjugate symmetry -/\n\n/-- The conjugate of a nontrivial zero is a nontrivial zero. -/\nlemma isNontrivialZero_conj {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n    IsNontrivialZero ((starRingEnd \u2102) \u03c1) := by\n  refine \u27e8?_, ?_, ?_\u27e9\n  \u00b7 rw [_root_.riemannZeta_conj, h\u03c1.1, map_zero]\n  \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.1\n  \u00b7 rw [Complex.conj_re]; exact h\u03c1.2.2\n\n/-! ## 1. The mult-weighted window count bridges -/\n\n/-- The local-count constant: from Zeta23's RvM local count\n(`zeta_local_zero_count`, [Tit86 Thm 9.2] \u2014 mult-weighted, two-sided,\nall t, PROVED unconditionally in Zeta23). -/\ndef A0count : \u211d := Classical.choose Zeta23.RvM.zeta_local_zero_count\n\nlemma A0count_ge_one : (1 : \u211d) \u2264 A0count :=\n  (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).1\n\nlemma A0count_pos : (0 : \u211d) < A0count := lt_of_lt_of_le one_pos A0count_ge_one\n\n/-- The unit-window bound: Ncount(t, t+1] \u2264 A\u2080\u00b7log(|t|+3). -/\nlemma Ncount_window_le (t : \u211d) :\n    (Zeta23.Ncount t (t + 1) : \u211d) \u2264 A0count * Real.log (|t| + 3) :=\n  (Classical.choose_spec Zeta23.RvM.zeta_local_zero_count).2 t\n\n/-- Window additivity: Ncount(a, c] = Ncount(a, b] + Ncount(b, c] for\na \u2264 b \u2264 c (the disjoint union of the ordinate windows). -/\nlemma Ncount_add_of_le {a b c : \u211d} (hab : a \u2264 b) (hbc : b \u2264 c) :\n    Zeta23.Ncount a c = Zeta23.Ncount a b + Zeta23.Ncount b c := by\n  have hunion : Zeta23.zerosIn a c = Zeta23.zerosIn a b \u222a Zeta23.zerosIn b c := by\n    ext \u03c1\n    constructor\n    \u00b7 intro h\u03c1c\n      obtain \u27e8h\u03c1, ha, hc\u27e9 := h\u03c1c\n      rcases le_or_gt \u03c1.im b with h | h\n      \u00b7 exact Set.mem_union_left _ \u27e8h\u03c1, ha, h\u27e9\n      \u00b7 exact Set.mem_union_right _ \u27e8h\u03c1, h, hc\u27e9\n    \u00b7 intro h\n      rcases h with h\u03c1b | h\u03c1c\n      \u00b7 obtain \u27e8h\u03c1, ha, hb\u27e9 := h\u03c1b\n        exact \u27e8h\u03c1, ha, hb.trans hbc\u27e9\n      \u00b7 obtain \u27e8h\u03c1, hb, hc\u27e9 := h\u03c1c\n        exact \u27e8h\u03c1, hab.trans_lt hb, hc\u27e9\n  have hdisj : Disjoint (Zeta23.zerosIn a b) (Zeta23.zerosIn b c) := by\n    rw [Set.disjoint_iff]\n    intro \u03c1 \u27e8h1, h2\u27e9\n    exact absurd (h1.2.2.trans_lt h2.2.1) (lt_irrefl \u03c1.im)\n  rw [Zeta23.Ncount, Zeta23.Ncount, Zeta23.Ncount, hunion]\n  exact_mod_cast finsum_mem_union hdisj (Zeta23.zerosIn_finite a b)\n    (Zeta23.zerosIn_finite b c)\n\n/-- The N-step unit-window chain: Ncount(a, a+N] \u2264 A\u2080\u00b7N\u00b7log(|a|+N+3). -/\nlemma Ncount_chain_le (a : \u211d) (N : \u2115) :\n    (Zeta23.Ncount a (a + (N : \u211d)) : \u211d)\n      \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := by\n  induction N with\n  | zero =>\n    simp only [Nat.cast_zero, add_zero]\n    have h0 : Zeta23.zerosIn a a = \u2205 := by\n      ext \u03c1\n      constructor\n      \u00b7 intro h\n        obtain \u27e8-, h1, h2\u27e9 := h\n        exact absurd (h2.trans_lt h1) (lt_irrefl _)\n      \u00b7 intro h\n        simp at h\n    have hz : Zeta23.Ncount a a = 0 := by\n      simp only [Zeta23.Ncount, h0, finsum_mem_empty]\n    rw [hz, Nat.cast_zero]\n    simp\n  | succ N ih =>\n    have hN0 : (0 : \u211d) \u2264 (N : \u211d) := Nat.cast_nonneg N\n    have hsplit : Zeta23.Ncount a (a + (N : \u211d) + 1)\n        = Zeta23.Ncount a (a + (N : \u211d)) + Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1) :=\n      Ncount_add_of_le (a := a) (b := a + (N : \u211d)) (c := a + (N : \u211d) + 1)\n        (by linarith) (by linarith)\n    have hcast : a + ((N + 1 : \u2115) : \u211d) = a + (N : \u211d) + 1 := by push_cast; ring\n    rw [hcast, hsplit]\n    have hwin := Ncount_window_le (a + (N : \u211d))\n    have hlog : Real.log (|a + (N : \u211d)| + 3) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n      apply Real.log_le_log (by positivity)\n      have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n        (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n      linarith\n    have hlogpos : (0 : \u211d) \u2264 Real.log (|a| + (N : \u211d) + 3) := by\n      apply Real.log_nonneg\n      have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n      linarith [hN0]\n    have hlogpos' : (0 : \u211d) \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n      apply Real.log_nonneg\n      have h1 : (1 : \u211d) \u2264 |a| + 3 := by linarith [abs_nonneg a]\n      linarith [hN0]\n    push_cast\n    -- goal: \u2191(Ncount a (a+\u2191N)) + \u2191(Ncount (a+\u2191N) (a+\u2191N+1)) \u2264 A\u2080(\u2191N+1)\u00b7log(|a|+(\u2191N+1)+3)\n    have hlogC : Real.log (|a| + (N : \u211d) + 3)\n        \u2264 Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n      Real.log_le_log (by positivity) (by linarith)\n    have hle1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n        \u2264 A0count * (N : \u211d) * Real.log (|a| + ((N : \u211d) + 1) + 3) :=\n      mul_le_mul_of_nonneg_left hlogC (mul_nonneg A0count_pos.le hN0)\n    have hle2 : A0count * Real.log (|a + (N : \u211d)| + 3)\n        \u2264 A0count * Real.log (|a| + ((N : \u211d) + 1) + 3) := by\n      apply mul_le_mul_of_nonneg_left _ A0count_pos.le\n      apply Real.log_le_log (by positivity)\n      have h1 : |a + (N : \u211d)| \u2264 |a| + (N : \u211d) :=\n        (abs_add_le _ _).trans (by rw [abs_of_nonneg (show (0 : \u211d) \u2264 (N : \u211d) from Nat.cast_nonneg N)])\n      linarith\n    have hsum : \u2191(Zeta23.Ncount a (a + (N : \u211d))) + \u2191(Zeta23.Ncount (a + (N : \u211d)) (a + (N : \u211d) + 1))\n        \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n          + A0count * Real.log (|a + (N : \u211d)| + 3) :=\n      add_le_add ih hwin\n    linarith [hsum, hle1, hle2]\n\n/-- The dyadic-interval count: Ncount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(b+4) for\n0 \u2264 a \u2264 b (the unit-window chain + the ceil cover). -/\nlemma Ncount_le_of_interval {a b : \u211d} (ha : 0 \u2264 a) (hab : a \u2264 b) :\n    (Zeta23.Ncount a b : \u211d) \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n  set N : \u2115 := \u2308b - a\u2309\u208a with hN\n  have hNb : b \u2264 a + (N : \u211d) := by\n    have h := Nat.le_ceil (b - a)\n    rw [\u2190 hN] at h\n    have h2 : (b - a : \u211d) \u2264 (N : \u211d) := h\n    linarith\n  have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n    intro \u03c1 h\u03c1\n    refine \u27e8h\u03c1.1, h\u03c1.2.1, ?_\u27e9\n    exact h\u03c1.2.2.trans hNb\n  have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n    rw [Zeta23.Ncount, Zeta23.Ncount]\n    rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n      finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n    apply Finset.sum_le_sum_of_subset_of_nonneg\n    \u00b7 intro \u03c1 h\u03c1\n      rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n      exact hsub h\u03c1\n    \u00b7 intro \u03c1 _ _\n      exact Nat.cast_nonneg _\n  have hchain := Ncount_chain_le a N\n  have hNle : (N : \u211d) \u2264 b - a + 1 := by\n    have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n    rw [\u2190 hN] at h\n    have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n    linarith\n  have hlogle : Real.log (|a| + (N : \u211d) + 3) \u2264 Real.log (b + 4) := by\n    apply Real.log_le_log (by positivity)\n    rw [abs_of_nonneg ha]\n    linarith\n  calc (Zeta23.Ncount a b : \u211d)\n      \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n    _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n    _ \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n        have hlogpos : (0 : \u211d) \u2264 Real.log (b + 4) := by\n          apply Real.log_nonneg; linarith\n        have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n            \u2264 A0count * (N : \u211d) * Real.log (b + 4) :=\n          mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n        have h2 : A0count * (N : \u211d) * Real.log (b + 4)\n            \u2264 A0count * (b - a + 1) * Real.log (b + 4) := by\n          apply mul_le_mul_of_nonneg_right _ hlogpos\n          nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n        exact h1.trans h2\n\n/-! ## 2. The Dirichlet bound -/\n\n/-- The Dirichlet majorant constant: the absolute sum of the von\nMangoldt L-series terms at s = 2 (summable since 2 > 1). -/\ndef dirichletC2 : \u211d :=\n  \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 C\u2082 for re s \u2265 2 (the Dirichlet-series majorant:\n\u2212\u03b6\u2032/\u03b6 = LSeries \u039b for re > 1, termwise \u2264 the s = 2 sum). -/\nlemma norm_logDeriv_zeta_le_dirichlet {s : \u2102} (hs : 2 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC2 := by\n  have hs1 : (1 : \u211d) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n      \u2264 dirichletC2 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum2\n      _ = dirichletC2 := rfl\n  calc \u2016logDeriv riemannZeta s\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 dirichletC2 := hle\n\n/-! ## 3. The tsum split + the generalized interval count + the low-zero\nconstant -/\n\n/-- Splitting a summable real tsum over a finset:\n\u2211' f = \u2211_{i \u2208 s} f i + \u2211' (if i \u2208 s then 0 else f i). -/\nlemma tsum_split_finset {\u03b9 : Type*} [DecidableEq \u03b9] {f : \u03b9 \u2192 \u211d} (hf : Summable f)\n    (s : Finset \u03b9) :\n    \u2211' i, f i = \u2211 i \u2208 s, f i + \u2211' i, (if i \u2208 s then 0 else f i) := by\n  classical\n  have h1 : Summable (fun i => if i \u2208 s then f i else 0) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h2 : Summable (fun i => if i \u2208 s then 0 else f i) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  have h3 : \u2211' i, f i\n      = \u2211' i, ((if i \u2208 s then f i else 0) + (if i \u2208 s then 0 else f i)) := by\n    apply tsum_congr\n    intro i\n    by_cases hi : i \u2208 s <;> simp [hi]\n  rw [h3, Summable.tsum_add h1 h2]\n  congr 1\n  rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n  exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n\n/-- The generalized dyadic-interval count (both signs):\nNcount(a, b] \u2264 A\u2080\u00b7(b\u2212a+1)\u00b7log(3\u00b7max|a||b| + 5). -/\nlemma Ncount_le_of_interval_gen {a b : \u211d} (hab : a \u2264 b) :\n    (Zeta23.Ncount a b : \u211d)\n      \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n  set N : \u2115 := \u2308b - a\u2309\u208a with hN\n  have hNb : b \u2264 a + (N : \u211d) := by\n    have h := Nat.le_ceil (b - a)\n    rw [\u2190 hN] at h\n    linarith\n  have hsub : Zeta23.zerosIn a b \u2286 Zeta23.zerosIn a (a + (N : \u211d)) := by\n    intro \u03c1 h\u03c1\n    exact \u27e8h\u03c1.1, h\u03c1.2.1, h\u03c1.2.2.trans hNb\u27e9\n  have hle : Zeta23.Ncount a b \u2264 Zeta23.Ncount a (a + (N : \u211d)) := by\n    rw [Zeta23.Ncount, Zeta23.Ncount]\n    rw [finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a b),\n      finsum_mem_eq_finite_toFinset_sum _ (Zeta23.zerosIn_finite a (a + (N : \u211d)))]\n    apply Finset.sum_le_sum_of_subset_of_nonneg\n    \u00b7 intro \u03c1 h\u03c1\n      rw [Set.Finite.mem_toFinset] at h\u03c1 \u22a2\n      exact hsub h\u03c1\n    \u00b7 intro \u03c1 _ _\n      exact Nat.cast_nonneg _\n  have hchain := Ncount_chain_le a N\n  have hNle : (N : \u211d) \u2264 b - a + 1 := by\n    have h := Nat.ceil_lt_add_one (sub_nonneg.mpr hab)\n    rw [\u2190 hN] at h\n    have h2 : ((N : \u211d)) < b - a + 1 := by exact_mod_cast h\n    linarith\n  have hlogle : Real.log (|a| + (N : \u211d) + 3)\n      \u2264 Real.log (3 * max |a| |b| + 5) := by\n    apply Real.log_le_log (by positivity)\n    have hM1 : |a| \u2264 max |a| |b| := le_max_left _ _\n    have hM2 : |b| \u2264 max |a| |b| := le_max_right _ _\n    have hba : b - a \u2264 |b| + |a| := by\n      have h1 := le_abs_self b\n      have h2 : -a \u2264 |a| := by rw [\u2190 abs_neg a]; exact le_abs_self (-a)\n      linarith\n    nlinarith [hNle, hM1, hM2, hba, abs_nonneg a, abs_nonneg b]\n  have hlogpos : (0 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n    apply Real.log_nonneg\n    have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n    linarith\n  calc (Zeta23.Ncount a b : \u211d)\n      \u2264 (Zeta23.Ncount a (a + (N : \u211d)) : \u211d) := by exact_mod_cast hle\n    _ \u2264 A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3) := hchain\n    _ \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n        have h1 : A0count * (N : \u211d) * Real.log (|a| + (N : \u211d) + 3)\n            \u2264 A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5) :=\n          mul_le_mul_of_nonneg_left hlogle (mul_nonneg A0count_pos.le (Nat.cast_nonneg N))\n        have h2 : A0count * (N : \u211d) * Real.log (3 * max |a| |b| + 5)\n            \u2264 A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5) := by\n          apply mul_le_mul_of_nonneg_right _ hlogpos\n          nlinarith [A0count_pos, hNle, sub_nonneg.mpr hab]\n        exact h1.trans h2\n\n/-- The low-zero finset: nontrivial zeros with \u2016\u03c1\u2016 \u2264 3. -/\ndef lowZeros : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n  (show {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u2016(\u03c1 : \u2102)\u2016 \u2264 3}.Finite from\n    (finite_subtype_norm_lt 4).subset\n      (fun \u03c1 h\u03c1 => lt_of_le_of_lt (show \u2016(\u03c1 : \u2102)\u2016 \u2264 3 from h\u03c1) (by norm_num))).toFinset\n\n/-- The low-zero symbolic constant (a fixed finite sum of fixed positive\nreals; \u2016\u03c1\u2016 > 0 for nontrivial \u03c1 since re \u03c1 > 0). -/\ndef lowZeroConst : \u211d :=\n  \u2211 \u03c1 \u2208 lowZeros, (zeroMult (\u03c1 : \u2102) : \u211d) * (1 + 1 / \u2016(\u03c1 : \u2102)\u2016)\n\nlemma lowZeroConst_nonneg : 0 \u2264 lowZeroConst :=\n  Finset.sum_nonneg fun _\u03c1 _ => mul_nonneg (Nat.cast_nonneg _)\n    (add_nonneg one_pos.le (div_nonneg one_pos.le (norm_nonneg _)))\n\n/-! ## 4. The far-tail bound -/\n\n/-- The dyadic log series closed form:\n\u2211' j, ((j+4)\u00b7log 2 + log X)/2^j = 10\u00b7log 2 + 2\u00b7log X. -/\nlemma tsum_dyadic_log (X : \u211d) :\n    \u2211' j : \u2115, ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j\n      = 10 * Real.log 2 + 2 * Real.log X := by\n  have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n  have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 :=\n    (hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)).tsum_eq\n  have hsplit : (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n      = fun j : \u2115 => Real.log 2 * ((j : \u211d) * ((1 : \u211d) / 2) ^ j)\n        + (4 * Real.log 2 + Real.log X) * ((1 : \u211d) / 2) ^ j := by\n    funext j\n    rw [div_eq_mul_inv, inv_pow]\n    ring\n  rw [hsplit, Summable.tsum_add (hlin.summable.mul_left _) (hgeom2.summable.mul_left _)]\n  rw [tsum_mul_left, tsum_mul_left, hlin, hgeom2]\n  ring\n\n/-- log 2 \u2264 1 (since 2 \u2264 e). -/\nlemma log_two_le_one : Real.log 2 \u2264 1 := by\n  rw [show (1 : \u211d) = Real.log (Real.exp 1) by rw [Real.log_exp]]\n  apply Real.log_le_log (by norm_num)\n  have h := Real.exp_one_gt_d9\n  linarith\n\n/-- For X \u2265 200: (4A\u2080/X)\u00b7(10\u00b7log 2 + 2\u00b7log X) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\nlemma dyadic_tail_constant {X : \u211d} (hX : 200 \u2264 X) :\n    (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n      \u2264 16 * A0count * Real.log X / X := by\n  have hX0 : (0 : \u211d) < X := by linarith\n  have hlogX : 5 \u2264 Real.log X := by\n    rw [show (5 : \u211d) = Real.log (Real.exp 5) by rw [Real.log_exp]]\n    apply Real.log_le_log (Real.exp_pos _)\n    have h1 : Real.exp 5 = (Real.exp 1) ^ 5 := by\n      rw [\u2190 Real.exp_nat_mul]\n      norm_num\n    have h2 := Real.exp_one_lt_d9.le\n    have h3 : (Real.exp 1) ^ 5 \u2264 (2.718281829 : \u211d) ^ 5 :=\n      pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n    have h4 : (2.718281829 : \u211d) ^ 5 \u2264 200 := by norm_num\n    linarith [h1, h3, h4]\n  have hlog2 := log_two_le_one\n  have hA0 : (0 : \u211d) \u2264 4 * A0count / X := by positivity\n  have h1 : 10 * Real.log 2 + 2 * Real.log X \u2264 4 * Real.log X := by linarith\n  calc (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X)\n      \u2264 (4 * A0count / X) * (4 * Real.log X) := mul_le_mul_of_nonneg_left h1 hA0\n    _ = 16 * A0count * Real.log X / X := by ring\n\n/-- The dyadic class of a zero relative to scale X:\nNat.log 2 \u230a|im \u03c1|/X\u230b\u208a, so 2^j\u00b7X \u2264 |im \u03c1| < 2^{j+1}\u00b7X when |im \u03c1| \u2265 X. -/\ndef dyadClass (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2115 :=\n  Nat.log 2 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a\n\nlemma dyadClass_lower {X : \u211d} (hX : 0 < X) {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}}\n    (h\u03c1 : X \u2264 |(\u03c1 : \u2102).im|) :\n    (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 |(\u03c1 : \u2102).im| := by\n  have hfl : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a \u2260 0 := by\n    rw [Ne, Nat.floor_eq_zero]\n    push Not\n    have h1 : (1 : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := (le_div_iff\u2080 hX).mpr (by linarith)\n    linarith\n  have h2 := Nat.pow_log_le_self 2 hfl\n  have h3 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a := by exact_mod_cast h2\n  have h4 : (\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) \u2264 |(\u03c1 : \u2102).im| / X := Nat.floor_le (by positivity)\n  have h5 : ((2 ^ dyadClass X \u03c1 : \u2115) : \u211d) = (2 : \u211d) ^ dyadClass X \u03c1 := by push_cast; ring\n  rw [h5] at h3\n  rw [le_div_iff\u2080 hX] at h4\n  linarith\n\nlemma dyadClass_upper {X : \u211d} (hX : 0 < X) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n    |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) * X := by\n  have h2 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a < 2 ^ (dyadClass X \u03c1 + 1) :=\n    Nat.lt_pow_succ_log_self (by norm_num) _\n  have h3 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a : \u211d) + 1) \u2264 (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n    have h4 : \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 \u2264 2 ^ (dyadClass X \u03c1 + 1) := h2\n    have h5 : ((\u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 : \u2115) : \u211d) \u2264 ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) := by\n      exact_mod_cast h4\n    push_cast at h5\n    linarith\n  have h6 : |(\u03c1 : \u2102).im| / X < \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a + 1 := Nat.lt_floor_add_one _\n  have h7 : ((2 ^ (dyadClass X \u03c1 + 1) : \u2115) : \u211d) = (2 : \u211d) ^ (dyadClass X \u03c1 + 1) := by\n    push_cast; ring\n  rw [h7] at h3\n  have h8 := (div_lt_iff\u2080 hX).mpr ((Nat.lt_floor_add_one _).trans_le h3)\n  linarith\n\n/-- The tail summand (if-form on the zero subtype). -/\ndef tailTerm (X : \u211d) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u211d :=\n  if X < |(\u03c1 : \u2102).im| then (zeroMult \u03c1 : \u211d) / (1 + \u03c1.im ^ 2) else 0\n\nlemma tailTerm_nonneg {X : \u211d} (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n    0 \u2264 tailTerm X \u03c1 := by\n  by_cases h : X < |(\u03c1 : \u2102).im| <;>\n    simp [tailTerm, h, div_nonneg (Nat.cast_nonneg _)\n      (by positivity : (0 : \u211d) \u2264 1 + \u03c1.im ^ 2)]\n\n/-- The tail summand is summable (dominated by 2\u00b7m/(1+\u2016\u03b3\u2016\u00b2) via\n1 + \u2016\u03b3\u2016\u00b2 \u2264 2(1 + im\u00b2)). -/\nlemma tailTerm_summable (X : \u211d) :\n    Summable (tailTerm X) := by\n  have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n      2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))) :=\n    (WeilEF.zero_sum_inv_sq zetaSeam).mul_left 2\n  apply Summable.of_norm_bounded hbase\n  intro \u03c1\n  rw [tailTerm]\n  by_cases h : X < |(\u03c1 : \u2102).im|\n  \u00b7 rw [if_pos h]\n    have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n        = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n      rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n      ring\n    have hcmp : 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 2 * (1 + (\u03c1 : \u2102).im ^ 2) := by\n      rw [hgam]\n      have hre : ((\u03c1 : \u2102).re - 1 / 2) ^ 2 \u2264 1 / 4 := by\n        have h0 := \u03c1.2.2.1\n        have h1 := \u03c1.2.2.2\n        nlinarith [sq_nonneg ((\u03c1 : \u2102).re - 1 / 2)]\n      nlinarith [sq_nonneg (\u03c1 : \u2102).im]\n    have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n      have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102)); linarith\n    have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n    have hfrac : 1 / (1 + (\u03c1 : \u2102).im ^ 2) \u2264 2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n      rw [div_le_div_iff\u2080 hpos2 hpos1]\n      nlinarith [hcmp]\n    have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n    calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016\n        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by\n          rw [norm_div, Nat.cast_nonneg, ...]  -- placeholder\n      _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by\n          rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\n              = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]\n          rw [show 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))))\n              = (zeroMult \u03c1 : \u211d) * (2 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\n          exact mul_le_mul_of_nonneg_left hfrac hm\n  \u00b7 rw [if_neg h]\n    positivity\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 461,
      "oldLines": 8,
      "newStart": 461,
      "newLines": 8,
      "lines": [
        "       nlinarith [hcmp]",
        "     have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _",
        "     calc \u2016(zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)\u2016",
        "-        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by",
        "-          rw [norm_div, Nat.cast_nonneg, ...]  -- placeholder",
        "+        = (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) :=",
        "+          norm_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)",
        "       _ \u2264 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := by",
        "           rw [show (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)",
        "               = (zeroMult \u03c1 : \u211d) * (1 / (1 + (\u03c1 : \u2102).im ^ 2)) from by ring]"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}