[{"type":"thinking","thinking":"The M-test `HasSumUniformlyOn.of_norm_le_summable` works for general α (index type) — the subtype works.\n\nNow, the analyticity on `ℂ ∖ zeros`: the domain is `{s | riemannZeta s ≠ 0}`? Wait — the series has poles at ALL zeros of ζ including trivial zeros? No — the series is over the NONTRIVIAL zeros only. The terms have poles at nontrivial ρ. The domain of analyticity: ℂ ∖ {nontrivial zeros}. But hold on — for the eventual F entire argument, the series minus the ρ-term must be analytic AT ρ. So the design:\n\n- Domain U := {s | s ∉ nontrivialZeros} = {s | ¬ IsNontrivialZero s}.\n- On any compact K ⊆ U: for ρ with ‖ρ‖ ≥ 2·max_{K}‖s‖ and ‖ρ‖ ≥ 2: ‖term‖ ≤ 2‖s‖/‖ρ‖²·mult ≤ C·mult/(1+‖γ‖²). But careful: the term also needs s ≠ ρ for all s ∈ K — K ⊆ U so s never equals a nontrivial zero. The bound ‖1/(s−ρ)+1/ρ‖ = ‖s/(ρ(s−ρ))‖ needs ρ ≠ 0 (nontrivial zeros have re > 0 so ρ ≠ 0 ✓) and the tail condition ‖ρ‖ ≥ 2‖s‖.\n\n- For the uniform M-test with `of_norm_le_summable` I need a bound for ALL ρ, not eventually. Two options: (a) use `of_norm_le_summable_eventually` with cofinite filter — but \"eventually in cofinite\" on the subtype means all but finitely many ρ — the tail set {ρ : ‖ρ‖ ≥ R} has finite complement (zeros finite in compacts) ✓. That's exactly what `of_norm_le_summable_eventually` is for. But wait — cofinite on the subtype: is {ρ : ‖ρ‖ < R} finite as a set of subtype elements? Yes — shown via the LiSkeleton pattern (Set.Finite of the subtype set). Finite ⟹ cofinite ✓.\n\n(b) Or: split the series as finite head + uniform tail. Option (a) is cleaner.\n\nPlan for `seriesFun` analyticity on U:\n- U := {s : ℂ | ¬ IsNontrivialZero s}. Is U open? IsNontrivialZero s ⟺ ζ s = 0 ∧ 0 < re < 1. The zero set within the open strip is closed in the strip (zeros of analytic function, closed + discrete). Simpler: work locally — for each s₀ ∈ U, produce a ball B(s₀,δ) ⊆ U. Since the nontrivial zero set is closed in ℂ? Nontrivial zero set = riemannZetaZeros ∩ {0 < re < 1}... Mathlib's `riemannZetaZeros` — let me check its def. If `riemannZetaZeros` is closed and the strip is open, then U = (riemannZetaZeros ∩ strip)ᶜ = riemannZetaZerosᶜ ∪ stripᶜ which is open (union of opens: riemannZetaZerosᶜ open if closed; stripᶜ open since strip open... complement of open is closed, not open — no). Hmm: U = {s | ¬(ζ s = 0 ∧ 0 < re s ∧ re s < 1)} = {ζ s ≠ 0} ∪ {re s ≤ 0} ∪ {re s ≥ 1}. Is {ζ s ≠ 0} open? ζ is entire so zero set is closed ⟹ complement open ✓. {re s ≤ 0} is closed not open. Ugh.\n\nAlternative: U = {ζ s ≠ 0} ∪ {re < 0} ∪ {re > 1} — wait that's not the complement either. ¬(A ∧ B ∧ C) = ¬A ∨ ¬B ∨ ¬C = {ζ s ≠ 0} ∪ {re ≤ 0} ∪ {re ≥ 1}. The set {re ≤ 0} is closed. But actually the union {ζ s ≠ 0} ∪ closed sets: not obviously open. However, note that on {re ≤ 0} ∪ {re ≥ 1}, ζ has zeros only at −2n (trivial) on re ≤ 0... and none for re ≥ 1. Points with re ≤ 0 that aren't trivial zeros: near them, are there nontrivial zeros arbitrarily close? No — nontrivial zeros have re ∈ (0,1) strictly. A point s₀ with re s₀ < 0 or re s₀ > 1 has a strip neighborhood avoiding the critical strip. A point s₀ with re s₀ = 0 or = 1 exactly, and ζ s₀ ≠ 0: since ζ's zero set is closed, there's a ball avoiding all zeros... but wait nontrivial zeros could accumulate? No — zeros of an entire function are discrete; the FULL zero set of ζ is closed and discrete, so any s₀ with ζ s₀ ≠ 0 has a ball with no zeros at all. And if s₀ ∈ U has ζ s₀ = 0, then re s₀ ≤ 0 or ≥ 1 — zeros of ζ with re ≤ 0 are exactly the trivial zeros −2n (is this in Mathlib/Zeta23? `IsNontrivialZero.not_trivial` is one direction; the other direction — zeros outside the strip are trivial — is `zeroDisc_isNontrivial` territory from LiDisc: \"re ≥ 1 via Mathlib's one_le_re nonvanishing; re ≤ 0 via ΓR-pole/FE\"). Indeed LiDisc has `zeroDisc_isNontrivial`: zeros in the disc with certain properties are nontrivial. Let me check its exact statement.\n\nActually — do I even need U to be open as a global statement? For analyticity at each s₀ ∈ U I can work with a local ball:\n- Case ζ s₀ ≠ 0: zeros closed ⟹ ∃ ball B(s₀,δ) with no zeros of ζ at all ⟹ no nontrivial zeros ⟹ series analytic on the ball by M-test (K = closedBall ⊆ ball, compact).\n- Case ζ s₀ = 0: then re s₀ ∉ (0,1) — s₀ is a trivial zero −2n or... s₀ = 1 is a pole not zero; s₀ with re s₀ ≥ 1 impossible (nonvanishing); re s₀ ≤ 0 ⟹ s₀ ∈ {−2n} (needs the \"zeros left of 0 are trivial\" fact). At s₀ = −2n, the series has no pole (series only over nontrivial zeros) — but is the series analytic AT −2n? Need a ball around −2n containing no nontrivial zeros: |re − (−2n)| < 1 say gives re < −2n+1 ≤ −1 < 0 — outside the strip, and zeros there are only trivial... at −2n exactly the only zero in that ball is −2n itself (trivial). So need: ball B(−2n, min(1, dist to other trivial zeros)) contains no NONTRIVIAL zero — any zero in the ball has re < 0 and must be trivial — but there are no other trivial zeros within distance 1... trivial zeros at −2n±2 are distance 2 away. So B(−2n,1) contains only −2n among all ζ-zeros. This needs the \"no zeros with re ≤ 0 except −2n\" fact. Is that in Zeta23? LiDisc's `zeroDisc_isNontrivial`: let me check. It said \"re ≥ 1 via Mathlib's one_le_re nonvanishing; re ≤ 0 via ΓR-pole/FE\" — i.e., a zero in the disc with re ≤ 0 leads to contradiction unless... Actually the lemma was probably: a zero in the closedBall(discCenter t, 5/2) (with |t| ≥ 10) is nontrivial — because such a zero has re ∈ [−1/2, 9/2]... hmm the disc at 2+it radius 5/2 has re ∈ [−1/2, 9/2]. For re ≤ 0 they got a contradiction via ΓR-pole/FE — meaning: zeros with re ≤ 0 AND |im| ≥ 10-ish don't exist? Wait — trivial zeros are at −2n (real). A zero with re ≤ 0 and im ≠ 0 would reflect via FE... The standard fact: ζ(s) = 0, re s ≤ 0 ⟹ s ∈ {−2, −4, ...}. Because Λ(s) = Λ(1−s); for re s < 0, re(1−s) > 1 ⟹ ζ(1−s) ≠ 0 and ΓR(1−s) ≠ 0 finite; so ΓR(s) = 0 or pole... ΓR(s) = π^{−s/2}Γ(s/2) has poles at s = −2n and no zeros; so ζ(s) = 0 requires ΓR(s) to have a pole ⟹ s = −2n. This is presumably what LiDisc did.\n\nFor the analyticity of the series at trivial zeros I need a neighborhood of −2n free of nontrivial zeros. Do I actually NEED analyticity at trivial zeros for 5e? The design D-068 §3 says \"analytic on ℂ ∖ zeros\" (nontrivial zeros). And §4 (5e-iv) handles the −2n splits for F: \"−½ψ(s/2) − 1/(s+2n) analytic at −2n\" and \"ζ′/ζ − 1/(s+2n) analytic at −2n\". The series IS analytic at −2n (no poles there — nearest nontrivial zeros have re ∈ (0,1), distance ≥ 2n+... ≥ 1 in re). So for 5e-iv we need the series analytic at −2n as well. So the natural domain is: U := {s | ¬ IsNontrivialZero s} — includes trivial zeros, 0, 1. To show U open or at least locally-around-each-point a ball free of nontrivial zeros:\n\nFor s₀ ∈ U: if ζ s₀ ≠ 0 → ball free of ALL zeros (closedness+discreteness... actually just closedness suffices: {ζ = 0} closed ⟹ ∃ ball avoiding it? No! Closed set complement is open ⟹ s₀ ∈ open complement ⟹ ball exists ✓. Zero set of entire ζ: is `riemannZetaZeros` or {s | ζ s = 0} closed in Mathlib? Preimage of {0} under continuous ζ ⟹ closed ✓ — continuous_riemannZeta or analytic. Easy.\n\nIf ζ s₀ = 0: s₀ ∈ U ⟹ ¬(0 < re < 1) ⟹ re ≤ 0 or re ≥ 1. re ≥ 1 impossible for a zero (1 is a pole; nonvanishing for re ≥ 1, s ≠ 1 — Mathlib `riemannZeta_ne_zero_of_one_le_re`). re ≤ 0: need s₀ = −2n for some n ≥ 1 (the \"zeros left of the strip are trivial\" fact) — check LiDisc for this. Then ball B(s₀, 1) — any nontrivial zero in it has re ∈ (0,1) but |re − re s₀| < 1 gives re > −2n−1... hmm re(s₀) = −2n, ball radius 1: re ∈ (−2n−1, −2n+1) ⊆ (−∞, −1] for n ≥ 1... −2n+1 ≤ −1 < 0 ✓ — so no point of the ball is even in the critical strip ⟹ no nontrivial zeros. Wait: nontrivial zeros need 0 < re. Points in B(−2n, 1) have re < −2n+1 ≤ −1 < 0 ✓. So B(−2n,1) ∩ {nontrivial zeros} = ∅ directly from re < 0 — no need for the ΓR-pole argument at all for THIS purpose! I only need: re s₀ ≤ 0 ⟹ ball of radius |re s₀| + ... Let me redo: s₀ ∈ U with ζ s₀ = 0: re s₀ ≤ 0 or re s₀ ≥ 1. re s₀ ≥ 1 impossible (nonvanishing + pole at 1 — ζ(1) isn't 0, junk/∞; actually riemannZeta 1 = 0? No — Mathlib has riemannZeta_ne_zero_of_one_le_re for re ≥ 1, s ≠ 1... and at s=1 there's a pole so ζ(1) is junk value (0 by some conventions? In Mathlib riemannZeta is entire-completed... no, riemannZeta has a pole at 1; its value at 1 is defined as... probably 0 junk or the limit... anyway ζ s₀ = 0 with re ≥ 1 ⟹ s₀ = 1 possible junk; need care). Take δ = dist-based: if re s₀ ≤ 0: δ = (1 − re s₀)/... any ball B(s₀, δ) with re s₀ + δ < 0, i.e. δ < |re s₀| when re s₀ < 0... if re s₀ = 0 exactly (s₀ = i t, ζ(it) = 0 — possible! zeros ON the line re = 0? ζ(it) = 0 would be a nontrivial zero? No: nontrivial requires 0 < re strictly. But zeros ON the imaginary axis: by FE ζ(it) = 0 ⟹ ... hmm ζ(it) for real t ≠ 0 is never 0? Zeros with re = 0: Λ(it) = Λ(1−it); |ΓR|>0... the standard argument: re = 0, im ≠ 0 ⟹ ζ ≠ 0 (via FE from re = 1 nonvanishing: ζ(1−s) ≠ 0 for re(1−s) = 1... wait nonvanishing on re = 1 IS the PNT-level fact. Mathlib has `riemannZeta_ne_zero_of_one_le_re` (re ≥ 1, covering re = 1!). That's a strong fact (PNT-equivalent, but it's in Mathlib). So re s = 0, s ≠ 0: ζ(s) = 0 ⟹ Λ(s) = ΓR(s)ζ(s) = 0; Λ(1−s) = Λ(s) = 0; but re(1−s) = 1, and ΓR(1−s) ≠ 0 (Gamma no zeros, π^... finite) ⟹ ζ(1−s) = 0 with re = 1, 1−s ≠ 1 (s ≠ 0) ⟹ contradiction with `riemannZeta_ne_zero_of_one_le_re`. So no zeros on re = 0 except s = 0. At s = 0: ζ(0) = −1/2 ≠ 0. Good.\n\nSo the case split for s₀ ∈ U:\n- ζ s₀ ≠ 0: open complement of zero set ⟹ ball avoiding all zeros ⟹ no nontrivial zeros in ball.\n- ζ s₀ = 0, re s₀ ≥ 1: impossible (nonvanishing: Mathlib; s₀ = 1 gives ζ(1) — need ζ(1) ≠ 0: Mathlib `riemannZeta_one`? The value at 1... Mathlib defines riemannZeta via the completed... no — `riemannZeta` at 1: it's defined by analytic continuation with the pole REMOVED? No — riemannZeta has a simple pole at 1; as a function ℂ → ℂ it's defined to be... In Mathlib, riemannZeta 1 = 0? Let me not guess; LiDisc's zeroDisc_isNontrivial handled re ≥ 1 via \"Mathlib's one_le_re nonvanishing\" — I'll mirror that).\n- ζ s₀ = 0, re s₀ ≤ 0: then from FE + ΓR nonvanishing/poles + one_le_re nonvanishing ⟹ s₀ ∈ {−2n : n ≥ 1} OR s₀ = 0 — ζ(0) ≠ 0 rules 0 out. So s₀ = −2n, n ≥ 1 ⟹ re s₀ ≤ −2 ⟹ ball B(s₀, 1) has re < −1 ⟹ no nontrivial zeros.\n\nAlternatively simpler: I recall LiDisc has `zeroDisc_isNontrivial` — let me look at it; maybe there's a ready lemma \"ζ s = 0 ∧ re s ≤ 0 → s = −2n\" somewhere in the Li* files or Zeta23. Session-024 notes said: \"zeroDisc_isNontrivial (re ≥ 1 via Mathlib's one_le_re nonvanishing; re ≤ 0 via ΓR-pole/FE)\". Let me read that part of LiDisc.lean.\n\nActually — wait. Do I even need the series analytic at trivial zeros for the F-entire build? Yes per D-068 §4: at s = −2n, F = [ζ′/ζ − 1/(s+2n)] − [series + elems − ½ψ − ...]. The series must be analytic at −2n. So yes.\n\nBut hold on — maybe simpler: prove the series is analytic on the OPEN set V := {s | re s > −2·ceil-ish...}? No — global: the domain should be all of ℂ minus nontrivial zeros, since 5e-v needs the identity on a big circle. But for analyticity of F on the circles and everywhere, the piecewise local argument is what matters. The cleanest formalization:\n\n**Theorem (5e-iii main)**: `AnalyticOnNhd ℂ seriesFun {s | ¬ IsNontrivialZero s}`? For AnalyticOnNhd I need: ∀ s₀ ∈ U, ∃ ball ⊆ U with seriesFun analytic on it — `AnalyticOnNhd` means analytic in a neighborhood of each point of the set. I can prove `AnalyticAt ℂ seriesFun s₀` for each s₀ ∈ U via: get δ-ball avoiding nontrivial zeros (per above case split), then on the OPEN ball, M-test with compact subsets... Actually simpler: M-test directly on the open ball B(s₀, δ) with the eventually-form: uniform bound for all but finitely many ρ on all of B(s₀,δ): for ρ with ‖ρ‖ ≥ 2(‖s₀‖+δ) and ‖ρ‖ ≥ 2: ‖term(s)‖ ≤ 2(‖s₀‖+δ)·(5/3)mult/(1+‖γ‖²) — hmm the M-test wants ‖f n x‖ ≤ u n for ALL x ∈ s with u summable — the eventually version handles the rest. `HasSumUniformlyOn.of_norm_le_summable_eventually` with cofinite: need {ρ : ‖ρ‖ < R} finite in the subtype (cofinite membership) — same finiteness as before ✓.\n\nBut wait — there's a subtlety with `of_norm_le_summable_eventually`: the conclusion is HasSumUniformlyOn f (fun x ↦ ∑' n, f n x) s — the uniform limit is the tsum — exactly seriesFun ✓.\n\nThen: TendstoUniformlyOn → tendstoLocallyUniformlyOn → differentiableOn (each finite partial-sum differentiable: each term s ↦ mult·(1/(s−ρ)+1/ρ) differentiable on the ball since s ≠ ρ there (ball avoids nontrivial zeros ✓) and ρ ≠ 0 ✓) → analyticOnNhd (ball open) → AnalyticAt at s₀.\n\nHmm wait, there's a subtlety with `TendstoUniformlyOn.differentiableOn` — the digamma case used `htend.differentiableOn _ dpsiDomain_isOpen` where htend : TendstoLocallyUniformlyOn (Finset partial sums). Note the digamma series index is ℕ with partial sums over Finset.range n; here the index is the subtype with tsum over ALL of it — the \"partial sums\" in `hasSumUniformlyOn_iff_tendstoUniformlyOn` are over Finsets of the subtype directed by inclusion? `HasSumUniformlyOn f g s` means the net of finite partial sums (over all finsets, atTop on Finset ι) converges uniformly. And `.differentiableOn` needs each finite partial sum differentiable — fine.\n\nLet me check the exact name: in the digamma case: `hasSumUniformlyOn_iff_tendstoUniformlyOn.mp` then `TendstoUniformlyOn.tendstoLocallyUniformlyOn` then `htend.differentiableOn (eventually each partial sum differentiableOn) isOpen`. \n\nNow — summability at each fixed s (also needed independently for seriesFun to be meaningful... well, the M-test gives HasSumUniformlyOn hence pointwise HasSum hence Summable on the ball; but for the capstone identity at arbitrary s (e.g., s near a zero but not on it) summability at each s ∉ zeros follows from the local uniform convergence ✓. And AT a zero ρ₀ itself: seriesFun ρ₀ = tsum with the ρ₀-term junk 0 — summable as well (same M-test on a ball around ρ₀ MINUS... no — the ball contains ρ₀ where the term blows up... the term at s = ρ₀ is mult·(1/(ρ₀−ρ₀) + 1/ρ₀) = mult·(1/0 + 1/ρ₀) = junk = mult·(0 + 1/ρ₀) — pointwise fine! The M-test uniform bound fails near ρ₀ though (1/(s−ρ) unbounded). But summability AT the single point s = ρ₀: terms with ρ ≠ ρ₀: fine, dominated by the same tail argument; the ρ₀-term is finite junk. So seriesFun is summable at EVERY s — including zeros (junk there). Good: `seriesSummable (s : ℂ) : Summable (seriesTerm s)` unconditionally.\n\nIsolation at each zero (part iii): for ρ₀ nontrivial zero: ∃ δ > 0, no OTHER nontrivial zero in B(ρ₀, δ). From finiteness of zeros in compacts: zeros in closedBall(ρ₀, ‖ρ₀‖+1) is finite; the others have positive distance; take min. Standard.\n\nThen \"series minus the ρ₀-term analytic at ρ₀\": define seriesFunSub ρ₀ s := ∑' ρ, if ρ = ρ₀ then 0 else seriesTerm s ρ. Hmm — better: analyticAt of (fun s => seriesFun s − mult·(1/(s−ρ₀)+1/ρ₀))? The difference equals ∑' ρ ≠ ρ₀ terms... For 5e-iv the needed statement: there's a function analytic at ρ₀ agreeing with seriesFun − m/(s−ρ₀) near ρ₀. Actually the cleanest: `AnalyticAt ℂ (fun s => seriesFun s - (zeroMult ρ₀ : ℂ)/(s - ρ₀)) ρ₀`? Hmm wait but seriesFun includes the junk term at ρ₀: seriesFun ρ₀ has the ρ₀-term = mult·(0 + 1/ρ₀) (junk 1/0 = 0). So seriesFun s − mult/(s−ρ₀) near ρ₀ = ∑'_{ρ≠ρ₀} terms + mult/ρ₀ (constant) — analytic. To prove: show the function g s := ∑' ρ, (if ρ = ρ₀ then mult/ρ₀... hmm.\n\nCleaner: define the reduced series `seriesFunSub ρ₀ s := ∑' ρ : {ρ // IsNontrivialZero ρ}, (if (ρ : ℂ) = (ρ₀ : ℂ) then 0 else seriesTerm s ρ)`? Then prove seriesFunSub ρ₀ analytic at ρ₀ via the M-test on the small ball B(ρ₀, δ) (δ from isolation; on this ball all terms with ρ ≠ ρ₀ are fine, and the ρ₀-term is 0 — uniform bound: for the tail same as before; for the head terms each is individually bounded on the ball... the M-test needs a summable uniform bound for ALL ρ eventually — with the eventually-form, the finitely many head terms just need to be individually bounded on the ball, which holds since the only pole in the ball was ρ₀ and it's zeroed out ✓... wait — `of_norm_le_summable_eventually` requires the bound ∀ x ∈ s for eventually-cofinite many n; the head terms are unconstrained — but uniform convergence of the FULL series needs the head terms bounded too... no — cofinite-eventually M-test: the finitely many exceptional terms each converge uniformly trivially?? Hmm, actually the standard result: if eventually (cofinite) the terms are uniformly bounded by a summable sequence, then the series converges uniformly — the finite head is a finite sum of continuous functions each separately well-behaved... The lemma `tendstoUniformlyOn_tsum_of_cofinite_eventually` handles this: the head is a FIXED finite set of terms; each is a function on the domain; the finite partial sums converge uniformly iff... the tail (cofinite complement) converges uniformly and the head is fixed — sum of a fixed finite part + uniformly convergent tail = uniformly convergent. But this requires the head terms to at least be defined/finite on the domain — they are (the zeroed ρ₀-term is 0; other head terms have poles only at their own ρ which is outside the ball... wait other head terms: ρ₁ with ‖ρ₁‖ < R could still have ρ₁ ∈ B(ρ₀,δ)? No — isolation: no other zero in B(ρ₀, δ) ✓. So all head terms ρ₁ ≠ ρ₀ have poles outside the ball ✓ bounded ✓.)\n\nAnd then: seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀ for s near ρ₀... on the ball: seriesFun s = tsum of all = tsum of (zeroed + the ρ₀ term) by tsum_add (both summable) — the zeroed series summable (M-test) and single-term series summable ✓. So near ρ₀: seriesFun s − mult·(1/(s−ρ₀) + 1/ρ₀) = seriesFunSub ρ₀ s, analytic; hence seriesFun s − mult/(s−ρ₀) = seriesFunSub ρ₀ s + mult/ρ₀ analytic at ρ₀ ✓.\n\nOK. Also needed later (5e-iv): seriesFun analytic at the trivial zeros, 0, 1 — all ∈ U ✓ covered by the general statement.\n\nNow, the \"zeros left of strip are trivial\" fact for the ζ s₀ = 0, re ≤ 0 case — wait, do I need it? The case split was: s₀ ∈ U, i.e. ¬(ζ s₀ = 0 ∧ 0 < re ∧ re < 1). I need a ball around s₀ containing no nontrivial zeros.\n- If re s₀ ≤ 0: ball B(s₀, |re s₀|/2 + ...)? If re s₀ < 0: B(s₀, |re s₀|/2): points have re < re s₀/2 < 0 ⟹ not nontrivial ✓. If re s₀ = 0: s₀ = it. If t = 0: s₀ = 0, ζ(0) = −1/2 ≠ 0 — but that's the OTHER case (ζ ≠ 0). If ζ(it) = 0 with re = 0... this point is in U ✓ but every ball around it could contain nontrivial zeros?? Zeros are discrete — the FULL zero set is discrete, so there's a ball containing no zeros except possibly s₀ itself. Nontrivial zeros in the ball: none, since no zeros at all except s₀, and s₀ is not nontrivial (re = 0) ✓. So discreteness of the full zero set handles it without FE!\n- If re s₀ ≥ 1: similarly — ζ s₀ ≠ 0 (nonvanishing, s₀ ≠ 1; at s₀ = 1 ζ has a pole...) — hmm s₀ = 1 ∈ U? IsNontrivialZero 1: ζ 1 = 0? junk value; 0 < re 1 < 1 false (re 1 = 1). So 1 ∈ U regardless ✓. Ball around 1: discreteness of... ζ has a POLE at 1, not a zero; zero set closed & discrete — 1 is not in the zero set (need ζ(1) ≠ 0 — Mathlib: `riemannZeta_one`? hmm, what's riemannZeta 1 in Mathlib? Probably defined via the Laurent... In Mathlib, riemannZeta is the meromorphic continuation; value at the pole is arbitrary junk — likely 0! If riemannZeta 1 = 0 in Mathlib's junk convention, then s₀=1 IS in the zero set as a junk point — but not a nontrivial zero (re = 1 fails < 1). Discreteness: \"zero set\" — if ζ(1) = 0 junk, the set {ζ = 0} contains 1 but 1 is isolated from other zeros anyway (pole neighborhood: |ζ| → ∞ near 1 ⟹ no zeros nearby ✓ via the Laurent/pole fact). Ugh, this needs the pole-at-1 fact: Mathlib `riemannZeta_residue_one` / `tendsto` at 1... There IS `Zeta23`'s zetaA = (s−1)ζ(s) analytic with zetaA 1 = 1 (ii′-1b LiResidue) ⟹ near 1, ζ(s) = zetaA(s)/(s−1) with zetaA(1) = 1 ≠ 0 ⟹ ζ ≠ 0 in a punctured ball ✓ — banked in LiResidue.\n\nOK so the full case analysis for \"ball avoiding nontrivial zeros\":\n- ζ s₀ ≠ 0: zero set closed ⟹ ball avoiding all zeros. (Zero set = ζ⁻¹{0} closed needs continuity of ζ: `continuous_riemannZeta`? ζ is differentiable (Mathlib `differentiable_riemannZeta`? there's `differentiableAt_riemannZeta` for s ≠ 1) — hmm at s₀ = 1 continuity fails. If s₀ ≠ 1: differentiableAt ⟹ continuousAt ⟹ |ζ| > 0 nearby... Cleaner: ‖ζ s₀‖ > 0, continuousAt ⟹ ball with ‖ζ‖ > 0 ⟹ no zeros ✓. Mathlib: `differentiableAt_riemannZeta (hs : s ≠ 1)` exists as `differentiableAt_riemannZeta`. And for s₀ = 1 with \"ζ s₀ ≠ 0\" — junk value could be 0; if junk is 0, s₀=1 falls into the ζ = 0 case: re s₀ = 1, handle via zetaA (punctured ball no zeros).\n- ζ s₀ = 0: discreteness via analyticOrderAt? For s₀ ≠ 1: analytic at s₀, not identically zero (ζ ≡ 0 false — e.g. ζ(2) = π²/6 ≠ 0 — Mathlib `riemannZeta_two`? hmm `riemannZeta_two : riemannZeta 2 = π^2/6` might not exist... easier: zetaA(1) = 1 ≠ 0 ⟹ ζ not identically zero on any neighborhood of 1 ⟹ by identity principle zeros isolated... but the identity principle needs the right connectedness. Simpler: `analyticOrderAt riemannZeta s₀` is finite (≠ ⊤) iff ζ not identically zero near s₀ — Zeta23/LiSides had `zeta_order_ne_top_of_ne`! (\"zeta_order_ne_top_of_ne via the entire zetaA (identity principle on univ)\"). Banked ✓. Finite order at s₀ ⟹ ζ(s) = (s−s₀)^m·g(s), g analytic nonzero at s₀ ⟹ punctured ball with no zeros ✓ — that's exactly the NF machinery from ii′-1b. So: ball B(s₀,δ) with ζ ≠ 0 on the punctured ball; zeros in the ball: only possibly s₀ itself. s₀ ∈ U ⟹ not nontrivial ⟹ ball has no nontrivial zeros ✓.\n  - s₀ = 1 with junk ζ 1 = 0: zetaA route directly ✓ (also covered by: order at 1... analyticOrderAt at a pole — zetaA(1) = 1 gives ζ(s) = zetaA(s)/(s−1) explicitly, punctured ball no zeros ✓ — the LiResidue punctured agreement.)\n\nHmm wait — but actually for 5e-iii as scoped in STATE.md/D-068, do I need this generality? The scoped deliverables:\n(i) Summable at each s ∉ zeros;\n(ii) analytic on ℂ ∖ zeros;\n(iii) isolation at each zero ⟹ series minus ρ-term analytic at ρ.\n\nFor (ii) \"ℂ ∖ zeros\" = U. Points of U: s₀ with ζ s₀ ≠ 0 (easy case) and s₀ with ζ s₀ = 0 but not nontrivial — these are: trivial zeros −2n (n ≥ 1), s₀ = 1 (if junk 0), possibly re = 0 points (none, but I don't need to prove none — the discreteness argument covers them uniformly!). So:\n\nFor s₀ ∈ U with ζ s₀ = 0, s₀ ≠ 1: NF machinery (zeta_order_ne_top) ⟹ punctured ball zero-free ⟹ any zero of ζ in the ball is s₀ itself ⟹ not nontrivial (s₀ ∈ U) ⟹ ball ⊆ U ✓.\nFor s₀ = 1 ∈ U: zetaA punctured ball ✓.\nFor s₀ ∈ U with ζ s₀ ≠ 0: continuity ⟹ ball with ζ ≠ 0 ⟹ ⊆ U ✓ (need s₀ ≠ 1 for differentiability — if s₀ = 1 then ζ s₀ = junk; if junk ≠ 0, then... hmm, Mathlib's `riemannZeta 1`: let me check. There is `riemannZeta_one`? I don't recall. Let me grep. Actually the pole: lim_{s→1} (s−1)ζ(s) = 1. Mathlib might define riemannZeta 1 = 0. Let me check quickly.)\n\nActually, you know what — simpler unified approach: for ANY s₀ ∈ U, I get the ball from:\n- s₀ ≠ 1: either ζ s₀ ≠ 0 (continuity ball) or ζ s₀ = 0 (NF punctured ball).\n- s₀ = 1: zetaA punctured ball.\n\nFine. Now — do I also want \"U is open\" as a corollary? AnalyticOnNhd ℂ seriesFun U directly gives analytic at each point with a neighborhood. With the per-point balls, `AnalyticOnNhd` unfolds to ∀ s ∈ U, AnalyticAt... hmm actually AnalyticOnNhd f U := ∀ x ∈ U, AnalyticAt f x? No: `AnalyticOnNhd 𝕜 f s := ∀ x ∈ s, ∃ t ∈ 𝓝 x, AnalyticOn 𝕜 f t`? Or \"AnalyticOnNhd f s ↔ ∀ x ∈ s, AnalyticAt f x\"? There's `analyticOnNhd_iff_analyticAt`? Hmm — in Mathlib, AnalyticOnNhd f s means ∀ x ∈ s, ∃ u ∈ 𝓝 x, AnalyticOn f u... There might be an iff with pointwise AnalyticAt: `analyticOnNhd_iff_isOpen`... Let me just target: ∀ s₀ ∈ U, AnalyticAt ℂ seriesFun s₀, and package as AnalyticOnNhd via whatever constructor the Li* files used (`DifferentiableOn.analyticOnNhd` needed DifferentiableOn on an open set). With per-point balls: on ball B(s₀,δ) (open), M-test ⟹ DifferentiableOn ⟹ analyticOnNhd on the ball ⟹ AnalyticAt at s₀. Then `analyticAt_iff`... To get AnalyticOnNhd on U from pointwise: there's `AnalyticOnNhd` def: `∀ x ∈ s, AnalyticAt f x`?? I think in recent Mathlib, `AnalyticOnNhd 𝕜 f s : Prop := ∀ x ∈ s, AnalyticAt 𝕜 f x`? Hmm no. Let me check: Mathlib def — `AnalyticOnNhd 𝕜 f s := ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)`? I don't remember exactly. There IS `analyticOnNhd_univ_iff_analyticAt`... I'll check in the Mathlib source when writing. Not critical.\n\nNow the M-test on the ball: domain = Metric.ball s₀ δ where the ball avoids nontrivial zeros. Bound: for ρ with ‖ρ‖ ≥ R₀ := max 2 (2(‖s₀‖+δ)): ∀ s ∈ ball: ‖s‖ ≤ ‖s₀‖+δ ≤ R₀/2 ≤ ‖ρ‖/2 ⟹ ‖s−ρ‖ ≥ ‖ρ‖/2; and ‖1/(s−ρ)+1/ρ‖ = ‖s/(ρ(s−ρ))‖ ≤ ‖s‖/(‖ρ‖·‖ρ‖/2) = 2‖s‖/‖ρ‖². Then ‖seriesTerm s ρ‖ = mult·that ≤ 2(‖s₀‖+δ)·mult/‖ρ‖² ≤ 2(‖s₀‖+δ)·mult·(C/(1+‖γ‖²)) with the comparison 1/‖ρ‖² ≤ C/(1+‖γ‖²) for ‖ρ‖ ≥ 2 — compute C: re ∈ (0,1): 1+‖γ‖² = 1+im²+(1/2−re)² ≤ 1+im²+1/4; ‖ρ‖² = re²+im² ≥ im². ‖ρ‖ ≥ 2 ⟹ im² ≥ 4−1 = 3 ⟹ 1+‖γ‖² ≤ 5/4+im² ≤ 5/4·(im²)/3·... let me do cleanly: 1+‖γ‖² ≤ 5/4 + im² ≤ (5/12)im² + im²·... hmm: 5/4 ≤ (5/12)·3 ≤ (5/12)im². So 1+‖γ‖² ≤ (5/12+1)im² = (17/12)im² ≤ (17/12)‖ρ‖². So 1/‖ρ‖² ≤ (17/12)/(1+‖γ‖²). Fine: u ρ := 2(‖s₀‖+δ)·(17/12)·mult/(1+‖γ‖²) — summable by zero_sum_inv_sq.mul_left ✓.\n\nCofinite: {ρ : ‖ρ‖ < R₀} is finite (the LiSkeleton pattern — Set.Finite of subtype, then cofinite membership: `Filter.mem_cofinite` = complement finite ✓).\n\nHmm wait — one wrinkle: `of_norm_le_summable_eventually` gives HasSumUniformlyOn for the FULL tsum function on the ball, but the eventual bound holds only for ρ outside a finite set; inside the finite set the terms must be... looking at `tendstoUniformlyOn_tsum_of_cofinite_eventually` — it handles this: the finite exceptional set's terms just need to be functions; uniform convergence of finite sums is unaffected by a fixed finite set (each term must be bounded?? No — even that's not needed; the finite head partial sums are fixed functions; convergence of the tail uniformly ⟹ whole thing. The head terms appear in every partial sum but they're the SAME fixed functions added — uniform convergence is about the tail. Actually for HasSumUniformlyOn via finsets-atTop: g_t = Σ_{ρ ∈ t} f_ρ → Σ_{head} + tail uniformly. Yes fine, no boundedness needed on head terms — but wait, they DO need to be finite-valued on the domain for the partial sum functions to make sense — they're ℂ-valued functions (junk at poles is 0 ∈ ℂ, fine). And the DIFFERENTIABILITY of each partial sum on the ball DOES need head terms differentiable on the ball — head terms ρ₁ ≠ any point of the ball... head terms with ρ₁ in the ball would break differentiability — but the ball avoids ALL nontrivial zeros ✓ so every term is differentiable on the ball ✓ (1/(s−ρ₁): s ≠ ρ₁ on the ball ✓; 1/ρ₁: ρ₁ ≠ 0 since re ρ₁ > 0 ✓).\n\nFor the reduced series at ρ₀ (isolation part): on B(ρ₀, δ/2), terms: ρ₀-term zeroed; other terms ρ₁: ‖ρ₁ − s‖ ≥ δ/2 for s ∈ B(ρ₀,δ/2) (isolation: ‖ρ₁−ρ₀‖ ≥ δ). All terms differentiable on the ball ✓. M-test eventually: same tail bound; head includes ρ₀ (zeroed — fine, differentiable) ✓.\n\nSo the isolation lemma: ∃ δ > 0, ∀ ρ₁ nontrivial zero, ρ₁ ≠ ρ₀ → ‖ρ₁ − ρ₀‖ ≥ δ. From: the set Z := closedBall(ρ₀, 1) ∩ {nontrivial zeros} is finite (compact-inter pattern); Z \\ {ρ₀} finite; distances positive; min over finite set — if empty, δ = 1. Formalize: Z.finite; the set of distances {‖ρ₁ − ρ₀‖ : ρ₁ ∈ Z, ρ₁ ≠ ρ₀} is a finite set of positive reals — take its min (or 1 if empty), δ := min/2.\n\nAlso needed: ρ ≠ 0 for nontrivial ρ (re > 0 ⟹ ρ ≠ 0 ✓ via norm_pos_iff... re ρ > 0 ⟹ ρ ≠ 0 since re 0 = 0).\n\nNow, also for later convenience, the pointwise summability at arbitrary s (including zeros): `seriesSummable (s : ℂ) : Summable (fun ρ => seriesTerm s ρ)`. Proof via the M-test machinery locally when s ∉ zeros... but at s = ρ₀ zero: the reduced series summable (M-test on ball) + one extra term: `summable_... ` — Summable (f + single term) ⟸ Summable.add / summable of finitely-supported modification: `Summable.add` of the reduced and the indicator... Or: the reduced series = series with if; Summable (fun ρ => if ρ = ρ₀ then 0 else f ρ) and (fun ρ => if ρ = ρ₀ then f ρ₀... this is `Summable.add` with a `summable_of_hasFiniteSupport` single-point function. Fine.\n\nHmm, actually simpler: prove summability at each s directly via the same dominator argument as liSummable (D-function trick): for fixed s: for ‖ρ‖ ≥ max 2 (2‖s‖): ‖seriesTerm s ρ‖ ≤ 2‖s‖·(17/12)mult/(1+‖γ‖²); the complement finite. Clone `liSummable`'s D-pattern. That's self-contained, no balls needed. Then the ball-based M-test gives analyticity. But note the M-test on a ball around s ALSO gives pointwise HasSum at s hence Summable — but only for s ∈ U. For s = ρ₀ (a zero), summability needs the junk-term argument. Do I need summability at zeros? The capstone identity is stated only for s ∉ zeros ∪ {0,1} ∪ {−2n}, so no. But seriesFun is DEFINED as a tsum for all s; having `seriesSummable` for all s makes rewriting safer. I'll do the liSummable-clone (works for all s uniformly, cheap).\n\nHmm wait, actually for s = ρ₀, the term seriesTerm ρ₀ ρ₀ = mult·(1/(ρ₀−ρ₀) + 1/ρ₀) = mult·(0 + 1/ρ₀) junk-fine, and the tail bound at s = ρ₀: for ‖ρ‖ ≥ 2‖ρ₀‖: same bound. And the finite head: D-function = ‖term‖ pointwise — fine, no singularity issues (junk 0 is a number). So yes, the D-trick gives Summable for ALL s with zero case-splitting. \n\nNow the plan for LiSeries.lean:\n\n```\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\nimport NguyenRH1.LiSkeleton (?? — for what? zeroMult is from Zeta23.Statement; gammaOf from Zeta23 Defs; the finiteness pattern uses IsCompact.inter_riemannZetaZeros_finite — Mathlib. Maybe LiResidue for zeta_order_ne_top_of_ne and the zetaA punctured facts, LiSides?)\n```\n\nCheck what LiSides has: `zeta_order_ne_top_of_ne`. And LiResidue: zetaA analytic at 1, zetaA 1 = 1, punctured agreement.\n\nDeclarations:\n\n1. `def seriesTerm (s : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ := (zeroMult ρ : ℂ) * (1 / (s - ρ) + 1 / ρ)`\n2. `def seriesFun (s : ℂ) : ℂ := ∑' ρ, seriesTerm s ρ`\n3. `lemma normSq_gammaOf_comparison`: for ρ nontrivial zero with 2 ≤ ‖ρ‖: (1/‖ρ‖² ≤ (17/12)/(1+normSq (gammaOf ρ)))? Or the direct form: 2·R·mult/‖ρ‖² ≤ (17/6)·R·mult/(1+‖γ‖²). Let me define the constant cleanly: for re ∈ (0,1), 2 ≤ ‖z‖: 1 + normSq(γ_z) ≤ (17/12)‖z‖². Hmm let me double check: normSq(γ) = im² + (1/2−re)². (1/2−re)² ≤ 1/4 (re ∈ (0,1) ⊂ |1/2−re| < 1/2). 1+‖γ‖² ≤ 1 + im² + 1/4 = 5/4 + im². ‖z‖² = re² + im² ≥ im² (drop re²) — hmm and I need 5/4 ≤ (5/12)im²: im² = ‖z‖² − re² ≥ 4 − 1 = 3 ⟹ (5/12)im² ≥ 5/4 ✓. So 1+‖γ‖² ≤ (5/12)im² + im² = (17/12)im² ≤ (17/12)‖z‖² ✓.\n\n4. `lemma seriesTerm_norm_le {s} {ρ} (hρ : R ≤ ‖ρ‖) (hs : ‖s‖ ≤ R/2) (hR : 4 ≤ R or something)`: ‖seriesTerm s ρ‖ ≤ (17/6)·R·mult/(1+‖γ‖²)... let me set: conditions 2 ≤ ‖ρ‖ and 2‖s‖ ≤ ‖ρ‖. Then ‖1/(s−ρ)+1/ρ‖: 1/(s−ρ)+1/ρ = s/(ρ(s−ρ)): (s−ρ) + ρ... 1/(s−ρ) + 1/ρ = (ρ + s − ρ)/(ρ(s−ρ)) = s/(ρ(s−ρ)) ✓ (needs ρ ≠ 0, s ≠ ρ). ‖s/(ρ(s−ρ))‖ = ‖s‖/(‖ρ‖‖s−ρ‖) ≤ ‖s‖/(‖ρ‖(‖ρ‖/2)) = 2‖s‖/‖ρ‖². Then total: ‖term‖ ≤ mult·2‖s‖/‖ρ‖² ≤ mult·2‖s‖·(17/12)/(1+‖γ‖²).\n\n5. `theorem seriesSummable (s : ℂ) : Summable (seriesTerm s)` — D-trick clone. Wait, in liSummable the D-trick used `Summable.of_norm_bounded hD` where D = if tail then dominator else ‖term‖. The dominator: (17/6)‖s‖·... hmm need ‖s‖ — for s = 0: bound 2‖s‖/‖ρ‖² = 0 — fine (terms are mult·(1/(0−ρ)+1/ρ) = mult·0 = 0 actually! 1/(0−ρ) + 1/ρ = −1/ρ+1/ρ = 0. So seriesFun 0 = 0 — nice). Dominator constant: (17/6)·max(1,‖s‖)·... just use (17/6)·‖s‖ but for s=0 the dominator is 0 — can't dominate nonzero terms... but at s=0 all terms ARE 0 exactly. Handle: use C := (17/6)·(‖s‖) and case s = 0 separately (all terms zero), or use C := (17/6)·(‖s‖+1)... but then the tail bound needs ‖term‖ ≤ C·mult/(1+‖γ‖²) with C independent of the tail condition — with ‖s‖+1: ‖term‖ ≤ 2‖s‖·(17/12)mult/(1+‖γ‖²) ≤ (17/6)(‖s‖+1)·mult/(1+‖γ‖²)? 2‖s‖·(17/12) = (17/6)‖s‖ ≤ (17/6)(‖s‖+1) ✓. Good: dominator u := (17/6)(‖s‖+1)·mult/(1+‖γ‖²), summable via zero_sum_inv_sq.mul_left.\n\n6. Isolation: `theorem exists_ball_no_nontrivial_zero (ρ₀ : {ρ // IsNontrivialZero ρ}) : ∃ δ > 0, ∀ ρ₁ : {ρ // IsNontrivialZero ρ}, ρ₁ ≠ ρ₀ → δ ≤ ‖(ρ₁:ℂ) − ρ₀‖`. Via finite zeros in closedBall(ρ₀,1) + min.\n\n7. Ball-avoidance for any s₀ ∈ U: `theorem exists_ball_avoid (s₀ : ℂ) (hs₀ : ¬ IsNontrivialZero s₀) : ∃ δ > 0, ∀ ρ : {ρ // IsNontrivialZero ρ}, ρ ∉... ` i.e. ∀ ρ nontrivial, δ ≤ ‖ρ − s₀‖. Cases as discussed. Uses: differentiability of ζ at s₀ ≠ 1 (Mathlib `differentiableAt_riemannZeta`), NF machinery (`zeta_order_ne_top_of_ne` from LiSides + analyticOrderAt finite ⟹ local factorization — what exactly does LiSides/LiResidue provide? ii′-1b has \"logDeriv NF residues at zeros\" — the local factorization ζ = (s−ρ)^m · g. Let me check what's available), zetaA at 1.\n\nHmm — this case analysis is the fiddliest part. Alternative that avoids the ζ s₀ = 0 sub-case ENTIRELY: note that for the eventual application (5e-iv/v), I need analyticity at: generic points (ζ ≠ 0), trivial zeros −2n, 0, 1 — and separately the reduced-series analyticity AT each nontrivial zero (part iii). The ζ s₀ = 0 ∧ s₀ ∈ U case = {−2n} ∪ {1-junk} ∪ {other junk points}. I still need those covered. The NF factorization: from `analyticOrderAt riemannZeta s₀ ≠ ⊤` (LiSides `zeta_order_ne_top_of_ne` — check its hypothesis: \"of_ne\" — of ζ s₀ ≠... let me check its statement) we get... hmm, analyticOrderAt at s₀ where ζ s₀ = 0: order = some m ≥ 1; the factorization ζ = (s−s₀)^m·g near s₀ with g analytic, g(s₀) ≠ 0 — Mathlib: `AnalyticAt.exists...`? There's `analyticOrderAt_eq_natCast` used in LiTrivialZeros/LiContour — and the existence of the factorization: `analyticOrderAt` API: `AnalyticAt.order...`? In this Mathlib: `analyticOrderAt_eq_natCast_iff`? LiTrivialZeros used \"the ii′-4c pattern via analyticOrderAt_eq_natCast\" — there's presumably a lemma giving ζ =ᶠ (s−s₀)^m · g. Let me check what LiSides has for the NF at zeros.\n\nLet me grep LiSides for the factorization.","signature":""},{"type":"text","text":"Now let me check the NF (local factorization) machinery from ii′-1b that I'll reuse for the ball-avoidance argument, plus `zeta_order_ne_top_of_ne`."},{"type":"tool_use","id":"Grep_21","name":"Grep","input":{"pattern":"zeta_order_ne_top|analyticOrderAt_eq_natCast|exists.*pow.*mul|order_ne_top","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1","output_mode":"content","-n":true,"head_limit":40},"extra_content":null}]