Session 028 — 2026-08-23 — ii′-5e-iii COMPLETE: the zero series (LiSeries.lean)

Directive

Continue tier ii′-5 per STATE.md: ii′-5e-iii (D-068 §3) — the zero-side partial-fraction series: summability, analyticity off the zeros, isolation at each zero. User: "let continue with the next stage."

Outcome: 5e-iii COMPLETE (LiSeries.lean, ~600 lines, 22 decls, all

audited clean: 3 standard axioms only; full build GREEN 8765 jobs, LiSeries root-imported)

§0–2 (summability): seriesTerm s ρ := (zeroMult ρ : ℂ)·(1/(s−ρ) + 1/ρ) over the nontrivial-zero subtype; seriesFun s := ∑' ρ, seriesTerm s ρ. The tail algebra one_div_sub_add_one_div (1/(s−ρ)+1/ρ = s/(ρ(s−ρ))) gives ‖term‖ ≤ 2‖s‖/‖ρ‖² for 2 ≤ ‖ρ‖, 2‖s‖ ≤ ‖ρ‖; the comparison one_add_normSq_gammaOf_le (1 + ‖γ_ρ‖² ≤ (17/12)‖ρ‖² for ‖ρ‖ ≥ 2: ‖γ‖² = im² + (1/2−re)² ≤ im² + 1/4 and im² ≥ 3) converts to the ii′-1a dominator (17/6)(‖s‖+1)·mult/(1+‖γ‖²), summable by Zeta23 WeilEF.zero_sum_inv_sq zetaSeam; the head is finite (finite_subtype_norm_lt, the liSummable compact-finiteness pattern). seriesSummable : ∀ s, Summable (seriesTerm s) — UNCONDITIONAL (the junk value at s = ρ is harmless), cloned from the liSummable D-trick.

§3–4 (analyticity off the zeros): exists_ball_avoid_nontrivialZeros — around any s₀ with ¬IsNontrivialZero s₀ a ball avoiding the nontrivial zeros, by the three-case split: ζ s₀ ≠ 0 → continuity ball (analyticAt_riemannZeta.continuousAt.eventually_ne); ζ s₀ = 0, s₀ ≠ 1 → the order normal form (analyticOrderAt_ne_top.mp of zeta_order_ne_top_of_ne: ζ = (z−s₀)^m·h, h ≠ 0 nearby ⟹ the only possible zero in the ball is s₀ itself, excluded by hypothesis); s₀ = 1 → the zetaA factorization (zetaA_ne_zero_near_one + zetaA_apply: ζ = zetaA/(w−1) ≠ 0 off 1 in a ball; ρ ≠ 1 since re ρ < 1). Then seriesFun_analyticAt/seriesFun_analyticOnNhd: the Weierstrass M-test HasSumUniformlyOn.of_norm_le_summable_eventually on the avoiding ball (cofinite = complement of the finite head via eventually_cofinite; the (17/6)M·mult/(1+‖γ‖²) majorant) → TendstoLocallyUniformlyOn.differentiableOn (finite partial sums differentiable termwise) → .analyticOnNhd Metric.isOpen_ball → apply at the center — the journal-020/021-banked pattern verbatim.

§5 (isolation + the reduced series): nontrivialZero_isolated — ∃ δ > 0, all OTHER nontrivial zeros at distance ≥ δ (the finite unit-ball subtype finset, the min-distance halved; empty case δ = 1/2). seriesTermSub ρ₀ (the ρ₀-term zeroed) / seriesFunSub ρ₀: summable everywhere (norm ≤ ‖seriesTerm‖), analytic AT ρ₀ (seriesFunSub_analyticAt — the same M-test on the isolation half-ball; the zeroed term is the constant 0, the others are pole-free by the isolation). Pointwise split seriesFun_eq_sub_add (tsum_congr + Summable.tsum_add + tsum_eq_single) ⟹ seriesFun_sub_term: seriesFun s − seriesTerm s ρ₀ = seriesFunSub ρ₀ s EVERYWHERE. Capstones: seriesFun_sub_self_term_analyticAt (AnalyticAt.congr) and seriesFun_sub_polar_analyticAt — s ↦ seriesFun s − mult(ρ₀)/(s−ρ₀) analytic at ρ₀ (the +mult/ρ₀ part is a constant) — exactly the residue-cancellation input 5e-iv needs at the nontrivial zeros.

