← Session 7 — All-forks plan approved; E-016 Herglotz work
thinking (487 chars)
Another network glitch. State: E-016 fixes applied but not yet rerun. Just rerun it. Also should add the xi_err to checks? I added print but didn't wire xi_err into checks — V2 check exists. Let me wire xi_err into the meta at least... Minor: add to checks dict? Keep simple: it's printed; also add to key_values later? To avoid more edit cycles, just run — actually the check should gate. Quick edit: add "xi_flint_crosscheck_rel" to key_values in meta. Let me do that quickly then run.
Same network glitch — no harm done. The fixes are in place; let me wire the flint cross-check into the metadata and rerun.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-016-herglotz-fine-structure.py",
"old_string": " \"key_values\": {\n \"rhoF_finitediff_max_rel\": v2_err,",
"new_string": " \"key_values\": {\n \"xi_flint_crosscheck_rel\": xi_err,\n \"rhoF_finitediff_max_rel\": v2_err,"
}
result 2026-08-18 10:50:42Z → 2026-08-23 22:43:09Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean",
"oldString": " have h2 : |-M| = M := abs_neg M",
"newString": " have h2 : |-M| = M := by\n rw [abs_neg]\n exact abs_of_nonneg (by linarith [hM1'] : (0 : \u211d) \u2264 M)",
"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 hgeom2H : Summable (fun j : \u2115 => ((1 : \u211d) / 2) ^ j) := summable_geometric_two\n have hgeom2 : \u2211' j : \u2115, ((1 : \u211d) / 2) ^ j = 2 := tsum_geometric_two\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\n have hlin : \u2211' j : \u2115, (j : \u211d) * ((1 : \u211d) / 2) ^ j = 2 := by\n have h := hlinH.tsum_eq\n norm_num at h\n exact h\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 have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit, Summable.tsum_add (hlinH.summable.mul_left _) (hgeom2H.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.7182818286 : \u211d) ^ 5 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 5\n have h4 : (2.7182818286 : \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 :=\n div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le\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 have h6 : (2 : \u211d) ^ dyadClass X \u03c1 * X \u2264 \u230a|(\u03c1 : \u2102).im| / X\u230b\u208a * X :=\n mul_le_mul_of_nonneg_right h3 hX.le\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 < (2 : \u211d) ^ (dyadClass X \u03c1 + 1) :=\n (Nat.lt_floor_add_one _).trans_le h3\n rw [div_lt_iff\u2080 hX] at h6\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 : \u2102).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 : \u2102).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 [Real.norm_eq_abs, abs_of_nonneg (div_nonneg (Nat.cast_nonneg _) hpos2.le)]\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, norm_zero]\n have hnn := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n exact mul_nonneg (by norm_num) (div_nonneg (Nat.cast_nonneg _) (by linarith))\n\n/-- The dyadic log series is summable. -/\nlemma dyadicLog_summable (X : \u211d) :\n Summable (fun j : \u2115 => ((j + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j) := by\n have hlinH := hasSum_coe_mul_geometric_of_norm_lt_one (r := (1 : \u211d) / 2) (by norm_num)\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 have hj : (2 : \u211d) ^ j \u2260 0 := pow_ne_zero _ two_ne_zero\n rw [one_div_pow]\n field_simp\n ring\n rw [hsplit]\n exact (hlinH.summable.mul_left _).add (summable_geometric_two.mul_left _)\n\n/-- The dyadic fiber {dyadClass X \u03c1 = j} is finite. -/\nlemma dyadClass_fiber_finite {X : \u211d} (hX : 0 < X) (j : \u2115) :\n {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j}.Finite := by\n apply (finite_subtype_norm_lt (1 + (2 : \u211d) ^ (j + 1) * X + 1)).subset\n intro \u03c1 h\u03c1\n have h\u03c1j : dyadClass X \u03c1 = j := h\u03c1\n have hup := dyadClass_upper hX \u03c1\n rw [h\u03c1j] at hup\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 \u2264 |(\u03c1 : \u2102).re| + |(\u03c1 : \u2102).im| :=\n Complex.norm_le_abs_re_add_abs_im _\n have hre : |(\u03c1 : \u2102).re| \u2264 1 := by\n rw [abs_le]\n exact \u27e8by linarith [\u03c1.2.2.1], by linarith [\u03c1.2.2.2]\u27e9\n have h2pow : (0 : \u211d) \u2264 (2 : \u211d) ^ (j + 1) * X := by positivity\n show \u2016(\u03c1 : \u2102)\u2016 < 1 + (2 : \u211d) ^ (j + 1) * X + 1\n linarith\n\n/-- The fiber count: the zeros in the dyadic fiber with X < |\u03b3| have\nmultiplicity-sum \u2264 A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/\nlemma fiber_mult_count {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211 \u03c1 \u2208 (Set.Finite.subset (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset,\n (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n classical\n have hX0 : (0 : \u211d) < X := by linarith\n have h2jX : (0 : \u211d) < (2 : \u211d) ^ j * X := by positivity\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n set FS := (Set.Finite.subset (dyadClass_fiber_finite (by linarith : (0 : \u211d) < X) j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset with hFS\n have hmemFS : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u03c1 \u2208 FS \u2194 dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im| := by\n intro \u03c1\n rw [hFS, Set.Finite.mem_toFinset]\n exact Iff.rfl\n have hW1 : (Zeta23.zerosIn ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X)).Finite :=\n Zeta23.zerosIn_finite _ _\n have hW2 : (Zeta23.zerosIn (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X))).Finite :=\n Zeta23.zerosIn_finite _ _\n have himg : FS.image (Subtype.val) \u2286 hW1.toFinset \u222a hW2.toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n rw [hmemFS] at h\u03c1\n obtain \u27e8h\u03c1j, hgt\u27e9 := h\u03c1\n have hup : |(\u03c1 : \u2102).im| < (2 : \u211d) ^ (j + 1) * X := by\n have h := dyadClass_upper hX0 \u03c1\n rw [h\u03c1j] at h\n exact h\n have hlo : (2 : \u211d) ^ j * X \u2264 |(\u03c1 : \u2102).im| := by\n have h := dyadClass_lower hX0 (show X \u2264 |(\u03c1 : \u2102).im| from hgt.le)\n rw [h\u03c1j] at h\n exact h\n rcases le_or_gt 0 (\u03c1 : \u2102).im with him | him\n \u00b7 apply Finset.mem_union_left\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_nonneg him] at hlo\n linarith\n \u00b7 rw [abs_of_nonneg him] at hup\n linarith\n \u00b7 apply Finset.mem_union_right\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_neg him] at hup\n linarith\n \u00b7 rw [abs_of_neg him] at hlo\n linarith\n have hsum_img : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.val_injective h)]\n have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : (2 : \u211d) ^ j * X - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -((2 : \u211d) ^ j * X) := hz2.2.2\n have hge : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1le : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1le, hX]\n linarith\n calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) := hsum_img\n _ \u2264 \u2211 z \u2208 hW1.toFinset \u222a hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg himg (fun z _ _ => Nat.cast_nonneg _)\n _ = \u2211 z \u2208 hW1.toFinset, (zeroMult z : \u211d) + \u2211 z \u2208 hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_union hdisj\n _ = (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n + (Zeta23.Ncount (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X)) : \u211d) := by\n rw [Zeta23.Ncount, Zeta23.Ncount, finsum_mem_eq_finite_toFinset_sum _ hW1,\n finsum_mem_eq_finite_toFinset_sum _ hW2, Nat.cast_sum, Nat.cast_sum]\n _ \u2264 A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n have h2jX1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1, hX]\n have hpowX : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by\n rw [pow_succ']; ring\n have hlogpos : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n linarith [h2j1X]\n have h1 := Ncount_le_of_interval_gen (a := (2 : \u211d) ^ j * X - 1)\n (b := (2 : \u211d) ^ (j + 1) * X) (by linarith [hpowX, h2jX1])\n have h2 := Ncount_le_of_interval_gen (a := -((2 : \u211d) ^ (j + 1) * X))\n (b := -((2 : \u211d) ^ j * X)) (by linarith [hpowX, h2jX1])\n -- the log arguments match L = log(3\u00b72^{j+1}X + 5)\n have hlog1 : Real.log (3 * max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |(2 : \u211d) ^ j * X - 1| |(2 : \u211d) ^ (j + 1) * X|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_of_nonneg (by linarith [h2jX1])]\n nlinarith [h2jX, h2j1X]\n \u00b7 rw [abs_of_nonneg h2j1X.le]\n linarith [hmax]\n have hlog2 : Real.log (3 * max |-((2 : \u211d) ^ (j + 1) * X)| |-((2 : \u211d) ^ j * X)| + 5)\n \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_le_log (by positivity)\n have hmax : max |-((2 : \u211d) ^ (j + 1) * X)| |-((2 : \u211d) ^ j * X)|\n \u2264 (2 : \u211d) ^ (j + 1) * X := by\n apply max_le\n \u00b7 rw [abs_neg, abs_of_nonneg h2j1X.le]\n \u00b7 rw [abs_neg, abs_of_nonneg h2jX.le]\n nlinarith [h2jX, h2j1X]\n linarith [hmax]\n -- the lengths: b\u2212a+1 = 2^jX + 2 and 2^jX + 1\n have hlen1 : (2 : \u211d) ^ (j + 1) * X - ((2 : \u211d) ^ j * X - 1) + 1\n = (2 : \u211d) ^ j * X + 2 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n rw [hpow]\n ring\n have hlen2 : -((2 : \u211d) ^ j * X) - (-((2 : \u211d) ^ (j + 1) * X)) + 1\n = (2 : \u211d) ^ j * X + 1 := by\n have hpow : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n rw [hpow]\n ring\n rw [hlen1] at h1\n rw [hlen2] at h2\n -- assemble: A\u2080(2^jX+2)L + A\u2080(2^jX+1)L = A\u2080(2^{j+1}X+3)L\n have hA0 := A0count_pos.le\n have h1' : (Zeta23.Ncount ((2 : \u211d) ^ j * X - 1) ((2 : \u211d) ^ (j + 1) * X) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 2) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h1.trans (mul_le_mul_of_nonneg_left hlog1 (by positivity))\n have h2' : (Zeta23.Ncount (-((2 : \u211d) ^ (j + 1) * X)) (-((2 : \u211d) ^ j * X)) : \u211d)\n \u2264 A0count * ((2 : \u211d) ^ j * X + 1) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) :=\n h2.trans (mul_le_mul_of_nonneg_left hlog2 (by positivity))\n have hpow : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by rw [pow_succ']; ring\n rw [hpow] at h1' h2' \u22a2\n linarith [h1', h2', hA0, hlogpos]\n\n/-- The per-fiber tail bound (in \u211d\u22650\u221e): the sum of ofReal(tailTerm X)\nover the dyadic fiber (dyadClass X)\u207b\u00b9'{j} is at most ofReal of\n(1/(2^j X)\u00b2)\u00b7A\u2080\u00b7(2^{j+1}X+3)\u00b7log(3\u00b72^{j+1}X+5). -/\nlemma fiber_tail_le {X : \u211d} (hX : 200 \u2264 X) (j : \u2115) :\n \u2211' b : (dyadClass X) \u207b\u00b9' {j}, ENNReal.ofReal (tailTerm X b.1)\n \u2264 ENNReal.ofReal ((1 / ((2 : \u211d) ^ j * X) ^ 2) *\n (A0count * ((2 : \u211d) ^ (j + 1) * X + 3)\n * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5))) := by\n classical\n have hX0 : (0 : \u211d) < X := by linarith\n have hfin : ((dyadClass X) \u207b\u00b9' {j} : Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1}).Finite := by\n have h := dyadClass_fiber_finite hX0 j\n have h2 : ((dyadClass X) \u207b\u00b9' {j} : Set {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n = {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j} := by\n ext \u03c1\n exact Iff.rfl\n rw [h2]\n exact h\n have htsum : \u2211' b : (dyadClass X) \u207b\u00b9' {j}, ENNReal.ofReal (tailTerm X b.1)\n = \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n ((dyadClass X) \u207b\u00b9' {j}).indicator (fun \u03c1 => ENNReal.ofReal (tailTerm X \u03c1)) \u03c1 :=\n tsum_subtype ((dyadClass X) \u207b\u00b9' {j})\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => ENNReal.ofReal (tailTerm X \u03c1))\n rw [htsum]\n rw [tsum_eq_sum (s := hfin.toFinset) (fun \u03c1 h\u03c1 => by\n apply Set.indicator_of_notMem\n rwa [Set.Finite.mem_toFinset] at h\u03c1)]\n rw [Finset.sum_congr rfl (fun \u03c1 h\u03c1 =>\n Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at h\u03c1) _)]\n rw [\u2190 ENNReal.ofReal_sum_of_nonneg (fun \u03c1 _ => tailTerm_nonneg \u03c1)]\n apply ENNReal.ofReal_le_ofReal\n rw [\u2190 Finset.sum_filter_add_sum_filter_not hfin.toFinset\n (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => X < |(\u03c1 : \u2102).im|) (tailTerm X)]\n have hzero : \u2211 \u03c1 \u2208 hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => \u00ac X < |(\u03c1 : \u2102).im|), tailTerm X \u03c1 = 0 := by\n apply Finset.sum_eq_zero\n intro \u03c1 h\u03c1\n rw [Finset.mem_filter] at h\u03c1\n rw [tailTerm, if_neg h\u03c1.2]\n rw [hzero, add_zero]\n have hfilter_eq : hfin.toFinset.filter (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} => X < |(\u03c1 : \u2102).im|)\n = (Set.Finite.subset (dyadClass_fiber_finite hX0 j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset := by\n ext \u03c1\n simp only [Finset.mem_filter, Set.Finite.mem_toFinset]\n exact Iff.rfl\n rw [hfilter_eq]\n calc \u2211 \u03c1 \u2208 (Set.Finite.subset (dyadClass_fiber_finite hX0 j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset, tailTerm X \u03c1\n \u2264 \u2211 \u03c1 \u2208 (Set.Finite.subset (dyadClass_fiber_finite hX0 j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset,\n (1 / ((2 : \u211d) ^ j * X) ^ 2) * (zeroMult (\u03c1 : \u2102) : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n rw [Set.Finite.mem_toFinset] at h\u03c1\n obtain \u27e8h\u03c1j, hgt\u27e9 := h\u03c1\n have hlo : (2 : \u211d) ^ j * X \u2264 |(\u03c1 : \u2102).im| := by\n have h := dyadClass_lower hX0 (show X \u2264 |(\u03c1 : \u2102).im| from hgt.le)\n rw [h\u03c1j] at h\n exact h\n have hlo2 : ((2 : \u211d) ^ j * X) ^ 2 \u2264 ((\u03c1 : \u2102).im) ^ 2 := by\n have h := pow_le_pow_left\u2080 (by positivity : (0 : \u211d) \u2264 (2 : \u211d) ^ j * X) hlo 2\n rwa [sq_abs] at h\n have hsq : ((2 : \u211d) ^ j * X) ^ 2 \u2264 1 + ((\u03c1 : \u2102).im) ^ 2 := by\n linarith [hlo2, sq_nonneg (\u03c1 : \u2102).im]\n have hpos1 : (0 : \u211d) < 1 + ((\u03c1 : \u2102).im) ^ 2 := by positivity\n have hpos2 : (0 : \u211d) < ((2 : \u211d) ^ j * X) ^ 2 := by positivity\n rw [tailTerm, if_pos hgt]\n rw [show (zeroMult (\u03c1 : \u2102) : \u211d) / (1 + ((\u03c1 : \u2102).im) ^ 2)\n = (zeroMult (\u03c1 : \u2102) : \u211d) * (1 / (1 + ((\u03c1 : \u2102).im) ^ 2)) from by ring]\n rw [show (1 / ((2 : \u211d) ^ j * X) ^ 2) * (zeroMult (\u03c1 : \u2102) : \u211d)\n = (zeroMult (\u03c1 : \u2102) : \u211d) * (1 / ((2 : \u211d) ^ j * X) ^ 2) from by ring]\n apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)\n rw [div_le_div_iff\u2080 hpos1 hpos2]\n nlinarith [hsq]\n _ = (1 / ((2 : \u211d) ^ j * X) ^ 2) *\n \u2211 \u03c1 \u2208 (Set.Finite.subset (dyadClass_fiber_finite hX0 j)\n (t := {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | dyadClass X \u03c1 = j \u2227 X < |(\u03c1 : \u2102).im|})\n (fun \u03c1 h\u03c1 => h\u03c1.1)).toFinset, (zeroMult (\u03c1 : \u2102) : \u211d) := by\n rw [Finset.mul_sum]\n _ \u2264 (1 / ((2 : \u211d) ^ j * X) ^ 2) *\n (A0count * ((2 : \u211d) ^ (j + 1) * X + 3)\n * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5)) :=\n mul_le_mul_of_nonneg_left (fiber_mult_count hX j) (by positivity)\n\n/-- **The far-tail bound**: for X \u2265 200, the zeros with |\u03b3| > X\ncontribute \u03a3 m/(1+\u03b3\u00b2) \u2264 16\u00b7A\u2080\u00b7log X / X. -/\ntheorem zero_tail_inv_sq_le {X : \u211d} (hX : 200 \u2264 X) :\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, tailTerm X \u03c1\n \u2264 16 * A0count * Real.log X / X := by\n have hX0 : (0 : \u211d) < X := by linarith\n have hlogXnn : (0 : \u211d) \u2264 Real.log X := Real.log_nonneg (by linarith)\n have hC0 : (0 : \u211d) \u2264 16 * A0count * Real.log X / X :=\n div_nonneg (mul_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hlogXnn) hX0.le\n rw [\u2190 ENNReal.ofReal_le_ofReal_iff hC0]\n rw [ENNReal.ofReal_tsum_of_nonneg (fun \u03c1 => tailTerm_nonneg \u03c1) (tailTerm_summable X)]\n rw [\u2190 ENNReal.tsum_fiberwise (fun \u03c1 => ENNReal.ofReal (tailTerm X \u03c1)) (dyadClass X)]\n -- the real dyadic majorant\n set F : \u2115 \u2192 \u211d := fun j => (1 / ((2 : \u211d) ^ j * X) ^ 2) *\n (A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5)) with hFdef\n set G : \u2115 \u2192 \u211d := fun j => (((j : \u211d) + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j with hGdef\n have hFnn : \u2200 j : \u2115, 0 \u2264 F j := by\n intro j\n rw [hFdef]\n have hL : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n linarith\n have h2j1X : (0 : \u211d) \u2264 (2 : \u211d) ^ (j + 1) * X := by positivity\n exact mul_nonneg (div_nonneg (by norm_num) (by positivity))\n (mul_nonneg (mul_nonneg A0count_pos.le (by linarith)) hL)\n have hGnn : \u2200 j : \u2115, 0 \u2264 (4 * A0count / X) * G j := by\n intro j\n rw [hGdef]\n have hlog2nn : (0 : \u211d) \u2264 Real.log 2 := Real.log_nonneg (by norm_num)\n have hjn : (0 : \u211d) \u2264 (j : \u211d) := Nat.cast_nonneg j\n have hGj : (0 : \u211d) \u2264 (((j : \u211d) + 4) * Real.log 2 + Real.log X) :=\n add_nonneg (mul_nonneg (by linarith) hlog2nn) hlogXnn\n exact mul_nonneg (div_nonneg (mul_nonneg (by norm_num) A0count_pos.le) hX0.le)\n (div_nonneg hGj (by positivity))\n have hFle : \u2200 j : \u2115, F j \u2264 (4 * A0count / X) * G j := by\n intro j\n rw [hFdef, hGdef]\n show (1 / ((2 : \u211d) ^ j * X) ^ 2)\n * (A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5))\n \u2264 (4 * A0count / X)\n * ((((j : \u211d) + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n have h2jX1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1 : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1, hX]\n have h2jX : (0 : \u211d) < (2 : \u211d) ^ j * X := by positivity\n have h2j1X : (0 : \u211d) < (2 : \u211d) ^ (j + 1) * X := by positivity\n have h2j : (0 : \u211d) < (2 : \u211d) ^ j := by positivity\n have hLnn : (0 : \u211d) \u2264 Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by\n apply Real.log_nonneg\n linarith\n -- log(3\u00b72^{j+1}X+5) \u2264 (j+4)\u00b7log 2 + log X\n have hlogle : Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5)\n \u2264 ((j : \u211d) + 4) * Real.log 2 + Real.log X := by\n have harg : 3 * (2 : \u211d) ^ (j + 1) * X + 5 \u2264 (2 : \u211d) ^ (j + 4) * X := by\n have hpow : (2 : \u211d) ^ (j + 4) = 16 * (2 : \u211d) ^ j := by\n rw [show (2 : \u211d) ^ (j + 4) = (2 : \u211d) ^ j * (2 : \u211d) ^ 4 from by rw [\u2190 pow_add]]\n ring_nf\n rw [hpow]\n have hpow2 : (2 : \u211d) ^ (j + 1) = 2 * (2 : \u211d) ^ j := by rw [pow_succ']\n rw [hpow2]\n nlinarith [h2jX1, h2jX]\n have hlogeq : Real.log ((2 : \u211d) ^ (j + 4) * X)\n = ((j : \u211d) + 4) * Real.log 2 + Real.log X := by\n rw [Real.log_mul (by positivity : (2 : \u211d) ^ (j + 4) \u2260 0) (by linarith : X \u2260 0)]\n rw [Real.log_pow]\n push_cast\n ring\n rw [\u2190 hlogeq]\n exact Real.log_le_log (by positivity) harg\n -- the two factor bounds\n have hfac1 : A0count * ((2 : \u211d) ^ (j + 1) * X + 3) / ((2 : \u211d) ^ j * X) ^ 2\n \u2264 (4 * A0count) / (X * (2 : \u211d) ^ j) := by\n rw [div_le_div_iff\u2080 (by positivity) (by positivity)]\n have hpow : (2 : \u211d) ^ (j + 1) * X = 2 * ((2 : \u211d) ^ j * X) := by rw [pow_succ']; ring\n have h2jX200 : (200 : \u211d) \u2264 (2 : \u211d) ^ j * X := by\n have h1p : (1 : \u211d) \u2264 (2 : \u211d) ^ j := by exact_mod_cast Nat.one_le_two_pow\n nlinarith [h1p, hX]\n have hkey : A0count * ((2 : \u211d) ^ j * X) * 3\n \u2264 A0count * ((2 : \u211d) ^ j * X) * (2 * ((2 : \u211d) ^ j * X)) := by\n apply mul_le_mul_of_nonneg_left _ (mul_nonneg A0count_pos.le (by positivity))\n linarith [h2jX200]\n rw [hpow]\n have hA0 := A0count_pos.le\n nlinarith [hkey, h2jX, hA0]\n have h1 : (1 / ((2 : \u211d) ^ j * X) ^ 2) *\n (A0count * ((2 : \u211d) ^ (j + 1) * X + 3) * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5))\n = (A0count * ((2 : \u211d) ^ (j + 1) * X + 3) / ((2 : \u211d) ^ j * X) ^ 2)\n * Real.log (3 * (2 : \u211d) ^ (j + 1) * X + 5) := by ring\n rw [h1]\n have h2 : (4 * A0count / X) * ((((j : \u211d) + 4) * Real.log 2 + Real.log X) / (2 : \u211d) ^ j)\n = ((4 * A0count) / (X * (2 : \u211d) ^ j))\n * (((j : \u211d) + 4) * Real.log 2 + Real.log X) := by\n field_simp\n rw [h2]\n apply mul_le_mul hfac1 hlogle hLnn\n apply div_nonneg _ (mul_nonneg hX0.le (by positivity))\n exact mul_nonneg (by norm_num) A0count_pos.le\n have hGsum : Summable (fun j : \u2115 => (4 * A0count / X) * G j) :=\n (dyadicLog_summable X).mul_left _\n have hFsum : Summable F := by\n apply Summable.of_norm_bounded hGsum\n intro j\n rw [Real.norm_eq_abs, abs_of_nonneg (hFnn j)]\n exact hFle j\n have hGtotal : \u2211' j : \u2115, G j = 10 * Real.log 2 + 2 * Real.log X := tsum_dyadic_log X\n have htotal : \u2211' j : \u2115, F j \u2264 16 * A0count * Real.log X / X := by\n calc \u2211' j : \u2115, F j \u2264 \u2211' j : \u2115, (4 * A0count / X) * G j :=\n Summable.tsum_le_tsum hFle hFsum hGsum\n _ = (4 * A0count / X) * (10 * Real.log 2 + 2 * Real.log X) := by\n rw [tsum_mul_left, hGtotal]\n _ \u2264 16 * A0count * Real.log X / X := dyadic_tail_constant hX\n calc \u2211' j : \u2115, \u2211' b : (dyadClass X) \u207b\u00b9' {j}, ENNReal.ofReal (tailTerm X b.1)\n \u2264 \u2211' j : \u2115, ENNReal.ofReal (F j) := by\n apply ENNReal.tsum_le_tsum\n intro j\n exact fiber_tail_le hX j\n _ = ENNReal.ofReal (\u2211' j : \u2115, F j) := (ENNReal.ofReal_tsum_of_nonneg hFnn hFsum).symm\n _ \u2264 ENNReal.ofReal (16 * A0count * Real.log X / X) := ENNReal.ofReal_le_ofReal htotal\n\n/-! ## 5. The threshold lemma and the zero-free circle (5e-v-b chunk 3a)\n\nThe \u03b3-gap circle radius R \u2208 [4k+5/2, 4k+3] with k \u2265 4000 satisfies\n416\u00b7\u0108\u2080(4k+9/2) \u2264 4k+5/2 \u2264 R (`gapCircle_threshold`) \u2014 explicit\nlinear/rational arithmetic from the two exp facts 2.7\u00b9\u2070 \u2265 16006.5 and\n2.72\u2079 \u2264 16006.5 plus log x \u2264 x\u22121. Consequences: 16\u00b7\u0108\u2080 < R (the circle\ncarries NO nontrivial zero, `not_isNontrivialZero_on_gapCircle`) and\n13/R \u2264 1/(32\u00b7\u0108\u2080) (the critical-arc clearance, used in the shell bounds\nof the next chunk). -/\n\n/-- **The threshold lemma**: for k \u2265 4000, 416\u00b7\u0108\u2080(4k+9/2) \u2264 4k+5/2.\nBase bound \u0108\u2080(16004.5) \u2264 9.3564 (log 16006.5 \u2264 10 via 2.7\u00b9\u2070 \u2265 16006.5;\nlog log \u2264 log 10 \u2264 2.4 via e^{2.4} \u2265 10.2); increment\n\u0108\u2080(x) \u2212 \u0108\u2080(16004.5) \u2264 0.532\u00b7(x\u221216004.5)/16006.5 via log(a/b) \u2264 a/b \u2212 1\n(twice; log 16006.5 \u2265 9 via 2.72\u2079 \u2264 16006.5). -/\ntheorem gapCircle_threshold {k : \u2115} (hk : 4000 \u2264 k) :\n 416 * C0hat (4 * (k : \u211d) + 9 / 2) \u2264 4 * (k : \u211d) + 5 / 2 := by\n have hk4 : (16000 : \u211d) \u2264 4 * (k : \u211d) := by\n have hkR : (4000 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast hk\n linarith\n -- the exp facts\n have he10 : (16006.5 : \u211d) \u2264 Real.exp 10 := by\n have h1 : Real.exp 10 = (Real.exp 1) ^ 10 := by\n rw [\u2190 Real.exp_nat_mul]; norm_num\n have h2 : (2.7 : \u211d) \u2264 Real.exp 1 := by\n have h := Real.exp_one_gt_d9; linarith\n have h3 : (2.7 : \u211d) ^ 10 \u2264 (Real.exp 1) ^ 10 :=\n pow_le_pow_left\u2080 (by norm_num) h2 10\n have h4 : (16006.5 : \u211d) \u2264 (2.7 : \u211d) ^ 10 := by norm_num\n linarith [h1, h3, h4]\n have hL0up : Real.log (16006.5) \u2264 10 := by\n rw [show (10 : \u211d) = Real.log (Real.exp 10) by rw [Real.log_exp]]\n exact Real.log_le_log (by norm_num) he10\n have he9 : Real.exp 9 \u2264 (16006.5 : \u211d) := by\n have h1 : Real.exp 9 = (Real.exp 1) ^ 9 := by\n rw [\u2190 Real.exp_nat_mul]; norm_num\n have h2 : Real.exp 1 \u2264 (2.72 : \u211d) := by\n have h := Real.exp_one_lt_d9.le; linarith\n have h3 : (Real.exp 1) ^ 9 \u2264 (2.72 : \u211d) ^ 9 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 9\n have h4 : (2.72 : \u211d) ^ 9 \u2264 16006.5 := by norm_num\n linarith [h1, h3, h4]\n have hL0lo : (9 : \u211d) \u2264 Real.log (16006.5) := by\n rw [show (9 : \u211d) = Real.log (Real.exp 9) by rw [Real.log_exp]]\n exact Real.log_le_log (Real.exp_pos _) he9\n have he2 : (2.7 : \u211d) ^ 2 \u2264 Real.exp 2 := by\n have h1 : Real.exp 2 = (Real.exp 1) ^ 2 := by\n rw [\u2190 Real.exp_nat_mul]; norm_num\n have h2 : (2.7 : \u211d) \u2264 Real.exp 1 := by\n have h := Real.exp_one_gt_d9; linarith\n have h3 : (2.7 : \u211d) ^ 2 \u2264 (Real.exp 1) ^ 2 :=\n pow_le_pow_left\u2080 (by norm_num) h2 2\n linarith [h1, h3]\n have he04 : (1.4 : \u211d) \u2264 Real.exp 0.4 := by\n have h := Real.add_one_le_exp (0.4 : \u211d)\n linarith\n have he24 : (10 : \u211d) \u2264 Real.exp 2.4 := by\n have h1 : Real.exp 2.4 = Real.exp 2 * Real.exp 0.4 := by\n rw [\u2190 Real.exp_add]; norm_num\n have h2 : (10 : \u211d) \u2264 (2.7 : \u211d) ^ 2 * 1.4 := by norm_num\n have h3 : (2.7 : \u211d) ^ 2 * 1.4 \u2264 Real.exp 2 * Real.exp 0.4 :=\n mul_le_mul he2 he04 (by norm_num) (Real.exp_pos 2).le\n linarith [h1, h3]\n have hlog10 : Real.log 10 \u2264 (2.4 : \u211d) := by\n rw [show (2.4 : \u211d) = Real.log (Real.exp 2.4) by rw [Real.log_exp]]\n exact Real.log_le_log (by norm_num) he24\n have hLL0 : Real.log (Real.log (16006.5)) \u2264 2.4 :=\n (Real.log_le_log (by linarith [hL0lo]) hL0up).trans hlog10\n -- the increments, with x = 4k+9/2, x+2 = 4k+13/2 \u2265 16006.5\n set y : \u211d := 4 * (k : \u211d) with hy\n have hx2 : (16006.5 : \u211d) \u2264 y + 13 / 2 := by linarith\n have h\u0394def : (y + 13 / 2) / 16006.5 - 1 = (y - 16000) / 16006.5 := by\n field_simp\n ring\n have hinc0 : Real.log (y + 13 / 2) - Real.log (16006.5)\n \u2264 (y - 16000) / 16006.5 := by\n have hpos : (0 : \u211d) < (y + 13 / 2) / 16006.5 := by positivity\n have h1 := Real.log_le_sub_one_of_pos hpos\n have h2 : Real.log (y + 13 / 2)\n = Real.log (16006.5) + Real.log ((y + 13 / 2) / 16006.5) := by\n rw [\u2190 Real.log_mul (by norm_num : (16006.5 : \u211d) \u2260 0)\n (by positivity : (y + 13 / 2) / 16006.5 \u2260 0)]\n congr 1\n field_simp\n rw [h\u0394def] at h1\n linarith [h2, h1]\n have hinc1 : Real.log (y + 13 / 2) \u2264 10 + (y - 16000) / 16006.5 := by\n linarith [hinc0, hL0up]\n have hLge : Real.log (16006.5) \u2264 Real.log (y + 13 / 2) :=\n Real.log_le_log (by norm_num) hx2\n have hinc2 : Real.log (Real.log (y + 13 / 2))\n \u2264 2.4 + (Real.log (y + 13 / 2) - Real.log (16006.5)) / 9 := by\n have hpos : (0 : \u211d) < Real.log (y + 13 / 2) / Real.log (16006.5) :=\n div_pos (by linarith [hL0lo, hLge]) (by linarith [hL0lo])\n have h1 := Real.log_le_sub_one_of_pos hpos\n have h2 : Real.log (Real.log (y + 13 / 2))\n = Real.log (Real.log (16006.5))\n + Real.log (Real.log (y + 13 / 2) / Real.log (16006.5)) := by\n rw [\u2190 Real.log_mul (by linarith [hL0lo] : Real.log (16006.5) \u2260 0)\n (by positivity : Real.log (y + 13 / 2) / Real.log (16006.5) \u2260 0)]\n congr 1\n field_simp\n have h3 : Real.log (y + 13 / 2) / Real.log (16006.5) - 1\n \u2264 (Real.log (y + 13 / 2) - Real.log (16006.5)) / 9 := by\n have h4 : Real.log (y + 13 / 2) / Real.log (16006.5) - 1\n = (Real.log (y + 13 / 2) - Real.log (16006.5))\n / Real.log (16006.5) := by\n field_simp\n rw [h4]\n exact div_le_div_of_nonneg_left (by linarith [hLge]) (by norm_num)\n hL0lo\n linarith [h1, h2, h3, hLL0]\n -- assemble: \u0108\u2080(4k+9/2) \u2264 9.3564 + 0.532\u00b7(y\u221216000)/16006.5\n unfold C0hat\n have h\u0394nn : (0 : \u211d) \u2264 (y - 16000) / 16006.5 := by positivity\n have h\u0394le : (y - 16000) / 16006.5 \u2264 (y - 16000) / 16000 :=\n div_le_div_of_nonneg_left (by linarith) (by norm_num) (by norm_num)\n have hC : 0.433 * Real.log (y + 9 / 2 + 2)\n + 0.886 * Real.log (Real.log (y + 9 / 2 + 2)) + 2.9\n \u2264 9.3564 + 0.532 * ((y - 16000) / 16006.5) := by\n have harg : y + 9 / 2 + 2 = y + 13 / 2 := by ring\n rw [harg]\n linarith [hinc1, hinc2, hinc0, h\u0394nn]\n have hC2 : 416 * (0.433 * Real.log (y + 9 / 2 + 2)\n + 0.886 * Real.log (Real.log (y + 9 / 2 + 2)) + 2.9)\n \u2264 416 * (9.3564 + 0.532 * ((y - 16000) / 16006.5)) :=\n mul_le_mul_of_nonneg_left hC (by norm_num)\n have hfin : 416 * (9.3564 + 0.532 * ((y - 16000) / 16006.5))\n \u2264 y + 5 / 2 := by\n have h1 : 416 * (9.3564 + 0.532 * ((y - 16000) / 16006.5))\n \u2264 416 * (9.3564 + 0.532 * ((y - 16000) / 16000)) := by\n exact mul_le_mul_of_nonneg_left\n (add_le_add (le_refl _)\n (mul_le_mul_of_nonneg_left h\u0394le (by norm_num : (0 : \u211d) \u2264 0.532)))\n (by norm_num : (0 : \u211d) \u2264 416)\n have h2 : 416 * (9.3564 + 0.532 * ((y - 16000) / 16000))\n = 3670.9504 + 0.013832 * y := by\n field_simp\n ring\n rw [h2] at h1\n linarith [hk4]\n calc 416 * (0.433 * Real.log (y + 9 / 2 + 2)\n + 0.886 * Real.log (Real.log (y + 9 / 2 + 2)) + 2.9)\n \u2264 416 * (9.3564 + 0.532 * ((y - 16000) / 16006.5)) := hC2\n _ \u2264 y + 5 / 2 := hfin\n\n/-- |im \u03c1| \u2265 \u2016\u03c1\u2016 \u2212 1 for a nontrivial zero (\u2016\u03c1\u2016 \u2264 |re| + |im| \u2264 1 + |im|). -/\nlemma abs_im_ge_norm_sub_one (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n \u2016(\u03c1 : \u2102)\u2016 - 1 \u2264 |(\u03c1 : \u2102).im| := by\n have hnorm : \u2016(\u03c1 : \u2102)\u2016 \u2264 |(\u03c1 : \u2102).re| + |(\u03c1 : \u2102).im| :=\n Complex.norm_le_abs_re_add_abs_im _\n have hre : |(\u03c1 : \u2102).re| \u2264 1 := by\n rw [abs_le]\n exact \u27e8by linarith [\u03c1.2.2.1], by linarith [\u03c1.2.2.2]\u27e9\n linarith\n\n/-- **The gap circle is zero-free**: for k \u2265 4000 and R with the\ngap-circle properties, no point s with \u2016s\u2016 = R is a nontrivial zero.\n(A zero on the circle would have ordinate \u00b1\u221a(R\u00b2\u2212re\u00b2) within 1/R of R,\nbelow the \u03b3-gap clearance 1/(16\u00b7\u0108\u2080) since 16\u00b7\u0108\u2080 < R by the threshold.) -/\ntheorem not_isNontrivialZero_on_gapCircle {k : \u2115} (hk : 4000 \u2264 k)\n {R : \u211d} (hRlo : 4 * (k : \u211d) + 5 / 2 \u2264 R)\n (hgap : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192\n (1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2))) \u2264 |\u03c1.im - R| \u2228\n 1 \u2264 |\u03c1.im - R|)\n {s : \u2102} (hs : \u2016s\u2016 = R) : \u00ac IsNontrivialZero s := by\n intro hz\n have hth := gapCircle_threshold hk\n have h\u01082 : (2 : \u211d) \u2264 C0hat (4 * (k : \u211d) + 9 / 2) := two_le_C0hat (by\n have hkR : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast (by omega : 1 \u2264 k)\n linarith)\n have hR1 : (1 : \u211d) < R := by\n have hkR : (1 : \u211d) \u2264 (k : \u211d) := by exact_mod_cast (by omega : 1 \u2264 k)\n linarith [hRlo]\n -- 16\u00b7\u0108\u2080 < R\n have h16 : 16 * C0hat (4 * (k : \u211d) + 9 / 2) < R := by\n have h1 : 16 * C0hat (4 * (k : \u211d) + 9 / 2)\n < 416 * C0hat (4 * (k : \u211d) + 9 / 2) := by\n have hpos : (0 : \u211d) < C0hat (4 * (k : \u211d) + 9 / 2) := by linarith [h\u01082]\n nlinarith [hpos]\n linarith [hth, hRlo, h1]\n -- the ordinate t = |im s| and its distance to R\n have hnormSq : \u2016s\u2016 ^ 2 = s.re ^ 2 + s.im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n have hre2 : s.re ^ 2 \u2264 1 := by\n have h0 := hz.2.1\n have h1 := hz.2.2\n nlinarith [sq_nonneg s.re]\n have ht_le : |s.im| \u2264 R := by\n have h := abs_im_le_norm s\n rw [hs] at h\n exact h\n have ht2 : |s.im| ^ 2 = R ^ 2 - s.re ^ 2 := by\n have h1 : s.im ^ 2 = R ^ 2 - s.re ^ 2 := by\n have h2 : s.re ^ 2 + s.im ^ 2 = R ^ 2 := by\n rw [\u2190 hnormSq, hs]\n linarith\n rw [sq_abs]\n linarith [h1]\n -- R \u2212 |im s| = re\u00b2/(R+|im s|) \u2264 1/R\n have hRt : R - |s.im| = s.re ^ 2 / (R + |s.im|) := by\n have hne : R + |s.im| \u2260 0 := by positivity\n field_simp\n have h1 : (R - |s.im|) * (R + |s.im|) = R ^ 2 - |s.im| ^ 2 := by ring\n rw [h1, ht2]\n ring\n have hRt_le : R - |s.im| \u2264 1 / R := by\n rw [hRt]\n have h1 : s.re ^ 2 / (R + |s.im|) \u2264 s.re ^ 2 / R := by\n apply div_le_div_of_nonneg_left (sq_nonneg _) (by linarith [hR1])\n have h2 : (0 : \u211d) \u2264 |s.im| := abs_nonneg _\n linarith\n have h3 : s.re ^ 2 / R \u2264 1 / R := by\n apply div_le_div_of_nonneg_right _ (by linarith [hR1])\n linarith [hre2]\n exact h1.trans h3\n -- the witness zero with positive ordinate\n have hkR0 : (0 : \u211d) < R := by linarith [hR1]\n set \u03c1' : \u2102 := if 0 \u2264 s.im then s else (starRingEnd \u2102) s with h\u03c1'\n have h\u03c1'z : IsNontrivialZero \u03c1' := by\n rw [h\u03c1']\n by_cases him : 0 \u2264 s.im\n \u00b7 rw [if_pos him]; exact hz\n \u00b7 rw [if_neg him]; exact isNontrivialZero_conj hz\n have h\u03c1'im : \u03c1'.im = |s.im| := by\n rw [h\u03c1']\n by_cases him : 0 \u2264 s.im\n \u00b7 rw [if_pos him]; exact (abs_of_nonneg him).symm\n \u00b7 rw [if_neg him, Complex.conj_im]\n exact (abs_of_neg (lt_of_not_ge him)).symm\n -- |im \u03c1' \u2212 R| = R \u2212 |im s| \u2264 1/R < min 1 (1/(16\u0108\u2080)): contradiction\n have hgap' := hgap \u03c1' h\u03c1'z\n rw [h\u03c1'im] at hgap'\n have hle : (|s.im| : \u211d) - R \u2264 0 := by linarith [ht_le]\n have hdist : |(|s.im| : \u211d) - R| = R - |s.im| := by\n rw [abs_of_nonpos hle]\n ring\n rw [hdist] at hgap'\n have hsmall : R - |s.im| < 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) := by\n have hpos : (0 : \u211d) < 16 * C0hat (4 * (k : \u211d) + 9 / 2) := by\n linarith [h\u01082]\n have h1 : 1 / R < 1 / (16 * C0hat (4 * (k : \u211d) + 9 / 2)) :=\n one_div_lt_one_div_of_lt hpos h16\n linarith [hRt_le, h1]\n have hsmall1 : R - |s.im| < 1 := by\n have h1 : 1 / R < 1 := (div_lt_one (by linarith [hR1] : (0 : \u211d) < R)).mpr hR1\n linarith [hRt_le, h1]\n rcases hgap' with h | h\n \u00b7 linarith [h, hsmall]\n \u00b7 linarith [h, hsmall1]\n\n/-! ## 6. The per-term norm identity, the count brick, and the tail\napplication (5e-v-b chunk 3b)\n\n`seriesTerm_norm_eq_div`: on the zero-free circle (\u2016s\u2016 = R),\n\u2016seriesTerm s \u03c1\u2016 = m\u00b7R/(\u2016\u03c1\u2016\u00b7\u2016s\u2212\u03c1\u2016) (the key algebra\n1/(s\u2212\u03c1)+1/\u03c1 = s/(\u03c1(s\u2212\u03c1))). `circleZeros R`: the finite part\n{\u2016\u03c1\u2016 < 2R+1}. `sum_zeroMult_le_of_im_band`: the reusable window-count\nbrick \u2014 a zero finset whose ordinates lie in the band [a, b] (with the\nsign-separation c, max a c \u2265 1) has multiplicity-sum \u2264\n3\u00b7A\u2080\u00b7(b\u2212a+2)\u00b7log(3\u00b7max|a||b|+5) (the two-window cover\n(M\u22121, b] \u222a (\u2212b\u22121, \u2212M], M := max a c; the \u22121 paddings absorb the\nnon-strict band bounds; the negative window's log loses +1 via\n3b+8 \u2264 2(3b+5)). `series_tail_le`: the far tail (\u2016\u03c1\u2016 \u2265 2R+1) \u2264\n91\u00b7A\u2080\u00b7log R via `seriesTerm_norm_le` + `zero_tail_inv_sq_le`.\n`seriesFun_norm_le_split`: the ONE tsum split. -/\n\n/-- The per-term norm identity on a zero-free circle. -/\nlemma seriesTerm_norm_eq_div {s : \u2102} {R : \u211d} (hs : \u2016s\u2016 = R)\n (hsz : \u00ac IsNontrivialZero s) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n \u2016seriesTerm s \u03c1\u2016 =\n (zeroMult (\u03c1 : \u2102) : \u211d) * (R / (\u2016(\u03c1 : \u2102)\u2016 * \u2016s - (\u03c1 : \u2102)\u2016)) := by\n have h0 : (\u03c1 : \u2102) \u2260 0 := by\n intro h\n have hre := \u03c1.2.2.1\n rw [h] at hre\n simp at hre\n have h1 : s - (\u03c1 : \u2102) \u2260 0 := by\n intro h\n apply hsz\n have hs_eq : s = (\u03c1 : \u2102) := by rw [\u2190 sub_eq_zero]; exact h\n rw [hs_eq]\n exact \u03c1.2\n have halg := one_div_sub_add_one_div h0 h1\n simp only [seriesTerm]\n rw [halg, norm_mul, RCLike.norm_natCast, norm_div, norm_mul, hs]\n\n/-- The finite-part finset for the circle split: {\u2016\u03c1\u2016 < 2R+1}. -/\ndef circleZeros (R : \u211d) : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1} :=\n (finite_subtype_norm_lt (2 * R + 1)).toFinset\n\nlemma mem_circleZeros {R : \u211d} {\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}} :\n \u03c1 \u2208 circleZeros R \u2194 \u2016(\u03c1 : \u2102)\u2016 < 2 * R + 1 :=\n Set.Finite.mem_toFinset _\n\n/-- **The count brick**: a zero finset with ordinates in the band\n[a, b] (sign-separated by c, 1 \u2264 max a c \u2264 b) has multiplicity-sum\n\u2264 3\u00b7A\u2080\u00b7(b\u2212a+2)\u00b7log(3\u00b7max|a||b|+5). -/\nlemma sum_zeroMult_le_of_im_band (FS : Finset {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n {a b c : \u211d} (hM1 : (1 : \u211d) \u2264 max a c) (hMb : max a c \u2264 b)\n (hsub : \u2200 \u03c1 \u2208 FS, a \u2264 |(\u03c1 : \u2102).im| \u2227 |(\u03c1 : \u2102).im| \u2264 b \u2227 c \u2264 |(\u03c1 : \u2102).im|) :\n \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 3 * A0count * (b - a + 2) * Real.log (3 * max |a| |b| + 5) := by\n classical\n set M := max a c with hM\n have hM1' : (1 : \u211d) \u2264 M := hM1\n have hMb' : M \u2264 b := hMb\n have hb1 : (1 : \u211d) \u2264 b := le_trans hM1' hMb'\n have hW1 : (Zeta23.zerosIn (M - 1) b).Finite := Zeta23.zerosIn_finite _ _\n have hW2 : (Zeta23.zerosIn (-b - 1) (-M)).Finite := Zeta23.zerosIn_finite _ _\n have himg : FS.image (Subtype.val) \u2286 hW1.toFinset \u222a hW2.toFinset := by\n intro z hz\n obtain \u27e8\u03c1, h\u03c1, rfl\u27e9 := Finset.mem_image.mp hz\n have hbnd1 := (hsub \u03c1 h\u03c1).1\n have hbnd2 := (hsub \u03c1 h\u03c1).2.1\n have hbnd3 := (hsub \u03c1 h\u03c1).2.2\n have hMle : M \u2264 |(\u03c1 : \u2102).im| := max_le_iff.mpr \u27e8hbnd1, hbnd3\u27e9\n rcases le_or_gt 0 (\u03c1 : \u2102).im with him | him\n \u00b7 apply Finset.mem_union_left\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_nonneg him] at hMle\n linarith\n \u00b7 rw [abs_of_nonneg him] at hbnd2\n exact hbnd2\n \u00b7 apply Finset.mem_union_right\n rw [Set.Finite.mem_toFinset]\n refine \u27e8\u03c1.2, ?_, ?_\u27e9\n \u00b7 rw [abs_of_neg him] at hbnd2\n linarith\n \u00b7 rw [abs_of_neg him] at hMle\n linarith\n have hdisj : Disjoint hW1.toFinset hW2.toFinset := by\n rw [Finset.disjoint_left]\n intro z hz1 hz2\n rw [Set.Finite.mem_toFinset] at hz1 hz2\n have h1 : M - 1 < z.im := hz1.2.1\n have h2 : z.im \u2264 -M := hz2.2.2\n linarith [hM1']\n have hbridge : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 (Zeta23.Ncount (M - 1) b : \u211d) + (Zeta23.Ncount (-b - 1) (-M) : \u211d) := by\n have hsum_img : \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n = \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d) :=\n (Finset.sum_image (fun x _ y _ h => Subtype.val_injective h)).symm\n rw [hsum_img]\n calc \u2211 z \u2208 FS.image (Subtype.val), (zeroMult z : \u211d)\n \u2264 \u2211 z \u2208 hW1.toFinset \u222a hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg himg (fun z _ _ => Nat.cast_nonneg _)\n _ = \u2211 z \u2208 hW1.toFinset, (zeroMult z : \u211d)\n + \u2211 z \u2208 hW2.toFinset, (zeroMult z : \u211d) :=\n Finset.sum_union hdisj\n _ = (Zeta23.Ncount (M - 1) b : \u211d) + (Zeta23.Ncount (-b - 1) (-M) : \u211d) := by\n rw [Zeta23.Ncount, Zeta23.Ncount, finsum_mem_eq_finite_toFinset_sum _ hW1,\n finsum_mem_eq_finite_toFinset_sum _ hW2, Nat.cast_sum, Nat.cast_sum]\n -- the log comparisons\n have hLpos : (0 : \u211d) < 3 * max |a| |b| + 5 := by\n have h1 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n linarith\n have hLnn : (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 have hL1 : (1 : \u211d) \u2264 Real.log (3 * max |a| |b| + 5) := by\n have h1 : (5 : \u211d) \u2264 3 * max |a| |b| + 5 := by\n have h2 : (0 : \u211d) \u2264 max |a| |b| := le_trans (abs_nonneg a) (le_max_left _ _)\n linarith\n rw [Real.le_log_iff_exp_le hLpos]\n have h2 : Real.exp 1 \u2264 (5 : \u211d) := by\n have h := Real.exp_one_lt_d9.le\n linarith\n linarith [h1, h2]\n have hLog1 : Real.log (3 * max |M - 1| |b| + 5)\n \u2264 Real.log (3 * max |a| |b| + 5) := by\n apply Real.log_le_log (by positivity)\n have h1 : |M - 1| \u2264 max |a| |b| := by\n have h2 : |M - 1| = M - 1 := abs_of_nonneg (by linarith [hM1'])\n rw [h2]\n have h3 : M - 1 \u2264 |b| := by\n have h4 : |b| = b := abs_of_nonneg (by linarith [hb1])\n rw [h4]\n linarith [hMb']\n have h4 : |b| \u2264 max |a| |b| := le_max_right _ _\n linarith [h3, h4]\n have h2 : |b| \u2264 max |a| |b| := le_max_right _ _\n have h3 := max_le h1 h2\n linarith [h3]\n have hLog2 : Real.log (3 * max |-b - 1| |-M| + 5)\n \u2264 Real.log (3 * max |a| |b| + 5) + 1 := by\n have h1 : |-b - 1| = b + 1 := by\n rw [show -b - 1 = -(b + 1) by ring, abs_neg, abs_of_nonneg (by linarith [hb1])]\n have h2 : |-M| = M := abs_neg M\n have h3 : max |-b - 1| |-M| = b + 1 := by\n rw [h1, h2]\n exact max_eq_left (by linarith [hMb'])\n rw [h3]\n have h4 : 3 * (b + 1) + 5 \u2264 2 * (3 * max |a| |b| + 5) := by\n have h5 : |b| = b := abs_of_nonneg (by linarith [hb1])\n have h6 : (b : \u211d) \u2264 max |a| |b| := by\n rw [\u2190 h5]\n exact le_max_right _ _\n linarith [h6]\n have h5 : Real.log (3 * (b + 1) + 5)\n \u2264 Real.log (2 * (3 * max |a| |b| + 5)) :=\n Real.log_le_log (by positivity) h4\n have h6 : Real.log (2 * (3 * max |a| |b| + 5))\n = Real.log 2 + Real.log (3 * max |a| |b| + 5) :=\n Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) (by linarith [hLpos])\n have h7 := log_two_le_one\n linarith [h5, h6, h7]\n -- the two window counts\n have hw1 : (Zeta23.Ncount (M - 1) b : \u211d)\n \u2264 A0count * (b - M + 2) * Real.log (3 * max |a| |b| + 5) := by\n have h1 := Ncount_le_of_interval_gen (a := M - 1) (b := b) (by linarith [hMb'])\n have h2 : b - (M - 1) + 1 = b - M + 2 := by ring\n rw [h2] at h1\n exact h1.trans (mul_le_mul_of_nonneg_left hLog1\n (mul_nonneg A0count_pos.le (by linarith [hMb'])))\n have hw2 : (Zeta23.Ncount (-b - 1) (-M) : \u211d)\n \u2264 A0count * (b - M + 2) * (Real.log (3 * max |a| |b| + 5) + 1) := by\n have h1 := Ncount_le_of_interval_gen (a := -b - 1) (b := -M) (by linarith [hMb'])\n have h2 : -M - (-b - 1) + 1 = b - M + 2 := by ring\n rw [h2] at h1\n exact h1.trans (mul_le_mul_of_nonneg_left hLog2\n (mul_nonneg A0count_pos.le (by linarith [hMb'])))\n have hMa : a \u2264 M := le_max_left _ _\n calc \u2211 \u03c1 \u2208 FS, (zeroMult (\u03c1 : \u2102) : \u211d)\n \u2264 (Zeta23.Ncount (M - 1) b : \u211d) + (Zeta23.Ncount (-b - 1) (-M) : \u211d) := hbridge\n _ \u2264 A0count * (b - M + 2) * Real.log (3 * max |a| |b| + 5)\n + A0count * (b - M + 2) * (Real.log (3 * max |a| |b| + 5) + 1) :=\n add_le_add hw1 hw2\n _ = A0count * (b - M + 2) * (2 * Real.log (3 * max |a| |b| + 5) + 1) := by ring\n _ \u2264 A0count * (b - a + 2) * (3 * Real.log (3 * max |a| |b| + 5)) := by\n apply mul_le_mul\n \u00b7 exact mul_le_mul_of_nonneg_left (by linarith [hMa]) A0count_pos.le\n \u00b7 linarith [hL1, hLnn]\n \u00b7 linarith [hL1, hLnn]\n \u00b7 exact mul_nonneg A0count_pos.le (by linarith [hMa, hMb'])\n _ = 3 * A0count * (b - a + 2) * Real.log (3 * max |a| |b| + 5) := by ring\n\n/-- 9 \u2264 log R for R \u2265 16002 (e\u2079 \u2264 2.72\u2079 \u2264 16002). -/\nlemma nine_le_log_of_16002_le {R : \u211d} (hR : (16002 : \u211d) \u2264 R) :\n (9 : \u211d) \u2264 Real.log R := by\n have he9 : Real.exp 9 \u2264 (16002 : \u211d) := by\n have h1 : Real.exp 9 = (Real.exp 1) ^ 9 := by\n rw [\u2190 Real.exp_nat_mul]; norm_num\n have h2 : Real.exp 1 \u2264 (2.72 : \u211d) := by\n have h := Real.exp_one_lt_d9.le\n linarith\n have h3 : (Real.exp 1) ^ 9 \u2264 (2.72 : \u211d) ^ 9 :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le h2 9\n have h4 : (2.72 : \u211d) ^ 9 \u2264 16002 := by norm_num\n linarith [h1, h3, h4]\n rw [show (9 : \u211d) = Real.log (Real.exp 9) by rw [Real.log_exp]]\n exact Real.log_le_log (Real.exp_pos _) (he9.trans hR)\n\n/-- **The tail application**: for \u2016s\u2016 = R \u2265 16002, the if-zeroed tail\nover {\u2016\u03c1\u2016 \u2265 2R+1} is \u2264 91\u00b7A\u2080\u00b7log R (per-term (17R/6)\u00b7m/(1+\u03b3\u00b2) via\n`seriesTerm_norm_le` + 1/(1+\u2016\u03b3\u2016\u00b2) \u2264 1/(1+im\u00b2), then\n`zero_tail_inv_sq_le` at X = 2R\u22121 \u2265 200). -/\nlemma series_tail_le {s : \u2102} {R : \u211d} (hs : \u2016s\u2016 = R) (hR : (16002 : \u211d) \u2264 R) :\n \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016)\n \u2264 91 * A0count * Real.log R := by\n have hRpos : (0 : \u211d) < R := by linarith [hR]\n have hX : (200 : \u211d) \u2264 2 * R - 1 := by linarith [hR]\n have hlogR : (9 : \u211d) \u2264 Real.log R := nine_le_log_of_16002_le hR\n have hpoint : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016)\n \u2264 (17 * R / 6) * tailTerm (2 * R - 1) \u03c1 := by\n intro \u03c1\n by_cases hmem : \u03c1 \u2208 circleZeros R\n \u00b7 rw [if_pos hmem]\n exact mul_nonneg (by positivity) (tailTerm_nonneg \u03c1)\n \u00b7 rw [if_neg hmem]\n have hnorm : (2 * R + 1 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := by\n have h := not_lt.mp (mt mem_circleZeros.mpr hmem)\n linarith\n have h\u03c12 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016 := by linarith [hR, hnorm]\n have hs\u03c1 : 2 * \u2016s\u2016 \u2264 \u2016(\u03c1 : \u2102)\u2016 := by rw [hs]; linarith [hnorm]\n have h1 := seriesTerm_norm_le \u03c1 h\u03c12 hs\u03c1\n rw [hs] at h1\n -- m/(1+\u2016\u03b3\u2016\u00b2) \u2264 m/(1+im\u00b2) = tailTerm (|im| \u2265 \u2016\u03c1\u2016\u22121 \u2265 2R > 2R\u22121)\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 : \u211d) + (\u03c1 : \u2102).im ^ 2\n \u2264 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n rw [hgam]\n have h2 : (0 : \u211d) \u2264 (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := sq_nonneg _\n linarith\n have hpos1 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n linarith\n have hpos2 : (0 : \u211d) < 1 + (\u03c1 : \u2102).im ^ 2 := by positivity\n have hfrac : 1 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n \u2264 1 / (1 + (\u03c1 : \u2102).im ^ 2) :=\n one_div_le_one_div_of_le hpos2 hcmp\n have hm : (0 : \u211d) \u2264 (zeroMult \u03c1 : \u211d) := Nat.cast_nonneg _\n have h2 : (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n \u2264 (zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2) := by\n rw [show (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n = (zeroMult \u03c1 : \u211d) * (1 / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) from by ring]\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 exact mul_le_mul_of_nonneg_left hfrac hm\n have him : (2 : \u211d) * R - 1 < |(\u03c1 : \u2102).im| := by\n have h3 := abs_im_ge_norm_sub_one \u03c1\n linarith [hnorm, hR]\n rw [tailTerm, if_pos him]\n calc \u2016seriesTerm s \u03c1\u2016\n \u2264 17 / 6 * R * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))) := h1\n _ \u2264 17 / 6 * R * ((zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)) :=\n mul_le_mul_of_nonneg_left h2 (by positivity)\n _ = 17 * R / 6 * ((zeroMult \u03c1 : \u211d) / (1 + (\u03c1 : \u2102).im ^ 2)) := by ring\n have hsumL : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016) := by\n apply Summable.of_norm_bounded (seriesSummable s).norm\n intro \u03c1\n by_cases h : \u03c1 \u2208 circleZeros R <;> simp [h]\n have hsumR : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n (17 * R / 6) * tailTerm (2 * R - 1) \u03c1) :=\n (tailTerm_summable (2 * R - 1)).mul_left _\n have htsum := Summable.tsum_le_tsum hpoint hsumL hsumR\n rw [tsum_mul_left] at htsum\n have htail := zero_tail_inv_sq_le hX\n have hlog2R : Real.log (2 * R - 1) \u2264 2 * Real.log R := by\n have h1 : Real.log (2 * R - 1) \u2264 Real.log (2 * R) := by\n apply Real.log_le_log (by linarith [hRpos])\n linarith\n have h2 : Real.log (2 * R) = Real.log 2 + Real.log R :=\n Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) (by linarith [hRpos] : R \u2260 0)\n have h3 := log_two_le_one\n linarith [h1, h2, h3, hlogR]\n have hR21 : R / (2 * R - 1) \u2264 1 := by\n rw [div_le_one (by linarith [hRpos] : (0 : \u211d) < 2 * R - 1)]\n linarith [hRpos]\n have hA0 := A0count_pos.le\n have hlogRnn : (0 : \u211d) \u2264 Real.log R := by linarith [hlogR]\n have hbound : 17 * R / 6 * (16 * A0count * Real.log (2 * R - 1) / (2 * R - 1))\n \u2264 91 * A0count * Real.log R := by\n have h1 : 17 * R / 6 * (16 * A0count * Real.log (2 * R - 1) / (2 * R - 1))\n = (17 / 6) * 16 * A0count * (R / (2 * R - 1)) * Real.log (2 * R - 1) := by\n field_simp\n ring\n rw [h1]\n have h2 : (17 / 6 : \u211d) * 16 * A0count * (R / (2 * R - 1)) * Real.log (2 * R - 1)\n \u2264 (17 / 6) * 16 * A0count * 1 * (2 * Real.log R) := by\n apply mul_le_mul\n \u00b7 apply mul_le_mul_of_nonneg_left _ hA0\n apply mul_le_mul_of_nonneg_left hR21 (by norm_num)\n \u00b7 exact hlog2R\n \u00b7 exact hlogRnn\n \u00b7 exact mul_nonneg (mul_nonneg (by norm_num : (0 : \u211d) \u2264 17 / 6 * 16) hA0)\n (by linarith [hR21] : (0 : \u211d) \u2264 R / (2 * R - 1))\n calc (17 / 6 : \u211d) * 16 * A0count * (R / (2 * R - 1)) * Real.log (2 * R - 1)\n \u2264 (17 / 6) * 16 * A0count * 1 * (2 * Real.log R) := h2\n _ = (272 / 3) * A0count * Real.log R := by ring\n _ \u2264 91 * A0count * Real.log R := by\n apply mul_le_mul_of_nonneg_right _ hlogRnn\n apply mul_le_mul_of_nonneg_right _ hA0\n norm_num\n calc \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016)\n \u2264 17 * R / 6 * \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, tailTerm (2 * R - 1) \u03c1 := htsum\n _ \u2264 17 * R / 6 * (16 * A0count * Real.log (2 * R - 1) / (2 * R - 1)) :=\n mul_le_mul_of_nonneg_left htail (by positivity)\n _ \u2264 91 * A0count * Real.log R := hbound\n\n/-- **The one tsum split**: \u2016seriesFun s\u2016 \u2264 the finite part over\n{\u2016\u03c1\u2016 < 2R+1} + the if-zeroed tail. -/\nlemma seriesFun_norm_le_split {s : \u2102} {R : \u211d} :\n \u2016seriesFun s\u2016\n \u2264 \u2211 \u03c1 \u2208 circleZeros R, \u2016seriesTerm s \u03c1\u2016\n + \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016) := by\n have h1 : \u2016seriesFun s\u2016\n \u2264 \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u2016seriesTerm s \u03c1\u2016 :=\n norm_tsum_le_tsum_norm (seriesSummable s).norm\n have h2 := tsum_split_finset (seriesSummable s).norm (circleZeros R)\n calc \u2016seriesFun s\u2016\n \u2264 \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u2016seriesTerm s \u03c1\u2016 := h1\n _ = \u2211 \u03c1 \u2208 circleZeros R, \u2016seriesTerm s \u03c1\u2016\n + \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n (if \u03c1 \u2208 circleZeros R then (0 : \u211d) else \u2016seriesTerm s \u03c1\u2016) := h2\n\nend NguyenRH1\n\nend",
"structuredPatch": [
{
"oldStart": 1244,
"oldLines": 7,
"newStart": 1244,
"newLines": 9,
"lines": [
" \u2264 Real.log (3 * max |a| |b| + 5) + 1 := by",
" have h1 : |-b - 1| = b + 1 := by",
" rw [show -b - 1 = -(b + 1) by ring, abs_neg, abs_of_nonneg (by linarith [hb1])]",
"- have h2 : |-M| = M := abs_neg M",
"+ have h2 : |-M| = M := by",
"+ rw [abs_neg]",
"+ exact abs_of_nonneg (by linarith [hM1'] : (0 : \u211d) \u2264 M)",
" have h3 : max |-b - 1| |-M| = b + 1 := by",
" rw [h1, h2]",
" exact max_eq_left (by linarith [hMb'])"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Another network glitch. State: E-016 fixes applied but not yet rerun. Just rerun it. Also should add the xi_err to checks? I added print but didn't wire xi_err into checks — V2 check exists. Let me wire xi_err into the meta at least... Minor: add to checks dict? Keep simple: it's printed; also add to key_values later? To avoid more edit cycles, just run — actually the check should gate. Quick edit: add \"xi_flint_crosscheck_rel\" to key_values in meta. Let me do that quickly then run.","signature":""},{"type":"text","text":"Same network glitch — no harm done. The fixes are in place; let me wire the flint cross-check into the metadata and rerun."},{"type":"tool_use","id":"Edit_36","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\numerics\\scripts\\E-016-herglotz-fine-structure.py","old_string":" \"key_values\": {\n \"rhoF_finitediff_max_rel\": v2_err,","new_string":" \"key_values\": {\n \"xi_flint_crosscheck_rel\": xi_err,\n \"rhoF_finitediff_max_rel\": v2_err,"},"extra_content":null}]