[{"type":"thinking","thinking":"I was mid-derivation checking the main extension constant for k ∈ (t, 2t]. Let me finish that arithmetic quickly and then record the full piece-3 plan compactly, then start writing Lean code.\n\nC0hat(3t+1) − C₀ where C₀ = C0hat(t+1):\n- log part: 0.433·log((3t+3)/(t+3)) = 0.433·log(3·(t+1)/(t+3)) ≤ 0.433·log 3 = 0.433·1.0986 = 0.4757.\n- loglog part: 0.886·[loglog(3t+3) − loglog(t+3)] ≤ 0.886·log(3)/log(t+3) ≤ 0.886·1.0986/log 13 = 0.9734/2.5649 = 0.3795.\nTotal ≤ 0.4757+0.3795 = 0.8552. So for k ∈ (t, 2t], right interval rate ≤ C₀ + 0.8552.\n\nExtra over main rate (C₀ + 0.55): 0.3052. Extra cost = 4.5·0.3052·w₀ where w₀ = Σ_{t<k≤2t} 1/(k√(1+k²)) ≤ Σ_{k≥11} 1/k² ≤ 0.1. Bound it crudely: ≤ 0.1 ⟹ extra ≤ 4.5·0.3052·0.1 = 0.1373. (Conservative — actual w₀ ≈ 0.0433 but bounding by 0.1 is cleaner in Lean; cost 0.08.)\n\nRevised piece-3 total:\n- Main (k ≤ t): 4.5·(2C₀+0.55)·S₃, S₃ ≤ 1.3703 ⟹ 12.333·C₀ + 3.3917.\n- Extension (t < k ≤ 2t): right rate C₀+0.8552, left rate C₀ (left interval k∈(t,2t]: γ ∈ (t−k−1, t−k] ⊂ (−t−1, 0), conj count ≤ C0hat(k−t+1) ≤ C0hat(t+1) = C₀ ✓). So rate ≤ 2C₀+0.8552, sum-weight Σ_{t<k≤2t} 1/(k√(1+k²)) ≤ w₀ ≤ 0.1.\n  Extension ≤ 4.5·(2C₀+0.8552)·w₀ ≤ 4.5·(2C₀+0.8552)·0.1 = 0.9·C₀ + 0.3848.\n- RIGHT₂ tail (k > 2t): ≤ 1.4038.\n- LEFT tail (γ < 0, j ≥ 14): ≤ 1.1769.\n\nHmm wait — now the extension adds a C₀ term: 0.9·C₀. Total C₀ coefficient: 12.333 + 0.9 = 13.233. That's worse than planned 12.333! The 0.9·C₀ ≈ 3.9 extra vs the tail savings. Let me recompute: without extension, intervals k∈(t,2t] on the right cost C0hat(2k+1) each — in the RIGHT tail bound I charged C0hat(2k+1)-pieces. With extension, they cost C₀+0.8552 ≈ 5.2 each vs C0hat(2k+1) ≈ 5.5 each — saving only 0.3/interval, but the bound structure changed.\n\nUgh, I'm overcomplicating. Let me step back and pick the FINAL simple structure:\n\n**FINAL piece-3 structure (simplest provable form):**\n\nRight sum (all k ≥ 1): Σ_k 4.5·countR_k/(k√(1+k²)) where countR_k ≤ C0hat(t+k+1).\n- k ≤ t: C0hat(t+k+1) ≤ C₀ + 0.55. Sum ≤ (C₀+0.55)·S₃.\n- k > t: C0hat(t+k+1) ≤ C0hat(2k+1) ≤ 0.433·(log k + 0.8329) + 0.886·(loglog k + 0.3475) + 2.9 (using 2k+3 ≤ 2.3k for k ≥ 10, and 0.8329/log 11 = 0.34746). Tail_R ≤ 0.433·(0.8329·W₀+W₁) + 0.886·(0.3475·W₀+W₂) + 2.9·W₀ with W₀ = Σ_{k≥11}1/k² ≤ 0.1, W₁ = Σ log k/k² ≤ 0.3303, W₂ = Σ loglog k/k² ≤ 0.1269.\n  = 0.433·(0.08329+0.3303) + 0.886·(0.03475+0.1269) + 0.29\n  = 0.433·0.41359 + 0.886·0.16165 + 0.29\n  = 0.17909 + 0.14322 + 0.29 = 0.61231. ×4.5 = 2.7554.\n\nLeft sum: k = 1..∞: intervals (t−k−1, t−k]:\n- k ≤ t−3: count ≤ C0hat(t−k) ≤ C₀. Sum ≤ C₀·S₃.\n- t−3 < k ≤ t+13: empty (NoLowZeros).\n- k > t+13 (i.e. j = k−t > 13, j ≥ 14): γ < 0, |γ| ∈ [j, j+1), count ≤ C0hat(j+1) ≤ 0.433·(log j + 0.1935) + 0.886·(loglog j + 0.0733) + 2.9; weight 1/(t+j)² ≤ 1/(10+j)². Tail_L ≤ 0.433·(0.1935·A₀+A₁) + 0.886·(0.0733·A₀+A₂) + 2.9·A₀ with A₀ = Σ_{j≥14}1/(j+10)² ≤ 1/23 = 0.043478, A₁ = Σ log j/(j+10)² ≤ 0.16862, A₂ = Σ loglog j/(j+10)² ≤ 0.063175.\n  = 0.433·(0.0084123+0.16862) + 0.886·(0.0031871+0.063175) + 0.12609\n  = 0.076654+0.058797+0.12609 = 0.261541. ×4.5 = 1.17693.\n\nPiece 3 ≤ 4.5·[(C₀+0.55)·S₃ + C₀·S₃ + 0.61231 + 0.26154]\n= 4.5·[(2C₀+0.55)·1.3703 + 0.87385]\n= 12.3327·C₀ + 3.39167 + 3.93233\n= 12.333·C₀ + 7.324.\n\nvs planned 12.333·C₀ + 6.014. Overrun 1.31 ≤ slack 1.87. Margin ≈ 0.56. \n\nCheck the pinch with this: assembly constant = 1 (piece1) + 2.7 (piece2) + [12.333·2.9658 + 7.324] + 0.09 + 0.6 = 1+2.7+36.579+7.324+0.09+0.6 = 48.293. Need 5.94L + 11.814LL + 48.293 ≤ 10.5L + 48 ⟺ f(L) = 11.814LL − 4.56L ≤ −0.293. f max = −0.568 ≤ −0.293 ✓ margin 0.275. Tight but OK... margin 0.275 on a certified pinch is acceptable (the pinch lemma will be proved by calculus + certified point evaluation, and the margin is what it is — actually wait, I should double-check f's max: f(L) = 11.814·log L − 4.56·L, L ≥ log 12 = 2.4849. f′(L) = 11.814/L − 4.56 = 0 at L* = 2.5912. f(L*) = 11.814·log(2.5912) − 4.56·2.5912 = 11.814·0.95197 − 11.8151 = 11.2474 − 11.8151 = −0.5677 ✓. So need −0.5677 ≤ −0.293 ⟺ 48.293 ≤ 48.568 ⟺ assembly constant ≤ 48.568. We have 48.293 ✓ margin 0.275.)\n\nHmm, margin 0.275 is thin. If I sharpen S₃ slightly (e.g. S₃ ≤ 1.36 via k ≤ 4 exact + telescope from 5: 1/(1·√2)+1/(2√5)+1/(3√10)+1/(4√17)+Σ_{k≥5}1/(k(k−1)) = 0.70721+0.22422+0.10549+0.06063+0.25 = 1.34755 — wait: Σ_{k≥5} 1/(k(k−1)) = 1/4 = 0.25. So S₃ ≤ 0.70721+0.22422+0.10549+0.06063+0.25 = 1.34755 ≤ 1.3476!). Then main = 4.5·(2C₀+0.55)·1.3476 = 12.1284·C₀ + 3.33594. Piece3 ≤ 12.1284·C₀ + 3.33594+3.93233 = 12.1284·C₀ + 7.2683. C₀-coefficient DROPS to 12.1284: 12.1284·2.9658 = 35.964; assembly = 1+2.7+35.964+7.268+0.09+0.6 = 47.622. Need ≤ 48.568: margin 0.95!! \n\nWait, that's much better — because S₃ multiplies (2C₀+0.55), a sharper S₃ saves on the C₀-coefficient too. Let me verify S₃ ≤ 1.3476: terms: k=1: 1/(1·√2), √2 ≥ 1.41421 ⟹ ≤ 0.70711·... 1/1.41421 = 0.70711. Journal used √2 ≥ 1.414 ⟹ 1/1.414 = 0.70721. k=2: 1/(2√5), √5 ≥ 2.236 ⟹ ≤ 1/4.472 = 0.22361·... journal: √5 ≥ 2.23 ⟹ 1/4.46 = 0.22422. k=3: √10 ≥ 3.16 ⟹ 1/9.48 = 0.10549 (3√10 = 3·3.16 = 9.48; journal said 1/(3·3.16) = 0.10549 ✓). k=4: √17 ≥ 4.123 ⟹ 1/(4·4.123) = 1/16.492 = 0.06064. Sum k≤4: 0.70721+0.22422+0.10549+0.06064 = 1.09756. +1/4 = 1.34756 ≤ 1.3476 ✓.\n\nNeed √17 ≥ 4.123: 4.123² = 16.999 ≤ 17 ✓. Nice rational bounds: √2 ≥ 1.414 (1.414² = 1.999396 ≤ 2 ✓), √5 ≥ 2.23 (2.23² = 4.9729 ≤ 5 ✓), √10 ≥ 3.16 (3.16² = 9.9856 ≤ 10 ✓), √17 ≥ 4.123 (4.123² = 16.999129 ≤ 17 ✓). All norm_num-able via Real.le_sqrt-ish lemmas or Real.sqrt_le_sqrt + (x)² ≤ y.\n\nActually the telescope for k ≥ 5: 1/(k√(1+k²)) ≤ 1/(k(k−1)) ⟺ k−1 ≤ √(1+k²) ⟺ (k−1)² ≤ 1+k² ⟺ k²−2k+1 ≤ k²+1 ⟺ −2k ≤ 0 ✓. And Σ_{k≥5} 1/(k(k−1)) = 1/4: via 1/(k(k−1)) = 1/(k−1) − 1/k, telescope from 5: = 1/4. In Lean: summable + tsum via the pattern... they used Finset.sum_range_sub for Σ_{k≥4} = 1/3 in journal-035's plan. There's likely an existing pattern in the codebase or Mathlib: tsum of 1/(n(n+1)) — hmm, there's `Real.tsum_one_div_mul_add_one`? Not sure. I may need: ∑' (1/(k+4) − 1/(k+5)) — telescoping tsum: Summable.hasSum of telescope: Σ_{k=0}^{N-1} (a_k − a_{k+1}) = a_0 − a_N → a_0 if a_N → 0. So ∑'_{k} (1/(k+4)−1/(k+5)) = 1/4. That's a clean pattern (tendsto + sum_range_sub).\n\nOK so the FINAL plan:\n\n**Piece 3 ≤ 12.1284·C₀ + 7.2683**, i.e.\n‖far series‖ ≤ 12.1284·C0hat(t+1) + 7.2683.\n\nLet me now also recompute with this the exact statement I'll prove, and figure out the cleanest constant packaging for Lean. In Lean, decimal rationals like 12.1284 are painful. Let me repackage with slightly-rounded but clean rationals:\n\n- S₃ ≤ 1.3476 (via 4 exact terms + telescope 1/4). Actually, let me express S₃ bound as a clean computation: S₃ ≤ 1/1.414 + 1/4.46 + 1/9.48 + 1/16.492 + 1/4. Hmm, decimals are rationals: 1.414 = 1414/1000 etc. norm_num can handle. Final S₃ ≤ 13476/10000 = 3369/2500. Fine as `(1.3476 : ℝ)` — Lean parses decimals as rationals, and norm_num can verify. We've used 0.433, 0.886, 2.9 etc. throughout, so decimal literals are the house style.\n\n- Right tail: 4.5·0.61231 = 2.7554 ≤ 2.7554. Components: W₀ ≤ 0.1, W₁ ≤ 0.3303, W₂ ≤ 0.1269, with C0hat(2k+1) ≤ 0.433·(log k + 0.8329) + 0.886·(loglog k + 0.3475) + 2.9.\n  Wait — I should double check 0.8329: 2k+3 ≤ 2.3k ⟺ 3 ≤ 0.3k ⟺ k ≥ 10 ✓. log(2k+3) ≤ log(2.3k) = log k + log 2.3. log 2.3 = 0.83291 ≤ 0.83291. Use 0.833. loglog(2k+3) = log(log(2k+3)) ≤ log(log k + 0.833) ≤ loglog k + 0.833/log k ≤ loglog k + 0.833/log 11 = loglog k + 0.34747. Use 0.3475.\n  Tail_R ≤ 0.433·(0.833·0.1 + 0.3303) + 0.886·(0.3475·0.1 + 0.1269) + 2.9·0.1 = 0.433·0.4136 + 0.886·0.16165 + 0.29 = 0.17909+0.14322+0.29 = 0.61231. ×4.5 = 2.75540.\n\n- Left tail: 4.5·0.261541 = 1.17694 ≤ 1.17694. Components: A₀ ≤ 1/23 (0.043478), A₁ ≤ 0.16862, A₂ ≤ 0.063175, C0hat(j+1) ≤ 0.433·(log j + 0.1935) + 0.886·(loglog j + 0.0733) + 2.9.\n  Check 0.1935: (j+3)/j ≤ 17/14 for j ≥ 14 ⟹ log(j+3) ≤ log j + log(17/14). log(17/14) = log 1.214286 = 0.19416·... let me compute: ln(17/14) = ln 17 − ln 14 = 2.833213 − 2.639057 = 0.194156. So 0.1942, not 0.1935! I made an error earlier (0.19347). Use 0.1942. Then loglog increment ≤ 0.1942/log 14 = 0.1942/2.6391 = 0.073587. Use 0.0736.\n  Tail_L ≤ 0.433·(0.1942·0.043478 + 0.16862) + 0.886·(0.0736·0.043478 + 0.063175) + 2.9·0.043478\n  = 0.433·(0.0084432+0.16862) + 0.886·(0.0032+0.063175) + 0.126087\n  = 0.433·0.17706 + 0.886·0.066375 + 0.126087\n  = 0.076667 + 0.058808 + 0.126087 = 0.261562. ×4.5 = 1.17703.\n\n- Piece 3 ≤ 4.5·[(2C₀+0.55)·1.3476 + 0.61231 + 0.26156] = 4.5·[2.6952·C₀ + 0.74118 + 0.87387] = 12.1284·C₀ + 4.5·1.61505 = 12.1284·C₀ + 7.26773.\n\nRound up: **piece 3 ≤ 12.1284·C0hat(t+1) + 7.2678**.\n\nAssembly check: piece3 ≤ 12.1284·(0.433L + 0.886LL + 2.9658) + 7.2678 = 5.2516·L + 10.7461·LL + 35.9638 + 7.2678 = 5.2516L + 10.7461LL + 43.2316. Assembly total = 1 + (0.6L+0.886LL+2.7) + that + 0.09 + 0.6 = 5.8516·L + 11.6321·LL + 47.6216. Pinch: need 11.6321·LL − 4.6484·L ≤ 48 − 47.6216 = 0.3784. f(L) = 11.6321·log L − 4.6484·L, L ≥ log 12 = 2.48491. f′ = 11.6321/L − 4.6484 = 0 at L* = 2.50235. f(L*) = 11.6321·log(2.50235) − 4.6484·2.50235 = 11.6321·0.91685 − 11.6322 = 10.6653 − 11.6322 = −0.9669. So f ≤ −0.9669 ≤ 0.3784 ✓✓ margin 1.345!! Excellent — the sharper S₃ (1.3476 vs 1.3703) reduced both the L and LL coefficients, making the pinch EASY (margin 1.35).\n\nWait, why did the journal plan have margin only 1.87−...? Their S₃ was 1.3703 and tail 0.5828: assembly 5.94L+11.813LL+46.7: margin = 48−46.7−(−(−0.568))·... f(L) = 11.813LL−4.56L, max −0.568, need ≤ 1.3, margin 1.868. Mine: assembly 47.62, f max −0.967, need ≤ 0.378, margin 1.345. Comparable. Good.\n\nActually — hmm, one more consideration. I should double check the claim \"left intervals for t−3 < k ≤ t+13 are empty\" and \"k ≤ t−3 left count ≤ C0hat(t−k) ≤ C₀\": ZeroCountProp at a = t−k−1 requires a ≥ 2, i.e. k ≤ t−3 ✓ gives count in [t−k−1, t−k] ≤ C0hat(t−k) ≤ C0hat(t+1) = C₀ (C0hat monotone increasing — need a lemma for that: C0hat_mono exists! (mentioned in journal-035: \"C0hat_mono\" from LiGapCircles usage). ✓.\n\nBut actually the left interval is (t−k−1, t−k] while zeroWindow(a) = [a, a+1] closed. The far zeros with x = |t−γ| ∈ [k, k+1): left side γ ≤ t−k... wait: x ∈ [k, k+1) and γ < t ⟺ γ ∈ (t−k−1, t−k]. The window [t−k−1, t−k] closed — boundary point γ = t−k−1 has x = k+1, NOT in [k, k+1). But for an upper bound, including extra zeros is fine: count over (t−k−1, t−k] ≤ count over [t−k−1, t−k] = zeroWindow(t−k−1) ≤ C0hat(t−k) ✓.\n\nSimilarly right side: γ ∈ [t+k, t+k+1) ⊂ [t+k, t+k+1] = zeroWindow(t+k) ≤ C0hat(t+k+1) ✓ (needs t+k ≥ 2 ✓).\n\nAnd the k = ⌊x⌋ partition: x ≥ 1 (far). k ranges over all naturals ≥ 1. Each far zero belongs to exactly one k. For the LEAN proof, the cleanest formalization:\n\nThe far tsum: ∑' ρ, farTerm ρ where farTerm = if near then 0 else seriesDiffTerm. Split the tsum by a FINSET covering all zeros with x < X_max, plus a tail. But intervals k > t+13 on the left and k > t on the right are infinite families — as a tsum split we'd do:\n\nFinset F = zeros with x < some bound (say |γ| ≤ 3t+20 — covers x ≤ 2t+20... hmm). Actually cleaner: \n- Left tail: reindex as a sum over j ≥ 14 of (count in window j) × (weight at j) — but this is a sum over WINDOWS, not zeros. In Lean, I need: Σ_{ρ: left tail} m·w(ρ) ≤ Σ_{j≥14} (Σ_{ρ: |γ|∈[j,j+1)} m)·w_j where w_j = 4.5/(10+j)² ≥ w(ρ) for ρ in window j. This is a fiberwise sum: group the tail zeros by j = ⌊|γ|⌋. In Lean: tsum over subtype, split by finsets... \n\nThe machinery for this exists: LiCircleBound used `tsum_split_finset` + `dyadic_family_le` (Finset.sum_fiberwise_of_maps_to) + `tsum_subtype`. But here I have THREE regimes (left main, right main, left tail, right tail). The cleanest approach:\n\nSince the far sum is bounded by a sum over intervals with per-interval counts, maybe the cleanest is:\n\n‖far series‖ ≤ ∑' ρ, ‖farTerm ρ‖ ≤ ∑' ρ, 4.5·m/(x_ρ√(1+x_ρ²)) [pointwise bound, far only]\nThen split this ℝ-valued tsum as:\n∑' ρ, g(ρ) = ∑_{ρ ∈ F} g(ρ) + ∑'_{ρ ∉ F} g(ρ) (tsum_split_finset, g summable — need summability of g! Is g summable? g(ρ) = 4.5·m/(x√(1+x²)) where x = |t−γ|. For zeros far from t: ~m/γ²-ish — summable by comparison with m/(1+γ²) (Zeta23 zero_sum_inv_sq exists as `WeilEF.zero_sum_inv_sq` — used in LiSeries as `zero_sum_inv_sq zetaSeam`... need to check exact name). Yes: for x ≥ 1: 4.5/(x√(1+x²)) ≤ 4.5/x² ≤ 4.5·2/(1+x²) and 1+x² vs 1+γ²: x = |t−γ| ≥ |γ|−t ⟹ for |γ| ≥ 2t: x ≥ |γ|/2 ⟹ 1+x² ≥ 1+γ²/4 ≥ (1+γ²)/4 ⟹ 4.5·2/(1+x²) ≤ 36/(1+γ²). For |γ| ≤ 2t (finite ball): finite. So g ≤ finite-part + 36·m/(1+γ²): summable ✓.\n\nPlan:\n1. g(ρ) := if ρ ∈ nearZerosSub t then 0 else 4.5·m/(x√(1+x²)) — hmm, actually simpler: bound ‖farTerm ρ‖ ≤ g(ρ) pointwise where g includes the if. Then norm tsum ≤ tsum of g (need: norm_tsum_le_tsum_norm-ish: ‖∑' f‖ ≤ ∑' ‖f‖ for summable norm — `norm_tsum_le_tsum_norm` exists in Mathlib for ℝ≥? There's `norm_tsum_le` / tsum_of_norm_bounded... In LiCircleBound they must have used something. I'll find it.)\n\n2. Split the g-tsum by the finset F := zeros with |γ| ≤ 2t+1 (covers all main-range zeros: x ≤ t+|γ|... wait, main range = x ≤ t+13 left, x ≤ t right — |γ| ≤ max(t+x...) — zeros with x < t+14 have |γ| ≤ t + x < 2t+14. So F = {‖ρ‖ ≤ 2t+14}-ish finite ball (finite_subtype_norm_lt exists!). Then:\n   - Finite part: ∑_{ρ ∈ F} g(ρ) — bound by grouping intervals k = 1..K within the finset: actually within F, bound ∑ g = ∑_k (count in interval k)·4.5/(k√(1+k²)) via fiberwise on k = ⌊x⌋... In a FINSET this is clean: Finset.sum_fiberwise or sum_le_sum by mapping each element to its interval bucket and using count bounds per bucket.\n   - Tail part: ∑'_{ρ ∉ F} g(ρ) — zeros with |γ| > 2t+14: bound via... hmm, the tail needs per-window counts again (infinite).\n\nUgh, the infinite tails are the annoying part. Alternative cleaner approach for tails: bound the tail tsum directly by the per-window technique used in LiCircleBound's `zero_tail_inv_sq_le` — the dyadic fiber machine (ENNReal.tsum_fiberwise). That was ~800 lines for the m/(1+γ²) tail. I don't want to rebuild that.\n\nBETTER IDEA: bound the left and right tails as sums over windows DIRECTLY using the existing count lemma `sum_zeroMult_le_of_im_band`?? No — that's for finite finsets.\n\nHmm wait — actually there's a MUCH cleaner idea for the tails using `zero_tail_inv_sq_le` (LiCircleBound, X ≥ 200): Σ_{|γ|>X} m/(1+γ²) ≤ 16·A₀·log X/X — but A₀ is opaque ≥ 1, and 16·1·log(200)/200 = 0.42 — too big ×4.5·(conversion)... The conversion: tail zeros (|γ| > 2t+14) have x ≥ |γ|−t ≥ |γ|·(1−t/(2t+14)) = |γ|·(t+14)/(2t+14) ≥ |γ|·24/34 ≥ 0.7·|γ|. So 1/x² ≤ 2/(1+γ²)·... 1/x² ≤ 1/(0.49·γ²) ≤ 2.05/γ² ≤ 2.05·2/(1+γ²)·... ≤ 4.1/(1+γ²) (for γ² ≥ 1). Tail ≤ 4.5·4.1·Σ_{|γ|>2t+14} m/(1+γ²) ≤ 18.45·16·A₀·log(2t+14)/(2t+14). At t = 10: = 295·A₀·log(34)/34 = 295·A₀·0.1037 = 30.6·A₀ ≥ 30. WAY too big. And A₀ opaque. Dead end — confirms the journal plan of per-window C0hat counts.\n\nOK so for the tails I need per-window sums over infinitely many windows. The clean Lean pattern: the right tail is Σ over zeros with γ > 2t... Actually — KEY SIMPLIFICATION: make the finite part cover EVERYTHING except a tail that's handled by a monotone-weight argument:\n\nFor the right tail (γ > 2t, i.e. x > t): write the sum as Σ_{j≥0} (sum over zeros in window W_j = [2t+j, 2t+j+1))·weight_j — as a tsum this is: define the window index j(ρ) = ⌊γ−2t⌋ for tail zeros. Then ∑'_{tail} g = ∑'_{j} Σ_{ρ: j(ρ)=j} g ≤ ∑'_{j} count_j·w_j where count_j ≤ C0hat(2t+j+1) ≤ C0hat(2(t+j)+1)... hmm wait, γ ∈ [2t+j, 2t+j+1) ⟹ x = γ−t ∈ [t+j, t+j+1) ⟹ k = t+j-ish and weight 4.5/(x√(1+x²)) ≤ 4.5/(t+j)². And count in W_j = zeroWindow(2t+j) ≤ C0hat(2t+j+1).\n\nSo right tail ≤ Σ_{j≥0} C0hat(2t+j+1)·4.5/(t+j)² — a tsum over j ∈ ℕ of an explicit function! That's summable (≈ log j/j²) and I can bound it by the integral-test machinery (AntitoneOn.tsum_comp_add_le_integral — already used in this file for the log/x² bound!). Similarly the left tail: Σ_{j≥14} C0hat(j+1)·4.5/(t+j)².\n\nTHIS is much cleaner: the tails become explicit real tsums over j, bounded by the integral test. The grouping (fiberwise) step: ∑'_{ρ: tail} g(ρ) ≤ Σ'_j count_j·w_j — needs: map each tail zero to its window index j(ρ), then bound the fiber sums. In Lean: for the right tail, all zeros in the tail satisfy γ > 2t. Use `tsum_fiberwise`-style: actually the simplest is:\n\n∑'_{ρ ∈ subtype, γ > 2t} g(ρ) where g(ρ) = 4.5·m/(x√(1+x²)) ≤ 4.5·m/(t+⌊γ−2t⌋)²... hmm, need x ≥ t+j: γ ≥ 2t+j ⟹ x = γ−t ≥ t+j ✓. So g(ρ) ≤ 4.5·m/(t+j(ρ))². Then ∑' g ≤ ∑' 4.5·m/(t+j(ρ))² — and now I want to group by j: = Σ_j Σ_{ρ: j(ρ)=j} 4.5·m/(t+j)² ≤ Σ_j 4.5·C0hat(2t+j+1)/(t+j)².\n\nThe grouping equality ∑'_{ρ} F(j(ρ), ρ) = Σ'_j Σ_{fiber j} F(j, ρ) is `tsum_fiberwise` (ENNReal) or for ℝ: there's `Summable.tsum_fiberwise`? In LiCircleBound they used ENNReal.tsum_fiberwise for a similar step (journal-031: \"the ENNReal.tsum_fiberwise + ofReal_tsum_of_nonneg assembly\"). So the pattern exists in the codebase — I can clone it.\n\nAlternatively — EVEN SIMPLER: avoid fiberwise entirely! Bound the right-tail tsum by an INTEGRAL-style comparison... no. OR: use the window-count differently: note that the map j(ρ) = ⌊γ−2t⌋ from tail zeros to ℕ has fiber sums ≤ C0hat(2t+j+1). \n\nActually, you know what's cleanest? The LEFT tail and RIGHT tail can BOTH avoid fiberwise via this trick:\n\n∑'_{ρ: tail} 4.5·m/(t+j(ρ))² ≤ ∑'_{ρ: tail} 4.5·m·φ(j(ρ)) where φ decreasing. Write φ(j) = Σ_{ℓ≥j} (φ(ℓ)−φ(ℓ+1)) (telescoping, φ(ℓ)→0). Then ∑' m·φ(j(ρ)) = ∑' m·Σ_{ℓ≥j(ρ)} Δφ(ℓ) = Σ_ℓ Δφ(ℓ)·(Σ_{ρ: j(ρ)≤ℓ} m) — the partial-count! And Σ_{ρ: j(ρ)≤ℓ} m = count in [2t, 2t+ℓ+1) ≤ (ℓ+1)·C0hat(2t+ℓ+1) — chained windows... that reintroduces the (ℓ+1) factor. No good — the fiberwise is the right tool (it keeps per-window counts).\n\nHmm, actually — wait. Let me reconsider. Is there an even simpler global structure? What if the FINITE part covers k ≤ some absolute K₀ (not t-dependent), and EVERYTHING else is \"tail\" handled by fiberwise window sums on both sides? The finite part: k = 1..K₀ windows, counts via ZeroCountProp (needs windows ≥ 2: right windows [t+k, t+k+1) fine; left windows [t−k−1, t−k] need t−k−1 ≥ 2 ⟺ k ≤ t−3 — for k ≤ K₀ ≤ t−3 when t ≥ K₀+3: if K₀ = 7, need t ≥ 10 ✓!!). \n\nOH NICE. If K₀ = 7 (≤ t−3 for t ≥ 10 ✓), the finite part is only 14 windows (7 left + 7 right), all with counts ≤ C₀ (left) / C₀+0.55-ish (right: C0hat(t+k+1) ≤ C0hat(t+8) ≤ C₀+0.433·log((t+10)/(t+3))+... ≤ C₀+0.433·log(20/13)+0.886·... ≈ C₀+0.19+0.066 = C₀+0.26). And the tails (k ≥ 8 both sides) are handled by fiberwise window sums:\n\n- Right tail: Σ_{j≥0} C0hat(t+8+j+1)·4.5/(8+j)²-ish (window [t+8+j, t+9+j), x ∈ [8+j, 9+j)): weight ≤ 4.5/(8+j)², count ≤ C0hat(t+9+j) ≤ 0.433·log(t+j+11)+0.886·loglog+2.9. With t ≥ 10: log(t+j+11) ≤ log(j+21)+log((t+j+11)/(j+21))·... hmm, t+j+11 vs (j+21): t+j+11 ≤ j+21 ⟺ t ≤ 10 — NOT for t > 10! Need log(t+j+11) ≤ log(j+21) + log((t+j+11)/(j+21)) and (t+j+11)/(j+21) ≤ (t+11)/21 (decreasing in j) ≤ (t+11)/21. So log ≤ log(j+21) + log((t+11)/21). Hmm, that brings t back in — and log((t+11)/21) is unbounded in t. That's FINE actually — the right-tail bound then depends on t logarithmically: ≈ [log((t+11)/21)]·Σ4.5/(8+j)² ≈ log(t)·4.5·(1/7)·... ≈ 0.64·log(t+11)−1.95·... — WAIT that adds an L-dependent term to the tail! 4.5·Σ_{j≥0}1/(8+j)² = 4.5·(π²/6 − Σ_{1..7}) ≈ 4.5·0.1504 = 0.677. So the right tail ≈ 0.677·(0.433·(log(j-stuff)+log((t+11)/21))+...) ≈ 0.677·0.433·log(t+11) + const ≈ 0.29·log(t+11) + ... — adds ≈ 0.29·L to the assembly L-coefficient. Current L-coefficient 5.85 → 6.14. Pinch: f(L) = 11.63LL − (10.5−6.14)L = 11.63LL − 4.36L, max at L = 11.63/4.36 = 2.667: f = 11.63·0.981 − 11.63 = −0.22. Assembly constant ≈ 47.6−... need ≤ 48: f ≤ 0.4: −0.22 ≤ 0.4 ✓ margin 0.62. Hmm OK still fits but now I realize the tail's t-dependence matters. But wait — this is WRONG accounting: the windows [t+8+j, t+9+j) for j large have counts growing like log(t+j), and I bound log(t+j+11) ≤ log(j+21) + log((t+11)/21) — for j ≥ t−10-ish, (t+j+11)/(j+21) ≤ ... actually the max of (t+j+11)/(j+21) over j ≥ 0 is at j = 0: (t+11)/21. So the bound log(t+j+11) ≤ log(j+21)+log((t+11)/21) is valid for all j ≥ 0 but LOSSY for large j. The sum Σ_j C0hat(t+9+j)/(8+j)² with this bound: = Σ [0.433·(log(j+21)+log((t+11)/21)) + 0.886·(loglog(j+21)+0.35-ish) + 2.9]/(8+j)² — the log((t+11)/21) term: 0.433·log((t+11)/21)·Σ1/(8+j)² = 0.433·log((t+11)/21)·0.1504·... hmm for t = 10: log(21/21) = 0 — at t = 10 it's ZERO and grows as log t. So actually at t = 10 the lossy term vanishes! And for large t it grows like 0.065·log t. L-coefficient addition ≈ 0.065. Fine!\n\nHmm, but honestly, splitting the tail sum at the t-dependent point (k > t) vs fixed point (k ≥ 8): the k > t split has the issue that the number of main-range intervals is t-dependent (infinite family) — the fiberwise machine is needed anyway for k > t. So why not make the main range FINITE (k ≤ 7) and put k ≥ 8 in the tail? The tail then = two fiberwise window sums starting at fixed heights. MUCH cleaner Lean!\n\nNew structure:\n- **Main (finite), k = 1..7:** left windows [t−k−1, t−k] count ≤ C₀ (need t−k−1 ≥ 2 ⟺ k ≤ t−3 ✓ for t ≥ 10, k ≤ 7). Right windows [t+k, t+k+1] count ≤ C0hat(t+k+1) ≤ C0hat(t+8) ≤ C₀ + δ₈ where δ₈ = C0hat(t+8)−C0hat(t+1) ≤ 0.433·log((t+10)/(t+3)) + 0.886·[log((t+10)/(t+3))]/log(t+3) ≤ 0.433·log(20/13) + 0.886·log(20/13)/log 13 = 0.433·0.43078 + 0.886·0.43078/2.5649 = 0.18653+0.14879 = 0.33532. So right ≤ C₀ + 0.3354.\n  Main ≤ 4.5·[7·C₀ + 7·(C₀+0.3354)]·(1/7)·... NO WAIT — the main sum is over intervals k = 1..7 with weights 4.5/(k√(1+k²)), NOT a flat sum: Main = Σ_{k=1..7} 4.5·(countL_k + countR_k)/(k√(1+k²)) ≤ 4.5·[C₀ + (C₀+0.3354)]·Σ_{k=1..7} 1/(k√(1+k²)) = 4.5·(2C₀+0.3354)·S₇ where S₇ = Σ_{k=1..7} 1/(k√(1+k²)).\n  S₇: k=1: 0.70721 (√2 ≥ 1.414); k=2: 0.22422 (√5 ≥ 2.23); k=3: 0.10549 (√10 ≥ 3.16); k=4: 0.06064 (√17 ≥ 4.123); k=5: 1/(5√26): √26 ≥ 5.099 ⟹ 1/25.495 = 0.039223; k=6: 1/(6√37): √37 ≥ 6.082 ⟹ 1/36.492 = 0.027403; k=7: 1/(7√50): √50 ≥ 7.071 ⟹ 1/49.497 = 0.020203. Sum: 0.70721+0.22422+0.10549+0.06064+0.039223+0.027403+0.020203 = 1.184398. So S₇ ≤ 1.1844.\n  Main ≤ 4.5·(2C₀+0.3354)·1.1844 = 10.6596·C₀ + 1.78747.\n  Check rational bounds: √26 ≥ 5.099: 5.099² = 25.9998 ≤ 26 ✓. √37 ≥ 6.082: 6.082² = 36.9907 ≤ 37 ✓. √50 ≥ 7.071: 7.071² = 49.999 ✓.\n\n- **Right tail (j ≥ 0, windows [t+8+j, t+9+j)):** ≤ Σ'_j C0hat(t+9+j)·4.5/(8+j)². \n  C0hat(t+9+j) = 0.433·log(t+j+11) + 0.886·loglog(t+j+11) + 2.9.\n  Bound: log(t+j+11) ≤ log(j+21) + log((t+11)/21) — at general t this is lossy; alternative: log(t+j+11) = log((j+21)·(1+(t−10)/(j+21))) = log(j+21) + log(1+(t−10)/(j+21)) ≤ log(j+21) + (t−10)/(j+21) ≤ log(j+21) + (t−10)/21. Hmm — that has a LINEAR t term!! (t−10)/21·Σ0.433·4.5/(8+j)² = (t−10)·0.433·0.677/21 = 0.014·(t−10) — LINEAR in t, would add 0.014·t to the assembly — DISASTER (breaks any L-bound for large t). NO GOOD.\n  \n  So the tail split must be at a t-dependent point to keep counts t-independent-ish, OR bound log(t+j+11) differently: log(t+j+11) ≤ log((t+11)·(j+21)/21) = log(t+11) + log(j+21) − log 21 — using t+j+11 ≤ (t+11)(j+21)/21 ⟺ 21(t+j+11) ≤ (t+11)(j+21) ⟺ 21t+21j+231 ≤ tj+21t+11j+231 ⟺ 10j ≤ tj ⟺ 10 ≤ t ✓!!! So log(t+j+11) ≤ log(t+11) + log(j+21) − log 21 for t ≥ 10 ✓. \n  Then C0hat(t+9+j) ≤ 0.433·(log(t+11) + log(j+21) − log 21) + 0.886·loglog(t+9+j) + 2.9. Hmm, and loglog(t+j+11) ≤ log(log(t+11)+log(j+21)−log 21) ≤ ... ≤ log(2·max(log(t+11), log(j+21)))... messy. Alternative for the loglog: loglog(t+j+11) ≤ loglog((t+11)(j+21)) (since t+j+11 ≤ (t+11)(j+21) for t ≥ 10, j ≥ 0: (t+11)(j+21) ≥ t+j+11 ⟺ tj+21t+11j+231 ≥ t+j+11 ✓ obvious). And log(log((t+11)(j+21))) = log(log(t+11)+log(j+21)) ≤ log(2·log(t+11)·log(j+21))·... if both ≥ 2: log(a+b) ≤ log(2ab) for a,b ≥ 2 ✓ (a+b ≤ ab for a,b ≥ 2... a+b ≤ 2ab always for a,b ≥ 1). log(t+11) ≥ log 21 = 3.0445 ≥ 2 ✓; log(j+21) ≥ 3.0445 ≥ 2 ✓. So loglog(t+j+11) ≤ log 2 + loglog(t+11) + loglog(j+21).\n  \n  So C0hat(t+9+j) ≤ 0.433·log(t+11) + 0.886·loglog(t+11) + [0.433·(log(j+21)−log 21) + 0.886·(log 2 + loglog(j+21)) + 2.9].\n  The t-part: 0.433·log(t+11)+0.886·loglog(t+11) = C0hat(t+9) − 2.9... interesting: = C0hat(t+9)−2.9 ≤ C₀ + 0.3354−2.9-ish. Hmm.\n  \n  Right tail ≤ Σ_j {C₀-part + j-part}·4.5/(8+j)² = (0.433·log(t+11)+0.886·loglog(t+11))·4.5·Σ1/(8+j)² + 4.5·Σ[0.433·(log(j+21)−log 21)+0.886·(log2+loglog(j+21))+2.9]/(8+j)².\n  Σ_{j≥0} 1/(8+j)² = Σ_{m≥8} 1/m² ≤ ∫₇^∞ dx/x² = 1/7 = 0.14286. \n  Σ log(j+21)/(8+j)² = Σ_{m≥8} log(m+13)/m² ≤ ∫₇^∞ log(x+13)/x² dx = [−log(x+13)/x − ...]: ∫ log(x+13)/x² dx = −log(x+13)/x + ∫ 1/(x(x+13)) dx = −log(x+13)/x + (1/13)·log(x/(x+13)). At 7: −log 20/7 + (1/13)log(7/20) = −0.42791−0.08090 = −0.50881. At ∞: 0. So ∫₇^∞ = 0.50881.\n  Σ loglog(j+21)/(8+j)² ≤ ∫₇^∞ loglog(x+13)/x² dx = [−loglog(x+13)/x]₇^∞ + ∫₇^∞ 1/(x²·log(x+13)·(x+13)/x·...) hmm: d/dx loglog(x+13) = 1/((x+13)log(x+13)). ∫₇^∞ loglog(x+13)/x² dx = −loglog(20)/7·(−1) + ∫₇^∞ 1/(x·(x+13)·log(x+13)) dx ≤ loglog(20)/7 + (1/log 20)·∫₇^∞ 1/(x(x+13)) dx = 1.09812/7·... = 0.15687 + (1/2.99573)·(1/13)·log(20/7) = 0.15687+0.025687·1.04982 = 0.15687+0.02697 = 0.18384.\n  \n  Right tail ≤ 4.5·[0.433·log(t+11)+0.886·loglog(t+11)]·0.14286 + 4.5·[0.433·(0.50881−log21·0.14286) + 0.886·(0.69315·0.14286+0.18384) + 2.9·0.14286]\n  log 21 = 3.04452. 0.433·(0.50881−0.43493) = 0.433·0.07388 = 0.03199. 0.886·(0.09902+0.18384) = 0.886·0.28286 = 0.25061. 2.9·0.14286 = 0.41429. j-part sum = 0.03199+0.25061+0.41429 = 0.69689. ×4.5 = 3.13600.\n  t-part: 4.5·0.14286·(0.433·log(t+11)+0.886·loglog(t+11)) = 0.64287·(0.433·log(t+11)+0.886·loglog(t+11)).\n  Hmm — 0.64287·0.433 = 0.27836·log(t+11) and 0.64287·0.886 = 0.56957·loglog(t+11). These are t-DEPENDENT pieces adding to the assembly: +0.28·L-ish and +0.57·LL-ish. Ugh — worse than the k>t split which kept the right tail t-independent (counts C0hat(2k+1) depend only on k)!\n\nHmm right — the k>t split was clever: for k > t, t+k+1 ≤ 2k+1 makes the count t-independent. With the fixed split at k = 8, the tail counts inevitably grow with t. The t-dependence ≈ 0.28·L + 0.57·LL — the assembly becomes ≈ 6.13·L + 12.20·LL + 47.6-ish: pinch f(L) = 12.20·LL − 4.37·L, max at L = 12.20/4.37 = 2.792: f = 12.20·1.0265−12.20 = 0.32. Need f ≤ 48−47.6 = 0.4: 0.32 ≤ 0.4 ✓ margin 0.08!!! WAY too tight.\n\nSo the fixed-split idea is bad for the pinch. The t-dependent split (k ≤ t main, k > t tail) is REQUIRED. That means the main range is an infinite (t-dependent) family — I need the fiberwise machine for the main range too. Fine — it all becomes fiberwise window sums:\n\n**FINAL STRUCTURE (all fiberwise window sums):**\n- Right side: windows W_j = [t+1+j, t+2+j) for j ≥ 0 covering γ > t+1 (x = γ−t > 1 ⟹ j = ⌊x⌋−1 = ⌊γ−t−1⌋ ≥ 0). Per-window: count ≤ C0hat(t+2+j), weight ≤ 4.5/((1+j)√(1+(1+j)²)).\n  Right sum ≤ Σ'_j C0hat(t+2+j)·4.5/((1+j)√(1+(1+j)²)).\n  Split at j+1 ≤ t (i.e. j < t, the \"main\") vs j+1 > t (\"tail\"):\n  - Main: C0hat(t+2+j) ≤ C0hat(2t+1) ≤ C₀ + 0.55. Sum ≤ (C₀+0.55)·4.5·S₃-part.\n  - Tail (k = j+1 > t): C0hat(t+2+j) = C0hat(t+k+1) ≤ C0hat(2k+1) ≤ 0.433·(log k + 0.8329)+0.886·(loglog k+0.3475)+2.9 (k ≥ 11 since k > t ≥ 10). Sum ≤ the t-independent tail_R ≤ 0.61231·4.5.\n- Left side: windows V_j = [t−2−j, t−1−j] for j ≥ 0 covering γ < t−1 (x = t−γ > 1, k = ⌊x⌋ ≥ 1: γ ∈ (t−k−1, t−k] ⟹ j = k−1 ≥ 0).\n  - For j ≤ t−4 (k ≤ t−3): window start t−2−j ≥ 2 ✓ count ≤ C0hat(t−1−j) ≤ C₀. \n  - For t−4 < j ≤ t+12: window ⊂ (−14, 14)-ish — empty by NoLowZeros: j > t−4 ⟺ t−1−j < 5; j ≤ t+12 ⟺ t−2−j ≥ −14. So zeros with γ ∈ (t−2−j, t−1−j]... hmm zeroWindow is CLOSED [a, a+1]: [t−2−j, t−1−j] with t−2−j ≥ −14 and t−1−j ≤ 5: γ ∈ [−14, 5] ⟹ |γ| ≤ 14 ⟹ empty by NoLowZeros (14 ≤ |γ| — wait, |γ| = 14 boundary: NoLowZeros says 14 ≤ |γ|, so zeros with |γ| ≤ 14 don't exist EXCEPT possibly |γ| = 14 exactly?? NoLowZeros: ∀ ρ, IsNontrivialZero ρ → 14 ≤ |ρ.im|. So zeros with |γ| < 14 don't exist; |γ| = 14 is allowed by the prop but the window [−14, 5] contains γ = −14 possibly. Hmm — need the window to avoid |γ| = 14: use j < t+12 (strict) giving t−2−j > −14, window ⊂ (−14, 5) — zeros there have |γ| < 14 ⟹ none ✓. Boundary handled by strictness; or just include one more window in the tail range with j ≥ ⌈t+12⌉... For cleanliness: tail starts at j ≥ J₀(t) = max(⌈t−4⌉, ...) — the empty range is finite so I can also just bound it crudely: empty ⟹ contributes 0. In Lean, the fiberwise sum over the empty-range windows: the fiber is empty ⟹ sum = 0 ✓ no count bound needed at all! The NoLowZeros proof just says the FIBER is empty. So the structure: left tail j ≥ t−3: fiber empty for j ≤ t+12 (|γ| < 14); for j > t+12 (|γ| ≥ 13·...): j > t+12 ⟺ γ < t−1−(t+12) = −13 ⟹ |γ| > 13... need |γ| ≥ 14: j ≥ t+13 ⟹ γ ≤ t−1−j ≤ −14 ⟹ |γ| ≥ 14 ✓ consistent.\n    Tail windows: γ ∈ [t−2−j, t−1−j], |γ| ∈ [1+j−t, 2+j−t] (negate). Count via conj: zerosIn(1+j−t, 2+j−t)-ish ≤ zeroWindow(1+j−t) ≤ C0hat(2+j−t) — need 1+j−t ≥ 2 ⟺ j ≥ t+1 ✓ (tail j ≥ t+13 satisfies). Weight: x = t−γ ≥ t+|γ| ≥ t+(1+j−t) = 1+j... wait: γ ≤ −(1+j−t) = t−1−j ⟹ x = t−γ ≥ 1+j. Hmm but also x < ... the window V_j corresponds to x ∈ [1+j, 2+j] hmm: γ ∈ [t−2−j, t−1−j] ⟹ x = t−γ ∈ [1+j, 2+j]. So k = ⌊x⌋ ∈ {1+j, ...}: weight 4.5/(x√(1+x²)) ≤ 4.5/((1+j)√(1+(1+j)²)) ✓ same form as right with k = 1+j.\n    Left tail sum ≤ Σ_{j ≥ t+13} C0hat(2+j−t)·4.5/((1+j)√(1+(1+j)²)). Substitute ℓ = 1+j−t (ℓ ≥ 14): j = ℓ+t−1, 1+j = ℓ+t: ≤ Σ_{ℓ≥14} C0hat(ℓ+1)·4.5/((ℓ+t)√(1+(ℓ+t)²)) ≤ Σ_{ℓ≥14} C0hat(ℓ+1)·4.5/(ℓ+10)² = the Tail_L ≤ 0.26156·4.5 ✓.\n\nSo the full piece-3 bound (matching my earlier computation):\nPiece3 ≤ 4.5·(2C₀+0.55)·S₃ + Tail_R + Tail_L ≤ 12.1284·C₀ + 3.33594 + 2.75540 + 1.17703 = 12.1284·C₀ + 7.26837.\n\n(S₃ ≤ 1.3476 with the k≤4-exact + k≥5-telescope; and the main sum over ALL k ≥ 1 not just k ≤ t — since the tail windows are bounded separately, the main sums with the full S₃ overestimate ⟹ fine: main_R ≤ (C₀+0.55)·Σ_{k: 1≤k≤t} 4.5/(k√(1+k²)) ≤ (C₀+0.55)·4.5·S₃ ✓ overestimate OK; main_L ≤ C₀·4.5·S₃ ✓.)\n\n**Lean formalization plan.** The fiberwise steps (mapping zeros to window indices and bounding fiber sums by C0hat counts) — how did LiCircleBound do the dyadic version? `dyadic_family_le` (generic machine via Finset.sum_fiberwise_of_maps_to with t := Ico 1 (J+1)) + `tsum_dyadic_log` + ENNReal.tsum_fiberwise. I should read those to clone the pattern. That's for the TAIL tsums (infinite). For the MAIN range (k ≤ t, t-dependent — infinitely many intervals as t varies but for FIXED t it's a finite set of windows...): hmm, for fixed t, the main range k ≤ t is finitely many windows — but the ZERO set in each window is finite, and the total main sum is over zeros with x ≤ t+1-ish, a finite set (bounded ball). So main = a FINSET sum, bounded by grouping: for each zero in the main finset, its interval k = ⌊x⌋, map to bucket, bound fiber cardinality... The finset version: `Finset.sum_fiberwise_of_maps_to`-style, or simpler: since the main finset is finite, bound the sum by Σ over ALL windows k = 1..K (K = ⌈t⌉) of (count bound)·weight — where \"count bound\" is via ZeroCountProp per window. The simplest Lean encoding: \n\nMain_R_finset := zeros in F_R(t) := {ρ : x_ρ ∈ [1, t+1), γ > t} (a finite ball: |γ| ≤ 2t+1 ⟹ finite_subtype_norm_lt). For ρ ∈ F_R: k(ρ) := ⌊x_ρ⌋ ∈ {1..⌈t⌉−1-ish}. ∑_{ρ ∈ F_R} 4.5·m/(x√(1+x²)) ≤ ∑_{ρ ∈ F_R} 4.5·m/(k(ρ)√(1+k(ρ)²)). Group: = Σ_{k=1..K} Σ_{ρ ∈ F_R, k(ρ)=k} 4.5·m/(k√(1+k²)) ≤ Σ_k 4.5·(count bound_k)/(k√(1+k²)) where count bound via: fiber maps into zeroWindow(t+k) (γ ∈ [t+k, t+k+1) — need k(ρ) = k ⟹ x ∈ [k, k+1), γ = t+x ∈ [t+k, t+k+1) ✓ so fiber ⊆ zeroWindow(t+k) image) ⟹ fiber mult-sum ≤ C0hat(t+k+1) ≤ C0hat(2t+1) ≤ C₀+0.55 (k ≤ t).\n\nIn Lean, rather than Finset.sum_fiberwise, maybe simplest: ∑_{ρ ∈ F} w(ρ) ≤ ∑_{ρ ∈ F} W(k(ρ))·m(ρ) and then bound ∑_{ρ ∈ F} W(k(ρ))·m(ρ) ≤ Σ_{k ∈ k-image} W(k)·(fiber mult-sum) — that IS sum_fiberwise. The dyadic machine in LiCircleBound (`dyadic_family_le`) did exactly this for finite finsets. Let me look at it before writing.\n\nAlso for the TAILS (infinite): the pattern from `zero_tail_inv_sq_le` (journal-031): dyadic fiber machine + ENNReal.tsum_fiberwise + ofReal_tsum_of_nonneg. I'll clone.\n\nThis is a big build (~600-900 lines estimated). Sub-stages:\n- **5f-ii-3a**: the per-term bound + pointwise far-term ≤ g(ρ) + summability of g + norm-tsum ≤ tsum-g reduction + the S₃ numeric brick (Σ_{k≥1} 1/(k√(1+k²)) ≤ 1.3476: 4 exact terms + telescope) + the weight-sum bricks W₀/W₁/W₂ (Σ_{k≥11}: 1/k² ≤ 0.1, log k/k² ≤ 0.3303, loglog k/k² ≤ 0.1269) + left-tail bricks A₀/A₁/A₂ (Σ_{j≥14} over (j+10)²). [numeric machine]\n- **5f-ii-3b**: the interval/window infrastructure: k(ρ) := ⌊|t−γ|⌋ buckets, fiber ⊆ zeroWindow image, count bounds via ZeroCountProp (main) / C0hat(j+1) via conj (left tail) / C0hat(2t+j+1) (right tail), NoLowZeros emptiness. [fiber machine]\n- **5f-ii-3c**: assembly: main ≤ (2C₀+0.55)·4.5·S₃, tails ≤ explicit, piece3 ≤ 12.1284·C₀ + 7.2684. Then 5f-iii.\n\nHmm wait, actually — let me reconsider the total structure once more to minimize Lean pain. \n\nALTERNATIVE much simpler encoding: forget the k-buckets for the MAIN range too. Bound:\n∑_{ρ far} 4.5·m/(x√(1+x²)) ≤ ∑_{ρ far} 4.5·m·w(x) where w(x) = 1/(x√(1+x²)) is DECREASING in x. \n\nFor the RIGHT side (γ > t+1): sort by γ... no, the window approach is the way.\n\nActually — SIMPLEST POSSIBLE main treatment: the main sum ≤ Σ over the main finset of 4.5·m/(x√(1+x²)) and use x ≥ 1 flat for... no: 4.5·(count)·1 = 4.5·(2t·C₀-ish) — diverges in t. No.\n\nOK the bucket structure is necessary. Let me look at the LiCircleBound dyadic machine to see how much I can clone. Let me read `dyadic_family_le` and `zero_tail_inv_sq_le`.\n\nAlso — one more simplification available: since BOTH main sides use the uniform C₀(+0.55) rate and weight Σ ≤ S₃, I can MERGE left+right mains into ONE bucket family: buckets k ≥ 1, bucket k = zeros with x ∈ [k, k+1) (BOTH sides). Fiber ⊆ zeroWindow(t+k) ∪ zeroWindow(t−k−1) (two windows) ⟹ fiber mult ≤ C0hat(t+k+1) + C0hat(t−k) ≤ (C₀+0.55) + C₀ for k ≤ t−3. For t−3 < k ≤ t: left part empty (or ≤ window bound — but the window [t−k−1, t−k] has t−k−1 < 2, ZeroCountProp doesn't apply; use NoLowZeros: [t−k−1, t−k] with k > t−3 ⟹ t−k < 5, and k ≤ t ⟹ t−k−1 ≥ −1... wait k ≤ t ⟹ t−k−1 ≥ −1: window ⊂ [−1, 5] ⊂ (−14, 14) ⟹ empty by NoLowZeros ✓). For k ∈ (t, t+13]: left part: γ ∈ (t−k−1, t−k] ⊂ [t−k−1, t−k] with t−k ∈ [−13, 0) and t−k−1 ≥ −14... empty-ish (|γ| ≤ 14 ✓ boundary care) ⟹ empty. Right part: γ ∈ [t+k, t+k+1), count ≤ C0hat(t+k+1) ≤ C0hat(2k+1) (k > t). For k > t+13: left part γ < −13: count ≤ C0hat(k−t+1) ≤ C0hat(k+1)·... (conj).\nSo unified bucket k:\n- k ≤ t: mult ≤ C₀ + (C₀+0.55) [+0 for the empty cases].\n- t < k ≤ t+13: mult ≤ C0hat(2k+1).\n- k > t+13: mult ≤ C0hat(2k+1) + C0hat(k−t+1)... hmm wait for k > t+13, right window count ≤ C0hat(t+k+1) ≤ C0hat(2k+1) ✓ and left window (conj) ≤ C0hat(k−t) ≤ C0hat(k)... hmm: left window [t−k−1, t−k], |γ| ∈ [k−t, k−t+1] = zeroWindow(k−t) (needs k−t ≥ 2 ⟺ k ≥ t+2 ✓). Count ≤ C0hat(k−t+1) ≤ C0hat(k+1).\nSo:\n- k > t+13: mult ≤ C0hat(2k+1) + C0hat(k+1) ≤ 2·C0hat(2k+1) (k+1 ≤ 2k+1 ✓).\n\nThen: Piece3 ≤ Σ_{k=1}^{⌊t⌋} 4.5·(2C₀+0.55)/(k√(1+k²)) + Σ_{k>t} 4.5·2·C0hat(2k+1)/(k√(1+k²))\n≤ 4.5·(2C₀+0.55)·S₃ + 9·Σ_{k≥11} C0hat(2k+1)/k².\n\nWith the unified tail = 9·[0.433·(0.8329·W₀+W₁)+0.886·(0.3475·W₀+W₂)+2.9·W₀] = 9·0.61231 = 5.5108. vs my split tails (2.7554+1.1770 = 3.9324) — the unified tail is 1.58 WORSE (it charges the left tail the C0hat(2k+1) rate instead of C0hat(j+1) with the (j+10)² weight). Piece3 ≤ 12.1284·C₀ + 3.33594+5.5108 = 12.1284·C₀ + 8.8467. Assembly: 1+2.7+[12.1284·2.9658+8.8467]+0.09+0.6 = 1+2.7+35.964+8.847+0.09+0.6 = 49.2. Need ≤ 48.57 (f ≤ −0.568 ⟺ const ≤ 48.568): 49.2 > 48.57 FAILS. So the unified tail breaks it — the split tails (with the left tail's sharper (j+t)² weight) are NECESSARY. OK, keep the left/right split.\n\nAlright — but NOTE: for the left side, the weight uses x ≥ t+|γ| ≥ t+j ⟹ 1/(x√(1+x²)) ≤ 1/((t+j)√(1+(t+j)²)) ≤ 1/(t+j)² ≤ 1/(10+j)². And I claimed Tail_L ≤ 0.26156·4.5. But in the unified bucket view, the left-tail bucket k corresponds to j = k−t... I had: left tail ≤ Σ_{ℓ≥14} C0hat(ℓ+1)·4.5/(ℓ+10)² ✓.\n\nLet me also double check the RIGHT tail brick values: W₀ = Σ_{k≥11} 1/k². For the Lean proof I need these as explicit lemmas. The antitone-integral comparison: Σ_{k≥11} f(k) ≤ ∫₁₀^∞ f for f antitone on [10,∞)... the pattern in this file: `AntitoneOn.tsum_comp_add_le_integral` gives ∑'_{n:ℕ} f(n+c+1) ≤ ∫_{Ioi c} f. For Σ_{k≥11} f(k) = ∑'_{n} f(n+11) ≤ ∫₁₀^∞ f ✓ (c = 10, n+10+1 = n+11 ✓). Need: f antitone on Ici 10, integrable on Ioi 10, explicit integral value.\n\nThe three right-tail functions:\n- f(x) = 1/x²: antitone ✓, ∫₁₀^∞ = 1/10. W₀ ≤ 0.1.\n- f(x) = log x/x²: antitone on [10,∞) ✓ (shown pattern), ∫₁₀^∞ = (log 10+1)/10 = 0.33026. W₁ ≤ 0.3303. (The antiderivative −(log x+1)/x — SAME as the existing `hasDerivAt_neg_log_add_one_div` in this file!! Reusable ✓.)\n- f(x) = log(log x)/x²: antitone on [10,∞): derivative (1/(x log x)·x² − 2x·loglog x)/x⁴ = (1/log x − 2 loglog x)/x³ ≤ 0 ⟺ 1 ≤ 2·log x·loglog x: at x = 10: 2·2.30259·0.83403 = 3.841 ≥ 1 ✓ and increasing. ∫₁₀^∞ loglog x/x² dx = [−loglog x/x]₁₀^∞ + ∫₁₀^∞ 1/(x²·log x) dx = loglog(10)/10 + ∫₁₀^∞ 1/(x² log x) dx. Bound the second: ≤ (1/log 10)·∫₁₀^∞ 1/x² = 1/(10·log 10) = 0.04343. So ∫ ≤ 0.083403+0.04343 = 0.126833. W₂ ≤ 0.1269. The antiderivative for the first part: −loglog x/x, and the second integral bounded via comparison 1/(x² log x) ≤ (1/log 10)/x². In Lean: split ∫₁₀^∞ loglog/x² = ... hmm, the clean way: antiderivative of loglog x/x² is NOT elementary, but I can do: integration by parts manually OR bound directly: loglog x/x² = d/dx[−loglog x/x] − 1/(x² log x)·(−1)·... d/dx[−loglog x/x] = −(1/(x log x)·x − loglog x)/x² = (loglog x − 1/log x)/x². So loglog x/x² = d/dx[−loglog x/x] + 1/(x² log x). Then ∫₁₀^∞ loglog/x² = [−loglog x/x]₁₀^∞ + ∫₁₀^∞ 1/(x² log x) dx = loglog(10)/10 + ∫₁₀^∞ 1/(x²log x). And ∫₁₀^∞ 1/(x² log x) dx ≤ (1/log 10)·∫₁₀^∞ 1/x² dx = 0.04343 — via measure_mono/integral_mono (both integrable: 1/(x² log x) ≤ 1/(x²·log 10) ✓). In Lean this is doable: integral_congr + integral_mono_ae.\n\nThe left-tail functions (weights 1/(x+10)², x ≥ 13):\n- f = 1/(x+10)²: ∫₁₃^∞ = 1/23. A₀ ≤ 1/23 = 0.0434783.\n- f = log x/(x+10)²: antiderivative −log x/(x+10) + (1/10)·log(x/(x+10)) — messy but provable via HasDerivAt quotient rules. ∫₁₃^∞ = 0 − [−log 13/23 + (1/10)·log(13/23)] = log(13)/23 + (1/10)·log(23/13) = 0.11152+0.05710 = 0.16862. A₁ ≤ 0.16862.\n  Hmm wait: the antiderivative at ∞: −log x/(x+10) → 0 ✓ and (1/10)log(x/(x+10)) → (1/10)·log 1 = 0 ✓. At 13: −log(13)/23 + (1/10)·log(13/23) = −0.11152 − 0.05710 = −0.16862. Integral = 0 − (−0.16862) = 0.16862 ✓.\n- f = loglog x/(x+10)²: same by-parts trick: loglog x/(x+10)² = d/dx[−loglog x/(x+10)] + 1/((x+10)·x·log x)·... d/dx[−loglog x/(x+10)] = −(1/(x log x))/(x+10) + loglog x/(x+10)². So f = d/dx[−loglog x/(x+10)] + 1/(x·log x·(x+10)). ∫₁₃^∞ = loglog(13)/23 + ∫₁₃^∞ 1/(x log x (x+10)) dx ≤ 0.94086/23 + (1/log 13)·∫₁₃^∞ 1/(x(x+10)) dx. And ∫₁₃^∞ 1/(x(x+10)) dx = (1/10)·log(x/(x+10))|₁₃^∞ = 0 − (1/10)·log(13/23) = (1/10)·log(23/13) = 0.05710. So A₂ ≤ 0.040907 + (1/2.56495)·0.05710 = 0.040907+0.022262 = 0.063169. Use A₂ ≤ 0.06317.\n  Hmm, in Lean: 1/(x·log x·(x+10)) ≤ (1/log 13)·1/(x(x+10)) for x ≥ 13 ✓ then the partial-fraction integral. And ∫ 1/(x(x+10)) = (1/10)(log x − log(x+10)): antiderivative (1/10)·log(x/(x+10)) — provable.\n\nWait, for A₁ I need log(23/13) and log 13 explicit: log 13 ≤ 2.56495 (e^2.56495 ≥ 13? e^2.56495 = e^2.5·e^0.06495 = 12.1825·1.06711 = 13.0001 ✓ barely). Use log 13 ≤ 2.5650. log(23/13) = log 23 − log 13: need log(23/13) ≤ 0.5710: e^0.5710 = 1.7700 ≥ 23/13 = 1.76923 ✓. These are certified by the exp-partial-sum trick (as done for log 3 ≤ 1.1 in this file: Real.sum_le_exp_of_nonneg).\n\nAnd log 10 ≤ 2.3026: e^2.3026 ≥ 10 ✓ (standard). loglog 10 = log(log 10) ≤ log 2.3026 ≤ 0.8341: e^0.8341 = 2.3028 ≥ 2.3026 ✓. loglog 13 ≤ log 2.5650 ≤ 0.9410: e^0.941 = 2.5627 < 2.5650?? e^0.9410: e^0.9 = 2.4596, e^0.041 = 1.04185: 2.4596·1.04185 = 2.5625 < 2.565. So log 2.565 > 0.941. loglog 13 = log(2.56495) — need upper bound: 2.56495 ≤ e^0.9411? e^0.9411 = 2.5628·... still < 2.565. Try 0.942: e^0.942 = 2.4596·e^0.042 = 2.4596·1.04289 = 2.5651 ≥ 2.56495 ✓. So loglog 13 ≤ 0.942. OK, these are all certifiable with enough digits.\n\nAlright. This is a big but well-defined build. Let me also reconsider: do I really need A₁, A₂ (the log/loglog left-tail bricks)? The left tail ≤ Σ_{j≥14} C0hat(j+1)·4.5/(j+10)² — could I instead bound C0hat(j+1) ≤ C0hat(2·(j−13)+... no. Alternatively use fewer pieces: C0hat(j+1) ≤ 0.433·log(j+3) + 0.886·loglog(j+3) + 2.9 ≤ 0.433·log(3j)+0.886·loglog(3j)+2.9 ≤ ... ≤ (0.433+0.886)·log(3j) + 2.9 (loglog ≤ log): = 1.319·(log 3 + log j) + 2.9. Then Tail_L ≤ 4.5·Σ[1.319·(1.0986+log j)+2.9]/(j+10)² = 4.5·[1.319·(1.0986·A₀ + A₁) + 2.9·A₀] — still needs A₁ (log j sum). A₂ avoidable: saves one brick, costs: 1.319 vs (0.433 + 0.886·loglog/log): at j = 14: loglog(17)/log(17) = 1.0404/2.8332 = 0.3672: so 0.886·loglog(3j) ≤ 0.886·log(3j)·0.367-ish — the 1.319 merge loses ≈ 0.886·(1−0.36)·log ≈ 0.57·log(j)-ish ≈ per sum: 0.57·A₁·4.5·... ≈ 0.57·0.16862·4.5 ≈ 0.43. Hmm, loses 0.43 in Tail_L: 1.177 → 1.61. Total piece3: 12.1284·C₀ + 3.33594+2.7554+1.61 = 12.1284·C₀ + 7.70. Assembly const: 35.964+7.70+1+2.7+0.09+0.6 = 48.05 ≤ 48.57 ✓ margin 0.52. Hmm — saves proving A₂ but costs 0.4 margin. Actually proving A₁ and A₂ are similar difficulty (same by-parts pattern). Keep both for margin. Actually — wait, alternatively drop A₁ too: bound log j/(j+10)² ≤ log(j)·1/(j+10)² and log j ≤ (j+10)/e·... log j ≤ (j+10)/e?? Then Σ log j/(j+10)² ≤ (1/e)·Σ 1/(j+10) = diverges. No. Use log j ≤ √(j+10)·c? Σ √(j+10)/(j+10)² = Σ (j+10)^{−3/2} converges: ≤ ∫₁₃^∞ (x+10)^{-3/2} = 2/√23 = 0.417. And log j ≤ (2/e)·√j ≤ (2/e)·√(j+10)·... log j ≤ (j+10)^{1/2}·(2/e)·(j/(j+10))^{1/2}-ish ≤ 0.7358·√(j+10). Then A₁ ≤ 0.7358·0.417·... = 0.3069 vs 0.16862 — loses 0.14·0.433·4.5 ≈ 0.27. Meh, keep A₁ proper.\n\nOK. FINAL numeric bricks to prove (all via the antitone-integral pattern):\nRight tail (Σ over k ≥ 11, i.e. tsum over n of f(n+11) ≤ ∫_{Ioi 10} f):\n- RW₀: Σ_{k≥11} 1/k² ≤ 0.1 (= 1/10).\n- RW₁: Σ_{k≥11} log k/k² ≤ 0.3303 (integral (log 10+1)/10 = 0.330259; use 0.3303).\n- RW₂: Σ_{k≥11} loglog k/k² ≤ 0.1269 (0.126833; use 0.1269).\nLeft tail (Σ over j ≥ 14, i.e. f(n+14) ≤ ∫_{Ioi 13}):\n- LA₀: Σ_{j≥14} 1/(j+10)² ≤ 1/23 (0.043478).\n- LA₁: Σ_{j≥14} log j/(j+10)² ≤ 0.1687 (0.16862; use 0.1687).\n- LA₂: Σ_{j≥14} loglog j/(j+10)² ≤ 0.0632 (0.063169; use 0.0632).\nMain:\n- S₃: Σ_{k≥1} 1/(k√(1+k²)) ≤ 1.3476 (4 exact + telescope 1/4).\nCount-function bridges:\n- C0hat(2k+1) ≤ 0.433·(log k + 0.833) + 0.886·(loglog k + 0.3475) + 2.9 for k ≥ 11. (via 2k+3 ≤ 2.3k ⟹ log(2k+3) ≤ log k + log 2.3 ≤ log k + 0.8329; loglog ≤ loglog k + 0.8329/log 11 ≤ +0.3475.)\n- C0hat(j+1) ≤ 0.433·(log j + 0.1942) + 0.886·(loglog j + 0.0736) + 2.9 for j ≥ 14. (log(j+3) ≤ log j + log(17/14) ≤ log j + 0.1942; loglog ≤ +0.1942/log 14 ≤ +0.0736.)\n- C0hat(t+k+1) ≤ C0hat(2t+1) ≤ C₀ + 0.55 for 1 ≤ k ≤ t (C0hat_mono + the 0.55 increment lemma: C0hat(2t+1) − C0hat(t+1) ≤ 0.433·log 2 + 0.886·log 2/log(t+3) ≤ 0.30011+0.23903·... = 0.53914 ≤ 0.55 ✓).\n\nHmm — wait, actually for the main I don't need the increment lemma per k: main_R ≤ Σ_{1≤k≤t} C0hat(t+k+1)·w_k ≤ C0hat(2t+1)·Σ w_k ✓ (mono) and then the ONE increment lemma C0hat(2t+1) ≤ C₀+0.55. ✓ simpler.\n\nAlso need C0hat monotone — `C0hat_mono` exists (used in LiGapCircles). ✓\n\nNow — the summability/fiber machinery for the tails. Let me look at how `zero_tail_inv_sq_le` did the dyadic tail (journal-031's machine: dyadClass, fiber bounds, ENNReal.tsum_fiberwise). For my tails:\n- Right tail: zeros with x > t (γ > 2t): map to window index j(ρ) = ⌊γ − 2t⌋... hmm wait, my right tail is over k = ⌊x⌋ > t. As a window-index sum: j = k − ... I set it up as: right tail = Σ_{ρ: γ>2t} 4.5·m/(x√(1+x²)) with x = γ−t. Window of ρ: γ ∈ [2t+n, 2t+n+1), n ≥ 0: x ∈ [t+n, t+n+1): weight ≤ 4.5/(t+n)² ≤ 4.5/((10+n)·...) hmm wait — earlier I had the right tail over k = ⌊x⌋ > t with count C0hat(t+k+1) ≤ C0hat(2k+1). In window-index n = k−t... k > t, k ≥ ⌊t⌋+1. n = k − t ∈ [0, ...): not integral. UGH — the bucket boundaries k (integers, x ∈ [k, k+1)) vs window boundaries (γ ∈ [t+k, t+k+1)) — with k > t non-integral boundary t. The right-tail zeros: γ > 2t (x > t). Their buckets k = ⌊x⌋ ≥ ⌊t⌋ ≥ 10... hmm, x > t ⟹ k = ⌊x⌋ ≥ ⌊t⌋ (if t not integer) or ≥ t (if integer). The bucket-k window [t+k, t+k+1) with k ≥ 10: count ≤ C0hat(t+k+1), and k > t... no wait — k ≥ ⌊t⌋ but I need k > t for the t+k+1 ≤ 2k+1 bound! k > t ⟺ k ≥ ⌊t⌋+1 (k integer). Buckets k ∈ {⌊t⌋} with x ∈ [k, t]: zeros with γ ∈ [t+k, 2t]: these are MAIN-range (k ≤ t — k = ⌊t⌋ ≤ t ✓). So main buckets: k = 1..⌊t⌋ (x ∈ [1, t]∪[⌊t⌋-part...) — main = x ≤ t, buckets 1..⌊t⌋ (the last bucket partial x ∈ [⌊t⌋, t] ⊂ [k, k+1) ✓ fine). Tail buckets: k ≥ ⌊t⌋+1 ⟹ k > t ✓ ⟹ t+k+1 ≤ 2k+1 ⟺ t ≤ k ✓.\n\nSo RIGHT side buckets k = 1..∞ (all), with count bound C0hat(t+k+1) ≤ {C0hat(2t+1) ≤ C₀+0.55 for k ≤ t; C0hat(2k+1) for k > t}. And the RIGHT tail as a tsum over buckets k ≥ 11 (k > t ≥ 10 ⟹ k ≥ 11 ✓): Σ_{k≥11} C0hat(2k+1)·4.5/(k√(1+k²)) — note k > t not exactly k ≥ 11 (t could be 10.5, k ≥ 11 ✓ since k > 10.5 ⟹ k ≥ 11 ✓; t = 10: k > 10 ⟹ k ≥ 11 ✓). So tail ≤ Σ_{k≥11}-sum REGARDLESS of t ✓ clean. The tail bucket family is indexed by k ∈ {11, 12, ...} = fixed infinite family ✓.\n\nBut the fiberwise machine: the tail tsum is over ZEROS, grouped by bucket k(ρ) = ⌊x_ρ⌋ ≥ 11. Map ρ ↦ k(ρ) ∈ {k : k ≥ 11} ⊆ ℕ. Fiber sums ≤ C0hat(2k+1)·... So I need: ∑'_{ρ: k(ρ) ≥ 11} 4.5·m/(x√(1+x²)) ≤ ∑'_{ρ} 4.5·m·W(k(ρ)) [W(k) = 1/(k√(1+k²))] = Σ'_{k≥11} W(k)·(fiber mult-sum) ≤ Σ'_{k≥11} W(k)·C0hat(2k+1). The middle equality = ENNReal.tsum_fiberwise (or an ℝ version). Let me check what's in Mathlib: `tsum_fiberwise`? There's `ENNReal.tsum_fiberwise` (used in LiCircleBound) and for ℝ≥∞... For ℝ: `Summable.tsum_fiberwise`? I don't remember. The LiCircleBound pattern (journal-031): \"the dyadic fiber machine + ENNReal.tsum_fiberwise + ofReal_tsum_of_nonneg assembly\". So: convert to ENNReal, fiberwise, convert back. I'll clone from LiCircleBound's `zero_tail_inv_sq_le` proof — let me read it now.\n\nSimilarly LEFT tail: buckets via ℓ(ρ) = ⌊|γ|⌋ ≥ 14 (zeros with γ < 0): weight 4.5·m/(x√(1+x²)) ≤ 4.5·m/(t+|γ|)² ≤ 4.5·m/(10+ℓ)² (|γ| ≥ ℓ). Fiber ℓ ⊆ conj-image of zeroWindow(ℓ) ⟹ mult ≤ C0hat(ℓ+1). Sum ≤ Σ_{ℓ≥14} C0hat(ℓ+1)·4.5/(10+ℓ)² ≤ 4.5·[0.433·(0.1942·A₀+A₁)+0.886·(0.0736·A₀+A₂)+2.9·A₀].\n\nAnd the MAIN: buckets k = 1..⌊t⌋: a FINITE family — but with t-dependent range. As a finset machine: the main zeros are in a finite ball ⟹ finite finset F. ∑_{ρ ∈ F} 4.5·m·W(k(ρ)) — with k(ρ) ∈ {1..⌊t⌋} — use Finset.sum_fiberwise_of_maps_to (clone of dyadic_family_le's grouping) into the index finset Ico 1 (⌊t⌋+1), each fiber ≤ count bound. The count bound per bucket: fiber ⊆ (zeroWindow(t+k) ∪ zeroWindow(t−k−1))-image ⟹ ≤ C0hat(t+k+1) + C0hat(t−k) ≤ (C₀+0.55) + C₀ (need t−k−1 ≥ 2 ⟺ k ≤ t−3; for k ∈ (t−3, t]: left window ⊂ (−14,14) ⟹ fiber left-empty by NoLowZeros ⟹ ≤ C0hat(t+k+1) + 0 ≤ C₀+0.55 ≤ 2C₀+0.55 ✓ same bound ✓ — so the uniform bound 2C₀+0.55 works for ALL k ≤ t ✓ with the NoLowZeros caveat absorbed).\n\nWait, actually careful: for k ∈ (t−3, t], the left window [t−k−1, t−k]: t−k−1 ∈ [−2, 2): the window could contain zeros with γ ∈ (−14, 14) — none by NoLowZeros ✓ — BUT the ZeroCountProp bound doesn't apply (window start < 2). So fiber ≤ right-window count only ≤ C₀+0.55 ≤ 2C₀+0.55 ✓. Fine, uniform.\n\nSo main ≤ Σ_{k=1}^{⌊t⌋} 4.5·(2C₀+0.55)/(k√(1+k²)) ≤ 4.5·(2C₀+0.55)·S₃ ≤ 4.5·(2C₀+0.55)·1.3476 = 12.1284·C₀ + 3.33594.\n\nHmm wait — but actually the main bucket fiber for bucket k maps to zeroWindow(t+k) ∪ zeroWindow(t−k−1): the mult-sum over the fiber ≤ sum over the two windows. But the fiber is a subset of the subtype zeros with k(ρ) = k — need an image-bridge like in near_sum_refPoint_le (Finset.sum_image with Subtype.val injective). Fine.\n\nNow, let me also double-check the per-term bound derivation once more (it drives W(k) = 1/(k√(1+k²))):\n‖seriesDiffTerm s s₀ ρ‖ = ‖m·(1/(s−ρ) − 1/(s₀−ρ))‖ = m·‖(s₀−s)/((s−ρ)(s₀−ρ))‖ = m·‖s₀−s‖/(‖s−ρ‖·‖s₀−ρ‖) ≤ 4.5·m/(x·√(1+x²)) where:\n- ‖s₀−s‖ ≤ 4.5 (from hsdiffle in one_div_diff_le — reusable: s₀ − s = (2−s.re:ℝ)✓, |2−s.re| ≤ 4.5 given −5/2 ≤ s.re ≤ 3 ✓).\n- ‖s−ρ‖ ≥ |im(s−ρ)| = |t−γ| = x ✓.\n- ‖s₀−ρ‖ ≥ √(1+x²): ‖s₀−ρ‖² = (2−β)²+(t−γ)² ≥ 1+x² (β = re ρ ∈ (0,1) ⟹ |2−β| > 1 ✓). So ‖s₀−ρ‖ ≥ √(1+x²) ✓.\nFor the bucket: x ≥ k ⟹ x√(1+x²) ≥ k√(1+k²) (the function u√(1+u²) is monotone for u ≥ 0: derivative √(1+u²)+u²/√(1+u²) > 0 — or just: u₁ ≤ u₂ ⟹ u₁√(1+u₁²) ≤ u₂√(1+u₂²) by mul_le_mul of u₁≤u₂ and √(1+u₁²)≤√(1+u₂²) ✓ no calculus needed).\nSo far-term ≤ 4.5·m/(k√(1+k²)) ✓.\n\nAnd in the LEFT tail: x = t+|γ| ≥ t+ℓ ⟹ 1/(x√(1+x²)) ≤ 1/((t+ℓ)√(1+(t+ℓ)²)) ≤ 1/(t+ℓ)² ≤ 1/(10+ℓ)² ✓ (using √(1+u²) ≥ u).\n\nNOW — the overall piece-3 statement. The far series is `∑' ρ, if ρ ∈ nearZerosSub t then 0 else seriesDiffTerm s s₀ ρ`. Piece 3:\n```\ntheorem far_series_le (hZC : ZeroCountProp) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t)\n    {s : ℂ} (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) (hζ : riemannZeta s ≠ 0) :\n    ‖∑' ρ, if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s (2 + t*I) ρ‖\n      ≤ 12.1284 * C0hat (t+1) + 7.2684\n```\nWait — the constants: 12.1284·C₀ + 3.33594 + 2.75540 + 1.17703 = 12.1284·C₀ + 7.26837. Round: 7.2684. So ≤ 12.1284·C0hat(t+1) + 7.2684.\n\nHmm, do I need hζ? For the far terms: 1/(s−ρ) needs s ≠ ρ: if s = ρ then s is a nontrivial zero ⟹ ζ(s) = 0, excluded by hζ ✓. Also s could be a nontrivial zero not equal... no, s = ρ exactly. hζ ⟹ s ≠ ρ for all nontrivial ρ ✓.\n\nLet me now also decide the assembly form for 5f-iii — not needed now, but the constants 12.1284/7.2684 feed it. Fine.\n\n**Build order (sub-stages for piece 3):**\n- **3a**: numeric bricks — S₃ (4 exact terms + telescope), RW₀/RW₁/RW₂ (right-tail weight sums), LA₀/LA₁/LA₂ (left-tail). All antitone-integral + certified numerics. [pure real analysis, no zero machinery]\n- **3b**: count bridges — C0hat(2k+1) bound (k ≥ 11), C0hat(j+1) bound (j ≥ 14), C0hat(2t+1) ≤ C0hat(t+1)+0.55 increment. [real analysis on C0hat]\n- **3c**: per-term bound + g-summability + norm-tsum reduction + the fiber machines (main finset + two tail tsums) + assembly.\n\nEstimated: 3a ~350 lines, 3b ~150, 3c ~500. That's 2 sessions-ish of work. Let me start with 3a.\n\nActually wait — before writing code, let me look at the LiCircleBound dyadic fiber machine to see exactly what patterns to clone for 3c. Let me read the relevant sections (tsum_split_finset, zero_tail_inv_sq_le, dyadic_family_le).","signature":""},{"type":"text","text":"Now let me study the fiber machines in LiCircleBound that I'll clone for the tail sums."},{"type":"tool_use","id":"Grep_21","name":"Grep","input":{"pattern":"lemma dyadic_family_le|lemma zero_tail_inv_sq_le|lemma tsum_split_finset|lemma fiber_tail_le|lemma tsum_dyadic_log|lemma dyadClass_fiber_finite|lemma fiber_mult_count","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiCircleBound.lean","output_mode":"content","-n":true},"extra_content":null}]