[{"type":"thinking","thinking":"Now 5e-v-b: the seriesFun circle bound. Let me design it concretely.\n\n**Target**: for s on the γ-gap circle (‖s‖ = R, R from exists_gapCircle_radius with k ≥ K₀ := some explicit threshold), a bound ‖seriesFun s‖ ≤ C·(log R)² + C_low (C explicit, C_low the symbolic low-zero constant).\n\nThe split by ordinate shells. Let me define the pieces:\n\nThe zeros partition (by |γ| = |ρ.im|):\n- Z0: |γ| ≤ 2 — the LOW set: symbolic constant C_low := Σ_{ρ : |γ| ≤ 2} m_ρ·(1/‖ρ‖·... hmm — actually for the low set, the term is m·|1/(s−ρ)+1/ρ| ≤ m·(1/|s−ρ| + 1/|ρ|) ≤ m·(2/R + 1/‖ρ‖)·... hmm 1/|s−ρ| ≤ 1/(R−3) for ‖ρ‖ ≤ 3 ≤ R/2. So low sum ≤ Σ_{|γ|≤2} m·(2/R + 1/‖ρ‖) = (2/R)·Σ m + Σ m/‖ρ‖ — both fixed finite-set constants. Symbolic: C_low := Σ_{ρ ∈ L} (zeroMult ρ : ℝ)·(2 + 1/‖ρ‖) where L := {ρ | nontrivial ∧ |ρ.im| ≤ 2}.toFinset — and the bound: low sum ≤ C_low (using 2/R ≤ 2 for R ≥ 1 ✓).\n- Z1: 2 < |γ| ≤ R−2 (lower dyadic shells in γ AND in R−|γ|): \n- Z2: R−2 < |γ| ≤ R+2 (critical band — γ-gap needed for strip arcs; re-split for near-axis).\n- Z3: R+2 < |γ| ≤ 2R (upper shells).\n- Z4: |γ| > 2R (far tail).\n\nThe tsum-splitting in Lean: seriesFun s = ∑' over the subtype — split into these 5 finite/infinite parts: Z0, Z1, Z2, Z3 finite (finsums over bounded-ordinate zeros — finite via zerosIn_finite); Z4 infinite (tsum over the subtype filtered). Splitting a tsum over a subtype by a predicate: ∑' ρ, f ρ = ∑' ρ in P, f + ∑' ρ in ¬P... — the cleanest: define the parts via `tsum` over sub-subtypes or use `Summable.tsum_add` chains with indicator functions. This gets heavy. ALTERNATIVE cleaner formalization: bound the WHOLE sum by splitting the NORM-sum: ‖seriesFun s‖ ≤ ∑' ρ, ‖seriesTerm s ρ‖ (norm_tsum_le_tsum_norm + (seriesSummable s).norm) and then bound the NORM tsum — the norm-summand is REAL-valued nonneg: ∑' ρ, ‖seriesTerm s ρ‖ ≤ (the five-part bound) — split the REAL tsum by shells via `tsum_le`-style comparisons... Still need tsum splitting by predicate: `tsum_add_tsum_compl`? For nonneg real functions: ∑'_{full} f = ∑'_{P} f + ∑'_{Pᶜ} f — Mathlib: `tsum_add_tsum_compl (hf : Summable f) (s)`: ∑' x, f x = ∑' x : s, f x + ∑' x : sᶜ, f x? there's `tsum_add_tsum_compl (s : Set α) (hf : Summable f) (hf' : Summable (f ∘ (↑)))...` — signature fiddly with summability-on-subtype requirements. Since my f is nonneg real and summable, the subtype restrictions are summable (Summable.of_norm_bounded / comap... — `Summable.subtype`? there's `Summable.subtype (hf : Summable f) (s : Set α) : Summable (f ∘ (↑) : s → ℝ)`? I believe `Summable.subtype` exists ✓ (Summable.subtype (hf) (s)). \n\nThis is going to be a genuinely long lemma (~400-500 lines). Let me structure it as:\n\n```\nlemma seriesFun_norm_le_on_gapCircle (hZC : ZeroCountProp) {k : ℕ} (hk : K₀ ≤ k)\n    {R : ℝ} {s : ℂ} ... (R the gap radius, s on the circle):\n    ‖seriesFun s‖ ≤ C1 * (Real.log R)^2 + C_low\n```\n\nHmm wait — actually, let me simplify the split: instead of 5 parts, use THREE:\n- A: |γ| ≤ R−2 (the bulk; includes low): term ≤ R/(‖ρ‖·‖s−ρ‖): ‖s−ρ‖ ≥ ||t|−|γ|| ≥ (R−|γ|)·(1/2)-ish (strip) or |re|-split (near-axis)... — hmm the near-axis vs strip split of the POINT s complicates every shell. ALTERNATIVE: handle the near-axis arcs SEPARATELY at the top level: for near-axis s (|im s| < 10): ‖s−ρ‖ ≥ |re s − re ρ| ≥ |re s| − 1 ≥ √(R²−100) − 1 ≥ R/2 − 1: term ≤ R/(‖ρ‖·(R/2−1)) ≤ 4/‖ρ‖ (R ≥ 4): so ‖seriesFun s‖ ≤ 4·Σ_ρ m/‖ρ‖ over ALL zeros — Σ m/‖ρ‖ over all zeros: does it converge? NO! Σ m/‖ρ‖ ~ Σ log γ/γ = ∞. So on near-axis arcs I ALSO need the shell split: term ≤ R/(‖ρ‖‖s−ρ‖) with ‖s−ρ‖ ≥ max(|R−‖ρ‖|, ...) hmm — for near-axis: ‖s−ρ‖ ≥ |re s − re ρ| ≥ |re s| − 1 and ALSO ‖s−ρ‖ ≥ ||s|−|ρ|| = |R − ‖ρ‖|: for ‖ρ‖ ≤ R−2: |R−‖ρ‖| ≥ 2: term ≤ R/(‖ρ‖·max(...)): use ‖s−ρ‖ ≥ |R−‖ρ‖| for ALL points s on the circle ✓ (reverse triangle, no arc split needed!): for ‖ρ‖ ∉ (R−2, R+2): ‖s−ρ‖ ≥ |R−‖ρ‖| ≥ 2·... so:\n  - shell |γ|-dyadic with ‖ρ‖ ∈ [R−2^{j+1}, R−2^j]... \n\nOK here's the cleanest full design — split by ‖ρ‖ (norm shells), using ‖s−ρ‖ ≥ |R − ‖ρ‖| everywhere (no γ-gap needed outside the critical annulus!!) and the γ-gap ONLY for the critical annulus on strip arcs + the |re|-split on near-axis arcs:\n\n- S0: ‖ρ‖ ≤ 2: finite symbolic C₀ := Σ_{‖ρ‖≤2} m·(1 + 1/‖ρ‖)·... terms: |1/(s−ρ)+1/ρ| ≤ 1/(R−2) + 1/‖ρ‖ ≤ 1 + 1/‖ρ‖ (R ≥ 4): C₀ covers it ✓.\n- S1: 2 < ‖ρ‖ ≤ R/2: ‖s−ρ‖ ≥ R−‖ρ‖ ≥ R/2: term ≤ R/(‖ρ‖·R/2) = 2/‖ρ‖: sum over dyadic shells [2^j, 2^{j+1}] (2^j ≤ R/2): count(≤ 2^{j+1}+... windows) — count of {‖ρ‖ ≤ 2^{j+1}}: |γ| ≤ 2^{j+1}: windows ≤ 2·(2^{j+1}+2)·A₀·log(2^{j+1}+3) ≍ 2^{j}·log — times 2/2^j per term: shell sum ≍ A₀·(j+3): summed j ≤ log₂R: O((log R)²) ✓.\n- S2: R/2 < ‖ρ‖ ≤ R−2: ‖s−ρ‖ ≥ R−‖ρ‖: term ≤ R/(‖ρ‖·(R−‖ρ‖)) ≤ 4/(R−‖ρ‖) (‖ρ‖ ≥ R/2... R/‖ρ‖ ≤ 2): shells d = R−‖ρ‖ ∈ [2, R/2]: {‖ρ‖ ∈ [R−2^{j+1}, R−2^j]}: count: |γ| ≤ ‖ρ‖ ≤ R: the count of zeros with ‖ρ‖ in that range: |γ| ∈ [√((R−2^{j+1})²−1)...] — ugh the norm-to-ordinate: zeros with ‖ρ‖ ≥ R−2^{j+1} have |γ| ≥ √(‖ρ‖²−1) ≥ ‖ρ‖−1: |γ| ∈ [R−2^{j+1}−1, R−2^j+...]: count ≍ 2^{j+1} windows·A₀ log — term ≤ 4/2^j: shell ≍ A₀ log R·2^{j+1}·4/2^j = 8A₀ log R per shell ⟹ O((log R)²) total ✓.\n- S3: critical R−2 < ‖ρ‖ < R+2: the γ-gap (strip) / |re|-split (near-axis): term ≤ R/((R−2)·gap): count ≍ 7 windows·A₀ log(R+2): O(Ĉ₀·log R) ✓.\n- S4: R+2 ≤ ‖ρ‖ ≤ 2R: ‖s−ρ‖ ≥ ‖ρ‖−R: term ≤ R/(‖ρ‖(‖ρ‖−R)) ≤ 1/(‖ρ‖−R)·(R/(R+2) ≤ 1): shells e = ‖ρ‖−R ∈ [2, R]: count ≍ 2^{j+1}·A₀ log: term ≤ 1/2^j: O((log R)²) total ✓.\n- S5: ‖ρ‖ > 2R: ‖s−ρ‖ ≥ ‖ρ‖−R ≥ ‖ρ‖/2: term ≤ 2R/‖ρ‖²: dyadic shells [2^j R, 2^{j+1} R]: count ≍ 2^{j+1}R·A₀ log(2^{j+1}R): term ≤ 2R/4^jR² = 2/(4^j R): shell sum ≍ 2^{j+1}R·A₀(j log 2 + log R)·2/(4^j R) = 4A₀(j + log R)/2^j: Σ_{j≥1} ≍ 4A₀(log R)·2 = O(log R) ✓.\n\nAll workable. The Lean formalization burden: the tsum splitting into 6 parts (S0..S5) over the zero subtype — the predicate-based tsum splits via tsum_add_tsum_compl chains (5 splits). Each split needs Summable.subtype justifications. And each part's bound via comparison with the window-count sums.\n\nHonestly, this is ~500-600 lines of careful Lean. This is the biggest single lemma of the project. Let me think about whether there's a SHORTER path to the same conclusion...\n\nALTERNATIVE: use the SPLIT structure of the already-proved bounds differently — the series appears in 5c/5d's form Σ m/(s−ρ) restricted to NEAR zeros... no.\n\nHmm — actually, hold on: maybe use a SOFTER series bound that's still o(R): even O(R^{1/2}) suffices for the squeeze. Does a softer target help? The issue is the critical annulus (γ-gap) and the shell sums (window counts) — both unavoidable in any form. No real saving.\n\nANOTHER ALTERNATIVE — bound the series via the CONVERGENT majorant directly: ‖seriesTerm s ρ‖ = m·R/(‖ρ‖·‖s−ρ‖): for the whole sum, split into {‖ρ‖ ≤ 2R} and {‖ρ‖ > 2R}:\n- {‖ρ‖ > 2R}: ≤ 2R/‖ρ‖²·... as S5 ✓ (needs Σ m/‖ρ‖²-convergence-ish via dyadic windows — or directly via zero_sum_inv_sq: m/‖ρ‖² ≤ (17/12)m/(1+‖γ‖²)·... wait 5e-iii's comparison: 1+‖γ‖² ≤ (17/12)‖ρ‖² for ‖ρ‖ ≥ 2 ⟹ 1/‖ρ‖² ≤ (17/12)/(1+‖γ‖²) — hmm that's 1/‖ρ‖² ≤ (17/12)/(1+‖γ‖²)?? from 1+‖γ‖² ≤ (17/12)‖ρ‖² ⟹ (12/17)(1+‖γ‖²) ≤ ‖ρ‖² ⟹ 1/‖ρ‖² ≤ (17/12)/(1+‖γ‖²) ✓. So Σ_{‖ρ‖>2R} m·2R/‖ρ‖² ≤ 2R·(17/12)·Σ_{‖ρ‖>2R} m/(1+‖γ‖²) — the TAIL of a convergent sum: ≤ 2R·(17/12)·(total T₀) — that's O(R) — TOO BIG (need o(R))! The tail decay matters: Σ_{‖γ‖>X} m/(1+γ²) ≤ (window counts) ≍ log X/X: so 2R·log(R)/R = O(log R) ✓ — via the dyadic window count as in S5 ✓ same work.\n  \nSo the dyadic window sums are unavoidable. FINE.\n\nLet me now think about the LEAN structure to minimize pain. Key sub-lemmas:\n\n(b1) A finset-free way to handle the shell sums: define for [a, b] ordinate intervals: ZI a b := (zerosIn a b) — with the finsum Ncount a b = Σ m. My shell sums are Σ over {ρ : X ≤ ‖ρ‖ < Y} m·(term bound) — convert to ordinate intervals: {X ≤ ‖ρ‖ < Y} ⊆ {zeros : |γ| < Y} (since |γ| ≤ ‖ρ‖) ∪ nothing... and {X ≤ ‖ρ‖} ⊇ {|γ| ≥ X}·... For an UPPER bound on Σ_{X ≤ ‖ρ‖ < Y} m: ≤ Σ_{|γ| < Y} m·... the term bound per zero uses ‖ρ‖ ≥ X: term ≤ 2R/(X·‖s−ρ‖)... I'll bound each shell sum by (count of a WIDER ordinate set)·(max term). The wider sets:\n- {X ≤ ‖ρ‖ < Y} ⊆ {|γ| < Y} (all): count ≤ Ncount(−Y, Y]-ish ≤ 2·Ncount(0, Y]... via symmetry? Ncount(−Y, Y] ≤ A₀·(2Y+1)·log(Y+4) ✓ direct from Ncount_le_of_interval with a := −Y (ha : 0 ≤ −Y fails!) — hmm Ncount_le_of_interval needs 0 ≤ a. Extend: for a < 0: Ncount a b with |a| ≤ b (b ≥ 0): |t| ≤ b for t ∈ [a,b] ✓ log(|t|+3) ≤ log(b+3) ✓ — restate the interval lemma for general a ≤ b with log(max(|a|,|b|)+4)? Let me generalize Ncount_le_of_interval: drop ha : 0 ≤ a; the chain's log argument: |a| + N + 3 ≤ max(|a|,|b|) + (b−a+1) + 3 ≤ 2·max(|a|,|b|) + 4: state: Ncount a b ≤ A₀·(b−a+1)·log(2·max |a| |b| + 4)... the current proof used |a| = a (ha). Generalize: |a| + N + 3 with N ≤ b−a+1: ≤ |a| + b − a + 4: if a ≥ 0: = b+4 ✓ current form; if a < 0 ≤ b: |a| + b − a + 4 = b + 2|a| + 4 ≤ 3b + 4 (|a| ≤ b case) — hmm not always (a = −10, b = 1: |a|+b−a+4 = 10+1+10+4 = 25 ≤ 2·10+4 = 24? 25 > 24 — use 2max+5). Just use 3·max(|a|,|b|) + 5 — loose constants are fine. Let me restate:\n\n`Ncount_le_of_interval {a b} (hab : a ≤ b) : (Ncount a b : ℝ) ≤ A0count * (b - a + 1) * Real.log (3 * max |a| |b| + 5)` — hmm the proof: |a| + N + 3 ≤ |a| + (b−a+1) + 3 — if a ≥ 0: b + 4 ≤ 3b+5 ✓; if a < 0: |a| + b − a + 4 = b + 2|a| + 4 (a<0: −a = |a|): ≤ b + 2M + 4 ≤ 3M + 5 ✓ (b ≤ M ⟹ b + 2M ≤ 3M ✓ +4 ≤ +5 ✓). Rework the proof's log-bound step. Or keep the 0≤a version AND add a negative-side corollary via... the negative windows: Ncount (−b) (−a) for 0 ≤ a ≤ b — the count of zeros with im ∈ (−b, −a] — via Ncount_le_of_interval directly with a' := −b (fails ha)... the proof structure is the same — just redo the log-bound with the general max form. Let me generalize the lemma to (hab : a ≤ b) with the log argument 3·max(|a|,|b|)+5. Actually simpler: TWO lemmas: the current one (0 ≤ a) + `Ncount_le_of_interval_neg {a b} (hb : b ≤ 0) (hab : a ≤ b)` for the negative side via the same chain with log(|a|+...) — for b ≤ 0: t ∈ [a,b]: |t| ≤ |a|: log(|a|+N+3) ≤ ... |a| + (b−a+1) + 3 = b + |a| − a + 4·... a < 0: |a| = −a: |a|+N+3 ≤ −a + (b−a) + 4 = b − 2a + 4 ≤ 2|a| + 4 (b ≤ 0) ≤ 3|a|+5. Symmetric. Or ONE general lemma with the 3M+5 form — cleanest. Let me restate the already-proved one — it's ALREADY PROVED (compiles). I'll add a general wrapper:\n\n`Ncount_le_of_interval_gen {a b} (hab : a ≤ b) : (Ncount a b : ℝ) ≤ A0count * (b - a + 1) * Real.log (3 * (max |a| |b|) + 5)`:\nproof: from Ncount_chain_le directly with the log-bound redone: |a| + N + 3 ≤ 3·max|a||b| + 5: |a| ≤ M ✓; N ≤ b−a+1 ≤ |b|+|a|+1 ≤ 2M+1: |a|+N+3 ≤ M + 2M+1+3 = 3M+4 ≤ 3M+5 ✓. So I can re-derive from Ncount_chain_le a N + the ceil cover with the adjusted log mono. ~30 lines.\n\n(b2) the low-zeros symbolic constant: C_low := Σ over {ρ : ‖ρ‖ ≤ 2 ∧ nontrivial}.toFinset of (zeroMult ρ : ℝ)·(1 + 1/‖ρ‖). Finset of subtype elements — hmm: the zeros with ‖ρ‖ ≤ 2: finite set of ℂ (compact-finiteness) — as a subtype finset: {ρ : subtype | ‖ρ‖ ≤ 2}.toFinset via the Set.Finite (the LiSkeleton/LiSeries finite_subtype pattern ✓ banked). C_low := ∑ ρ ∈ that, (zeroMult ρ : ℝ)·(1 + 1/‖(ρ:ℂ)‖) ✓ well-defined.\n\n(b3) the shell-sum bounds: for each shell family, a lemma: Σ_{ρ : shell} m·(term bound) ≤ count·(max term) — the shells as subtype-finsets... These sums over {ρ : P ρ} (subtype sub-finsets): bound by (∑ over the covering ordinate-interval finset of m)·(max term) — monotonicity via Finset.sum_le_sum_of_subset_of_nonneg (subtype-finsets) ✓.\n\n(b4) the tsum split: ‖seriesFun s‖ ≤ ∑' ρ, ‖seriesTerm s ρ‖ (norm_tsum_le_tsum_norm (seriesSummable s).norm) then split the real nonneg tsum:\n∑' ρ, f ρ = Σ_{S0} + ∑'_{S1..S5 parts}: via tsum_add_tsum_compl — signature: `tsum_add_tsum_compl {s : Set α} (hf : Summable f) (hf₁ : Summable (f ∘ (↑) : s → ℝ))?? : ∑' x, f x = ∑' x : s, f ↑x + ∑' x : sᶜ, f ↑x`? something like that. The subtype-summabilities: from Summable.subtype (hf s). For nonneg f the ≤ chains via Summable.tsum_le_tsum / tsum_subtype_le... \n\nThis is genuinely ~600 lines. It's the heart of 5e-v and unavoidable. Let me get going — but FIRST, given the size, maybe reconsider once more whether the FULL norm-tsum split is needed, or whether I can shortcut via a DIFFERENT decomposition of seriesFun that reuses 5c/5d's near-sum analysis...\n\nHonestly — no shortcut. The series circle bound is the content of the partial-fraction growth argument. Proceed.\n\nActually — WAIT. One more simplification available: I don't need to split by BOTH norm and ordinate cleverly; the simplest uniform scheme: split the zeros by ORDINATE dyadic shells only, using:\n- |1/(s−ρ)+1/ρ| = R/(‖ρ‖‖s−ρ‖) with ‖ρ‖ ≥ |γ| (so 1/‖ρ‖ ≤ 1/|γ| for |γ| ≥ 1) and ‖s−ρ‖ ≥ max( |R−‖ρ‖| , |t−γ| ):\n  - for the critical band (|γ| near R): the γ-gap.\n  - for the rest: ‖s−ρ‖ ≥ |R − ‖ρ‖| and ‖ρ‖ ∈ [|γ|, |γ|+1] ⟹ |R−‖ρ‖| ≥ |R−|γ|| − 1: for ||γ|−R| ≥ 3: ‖s−ρ‖ ≥ ||γ|−R| − 1 ≥ ||γ|−R|/2 (||γ|−R| ≥ 3 ≥ 2... (x−1 ≥ x/2 ⟺ x ≥ 2 ✓ for ||γ|−R| ≥ 3 wait need ≥ 2: ||γ|−R| ≥ 3 ⟹ −1 version ≥ 2 ≥ (3)/2-ish — let me just use ‖s−ρ‖ ≥ ||γ|−R| − 1 ≥ (||γ|−R|)/2 for ||γ|−R| ≥ 2 ✓).\n  \nSo with the ordinate split:\n- |γ| ≤ 3 (low): symbolic C_low.\n- 3 < |γ| ≤ R−2: ‖s−ρ‖ ≥ (R−|γ|−1) ≥ (R−|γ|)/2 (R−|γ| ≥ 2 ✓): term ≤ R/(|γ|·(R−|γ|)/2) = 2R/(|γ|(R−|γ|)): dyadic in |γ| AND in (R−|γ|)... the double dyadic: split [3, R−2] into lower half |γ| ≤ R/2 (then R−|γ| ≥ R/2: term ≤ 2R/(|γ|·R/2) = 4/|γ|: dyadic |γ| shells: count([2^j, 2^{j+1}]) ≍ 2^j A₀ log(2^{j+1}): term ≤ 4/2^j: shell ≍ 4A₀(j+1): total over j ≤ log R: O((log R)²) ✓) and upper band |γ| ∈ [R/2, R−2] (dyadic in d = R−|γ| ∈ [2, R/2]: count({|γ| ∈ [R−2^{j+1}, R−2^j]}) ≍ 2^{j+1} A₀ log R: term ≤ 2R/((R/2)·2^j) = 4/2^j: shell ≍ 8A₀ log R: total O((log R)²) ✓).\n- critical |γ| ∈ (R−2, R+2): γ-gap: on strip arcs |s−ρ| ≥ |t−γ| ≥ 1/(32Ĉ₀); on near-axis arcs ‖s−ρ‖ ≥ √(R²−100)−1 ≥ R/2 (even better): term ≤ R/((R−3)·min(1/(32Ĉ₀), ...)) — handle arcs separately: strip: ≤ 64Ĉ₀; near-axis: ≤ 2/(R−3): count ≍ 4 windows ≍ 4A₀log(R+2): strip sum ≍ 256·Ĉ₀·A₀·log R = O((log R)²) ✓; near-axis ≍ 8A₀logR/R ✓ tiny.\n- upper |γ| ∈ [R+2, 2R]: ‖s−ρ‖ ≥ (|γ|−R−1) ≥ (|γ|−R)/2 (|γ|−R ≥ 2 ✓): term ≤ 2R/(|γ|(|γ|−R)) ≤ 4/(|γ|−R) (|γ| ≥ R): dyadic in e = |γ|−R ∈ [2, R]: count ≍ 2^{j+1} A₀ log(2R): term ≤ 4/2^j: shell ≍ 8A₀ log R: total O((log R)²) ✓.\n- far |γ| > 2R: ‖s−ρ‖ ≥ (|γ|−R)/2 ≥ |γ|/4 (|γ| ≥ 2R ⟹ |γ|−R ≥ |γ|/2, /2−adjusted: (|γ|−R)/2 ≥ |γ|/4 ⟺ |γ| ≥ 2R ✓): term ≤ R/(|γ|·|γ|/4) = 4R/|γ|²: dyadic: shell [2^j, 2^{j+1}] (2^j ≥ 2R): count ≍ 2^{j+1}A₀(j+1)log2-ish: term ≤ 4R/4^j: shell ≍ 8R·A₀(j+1)/2^j: Σ_j ≍ 8RA₀·(log R + 2)/R·2 = O(log R) ✓.\n\nWait — the critical band on the STRIP arcs: |s−ρ| ≥ |t−γ| — need |t| ≥ 10 there ✓ (strip arcs have |t| ≥ √(R²−12.25) ≥ 10 for R ≥ 11 ✓). And the γ-gap's |R − |γ|| analysis with |t| ∈ [R−13/R, R]: |t−γ| ≥ ||t|−|γ|| ≥ |R−|γ|| − 13/R: with the 5e-i clearance (fine 1/(16Ĉ₀) or coarse 1): ⟹ |t−γ| ≥ min(1/(16Ĉ₀), 1) − 13/R ≥ 1/(32Ĉ₀) for 13/R ≤ 1/(32Ĉ₀)·... 13/R ≤ 1/(32Ĉ₀) ⟺ R ≥ 416·Ĉ₀(4k+9/2): Ĉ₀(4k+9/2) ≤ 2.9 + 0.433·log(4k+6.5) + 0.886·log log(4k+6.5): for k ≥ 2000: R ≥ 8002.5; Ĉ₀ ≤ 2.9 + 0.433·log(8007) + 0.886·log log(8007): log(8007) ≤ log(8104) = 9 (e⁹ ≥ 8104·... e⁹ = 8103.08 — hmm need e⁹ ≥ 8007: e⁹ ≥ 2.7⁹: 2.7² = 7.29, 2.7³ = 19.683, 2.7⁴ = 53.14, 2.7⁵ = 143.5, 2.7⁶ = 387.4, 2.7⁷ = 1046, 2.7⁸ = 2824, 2.7⁹ = 7625 < 8007!! So e⁹ might be < 8007 ⟹ log(8007) > 9 slightly: e⁹ = 8103.08 ≥ 8007 ✓ YES 8103 > 8007 ✓ log(8007) ≤ 9 ✓ (e⁹ ≥ 2.71828⁹ — need a numeric lower bound for e: Real.exp_one_lt_d9 : 2.718281828 < e? something like that ✓ used in LiGapCircles as Real.exp_one_lt_d9.le ✓. 2.718281828⁹ vs 8007: compute: 2.71828² = 7.389; ⁴ = 54.6; ⁸ = 2981; ×2.71828 = 8103 ≥ 8007 ✓ — the norm_num evaluation of 2.718281828^9 — 9 multiplications of decimals — norm_num can do it (slow but OK) or via Real.exp_one_lt_d9 + Real.exp_nat_mul... Let me handle the numeric threshold when I get there — k ≥ 2000 gives enough slack that even rough bounds work: Ĉ₀(4k+9/2) ≤ 2.9 + 0.433·(4k+6.5)·... no — need log ≤ linear: log x ≤ x/e-ish. For k ≥ 2000: log(4k+6.5) ≤ 4k+6.5 ≤ ... 416·Ĉ₀ ≤ 416·(2.9 + 0.433·L + 0.886·L') where L = log(4k+6.5), L' = log L: use L ≤ √(4k+6.5)·2 (log x ≤ 2(√x−1)): 416·(2.9 + 0.866√x + 1.772·log... — vs R ≥ 4k+2.5 =: x−4: need 416·(2.9+0.433L+0.886L') ≤ x−4 with x = 4k+6.5 ≥ 8006.5: L ≤ 2√x ≤ 2·90 = 180; L' = log L ≤ log 180 ≤ 6: 416·(2.9 + 0.433·180 + 0.886·6) = 416·(2.9+78+5.3) = 416·86.2 = 35859 — vs x−4 = 8002 — FAILS! The slack isn't enough with these crude log bounds. Let me compute honestly: Ĉ₀(8006.5) = 2.9 + 0.433·log(8008.5) + 0.886·log log(8008.5): log(8008.5) = 8.988: 0.433·8.988 = 3.89; log(8.988) = 2.196: 0.886·2.196 = 1.95: Ĉ₀ ≈ 2.9+3.89+1.95 = 8.74: 416·8.74 = 3636 ≤ 8002.5 ✓✓ — the HONEST value works with slack 2.2×. The crude bounds failed because log x ≤ 2√x is too lossy (2√8006 = 179 vs 9). Use instead: log x ≤ x/1800+... for x ≥ 8000: log x ≤ 9 (from e⁹ ≥ x: e⁹ ≥ 8103 > 8008.5): the e⁹ lower bound: Real.exp 9 = (Real.exp 1)^9: from Real.exp_one_lt_d9 : 2.718281828459045 < e (the d9 form: 2.718281828 < exp 1 presumably): exp 9 = (exp 1)^9 ≥ 2.718281828^9 — the numeric power: norm_num [Real.exp_nat_mul]?? exp 9 = exp(1·9) = (exp 1)^9 via Real.exp_nat_mul: rw then `norm_num [Real.exp_one_lt_d9.le]`?? The power 2.718281828^9 ≥ 8008.5: compute by repeated squaring with norm_num at each step (norm_num handles real numeral multiplication): 2.718281828^2 = 7.38905...; ^4 = 54.598; ^8 = 2980.96; ×2.718281828 = 8102.9: each step norm_num-verifiable ✓. So: log(8008.5) ≤ 9 ⟸ 8008.5 ≤ 2.718281828⁹ ≤ e⁹: Real.log_le_log ⟸ Real.exp_le_exp: log x ≤ 9 ⟺ x ≤ e⁹ (Real.log_le_iff... `Real.log_le_iff_le_exp`? or via exp-log: log x ≤ y ⟺ x ≤ exp y for x > 0: `Real.log_le_iff_le_exp (hx : 0 < x) : log x ≤ y ↔ x ≤ exp y`?? name check later). Then Ĉ₀ ≤ 8.75 via the arithmetic with log log(8008.5) ≤ log 9 ≤ 2.2 (9 ≤ e^{2.2}: e^{2.2} ≥ e² = 7.389 ≥ ... 9 > 7.389! log 9 ≤ 2.2 ⟺ 9 ≤ e^{2.2}: e^{2.2} = e²·e^{0.2} ≥ 7.389·1.2 = 8.87 < 9!! so log 9 > 2.2 slightly: log 9 = 2.1972 ≤ 2.2 ✓ YES 2.1972 < 2.2 ✓ — e^{2.2} ≥ 8.87 < 9 fails ⟹ can't prove log 9 ≤ 2.2 via e^{2.2} ≥ 9 — use log 9 ≤ 2.2 ⟺ 9 ≤ e^{2.2}: e^{2.2} = 9.025 ✓ (e^{0.2} ≈ 1.2214: 7.389·1.2214 = 9.025 ≥ 9 ✓): need e^{0.2} ≥ 1.2214: from exp_one_lt_d9: e^{0.2} = (e)^{1/5}... awkward — use Real.exp 0.2 ≥ 1 + 0.2 + 0.02 + ... (Taylor): Real.add_one_le_exp gives e^x ≥ 1+x: e^{0.2} ≥ 1.2 ⟹ e^{2.2} ≥ 7.389·1.2 = 8.87 < 9 — not enough. e^{0.2} ≥ 1.2214 needs the quadratic term: is there `Real.exp_le`... or exp_two... Use a different slack: Ĉ₀ ≤ 2.9 + 3.89 + 0.886·log(8.988): log(8.988) ≤ log 9: and log 9 ≤ 2.2 — I just need SOME bound ≤ 2.2: log 9 = 2 log 3: log 3 ≤ 1.1 ⟺ 3 ≤ e^{1.1}: e^{1.1} ≥ e·1.2?... e^{1.1} = e·e^{0.1} ≥ 2.71828·1.1 = 2.99 < 3 — again just short. e^{0.1} ≥ 1.105: Taylor 1+0.1+0.005+0.000167 = 1.105167 ✓ — is there a Mathlib exp lower bound with quadratic terms? `Real.add_one_le_exp` only linear. `Real.exp_one_lt_d9` is e > 2.718281828... For e^{0.1}: hmm. ALTERNATIVE: avoid the tight numeric: take k ≥ 4000 (R ≥ 16002): then log(16007) ≤ 10 (e^{10} ≥ e⁹·2.7 ≥ 8103·2.7 = 21878 ≥ 16007 ✓ — provable from exp_one_lt_d9 via exp_nat_mul + norm_num squaring ✓): Ĉ₀ ≤ 2.9 + 0.433·10 + 0.886·log 10: log 10 ≤ 2.4 (10 ≤ e^{2.4}: e^{2.4} = e²·e^{0.4} ≥ 7.389·1.4 = 10.34 ≥ 10 ✓ (e^{0.4} ≥ 1.4 via add_one_le_exp 1+0.4 = 1.4 ✓✓ — JUST enough (1.4 exact, need e^{0.4} ≥ 1.4 = 1+0.4 ✓ add_one_le_exp ✓)): so Ĉ₀ ≤ 2.9 + 4.33 + 0.886·2.4 = 2.9+4.33+2.13 = 9.36: 416·9.36 = 3894 ≤ 16002 ✓✓ HUGE slack. And e^{10} ≥ 21878: e^{10} = (e^...): exp 10: Real.exp 10 = (Real.exp 1)^{10}: ≥ 2.718281828^{10} = 2980.96·2.71828 = 8103·2.71828 ≈ 22026 — provable: 2.718281828^10 ≥ 16007: norm_num chain ✓. So K₀ := 4000, R ≥ 16002. All numerics provable with add_one_le_exp + exp_one_lt_d9 + norm_num. ✓\n\nOK — enough analysis. The structure is clear. Now — realistic assessment: 5e-v-b (the series bound) is ~500-600 lines and the remaining 5e-v-c/d ~400. This is a lot for one session; the pacing directive says no rush, break into clean sub-stages. Let me proceed stepwise and commit as I go.\n\nActually — hmm, wait. Let me reconsider the SIZE once more. Is there any way to reduce the series-bound work using the ALREADY-BUILT 5c/5d near-sum bounds MORE aggressively? The identity-to-be is F = ζ′/ζ − series − elems. The circle bound needs each piece. The series is the only piece without a pre-built bound. No way around it.\n\nOne simplification I CAN make: instead of bounding the series via tsum-splitting into 5 parts with subtype-summability gymnastics, use the direct approach: \n\n‖seriesFun s‖ ≤ ∑' ρ, ‖seriesTerm s ρ‖ = ∑' ρ, m_ρ·R/(‖ρ‖·‖s−ρ‖) — then decompose the SUM over the subtype as a sum over shells... the tsum-splitting over the subtype by predicates: with the 5-piece split, I'd do 4 tsum_add_tsum_compl applications — each needs Summable-on-subtype proofs (Summable.subtype hf — check exists). Then bound each.\n\nAlternatively — CLEANER: pull the sum back to a sum over ORDINATE WINDOWS and bound via those directly?? The zeros are a subtype; the shells are sub-finsets... \n\nYou know what — let me define the split via the FINSET of zeros below a height + a tail tsum:\nΣ'all = Σ_{|γ| ≤ 2R} + Σ_{|γ| > 2R}: ONE tsum split only:\n- The finite part {‖ρ‖... |γ| ≤ 2R}: a FINSET (finiteness via zerosIn_finite cover: |γ| ≤ 2R ⟹ γ ∈ [−2R, 2R] ⊆ zerosIn (−2R) (2R) finite ✓): the finite sum splits into finset sub-pieces by Finset.filter — NO subtype-summability issues (plain finset sums ✓✓).\n- The tail {|γ| > 2R}: a tsum over the subtype-complement — ONE tsum, bounded by the dyadic sum: ∑'_{|γ|>2R} m·4R/|γ|² ≤ Σ_j (count shell)·4R/4^j — the tail tsum ≤ the explicit convergent majorant: via Summable comparisons: the dyadic majorant is summable (geometric·polynomial): Σ_j 2^{j+1}A₀(j...)·4R/4^j — summable over j (2^j decay) ✓ — the comparison ∑'_{tail} ≤ ∑'_{j} (shell bounds) needs a shell-sum ↔ dyadic-sum bridge: group the tail zeros by ⌊log₂(|γ|/R)⌋ — ugh.\n\nAlternative for the tail: use zero_sum_inv_sq's CONVERGENCE with the explicit tail bound: Σ_{|γ|>2R} m/(1+γ²) ≤ (window bound): Σ_{|γ|>X} m/(1+γ²) ≤ Σ_{j} Ncount-shells/(1+4^jX²)... still dyadic.\n\nHmm OK — actually, the cleanest for the TAIL: bound the tail TSUM directly by a comparison with a dyadic-majorant tsum over the SAME subtype: for ρ with |γ| > 2R: m·4R/|γ|² ≤ m·4R/(1+γ²)·(1+γ²)/γ²·... ≤ m·(17/12)/(1+γ²)·4R·2 (since (1+γ²)/γ² ≤ 2 for |γ| ≥ 1 ✓): ≤ 8R·(17/12)·m/(1+γ²) — and the tail of the CONVERGENT Σ m/(1+γ²): Σ_{|γ|>2R} m/(1+γ²) ≤ ??? — the TAIL VALUE: zero_sum_inv_sq gives the total but the tail needs the dyadic estimate: Σ_{|γ|>X} m/(1+γ²) ≤ Σ_j A₀·(2^jX+2)·log(2^{j+1}X+3)·2/(1+4^jX²)·... ≍ A₀ log X/X·... — the tail IS O(A₀ log X / X) via dyadic windows — same work. OK the dyadic tail bound is unavoidable; write it once as a lemma:\n\n`tail_inv_sq_le {X : ℝ} (hX : 2 ≤ X) : ∑' ρ : subtype-with-|γ|>X, m/(1+γ²) ≤ 100·A₀·(log X)/X` — hmm the constant: Σ_{j≥0} (count of {2^j X < |γ| ≤ 2^{j+1}X})·1/(1+4^jX²): count ≤ 2·Ncount(0, 2^{j+1}X]-ish via my interval lemma ≤ 2A₀(2^{j+1}X+1)log(2^{j+1}X+4): term ≤ 2A₀(2^{j+1}X+1)log(...)/(4^j X²) = 2A₀(2/X + ...)·(j log 2 + log X + ...)/4^j·... ≍ (4A₀/X)·(j+log X)/2^j: sum over j: (4A₀/X)·(2 + 2 log X)-ish = O(A₀ log X / X) ✓.\n\nThen the tail series part: Σ_{|γ|>2R} m·|1/(s−ρ)+1/ρ| ≤ Σ m·4R/|γ|² ≤ Σ m·4R·(17/12)·2/(1+γ²) ≤ 8R·(17/12)·(tail) ≤ 8R·3·(100A₀ log(2R)/(2R)) = O(A₀ log R) ✓.\n\nOK let me stop analyzing and START WRITING. The session has already done 5e-v-a; 5e-v-b is big — I'll build it piecewise with compiles in between. Given the natural break, let me commit 5e-v-a (done ✓) and now write 5e-v-b's helper lemmas (the interval-count generalization + the tail bound + the finset-shell comparisons), then the main series bound.\n\nActually, let me reconsider the time budget. This session has already been long (5e-v-a compiled + committed). The pacing rule says break into clean committed sub-stages. 5e-v-b is a natural next sub-stage but it's ~600 lines — likely a full session on its own. Since everything is committed and resumable, and the user said \"let's work on ii'-5e-v\" — I should continue working on 5e-v-b now as far as reasonable. Let me write the helpers + main bound skeleton.\n\nHmm, actually — let me reconsider the overall shape ONE more time to minimize the Lean burden. The KEY observation: the tsum-splitting pain comes from mixing finite and infinite parts over the subtype. Alternative formulation that avoids ALL tsum splits:\n\nBound ‖seriesFun s‖ ≤ ∑' ρ, ‖seriesTerm s ρ‖ (one step). Then bound the REAL nonneg tsum ∑' ρ, g ρ where g ρ := m_ρ·R/(‖ρ‖·‖s−ρ‖) by a comparison: g ρ ≤ M ρ where M is an explicit summable family built from... no — the shell structure is inherent to the bound.\n\nAlternative: bound ∑' ρ, g ρ via the layer-cake/dyadic identity directly: for ANY zero, classify into the 5 cases and bound termwise: g ρ ≤ M_j ρ on shell j — then ∑' g ≤ Σ over shells of (bound) — the splitting is unavoidable for the ≤.\n\nBUT — here's a cleaner formalization trick: bound by a SINGLE summable comparison on the whole subtype + a finite exceptional sum:\nFor ρ NOT in the critical band (|R−|γ|| ≥ 2): ‖s−ρ‖ ≥ ... the shells...\nNo — the shell structure is the mathematics. Accept it.\n\nFINAL structural decision to minimize pain: express the bound as\n\n‖seriesFun s‖ ≤ C_low + C₁·A0count·(log R)² + C₂·A0count·Ĉ₀(4k+9/2)·log R\n\nwith the proof decomposed as:\n1. ‖seriesFun s‖ ≤ ∑' ρ, ‖term‖ (norm_tsum).\n2. ∑' ρ, ‖term‖ = Σ_{F₀} ‖term‖ + ∑'_{ρ ∉ F₀} ‖term‖ where F₀ := {‖ρ‖ ≤ 3}-finset (ONE tsum split via tsum_add_tsum_compl or the subtype-sum: `Summable.tsum_finsetSum`?? — for a FINITE set: ∑' ρ, g ρ = ∑_{ρ ∈ F₀-finset} g ρ + ∑'_{ρ ∈ F₀ᶜ-subtype} g ρ: `tsum_eq_sum_add_tsum_compl`? there might be `Summable.tsum_eq_sum_add_...`... hmm: the cleanest: `tsum_add_tsum_compl (s := F₀set) (hf : Summable g) (hfs : Summable (g ∘ Subtype.val))...`. Let me check the exact name/signature.\n\nLet me check tsum_add_tsum_compl.","signature":""},{"type":"text","text":"5e-v-a committed. Now 5e-v-b (the series circle bound). Checking the tsum-splitting API first — the structural key for the shell decomposition."},{"type":"tool_use","id":"Bash_297","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem tsum_add_tsum_compl\\|lemma tsum_add_tsum_compl\" Mathlib/ -r --include=*.lean | head -2 && grep -rn -A 6 \"theorem tsum_add_tsum_compl\" Mathlib/Topology/Algebra/InfiniteSum/*.lean | head -10; grep -rn \"theorem Summable.subtype\\b\\|lemma Summable.subtype\\b\" Mathlib/ -r --include=*.lean | head -3","description":"tsum_add_tsum_compl and Summable.subtype"},"extra_content":null}]