[{"type":"thinking","thinking":"The file ends at line 2865-2867 with `positivity)` then `end NguyenRH1`/`end`. My failed Edit's old_string had the exact same ending (`(by have h2 := two_le_C0hat ...; positivity)`) — matches ✓. So the old_string WAS present; the error said \"text to replace is not within the read portion\" — because I hadn't READ the file recently (the Edit tool requires a recent read of the exact region). Now I've read 2850-2865. Let me retry the §17 edit, but with the CLEANED-UP version (no sorries, restructured farGLeftMaj section). I'll write the whole §17 in one Edit with the good structure.\n\nPlan the final §17 structure (avoiding the duplication):\n1. farGLeft + nonneg + summable.\n2. farGLeft_term_le.\n3. farGLeft_fiber_finite.\n4. farGLeft_fiber_count.\n5. farGLeft_fiber_le (ENNReal per-fiber).\n6. tail14_inv_add_sq_summable + tail14_loglog_div_add_sq_summable (standalone).\n7. farGLeftMaj + farGLeftMaj_shift_le + farGLeftMaj_shift_summable + farGLeftMaj_series_le.\n8. farGLeft_le (the outer ENNReal assembly: ofReal_tsum + tsum_fiberwise + per-fiber ≤ + series bound).\n\nFor #8, the outer assembly (cloning zero_tail_inv_sq_le's ending):\n```\nlemma farGLeft_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) :\n    ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGLeft t ρ\n      ≤ 4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n          + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23)) := by\n  have hC0 : (0 : ℝ) ≤ 4.5 * (...) := by\n    positivity? — needs two_le_C0hat? no — the combo is a number ✓ norm_num: 0.433·(0.1942/23+0.1687) = 0.433·0.17713 = 0.07669; 0.886·(0.0736/23+0.0621) = 0.886·0.06530 = 0.05786; 2.9/23 = 0.12609: sum 0.26064·4.5 = 1.17288 ≥ 0 ✓ norm_num.\n  rw [← ENNReal.ofReal_le_ofReal_iff hC0]\n  rw [ENNReal.ofReal_tsum_of_nonneg (fun ρ => farGLeft_nonneg t ρ) (farGLeft_summable (by linarith : (0:ℝ) ≤ t))]\n  rw [← ENNReal.tsum_fiberwise (fun ρ => ENNReal.ofReal (farGLeft t ρ))\n    (fun ρ => Nat.floor |ρ.1.im|)]\n  -- ∑' j, ∑' b : fiber j, ... ≤ ∑' j, ofReal (farGLeftMaj j)\n  have hper : ∀ ℓ : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ},\n      ENNReal.ofReal (farGLeft t b.1)\n      ≤ ENNReal.ofReal (farGLeftMaj ℓ) :=\n    fun ℓ => farGLeft_fiber_le hZC hNLZ ht ℓ\n  have hle1 : ∑' j : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {j},\n      ENNReal.ofReal (farGLeft t b.1)\n      ≤ ∑' j : ℕ, ENNReal.ofReal (farGLeftMaj j) :=\n    ENNReal.tsum_le_tsum hper\n  have heq : ∑' j : ℕ, ENNReal.ofReal (farGLeftMaj j)\n      = ENNReal.ofReal (∑' j : ℕ, farGLeftMaj j) := by\n    rw [ENNReal.ofReal_tsum_of_nonneg (fun ℓ => farGLeftMaj_nonneg ℓ) farGLeftMaj_summable]\n  calc ENNReal.ofReal (∑' ρ, farGLeft t ρ)\n      = ∑' ρ, ENNReal.ofReal (farGLeft t ρ) := by\n        rw [ENNReal.ofReal_tsum_of_nonneg (fun ρ => farGLeft_nonneg t ρ) (farGLeft_summable ...)]\n    ...\n```\nHmm — the structure: the GOAL after rw [← ofReal_le_ofReal_iff hC0] is ofReal(tsum) ≤ ofReal(bound). Then:\n```\n  rw [ENNReal.ofReal_tsum_of_nonneg (nonneg) (summable)] -- ofReal(tsum) = ∑' ofReal-terms\n  rw [← ENNReal.tsum_fiberwise ...] -- ∑' ofReal-terms = ∑' j, ∑' fiber j\n  calc ∑' j, ∑' b : fiber j, ofReal (farGLeft t b.1)\n      ≤ ∑' j, ENNReal.ofReal (farGLeftMaj j) := ENNReal.tsum_le_tsum hper\n    _ = ENNReal.ofReal (∑' j, farGLeftMaj j) := by\n        rw [ENNReal.ofReal_tsum_of_nonneg farGLeftMaj_nonneg farGLeftMaj_summable]\n    _ ≤ ENNReal.ofReal (bound) :=\n        ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n```\nThe hper conclusion ≤ ofReal (farGLeftMaj ℓ) — farGLeft_fiber_le's conclusion has the if-form — and farGLeftMaj ℓ = the if-form by def ✓ rw [farGLeftMaj]? — farGLeft_fiber_le's RHS is `ENNReal.ofReal (if 14 ≤ ℓ then 4.5·C0hat((ℓ:ℝ)+1)/(10+(ℓ:ℝ))² else 0)` and farGLeftMaj ℓ unfolds to exactly that ✓ — make hper: (farGLeft_fiber_le hZC hNLZ ht ℓ).trans_eq? — no: farGLeftMaj ℓ is DEFEQUAL to the if-form: `farGLeftMaj` unfolds by rfl — the ≤ with ofReal (farGLeftMaj ℓ): `show ... ≤ ENNReal.ofReal (farGLeftMaj ℓ); rw [farGLeftMaj]; exact farGLeft_fiber_le hZC hNLZ ht ℓ` — or just: have hper := fun ℓ => farGLeft_fiber_le hZC hNLZ ht ℓ — its TYPE is ≤ ofReal(if-form) and farGLeftMaj ℓ is defeq — when used in ENNReal.tsum_le_tsum hper against the farGLeftMaj-family, the unification is up to defeq ✓ should work directly. If not, add `simp only [farGLeftMaj] at hper`.\n\nAlso need farGLeftMaj_nonneg + farGLeftMaj_summable (the FULL summable, from the shift + summable_nat_add_iff).\n\nLet me also double check `ENNReal.tsum_fiberwise` signature: from zero_tail_inv_sq_le: `rw [← ENNReal.tsum_fiberwise (fun ρ => ENNReal.ofReal (tailTerm X ρ)) (dyadClass X)]` ✓ — ENNReal.tsum_fiberwise (f : α → ℝ≥0∞) (g : α → β) : ∑' a, f a = ∑' b, ∑' a : g ⁻¹' {b}, f a — the ← direction turns the fiberwise double-sum into the plain tsum ✓.\n\nAnd `ENNReal.ofReal_tsum_of_nonneg (hf : ∀ i, 0 ≤ f i) (hsum : Summable f) : ENNReal.ofReal (∑' i, f i) = ∑' i, ENNReal.ofReal (f i)` ✓ used in zero_tail_inv_sq_le ✓.\n\nNow write the full §17. It's long (~700 lines). Let me assemble the complete text carefully, incorporating all the fixes I identified:\n- farGLeft_term_le's hxfar linarith [h1, ht, hγ]: h1 : t − ρ.1.im < 1 — wait: mem_nearZerosSub gives |γ−t| < 1: after h2 : |γ−t| = t−γ: t−γ < 1: with γ < 0: t−γ > t ≥ 10 > 1 contradiction ✓ linarith ✓.\n- farGLeft_fiber_le's hzero filter predicate: (fun ρ => ¬ ρ.1.im < 0) ✓.\n- The calc's first step h1 usage: `rw [hmem] at h1` — hmem : ⌊|ρ.1.im|⌋₊ = ℓ: farGLeft_term_le's conclusion has ⌊|ρ.1.im|⌋₊ — rw [hmem] at h1 : .../(10 + (ℓ:ℝ))² ✓ — hmm — hmem is about Nat.floor |ρ.1.im| — the term in h1 is (Nat.floor |ρ.1.im| : ℝ) — rw [hmem] rewrites Nat.floor |ρ.1.im| → ℓ ✓ then the cast (↑ℓ) ✓.\n- In farGLeft_fiber_le the show-rw: `rw [show (4.5:ℝ)/(10+(ℓ:ℝ))² * m = 4.5*m/(10+(ℓ:ℝ))² from by ring]` — matches h1's form after the rw [hmem] ✓.\n\nFor farGLeftMaj_series_le's combo-summable and the eval — write them ONCE as standalone haves at the lemma top.\n\nLet me write it all now.","signature":""},{"type":"text","text":"Now writing the complete §17 (left-tail machine) in one clean pass."},{"type":"tool_use","id":"Edit_183","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"    _ ≤ (4.5 * (2 * C0hat (t + 1) + 0.55)) * 1.3476 :=\n        mul_le_mul_of_nonneg_left (farW_Ico_le _)\n          (by\n            have h2 := two_le_C0hat (by linarith [ht] : (1 : ℝ) ≤ t + 1)\n            positivity)\n\nend NguyenRH1\n\nend","new_string":"    _ ≤ (4.5 * (2 * C0hat (t + 1) + 0.55)) * 1.3476 :=\n        mul_le_mul_of_nonneg_left (farW_Ico_le _)\n          (by\n            have h2 := two_le_C0hat (by linarith [ht] : (1 : ℝ) ≤ t + 1)\n            positivity)\n\n/-! ## 17. Piece 3i: the left-tail machine (γ < 0) -/\n\n/-- The left-tail summand (farG restricted to γ < 0). -/\ndef farGLeft (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if ρ.1.im < 0 then farG t ρ else 0\n\nlemma farGLeft_nonneg (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : (0 : ℝ) ≤ farGLeft t ρ := by\n  by_cases h : ρ.1.im < 0\n  · rw [farGLeft, if_pos h]\n    exact farG_nonneg t ρ\n  · rw [farGLeft, if_neg h]\n\nlemma farGLeft_summable {t : ℝ} (ht : 0 ≤ t) : Summable (farGLeft t) := by\n  apply Summable.of_norm_bounded (farG_summable ht)\n  intro ρ\n  rw [Real.norm_eq_abs, abs_of_nonneg (farGLeft_nonneg t ρ)]\n  by_cases h : ρ.1.im < 0\n  · rw [farGLeft, if_pos h]\n  · rw [farGLeft, if_neg h]\n    exact farG_nonneg t ρ\n\n/-- The per-element left-tail bound: farGLeft ≤ 4.5·m/(10+⌊|γ|⌋₊)². -/\nlemma farGLeft_term_le {t : ℝ} (ht : 10 ≤ t) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    farGLeft t ρ ≤ 4.5 * (zeroMult ρ.1 : ℝ) / (10 + (Nat.floor |ρ.1.im| : ℝ)) ^ 2 := by\n  classical\n  by_cases hγ : ρ.1.im < 0\n  · rw [farGLeft, if_pos hγ]\n    have hxfar : ρ ∉ nearZerosSub t := by\n      intro hmem\n      have h1 := mem_nearZerosSub.mp hmem\n      have h2 : |ρ.1.im - t| = t - ρ.1.im := by\n        rw [abs_of_neg (by linarith [hγ] : ρ.1.im - t < 0)]\n        ring\n      rw [h2] at h1\n      linarith [h1, ht, hγ]\n    rw [farG, if_neg hxfar]\n    have hx : |ρ.1.im - t| = t + |ρ.1.im| := by\n      rw [abs_of_neg (by linarith [hγ] : ρ.1.im - t < 0)]\n      have h3 : |ρ.1.im| = -ρ.1.im := abs_of_neg hγ\n      rw [h3]\n      ring\n    have hℓ : (Nat.floor |ρ.1.im| : ℝ) ≤ |ρ.1.im| := Nat.floor_le (abs_nonneg _)\n    have hx1 : (10 : ℝ) + (Nat.floor |ρ.1.im| : ℝ) ≤ |ρ.1.im - t| := by\n      rw [hx]\n      linarith [hℓ, ht]\n    have hmono : ((10 : ℝ) + (Nat.floor |ρ.1.im| : ℝ)) ^ 2\n        ≤ |ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n      have h2 : ((10 : ℝ) + (Nat.floor |ρ.1.im| : ℝ)) ^ 2 ≤ |ρ.1.im - t| ^ 2 := by\n        have h3 : (0 : ℝ) ≤ (10 : ℝ) + (Nat.floor |ρ.1.im| : ℝ) := by positivity\n        exact pow_le_pow_left₀ h3 hx1 2\n      have h4 : |ρ.1.im - t| ^ 2 ≤ |ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n        have h5 : |ρ.1.im - t| ≤ Real.sqrt (1 + (ρ.1.im - t) ^ 2) := by\n          calc |ρ.1.im - t| = Real.sqrt ((ρ.1.im - t) ^ 2) := by rw [Real.sqrt_sq_eq_abs]\n            _ ≤ Real.sqrt (1 + (ρ.1.im - t) ^ 2) :=\n              Real.sqrt_le_sqrt (by linarith [sq_nonneg (ρ.1.im - t)])\n        have h6 : (0 : ℝ) ≤ |ρ.1.im - t| := abs_nonneg _\n        calc |ρ.1.im - t| ^ 2 = |ρ.1.im - t| * |ρ.1.im - t| := by ring\n          _ ≤ |ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2) :=\n            mul_le_mul_of_nonneg_left h5 h6\n      exact h2.trans h4\n    have hm : (0 : ℝ) ≤ (zeroMult ρ.1 : ℝ) := Nat.cast_nonneg _\n    have hpos : (0 : ℝ) < ((10 : ℝ) + (Nat.floor |ρ.1.im| : ℝ)) ^ 2 := by positivity\n    rw [show (4.5 : ℝ) * (zeroMult ρ.1 : ℝ) / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))\n        = (4.5 * (zeroMult ρ.1 : ℝ)) * (1 / (|ρ.1.im - t| * Real.sqrt (1 + (ρ.1.im - t) ^ 2))) from by\n          rw [div_eq_mul_inv, one_div]]\n    rw [show (4.5 : ℝ) * (zeroMult ρ.1 : ℝ) / (10 + (Nat.floor |ρ.1.im| : ℝ)) ^ 2\n        = (4.5 * (zeroMult ρ.1 : ℝ)) * (1 / ((10 + (Nat.floor |ρ.1.im| : ℝ)) ^ 2)) from by\n          rw [div_eq_mul_inv, one_div]]\n    apply mul_le_mul_of_nonneg_left _ (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4.5) hm)\n    exact one_div_le_one_div_of_le hpos hmono\n  · rw [farGLeft, if_neg hγ]\n    positivity\n\n/-- The left-tail fiber {⌊|γ|⌋₊ = ℓ} is finite. -/\nlemma farGLeft_fiber_finite (ℓ : ℕ) :\n    ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ} :\n      Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := by\n  apply (finite_subtype_norm_lt ((ℓ : ℝ) + 2)).subset\n  intro ρ hρ\n  show ‖ρ.1‖ < (ℓ : ℝ) + 2\n  have hmem : Nat.floor |ρ.1.im| = ℓ := hρ\n  have h1 : |ρ.1.im| < (ℓ : ℝ) + 1 := by\n    have h2 := Nat.lt_floor_add_one |ρ.1.im|\n    rwa [hmem] at h2\n  have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n  have hre : |ρ.1.re| ≤ 1 := by\n    have h3 : 0 < ρ.1.re := ρ.2.2.1\n    have h4 : ρ.1.re < 1 := ρ.2.2.2\n    rw [abs_le]\n    constructor <;> linarith\n  linarith [hle, hre, h1]\n\n/-- The per-fiber left-tail count (via conj + zeroWindow + zeroMult_conj). -/\nlemma farGLeft_fiber_count (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)\n    (ℓ : ℕ) (hℓ : 14 ≤ ℓ) :\n    ∑ ρ ∈ (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      ρ.1.im < 0), (zeroMult ρ.1 : ℝ)\n      ≤ C0hat ((ℓ : ℝ) + 1) := by\n  classical\n  set FS := (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n    ρ.1.im < 0) with hFS\n  have hsub : FS.image (fun ρ => (starRingEnd ℂ) ρ.1)\n      ⊆ (zeroWindow_finite (ℓ : ℝ)).toFinset := by\n    intro z hz\n    obtain ⟨ρ, hρ, rfl⟩ := Finset.mem_image.mp hz\n    rw [hFS, Finset.mem_filter] at hρ\n    obtain ⟨hmem, hγ⟩ := hρ\n    rw [Set.Finite.mem_toFinset] at hmem\n    have hγ2 : ((starRingEnd ℂ) ρ.1).im = -ρ.1.im := by simp\n    have hneg : |ρ.1.im| = -ρ.1.im := abs_of_neg hγ\n    have hℓ1 : (ℓ : ℝ) ≤ |ρ.1.im| := by\n      have h1 := Nat.floor_le (abs_nonneg ρ.1.im)\n      rwa [hmem] at h1\n    have hℓ2 : |ρ.1.im| < (ℓ : ℝ) + 1 := by\n      have h1 := Nat.lt_floor_add_one |ρ.1.im|\n      rwa [hmem] at h1\n    rw [Set.Finite.mem_toFinset]\n    refine ⟨isNontrivialZero_conj ρ.2, ?_, ?_⟩\n    · rw [hγ2]\n      linarith [hℓ1, hneg]\n    · rw [hγ2]\n      linarith [hℓ2, hneg]\n  have h1 : ∑ z ∈ FS.image (fun ρ => (starRingEnd ℂ) ρ.1), (zeroMult z : ℝ)\n      = ∑ ρ ∈ FS, (zeroMult ((starRingEnd ℂ) ρ.1) : ℝ) :=\n    Finset.sum_image (fun x _ y _ h => Subtype.ext ((starRingEnd ℂ).injective h))\n  have h2 : ∑ ρ ∈ FS, (zeroMult ((starRingEnd ℂ) ρ.1) : ℝ)\n      = ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ) :=\n    Finset.sum_congr rfl (fun ρ _ => by rw [zeroMult_conj ρ.2])\n  calc ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n      = ∑ z ∈ FS.image (fun ρ => (starRingEnd ℂ) ρ.1), (zeroMult z : ℝ) := by\n        rw [h1, h2]\n    _ ≤ ∑ z ∈ (zeroWindow_finite (ℓ : ℝ)).toFinset, (zeroMult z : ℝ) :=\n        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun z _ _ => Nat.cast_nonneg _)\n    _ = (((zeroWindow_finite (ℓ : ℝ)).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := rfl\n    _ ≤ C0hat ((ℓ : ℝ) + 1) := hZC (ℓ : ℝ) (by exact_mod_cast (by omega : 2 ≤ ℓ))\n\n/-- The per-fiber left-tail bound (ENNReal form). -/\nlemma farGLeft_fiber_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) (ℓ : ℕ) :\n    ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ},\n      ENNReal.ofReal (farGLeft t b.1)\n      ≤ ENNReal.ofReal (if 14 ≤ ℓ then 4.5 * C0hat ((ℓ : ℝ) + 1) / (10 + (ℓ : ℝ)) ^ 2 else 0) := by\n  classical\n  have hfin : ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ} :\n      Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := farGLeft_fiber_finite ℓ\n  have htsum : ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ},\n      ENNReal.ofReal (farGLeft t b.1)\n      = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n        ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ}).indicator\n          (fun ρ => ENNReal.ofReal (farGLeft t ρ)) ρ :=\n    tsum_subtype _ (fun ρ => ENNReal.ofReal (farGLeft t ρ))\n  rw [htsum]\n  rw [tsum_eq_sum (s := hfin.toFinset) (fun ρ hρ => by\n    apply Set.indicator_of_notMem\n    rwa [Set.Finite.mem_toFinset] at hρ)]\n  rw [Finset.sum_congr rfl (fun ρ hρ =>\n    Set.indicator_of_mem (by rwa [Set.Finite.mem_toFinset] at hρ) _)]\n  rw [← ENNReal.ofReal_sum_of_nonneg (fun ρ _ => farGLeft_nonneg t ρ)]\n  apply ENNReal.ofReal_le_ofReal\n  by_cases hℓ : 14 ≤ ℓ\n  · rw [if_pos hℓ]\n    rw [← Finset.sum_filter_add_sum_filter_not hfin.toFinset\n      (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ρ.1.im < 0) (farGLeft t)]\n    have hzero : ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n        ¬ ρ.1.im < 0), farGLeft t ρ = 0 := by\n      apply Finset.sum_eq_zero\n      intro ρ hρ\n      rw [Finset.mem_filter] at hρ\n      rw [farGLeft, if_neg hρ.2]\n    rw [hzero, add_zero]\n    calc ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ρ.1.im < 0),\n        farGLeft t ρ\n        ≤ ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ρ.1.im < 0),\n          (4.5 / (10 + (ℓ : ℝ)) ^ 2) * (zeroMult ρ.1 : ℝ) := by\n          apply Finset.sum_le_sum\n          intro ρ hρ\n          have h1 := farGLeft_term_le ht ρ\n          rw [Finset.mem_filter] at hρ\n          obtain ⟨hmem, _⟩ := hρ\n          rw [Set.Finite.mem_toFinset] at hmem\n          rw [hmem] at h1\n          rw [show (4.5 : ℝ) / (10 + (ℓ : ℝ)) ^ 2 * (zeroMult ρ.1 : ℝ)\n              = 4.5 * (zeroMult ρ.1 : ℝ) / (10 + (ℓ : ℝ)) ^ 2 from by ring]\n          exact h1\n      _ = (4.5 / (10 + (ℓ : ℝ)) ^ 2) *\n          ∑ ρ ∈ hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ρ.1.im < 0),\n            (zeroMult ρ.1 : ℝ) := by\n          rw [Finset.mul_sum]\n      _ ≤ (4.5 / (10 + (ℓ : ℝ)) ^ 2) * C0hat ((ℓ : ℝ) + 1) :=\n          mul_le_mul_of_nonneg_left (farGLeft_fiber_count hZC hNLZ ht ℓ hℓ)\n            (by positivity)\n      _ = 4.5 * C0hat ((ℓ : ℝ) + 1) / (10 + (ℓ : ℝ)) ^ 2 := by ring\n  · rw [if_neg hℓ]\n    apply Finset.sum_eq_zero\n    intro ρ hρ\n    rw [Set.Finite.mem_toFinset] at hρ\n    by_cases hγ : ρ.1.im < 0\n    · have h1 : 14 ≤ |ρ.1.im| := hNLZ ρ.1 ρ.2\n      have h2 : 14 ≤ Nat.floor |ρ.1.im| := by\n        have h3 := Nat.floor_mono h1\n        rw [Nat.floor_ofNat] at h3\n        exact h3\n      rw [h2] at hρ\n      omega\n    · rw [farGLeft, if_neg hγ]\n\n/-- The shifted LA₀-family is summable. -/\nlemma tail14_inv_add_sq_summable :\n    Summable (fun j : ℕ => (1 : ℝ) / (((j : ℝ) + 14) + 10) ^ 2) := by\n  have h := antitoneOn_one_div_add_sq.summable_of_integrableOn_Ioi\n    integrableOn_one_div_add_sq (fun t ht => by\n      have ht13 : (13 : ℝ) < t := ht\n      positivity)\n  have h2 := (summable_nat_add_iff (f := fun n : ℕ => (1 : ℝ) / ((n : ℝ) + 10) ^ 2) 14).mpr h\n  refine h2.congr fun n => ?_\n  push_cast\n  ring_nf\n\n/-- The shifted LA₂-family is summable. -/\nlemma tail14_loglog_div_add_sq_summable :\n    Summable (fun j : ℕ =>\n      Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2) := by\n  apply Summable.of_norm_bounded (tail14_log_div_add_sq_summable.mul_left (1 / Real.exp 1))\n  intro j\n  rw [Real.norm_eq_abs]\n  rw [abs_of_nonneg (by\n    have hj1 : (1 : ℝ) ≤ Real.log ((j : ℝ) + 14) := by\n      have h1 := log_fourteen_ge\n      have h2 : Real.log 14 ≤ Real.log ((j : ℝ) + 14) :=\n        Real.log_le_log (by norm_num : (0 : ℝ) < 14) (by\n          have h : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n          linarith)\n      linarith [h1, h2]\n    have h3 : (0 : ℝ) ≤ Real.log (Real.log ((j : ℝ) + 14)) := Real.log_nonneg hj1\n    positivity : (0 : ℝ) ≤ Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2)]\n  have hj1 : (1 : ℝ) < (j : ℝ) + 14 := by\n    have h : (0 : ℝ) ≤ (j : ℝ) := Nat.cast_nonneg j\n    linarith\n  have h4 := log_log_le_div_exp hj1\n  have h5 : (0 : ℝ) ≤ (((j : ℝ) + 14) + 10) ^ 2 := by positivity\n  have h6 := div_le_div_of_nonneg_right h4 h5\n  rw [mul_div_assoc] at h6\n  exact h6\n\n/-- The left-tail majorant series (if-form on ℕ). -/\ndef farGLeftMaj : ℕ → ℝ := fun ℓ =>\n  if 14 ≤ ℓ then 4.5 * C0hat ((ℓ : ℝ) + 1) / (10 + (ℓ : ℝ)) ^ 2 else 0\n\nlemma farGLeftMaj_nonneg (ℓ : ℕ) : (0 : ℝ) ≤ farGLeftMaj ℓ := by\n  by_cases h : 14 ≤ ℓ\n  · rw [farGLeftMaj, if_pos h]\n    have h1 : (1 : ℝ) ≤ (ℓ : ℝ) + 1 := by\n      have h2 : (0 : ℝ) ≤ (ℓ : ℝ) := Nat.cast_nonneg ℓ\n      linarith\n    have h3 := two_le_C0hat h1\n    positivity\n  · rw [farGLeftMaj, if_neg h]\n\n/-- The pointwise majorant bound for the shifted farGLeftMaj. -/\nlemma farGLeftMaj_shift_le (ℓ : ℕ) :\n    farGLeftMaj (ℓ + 14)\n      ≤ 4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / (((ℓ : ℝ) + 14) + 10) ^ 2)\n          + (0.433 * Real.log ((ℓ : ℝ) + 14) / (((ℓ : ℝ) + 14) + 10) ^ 2)\n          + (0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) / (((ℓ : ℝ) + 14) + 10) ^ 2)) := by\n  have hℓ : 14 ≤ ℓ + 14 := by omega\n  rw [farGLeftMaj, if_pos hℓ]\n  have h1 := C0hat_add_one_le_of_fourteen_le (j := ℓ + 14) (by omega : 14 ≤ ℓ + 14)\n  have hcast : ((ℓ + 14 : ℕ) : ℝ) = (ℓ : ℝ) + 14 := by push_cast; ring\n  have h9 : (0.433 * (Real.log ((ℓ : ℝ) + 14) + 0.1942)\n      + 0.886 * (Real.log (Real.log ((ℓ : ℝ) + 14)) + 0.0736) + 2.9)\n      = (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9)\n        + 0.433 * Real.log ((ℓ : ℝ) + 14) + 0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) := by ring\n  calc 4.5 * C0hat ((ℓ + 14 : ℝ) + 1) / (10 + ((ℓ + 14 : ℕ) : ℝ)) ^ 2\n      ≤ 4.5 * (0.433 * (Real.log ((ℓ : ℝ) + 14) + 0.1942)\n          + 0.886 * (Real.log (Real.log ((ℓ : ℝ) + 14)) + 0.0736) + 2.9)\n        / (10 + ((ℓ + 14 : ℕ) : ℝ)) ^ 2 := by\n          apply div_le_div_of_nonneg_left (by norm_num : (0 : ℝ) ≤ 4.5) (by positivity) _\n          rw [show ((ℓ + 14 : ℝ) + 1) = (((ℓ + 14 : ℕ) : ℝ) + 1) from by push_cast; ring]\n          exact h1\n    _ = 4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / (((ℓ : ℝ) + 14) + 10) ^ 2)\n        + (0.433 * Real.log ((ℓ : ℝ) + 14) / (((ℓ : ℝ) + 14) + 10) ^ 2)\n        + (0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) / (((ℓ : ℝ) + 14) + 10) ^ 2)) := by\n          rw [hcast, h9]\n          field_simp\n          ring\n\n/-- The combo majorant is summable. -/\nlemma farGLeftMaj_combo_summable : Summable (fun ℓ : ℕ =>\n    4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / (((ℓ : ℝ) + 14) + 10) ^ 2)\n        + (0.433 * Real.log ((ℓ : ℝ) + 14) / (((ℓ : ℝ) + 14) + 10) ^ 2)\n        + (0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) / (((ℓ : ℝ) + 14) + 10) ^ 2))) := by\n  exact (((tail14_inv_add_sq_summable.mul_left _).add\n    (tail14_log_div_add_sq_summable.mul_left _)).add\n    (tail14_loglog_div_add_sq_summable.mul_left _)).mul_left _\n\nlemma farGLeftMaj_shift_summable : Summable (fun ℓ : ℕ => farGLeftMaj (ℓ + 14)) := by\n  apply Summable.of_norm_bounded farGLeftMaj_combo_summable\n  intro ℓ\n  rw [Real.norm_eq_abs, abs_of_nonneg (farGLeftMaj_nonneg _)]\n  exact farGLeftMaj_shift_le ℓ\n\nlemma farGLeftMaj_summable : Summable farGLeftMaj :=\n  (summable_nat_add_iff (f := farGLeftMaj) 14).mp farGLeftMaj_shift_summable\n\n/-- **The left-tail series bound**. -/\nlemma farGLeftMaj_series_le :\n    (∑' ℓ : ℕ, farGLeftMaj ℓ)\n      ≤ 4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n          + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23)) := by\n  have hsplit : (∑' ℓ : ℕ, farGLeftMaj ℓ)\n      = (∑ ℓ ∈ Finset.range 14, farGLeftMaj ℓ) + ∑' ℓ : ℕ, farGLeftMaj (ℓ + 14) :=\n    (farGLeftMaj_summable.sum_add_tsum_nat_add 14).symm\n  have hzero : ∑ ℓ ∈ Finset.range 14, farGLeftMaj ℓ = 0 := by\n    apply Finset.sum_eq_zero\n    intro ℓ hℓ\n    rw [Finset.mem_range] at hℓ\n    rw [farGLeftMaj, if_neg (by omega : ¬14 ≤ ℓ)]\n  have hle := Summable.tsum_le_tsum farGLeftMaj_shift_le farGLeftMaj_shift_summable\n    farGLeftMaj_combo_summable\n  have hA0 := tail14_inv_add_sq_le\n  have hA1 := tail14_log_div_add_sq_le\n  have hA2 := tail14_loglog_div_add_sq_le\n  have heval : (∑' ℓ : ℕ,\n      4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / (((ℓ : ℝ) + 14) + 10) ^ 2)\n          + (0.433 * Real.log ((ℓ : ℝ) + 14) / (((ℓ : ℝ) + 14) + 10) ^ 2)\n          + (0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) / (((ℓ : ℝ) + 14) + 10) ^ 2)))\n      ≤ 4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23)\n          + 0.433 * 0.1687 + 0.886 * 0.0621) := by\n    rw [tsum_mul_left]\n    apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 4.5)\n    rw [Summable.tsum_add ((tail14_inv_add_sq_summable.mul_left _).add\n      (tail14_log_div_add_sq_summable.mul_left _)) (tail14_loglog_div_add_sq_summable.mul_left _)]\n    rw [Summable.tsum_add (tail14_inv_add_sq_summable.mul_left _)\n      (tail14_log_div_add_sq_summable.mul_left _)]\n    rw [tsum_mul_left, tsum_mul_left, tsum_mul_left]\n    have hle1 := mul_le_mul_of_nonneg_left hA0 (by positivity : (0 : ℝ) ≤\n      0.433 * 0.1942 + 0.886 * 0.0736 + 2.9)\n    have hle2 := mul_le_mul_of_nonneg_left hA1 (by positivity : (0 : ℝ) ≤ 0.433)\n    have hle3 := mul_le_mul_of_nonneg_left hA2 (by positivity : (0 : ℝ) ≤ 0.886)\n    linarith [hle1, hle2, hle3]\n  calc (∑' ℓ : ℕ, farGLeftMaj ℓ)\n      = (∑ ℓ ∈ Finset.range 14, farGLeftMaj ℓ) + ∑' ℓ : ℕ, farGLeftMaj (ℓ + 14) := hsplit\n    _ = 0 + ∑' ℓ : ℕ, farGLeftMaj (ℓ + 14) := by rw [hzero]\n    _ ≤ 4.5 * ((0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23)\n        + 0.433 * 0.1687 + 0.886 * 0.0621) := by linarith [hle, heval]\n    _ = 4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n        + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23)) := by ring\n\n/-- **The left-tail bound** (the ENNReal fiberwise assembly). -/\nlemma farGLeft_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) :\n    ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGLeft t ρ\n      ≤ 4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n          + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23)) := by\n  have hC0 : (0 : ℝ) ≤ 4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n      + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23)) := by\n    positivity\n  rw [← ENNReal.ofReal_le_ofReal_iff hC0]\n  rw [ENNReal.ofReal_tsum_of_nonneg (fun ρ => farGLeft_nonneg t ρ)\n    (farGLeft_summable (by linarith : (0 : ℝ) ≤ t))]\n  rw [← ENNReal.tsum_fiberwise (fun ρ => ENNReal.ofReal (farGLeft t ρ))\n    (fun ρ => Nat.floor |ρ.1.im|)]\n  have hper : ∀ ℓ : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ},\n      ENNReal.ofReal (farGLeft t b.1)\n      ≤ ENNReal.ofReal (farGLeftMaj ℓ) := by\n    intro ℓ\n    have h := farGLeft_fiber_le hZC hNLZ ht ℓ\n    rwa [farGLeftMaj] at *\n  calc ∑' j : ℕ, ∑' b : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {j},\n        ENNReal.ofReal (farGLeft t b.1)\n      ≤ ∑' j : ℕ, ENNReal.ofReal (farGLeftMaj j) := ENNReal.tsum_le_tsum hper\n    _ = ENNReal.ofReal (∑' j : ℕ, farGLeftMaj j) := by\n        rw [ENNReal.ofReal_tsum_of_nonneg farGLeftMaj_nonneg farGLeftMaj_summable]\n    _ ≤ ENNReal.ofReal (4.5 * (0.433 * (0.1942 * (1 / 23) + 0.1687)\n          + 0.886 * (0.0736 * (1 / 23) + 0.0621) + 2.9 * (1 / 23))) :=\n        ENNReal.ofReal_le_ofReal farGLeftMaj_series_le\n\nend NguyenRH1\n\nend"},"extra_content":null}]