[{"type":"thinking","thinking":"I now have all the patterns I need:\n\n1. **`dyadic_family_le`** — the finset version (main range): given FS finite, a bucket index j(ρ) ∈ Ico 1 (J+1), per-element bound g ≤ C₁·m·w(j(ρ)), per-fiber mult count ≤ cnt j ⟹ FS-sum ≤ Σ w·cnt. I'll write an analogous `unit_family_le` where the weight is a general W j (not just C₁/2^j). Actually — I can GENERALIZE: the proof structure is identical with weight W j instead of C₁/2^j. Let me write `unit_family_le` with (W : ℕ → ℝ) and bound `g ρ ≤ W (j ρ) * m ρ` (needs W j ≥ 0).\n\n2. **The tail tsum machine** (`zero_tail_inv_sq_le` pattern): ENNReal.ofReal_tsum_of_nonneg + ENNReal.tsum_fiberwise + per-fiber bound (fiber_tail_le-style: tsum over the fiber subtype = finset sum ≤ weight × count) + comparison with a summable real majorant + tsum_le_tsum + ofReal_le_ofReal.\n\n3. **The weight-sum bricks** (RW₀/1/2, LA₀/1/2, S₃) via `AntitoneOn.tsum_comp_add_le_integral` + explicit integrals (the hasDerivAt antiderivative pattern already in LiTightR for log/x²).\n\nNow — plan the file layout. Piece 3 goes into LiTightR.lean (per journal: \"piece 3 in LiTightR.lean\"). It's already ~820 lines; piece 3 will add maybe 900+. That's fine (LiCircleBound is 3928).\n\nOrder of construction (bottom-up):\n- §9: the real weight functions + the numeric bricks:\n  - `farWeight k := 1/(k·sqrt(1+k²))` (k ≥ 1).\n  - S₃: Σ_{k≥1} farWeight k ≤ 1.3476. Proof: split tsum at 4: Σ_{k=1..4} exact (via sqrt rational lower bounds) + Σ_{k≥5} 1/(k(k−1)) = 1/4 (telescope). The telescope: ∑'_{n:ℕ} 1/((n+5)(n+4)) = 1/4. Via 1/((n+5)(n+4)) = 1/(n+4) − 1/(n+5): telescope tsum = 1/4: pattern: `Summable.hasSum` of partial sums: Σ_{n<N} (1/(n+4)−1/(n+5)) = 1/4 − 1/(N+4) → 1/4. There might be a Mathlib lemma `Real.tsum_one_div_natCast_mul_natCast_add_one`? Not sure. I'll prove via Finset.sum_range_sub + tendsto. Actually check: `tsum_one_div_mul_add_one`? Hmm, safer to prove manually:\n    summable: comparison with 1/n² (summable_one_div_nat_pow 2-ish; or use the telescope itself: hasSum via partial sums).\n    hasSum: partial sums telescope: ∑_{n ∈ range N} (1/(n+4) − 1/(n+5)) = 1/4 − 1/(N+4) (Finset.sum_range_sub' — the telescoping sum lemma: `Finset.sum_range_sub` : ∑ i in range n, (f (i+1) − f i) = f n − f 0; and sum_range_sub' = f 0 − f n). Then → 1/4 since 1/(N+4) → 0. hasSum ⟹ tsum = 1/4. ✓\n  - The exact terms: 1/(1·√2) ≤ 1/1.414 etc. — need √2 ≥ 1.414: `Real.le_sqrt` (x ≤ sqrt y ⟺ x² ≤ y for x ≥ 0?): Real.le_sqrt : 0 ≤ x → (x ≤ sqrt y ⟺ x^2 ≤ y)? Signature something like `Real.le_sqrt (hx : 0 ≤ x) : x ≤ sqrt y ↔ x^2 ≤ y`. Then 1.414² = 1.999396 ≤ 2 ✓ norm_num.\n    Then farWeight 1 = 1/(1·√(1+1²)) = 1/√2 ≤ 1/1.414: div_le_div_of_nonneg_left... need √2 > 0 etc.\n    farWeight 1 ≤ 0.70721; farWeight 2 ≤ 0.22422; farWeight 3 ≤ 0.10549; farWeight 4 ≤ 0.06064. Sum + 1/4: 0.70721+0.22422+0.10549+0.06064+0.25 = 1.34756 ≤ 1.3476 ✓.\n    The tsum split: ∑'_{k≥1} farWeight k = Σ_{k ∈ range 4} farWeight (k+1) + ∑' farWeight (k+5) — via Summable.sum_add_tsum_nat_add (used in this file already ✓) — need farWeight-summability on the shifted index: farWeight (k+5) ≤ 1/((k+5)(k+4)) (telescope dominator — since k√(1+k²) ≥ k(k−1)... for k ≥ 5: k−1 ≤ √(1+k²) ⟹ k(k−1) ≤ k√(1+k²) ⟹ 1/(k√(1+k²)) ≤ 1/(k(k−1)) ✓). Summability: of_norm_bounded by the telescope sum.\n  - Right-tail bricks:\n    - RW₀: Σ_{k≥11} 1/k² ≤ 0.1: antitone f = 1/x² on Ici 10, integrable, ∫ = 1/10. Pattern: `AntitoneOn.tsum_comp_add_le_integral` gives ∑'_{n} f(n+11) ≤ ∫_{Ioi 10} f(x). The integral ∫₁₀^∞ 1/x² = 1/10: antiderivative −1/x: `integral_Ioi_of_hasDerivAt_of_tendsto'` (used above ✓) with F(x) = −1/x, F'(x) = 1/x², F → 0, boundary −F(10) = 1/10 ✓.\n      Need: AntitoneOn (1/x²) (Ici 10) — via antitoneOn_of_deriv_nonpos or simpler: directly by monotonicity of x²: intro a ha b hb hab: 1/a² ≥ 1/b² ⟺ b² ≥ a² — `one_div_le_one_div_of_le` (banked: takes the small side's positivity first) + pow_le_pow_left₀. Simple direct proof, no calculus ✓.\n      IntegrableOn 1/x² (Ioi 10): integrableOn_Ioi_deriv_of_nonneg' pattern ✓.\n      Summability of the n-shift: via AntitoneOn.summable_of_integrableOn_Ioi (pattern above ✓).\n    - RW₁: Σ_{k≥11} log k/k² ≤ 0.3303: f = log x/x², antitone on Ici 10 — the file already has `antitoneOn_log_div_sq` on Ici 3!! Reuse (Ici 10 ⊆ Ici 3: AntitoneOn.mono ✓). Integrable: `integrableOn_log_div_sq` on Ioi 3 ⊇ Ioi 10 (IntegrableOn.mono_set ✓). Integral ∫₁₀^∞ log x/x² = (log 10+1)/10: same antiderivative pattern (integral_Ioi_of_hasDerivAt_of_tendsto' with F = −(log x+1)/x — `hasDerivAt_neg_log_add_one_div` exists ✓ — boundary: F(10) = −(log 10+1)/10, integral = 0 − F(10) = (log 10+1)/10 ≤ (2.3026+1)/10 = 0.33026 ≤ 0.3303: need log 10 ≤ 2.3026 (certify via exp partial sums like log 3 ≤ 1.1 in this file).\n    - RW₂: Σ_{k≥11} log(log k)/k² ≤ 0.1269: f = loglog x/x². Antitone on Ici 10: antitoneOn_of_deriv_nonpos — derivative = (1/log x − 2·loglog x)/x³: need HasDerivAt computation: d/dx[loglog x·x^{-2}] = (1/(x log x))·x^{-2} + loglog x·(−2x^{-3}) = (1/log x − 2 loglog x)/x³. ≤ 0 ⟺ 1 ≤ 2·log x·loglog x: for x ≥ 10: log x ≥ log 10 ≥ 2.3, loglog x ≥ loglog 10 ≥ 0.8 (log 10 ≥ 2.3, log 2.3 ≥ 0.83 — need log 2.3026 ≥ 0.83: e^0.83 = 2.2933 ≤ 2.3026 ✓): 2·2.3·0.8 = 3.68 ≥ 1 ✓. So deriv ≤ 0 via: 1/log x ≤ 1/2.3 = 0.435 and 2 loglog x ≥ 1.66 ⟹ 1/log x − 2 loglog x ≤ 0.435−1.66 < 0 ✓.\n      Integrable + integral: loglog x/x² = d/dx[−loglog x/x] + 1/(x²·log x). Hmm — for the integral test I need ∫₁₀^∞ f ≤ 0.1269. Approach: bound f(x) = loglog x/x² = d/dx[−loglog x/x] + 1/(x² log x), so ∫₁₀^∞ f = [0 − (−loglog 10/10)] + ∫₁₀^∞ 1/(x² log x) = loglog(10)/10 + ∫₁₀^∞ 1/(x² log x). And ∫₁₀^∞ 1/(x² log x) ≤ (1/log 10)·∫₁₀^∞ 1/x² = 1/(10·log 10) ≤ 1/(10·2.3025) = 0.043431·... ≤ 0.04344. Total ≤ 0.8341/10 + 0.04344 = 0.08341+0.04344 = 0.12685 ≤ 0.1269 ✓.\n      In Lean: ∫ f = ∫ g + ∫ h where g = deriv-part, h = 1/(x² log x): use `integral_add` (both integrable: g integrable via deriv machinery; h integrable: bounded by (1/log 10)/x² integrable ✓ — IntegrableOn.mono with eventually... need ae-comparison, there's `IntegrableOn.mono` (takes hfg : ∀ x ∈ s, ‖f x‖ ≤ ‖g x‖) — the pattern in Mathlib: `IntegrableOn.mono_fun`? I'll use Integrable.of_norm_bounded... on sets: `MeasureTheory.IntegrableOn.mono_fun hf hg` hmm. Let me not over-plan; the standard route: integrableOn_of_deriv... for h: h = (1/log x)·(1/x²) and 1/log x ≤ 1/log 10: bound ‖h‖ ≤ (1/log 10)·(1/x²), use `MeasureTheory.IntegrableOn.mono'` or `.mono` with the norm comparison. Fine.\n      Hmm — actually, is there a slicker way for RW₂? Bound loglog x ≤ c·(log x)^{1/2}-ish? No — keep the plan.\n      Actually even slicker: since loglog x ≤ log x / e·... loglog x ≤ log(x)/e? (max of log u/u is 1/e at u = e: log u ≤ u/e for u > 0: loglog x ≤ log x/e ⟺ log(log x) ≤ log x/e — with u = log x: log u ≤ u/e ✓ since log u ≤ u/e for all u > 0 (u/e is the tangent at u = e: log u ≤ u/e ⟺ log u − 1 ≤ (u−e)/e·... the standard log u ≤ u − 1 gives log u ≤ u/e after u ↦ u/e: log(u/e) ≤ u/e − 1 ⟹ log u ≤ u/e). So loglog x ≤ (1/e)·log x ≤ 0.3679·log x. Then RW₂ ≤ 0.3679·RW₁ ≤ 0.3679·0.3303 = 0.12151 ≤ 0.1269 ✓!! MUCH simpler — no new integral! log u ≤ u/e: from Real.log_le_sub_one_of_pos? log u ≤ u−1... substitute: log(u/e) ≤ u/e − 1: log u − 1 ≤ u/e − 1 ⟹ log u ≤ u/e ✓. In Lean: have := Real.log_le_sub_one_of_pos (x := u/e) (pos): log(u/e) ≤ u/e − 1; rw log_div at; linarith. Need u > 0 ✓ (u = log x ≥ log 10 > 0).\n      With 1/e ≤ 0.3679 (e ≥ 2.718: 1/2.718 = 0.36792 ≤ 0.3679 ✓): RW₂ ≤ 0.3679·RW₁.\n      Then RW₂-contribution: 0.886·0.3475·W₀ + 0.886·RW₂ ≤ 0.886·(0.03475+0.12151) = 0.886·0.15626 = 0.13845 (vs my earlier 0.14322 with RW₂ ≤ 0.1269 — wait, 0.886·(0.3475·0.1+0.1269) = 0.886·0.16165 = 0.14322; with 0.12151: 0.886·0.15626 = 0.13845 — BETTER by 0.005). New Tail_R = 0.17909+0.13845+0.29 = 0.60754. ×4.5 = 2.73393.\n  - Left-tail bricks:\n    - LA₀: Σ_{j≥14} 1/(j+10)² ≤ 1/23: f = 1/(x+10)², antitone on Ici 13 ✓ (direct), integrable (deriv of −1/(x+10)), ∫₁₃^∞ = 1/23 ✓.\n    - LA₁: Σ_{j≥14} log j/(j+10)² ≤ 0.1687: f = log x/(x+10)². Antitone on Ici 13: derivative: (1/x·(x+10)² − 2(x+10)log x)/(x+10)⁴ = ((x+10)/x − 2 log x)/(x+10)³ ≤ 0 ⟺ (x+10)/x ≤ 2 log x: x ≥ 13: LHS = 1+10/x ≤ 1+10/13 = 1.7693; RHS ≥ 2·log 13 ≥ 2·2.5649 = 5.1298 ✓.\n      Integrable + ∫₁₃^∞ = 0.16862: antiderivative F(x) = −log x/(x+10) + (1/10)·log(x/(x+10)). HasDerivAt: messy but doable: F = −(log x)·(x+10)⁻¹ + (1/10)(log x − log(x+10)). F' = −(1/x)(x+10)⁻¹ + log x·(x+10)⁻² + (1/10)(1/x − 1/(x+10)) = log x/(x+10)² + [−(1/x)/(x+10) + (1/10)·(10/(x(x+10)))] = log x/(x+10)² + [−1/(x(x+10)) + 1/(x(x+10))] = log x/(x+10)² ✓.\n      Boundary: F(x) → 0 as x → ∞: −log x/(x+10) → 0 (log x/x → 0) and (1/10)·log(x/(x+10)) → (1/10)·log 1 = 0 (x/(x+10) → 1, log continuous at 1). Integral = 0 − F(13) = log 13/23 + (1/10)·log(23/13) ≤ 2.5650/23 + 0.5710/10 = 0.111522+0.0571 = 0.168622 ≤ 0.1687 ✓.\n      Certified numerics: log 13 ≤ 2.5650 (e^2.565 ≥ 13: partial sums — e^2.565 = e^2·e^0.565·... or directly e^2.5650 ≥ Σ_{k<9} 2.565^k/k! — let me precompute: e^2.565 ≈ 13.0010 ✓ (I'll verify numerically before certifying). log(23/13) ≤ 0.5710: e^0.571 ≥ 23/13 ⟺ e^0.571 ≥ 1.76923: e^0.571 ≈ 1.77001 ✓.\n    - LA₂: Σ_{j≥14} loglog j/(j+10)² ≤ 0.0632: same trick as RW₂! loglog j ≤ (1/e)·log j: LA₂ ≤ 0.3679·LA₁ ≤ 0.3679·0.1687 = 0.062061 ≤ 0.0632 ✓. (Even simpler.) Then LA₂-contribution: 0.886·(0.0736·A₀ + LA₂) = 0.886·(0.0032+0.06207) = 0.886·0.06527 = 0.05783 (vs 0.058808 — better by 0.001). New Tail_L = 0.433·(0.0084432+0.16862) + 0.05783 + 0.126087 = 0.076667+0.05783+0.126087 = 0.260584. ×4.5 = 1.17263.\n\nUpdated totals:\n- Main: 4.5·(2C₀+0.55)·1.3476 = 12.1284·C₀ + 3.33594.\n- Tail_R: 4.5·0.60754 = 2.73393.\n- Tail_L: 4.5·0.260584 = 1.17263.\n- Piece3 ≤ 12.1284·C₀ + 3.33594+2.73393+1.17263 = 12.1284·C₀ + 7.2425.\n\nAssembly: 1+2.7+(12.1284·2.9658+7.2425)+0.09+0.6 = 1+2.7+35.964+7.2425+0.09+0.6 = 47.5965. Pinch: f(L) = 11.6321·LL − 4.6484·L ≤ 48−47.5965 = 0.4035; f max −0.9669 ✓ margin 1.37. \n\nLet me fix the FINAL constants:\n- piece3 statement: ‖far‖ ≤ 12.1284·C0hat(t+1) + 7.2425.\n\nActually — hold on, let me double-check the main's right-side increment C0hat(2t+1) ≤ C0hat(t+1)+0.55 once more, and also double check C0hat(j+1) ≤ 0.433·(log j+0.1942)+0.886·(loglog j+0.0736)+2.9 and C0hat(2k+1) ≤ 0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9:\n\nC0hat(y) = 0.433·log(y+2) + 0.886·log(log(y+2)) + 2.9.\n- C0hat(2k+1) = 0.433·log(2k+3)+0.886·loglog(2k+3)+2.9. For k ≥ 11: 2k+3 ≤ 2.3k ⟺ 3 ≤ 0.3k ⟺ k ≥ 10 ✓. log(2k+3) ≤ log(2.3k) = log 2.3 + log k ≤ 0.8329 + log k (log 2.3 ≤ 0.8329: e^0.8329 ≥ 2.3? e^0.8329 ≈ 2.30000 ✓ — need care: e^0.8329 = ? e^0.8 = 2.22554, e^0.0329 = 1.03345: 2.22554·1.03345 = 2.30000 ✓ borderline — use 0.833). loglog(2k+3) ≤ log(log k + 0.833) ≤ loglog k + 0.833/log k ≤ loglog k + 0.833/log 11 = loglog k + 0.34743 (log 11 ≥ 2.3979: e^2.3979 ≥ 11 ✓). 0.833/2.3979 = 0.347388 ≤ 0.3475 ✓.\n- C0hat(j+1) = 0.433·log(j+3)+0.886·loglog(j+3)+2.9. For j ≥ 14: j+3 ≤ (17/14)·j ⟺ 3 ≤ (3/14)j ⟺ j ≥ 14 ✓. log(j+3) ≤ log j + log(17/14) ≤ log j + 0.1942 (log(17/14) ≤ 0.1942: e^0.1942 ≥ 17/14 = 1.21429: e^0.1942 = 1.21441 ✓). loglog(j+3) ≤ loglog j + 0.1942/log j ≤ loglog j + 0.1942/log 14 = loglog j + 0.073588 (log 14 ≥ 2.6391: e^2.6391 ≥ 14 ✓). 0.1942/2.6391 = 0.073586 ≤ 0.0736 ✓.\n- C0hat(2t+1) ≤ C0hat(t+1)+0.55 for t ≥ 10: diff = 0.433·log((2t+3)/(t+3)) + 0.886·[loglog(2t+3)−loglog(t+3)]. log((2t+3)/(t+3)) ≤ log 2 ≤ 0.6932 (2t+3 ≤ 2(t+3) ✓). loglog(2t+3)−loglog(t+3) ≤ log((log(t+3)+log 2)/log(t+3))·... = log(1+log2/log(t+3)) ≤ log 2/log(t+3) ≤ 0.6932/log 13 ≤ 0.6932/2.5649 = 0.270265·... = 0.27027. Diff ≤ 0.433·0.6932+0.886·0.27027 = 0.30016+0.23946 = 0.53962 ≤ 0.55 ✓.\n\nAll verified. Also S₃ terms verified earlier. Also the main left-side: for k ∈ (t−3, t]: left window empty — hmm wait, in the MERGED bucket approach, bucket k's left part: zeros with x ∈ [k, k+1), γ < t ⟹ γ ∈ (t−k−1, t−k]. For k ≤ t: t−k ≥ 0. For the count via ZeroCountProp at (t−k−1) need t−k−1 ≥ 2 ⟺ k ≤ t−3. For k ∈ (t−3, t]: window (t−k−1, t−k] ⊆ (−2-ish, 5]: zeros there have |γ| ≤ 5 < 14 ⟹ none by NoLowZeros ✓ (|γ| ≤ max(|t−k−1|, |t−k|) ≤ max(3, 5)... t−k−1 ∈ [−2, 2), t−k ∈ [0, 3] ⟹ γ ∈ (−2, 3] ⟹ |γ| < 14 ✓ empty). ✓\n\nBut actually — for the Lean proof of the main-fiber count, the cleanest statement: for bucket k ≤ t (as naturals: k ≤ ⌊t⌋), the fiber (zeros with ⌊x⌋ = k, x = |t−γ|) has mult-sum ≤ 2C₀+0.55. Proof: fiber ⊆ (zeroWindow (t+k) ∪ zeroWindow (t−k−1))-image... For ρ in the fiber with γ ≥ t: x = γ−t ∈ [k, k+1) ⟹ γ ∈ [t+k, t+k+1) ⊆ zeroWindow(t+k) ✓ (closed [t+k, t+k+1]). For γ < t: γ ∈ (t−k−1, t−k]: ⊆ zeroWindow(t−k−1) (closed). Then mult-sum ≤ count(t+k) + count(t−k−1) with:\n- count(t+k) ≤ C0hat(t+k+1) via hZC (t+k) (t+k ≥ 2 ✓) ≤ C0hat(2t+1) (mono, k ≤ t) ≤ C₀+0.55.\n- count(t−k−1): case k ≤ t−3: ≤ C0hat(t−k) ≤ C0hat(t) ≤ C0hat(t+1) = C₀ (mono). Case k > t−3: the window ⊆ (−14, 14) ⟹ EMPTY (NoLowZeros) ⟹ sum = 0 ≤ C₀ ✓. Hmm — but \"empty ⟹ sum = 0\" needs: every nontrivial zero in the window has |γ| < 14, contradicting NoLowZeros, so the toFinset sum = 0 ✓.\nSo fiber ≤ (C₀+0.55) + C₀ = 2C₀+0.55 ✓ uniformly.\n\nWait, one more check: C0hat(t−k) ≤ C0hat(t+1) needs C0hat monotone on the range: C0hat_mono — what's its exact form? It was used in LiGapCircles (\"C0hat_mono\"). Let me check its statement. Also `two_le_C0hat` exists. I'll grep C0hat_mono.\n\nAnd the MAIN bucket fiber map into the two windows: the mult-sum over the fiber finset ≤ mult-sum over zeroWindow-toFinsets via Finset.sum_le_sum_of_subset_of_nonneg + sum_union (disjoint: γ ≥ t vs γ < t... zeroWindow(t+k) has γ ≥ t+k ≥ t; zeroWindow(t−k−1) has γ ≤ t−k ≤ t−1 < t ✓ disjoint for k ≥ 1 ✓).\n\nFor the MAIN sum: the main zeros = far zeros with x ≤ t (hmm — x < t+1, i.e. k = ⌊x⌋ ≤ ⌊t⌋... let me define the main finset directly as far zeros with ⌊x⌋ ≤ K where K := ⌊t⌋₊... careful with Nat.floor of possibly... t ≥ 10 > 0 so ⌊t⌋₊ = natFloor fine). Actually simpler: main finset := nearZerosSub-complement intersect (finite ball): far zeros have x ≥ 1; main: x ≤ t. |γ| ≤ t+x ≤ 2t ⟹ finite ball finite_subtype_norm_lt (2t+1). So mainFinset t := (finite_subtype_norm_lt (2t+1)).toFinset.filter (fun ρ => 1 ≤ |ρ.1.im − t| ∧ |ρ.1.im − t| ≤ t). Then the tail zeros: far with x > t — split the tsum by mainFinset via tsum_split_finset(-complex? the g-function is ℝ-valued: use the ℝ tsum_split_finset from LiCircleBound — it's imported via LiSqueeze? LiTightR imports LiSqueeze which imports... LiCircleBound is root-imported separately. tsum_split_finset is in LiCircleBound (line 249) ✓ accessible since LiTightR imports LiSqueeze which imports LiCircleBound? Let me verify the import chain: LiSqueeze imports LiCircleBound presumably. LiTightR imports NguyenRH1.LiSqueeze — so LiCircleBound decls are available ✓ (tsum_split_finset was used in LiTightR? No — LiTightR defined its own tsum_split_finset_complex for ℂ. The ℝ one is tsum_split_finset ✓.)\n\n- The tail tsum (ℝ-valued, on the subtype): ∑' ρ, if ρ ∈ mainFinset then 0 else g ρ — split into right-tail (γ > 2t) and left-tail (γ < 0): zeros with x > t have γ > 2t or γ < 0 ✓ (x = |t−γ| > t ⟺ γ > 2t or γ < 0). Then TWO further tsum splits (by finiteness? NO — both are infinite families!). Splitting the tail tsum into right/left needs another finset split — but neither is finite. Use instead: ∑' g_tail = ∑' g_tailR + ∑' g_tailL where g_tailR ρ = if γ > 2t then g ρ else 0, g_tailL = if γ < 0 then g ρ else 0 — via Summable.tsum_add (both summable by of_norm_bounded from g) + tsum_congr (every tail zero: γ > 2t or γ < 0 exclusive ✓ — actually need: if x > t then exactly one holds: γ > 2t ∨ γ < 0, disjoint ✓; and g_tail ρ (x > t) = g ρ; for x ≤ t... wait — the tail function after the mainFinset split is h ρ = if ρ ∈ mainFinset then 0 else g ρ where mainFinset also requires x ≥ 1. Hmm — zeros with x < 1 are NEAR (excluded from g already — g has the nearZerosSub-if). Let me restructure cleanly:\n\nDefine g : subtype → ℝ, g ρ = if ρ ∈ nearZerosSub t then 0 else 4.5·(m:ℝ)/(x_ρ·sqrt(1+x_ρ²)) where x_ρ = |ρ.im − t|.\n- g ≥ 0 ✓, summable (dominated by C·m/(1+γ²) as computed — need the comparison lemma).\n- ‖far series‖ ≤ ∑' g (via: ‖∑' f‖ ≤ ∑' ‖f‖ and ‖f ρ‖ ≤ g ρ: norm bound of the tsum — Mathlib: `norm_tsum_le_tsum_norm`? For ℝ-valued: `Summable.norm_tsum_le`? There's `tsum_le_tsum_of_norm_le`? Let me recall: `norm_tsum_le_tsum_norm (hf : Summable (norm ∘ f)) : ‖∑' f‖ ≤ ∑' ‖f‖`? I believe `norm_tsum_le_tsum_norm` exists. Then ∑' ‖f‖ ≤ ∑' g by Summable.tsum_le_tsum (‖f ρ‖ ≤ g ρ pointwise, both summable) ✓.)\n\n- Split g's tsum: mainFinset covers far zeros with x ≤ t (and the membership condition includes x ≥ 1 automatically for far zeros — since g = 0 for near). Hmm — the if-zeroed split function: ∑' g = ∑_{mainFinset} g + ∑' (if ∉ mainFinset then g else 0). The second tsum: for ρ ∉ mainFinset: either near (g = 0 ✓) or x > t (g = g ρ). So ∑'₂ = ∑' (fun ρ => if x_ρ > t then g ρ else 0) — by tsum_congr (cases: near ⟹ both 0; far & x ≤ t ⟹ ∈ mainFinset ⟹ 0 = 0... wait need ρ ∈ mainFinset ⟺ (far ∧ x ≤ t): mainFinset def'd via the ball + 1 ≤ x ∧ x ≤ t. For ρ far (x ≥ 1) and x ≤ t: ball condition |γ| ≤ t+x ≤ 2t ⟹ ‖ρ‖ ≤ |re|+|im| ≤ 1+2t < 2t+1 ✓ mem ✓. For ρ ∉ mainFinset with g ρ ≠ 0: far (x ≥ 1) and (x > t or ‖ρ‖ ≥ 2t+1); ‖ρ‖ ≥ 2t+1 ⟹ |γ| ≥ ‖ρ‖−|re| ≥ 2t ⟹ x ≥ |γ|−t ≥ t — hmm boundary: x > t needed strictly. |γ| ≥ 2t ⟹ γ ≥ 2t or γ ≤ −2t ⟹ x = |t−γ| ≥ t ✓ but need x > t STRICT: γ > 2t gives x > t ✓; γ = 2t exactly: x = t — but then |γ| = 2t, ‖ρ‖ ≥ 2t+1 needs |re| ≥ 1 — |re| < 1 for nontrivial zeros (re ∈ (0,1)) — so ‖ρ‖ < 1+2t < 2t+1 ⟹ ρ with |γ| = 2t exactly IS in the ball ⟹ in mainFinset if far (x = t ≥ 1 ✓ and x ≤ t ✓). So ρ ∉ mainFinset with g ρ ≠ 0 ⟹ x > t ✓.)\n  Then ∑'₂ = ∑' (if x > t then g else 0) — and split into γ > 2t / γ < 0 via tsum_add as above ✓.\n\n- Right tail: ∑' (if γ > 2t then g else 0) ≤ Σ'_{k≥11} 4.5·C0hat(2k+1)/(k√(1+k²)) — via the ENNReal.tsum_fiberwise machine with bucket k(ρ) = ⌊x_ρ⌋₊ (Nat.floor), fibers for k ≥ 11 (ρ with γ > 2t: x > t ≥ 10 ⟹ k ≥ 10 — hmm ⌊x⌋ for x > 10: k ≥ 10; need k ≥ 11 for the brick sums! x > t ≥ 10: if t = 10.5, x > 10.5, k ≥ 10 — bucket k = 10 exists (x ∈ [10.5, 11)). The brick sums start at 11! Need care: right tail = γ > 2t ⟹ x > t. Buckets k = ⌊x⌋ ≥ ⌊t⌋₊. For the count bound C0hat(t+k+1) ≤ C0hat(2k+1) I need k ≥ t. k ≥ ⌊t⌋₊ — is ⌊t⌋₊ ≥ t? NO: ⌊t⌋₊ ≤ t. Bucket k = ⌊t⌋₊ has x ∈ [k, k+1) possibly with x < t (if t not integer): those zeros (x ∈ [⌊t⌋₊, t]) are in the MAIN range (x ≤ t) not the tail! But γ > 2t ⟹ x > t ⟹ x ≥ t > ⌊t⌋₊... x > t ≥ ⌊t⌋₊: if t = 10.5: x > 10.5 ⟹ ⌊x⌋₊ ≥ 10 — bucket 10 = x ∈ [10.5, 11): count window γ ∈ [t+10, t+11) ⊂ [20.5, 21.5): count ≤ C0hat(t+11) ≤ C0hat(2t+1)?? t+11 = 21.5, 2t+1 = 22 ✓ C0hat(t+11) ≤ C0hat(22) = C0hat(2t+1) ✓ — actually for bucket k = 10 = ⌊t⌋₊: window count ≤ C0hat(t+k+1) = C0hat(21.5) ≤ C0hat(2t+1) (t+k+1 = 21.5 ≤ 22 = 2t+1 ✓ — in general t+⌊t⌋₊+1 ≤ 2t+1 ⟺ ⌊t⌋₊ ≤ t ✓). So bucket ⌊t⌋₊ in the tail can ALSO use the C₀+0.55 rate! And for k ≥ ⌊t⌋₊+1 > t: C0hat(t+k+1) ≤ C0hat(2k+1) ⟺ t+k+1 ≤ 2k+1 ⟺ t ≤ k ✓.\n  \n  So the right tail (γ > 2t): buckets k ≥ ⌊t⌋₊ ≥ 10. Bucket ⌊t⌋₊: rate C0hat(2t+1) ≤ C₀+0.55. Buckets k > t: rate C0hat(2k+1) ≤ (brick form). For the BRICK SUMS (Σ_{k≥11}): buckets k ≥ 11 — since ⌊t⌋₊ ≥ 10, buckets k ∈ {⌊t⌋₊} ∪ {≥ 11}: the k = 10 bucket (when ⌊t⌋₊ = 10, i.e. t ∈ [10, 11)) uses C₀+0.55 — fold into the MAIN bound! I.e.:\n\n  RESTRUCTURE the split: main = far zeros with k(ρ) ≤ t (i.e. ⌊x⌋₊ ≤ ⌊t⌋₊... simpler: main = far with x ≤ t as before), tail = x > t. For the tail, buckets k(ρ) ≥ ⌊t⌋₊. Then:\n  Tail ≤ Σ_{k ≥ ⌊t⌋₊} rate_k·4.5·W(k) where rate_{⌊t⌋₊} ≤ C0hat(2t+1) ≤ C₀+0.55 (for the bucket part x ∈ [max(⌊t⌋₊, t), ⌊t⌋₊+1)) — hmm wait, bucket ⌊t⌋₊'s window is γ ∈ [t+⌊t⌋₊, t+⌊t⌋₊+1) and count ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) ✓.\n  ≤ (C₀+0.55)·4.5·W(⌊t⌋₊) + Σ_{k≥11} C0hat(2k+1)·4.5·W(k) [since buckets k > t are k ≥ ⌊t⌋₊+1 ≥ 11 ✓ and W(⌊t⌋₊) ≥ W(k) for k ≥ ⌊t⌋₊... hmm no — the fiberwise sum for buckets k ≥ 11 with rate ≤ C0hat(2k+1) and bucket ⌊t⌋₊ separate].\n  The (C₀+0.55)·4.5·W(⌊t⌋₊) term: W(⌊t⌋₊) ≤ W(10) = 1/(10√101) ≤ 0.09951·... = 1/(10·10.0499) = 0.099504·... Actually simpler: W(k) ≤ 1/k² ≤ 1/100. So this term ≤ (C₀+0.55)·4.5·0.01 = 0.045·C₀+0.02475. Fold into main: main' = main + this ≤ (2C₀+0.55)·4.5·S₃ + 0.045·C₀+0.02475. Hmm — 0.045·C₀ adds to the C₀-coefficient: 12.1284+0.045 = 12.1734·C₀. And constants: +0.02475.\n  \n  Hmm wait, actually — do I even need the bucket-⌊t⌋₊ separation? The tail buckets are k ≥ ⌊t⌋₊ ≥ 10 and the brick sums are k ≥ 11. If ⌊t⌋₊ ≥ 11 (t ≥ 11), all tail buckets are k ≥ 11 ✓ bricks apply directly. If ⌊t⌋₊ = 10 (t ∈ [10, 11)): one extra bucket k = 10 at rate C0hat(2t+1) ≤ C₀+0.55, weight W(10) ≤ 0.01·... Handle by: Tail ≤ Σ_{k≥11}-bricks + (if ⌊t⌋₊ = 10 then (C₀+0.55)·4.5·W(10) else 0) ≤ bricks + (C₀+0.55)·4.5·0.01.\n  \n  In the LEAN fiberwise machine, this case-split is annoying. ALTERNATIVE: make the tail bricks start at k ≥ 10 instead of 11!! Recompute bricks with Σ_{k≥10}: W₀ = Σ_{k≥10} 1/k² ≤ ∫₉^∞ = 1/9 = 0.11111; W₁ = Σ log k/k² ≤ (log 9+1)/9 = 0.35524; W₂ ≤ 0.3679·0.35524 = 0.13071. Tail_R ≤ 4.5·[0.433·(0.833·0.11111+0.35524)+0.886·(0.3475·0.11111+0.13071)+2.9·0.11111] = 4.5·[0.433·0.44780+0.886·0.16933+0.32222] = 4.5·[0.19390+0.15003+0.32222] = 4.5·0.66615 = 2.99768. And for k ≥ 10 the C0hat(2k+1)-bound needs 2k+3 ≤ 2.3k ⟺ k ≥ 10 ✓ STILL VALID. And the rate for bucket k ∈ tail: k ≥ ⌊t⌋₊ ≥ 10: hmm — but bucket ⌊t⌋₊ has rate C0hat(2t+1) vs C0hat(2k+1): at k = ⌊t⌋₊: 2k+1 = 2⌊t⌋₊+1 vs 2t+1: 2⌊t⌋₊+1 ≤ 2t+1 ✓ so C0hat(2k+1) ≤ C0hat(2t+1)!! So rate C0hat(2k+1) is VALID for bucket ⌊t⌋₊ too?? Wait — bucket ⌊t⌋₊'s true count ≤ C0hat(t+⌊t⌋₊+1) and t+⌊t⌋₊+1 ≤ 2⌊t⌋₊+2·... hmm: t+⌊t⌋₊+1 ≤ 2⌊t⌋₊+1 ⟺ t ≤ ⌊t⌋₊ FALSE. But C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) ✓ (t+⌊t⌋₊+1 ≤ 2t+1 ✓) and 2t+1 vs 2k+1 = 2⌊t⌋₊+1: 2t+1 ≥ 2⌊t⌋₊+1 — so C0hat(t+k+1) ≤ C0hat(2t+1) — and I want ≤ C0hat(2k+1) = C0hat(2⌊t⌋₊+1) which is SMALLER — NOT valid!! For bucket ⌊t⌋₊: count ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) but NOT ≤ C0hat(2⌊t⌋₊+1) (since t+⌊t⌋₊+1 > 2⌊t⌋₊+1). So bucket ⌊t⌋₊ genuinely needs the C₀+0.55 rate. UNLESS ⌊t⌋₊ ≥ 11.\n\n  Cleanest: handle bucket ⌊t⌋₊ separately ALWAYS (fold into main):\n  Tail ≤ (C₀+0.55)·4.5·W(⌊t⌋₊) + Σ_{k≥11} C0hat(2k+1)·4.5·W(k), with W(⌊t⌋₊) ≤ 1/⌊t⌋₊² ≤ 1/100.\n  Main' = main + bucket-⌊t⌋₊-share ≤ (2C₀+0.55)·4.5·S₃ + (C₀+0.55)·4.5·0.01 = (2C₀+0.55)·4.5·(S₃+0.005) ≤ (2C₀+0.55)·4.5·1.3526.\n  = 4.5·(2C₀+0.55)·1.3526 = 12.1734·C₀+0.55·6.0867 = 12.1734·C₀+3.34769.\n  Hmm — that adds 0.045·C₀ + 0.01175 to the constants. Then Piece3 ≤ 12.1734·C₀ + 3.34769 + 2.73393 + 1.17263 = 12.1734·C₀ + 7.25425.\n  Assembly: 12.1734·2.9658 = 36.098; total const = 1+2.7+36.098+7.2543+0.09+0.6 = 47.742 ≤ 48.568-ish ✓ margin still ~0.8. L-coeff: 12.1734·0.433+0.6 = 5.871; LL: 12.1734·0.886+0.886 = 11.672. f(L) = 11.672LL−4.629L, max at L = 11.672/4.629 = 2.5216: f = 11.672·0.92499−11.672 = −0.8747·... = 10.797−11.672 = −0.875. Need f ≤ 48−47.742 = 0.258: −0.875 ≤ 0.258 ✓ margin 1.13. OK.\n\n  Hmm, but actually — simpler alternative: bound W(⌊t⌋₊) ≤ W(10) and charge it to the TAIL bricks by extending them to k ≥ 10 with the C₀+0.55 rate for bucket 10?? No — cleaner as above: bucket ⌊t⌋₊ at rate C₀+0.55, weight ≤ 0.01, constant 0.045·C₀+0.02475. OR EVEN SIMPLER: charge bucket ⌊t⌋₊ at the SAME per-bucket rate as the main (2C₀+0.55)!! The bucket's true count: right part ≤ C0hat(2t+1) ≤ C₀+0.55; LEFT part (γ < t, x ∈ [⌊t⌋₊, ⌊t⌋₊+1) ⟹ γ ∈ (t−⌊t⌋₊−1, t−⌊t⌋₊] ⊆ (−1, 1]-ish ⟹ |γ| ≤ 2 < 14 ⟹ EMPTY by NoLowZeros ✓ — wait: x > t for the tail, so left part γ = t−x < 0, |γ| = x−t ∈ [⌊t⌋₊−t, ⌊t⌋₊+1−t) ⊆ [0, 1) ⟹ |γ| < 1 < 14 ✓ EMPTY). So bucket ⌊t⌋₊ count ≤ C₀+0.55 + 0 ≤ 2C₀+0.55 ✓ (the uniform main rate!). So actually bucket ⌊t⌋₊ IS a main bucket in disguise: its left part is empty and right part ≤ C₀+0.55.\n\n  ⟹ SIMPLEST UNIFORM TREATMENT: buckets k = 1..∞; for k ≤ t: rate 2C₀+0.55 (right ≤ C0hat(2t+1), left ≤ C₀ or empty); for k > t (⟹ k ≥ 11): rate C0hat(2k+1)+C0hat-conj-left... \n\n  hmm wait, for k > t the LEFT part: γ ∈ (t−k−1, t−k] ⊂ negatives with |γ| ∈ [k−t, k−t+1): conj-count ≤ C0hat(k−t+1). And I bounded left-tail separately with the ℓ = ⌊|γ|⌋ indexing and the sharper (10+ℓ)² weight. In the k-bucket view, left-tail in bucket k has weight W(k) = 1/(k√(1+k²)) ≤ 1/k² where k = ⌊x⌋ ≥ t+ℓ-ish... The left-tail ℓ-buckets: ℓ = ⌊|γ|⌋, weight 1/(t+ℓ)² ≤ 1/(10+ℓ)². The k-bucket = ⌊x⌋ = ⌊t+|γ|⌋ ≥ ⌊t⌋₊+ℓ-ish ≥ 10+ℓ ⟹ W(k) ≤ 1/(10+ℓ)²-ish ✓ consistent. The ℓ-indexing is cleaner for the left tail (fixed family ℓ ≥ 14). KEEP the left/right tail split as planned.\n\n  So the tail machine:\n  - Right tail (γ > 2t): bucket k(ρ) = ⌊x⌋₊ ≥ ⌊t⌋₊ ≥ 10. Sub-split: bucket ⌊t⌋₊ (rate ≤ C₀+0.55+0, weight ≤ W(10) ≤ 0.01... hmm — as part of the fiberwise tsum machine, the buckets are k ≥ ⌊t⌋₊ — a t-dependent start. The ENNReal.tsum_fiberwise sums over ALL buckets: for k < ⌊t⌋₊ the fiber is EMPTY (contributes 0 ✓ automatically!). So the fiberwise machine runs over k ∈ ℕ with fiber_k = {γ > 2t ∧ ⌊x⌋₊ = k}: empty for k < ⌊t⌋₊ ✓. Then the per-bucket bound: cnt(k)·W(k) where cnt(k) = 0 for k < ⌊t⌋₊... — the cleanest: bound the bucket sum ≤ Σ_{k} cnt(k)·4.5·W(k) with cnt(k) ≤ rate(k) and then bound the SERIES Σ rate·W by splitting the series at 11: Σ_{k<11} + Σ_{k≥11}: the k < 11 part: only k = 10 (= ⌊t⌋₊ when t < 11) can be nonempty; rate(10) ≤ C₀+0.55; weight 4.5·W(10) ≤ 4.5·0.01 = 0.045. So the k<11 part ≤ (C₀+0.55)·0.045·(indicator) ≤ (C₀+0.55)·0.045. In Lean: Σ_{k ∈ range 11} rate(k)·4.5·W(k) ≤ (C₀+0.55)·4.5·0.01: prove by showing all terms except k = 10 vanish (cnt(k) = 0 for k < 10 since ⌊t⌋₊ ≥ 10 — hmm, and for k < 10: empty ✓) and for k = 10: rate·W ≤ (C₀+0.55)·0.01. This is a finite sum of 11 terms with most zero — doable but fiddly. ALTERNATIVE clean bound: Σ_{k<11} cnt(k)·4.5·W(k) ≤ 4.5·W(1)·Σ_{k<11} cnt(k) — no, W(1) big. Hmm: ≤ 4.5·(Σ_{k<11} cnt(k))·W(10)·... W decreasing: Σ_{k≤10} cnt(k)W(k) ≤ W(1)·cnt... no. Simplest: Σ_{k<11} cnt(k)·4.5·W(k) ≤ 4.5·(Σ_{k<11} cnt(k))·max... Actually — Σ_{k<11} cnt(k) = total tail zeros in buckets ≤ 10 = zeros with γ > 2t and x < 11: γ ∈ (2t, t+11): count ≤ C0hat(t+11)·11-chained?? no — single window-ish: γ ∈ (2t, t+11) ⊂ (t, t+11): Ncount ≤ 11·C0hat(t+11)-ish — NO, too big (11·C₀·4.5·0.01·... = 0.5·C₀ — hmm actually that's not terrible: 4.5·0.01·11·C0hat(t+11)·... no wait: Σ_{k<11} cnt(k)·4.5·W(k) ≤ 4.5·W(10)·Σ_{k<11}·... W(k) ≤ W(10) only for k ≥ 10; for k < 10 the fibers are EMPTY ⟹ cnt(k) = 0 ✓!! So Σ_{k<11} cnt(k)W(k) = cnt(10)·W(10) ≤ (C₀+0.55)·0.01·... wait cnt(10) ≤ C₀+0.55 and W(10) ≤ 1/100 ✓: ≤ (C₀+0.55)·4.5/100 = 0.045·C₀+0.02475 ✓ as computed. The Lean proof: the fiberwise bucket-sum = Σ_{k} cnt'(k)·W(k) as a TSUM (not finite sum!) — the fiberwise machine gives ∑'_{k:ℕ} (fiber-bound). Bound the tsum: ∑' ≤ Σ_{k∈range 11} + ∑'_{k≥11}: via Summable.sum_add_tsum_nat_add on the majorant ✓. The range-11 part: show the summand ≤ if k = 10 then (C₀+0.55)·4.5·0.01 else 0 — per-bucket: cnt(k)·4.5·W(k) with cnt(k) ≤ (if k = 10 then C₀+0.55 else 0) for k < 11: k < 10 ⟹ fiber empty ⟹ cnt(k) = 0 ✓; k = 10 ⟹ cnt ≤ C₀+0.55 (or 0 if ⌊t⌋₊ > 10) ✓ either way. Then Σ_{range 11} ≤ (C₀+0.55)·4.5·0.01·... — finite sum with single nonzero-ish term: bound by Finset.sum_le_sum with per-term bounds + sum_eq_single-ish. Doable.\n\n  Hmm OK wait, this is getting really involved. Let me simplify by choosing a cleaner threshold: make the tail start at x > ⌈t⌉₊ instead (buckets k ≥ ⌈t⌉₊ ≥ 10... same issue at k = 10 = ⌈t⌉ when t ∈ [10,11)).\n  \n  You know what — actually the CLEANEST fix: prove the tail bricks for k ≥ 10 (not 11)!! Bricks: W₀' = Σ_{k≥10} 1/k² ≤ 1/9 (0.11112), W₁' ≤ 0.3553, W₂' ≤ 0.3679·0.3553 = 0.13077. And the C0hat(2k+1)-form for k ≥ 10 ✓ valid. Then the tail machine: buckets k ≥ ⌊t⌋₊ ≥ 10 all get rate... — but bucket ⌊t⌋₊ can't use C0hat(2k+1)!! ARGH. \n\n  Hmm hmm. OK actually — wait. Reconsider: bucket ⌊t⌋₊ in the tail has x ∈ (t, ⌊t⌋₊+1) (only the part above t). Its window: γ ∈ (2t, t+⌊t⌋₊+1). The count: zeroWindow(2t)-ish... the window [2t, t+⌊t⌋₊+1] has length ⌊t⌋₊+1−t ≤ 1: ⊆ zeroWindow(2t) ∪ zeroWindow(t+⌊t⌋₊)... ⊂ [2t, 2t+1] ∪ [t+⌊t⌋₊, t+⌊t⌋₊+1]: count ≤ C0hat(2t+1)+C0hat(t+⌊t⌋₊+1) ≤ 2·C0hat(2t+1) ≤ 2(C₀+0.55)·... hmm 2C₀+1.1 — worse. OR: [2t, t+⌊t⌋₊+1] ⊆ [2t, 2t+2): count ≤ N(2t, 2t+2] ≤ 2 windows... The cleanest: count ≤ C0hat(2t+1) + C0hat(2t+2)?? no...\n  \n  Actually simplest: [2t, t+⌊t⌋₊+1] ⊆ [2t, 2t+2] — but ZeroCountProp is per-UNIT-window: [2t, 2t+1] ≤ C0hat(2t+1), [2t+1, 2t+2] ≤ C0hat(2t+2) ≤ C0hat(2t+1)+small. Total ≤ 2C0hat(2t+2) ≤ 2(C₀+0.55+0.03)... ≈ 2C₀+1.16. That's a big rate for one bucket: 2C₀·4.5·0.01 = 0.09·C₀ — adds 0.09·C₀+0.05 to constants: C₀-coeff → 12.1284+0.09 = 12.22. Hmm.\n\n  vs the earlier approach (bucket ⌊t⌋₊ at C₀+0.55 rate, since left-empty + right-window ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1)): adds only 0.045·C₀+0.02475. The earlier approach is better AND correct: bucket ⌊t⌋₊ zeros: γ ∈ (2t, t+⌊t⌋₊+1) — RIGHT side only (γ > t ✓), so the \"right part\" count = zeros in [2t, t+⌊t⌋₊+1) ⊆ [t+⌊t⌋₊, t+⌊t⌋₊+1]?? NO: 2t vs t+⌊t⌋₊: 2t ≥ t+⌊t⌋₊ ⟺ t ≥ ⌊t⌋₊ ✓. So [2t, t+⌊t⌋₊+1) ⊆ [t+⌊t⌋₊, t+⌊t⌋₊+1] = zeroWindow(t+⌊t⌋₊) ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) ≤ C₀+0.55 ✓✓. So bucket ⌊t⌋₊ ≤ C₀+0.55 with NO left part (γ > 2t > t ✓). GREAT — so bucket ⌊t⌋₊ rate = C₀+0.55 exactly as I said. \n\n  So RIGHT TAIL machine: fiberwise over k ∈ ℕ, fiber_k = {γ > 2t, ⌊x⌋₊ = k}; cnt(k) ≤ C0hat(t+k+1) for ALL k (bucket k nonempty ⟹ window [t+k, t+k+1] — wait, bucket k = ⌊x⌋₊: x ∈ [k, k+1) ⟹ γ = t+x ∈ [t+k, t+k+1) ✓ ⊆ zeroWindow(t+k) ✓ ≤ C0hat(t+k+1) via hZC (t+k ≥ 2 ✓) — VALID FOR ALL k ✓!!). Then the series Σ_k C0hat(t+k+1)·4.5·W(k): for k ≤ t: C0hat(t+k+1) ≤ C0hat(2t+1) ≤ C₀+0.55; for k > t: C0hat(t+k+1) ≤ C0hat(2k+1). And fibers empty for k < ⌊t⌋₊ — but I can just use the crude bound anyway (the series bound overestimates): Σ_k ≤ Σ_{k<11} (C₀+0.55)·4.5·W(k)·[k ≤ t-bound — hmm for k < 11 the rate C0hat(t+k+1) ≤ C0hat(2t+1) needs k ≤ t — for k ≤ 10 ≤ t ✓ (t ≥ 10)]. So:\n  Σ_k C0hat(t+k+1)·4.5·W(k) ≤ Σ_{k=1}^{10} (C₀+0.55)·4.5·W(k) + Σ_{k≥11} C0hat(2k+1)·4.5·W(k)\n  ≤ (C₀+0.55)·4.5·S_{≤10} + Tail_R\n  where S_{≤10} = Σ_{k=1}^{10} W(k) ≤ S₃ ≤ 1.3476.\n  \n  WAIT — but this is for the right tail only (γ > 2t). And the MAIN range uses buckets k ≤ t for BOTH sides. There's OVERLAP: the main sum covers x ≤ t (k ≤ ⌊t⌋₊... x ≤ t ⟹ k = ⌊x⌋₊ ≤ ⌊t⌋₊ ≤ t ✓) and the right tail covers γ > 2t (x > t). The right-tail series bound I just wrote sums over ALL k (1..∞) — overestimating since buckets k < ⌊t⌋₊ are empty in the tail. That's FINE for an upper bound but it double-charges nothing (it's a bound on the TAIL sum only). Hmm, but it's LOSSY: Σ_{k=1}^{10} (C₀+0.55)·4.5·W(k) ≈ (C₀+0.55)·4.5·1.27 ≈ 5.7·C₀+1.6 — HUGE (the fibers are empty but I'm charging full rate). NO GOOD.\n\n  So the fiberwise machine must respect that tail fibers with k < ⌊t⌋₊ are empty: cnt(k) = 0 for k < ⌊t⌋₊. In the series bound: Σ_{k≥⌊t⌋₊} C0hat(t+k+1)·4.5·W(k) — and I split at 11: Σ_{k=⌊t⌋₊}^{10} (empty unless ⌊t⌋₊ = 10) + Σ_{k≥11}. The first part: k = ⌊t⌋₊ = 10 (if t < 11): (C₀+0.55)·4.5·W(10) ≤ (C₀+0.55)·4.5·0.01 = 0.045·C₀+0.02475. In Lean: Σ_{k≥⌊t⌋₊} ... = ∑' over k of (cnt-bound)·W — the fiberwise machine gives a per-bucket bound F(k) := C0hat(t+k+1)·4.5·W(k) for k ≥ ⌊t⌋₊ and 0 else — encode as: F(k) = if k < ⌊t⌋₊ then 0 else C0hat(t+k+1)·4.5·W(k)?? NO — the per-fiber bound is ≤ cnt(k)·W(k)·4.5 with cnt(k) = 0 for k < ⌊t⌋₊. So define the majorant G(k) := if ⌊t⌋₊ ≤ k then C0hat(t+k+1)·4.5·W(k) else 0. Summable (≤ C·something). Then ∑' G = ∑'_{k ≥ 11-part} + finite part: split via sum_add_tsum_nat_add at 11: Σ_{k ∈ range 11} G(k) + ∑'_{k} G(k+11). Range part: G(k) = 0 for k < ⌊t⌋₊, and for k = 10 (= ⌊t⌋₊ when t < 11): G(10) = C0hat(t+11)·4.5·W(10) ≤ (C₀+0.55)·4.5·0.01. So Σ_{range 11} G ≤ (C₀+0.55)·0.045 (a finite sum where each term ≤ the k=10-bound·δ_{k,10}: Finset.sum_le_sum + sum_eq_single 10-ish or bound each: G(k) ≤ (C₀+0.55)·4.5·0.01·(if k = 10 then 1 else 0)... — hmm, cleanest: show ∀ k ∈ range 11, G(k) ≤ (C₀+0.55)·4.5·(if k = 10 then W(10) else 0) then sum ≤ (C₀+0.55)·4.5·W(10) via sum_le_sum + sum_ite_eq'... fine, fiddly but OK.\n  Tail part: ∑'_{k} G(k+11) = ∑' C0hat(t+k+12)·4.5·W(k+11) (k+11 ≥ 11 > t... wait k+11 > t needs t < 11+k ✓ t could be ≥ 11+k!! For t = 20: bucket k = 15 ≤ t = 20 has rate C0hat(t+16) ≤ C0hat(41) vs C0hat(2·15+1) = C0hat(31) — C0hat(2k+1) NOT valid for k ≤ t!!). ARGH — the k > t condition: for the tail buckets k ≥ ⌊t⌋₊, and k > t ⟺ k ≥ ⌊t⌋₊+1... no: k > t ⟺ k ≥ ⌈t⌉ (k integer). ⌊t⌋₊ < t (non-integer t): bucket ⌊t⌋₊+1 ≥ ... is ⌊t⌋₊+1 > t ✓ yes (⌊t⌋₊+1 > t always). So tail buckets: k = ⌊t⌋₊ (rate C0hat(t+k+1) ≤ C0hat(2t+1)) and k ≥ ⌊t⌋₊+1 (rate ≤ C0hat(2k+1) ✓ since t < ⌊t⌋₊+1 ≤ k). So for the ∑'_{k≥11} part: buckets k ≥ 11: if t < 11 then k ≥ 11 > t ✓ rate C0hat(2k+1) ✓. If t ≥ 11: buckets k ∈ [11, t]?? — those buckets are EMPTY (tail starts at ⌊t⌋₊ ≥ 11) ⟹ cnt = 0 ✓ and my majorant G(k) = 0 there ✓ automatically! So ∑'_{k≥11} G(k) = ∑' (if ⌊t⌋₊ ≤ k then C0hat(t+k+1)·4.5·W(k) else 0) over k ≥ 11 — for the nonzero terms k ≥ ⌊t⌋₊ ≥ 11... wait if t ≥ 11, nonzero terms are k ≥ ⌊t⌋₊ and rate C0hat(t+k+1) ≤ C0hat(2k+1)?? k ≥ ⌊t⌋₊+1 > t for the rate — but k = ⌊t⌋₊ has rate C0hat(2t+1) NOT ≤ C0hat(2k+1)!! For t ≥ 11, bucket ⌊t⌋₊ ≥ 11 sits in the k≥11 tail-sum with rate C0hat(2t+1) which is NOT ≤ C0hat(2⌊t⌋₊+1). ARGH ARGH.\n\n  OK so the k ≥ 11 tail part needs: G(k) ≤ C0hat(2k+1)·4.5·W(k) + (extra for k = ⌊t⌋₊ if ≥ 11). The extra: C0hat(2t+1)·4.5·W(⌊t⌋₊) ≤ (C₀+0.55)·4.5·W(11)·... ≤ (C₀+0.55)·4.5·(1/121) = 0.0372·C₀+0.02045. So: G(k) ≤ C0hat(2k+1)·4.5·W(k) + (if k = ⌊t⌋₊ then (C₀+0.55)·4.5·W(11) else 0) for k ≥ 11. Then ∑'_{k≥11} G ≤ Tail_R + (C₀+0.55)·4.5/121.\n  Combined with the range-11 part (≤ (C₀+0.55)·4.5·0.01 when ⌊t⌋₊ = 10, else 0 — and when t ≥ 11 the range part is 0 but the bucket-⌊t⌋₊ extra appears in the k≥11 part): uniform bound: RIGHT TAIL ≤ Tail_R + (C₀+0.55)·4.5·0.01 (since 1/100 ≥ 1/121, the k=10 case bound covers: use W ≤ 0.01 for both).\n\n  Hmm wait — cleaner: handle bucket ⌊t⌋₊ ALWAYS as part of the MAIN sum!! Main = far zeros with x ≤ ⌊t⌋₊+1?? — no: main = far zeros with ⌊x⌋₊ ≤ ⌊t⌋₊ (buckets 1..⌊t⌋₊), tail = ⌊x⌋₊ ≥ ⌊t⌋₊+1 (buckets > t ✓ rate C0hat(2k+1) ✓✓). Main bucket ⌊t⌋₊ = x ∈ [⌊t⌋₊, ⌊t⌋₊+1): RIGHT part γ ∈ [t+⌊t⌋₊, t+⌊t⌋₊+1): count ≤ C0hat(t+⌊t⌋₊+1) ≤ C0hat(2t+1) ≤ C₀+0.55 ✓; LEFT part γ ∈ (t−⌊t⌋₊−1, t−⌊t⌋₊]: t−⌊t⌋₊ ∈ [0, 1]: zeros with γ ∈ (−1, 1]-ish: |γ| ≤ 2 < 14 ⟹ EMPTY by NoLowZeros ✓. So bucket ⌊t⌋₊ ≤ C₀+0.55+0 ≤ 2C₀+0.55 ✓ THE UNIFORM MAIN RATE ✓✓.\n  And the main buckets k < ⌊t⌋₊: x ∈ [k, k+1) with k+1 ≤ ⌊t⌋₊ ≤ t: left part γ ∈ (t−k−1, t−k] with t−k−1 ≥ t−⌊t⌋₊ ≥ 0 — for k ≤ t−3 the count ≤ C₀; for k ∈ (t−3, t]: t−k ∈ [0, 3): |γ| ≤ max(t−k, |t−k−1|) ≤ 4 < 14 ⟹ empty ✓. ✓ uniform rate 2C₀+0.55 for ALL main buckets ✓.\n  \n  So CLEAN FINAL SPLIT:\n  - MAIN: far zeros with k(ρ) := ⌊x⌋₊ ≤ ⌊t⌋₊ (buckets 1..⌊t⌋₊ — a FINITE bucket family for fixed t, but the zero set is finite anyway (ball |γ| ≤ 2t+1-ish)). Main ≤ Σ_{k=1}^{⌊t⌋₊} (2C₀+0.55)·4.5·W(k) ≤ (2C₀+0.55)·4.5·S₃.\n    As a FINSET sum: mainFinset := far zeros with ⌊x⌋₊ ≤ ⌊t⌋₊ (finite: |γ| ≤ t+x ≤ t+⌊t⌋₊+1 ≤ 2t+1 ⟹ ball). Group via the dyadic_family_le-pattern (unit_family_le with weight W(k), cnt(k) = 2C₀+0.55 constant!) into Σ_{k ∈ Ico 1 (⌊t⌋₊+1)} W(k)·(2C₀+0.55)·4.5 ≤ (2C₀+0.55)·4.5·S₃ — the bucket-index sum ≤ S₃ via: Σ_{k ∈ Ico 1 (K+1)} W(k) ≤ Σ_{k=1..4} + Σ_{k=5}^{K} ≤ 1.09756 + Σ_{k≥5}1/(k(k−1))·... — the finite tail Σ_{k=5}^{K} 1/(k(k−1)) = 1/4 − 1/K ≤ 1/4 ✓ (finite telescope: Finset.sum Ico — sum_range_sub pattern). So main ≤ (2C₀+0.55)·4.5·1.3476 ✓.\n  - RIGHT TAIL: far zeros with γ > t and k(ρ) ≥ ⌊t⌋₊+1: — hmm wait, the tail split: tail = far with k(ρ) ≥ ⌊t⌋₊+1. These have x ≥ ⌊t⌋₊+1 > t ⟹ γ > 2t or γ < 0. Right tail = tail ∩ {γ > t} (i.e. γ > 2t): bucket k ≥ ⌊t⌋₊+1 > t ✓ rate C0hat(t+k+1) ≤ C0hat(2k+1) ✓ (k > t ✓✓ — k ≥ ⌊t⌋₊+1 > t ✓). Bucket family k ≥ 11 (⌊t⌋₊+1 ≥ 11 ✓). Fiberwise tsum machine over k ∈ ℕ (fibers empty for k ≤ ⌊t⌋₊): majorant F(k) = if ⌊t⌋₊ < k then C0hat(2k+1)·4.5·W(k) else 0. ∑' F ≤ Σ_{k≥11} C0hat(2k+1)·4.5·W(k) = Tail_R ✓ (the if-kills make the k<11 terms 0, and for k ≥ 11 > ... the bound C0hat(t+k+1) ≤ C0hat(2k+1) needs t < k — for nonzero terms k > ⌊t⌋₊ ⟹ k ≥ ⌊t⌋₊+1 > t ✓✓).\n    Hmm wait — subtlety: F(k) = if ⌊t⌋₊ < k then C0hat(2k+1)·4.5·W(k) else 0 — for k = 11 > ⌊t⌋₊ (t < 11): C0hat(2·11+1) = C0hat(23) — the bucket count C0hat(t+12) ≤ C0hat(23) ⟺ t+12 ≤ 23 ⟺ t ≤ 11 ✓ (t < 11 since ⌊t⌋₊ < 11). ✓ good.\n    Then ∑' F ≤ ∑' (fun k => C0hat(2k+1)·4.5·W(k)·(if 11 ≤ k then 1 else 0)) — the brick sum: = 4.5·Σ_{k≥11} C0hat(2k+1)·W(k) ≤ 4.5·[0.433·(0.833·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀] with the bricks W₀/1/2 (Σ over k ≥ 11 of 1/k², log k/k², loglog k/k²) — note: W(k) = 1/(k√(1+k²)) ≤ 1/k² and log-parts similar. The brick W(k)·C0hat(2k+1) ≤ [0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9]/k² — summable ✓ (each piece summable via the antitone-integral machines). ✓\n  - LEFT TAIL: tail ∩ {γ < t} — γ < 0 actually (tail x > t, γ < t ⟹ γ < 0): bucket ℓ(ρ) := ⌊|γ|⌋₊ ≥ 14 (NoLowZeros: |γ| ≥ 14 ⟹ ℓ ≥ 14 ✓). Weight: x = t+|γ| ≥ t+ℓ ⟹ g(ρ) ≤ 4.5·m/((t+ℓ)√(1+(t+ℓ)²)) ≤ 4.5·m/(t+ℓ)² ≤ 4.5·m/(10+ℓ)². Count fiber ℓ: zeros with ⌊|γ|⌋₊ = ℓ, γ < 0 ⟹ |γ| ∈ [ℓ, ℓ+1) ⟹ conj ∈ zeroWindow(ℓ)... wait conj(ρ) has im = −γ = |γ| ∈ [ℓ, ℓ+1) ⊆ zeroWindow(ℓ) (closed [ℓ, ℓ+1]) ✓ ℓ ≥ 14 ≥ 2 ✓ ≤ C0hat(ℓ+1) ✓. Fiberwise tsum machine over ℓ ∈ ℕ (fibers empty for ℓ < 14): majorant F'(ℓ) = if 14 ≤ ℓ then C0hat(ℓ+1)·4.5/(10+ℓ)² else 0. ∑' F' ≤ 4.5·Σ_{ℓ≥14} [0.433·(log ℓ+0.1942)+0.886·(loglog ℓ+0.0736)+2.9]/(10+ℓ)² = Tail_L ≤ 4.5·[0.433·(0.1942·A₀+A₁)+0.886·(0.0736·A₀+A₂)+2.9·A₀] ✓ with bricks A₀/1/2 over ℓ ≥ 14 weights 1/(10+ℓ)², log ℓ/(10+ℓ)², loglog ℓ/(10+ℓ)² ✓.\n\n  TOTALS (final): Piece3 ≤ (2C₀+0.55)·4.5·1.3476 + 4.5·0.60754 + 4.5·0.260584\n  = 12.1284·C₀ + 3.33594 + 2.73393 + 1.17263 = 12.1284·C₀ + 7.2425. ✓ (as computed).\n\nNow, the MAIN bucket-family grouping: the mainFinset is finite; buckets k = 1..⌊t⌋₊; use the unit_family_le (dyadic_family_le generalized): with constant cnt — actually dyadic_family_le has the weight form C₁/2^j baked in. I need weight W(k) = 1/(k√(1+k²)) and cnt(k) = 2C₀+0.55. Let me write a generalized `unit_family_le`:\n```\nlemma unit_family_le (FS : Finset ZSubtype) (j : ZSubtype → ℕ) (K : ℕ)\n    (g : ZSubtype → ℝ) (W : ℕ → ℝ) (cnt : ℕ → ℝ)\n    (hW : ∀ k, 0 ≤ W k)\n    (hj : ∀ ρ ∈ FS, 1 ≤ j ρ ∧ j ρ ≤ K)\n    (hterm : ∀ ρ ∈ FS, g ρ ≤ W (j ρ) * (zeroMult ρ : ℝ))\n    (hcount : ∀ k, ∑ ρ ∈ FS.filter (j · = k), (zeroMult ρ : ℝ) ≤ cnt k) :\n    ∑ ρ ∈ FS, g ρ ≤ ∑ k ∈ Ico 1 (K+1), W k * cnt k\n```\n— a direct clone of dyadic_family_le with W instead of C₁/2^j. Then main: cnt k = 2C₀+0.55 const; Σ W·cnt = (2C₀+0.55)·Σ_{Ico 1 (K+1)} W ≤ (2C₀+0.55)·1.3476.\n\nFor the main bucket count (per bucket k ≤ ⌊t⌋₊ ≤ t): the fiber filter sum ≤ 2C₀+0.55 — via the two-window image bridge (like fiber_mult_count / near_sum_refPoint_le patterns).\n\nAnd the tail machines: clone `fiber_tail_le` + `zero_tail_inv_sq_le`'s ENNReal assembly.\n\nPlus the g-summability + norm reduction + the x > t ∨ structure splits.\n\nOK. This is a LOT. Let me organize the work into Lean sections and start writing. Estimated sections:\n\n§9 (piece 3a): real weight + numeric bricks\n- farW (k : ℕ) : ℝ := 1/(k·√(1+k²)) — actually index from k ≥ 1: use (k:ℝ) with k : ℕ.\n- farW_nonneg, farW_anti (monotone decreasing in k).\n- S₃ bricks: the four exact terms + telescope: `farW_sum_four` (Σ_{k=1..4} farW ≤ 1.09756), `farW_tail_five` (Σ'_{k≥5} farW ≤ 1/4 — hmm: Σ over ℕ of farW(k+5) ≤ Σ 1/((k+5)(k+4)) = 1/4), `farW_tsum_le` (Σ'_{k≥1} farW k ≤ 1.3476). And the finite-Ico version for the main: `farW_Ico_le` (Σ_{k ∈ Ico 1 (K+1)} farW k ≤ 1.3476).\n- RW bricks: `one_div_sq_tail_le` (Σ'_{k≥11} 1/k² ≤ 0.1 — hmm actually Σ over n of 1/(n+11)²), `log_div_sq_tail_le` (≤ 0.3303), `loglog_div_sq_tail_le` (≤ 0.3679·0.3303 — via the loglog ≤ log/e trick — actually just bound pointwise loglog k ≤ 0.3679·log k then tsum_le_tsum).\n- LA bricks: `one_div_add_sq_tail_le` (Σ_{j≥14} 1/(j+10)² ≤ 1/23), `log_div_add_sq_tail_le` (≤ 0.1687), `loglog_div_add_sq_tail_le` (≤ 0.3679·0.1687 ≤ 0.06207 — pointwise again).\n- The certified numerics: log 2 ≤ 0.6932 (have: Real.log_two_lt_d9 used in dirichletC2_le_one ✓), log 10 ≤ 2.3026, log 13 ≤ 2.565, log(23/13) ≤ 0.571, log(17/14) ≤ 0.1942, log 2.3 ≤ 0.833, log 11 ≥ 2.3979, log 14 ≥ 2.6391, 1/e ≤ 0.3679, loglog-bounds via the u/e trick (no new constants needed), sqrt bounds (1.414, 2.23, 3.16, 4.123).\n\n§10 (piece 3b): C0hat bridges\n- `C0hat_two_mul_add_one_le` (k : ℕ, 10 ≤ k): C0hat(2k+1) ≤ 0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9.\n- `C0hat_add_one_le_of_fourteen_le` (j ≥ 14): C0hat(j+1) ≤ 0.433·(log j+0.1942)+0.886·(loglog j+0.0736)+2.9.\n- `C0hat_two_t_add_one_le` (t ≥ 10): C0hat(2t+1) ≤ C0hat(t+1)+0.55.\n- (C0hat_mono exists? check.)\n\n§11 (piece 3c): the far-series machine\n- farG (the ℝ-valued g), farG_nonneg, farG_summable.\n- per-term bound: ‖seriesDiffTerm s s₀ ρ‖ ≤ farG-term for ρ far (needs s.im = t, s₀ = 2+tI, s.re ∈ [−5/2, 3], ζ s ≠ 0 ⟹ s ≠ ρ).\n- norm reduction: ‖∑' far-series‖ ≤ ∑' farG.\n- mainFinset + unit_family_le + per-bucket count (two-window bridge + NoLowZeros emptiness) ⟹ main ≤ (2C₀+0.55)·4.5·1.3476.\n- right tail machine (ENNReal fiberwise) ⟹ ≤ Tail_R-part.\n- left tail machine ⟹ ≤ Tail_L-part.\n- assembly: `far_series_le`.\n\nThat's a big build. Let me start with §9 (piece 3a — the numeric bricks). Actually — to keep commits clean per the sub-stage rule, I'll do 3a first (numeric bricks, self-contained), commit, then 3b, commit, then 3c.\n\nLet me check C0hat_mono's exact form first, plus what Real.log lemmas exist (log_two_lt_d9 was used). And check `Real.le_sqrt` signature. Let me grep quickly.","signature":""},{"type":"text","text":"I have the full picture now. Let me verify a few helper lemmas exist (C0hat_mono, Real.le_sqrt) and check the venv for numeric verification of my planned constants."},{"type":"tool_use","id":"Grep_26","name":"Grep","input":{"pattern":"C0hat_mono|theorem.*C0hat.*mono|lemma.*C0hat","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1","output_mode":"content","-n":true,"head_limit":15},"extra_content":null},{"type":"tool_use","id":"Bash_27","name":"Bash","input":{"command":"./.venv/Scripts/python.exe -c \"\nimport mpmath as mp\nmp.mp.dps = 30\n# verify piece-3 constants\nS3_terms = [1/(1*mp.sqrt(2)), 1/(2*mp.sqrt(5)), 1/(3*mp.sqrt(10)), 1/(4*mp.sqrt(17))]\nprint('S3 4 exact terms:', [mp.nstr(x,10) for x in S3_terms], 'sum', mp.nstr(sum(S3_terms),10))\nprint('S3 bound 1.3476: sum4+1/4 =', mp.nstr(sum(S3_terms)+mp.mpf(1)/4, 10))\nprint('rational sqrt lbs ok:', mp.sqrt(2) >= mp.mpf('1.414'), mp.sqrt(5) >= mp.mpf('2.23'), mp.sqrt(10) >= mp.mpf('3.16'), mp.sqrt(17) >= mp.mpf('4.123'))\nprint('  exact-term bounds:', 1/mp.mpf('1.414'), 1/(2*mp.mpf('2.23')), 1/(3*mp.mpf('3.16')), 1/(4*mp.mpf('4.123')))\nprint('  sum of bounds:', 1/mp.mpf('1.414')+1/(2*mp.mpf('2.23'))+1/(3*mp.mpf('3.16'))+1/(4*mp.mpf('4.123')) + mp.mpf('0.25'))\n# right-tail bricks (k>=11)\nW0 = (mp.log(10)+1)/10  # actually integral; sum_{k>=11} 1/k^2 <= 1/10\nprint('W0 1/10 ok:', mp.nsum(lambda k: 1/k**2, [11, mp.inf]))\nW1 = (mp.log(10)+1)/10\nprint('W1 (log10+1)/10 =', mp.nstr(W1,10), ' true sum:', mp.nstr(mp.nsum(lambda k: mp.log(k)/k**2, [11, mp.inf]),10))\nprint('log 10 <= 2.3026:', mp.log(10) <= mp.mpf('2.3026'), mp.nstr(mp.log(10),10))\nprint('1/e <= 0.3679:', 1/mp.e <= mp.mpf('0.3679'), mp.nstr(1/mp.e,10))\n# left-tail bricks (j>=14, weight 1/(j+10)^2)\nA0 = 1/mp.mpf(23)\nprint('A0 = 1/23 =', mp.nstr(A0,10), ' true:', mp.nstr(mp.nsum(lambda j: 1/(j+10)**2, [14, mp.inf]),10))\nA1 = mp.log(13)/23 + mp.log(mp.mpf(23)/13)/10\nprint('A1 =', mp.nstr(A1,10), ' true:', mp.nstr(mp.nsum(lambda j: mp.log(j)/(j+10)**2, [14, mp.inf]),10))\nprint('log 13 <= 2.565:', mp.log(13) <= mp.mpf('2.565'), mp.nstr(mp.log(13),10))\nprint('log(23/13) <= 0.571:', mp.log(mp.mpf(23)/13) <= mp.mpf('0.571'), mp.nstr(mp.log(mp.mpf(23)/13),10))\n# C0hat bridges\nprint('log(17/14) <= 0.1942:', mp.log(mp.mpf(17)/14) <= mp.mpf('0.1942'), mp.nstr(mp.log(mp.mpf(17)/14),10))\nprint('log 2.3 <= 0.833:', mp.log(mp.mpf('2.3')) <= mp.mpf('0.833'), mp.nstr(mp.log(mp.mpf('2.3')),10))\nprint('log 11 >= 2.3979:', mp.log(11) >= mp.mpf('2.3979'), mp.nstr(mp.log(11),10))\nprint('  0.833/log11 =', mp.nstr(mp.mpf('0.833')/mp.log(11),10), '<= 0.3475')\nprint('log 14 >= 2.6391:', mp.log(14) >= mp.mpf('2.6391'), mp.nstr(mp.log(14),10))\nprint('  0.1942/log14 =', mp.nstr(mp.mpf('0.1942')/mp.log(14),10), '<= 0.0736')\n# C0hat(2t+1) <= C0hat(t+1)+0.55 at t=10\ndef C0(y): return mp.mpf('0.433')*mp.log(y+2)+mp.mpf('0.886')*mp.log(mp.log(y+2))+mp.mpf('2.9')\nprint('C0(21)-C0(11) =', mp.nstr(C0(21)-C0(11),10), '<= 0.55')\n# totals\nS3 = mp.mpf('1.3476')\nTR = mp.mpf('0.433')*(mp.mpf('0.833')*mp.mpf('0.1')+mp.mpf('0.3303')) + mp.mpf('0.886')*(mp.mpf('0.3475')*mp.mpf('0.1')+mp.mpf('0.3679')*mp.mpf('0.3303')) + mp.mpf('2.9')*mp.mpf('0.1')\nTL = mp.mpf('0.433')*(mp.mpf('0.1942')*A0+mp.mpf('0.1687')) + mp.mpf('0.886')*(mp.mpf('0.0736')*A0+mp.mpf('0.3679')*mp.mpf('0.1687')) + mp.mpf('2.9')*A0\nprint('Tail_R bracket:', mp.nstr(TR,10), ' x4.5 =', mp.nstr(4.5*TR,10))\nprint('Tail_L bracket:', mp.nstr(TL,10), ' x4.5 =', mp.nstr(4.5*TL,10))\nmain_c = 4.5*2*S3\nmain_k = 4.5*mp.mpf('0.55')*S3\nprint('main:', mp.nstr(main_c,10),'*C0 +', mp.nstr(main_k,10))\ntot_k = main_k + 4.5*TR + 4.5*TL\nprint('piece3 =', mp.nstr(main_c,10),'*C0 +', mp.nstr(tot_k,10))\n\"\n","description":"Verify all piece-3 numeric constants with mpmath"},"extra_content":null}]