[{"type":"thinking","thinking":"Now §17 (3e): the two tail tsum machines. This is the trickiest part — the ENNReal fiberwise pattern from `zero_tail_inv_sq_le`. Plan:\n\n**Right tail** (zeros with γ > 2t):\n```\ndef farGRight (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if 2 * t < ρ.1.im then farG t ρ else 0\n```\n- farGRight_nonneg, farGRight_summable (of_norm_bounded farG_summable).\n- The bucket: k(ρ) = Nat.floor |ρ.1.im − t| (same as main). For ρ with γ > 2t: x = γ−t > t ⟹ k ≥ Nat.floor t + 1 (k > t: k ≥ ⌊t⌋₊+1: since x > t ≥ ⌊t⌋₊: ⌊x⌋₊ ≥ ⌊t⌋₊... hmm x > t ⟹ ⌊x⌋₊ ≥ ⌊t⌋₊ (floor_mono) — need k ≥ ⌊t⌋₊+1: x > t ⟹ ⌊x⌋₊ ≥ Nat.ceil t ≥ ⌊t⌋₊... For t integer: x > t ⟹ ⌊x⌋₊ ≥ t+1 ✓ (x > t = ⌊t⌋₊ ⟹ ⌊x⌋₊ ≥ ⌊t⌋₊+1 since floor of x > t is ≥ t+1 when... x > t ⟹ ⌊x⌋₊ > t−1 hmm: ⌊x⌋₊ ≥ t? For x > t with t = 10: x = 10.5: ⌊x⌋₊ = 10 = t — NOT ≥ 11!! The bucket k = 10 for x ∈ (10, 11) — and the main finset had x < ⌊t⌋₊+1 = 11 — so x ∈ (10, 11) with t = 10 is in the MAIN (x < 11 ✓)! The tail is ρ ∉ mainFinset: x ≥ ⌊t⌋₊+1. So tail-buckets k = ⌊x⌋₊ ≥ ⌊t⌋₊+1 ⟹ k > t ✓ (⌊t⌋₊+1 > t always). GOOD — the tail condition is x ≥ ⌊t⌋₊+1 (not x > t). k ≥ ⌊t⌋₊+1 ≥ 11 (⌊t⌋₊ ≥ 10 since t ≥ 10).\n  The tail tsum (ρ ∉ mainFinset) splits into γ > 2t and γ < 0:\n  ρ ∉ mainFinset with farG ρ ≠ 0 ⟹ far (x ≥ 1) and ¬(x < ⌊t⌋₊+1) ⟹ x ≥ ⌊t⌋₊+1 > t ⟹ γ > 2t or γ < 0 ✓.\n\n- The fiberwise machine: buckets k ∈ ℕ, fiber_k = {ρ : γ > 2t, ⌊x⌋₊ = k}. Per-fiber mult count: bucket k (nonempty ⟹ k ≥ ⌊t⌋₊+1 > t): zeros with x ∈ [k, k+1), γ > 2t > t: γ = t+x ∈ [t+k, t+k+1) ⊆ zeroWindow (t+k) ✓ count ≤ C0hat(t+k+1) via hZC (t+k ≥ 2 ✓). And C0hat(t+k+1) ≤ C0hat(2k+1) (k > t ✓ mono, 1 ≤ t+k+1). Then the majorant: per-bucket contribution ≤ 4.5·farW k·C0hat(2k+1) — and the SERIES Σ'_{k} 4.5·farW k·C0hat(2k+1) — hmm, as an ENNReal fiberwise sum: Σ'_k ofReal(4.5·farW k·C0hat(2k+1)) — then bound the real tsum: Σ_{k≥11} 4.5·farW k·C0hat(2k+1) ≤ 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀] = Tail_R.\n\nThe machine (cloning zero_tail_inv_sq_le's structure):\n```\nlemma farGRight_le (hZC : ZeroCountProp) {t : ℝ} (ht : 10 ≤ t) :\n    ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGRight t ρ\n      ≤ 4.5 * (0.433 * (0.833 * 0.1 + 0.3303) + 0.886 * (0.3475 * 0.1 + 0.1216) + 2.9 * 0.1) := by\n  -- = ENNReal.ofReal_tsum_of_nonneg + ENNReal.tsum_fiberwise + per-fiber bounds + series bound\n```\nPer-fiber bound (fiber_tail_le analog): the bucket function: use `Nat.floor |ρ.1.im − t|` as the fiber map — but fibers over ALL of the subtype; the farGRight is 0 outside γ > 2t. The fiber {⌊x⌋₊ = k}:\n∑' b : fiber_k, ofReal (farGRight t b) ≤ ofReal (4.5·farW k·C0hat(2k+1)):\n- The fiber is finite (zeros with ⌊x⌋₊ = k: x < k+1 ⟹ |γ| ≤ t+k+1 ⟹ finite ball).\n- On the fiber, farGRight t ρ = if 2t < γ then farG t ρ else 0 ≤ farG t ρ ≤ 4.5·farW k·m (farG_le_farW_mul — needs x ≥ 1: fiber elements with farGRight ≠ 0 have γ > 2t ⟹ x > t ≥ 10 ≥ 1 ✓; the others are 0 ≤ ✓).\n- Σ ≤ 4.5·farW k·(fiber mult count) ≤ 4.5·farW k·C0hat(2k+1) (via the window-count bridge: fiber (with farGRight ≠ 0) ⊆ zeroWindow (t+k) — for k < ⌊t⌋₊+1: the fiber's farGRight-nonzero elements have γ > 2t and x ∈ [k,k+1): γ ∈ [2t, t+k+1) ∩ [t+k, t+k+1)... for k ≤ ⌊t⌋₊: [2t, t+k+1) with 2t ≥ t+k ⟹ γ ∈ [t+k, t+k+1) still ✓ the window bound holds for ALL k via hZC (t+k ≥ 2 ⟸ t ≥ 10, k ≥ 0 ✓). So the count ≤ C0hat(t+k+1) ≤ C0hat(2k+1) for k > t (⌊t⌋₊ < k ⟹ t < k ✓); for k ≤ ⌊t⌋₊: C0hat(t+k+1) ≤ C0hat(2t+1) ≤ C0hat(t+1)+0.55 — DIFFERENT bound! Handle: for k ≤ ⌊t⌋₊, the count bound ≤ C0hat(2t+1) ≤ C0hat(t+1)+0.55. Hmm — the majorant per bucket then varies. UGLY. \n\nSimplification: make the fiber-majorant piecewise: for the series bound, I want Σ_k 4.5·farW k·cnt(k) with cnt(k) ≤ C0hat(t+k+1) ∀ k (valid ∀ k ✓). Then split the series at 11 (like the design): Σ_{k<11} + Σ_{k≥11}: for k < 11: cnt(k) ≤ C0hat(t+11) ≤ C0hat(2t+1) (t ≥ 10, k ≤ 10: t+k+1 ≤ t+11 ≤ 2t+1 ⟸ t ≥ 10 ✓) ≤ C0hat(t+1)+0.55 — and the k<11 part ≤ (C0hat(t+1)+0.55)·4.5·Σ_{k=1}^{10} farW k ≤ (C0hat(t+1)+0.55)·4.5·S₃-part ≤ (C0+0.55)·4.5·1.3476 — WAIT — but that's the same as the main bound! Double-counting: the tail fibers with k < ⌊t⌋₊+1 are EMPTY (farGRight ≠ 0 needs γ > 2t and bucket k — for k ≤ ⌊t⌋₊: possible (x ∈ (t, ⌊t⌋₊+1) with γ > 2t requires x > t and x < ⌊t⌋₊+1 — for t = 10.5: x ∈ (10.5, 11): k = 10 = ⌊t⌋₊ — NONEMPTY fiber!). So the k = ⌊t⌋₊ fiber CAN be nonempty (when t ∉ ℤ). Its count: zeros with γ > 2t, x ∈ [⌊t⌋₊, ⌊t⌋₊+1): γ ∈ [2t, t+⌊t⌋₊+1) ⊆ [t+⌊t⌋₊, t+⌊t⌋₊+1] = zeroWindow(t+⌊t⌋₊) ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) ≤ C0+0.55 ✓. So the k < 11 part: only k = 10 (if ⌊t⌋₊ = 10) with count ≤ C0+0.55, weight 4.5·farW 10 ≤ 4.5·0.01 = 0.045 (farW 10 = 1/(10√101) ≤ 1/(10·10.0499) = 0.09951·... hmm 1/(10√101): √101 ≥ 10.0499: 1/(10·10.0499) = 0.0099503 ≤ 0.01 ✓). So the k<11 part ≤ (C0+0.55)·4.5·0.01·(number of nonempty k<11 buckets ≤ 1) — formalize: the k<11 fibers are empty for k ≠ 10... NO WAIT — fibers for k < 10: farGRight-nonzero elements need γ > 2t and ⌊x⌋₊ = k: x ≥ k... γ > 2t ⟹ x > t ≥ 10 ⟹ k = ⌊x⌋₊ ≥ 10 — for t ≥ 10: x > 10 ⟹ ⌊x⌋₊ ≥ 10 ✓ so fibers k < 10 are empty ✓. k = 10: possibly nonempty (t ∈ [10, 11)). So Σ_{k<11}-part = Σ_{k=10}-part ≤ 4.5·farW 10·C0hat(t+11) ≤ 4.5·0.01·(C0+0.55)... and C0hat(t+11) ≤ C0hat(2t+1) (t ≥ 10 ✓) ≤ C0+0.55 ✓.\n  \n  In the fiberwise machine, the majorant F(k) per bucket: I can use a UNIFORM majorant that absorbs the k<11 case: F(k) = 4.5·farW k·C0hat(2k+1) for k ≥ 11 and F(k) = 4.5·farW k·(C0+0.55) for k < 11 (only k = 10 contributes). Then Σ' F = Σ_{k=10} F + Σ_{k≥11} F ≤ 4.5·farW 10·(C0+0.55) + Tail_R-part. With farW 10 ≤ 0.01 (hmm — farW 10 = 1/(10·√101): bound ≤ 1/100: √101 ≥ 10 ⟹ 1/(10·√101) ≤ 1/100 ✓ via √101 ≥ √100 = 10: Real.sqrt_le_sqrt (by norm_num : 100 ≤ 101): √100 = 10: Real.sqrt_eq_of_sq_eq? — √100 = 10 via Real.sqrt_eq_cases? or (Real.sqrt_eq_iff...). Simplest: √101 ≥ 10 ⟺ 100 ≤ 101 via Real.le_sqrt (0 ≤ 10)(0 ≤ 101): 10 ≤ √101 ⟺ 10² ≤ 101 ✓ norm_num. So farW 10 ≤ 1/100 ✓.) \n\nThen the per-fiber count bridge needs the k-dependent case: for k < 11 (i.e. k = 10 when nonempty): count ≤ C0hat(t+11) ≤ C0+0.55; for k ≥ 11: count ≤ C0hat(t+k+1) ≤ C0hat(2k+1). Both via the SAME window argument (zeroWindow (t+k), count ≤ C0hat(t+k+1)); then case-split the C0hat bound.\n\nOK — this is doable but fiddly. The LEFT tail is cleaner (fixed family ℓ ≥ 14):\n\n**Left tail** (zeros with γ < 0):\n```\ndef farGLeft (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if ρ.1.im < 0 then farG t ρ else 0\n```\n- bucket ℓ(ρ) = Nat.floor |ρ.1.im| (for γ < 0). NoLowZeros ⟹ ℓ ≥ 14 ✓ (|γ| ≥ 14 ⟹ ⌊|γ|⌋₊ ≥ 14 via floor_mono + Nat.floor_one... |γ| ≥ 14 ⟹ ⌊|γ|⌋₊ ≥ ⌊14⌋₊ = 14: Nat.floor_mono h + Nat.floor_ofNat : ⌊(14:ℝ)⌋₊ = 14 ✓).\n- Per-element: farGLeft t ρ ≤ 4.5·m/(10+ℓ)² — needs: farG = 4.5·m/(x√(1+x²)) with x = t+|γ| (γ < 0: x = |t−γ| = t−γ = t+|γ| since γ < 0 < t): x ≥ t+ℓ (|γ| ≥ ℓ): 1/(x√(1+x²)) ≤ 1/((t+ℓ)√(1+(t+ℓ)²)) ≤ 1/(t+ℓ)² ≤ 1/(10+ℓ)² (t ≥ 10).\n  farGLeft_le (ρ): farGLeft t ρ ≤ 4.5·m/((10:ℝ)+(Nat.floor |ρ.1.im|))² — as a real.\n- Per-fiber count: fiber_ℓ = {γ < 0, ⌊|γ|⌋₊ = ℓ}: zeros with |γ| ∈ [ℓ, ℓ+1), γ < 0 ⟹ −γ ∈ [ℓ, ℓ+1) ⟹ conj ρ ∈ zeroWindow ℓ ✓ (ℓ ≥ 14 ≥ 2 ✓) — mult: zeroMult ρ = zeroMult (conj ρ) (zeroMult_conj ✓) — the fiber-image under (starRingEnd ℂ) ⊆ zeroWindow ℓ ⟹ fiber mult-sum ≤ C0hat(ℓ+1) via hZC ℓ. The image bridge: map fiber via val∘conj: Finset.image (fun ρ => (starRingEnd ℂ) ρ.1) — sum over image = sum over fiber (zeroMult_conj: each term preserved — Finset.sum_image needs injectivity of the map on the finset: conj injective ✓ but the SUM is of zeroMult of the IMAGE points: Σ_{fiber} m(ρ) = Σ_{image} m(conj ρ.1)?? — the image sum: ∑_{z ∈ fiber.image conj} (zeroMult z : ℝ) — Finset.sum_image (inj) : ∑_{x ∈ fiber} (zeroMult (conj x.1)) = ∑_{fiber} zeroMult (conj ρ.1) = ∑_{fiber} zeroMult ρ.1 (zeroMult_conj ρ.2 ✓ per-term) ✓.\n- The majorant series: Σ'_{ℓ} ofReal(4.5·C0hat(ℓ+1)/(10+ℓ)²) — real series Σ_{ℓ≥14} 4.5·C0hat(ℓ+1)/(10+ℓ)² ≤ 4.5·[0.433·(0.1942·A₀+A₁)+0.886·(0.0736·A₀+A₂)+2.9·A₀] = Tail_L ✓ with A₀ = tail14_inv_add_sq_le, A₁, A₂ ✓.\n\nThe ENNReal fiberwise machine for both tails — clone `fiber_tail_le` + `zero_tail_inv_sq_le` structure. That's ~500 lines for both. Let me look once more at the exact structure of fiber_tail_le/zero_tail_inv_sq_le to clone faithfully (I read them earlier — the pattern: fiber finite via dyadClass_fiber_finite; tsum_subtype + tsum_eq_sum + indicator; per-fiber real bound; then the outer: ofReal_tsum_of_nonneg + ENNReal.tsum_fiberwise + ENNReal.tsum_le_tsum + the real majorant series bound + ofReal_le_ofReal).\n\nFor the RIGHT tail, the fiber map: `Nat.floor |ρ.1.im − t|` (ℕ-valued) — fibers: (fun ρ => ⌊|ρ.1.im − t|⌋₊) ⁻¹' {k}.\nFor the LEFT tail: `Nat.floor |ρ.1.im|`.\n\nPer-fiber finiteness: zeros with ⌊x⌋₊ = k: x < k+1 ⟹ |γ| ≤ t+k+1 (right: |γ| = γ = t+x < t+k+1; left: |γ| < ℓ+1): finite ball finite_subtype_norm_lt.\n\nLet me write the left tail FIRST (cleaner), then the right. Actually — to economize, let me write a GENERIC fiber-tail machine that both tails instantiate. Hmm — the count bridges differ (zeroWindow vs conj). Let me just write both directly, cloning the pattern.\n\nActually, let me reconsider the outer assembly to minimize duplication. The outer theorem form (for each tail):\n```\nlemma farGLeft_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) :\n    ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, farGLeft t ρ ≤ 4.5 * (Tail_L-bracket)\n```\nStructure (from zero_tail_inv_sq_le):\n1. rw [← ENNReal.ofReal_le_ofReal_iff hC0] (C0 = the bound, nonneg).\n2. rw [ENNReal.ofReal_tsum_of_nonneg (nonneg) (summable)].\n3. rw [← ENNReal.tsum_fiberwise (fun ρ => ofReal (farGLeft t ρ)) (floor-map)].\n4. calc ∑' j, ∑' b : fiber j, ofReal (farGLeft t b) ≤ ∑' j, ofReal (F j) [ENNReal.tsum_le_tsum per-fiber]\n   _ = ofReal (∑' j, F j) [ofReal_tsum_of_nonneg reversed: ENNReal.ofReal_tsum_of_nonneg]\n   _ ≤ ofReal (bound) [ofReal_le_ofReal with the real series bound].\n5. The real series bound: ∑' j, F j ≤ bound — the tsum over ℕ of the majorant, bounded by the bricks: F(ℓ) = 4.5·C0hat(ℓ+1)/(10+ℓ)²·(if 14 ≤ ℓ) — for ℓ < 14 the fiber is empty (NoLowZeros) so the per-fiber bound can be F(ℓ) = 0 there? — cleaner: F(ℓ) = if ℓ < 14 then 0 else 4.5·C0hat(ℓ+1)/(10+ℓ)². Then ∑' F = ∑'_{ℓ≥14}-part: bound via: ∑' (fun ℓ => F (ℓ+14)) ≤ the LA-bricks: F(ℓ+14) = 4.5·C0hat(ℓ+15)/(10+ℓ+14)² — hmm — the C0hat(j+1) with j = ℓ+14: C0hat(ℓ+15) ≤ 0.433·(log(ℓ+14)+0.1942)+... — the C0hat_add_one_le_of_fourteen_le applies to j = ℓ+14 ≥ 14 ✓. Then the series Σ_{ℓ≥0} 4.5·[0.433·(log(ℓ+14)+0.1942)+0.886·(loglog(ℓ+14)+0.0736)+2.9]/((ℓ+14)+10)² — bounded by the bricks: split into the four summands: 0.433·0.1942·Σ1/(j+10)² + 0.433·Σlog j/(j+10)² + 0.886·0.0736·Σ1/(j+10)² + 0.886·Σloglog j/(j+10)² + 2.9·Σ1/(j+10)² — the bricks are EXACTLY those tsums (tail14_inv_add_sq_le etc. with j = ℓ+14) ✓. So the real series bound:\n   ∑' ℓ, F(ℓ+14) ≤ 4.5·[0.433·(0.1942·A₀+A₁)+0.886·(0.0736·A₀+A₂)+2.9·A₀] where A₀ = tail14_inv_add_sq_le's tsum... — need the tsum additivity/mul_left to assemble: each brick is a tsum bound; the sum of tsums = tsum of sums (Summable.tsum_add) — assemble: \n   ```\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   -- F(ℓ+14) ≤ 4.5·[termwise]\n   -- ∑' F(ℓ+14) ≤ 4.5·[...]\n   ```\n   And the tsum split ∑'_{ℓ:ℕ} F ℓ = Σ_{range 14} F + ∑' F(ℓ+14) via Summable.sum_add_tsum_nat_add (with F(ℓ) = 0 for ℓ < 14 ⟹ the range part = 0 ✓).\n   F's summability: dominated by the C·(bricks-summands) — the brick summands are summable (the antitone machines give summable families — tail14_log_div_add_sq_summable exists ✓; the 1/(j+10)² family: from the integral machine — its summable: antitoneOn_one_div_add_sq.summable_of_integrableOn_Ioi ✓; the loglog one: hsumm inside tail14_loglog — need to expose it? I defined hsumm inside the proof — not exposed. For the series bound, F ≤ the four summand families each summable: F summable via Summable.of_norm_bounded by their sum... Let me instead bound the REAL series via direct comparison: \n   ∑' ℓ, F(ℓ+14) ≤ ∑' ℓ, G(ℓ) where G = the 4.5·[0.433·(log+0.1942)+0.886·(loglog+0.0736)+2.9]/((ℓ+14)+10)² explicit — and ∑' G = 4.5·[0.433·(0.1942·S0+S1)+0.886·(0.0736·S0+S2)+2.9·S0] via tsum_add/tsum_mul_left with the three brick-tsums (each summable — expose the summables: tail14_log_div_add_sq_summable ✓ exists; for the other two: 1/(j+10)²-summable: expose `tail14_inv_add_sq_summable`; loglog: `tail14_loglog_div_add_sq_summable` — I need to add these (the LA₂/RW₂ proofs had inline hsumm — expose as standalone lemmas).\n   \n   G's summable: from the three summables via .mul_left/.add ✓.\n\nOK — this is a LOT of assembly. Let me estimate: left tail ~400 lines, right tail ~450 lines. Let me write them carefully.\n\nFirst — expose the summables for the brick families (small edit to §11/§12):\n- tail11_inv_sq_summable (from antitoneOn_one_div_sq.summable_of_integrableOn_Ioi).\n- tail14_inv_add_sq_summable.\n- tail11_loglog_div_sq_summable (the inline hsumm from RW₂).\n- tail14_loglog_div_add_sq_summable (the inline hsumm from LA₂).\n\nLet me write §17 now — left tail first. Structure:\n\n```lean\n/-! ## 17. Piece 3i: the left-tail machine (γ < 0) -/\n\ndef farGLeft (t : ℝ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℝ :=\n  if ρ.1.im < 0 then farG t ρ else 0\n\nlemma farGLeft_nonneg ...\nlemma farGLeft_summable ...\n\n/-- per-element bound: farGLeft ≤ 4.5·m/(10+⌊|γ|⌋₊)² -/\nlemma farGLeft_le {t : ℝ} (ht : 10 ≤ t) (hNLZ : NoLowZeros) (ρ) :\n    farGLeft t ρ ≤ 4.5 * (zeroMult ρ.1 : ℝ) / (10 + (Nat.floor |ρ.1.im| : ℝ)) ^ 2\n\n/-- the fiber finiteness -/\nlemma farGLeft_fiber_finite {t : ℝ} (ℓ : ℕ) :\n    {ρ : {ρ // IsNontrivialZero ρ} | Nat.floor |ρ.1.im| = ℓ}.Finite\n\n/-- the per-fiber count (via conj + zeroWindow + zeroMult_conj) -/\nlemma farGLeft_fiber_count (hZC) (hNLZ) {t} (ht : 10 ≤ t) (ℓ : ℕ) (hℓ : 14 ≤ ℓ) :\n    ∑ ρ ∈ (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ => ρ.1.im < 0), (zeroMult ρ.1 : ℝ)\n      ≤ C0hat (ℓ + 1)\n\n/-- the per-fiber bound (ENNReal) -/\nlemma farGLeft_fiber_le (hZC) (hNLZ) {t} (ht) (ℓ : ℕ) :\n    ∑' b : (fun ρ => Nat.floor |ρ.1.im|) ⁻¹' {ℓ}, ENNReal.ofReal (farGLeft t b.1)\n      ≤ ENNReal.ofReal (if 14 ≤ ℓ then 4.5 * C0hat (ℓ + 1) / (10 + (ℓ : ℝ)) ^ 2 else 0)\n\n/-- the real series bound -/\nlemma farGLeft_series_le : ∑' ℓ : ℕ, (if 14 ≤ ℓ then 4.5 * C0hat (ℓ + 1) / (10 + (ℓ : ℝ)) ^ 2 else 0)\n      ≤ 4.5 * (0.433 * (0.1942 * (1/23) + 0.1687) + 0.886 * (0.0736 * (1/23) + 0.0621) + 2.9 * (1/23))\n\n/-- **The left-tail bound** -/\nlemma farGLeft_le (hZC) (hNLZ) {t} (ht) :\n    ∑' ρ, farGLeft t ρ ≤ ...\n```\n\nWait — the per-element bound: farG for γ < 0: farG = 4.5·m/(x√(1+x²)) with x = t−γ = t+|γ|: x ≥ t+⌊|γ|⌋₊·... |γ| ≥ ⌊|γ|⌋₊: x ≥ t+ℓ. So 1/(x√(1+x²)) ≤ 1/((t+ℓ)√(1+(t+ℓ)²)) ≤ 1/(t+ℓ)² ≤ 1/(10+ℓ)² (t ≥ 10). Formalize:\n```\nlemma farGLeft_term_le {t : ℝ} (ht : 10 ≤ t) (hNLZ : NoLowZeros) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :\n    farGLeft t ρ ≤ 4.5 * (zeroMult ρ.1 : ℝ) / (10 + (Nat.floor |ρ.1.im| : ℝ)) ^ 2 := by\n  by_cases hγ : ρ.1.im < 0\n  · rw [farGLeft, if_pos hγ]\n    -- far case: ρ far from t (x = t − γ ≥ t > 1)\n    have hxfar : ρ ∉ nearZerosSub t := by\n      intro hmem\n      have h1 := mem_nearZerosSub.mp hmem\n      -- |γ − t| < 1 but γ < 0 < t: |γ − t| = t − γ > t ≥ 10 contradiction\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    -- x = t + |γ| ≥ t + ℓ\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    -- the chain: x√(1+x²) ≥ (t+ℓ)²-ish\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      -- (10+ℓ)² ≤ x·√(1+x²): since 10+ℓ ≤ x and 10+ℓ ≥ ... (10+ℓ)² ≤ x·x ≤ x·√(1+x²)\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\nThe per-fiber count:\n```\nlemma farGLeft_fiber_count (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)\n    (ℓ : ℕ) (hℓ : 14 ≤ ℓ) :\n    ∑ ρ ∈ (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ => ρ.1.im < 0), (zeroMult ρ.1 : ℝ)\n      ≤ C0hat ((ℓ : ℝ) + 1) := by\n  classical\n  set FS := (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ => ρ.1.im < 0) with hFS\n  -- map via ρ ↦ conj ρ.1 into zeroWindow ℓ\n  have hsub : FS.image (fun ρ => (starRingEnd ℂ) ρ.1) ⊆ (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    -- hmem : ⌊|ρ.1.im|⌋₊ = ℓ\n    have hγ2 : ((starRingEnd ℂ) ρ.1).im = -ρ.1.im := Complex.conj_im _\n    have habs : |(starRingEnd ℂ) ρ.1|.im?? — the im of conj: (conj ρ).im = −ρ.im ✓\n    -- |γ| ∈ [ℓ, ℓ+1): ℓ ≤ −γ < ℓ+1 ⟹ conj.im = −γ ∈ [ℓ, ℓ+1) ⊆ zeroWindow ℓ\n    have hℓ1 : (ℓ : ℝ) ≤ |ρ.1.im| := by\n      have h1 := Nat.floor_le (abs_nonneg ρ.1.im)\n      rw [hmem] at h1\n      exact h1\n    have hℓ2 : |ρ.1.im| < (ℓ : ℝ) + 1 := by\n      have h1 := Nat.lt_floor_add_one |ρ.1.im|\n      rw [hmem] at h1\n      exact h1\n    have hneg : |ρ.1.im| = -ρ.1.im := abs_of_neg hγ\n    rw [Set.Finite.mem_toFinset]\n    refine ⟨isNontrivialZero_conj ρ.2, ?_, ?_⟩\n    · rw [hγ2, hneg] at *; linarith [hℓ1]\n    · rw [hγ2, hneg] at *; linarith [hℓ2]\n  -- the sum bridge via zeroMult_conj\n  have hbridge : ∑ ρ ∈ FS, (zeroMult ρ.1 : ℝ)\n      = ∑ z ∈ FS.image (fun ρ => (starRingEnd ℂ) ρ.1), (zeroMult z : ℝ) := by\n    rw [Finset.sum_image (fun x _ y _ h => by\n      have h2 := (starRingEnd ℂ).injective h\n      exact Subtype.ext h2)]\n    exact Finset.sum_congr rfl (fun ρ _ => by rw [zeroMult_conj ρ.2])\n  ...\n```\nHmm — Finset.sum_image (h : Set.InjOn) : ∑_{x ∈ s} g (f x) = ∑_{y ∈ s.image f} g y — direction: the sum over the image of g equals the sum over s of g∘f. I want: ∑_{z ∈ image} m(z) = ∑_{ρ ∈ FS} m(conj ρ.1) = ∑_{ρ ∈ FS} m(ρ.1) (per-term zeroMult_conj). So: hbridge : ∑_{ρ ∈ FS} m(ρ.1) = ∑_{z ∈ image} m(z): via Finset.sum_image : ∑_{x ∈ FS} m(conj x.1) = ∑_{z ∈ image} m(z) — and ∑_{x ∈ FS} m(conj x.1) = ∑_{x ∈ FS} m(x.1) via per-term zeroMult_conj ✓:\n```\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```\nThen ≤ the zeroWindow sum = hZC ℓ (ℓ ≥ 14 ≥ 2 ✓) ≤ C0hat(ℓ+1) ✓.\n\nThe fiber finiteness: zeros with ⌊|γ|⌋₊ = ℓ: |γ| < ℓ+1 ⟹ ‖ρ‖ ≤ |re|+|im| ≤ 1+ℓ+1 = ℓ+2 ⟹ finite_subtype_norm_lt (ℓ+2) ✓.\n\nThe per-fiber ENNReal bound: clone fiber_tail_le:\n```\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 ρ => 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  -- the real sum over the fiber ≤ the bound\n  by_cases hℓ : 14 ≤ ℓ\n  · rw [if_pos hℓ]\n    -- split the fiber by γ < 0 (farGLeft = 0 for γ ≥ 0)\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 ρ => ¬ ρ.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    have hfilter_eq : hfin.toFinset.filter (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => ρ.1.im < 0)\n        = (farGLeft_fiber_finite ℓ).toFinset.filter (fun ρ => ρ.1.im < 0) := by\n      ext ρ\n      simp only [Finset.mem_filter, Set.Finite.mem_toFinset]\n      -- membership: (⌊|ρ.1.im|⌋₊ = ℓ) ∧ γ < 0 — both sides same? hfin.toFinset has ⌊|·|⌋₊ = ℓ ✓ farGLeft_fiber_finite same def ✓ — need the defs to match: make farGLeft_fiber_finite's set EXACTLY the fiber set.\n      exact Iff.rfl\n    rw [hfilter_eq]\n    calc ∑ ρ ∈ ..., farGLeft t ρ\n        ≤ ∑ ρ ∈ ..., 4.5 * (zeroMult ρ.1 : ℝ) / (10 + (ℓ : ℝ)) ^ 2 := by\n          apply Finset.sum_le_sum\n          intro ρ hρ\n          rw [Finset.mem_filter] at hρ\n          have h1 := farGLeft_term_le ht hNLZ ρ\n          -- 4.5·m/(10+⌊|γ|⌋₊)² = 4.5·m/(10+ℓ)² on the fiber\n          rw [Finset.mem_filter] at hρ\n          obtain ⟨hmem, hγ⟩ := hρ\n          rw [Set.Finite.mem_toFinset] at hmem\n          rw [hmem] at h1\n          exact h1\n      _ = (4.5 / (10 + (ℓ : ℝ)) ^ 2) * ∑ ρ ∈ ..., (zeroMult ρ.1 : ℝ) := by\n          rw [Finset.mul_sum]\n          apply Finset.sum_congr rfl\n          intro ρ _\n          ring\n      _ ≤ (4.5 / (10 + (ℓ : ℝ)) ^ 2) * C0hat ((ℓ : ℝ) + 1) :=\n          mul_le_mul_of_nonneg_left (farGLeft_fiber_count hZC hNLZ ht ℓ hℓ) (by positivity)\n      _ = 4.5 * C0hat ((ℓ : ℝ) + 1) / (10 + (ℓ : ℝ)) ^ 2 := by ring\n  · rw [if_neg hℓ]\n    -- the fiber's farGLeft is all 0 (γ ≥ 0 ⟹ farGLeft = 0; γ < 0 with ℓ < 14: NoLowZeros gives |γ| ≥ 14 ⟹ ⌊|γ|⌋₊ ≥ 14 ≠ ℓ)\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ρ  -- hρ : ⌊|ρ.1.im|⌋₊ = ℓ: 14 ≤ ℓ contradiction\n      omega\n    · rw [farGLeft, if_neg hγ]\n```\nHmm — the hNLZ form: NoLowZeros : ∀ ρ, IsNontrivialZero ρ → 14 ≤ |ρ.im| ✓ hNLZ ρ.1 ρ.2 ✓.\nAnd `h2 : 14 ≤ Nat.floor |ρ.1.im|` via Nat.floor_mono h1 : ⌊14⌋₊ ≤ ⌊|γ|⌋₊, Nat.floor_ofNat : ⌊(14:ℝ)⌋₊ = 14 ✓. Then hρ : ⌊|γ|⌋₊ = ℓ ⟹ ℓ = ⌊|γ|⌋₊ ≥ 14 ⟹ ¬(¬14 ≤ ℓ) ✓ omega with hℓ : ¬14 ≤ ℓ.\n\nWait — in the hℓ-false case, the sum is over hfin.toFinset (ALL fiber elements incl. γ ≥ 0 which give farGLeft = 0 ✓). But the γ < 0 ones: their ⌊|γ|⌋₊ ≥ 14 ≠ ℓ (ℓ < 14) — contradicting fiber membership. So all terms 0 ✓.\n\nHmm — but hρ after `rw [Set.Finite.mem_toFinset] at hρ` — hρ : ρ ∈ the fiber set = ⌊|ρ.1.im|⌋₊ = ℓ ✓.\n\nOne important check: the FIBER SET def — `farGLeft_fiber_finite ℓ` must produce the same set as the fiber preimage:\n```\nlemma farGLeft_fiber_finite (ℓ : ℕ) :\n    {ρ : {ρ : ℂ // IsNontrivialZero ρ} | Nat.floor |ρ.1.im| = ℓ}.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    rw [hmem] at h2\n    exact 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```\nAnd in farGLeft_fiber_le, the fiber set (fun ρ => ⌊|ρ.1.im|⌋₊) ⁻¹' {ℓ} — show it equals {ρ | ⌊|ρ.1.im|⌋₊ = ℓ}: ext + Iff.rfl (as in fiber_tail_le's hfin).\n\nNow — the hfilter_eq Iff.rfl issue: hfin.toFinset.filter (γ < 0) vs (farGLeft_fiber_finite ℓ).toFinset.filter (γ < 0) — both filter the same predicate over the same set (if defs align): make farGLeft_fiber_finite's statement use EXACTLY the fiber preimage set:\n```\nlemma farGLeft_fiber_finite (ℓ : ℕ) :\n    ((fun ρ : {ρ : ℂ // IsNontrivialZero ρ} => Nat.floor |ρ.1.im|) ⁻¹' {ℓ} :\n      Set {ρ : ℂ // IsNontrivialZero ρ}).Finite := ...\n```\nthen in fiber_le: hfin := farGLeft_fiber_finite ℓ directly ✓ no Iff.rfl bridge needed for the toFinset... The tsum_eq_sum uses hfin.toFinset ✓ and the filter afterward: both over hfin.toFinset ✓ no bridge ✓.\n\nHmm wait — farGLeft_fiber_count ALSO uses (farGLeft_fiber_finite ℓ).toFinset.filter — consistent ✓.\n\nThe real series bound + the outer assembly. Let me also handle farGLeft's summability: of_norm_bounded farG_summable (|farGLeft| ≤ farG since farGLeft is farG or 0 ✓).\n\nLet me now write the full §17 (left tail) + §18 (right tail) — actually, let me do the left tail first and compile it, then the right tail in the next edit. Write §17 now.","signature":""},{"type":"text","text":"Now §17 (3e-i: the left-tail machine). This is the biggest sub-stage; writing it in one go."},{"type":"tool_use","id":"Edit_179","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):\nthe mult-weighted count of zeros with ⌊|γ|⌋₊ = ℓ and γ < 0 is ≤ C0hat(ℓ+1). -/\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 left-tail majorant series (if-form on ℕ). -/\ndef farGLeftMaj : ℕ → ℝ := fun ℓ =>\n  if 14 ≤ ℓ then 4.5 * C0hat ((ℓ : ℝ) + 1) / (10 + (ℓ : ℝ)) ^ 2 else 0\n\n/-- The shifted majorant is summable (dominated by the LA-brick families). -/\nlemma farGLeftMaj_shift_summable :\n    Summable (fun ℓ : ℕ => farGLeftMaj (ℓ + 14)) := by\n  have hbase : Summable (fun ℓ : ℕ =>\n      (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 h1 : 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    have h2 : Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) :=\n      tail14_log_div_add_sq_summable\n    have h3 : 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\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      have h7 : (1 / Real.exp 1) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)\n          ≤ (0.3679 : ℝ) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by\n        apply mul_le_mul_of_nonneg_right _ (by positivity : (0 : ℝ) ≤\n          Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)\n        exact one_div_exp_one_le\n      have h8 : Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2\n          ≤ Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2 := le_rfl\n      have h9 : Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2\n          ≤ Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2 := by\n        calc Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2\n            ≤ (1 / Real.exp 1) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := h6\n          _ ≤ (0.3679 : ℝ) * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := h7\n          _ ≤ 1 * (Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) := by\n              apply mul_le_mul_of_nonneg_right _ (by positivity : (0 : ℝ) ≤\n                Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)\n              norm_num\n          _ = Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2 := by ring\n      exact h9\n    exact ((h1.mul_left _).add (h2.mul_left _)).add (h3.mul_left _)\n  apply Summable.of_norm_bounded hbase\n  intro ℓ\n  rw [farGLeftMaj]\n  have hℓ : 14 ≤ ℓ + 14 := by omega\n  rw [if_pos hℓ]\n  have h1 := C0hat_add_one_le_of_fourteen_le (j := ℓ + 14) (by omega : 14 ≤ ℓ + 14)\n  rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : (0 : ℝ) ≤\n    4.5 * C0hat ((ℓ + 14 : ℝ) + 1) / (10 + ((ℓ + 14 : ℕ) : ℝ)) ^ 2)]\n  have h2 : (0 : ℝ) ≤ (0.433 * Real.log ((ℓ : ℝ) + 14) / (((ℓ : ℝ) + 14) + 10) ^ 2) := by\n    have h3 : (0 : ℝ) ≤ Real.log ((ℓ : ℝ) + 14) :=\n      Real.log_nonneg (by\n        have h : (0 : ℝ) ≤ (ℓ : ℝ) := Nat.cast_nonneg ℓ\n        linarith : (1 : ℝ) ≤ (ℓ : ℝ) + 14)\n    positivity\n  have h4 : (0 : ℝ) ≤ (0.886 * Real.log (Real.log ((ℓ : ℝ) + 14)) / (((ℓ : ℝ) + 14) + 10) ^ 2) := by\n    have h5 : (0 : ℝ) ≤ Real.log (Real.log ((ℓ : ℝ) + 14)) := by\n      apply Real.log_nonneg\n      have h6 : (1 : ℝ) ≤ Real.log ((ℓ : ℝ) + 14) := by\n        have h7 := log_fourteen_ge\n        have h8 : Real.log 14 ≤ Real.log ((ℓ : ℝ) + 14) :=\n          Real.log_le_log (by norm_num : (0 : ℝ) < 14) (by\n            have h : (0 : ℝ) ≤ (ℓ : ℝ) := Nat.cast_nonneg ℓ\n            linarith)\n        linarith [h7, h8]\n      exact h6\n    positivity\n  have hcast : ((ℓ + 14 : ℕ) : ℝ) = (ℓ : ℝ) + 14 := by push_cast; ring\n  have hmain : 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  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  rw [hcast]\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          exact h1\n    _ = (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 [h9]\n          field_simp\n          ring\n    _ ≤ (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) := le_rfl\n\n/-- **The left-tail series bound**: the farGLeftMaj series is at most\n4.5·[0.433·(0.1942/23 + 0.1687) + 0.886·(0.0736/23 + 0.0621) + 2.9/23]. -/\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 hsumm : Summable farGLeftMaj := by\n    apply (summable_nat_add_iff (f := farGLeftMaj) 14).mp\n    exact farGLeftMaj_shift_summable\n  have hsplit : (∑' ℓ : ℕ, farGLeftMaj ℓ)\n      = (∑ ℓ ∈ Finset.range 14, farGLeftMaj ℓ) + ∑' ℓ : ℕ, farGLeftMaj (ℓ + 14) :=\n    (hsumm.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  -- the shifted series bound via the LA bricks\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 hpt : ∀ ℓ : ℕ, 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    intro ℓ\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  have hsumm_shift : 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    have h1 : 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    have h2 : Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) :=\n      tail14_log_div_add_sq_summable\n    have h3 : 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    exact ((h1.mul_left _).add (h2.mul_left _)).add (h3.mul_left _) |>.mul_left _\n  have hle := Summable.tsum_le_tsum hpt farGLeftMaj_shift_summable hsumm_shift\n  -- evaluate the majorant tsum\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    have h1 : 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    have h2 : Summable (fun j : ℕ => Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) :=\n      tail14_log_div_add_sq_summable\n    have h3 : 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    have hadd : (∑' ℓ : ℕ,\n        ((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        = (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23)\n            + 0.433 * 0.1687 + 0.886 * 0.0621 := by\n      have hs1 : (∑' j : ℕ, (1 : ℝ) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 1 / 23 := hA0\n      have hs2 : (∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2) ≤ 0.1687 := hA1\n      have hs3 : (∑' j : ℕ, Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2)\n          ≤ 0.0621 := hA2\n      rw [Summable.tsum_add (h1.mul_left _ |>.add (h2.mul_left _)) (h3.mul_left _)]\n      rw [Summable.tsum_add (h1.mul_left _) (h2.mul_left _)]\n      rw [tsum_mul_left, tsum_mul_left, tsum_mul_left]\n      -- the bound is an equality-free inequality; assemble with le\n      have hA0' : (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23)\n          + 0.433 * 0.1687 + 0.886 * 0.0621\n          = (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23)\n            + 0.433 * 0.1687 + 0.886 * 0.0621 := rfl\n      have hle1 : (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) *\n          (∑' j : ℕ, (1 : ℝ) / (((j : ℝ) + 14) + 10) ^ 2)\n          ≤ (0.433 * 0.1942 + 0.886 * 0.0736 + 2.9) * (1 / 23) :=\n        mul_le_mul_of_nonneg_left hs1 (by positivity)\n      have hle2 : 0.433 * (∑' j : ℕ, Real.log ((j : ℝ) + 14) / (((j : ℝ) + 14) + 10) ^ 2)\n          ≤ 0.433 * 0.1687 :=\n        mul_le_mul_of_nonneg_left hs2 (by positivity)\n      have hle3 : 0.886 * (∑' j : ℕ,\n          Real.log (Real.log ((j : ℝ) + 14)) / (((j : ℝ) + 14) + 10) ^ 2)\n          ≤ 0.886 * 0.0621 :=\n        mul_le_mul_of_nonneg_left hs3 (by positivity)\n      -- hmm — hadd is an EQUALITY claim but I only have ≤ for each piece.\n      -- Replace: make heval an inequality instead (see below).\n      sorry\n    sorry\n  sorry\n\nend NguyenRH1\n\nend"},"extra_content":null}]