Banked gotchas (session 028 additions)

• rw [heq] leaves a beta-redex RHS: after rewriting with an EventuallyEq-style fact (fun z => ... • h z) ↑ρ, the • is hidden under the unreduced application — rw [smul_eq_mul] fails. Fix: show (↑ρ − s₀)^m * h ↑ρ ≠ 0 (defeq via beta + smul=mul on ℂ).
• rw [not_lt] at h fails on ρ ∉ {x | p x} (setOf-membership is folded): insert show p ρ-form for the goal or restructure; the membership itself IS defeq to the predicate, so apply hρ on hρ : ρ ∈ {x | ¬ P x} turns the goal into P directly.
• Finset.image lambdas need the bound var's TYPE pinned when the body coerces: fun ρ : {ρ // P ρ} => ‖(ρ:ℂ) − ρ₀‖ — otherwise the elaborator types the lambda at ℂ (identity coe) and the Finset argument mismatches.
• NEVER rw [hd] at a hypothesis whose type depends on the set-var (e.g. Finset.min'_mem d hdne — hdne : d.Nonempty makes the motive ill-typed). Route: a standalone membership iff hdm (rw [hd] in the GOAL only — no dependent hypotheses there) + .mp/.mpr everywhere.
• obtain ⟨..., rfl⟩ fails when the equation's other side is not a local variable (e.g. ‖…‖ = d.min' hdne): name it (heq) and rw [← heq].
• rw [if_pos h]/if_neg cannot rewrite under a binder (inside fun s => if ...): use simp only [if_pos h] (simp goes under).
• Set.mem_setOf_eq is DEPRECATED (→ Set.mem_ofPred_eq); setOf membership is defeq anyway — prefer defeq ascriptions.
• push_neg is DEPRECATED in this Mathlib: use rw [not_le] etc.
• File-ending convention: end NguyenRH1 THEN end (the noncomputable section wraps the namespace).
• rw [hsingle]-then-goal-open when the residual equality is defeq-only (tsum vs the seriesFunSub def): close with an explicit rfl (rw's auto-rfl won't unfold plain defs).
• AnalyticOnNhd f s is literally ∀ x ∈ s, AnalyticAt f x — apply the AnalyticOnNhd hypothesis at the center with Metric.mem_ball_self.
• simp only [Finset.mem_image, Set.Finite.mem_toFinset] can close an iff goal entirely (rfl-closure) — a following constructor bullet then errors "no goals"; drop it.
• Summable.of_norm_bounded needs a REAL-valued dominator: for ℂ-valued f use (hf).norm (Summable.norm) as the comparison input.

Status / next

ii′-5e-iii COMPLETE. Next: ii′-5e-iv (D-068 §4): F entire by principal-part splits — at nontrivial zeros via ii′-1b's logDeriv-NF + seriesFun_sub_polar_analyticAt (this session) + the elementary terms analytic there (re ρ ∈ (0,1) avoids 0, 1, −2n); at s = 1 via ii′-1b's zetaA logDeriv (logDeriv zetaA analytic at 1, zetaA 1 = 1); at s = 0 via the digamma-series split (−½ψ(s/2) = 1/s − ½h₀(s), h₀ analytic — the Weierstrass machinery of this session applies to the digamma series terms, |term| ≤ C/(n+1)² on ‖w‖ ≤ 1/2); at s = −2n via ii′-1b NF + zeroMult_neg_two_mul (session 026) + the ψ-pole split (the j = n−1 term). Then 5e-v (the circle bound O((log R)³) + max-modulus squeeze ⟹ F ≡ const; capstone ∃ B identity) → ii′-5f → ii′-3b → ii′-3c → ii′-6 → ii′-7.