[{"type":"thinking","thinking":"The audit: a per-file PrintAxioms script run through `lake env lean`, output saved. I'll create a session-028 audit script at the end.\n\nNow let me set up the task list and write LiSeries.lean. Plan of declarations:\n\n```\n/- §0 — the term and the series -/\ndef seriesTerm (s : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ\ndef seriesFun (s : ℂ) : ℂ\n\n/- §1 — the norm comparison and the tail bound -/\nlemma one_add_normSq_gammaOf_le (ρ : {ρ // IsNontrivialZero ρ}) (hρ : 2 ≤ ‖(ρ:ℂ)‖) :\n    1 + Complex.normSq (gammaOf (ρ:ℂ)) ≤ 17/12 * ‖(ρ:ℂ)‖^2\n\nlemma seriesTerm_norm_le {s : ℂ} (ρ : {ρ // IsNontrivialZero ρ})\n    (hρ : 2 ≤ ‖(ρ:ℂ)‖) (hs : 2 * ‖s‖ ≤ ‖(ρ:ℂ)‖) :\n    ‖seriesTerm s ρ‖ ≤ (17/6) * ‖s‖ * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ:ℂ)))\n\n/- §2 — summability for all s (the D-trick) -/\ntheorem seriesSummable (s : ℂ) : Summable (seriesTerm s)\n\n/- §3 — finite balls in the subtype (shared finiteness) -/\nlemma finite_subtype_norm_lt (R : ℝ) : {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ:ℂ)‖ < R}.Finite\n\n/- §4 — analyticity on the complement of the nontrivial zeros -/\nlemma exists_ball_avoid_nontrivialZeros (s₀ : ℂ) (hs₀ : ¬ IsNontrivialZero s₀) :\n    ∃ δ > 0, ∀ ρ : {ρ // IsNontrivialZero ρ}, (ρ:ℂ) ∉ Metric.ball s₀ δ\n\ntheorem seriesFun_analyticAt {s₀ : ℂ} (hs₀ : ¬ IsNontrivialZero s₀) : AnalyticAt ℂ seriesFun s₀\n\ntheorem seriesFun_analyticOnNhd : AnalyticOnNhd ℂ seriesFun {s | ¬ IsNontrivialZero s}\n\n/- §5 — isolation and the reduced series -/\ntheorem nontrivialZero_isolated (ρ₀ : {ρ // IsNontrivialZero ρ}) :\n    ∃ δ > 0, ∀ ρ₁ : {ρ // IsNontrivialZero ρ}, ρ₁ ≠ ρ₀ → δ ≤ ‖(ρ₁:ℂ) - ρ₀‖\n\ndef seriesTermSub (ρ₀ : {ρ // IsNontrivialZero ρ}) (s : ℂ) (ρ : {ρ // IsNontrivialZero ρ}) : ℂ :=\n  if ρ = ρ₀ then 0 else seriesTerm s ρ\n\ndef seriesFunSub (ρ₀) (s : ℂ) : ℂ := ∑' ρ, seriesTermSub ρ₀ s ρ\n\ntheorem seriesFunSub_analyticAt (ρ₀) : AnalyticAt ℂ (seriesFunSub ρ₀) ρ₀\n\ntheorem seriesFun_sub_term_eq (ρ₀) : ∀ s ∈ ball ρ₀ (δ/2), seriesFun s - seriesTerm s ρ₀ = seriesFunSub ρ₀ s\n\ntheorem seriesFun_sub_self_term_analyticAt (ρ₀) :\n    AnalyticAt ℂ (fun s => seriesFun s - seriesTerm s ρ₀) ρ₀\n\ntheorem seriesFun_sub_polar_analyticAt (ρ₀) :\n    AnalyticAt ℂ (fun s => seriesFun s - (zeroMult (ρ₀:ℂ) : ℂ) / (s - ρ₀)) ρ₀\n```\n\nWait — in the term `seriesTerm s ρ₀`, ρ₀ : subtype; the def seriesTerm (s) (ρ : subtype) — seriesTerm s ρ₀ with ρ₀ subtype ✓. And `(zeroMult ρ₀ : ℂ)` — zeroMult takes ℂ; zeroMult ρ₀ with ρ₀ subtype coerces ✓ (liSummand did `(zeroMult ρ : ℂ)`).\n\nAlso useful constant naming: `17/6 * M * mult / (1+γ²)` where M = bound on ‖s‖.\n\nDetails on §1 proof: normSq (gammaOf z) = z.im² + (1/2 − z.re)² (proved in LiSkeleton `hgam` line 242-244 via `Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im`). I can reuse that rewrite.\n\nFor hρ : 2 ≤ ‖ρ‖, hzre : 0 < re < 1:\n- him2 : 3 ≤ ρ.im²: ρ.im² = ‖ρ‖² − ρ.re² ≥ 4 − 1 = 3. From Complex.normSq_apply: ‖ρ‖² = re²+im². re² < 1 (|re| < 1: 0 < re < 1 ⟹ re² < 1 — sq_lt... nlinarith with 0 < re < 1: re^2 < 1 via mul_lt_mul... nlinarith [hz.2.1, hz.2.2] can do re^2 < 1? nlinarith with products: re*re < 1*re·... hint: re^2 < re < 1 since 0<re<1: nlinarith [mul_lt_mul_of_pos... nlinarith can find re*re ≤ 1*re = re < 1 given 0 < re, re < 1 — yes with product hint mul_self... Let me just use nlinarith [hz.2.1, hz.2.2, sq_nonneg ...] — nlinarith multiplies pairs of hypotheses; re*re < 1*1 needs re < 1 and re < 1 with nonneg... nlinarith should find re^2 < 1 from 0 < re ∧ re < 1: it considers product (1−re)·re > 0 ⟹ re² < re < 1 ✓.\n- Then 1 + normSq γ ≤ 1 + im² + 1/4 ≤ (5/12)·3 + im² ≤ (5/12)im² + im² = 17/12 im² ≤ 17/12 ‖ρ‖².\n  The step \"1 ≤ (5/12)·im²\": im² ≥ 3 ⟹ (5/12)im² ≥ 5/4 ≥ 1 ✓... wait I need 1 + 1/4 ≤ (5/12)im²: 5/4 ≤ (5/12)·3 = 5/4 ✓ equality. Good.\n  And normSq γ = im² + (1/2−re)² ≤ im² + 1/4: (1/2−re)² ≤ 1/4 since |1/2−re| ≤ 1/2 ⟺ re ∈ [0,1] ✓ nlinarith.\n  So 1 + normSq γ ≤ 1 + im² + 1/4 ≤ (5/12)im² + im² = (17/12)im² ≤ (17/12)‖ρ‖² ✓ (‖ρ‖² = re²+im² ≥ im²).\n\n§1 seriesTerm_norm_le: \n- ρ ≠ 0: ‖ρ‖ ≥ 2 > 0 ⟹ norm_pos_iff.\n- s − ρ ≠ 0: ‖s−ρ‖ ≥ ‖ρ‖ − ‖s‖ ≥ ‖ρ‖/2 ≥ 1 > 0.\n- algebra: 1/(s−ρ) + 1/ρ = s/(ρ·(s−ρ)): field_simp ⟹ ρ·(s−ρ) ≠ 0.\n  Check: 1/(s−ρ) + 1/ρ = (ρ + s − ρ)/((s−ρ)ρ) = s/((s−ρ)ρ) ✓.\n- norm: ‖s‖/(‖s−ρ‖·‖ρ‖) ≤ ‖s‖/((‖ρ‖/2)·‖ρ‖) = 2‖s‖/‖ρ‖².\n- Then ‖seriesTerm‖ = mult·‖…‖ (zeroMult nonneg cast: norm_mul, Complex.norm_natCast — zeroMult ρ : ℕ cast to ℂ; ‖(zeroMult ρ : ℂ)‖ = zeroMult ρ as ℝ ✓ `Complex.norm_natCast`).\n- ≤ mult·2‖s‖/‖ρ‖² ≤ mult·2‖s‖·(17/12)/(1+‖γ‖²) [from §1 lemma via div: 1/‖ρ‖² ≤ (17/12)/(1+‖γ‖²) from 1+‖γ‖² ≤ (17/12)‖ρ‖² — `div_le_div`...: a/b form: 1+γ² ≤ c·ρ² ⟹ 1/ρ² ≤ c/(1+γ²): via `div_le_div_iff` or le_div_iff₀ juggling: 1/ρ² ≤ c/(1+γ²) ⟺ 1+γ² ≤ c·ρ² (cross-multiply, both sides positive) ✓.\n- = (17/6)‖s‖·mult/(1+‖γ‖²) by ring.\n\n§2 seriesSummable: clone liSummable exactly:\n- hbase : Summable (fun ρ => (17/6)(‖s‖+1)·mult/(1+‖γ‖²)) := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left _\n- D ρ := if 2*max 2 ‖s‖ ≤ ‖ρ‖... hmm the tail condition: need 2 ≤ ‖ρ‖ AND 2‖s‖ ≤ ‖ρ‖. Single condition: ‖ρ‖ ≥ R₀ where R₀ := max 2 (2‖s‖). D := if R₀ ≤ ‖ρ‖ then dominator else ‖term‖.\n- finiteness of {ρ | ¬ R₀ ≤ ‖ρ‖} = {ρ | ‖ρ‖ < R₀}: the LiSkeleton pattern with closedBall(0, R₀):\n  hzeros : closedBall 0 R₀ ∩ {IsNontrivialZero} ⊆ closedBall 0 R₀ ∩ riemannZetaZeros (via hz.2.1... wait IsNontrivialZero z = (ζ z = 0 ∧ 0 < re ∧ re < 1); hz.2.1 is 0 < re... the .1 is ζ z = 0. In LiSkeleton: `intro z hz; exact ⟨hz.1, hz.2.1⟩` — hmm hz : z ∈ closedBall ∩ {ρ | IsNontrivialZero ρ}; hz.2 : IsNontrivialZero z; hz.2.1 : riemannZeta z = 0? No wait — IsNontrivialZero is an And: .1 : riemannZeta ρ = 0, .2.1 : 0 < re, .2.2 : re < 1. In LiSkeleton line 311-312: `intro z hz; exact ⟨hz.1, hz.2.1⟩` where the target is closedBall ∩ riemannZetaZeros — membership in riemannZetaZeros is ζ z = 0 = hz.2.1... hmm hz.2.1 of (hz.2 : ζ z = 0 ∧ 0 < re ∧ re < 1) is (ζ z = 0).1? No: hz.2.1 = (ζ z = 0 ∧ (0 < re ∧ re < 1)).1? In Lean, for `a ∧ b ∧ c` which is `a ∧ (b ∧ c)`: hz.2.1 = first component of hz.2 = (ζ z = 0). Hmm: hz.2 : IsNontrivialZero z i.e. (ζ z = 0 ∧ 0 < re ∧ re < 1). hz.2.1 : ζ z = 0 ✓ (`.1` of the And). And hz.2.2.1 : 0 < re? But liSummand_norm_le used hz.2.1.le : 0 ≤ re where hz := ρ.2 : 0 < re ∧ re < 1... wait that was hz := ρ.2 where ρ.2 : IsNontrivialZero ρ — so hz.2.1 : 0 < ρ.re? But IsNontrivialZero unfolds to (ζ ρ = 0 ∧ 0 < re ∧ re < 1), and hz = ρ.2 is the whole conjunction. hz.2.1 : (0 < re ∧ re < 1).1 = 0 < re? Hmm: hz.1 : ζ ρ = 0; hz.2 : 0 < re ∧ re < 1; hz.2.1 : 0 < re; hz.2.2 : re < 1. And liSummand_norm_le: `have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le` ✓ (0 < re).le. But then `hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le` ✓ re < 1. OK consistent. And in liSummable: `exact ⟨hz.1, hz.2.1⟩` — hz : z ∈ ball ∧ IsNontrivialZero z: hz.2.1 : riemannZeta z = 0? hz.2 : IsNontrivialZero z = (ζ z = 0 ∧ ...); hz.2.1 : ζ z = 0 ✓ membership in riemannZetaZeros (mem_riemannZetaZeros is .rfl so direct) ✓.\n  \n  Then finite subtype set via image under Subtype.val + injectivity (Set.Finite.of_finite_image himg Subtype.val_injective.injOn) — copy verbatim from liSummable (lines 306-321).\n\n- hE : Summable (D − dominator): summable_of_hasFiniteSupport — hfin.subset: support of (D − dominator): D − dominator ≠ 0 ⟹ ¬(R₀ ≤ ‖ρ‖): if R₀ ≤ ‖ρ‖ then D = dominator ⟹ difference 0 ✓. Copy.\n- hD := hbase.add hE + funext ring-eq ✓.\n- Summable.of_norm_bounded hD (fun ρ => ...) with by_cases R₀ ≤ ‖ρ‖: pos: seriesTerm_norm_le (with the two preconditions: 2 ≤ ‖ρ‖ from R₀ ≤ ‖ρ‖ and R₀ ≥ 2; 2‖s‖ ≤ ‖ρ‖ from R₀ ≥ 2‖s‖) ⟹ ‖term‖ ≤ (17/6)‖s‖·mult/(1+γ²) ≤ (17/6)(‖s‖+1)·mult/(1+γ²) — need the dominator monotone upgrade: mult·(17/6)‖s‖/(1+γ²) ≤ mult·(17/6)(‖s‖+1)/(1+γ²): both factors nonneg, ‖s‖ ≤ ‖s‖+1, 1+γ² > 0: div_le_div_of_nonneg... just: (17/6)·‖s‖·m/d ≤ (17/6)·(‖s‖+1)·m/d ⟺ (17/6)‖s‖ ≤ (17/6)(‖s‖+1) (multiply by m/d ≥ 0) ✓ mul_le_mul_of_nonneg_right... careful ordering: a·‖s‖·m/d: reassociate: ((17/6)·m/d)·‖s‖ ≤ ((17/6)·m/d)·(‖s‖+1) ✓ mul_le_mul_of_nonneg_left (linarith) (positivity).\n  neg: D = ‖term‖ ✓ le_refl.\n\n§4 exists_ball_avoid_nontrivialZeros: cases:\n```\nby_cases h1 : s₀ = 1\n· -- zetaA route: zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 1, zetaA w ≠ 0\n  -- + eventually_ne_nhds (1:ℂ)... need: for w ≠ 1 near 1: ζ w = zetaA w/(w−1) ≠ 0.\n  -- combine: filter_upwards [zetaA_ne_zero_near_one, eventually_ne_nhds (one_ne... hmm s₀ = 1: eventually_ne_nhds (show (1:ℂ) ≠ 1?? no: eventually w ≠ 1: `eventually_ne_nhds (show (1:ℂ) ≠ 1 from ...)` — false! eventually_ne_nhds (h : a ≠ b) : ∀ᶠ x in 𝓝 a, x ≠ b. We want ∀ᶠ w in 𝓝 1, w ≠ 1 — that's NOT eventually true ( neighborhoods contain 1). Use 𝓝[≠]: self_mem_nhdsWithin. Instead: take the ball from zetaA_ne_zero_near_one via eventually_nhds_iff_ball; then for w ∈ ball, w ≠ 1: ζ w = zetaA w/(w−1): from zetaA_apply: zetaA w = (w−1)·ζ w ⟹ ζ w = zetaA w/(w−1) ≠ 0 ✓. So: ∀ w ∈ ball(1, ε), w ≠ 1 → ζ w ≠ 0. And any nontrivial zero ρ in the ball: ρ ≠ 1 (re < 1 ⟹ ρ ≠ 1: if ρ = 1 then re = 1 not < 1 — actually just: IsNontrivialZero ρ ⟹ re < 1 ⟹ ρ ≠ 1 since re 1 = 1). Then ζ ρ ≠ 0 contradicts ρ.2.1. \n  -- So the ball works: ∀ ρ nontrivial, ρ ∉ ball.\n· by_cases h0 : riemannZeta s₀ = 0\n  · -- NF route: obtain ⟨h, hh, hh0, hfh⟩ := (analyticAt_riemannZeta h1).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne h1)\n    -- hh.continuousAt.eventually_ne hh0 : ∀ᶠ w, h w ≠ 0 → ball ε₁\n    -- hfh eventually → ball ε₂\n    -- on ball min: w ≠ s₀ → ζ w = (w−s₀)^m·h w ≠ 0. So ζ-zeros in ball ⊆ {s₀}; s₀ not nontrivial (hs₀) ✓\n  · -- continuity route: (analyticAt_riemannZeta h1).continuousAt.eventually_ne h0 → ball ✓ ζ ≠ 0 throughout\n```\nNeed: `eventually_nhds_iff_ball : (∀ᶠ y in 𝓝 x, P y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, P y` — Mathlib `Metric.eventually_nhds_iff_ball` ✓.\n\n§4 seriesFun_analyticAt: given δ from the ball-avoidance:\n- Domain: Metric.ball s₀ δ.\n- R₀ := max 2 (2·(‖s₀‖ + δ)).\n- u : subtype → ℝ := fun ρ => (17/6)·(‖s₀‖+δ)·mult/(1+‖γ‖²) — Summable: zero_sum_inv_sq.mul_left.\n- hfu : ∀ᶠ ρ in cofinite, ∀ s ∈ ball, ‖seriesTerm s ρ‖ ≤ u ρ: mem_cofinite: the set A := {ρ | R₀ ≤ ‖ρ‖} is cofinite (complement finite by §3's finite_subtype_norm_lt with complement {‖ρ‖ < R₀}: `Set.Finite.compl_mem_cofinite`? signature: (hs : s.Finite) : sᶜ ∈ cofinite — check name; alternative `Filter.mem_cofinite.mpr`. Filter.cofinite: s ∈ cofinite ↔ sᶜ.Finite — `Filter.mem_cofinite : s ∈ cofinite ↔ Set.Finite sᶜ`? I'll grep. For ρ ∈ A: 2 ≤ ‖ρ‖ ✓ (R₀ ≥ 2); ∀ s ∈ ball: ‖s‖ ≤ ‖s−s₀‖+‖s₀‖ < δ + ‖s₀‖ ⟹ 2‖s‖ ≤ 2(‖s₀‖+δ) ≤ R₀ ≤ ‖ρ‖ ✓; then seriesTerm_norm_le gives ≤ (17/6)‖s‖·… ≤ (17/6)(‖s₀‖+δ)·… ✓ (need ‖s‖ ≤ ‖s₀‖+δ: from dist triangle: ‖s‖ = ‖s − s₀ + s₀‖ ≤ ‖s−s₀‖ + ‖s₀‖ < δ + ‖s₀‖; ≤ fine).\n- HasSumUniformlyOn via of_norm_le_summable_eventually hu hfu — wait, the conclusion limit function is `fun x ↦ ∑' n, f n x` = fun s => ∑' ρ, seriesTerm s ρ = seriesFun ✓ (defeq; may need `show`).\n- → TendstoUniformlyOn (hasSumUniformlyOn_iff_tendstoUniformlyOn.mp) → .tendstoLocallyUniformlyOn → .differentiableOn hdiff isOpen_ball where hdiff : ∀ᶠ t in atTop (Finset), DifferentiableOn ℂ (fun s => ∑ ρ ∈ t, seriesTerm s ρ) (ball): Filter.Eventually.of_forall; each partial sum: DifferentiableAt.sum of terms: fun s => (zeroMult ρ : ℂ)·(1/(s−ρ)+1/ρ): differentiable at s ∈ ball: s ≠ ρ (ρ ∉ ball ✓) and ρ ≠ 0 ✓: (differentiableAt_const _).div ((differentiableAt_id.sub (differentiableAt_const _)) hsr... .sub / .add composition:\n  term s = c·(1/(s−ρ) + 1/ρ): DifferentiableAt ℂ (fun s => 1/(s−↑ρ)) s: (differentiableAt_const (1:ℂ)).div (differentiableAt_id.sub (differentiableAt_const _)) (sub_ne_zero: s − ρ ≠ 0 ✓); plus const 1/ρ: differentiableAt_const; .add; .const_mul or .mul const.\n- .analyticOnNhd isOpen_ball → apply s₀ (mem_ball_self hδ) : AnalyticAt ✓.\n\nWait — `TendstoLocallyUniformlyOn.differentiableOn`: signature from LiDigamma: `htend.differentiableOn _ dpsiDomain_isOpen` where the `_` is the eventually-differentiable hypothesis. htend : TendstoLocallyUniformlyOn F f atTop dpsiDomain where F : Finset ι → ℂ → ℂ. The `.differentiableOn` lemma: `TendstoLocallyUniformlyOn.differentiableOn (ht : TendstoLocallyUniformlyOn F g l s) (hd : ∀ᶠ n in l, DifferentiableOn ℂ (F n) s) (hs : IsOpen s) : DifferentiableOn ℂ g s` — needsCompleteSpace etc. ℂ ✓.\n\n§5 nontrivialZero_isolated: \nOption A via isDiscrete_riemannZetaZeros: IsDiscrete s def: `IsDiscrete s ↔ sᶜ ∈ codiscreteWithin...`? From DiscreteSubset: `isDiscrete_iff_nhdsNE : IsDiscrete s ↔ ∀ x ∈ s, 𝓝[≠] x ⊓ 𝓟 s = ⊥`? Hmm. There's `IsDiscrete.exists_nhds_...`? Let me instead do the finite-min approach (self-contained, matches the banked patterns):\n\nZ := closedBall ρ₀ 1 ∩ {nontrivial zeros}: finite (the §3 pattern generalized — actually the pattern is on closedBall 0 R; here ball centered ρ₀ radius 1: isCompact_closedBall _ _ works for any center ✓ same code).\nConsider the finite set of subtype elements in Z... I want δ > 0 with all OTHER nontrivial zeros at distance ≥ δ:\n- Let F : Finset of subtype := the finite subtype elements in closedBall ρ₀ 1, minus ρ₀.\n- F finite: from Z.Finite: the subtype elements with val in Z... Hmm, Z := closedBall ∩ {IsNontrivialZero}; Z.Finite as a set of ℂ. The subtype set {ρ : subtype | (ρ:ℂ) ∈ Z} maps bijectively (image + injective — the liSummable pattern) ⟹ finite ⟹ toFinset.\n- For ρ₁ ∈ F: ‖ρ₁ − ρ₀‖ > 0 (ρ₁ ≠ ρ₀ ⟹ val ≠ val (injective) ⟹ norm_sub_pos_iff...).\n- δ := min (1/2) (F.min' of distances / 2)... if F empty: δ = 1/2. Use Finset.inf' or min' with nonempty cases. Cleaner: δ := (F.inf' ... )/2 if nonempty else 1/2... messy. Alternative cleaner: δ := min (1 : ℝ) (F.min'' (image...))/2. Simplest formalization: \n  distances d : Finset ℝ := F.image (fun ρ => ‖ρ.val − ρ₀.val‖); all positive.\n  δ := if h : d.Nonempty then (d.min' h)/2 else 1/2? And min (1/2)? For ρ₁ ∉ closedBall ρ₀ 1: ‖ρ₁ − ρ₀‖ ≥ 1 ≥ δ if δ ≤ 1/2 ✓. For ρ₁ ∈ closedBall, ρ₁ ≠ ρ₀: ρ₁ ∈ F ⟹ its distance ∈ d ≥ min' > 0; δ = min'/2 < min' ≤ dist ✓. And δ ≤ 1/2 ✓ (min'/2 could exceed 1/2 if all distances > 1... but those ρ₁ are ≥... hmm min' over F where F ⊆ closedBall ρ₀ 1: distances ≤ 1! So min' ≤ 1 ⟹ δ ≤ 1/2 ✓ automatically when nonempty. But if F empty δ = 1/2 ✓. Wait is that right: ρ₁ ∈ F ⟹ ‖ρ₁−ρ₀‖ ≤ 1 ⟹ min' ≤ that ≤ 1 ✓ (need F nonempty — d nonempty ✓ same).\n\nActually — simpler: use `isDiscrete_riemannZetaZeros` directly. IsDiscrete s in Mathlib means DiscreteTopology on the subtype, which unfolds (isDiscrete_iff_nhdsNE or similar) to: ∀ x ∈ s, ∃ U ∈ 𝓝 x, U ∩ s = {x}? There should be a lemma. If riemannZetaZeros is discrete and ρ₀ ∈ riemannZetaZeros: ∃ V ∈ 𝓝 ρ₀, V ∩ riemannZetaZeros = {ρ₀}? Then ball inside V. Then nontrivial zeros in the ball ⊆ {ρ₀} ✓ gives isolation with metric ball. That's ~5 lines if the API is nice. Let me grep DiscreteSubset.lean for the right lemma.\n\nEither way works; the finite-min is guaranteed (all pieces banked), IsDiscrete is cleaner if API cooperates. Let me check the API quickly when writing.\n\n§5 seriesFunSub_analyticAt: M-test on ball(ρ₀, δ/2) with the same dominator but R₀' := max 2 (2(‖ρ₀‖+δ/2)):\n- hfu: ∀ᶠ ρ cofinite, ∀ s ∈ ball: ‖seriesTermSub ρ₀ s ρ‖ ≤ u ρ: for ρ in tail: if ρ = ρ₀: 0 ≤ u ρ₀ (u nonneg: (17/6)·M·mult/(1+γ²) ≥ 0 ✓ positivity); else seriesTerm_norm_le as before.\n- partial sums differentiable on the ball: term ρ: if ρ = ρ₀: const 0 ✓; else: s ≠ ρ: s ∈ ball(ρ₀, δ/2), ‖ρ − ρ₀‖ ≥ δ ⟹ ‖s − ρ‖ ≥ δ − δ/2 = δ/2 > 0 ✓; ρ ≠ 0 ✓.\n- limit: fun s => ∑' ρ, seriesTermSub ρ₀ s ρ = seriesFunSub ρ₀ ✓.\n\n§5 seriesFun_sub_term_eq: for s ∈ ball(ρ₀, δ/2):\n- funext: seriesTerm s ρ = seriesTermSub ρ₀ s ρ + (if ρ = ρ₀ then seriesTerm s ρ else 0) — by_cases ρ = ρ₀: then seriesTermSub = 0 and second = term ✓ (0 + x = x); else: term + 0 ✓. ring-ish: `by by_cases h : ρ = ρ₀ <;> simp [seriesTermSub, h]`.\n- Summable (seriesTermSub ρ₀ s): hmm — from the M-test HasSumUniformlyOn on the ball ⟹ pointwise HasSum at s ∈ ball ⟹ Summable: `HasSumUniformlyOn` ⟹ ∀ x ∈ s, HasSum (f · x) (g x)? There's `HasSumUniformlyOn.hasSum` or similar. Check: hasSumUniformlyOn_iff... maybe `HasSumUniformlyOn.tendstoUniformlyOn` then pointwise. Hmm — alternative: prove Summable (seriesTermSub ρ₀ s) directly via comparison with seriesTerm s: ‖seriesTermSub‖ ≤ ‖seriesTerm‖ pointwise (if-zero ≤) ⟹ Summable.of_norm_bounded (seriesSummable s): ‖if ρ = ρ₀ then 0 else t ρ‖ ≤ ‖t ρ‖ ✓ by by_cases simp. That's cleaner and pointwise for ALL s! seriesTermSub_summable : ∀ s, Summable (seriesTermSub ρ₀ s) ✓.\n- singleSupport : Summable (fun ρ => if ρ = ρ₀ then seriesTerm s ρ else 0) := summable_of_hasFiniteSupport (support ⊆ {ρ₀}: Set.Finite.subset (Set.finite_singleton ρ₀) ...) — the liSummable file used `summable_of_hasFiniteSupport` ✓.\n- tsum: ∑' ρ, seriesTerm s ρ = ∑' ρ, (seriesTermSub ρ₀ s ρ + single ρ) = tsum + tsum (Summable.tsum_add? signature: (hg : Summable g) (hh : Summable h) : ∑' (g + h) = ... or `Summable.tsum_add : ∑' x, (g x + h x) = ∑' g + ∑' h`? In this Mathlib: `Summable.tsum_add (hg : Summable g) (hh : Summable h) : ∑' x, (g x + h x) = ...`? Might need `show seriesTerm s = fun ρ => seriesTermSub ρ₀ s ρ + single ρ` funext first.\n- tsum of single: ∑' ρ, if ρ = ρ₀ then seriesTerm s ρ else 0 = seriesTerm s ρ₀: `tsum_eq_single ρ₀ (fun ρ hρ => by simp [hρ])`? `tsum_eq_single (a) (h : ∀ b ≠ a, f b = 0) : ∑' f = f a`? hmm name: `tsum_eq_single`. ✓ I believe exists.\n- Then seriesFun s = seriesFunSub ρ₀ s + seriesTerm s ρ₀ ⟹ seriesFun s − seriesTerm s ρ₀ = seriesFunSub ρ₀ s (sub_eq: a = b + c ⟹ a − c = b: linarith-style: rw, abel/ring).\n\nWait — this equality holds for ALL s (both sides well-defined, summable everywhere) — not just the ball! seriesFun_sub_term_eq : ∀ s, seriesFun s − seriesTerm s ρ₀ = seriesFunSub ρ₀ s. \n\nThen seriesFun_sub_self_term_analyticAt: AnalyticAt ℂ (fun s => seriesFun s − seriesTerm s ρ₀) ρ₀: EventualEq with seriesFunSub ρ₀ (eventually_of_forall via the pointwise eq) ⟹ AnalyticAt.congr: `AnalyticAt.congr (hf : AnalyticAt ℂ f x) (h : f =ᶠ[𝓝 x] g) : AnalyticAt ℂ g x` ✓ exists I believe.\n\nThen the polar form: fun s => seriesFun s − mult/(s−ρ₀): seriesFun s − mult/(s−ρ₀) = (seriesFun s − seriesTerm s ρ₀) + mult/ρ₀ (constant): funext ring with field: seriesTerm s ρ₀ = mult·(1/(s−ρ₀) + 1/ρ₀) = mult/(s−ρ₀) + mult/ρ₀ — needs s − ρ₀ ≠ 0 to split?? mult·(1/(s−ρ₀)+1/ρ₀) = mult/(s−ρ₀) + mult/(ρ₀) via mul_add + mul_div... 1/X form: mult·(1/(s−ρ₀)) = mult/(s−ρ₀): one_div: a·(1/b) = a/b ✓ div_eq_mul_one_div... no field_simp needed: (mult : ℂ)·(1/(s−ρ₀) + 1/ρ₀) = mult/(s−ρ₀) + mult/ρ₀ by ring? ring handles 1/x as x⁻¹: mult·((s−ρ₀)⁻¹ + ρ₀⁻¹) = mult·(s−ρ₀)⁻¹ + mult·ρ₀⁻¹ ring ✓ and a/b = a·b⁻¹ by definition? div_eq_mul_inv: a/b = a*b⁻¹ is a lemma not def... in ℂ, `div_eq_mul_inv` is definitional? HDivision.hDiv = a * b⁻¹ for field — `div_eq_mul_inv` is `@[simp]`-lemma; ring normal forms treat a/b as a*b⁻¹ ✓. So funext s: show (fun s => seriesFun s − mult/(s−ρ₀)) = (fun s => (seriesFun s − seriesTerm s ρ₀) + mult/ρ₀) by funext s; simp [seriesTerm]; ring. Then AnalyticAt.add const ✓.\n\nHmm wait, one more check on `of_norm_le_summable_eventually`'s `hu : Summable u` — u is on the subtype; `WeilEF.zero_sum_inv_sq zetaSeam` is Summable over `(zetaZeros zetaSeam).carrier` — in liSummable they wrote `(WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9/2)*(n:ℝ)^2)` and hbase had type Summable (fun ρ : {ρ // IsNontrivialZero ρ} => ...) — the carrier subtype `{ρ : ℂ // ρ ∈ (zetaZeros zetaSeam).carrier}` vs `{ρ : ℂ // IsNontrivialZero ρ}`: defeq via zetaZeros_carrier (rfl per the simp lemma: `(zetaZeros hs).carrier = {ρ | IsNontrivialZero ρ} := rfl`) — and it typechecked in liSummable ✓. Good.\n\nBUT careful: in zero_sum_inv_sq the summand is `(zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))` — with ρ : carrier subtype coerced. My dominator: (17/6)·M·((zeroMult ρ:ℝ)/(1+normSq(gammaOf ρ))) — write as `(17/6 * M) * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))` and use `.mul_left (17/6 * M)`? mul_left c : Summable (fun ρ => c * f ρ) — then my u = c·(mult/(1+γ²)) ✓.\n\nNow the ball-avoidance §4 — one more subtlety in the NF case: hfh : riemannZeta =ᶠ[𝓝 s₀] fun z => (z − s₀) ^ analyticOrderNatAt riemannZeta s₀ • h z. From Metric.eventually_nhds_iff_ball get ε₂ with ∀ z ∈ ball, ζ z = (z−s₀)^m • h z. h ≠ 0 on ball ε₁. On ball min ε: for z ≠ s₀: (z−s₀)^m ≠ 0, h z ≠ 0 ⟹ ζ z ≠ 0. So zeros of ζ in ball ⊆ {s₀}. A nontrivial zero ρ in the ball: ζ ρ = 0 ⟹ ρ = s₀; but s₀ not nontrivial (hs₀) ⟹ contradiction ✓.\n\nThe zetaA case (s₀ = 1): zetaA_ne_zero_near_one : ∀ᶠ w in 𝓝 1, zetaA w ≠ 0 → ball ε. For ρ nontrivial in ball(1, ε): ρ ≠ 1 (re ρ < 1 = re 1 ⟹ ρ ≠ 1: intro h; rw h at... re ρ < 1, re 1 = 1: `Complex.one_re`; if ρ = 1 then re ρ = 1 contradiction ✓); zetaA ρ = (ρ−1)·ζ ρ = (ρ−1)·0 = 0 — contradicts zetaA ρ ≠ 0 ✓. Use zetaA_apply (hρ1 : ρ ≠ 1).\n\nNow, file header comment per convention. Also the root NguyenRH1.lean import + comment update.\n\nEstimated: ~450–550 lines. Time to write. Let me also double-check a few lemma names by grepping Mathlib:\n- `Set.Finite.compl_mem_cofinite` or mem_cofinite.\n- `tsum_eq_single`.\n- `Metric.eventually_nhds_iff_ball`.\n- `AnalyticAt.congr`.\n- `IsCompact.inter_riemannZetaZeros_finite` ✓ (have).\n- `Complex.norm_natCast` ✓ (used in LiDisc: `Complex.norm_natCast` — saw \"RCLike.norm_natCast\" in LiSkeleton line 251; LiDisc line ~204 `Complex.norm_natCast`. Both exist presumably.)\n\nLet me grep for these four quickly.","signature":""},{"type":"text","text":"All infrastructure confirmed. Let me verify a few Mathlib lemma names before writing."},{"type":"tool_use","id":"Bash_31","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem tsum_eq_single\\b\\|lemma tsum_eq_single\\b\" Mathlib/Topology/Algebra/InfiniteSum/Basic.lean | head -3; grep -rn \"compl_mem_cofinite\\|theorem mem_cofinite\\b\" Mathlib/Order/Filter/Cofinite.lean Mathlib/Topology/ 2>/dev/null -r | head -5; grep -rn \"eventually_nhds_iff_ball\" Mathlib/Topology/MetricSpace/*.lean Mathlib/Topology/MetricSpace/**/*.lean 2>/dev/null | head -3; grep -rn \"theorem AnalyticAt.congr\\b\\|protected theorem AnalyticAt.congr\" Mathlib/Analysis/Analytic/*.lean | head -3; grep -rn \"theorem summable_of_hasFiniteSupport\\|lemma summable_of_hasFiniteSupport\" Mathlib/ -r | head -3; grep -rn \"tendstoUniformlyOn_tsum_of_cofinite_eventually\" Mathlib/ -r | head -2","description":"Verify Mathlib lemma names for LiSeries"},"extra_content":null}]