[{"type":"thinking","thinking":"The user wants to continue: ii′-5e-iv (F entire by principal-part splits, D-068 §4). Let me start by reviewing what I need.\n\nFrom D-068 §4, F entire via principal-part splits:\n- F := logDeriv ζ − [seriesFun − 1/s − 1/(s−1) + (log π)/2 − ½ψ(s/2)]... wait, actually F := LHS − RHS where RHS = B + series − 1/s − 1/(s−1) + ½log π − ½ψ(s/2). But B is existential — so really we define F := logDeriv ζ − seriesFun + 1/s + 1/(s−1) − ½log π + ½ψ(s/2) (without B), prove F entire, bound on circles, then F ≡ const =: B.\n\nHmm wait, let me recheck D-068 §0:\nζ′/ζ(s) = B + Σ_ρ m_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2)\n\nSo F := ζ′/ζ − seriesFun + 1/s + 1/(s−1) − ½log π + ½ψ(s/2). Excluded points: nontrivial zeros (poles of both ζ′/ζ and series), 0 (1/s pole and ψ(s/2) pole ~ −2/s·(−1/2)... wait ψ(w) ~ −1/w at w=0 so ½ψ(s/2) ~ ½·(−2/s) = −1/s; so +1/s + ½ψ(s/2) ~ 1/s − 1/s = 0 cancellation ✓), 1 (pole of ζ′/ζ: residue −1; +1/(s−1) has residue +1 ✓), −2n (ζ′/ζ residue +1; ½ψ(s/2) at s=−2n: ψ(w) at w=−n has residue −1, w = s/2 so ½ψ(s/2) residue ½·(−1)·2 = −1 ✓ cancels).\n\n5e-iv goal: F is entire (analytic everywhere), where analyticity at each excluded point comes from the splits. Formally in Lean, the cleanest statement: for every s₀ : ℂ, AnalyticAt ℂ F s₀. Case split on whether s₀ is in the excluded set.\n\nThis is a substantial build. Let me plan the Lean file LiFEntire.lean (or similar).\n\nFirst, what do I need to check/have:\n1. The definition: `Ffun5e s := logDeriv riemannZeta s - seriesFun s + 1/s + 1/(s-1) - (Real.log π)/2 + (digamma (s/2))/2`.\n\nWait, careful with signs: F = ζ′/ζ − series + 1/s + 1/(s−1) − ½logπ + ½ψ(s/2). Let me double check the residue at 0: ψ(w) = −γ − 1/w + O(w) near w=0 (digamma has simple pole residue −1 at 0: ψ(w) = −1/w − γ + ...). So ½ψ(s/2) = ½(−2/s − γ + ...) = −1/s − γ/2 + .... Then +1/s + ½ψ(s/2) = 1/s − 1/s − γ/2 = −γ/2 + O(s) ✓ analytic at 0 after cancellation. And ζ′/ζ at 0: ζ(0) = −1/2 ≠ 0 so analytic ✓. And −1/(s−1) at 0 is analytic ✓. Series at 0: seriesFun 0 = 0 and analytic (0 is not a nontrivial zero ✓ by 5e-iii). So F analytic at 0 ✓.\n\nAt s = 1: ζ′/ζ has pole residue −1 (ζ has simple pole residue +1 ⟹ logDeriv has simple pole residue −1): ζ′/ζ + 1/(s−1) = logDeriv zetaA analytic at 1 (ii′-1b). F = [ζ′/ζ + 1/(s−1)] − series + 1/s − ½logπ + ½ψ(s/2) — all other pieces analytic at 1 ✓ (series: 1 not a nontrivial zero ✓ re = 1; ψ(1/2) fine).\n\nAt s = −2n: ζ′/ζ = 1/(s+2n) + analytic (simple zero); ½ψ(s/2) = −1/(s+2n) + analytic (ψ(w)+1/(w+n) analytic at w = −n). So ζ′/ζ + ½ψ(s/2) analytic at −2n. Other pieces analytic (series ✓ since −2n not nontrivial (re < 0); 1/s, 1/(s−1) fine).\n\nAt nontrivial ρ₀: ζ′/ζ − m/(s−ρ₀) analytic (NF); series − m/(s−ρ₀) analytic (5e-iii); so ζ′/ζ − series = [ζ′/ζ − m/(s−ρ₀)] − [series − m/(s−ρ₀)] analytic; elems analytic at ρ₀ since re ∈ (0,1) avoids 0,1,−2n ✓.\n\nElsewhere: s not a zero of ζ... wait — F involves logDeriv ζ = ζ′/ζ which needs ζ s ≠ 0 AND s ≠ 1 for analyticity. Generic s: s ∉ {nontrivial zeros} ∪ {trivial zeros} ∪ {1}: ζ s ≠ 0 and s ≠ 1 ⟹ logDeriv ζ analytic (analyticAt_riemannZeta + deriv + div). Series analytic (s not nontrivial zero ✓). 1/s: s ≠ 0 — 0 is a... wait 0 is in the excluded set? ζ(0) ≠ 0 so 0 is \"generic\" except 1/s blows. 0 ∈ {−2n}? No, −2n for n ≥ 1 starts at −2. So 0 needs its own split (the 1/s vs ψ cancellation). Similarly the generic case needs s ≠ 0 for the 1/s term and s/2 ∉ −ℕ... wait ψ(s/2) analytic requires s/2 ∉ {0, −1, −2, ...} i.e. s ∉ {0, −2, −4, ...} — the non-positive even integers. For s = −2n+... odd negative integers −1, −3, ...: ψ(s/2) = ψ(−1/2) etc fine (poles of ψ at nonpositive INTEGERS; s/2 = −1/2 fine ✓).\n\nSo the excluded set: {nontrivial zeros} ∪ {0} ∪ {1} ∪ {−2n : n ≥ 1}. Generic point: s ∉ that set ⟹ every piece analytic:\n- logDeriv ζ: ζ s ≠ 0 needed. s ∉ nontrivial zeros and s ∉ trivial zeros {−2n} and s ≠ 1: but ζ could have OTHER zeros? No — zeros of ζ = trivial ∪ nontrivial ∪ ... that's all (Mathlib's riemannZetaZeros is the preimage — we don't know a priori that zeros are only those, but it doesn't matter: for the generic case I need ζ s ≠ 0 — hmm, if s ∉ {nontrivial} ∪ {−2n}, is ζ s ≠ 0? A zero that's neither nontrivial nor trivial would violate... the classification: ζ s = 0 ⟹ s nontrivial (0 < re < 1) or s ∈ {−2n} or s = 1-junk (no, ζ(1)≠0 in Mathlib per riemannZeta_one_ne_zero). Do we HAVE the classification \"ζ s = 0 ⟹ nontrivial or trivial\" available? From LiDisc's zeroDisc_isNontrivial reasoning: re ≥ 1 nonvanishing (Mathlib one_le_re), re ≤ 0 ⟹ s = −2n (ΓR-pole/FE). Was that packaged as a standalone lemma? LiDisc `zeroDisc_isNontrivial` — scoped to the disc. Hmm. For 5e-iv I need the global classification: ζ s = 0 ∧ s ≠ 1 ⟹ IsNontrivialZero s ∨ ∃ n ≥ 1, s = −2n.\n\nWait — is that needed? Generic case: s ∉ excluded set. I claim ζ s ≠ 0. Suppose ζ s = 0: then by the classification s is nontrivial (excluded ✓ contradiction) or s = −2n (excluded ✓) — so I need the classification lemma: `riemannZeta_eq_zero_iff`: riemannZeta s = 0 → s ≠ 1 → IsNontrivialZero s ∨ ∃ n : ℕ, 1 ≤ n ∧ s = −2*n. Build it: re > 1? No wait: cases on re s: re ≥ 1: nonvanishing (Mathlib riemannZeta_ne_zero_of_one_le_re needs s ≠ 1? name: `riemannZeta_ne_zero_of_one_le_re : 1 ≤ s.re → s ≠ 1 → ζ s ≠ 0`? something like that — LiDisc used it). 0 < re < 1: nontrivial ✓ by def. re ≤ 0: the ΓR/FE argument: Λ(s) = ΓR(s)ζ(s) entire-ish: ζ(s) = 0 ⟹ Λ(s) = 0 = Λ(1−s) = ΓR(1−s)ζ(1−s); re(1−s) ≥ 1, 1−s ≠ 1 (s ≠ 0 — if s = 0: ζ(0) = −1/2 ≠ 0 so s ≠ 0 anyway) ⟹ ζ(1−s) ≠ 0; ΓR(1−s) ≠ 0 (Gammaℝ nonzero everywhere? Gammaℝ(s) = π^(−s/2)Γ(s/2): Γ never 0, π^... never 0 ⟹ Gammaℝ never 0 — Mathlib: `Complex.Gammaℝ_eq_zero_iff`? session 026 banked: \"Gammaℝ_eq_zero_iff gives −(2*↑m)\" — hmm that's Gammaℝ_eq_zero_iff saying Gammaℝ s = 0 ↔ ∃ m, s = −2m?? But Γ never vanishes... Gammaℝ s = π^(−s/2)·Γ(s/2): Γ(s/2) is never 0 (Mathlib `Complex.Gamma_ne_zero`? Gamma_ne_zero_of... for ℂ: Gamma s ≠ 0 for all s? Gamma has no zeros — Mathlib `Complex.Gamma_ne_zero`?). The session-026 gotcha said \"Gammaℝ_eq_zero_iff gives −(2*↑m)\" — hmm, that suggests Gammaℝ_eq_zero_iff : Gammaℝ s = 0 ↔ ∃ m:ℕ, s = −(2*m)?? That can't be right for the actual Gamma... unless Mathlib's Gammaℝ is defined as π^(−s/2)·Γ(s/2)/... no wait. Actually Mathlib's Gammaℝ := π^(-s/2) * Gamma(s/2)? and Gamma is defined as 1/Gamma⁻¹... In Mathlib, Complex.Gamma is the meromorphic Gamma with zeros at nonpositive integers?? NO — Mathlib's Complex.Gamma is defined such that Gamma(s) = 0 at s = 0, −1, −2, ... (junk values at poles are 0!). Yes — Mathlib's Gamma has value 0 at the poles (they use the entire 1/Γ... hmm). Let me check what LiTrivialZeros did — it has the cofactor HfunT handling exactly this. The point: in Mathlib, Gammaℝ(s) = 0 ↔ s ∈ {−2n : n ≥ 0... or n : ℕ} (junk zeros at the poles). So the FE argument: ζ s = 0, re ≤ 0 ⟹ Λ s = ΓR s · ζ s = 0; Λ(1−s) = Λ(s) = 0 = ΓR(1−s)ζ(1−s); re(1−s) ≥ 1: ζ(1−s) ≠ 0 (needs 1−s ≠ 1 i.e. s ≠ 0 — and s = 0 handled by ζ(0) ≠ 0) and ΓR(1−s): re(1−s) ≥ 1 > 0 ⟹ 1−s ∉ {−2m} ⟹ ΓR(1−s) ≠ 0 — contradiction ⟹ ... wait that gives NO zeros with re ≤ 0 except... but trivial zeros DO exist with re ≤ 0! The flaw: Λ(s) = ΓR(s)ζ(s) — if ΓR(s) has a POLE at s = −2n (junk value 0?) and ζ(s) = 0 — the product Λ is entire: at s = −2n, ΓR junk-0 times ζ... the identity Λ(s) = ΓR(s)·ζ(s) holds only where both sides are defined properly — as functions with junk values, Λ(s) = ΓR(s)ζ(s) as a Mathlib equation holds everywhere (Λ is defined via... `completedRiemannZeta`? The relation `completedRiemannZeta s = Gammaℝ s * riemannZeta s` — Mathlib `completedRiemannZeta_def`? holds for all s as functions (with junk)). So ζ s = 0 ⟹ Λ s = ΓR s · 0 = 0 ✓ fine. Λ(1−s) = Λ(s) (Mathlib `completedRiemannZeta_one_sub` ✓). So ΓR(1−s)ζ(1−s) = 0 with both factors ≠ 0 for re s ≤ 0, s ≠ 0, s ≠ −2n... contradiction ⟹ no such zeros — BUT s = −2n ARE zeros! Where does the argument break at s = −2n? ΓR(1−s) = ΓR(1+2n) ≠ 0 ✓, ζ(1−s) = ζ(1+2n) ≠ 0 ✓ (re > 1) ⟹ Λ(1−s) ≠ 0 ⟹ Λ(s) ≠ 0. But Λ(−2n) = ΓR(−2n)·ζ(−2n) = 0·0 = 0 as junk product — the issue: the \"identity\" Λ = ΓR·ζ as junk-valued functions: at s = −2n, ΓR(−2n) = 0 (junk) and ζ(−2n) = 0 (true zero), product 0 = Λ(−2n) — but the TRUE Λ(−2n) is nonzero (Λ entire nonvanishing there since Λ(1+2n) ≠ 0). So the Mathlib function equation Λ = ΓR·ζ must FAIL at s = −2n as junk values — i.e., Mathlib's `completedRiemannZeta s = Gammaℝ s * riemannZeta s` is NOT valid at the poles of Gammaℝ as a pointwise identity... In fact Mathlib has `completedRiemannZeta s = Gammaℝ s * riemannZeta s` only for s ∉ {−2n}? Something like `riemannZeta_def` or the relation holds where Gammaℝ ≠ 0. Right — the correct statement: for s with Gammaℝ s ≠ 0: ζ s = Λ s / ΓR s. The zero classification: ζ s = 0, re s ≤ 0: if ΓR s ≠ 0 (s ∉ {−2m}) then Λ s = 0 (via the valid product identity... which needs care at poles), then Λ(1−s) = 0, factor ⟹ contra. So ζ s = 0 ∧ re ≤ 0 ⟹ s ∈ {−2m} (m ≥ 0); s = 0: m = 0: ζ(0) = −1/2 ≠ 0 excludes ⟹ m ≥ 1 ⟹ s = −2n, n ≥ 1 ✓.\n\nThis classification lemma may essentially exist in LiTrivialZeros/LiDisc machinery. zeroDisc_isNontrivial (LiDisc): zeros in the disc with re bounds... let me look at what it proves exactly and whether a global version is easy. Actually — hmm, for 5e-iv, do I really need the full classification? The generic-case analyticity of logDeriv ζ at s requires ζ s ≠ 0. The excluded set in the capstone is {nontrivial} ∪ {0,1} ∪ {−2n}. For F to be ENTIRE I need analyticity at every other point, which requires ζ s ≠ 0 there. If there were an exotic zero ρ* (neither nontrivial nor trivial — but there are none mathematically) F would have a pole there. Since mathematically there are none, I need the classification lemma. It's a real (small) build: ~50–100 lines with the FE + Gammaℝ_eq_zero_iff + nonvanishing.\n\nWait — maybe Zeta23 or Mathlib already has it? Mathlib: `riemannZeta_zeros_...`? Hmm. There's the set `riemannZetaZeros` = full preimage. LiDisc's zeroDisc_isNontrivial: let me look at its statement — \"re ≥ 1 via Mathlib's one_le_re nonvanishing; re ≤ 0 via ΓR-pole/FE\" — inside a disc context. Let me read it and see if the argument is cleanly separable.\n\nActually — for 5e-iv there's a cleaner path avoiding the classification ENTIRELY: don't prove \"F analytic at each generic point\" via case exclusion; instead prove F analytic on the complement of the excluded set E = {nontrivial} ∪ {0,1} ∪ {−2n}... no wait, that still needs ζ ≠ 0 on the complement.\n\nAlternatively use the classification but only as: riemannZeta s = 0 → IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n ≥ 1, s = −2n. Hmm but ζ(0) ≠ 0 and ζ(1) ≠ 0 so those two clauses are vacuous — fine to include for a smoother statement.\n\nLet me look at LiDisc.zeroDisc_isNontrivial to see how much is reusable.\n\nActually, let me reconsider the overall structure of 5e-iv. The target per D-068:\n\nF entire where F := logDeriv ζ − seriesFun + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2.\n\nHmm wait — actually, do we even need F defined with logDeriv at the bad points? logDeriv ζ s = ζ′ s / ζ s — at zeros it's junk (x/0 = 0). F as a function is defined everywhere with junk values at the excluded set; \"F entire\" = AnalyticAt at every point — at the excluded points the analytic function's value is whatever the junk is, but AnalyticAt at ρ₀ means F agrees near ρ₀ (including AT ρ₀) with an analytic function — the junk value at exactly ρ₀ matters! AnalyticAt ℂ F ρ₀ requires F =ᶠ[𝓝 ρ₀] (analytic g) — including the point ρ₀ itself. Our splits show F = g on a PUNCTURED neighborhood; at ρ₀, F ρ₀ is junk (logDeriv = 0/0-form junk + series junk...). Need to also fix the VALUE: AnalyticAt.congr needs full EventuallyEq including the point. Standard trick: show F is continuous at ρ₀... no — simpler: the punctured agreement + boundedness ⟹ the value must match? Not automatic for junk. Hmm — actually there's a cleaner formalization: define F via the pieces but PROVE AnalyticAt at ρ₀ by showing F equals (on the full neighborhood) a function built from analytic pieces where the piecewise analytic function at ρ₀ is DEFINED by the analytic parts... The clean approach used by LiSides for the removable singularity at 1: \"Removable singularity at 1 via Taylor-remainder order ≥ n+1 (Ffun−TaylP)\" — they showed R extends continuously across 1. For analyticity they presumably used: punctured equality + continuity ⟹ full equality? No — for AnalyticAt they need agreement everywhere INCLUDING the point.\n\nHmm — wait, how does one normally prove \"F analytic at ρ₀\" when F is defined by an expression that's junk at ρ₀? The standard Lean route: AnalyticAt.congr with an EventualEq on the FULL neighborhood — so I must ensure the value at ρ₀ matches too. If g is analytic at ρ₀ and F = g punctured, and F is CONTINUOUS at ρ₀, then F ρ₀ = g ρ₀ (both are limits along the punctured filter: g continuous, F continuous, agree punctured ⟹ equal at the point — `eq_of_tendsto`... something like: F ρ₀ = lim F(punctured) = lim g(punctured) = g ρ₀). So need: F continuous at ρ₀ + F = g punctured + g analytic ⟹ F =ᶠ[𝓝] g (for y ≠ ρ₀ punctured ✓; y = ρ₀: the continuity argument) ⟹ AnalyticAt.congr. Continuity of F at ρ₀: from the split F = A − B punctured where A, B analytic (continuous) at ρ₀: F = A − B punctured with A−B continuous ⟹ F has a limit... continuity of F at ρ₀ means F y → F ρ₀ — junk F ρ₀ breaks it. Circular-ish. Alternative: REDEFINE F at the bad points! Since the bad set is discrete, define F properly: F := fun s => if s ∈ badset then (limit value) else (expression). Ugh.\n\nCleaner Mathlib-idiomatic approach: there might be a lemma \"analytic on punctured neighborhood + continuous ⟹ analytic at the point\"? Hmm, actually the real theorem: bounded near the point + analytic on punctured nhd ⟹ extends. Mathlib's removability: `Complex.analyticAt_of_...`? There IS `AnalyticOnNhd.removable...`? Hmm, I don't remember a general removable-singularity theorem in Mathlib (D-068 says \"Mathlib lacks it in general form\" — that was the motivation for the principal-part splits!). But the splits as designed AVOID removability by writing F as a difference of pointwise-analytic functions — i.e., the key claim at each bad point is:\n\nF =ᶠ[𝓝 ρ₀] (analytic expression)  — FULL neighborhood, not punctured!\n\nbecause each piece of F is defined as an analytic function WITH its correct value at ρ₀. E.g. at ρ₀: F = [logDeriv ζ − m/(s−ρ₀)] − [seriesFun − m/(s−ρ₀)] − [elems] — this equality holds POINTWISE for all s ≠ ρ₀ (both sides same expression); AT s = ρ₀: LHS is junk, RHS is A(ρ₀) − B(ρ₀) − elems(ρ₀) — some specific complex number. So the equality at the point fails in general (junk ≠ value). UNLESS the junk happens to match — it doesn't necessarily.\n\nHmm. So how did the design intend to handle the point value? D-068 §4 says \"write F as a difference of pointwise-analytic functions\" — the equality F = A − B holds pointwise EXCEPT at the center. For AnalyticAt we need the eventual equality on a full neighborhood.\n\nOption: prove F is continuous at the center separately, then patch the value: F(ρ₀) must equal (A−B)(ρ₀) by continuity from punctured values... but F's continuity at ρ₀ is itself the issue.\n\nAlternative clean route: redefine the capstone function not as `logDeriv ζ − ...` but as the analytic extension directly, and state the capstone identity only at good points (which is all 5f needs). I.e.:\n\nDefine F : ℂ → ℂ by cases isn't needed — instead define the ENTIRE function abstractly: prove `∃ G : ℂ → ℂ, (AnalyticOnNhd ℂ G univ... wait AnalyticAt everywhere) ∧ ∀ s (good), G s = logDeriv ζ s − seriesFun s + ...`. Then G is the entire function; the circle bound applies to G (circles avoid bad points); Liouville squeeze ⟹ G ≡ const; capstone: at good s, logDeriv ζ s = B + seriesFun s − ... where B := G's constant value adjusted. The existential packaging avoids ALL point-value issues!\n\nHow to get ∃ G entire agreeing with the expression at good points? At each bad point ρ₀, the analytic difference A − B (with correct value at ρ₀) agrees with the expression punctured. Standard gluing: G := expression at good points, G(ρ₀) := (A−B)(ρ₀) at bad points — but that's a piecewise definition... In Lean: G s := if s ∈ badSet then limValue else expr s — messy but the bad set is discrete... Alternatively use the identity theorem glue: the expression is analytic on the dense open connected set U = complement of bad points... \n\nHmm wait — actually there's a MUCH cleaner standard trick: F_expr is analytic on U (punctured at bad points). At each bad point, F_expr is continuous-extendible (bounded near the point — from the split: punctured = A − B bounded). The extended function G (defined at bad points by the limit) is continuous everywhere and analytic on U. Then: continuous + analytic on U where U = complement of a discrete set ⟹ analytic everywhere? That's the removable singularity theorem again (continuous version) — which Mathlib lacks per D-068.\n\nHmm OK so how do we actually get entire G in Lean without removability? Direct definition by cases on the bad set! The bad set E := {nontrivial zeros} ∪ {0, 1} ∪ {−2n} is discrete & countable-ish. Define:\n\nG s := if h : IsNontrivialZero s then (localAnalyticValue) else if s = 0 then ... — painful because the \"value\" at each bad point is the limit of the expression, which must be shown to exist.\n\nALTERNATIVELY — define G via the NF-based analytic pieces directly, globally:\n\nG := logDerivCorrection ζ − seriesFunCorrected + ... where each \"corrected\" piece is a globally-defined analytic function minus explicit poles... The classical statement: F is entire — the cleanest Lean formulation might be:\n\nG s := logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (log π)/2 + digamma(s/2)/2 − [junk corrections]... no.\n\nHmm, let me think about what's actually the minimal thing 5e-v needs:\n1. An entire function G.\n2. G agrees with the explicit expression at all good points (s ∉ E).\n3. |G| ≤ C(log R)³ on the 5e-i circles (circles consist of good points — need: circle |s| = R_k avoids E: nontrivial zeros off the circle by the γ-gap ✓; −2n: R/2 dist to ℤ ≥ 1/4 ⟹ circle avoids −2n? |s| = R, s = −2n ⟹ R = 2n exactly: dist(R/2, ℤ) ≥ 1/4 ⟹ R/2 not integer... 2n = R ⟹ R/2 = n integer — excluded ✓; s = 0, 1 not on circle (R ≥ 4) ✓).\n4. The squeeze: (G(z) − G(0))/z entire-ish, |·| ≤ C(log R)³/R → 0 on the circles ⟹ G ≡ G(0) by max-modulus on the discs.\n\nFor (1)+(2), the cleanest: prove `AnalyticOnNhd ℂ Gexpr {s | s ∉ E}` (the expression analytic off E) AND at each point of E produce AnalyticAt of a LOCALLY-EQUAL function... then G := Gexpr outside E, G := local value on E. The piecewise G: analyticity at good s: G =ᶠ Gexpr near s (E discrete ⟹ ball avoiding E... wait E not closed — nontrivial zeros discrete, fine, each good point has a ball avoiding E? E = {nontrivial} ∪ {0,1} ∪ {−2n}: all components discrete; union discrete? The −2n accumulate only at ∞; the nontrivial zeros discrete; so E is discrete ⟹ every point has a ball meeting E in at most itself ✓ (need: E locally finite — zeros closed discrete {0,1,−2n} finite sets... yes).\n\nAt bad points ρ₀: G agrees punctured with A−B (analytic) and G(ρ₀) = (A−B)(ρ₀) BY DEFINITION if I define G via the local analytic functions at bad points... The piecewise definition in Lean:\n\nG : ℂ → ℂ := fun s => if IsNontrivialZero s then V_zero s else if s = 0 then V_0 else if s = 1 then V_1 else if (∃ n ≥ 1, s = −2n) then V_triv s else Gexpr s\n\nwhere V_zero s := the value of the local analytic difference at s — but the local analytic difference is only constructed near each ρ₀ (its definition involves the NF choice h)... The value at the center is determined (the limit), but writing it requires choice. This is getting ugly.\n\nBETTER: the whole point-value problem dissolves if instead of \"F = expression\" I package the conclusion differently. Observe: at each bad point ρ₀, what I actually prove is: ∃ function A analytic at ρ₀ with A =ᶠ[𝓝[≠] ρ₀] F_expr (punctured agreement, where F_expr is analytic on U). Standard consequence needed by 5e-v: F_expr is BOUNDED on each circle (the circle avoids E — bound the expression directly via the pieces, no G needed!); and the IDENTITY to conclude is only at good points. The squeeze: G(z) := (F(z)−F(0))/z... needs F entire.\n\nHmm, but here's the thing — the ENTIRETY of F is used in 5e-v ONLY for: (a) the max-modulus principle on discs |z| ≤ R_k applied to G(z) = (F(z)−F(0))/z; (b) hence F ≡ F(0); (c) evaluate the identity at good s. \n\nWhat if F is only meromorphic with the disk... no, the squeeze needs analyticity inside the discs (the discs CONTAIN bad points — poles would break max-modulus).\n\nOK here's the cleanest genuine resolution, the one the classical proof uses and D-068 gestures at: F is ENTIRE as a function because at each bad point the local expression defines the value continuously. In Lean, the standard tool for \"defined by one expression on a dense set, extends continuously, extension analytic\": I recall Mathlib DOES have some removability now? D-068 says \"Mathlib lacks it in general form\" (session 026 survey). Let me verify — search Mathlib for \"removable\" / analyticAt_of_...: there's `Complex.analyticAt_of_differentiable_on_punctured_nhds`? Hmm — actually I recall `DifferentiableOn.analyticAt_of_...`? Let me search for punctured + analytic lemmas in this Mathlib checkout. There's `RiemannRemovableSingularities`?? Mathlib has the Riemann removable singularity theorem for the complex plane? I believe there IS something: `Mathlib/Analysis/Complex/RemovableSingularity.lean`?? Hmm — not sure. Let me check! If Mathlib has: differentiableOn ℂ f (ball \\ {c}) + continuous/bounded ⟹ analyticAt — then 5e-iv becomes much simpler: F differentiable off E (analytic off E ✓), continuous/bounded near each bad point (from the splits — the split gives punctured equality with A−B which is continuous ⟹ F bounded near the point... but differentiability AT the point for the extension...). \n\nActually the classical Riemann theorem: if f is holomorphic on D \\ {c} and bounded near c (or continuous), then f extends holomorphically. If Mathlib has it (I have a feeling there is `Complex.RemovableSingularity`... let me actually grep), then:\n- G := the extension at each bad point... still needs the function defined by the expression to BE the extension... The theorem would give: F_expr differentiable on punctured ball + bounded ⟹ ∃ g analytic on ball agreeing punctured... then G as a global function: define G := F_expr outside E; at E points... still piecewise. UNLESS: the theorem applies to give AnalyticAt of F_expr ITSELF when F_expr is continuous at the point with its own value — no, junk value breaks continuity.\n\nHmm hmm. Let me think again about the point-value issue. Actually — wait. Is the value junk? Let's compute F_expr at ρ₀ (nontrivial zero): logDeriv ζ ρ₀ = ζ' ρ₀/ζ ρ₀ = ζ'ρ₀/0 = 0 (junk: x/0 = 0 in a field with inv_zero = 0). seriesFun ρ₀ = tsum with the ρ₀-term = mult·(1/(ρ₀−ρ₀)+1/ρ₀) = mult·(0+1/ρ₀) = mult/ρ₀. So F_expr(ρ₀) = 0 − mult/ρ₀ + 1/ρ₀ + 1/(ρ₀−1) − (logπ)/2 + ψ(ρ₀/2)/2 — a SPECIFIC complex number (all pieces have definite junk values). And the analytic candidate value A(ρ₀)−B(ρ₀)−... is some other specific number. They don't agree in general.\n\nSo indeed we cannot use F_expr as the entire function directly at bad points.\n\nDECISION: The piecewise definition with classical choice is actually not that bad if packaged right. Define:\n\nentirePart : ℂ → ℂ := fun s => if s ∈ E then 0 else F_expr s? No — wrong values on E.\n\nHmm OK — alternative classical packaging that TOTALLY avoids this: prove the identity form directly:\n\n**Capstone (5e-v)**: ∃ B : ℂ, ∀ s ∉ E, logDeriv ζ s = B + seriesFun s − 1/s − 1/(s−1) + (log π)/2 − digamma(s/2)/2.\n\nProof route for this WITHOUT naming an entire function explicitly: \n\nConsider the expression F_expr on U = ℂ ∖ E. Step 1 (5e-iv content): F_expr is LOCALLY BOUNDED near each bad point (punctured agreement with analytic A−B). Step 2: F_expr analytic on U. Step 3: Riemann removability per point ⟹ ∃! entire G extending F_expr... — the extension is the issue in Lean.\n\nAlternatively AVOID the extension: prove directly \"∃ B, ∀ good s, identity\" via the following ENTIRELY differentiating-free squeeze: for any two good points... no, the Liouville step fundamentally needs the entire function.\n\nOK here's another thought — what about defining G by the SERIES-CORRECTED expression that's actually well-defined everywhere:\n\nG s := F_expr s + (junk correction) where the junk correction is a finite combination of explicit \"correction\" functions that are nonzero only at bad points? E.g., at a nontrivial zero ρ₀, F_expr(ρ₀) is off from the analytic value by some δ_{ρ₀} — the correction would need to be a function supported exactly on E — e.g. via an infinite series over E of corrections... each correction needs its value = the discrepancy — which depends on the analytic extension value — choice + convergence — WAY worse.\n\nPractical resolution used in formalizations: define G by strong choice from the local analyticity witnesses:\n\nFor s : ℂ, decide: s ∈ E or not. If not: G s := F_expr s. If s ∈ E: G s := the limit... — Actually you know what, the cleanest: use `Classical.choice` on the local theorem at each bad point to get, for each bad point ρ₀, an analytic function A_{ρ₀} on a ball with punctured agreement. Then define G piecewise: G s := if h : s ∈ E then A_s(s) ... but A_s only exists near s...\n\nHmm, actually — WAIT. There's a classical trick I missed: prove DIRECTLY that F_expr is analytic at the bad points by exhibiting a power series... no.\n\nLet me look at this from the Mathlib-API angle: is there `AnalyticAt.congr`punctured-to-full? I.e., a lemma: f analytic on punctured nhd + f bounded near c ⟹ AnalyticAt (extension of f by any value...)? If Mathlib has the Riemann removable singularity theorem in the form:\n\n`theorem Complex.analyticAt_update_of_...`? or `analyticOn_insert_iff_...`? \n\nI should just search. If it exists, the build is: F_expr analytic on U; at each bad point: bounded near (from splits); update the value at the point (Function.update with the limit... any value works for boundedness⟹existence of analytic extension agreeing punctured — and the extension's value at the point is determined). Then define G globally via... still piecewise but now at each bad point I get AnalyticAt of SOME function agreeing punctured — for the GLOBAL entire function I still need a single function.\n\nHmm — the gluing: if ∀ s, AnalyticAt ℂ G s where G is the piecewise function — then G entire ✓ (AnalyticAt everywhere = analytic on univ). The piecewise G CAN be glued: at good s: G =ᶠ F_expr near s (ball avoiding E; on the ball, G = F_expr since no bad points) ⟹ AnalyticAt G s by congr ✓. At bad ρ₀: G = A_{ρ₀} on the punctured ball AND G(ρ₀) = A_{ρ₀}(ρ₀) — if I DEFINE G(ρ₀) := A_{ρ₀}(ρ₀) — but A_{ρ₀} comes from choice per point... Define G as: G s := if h : ∃ (e : E), s = e then (localValue s) else F_expr s where localValue needs the A-function at s — circular but: localValue s := (Classical.choose (local_theorem s)).extendValue... The local theorem at s ∈ E: ∃ (g : ℂ → ℂ), AnalyticAt ℂ g s ∧ (∀ᶠ y in 𝓝[≠] s, F_expr y = g y). Choose g_s := Classical.choose (this). Define G s := if s ∈ E then (choose...) s else F_expr s — wait but (choose h) is a function analytic at s; evaluating at s gives the right value; and on the punctured nhd G y = F_expr y = g_s y ✓. Then G =ᶠ[𝓝 s] g_s: for y ≠ s near: G y: if y ∈ E — PROBLEM: the punctured nhd might contain OTHER bad points y' where G(y') = g_{y'}(y') ≠ F_expr(y') — breaking the agreement with g_s at those points! Since E is discrete: choose the ball small enough that s is the ONLY bad point in it ✓ (E discrete). Then on the punctured ball: y ∉ E ⟹ G y = F_expr y = g_s y ✓; at s: G s = g_s s ✓ by def. So G =ᶠ[𝓝 s] g_s ⟹ AnalyticAt G s ✓✓.\n\nSo G is well-defined and entire. This is doable but fiddly (the E-membership decidability is classical — `if h : s ∈ E then ... else ...` with Classical.propDecidable — fine in noncomputable section).\n\nHmm wait — actually, hold on. Let me reconsider. Is there an even simpler global definition? \n\nG(s) := F_expr(s) for good s; for bad s the value is the punctured limit. Since F_expr is locally bounded near each bad point and analytic on U... the limit lim_{y→s, y≠s} F_expr y EXISTS (it equals A_s(s) where A_s is the local analytic witness) — and G(s) := lim if exists... `limUnder`! Define G s := if h : ∃ L, Tendsto F_expr (𝓝[≠] s) (nhds L) then limUnder (𝓝[≠] s) F_expr else F_expr s? For good s the punctured limit = F_expr s? F_expr continuous at good s ✓ (analytic) ⟹ punctured limit = value ✓ (T2). For bad s: punctured limit exists (= A_s(s)) ✓. So G := fun s => limUnder (𝓝[≠] s) F_expr — single clean definition! Then:\n- Good s: G s = F_expr s (continuous ⟹ limUnder = value: `ContinuousAt.limUnder_eq`? there's `tendsto_nhdsWithin...`: ContinuousAt ⟹ Tendsto f (𝓝[≠] s) (𝓝 (f s)) and limUnder = f s by uniqueness — but limUnder needs the limit to exist (nonempty... `Tendsto.limUnder_eq`? `Filter.Tendsto.limUnder_eq (h : ∃ l, Tendsto f l (𝓝 l))`? hmm: `limUnder_eq` API: `Tendsto.limUnder_eq (hf : Tendsto f l (𝓝 a)) : limUnder l f = a`? requires [NeBot l]? 𝓝[≠] s in ℂ is NeBot ✓ (NoIsolate... `nhdsWithin` NeBot for perfect spaces: `instNeBotNhdsWithin...`? ℂ is a perfect space — `NontriviallyNormedField`... there should be `NeBot (𝓝[≠] s)` for ℂ ✓).\n- So G s = F_expr s at ALL good s ✓ — then the capstone identity at good points uses F_expr directly ✓.\n- Bad s: G =ᶠ[𝓝 s] A_s (punctured agreement + value-at-point = A_s(s) = limUnder... need: limUnder (𝓝[≠] s) F_expr = A_s(s): A_s continuous at s + punctured agreement F_expr = A_s on 𝓝[≠] s ⟹ Tendsto F_expr (𝓝[≠]s) (𝓝 (A_s s)) ⟹ limUnder = A_s(s) ✓ by uniqueness).\n- And at bad s, G agrees with A_s on a FULL nhd: for y ≠ s in the small ball avoiding E\\{s}: G y = F_expr y (y good — wait y might be bad: the ball avoids other bad points ⟹ y good ✓ G y = F_expr y) = A_s y (punctured agreement) ✓; at s ✓. So G =ᶠ A_s ⟹ AnalyticAt G s ✓.\n\nThe limUnder definition is clean! But it hinges on: (i) Tendsto F_expr (𝓝[≠] s) (𝓝 (F_expr s)) at good s — continuity ✓; (ii) at bad s, the local analytic witness with punctured agreement — that's the actual 5e-iv content (the splits).\n\nActually — hmm, one more simplification: I don't even need the limUnder trick to be UNIFORM. I can define:\n\nG : ℂ → ℂ := fun s => limUnder (𝓝[≠] s) F_expr\n\nand prove:\n(1) ∀ good s: G s = F_expr s — via continuity.\n(2) ∀ s, AnalyticAt ℂ G s:\n   - good s: F_expr analytic at s; E discrete ⟹ ball with only-s-possibly-bad... s good so ball avoiding E entirely? E is closed? {nontrivial} ∪ {0,1} ∪ {−2n}: closed? nontrivial-zero set is not closed in ℂ?? It IS closed as a subset... zeros of ζ are closed+discrete; {nontrivial} = zeros ∩ strip — the strip's boundary (re = 0, 1) contains no zeros (except junk 1) — so {nontrivial} is closed (a discrete set with no accumulation... any accumulation point of {nontrivial} would be a zero accumulation ⟹ in zeros (closed) ⟹ some zero — on the boundary re ∈ {0,1}: no zeros there (needs the re=0/1 nonvanishing — Mathlib has re ≥ 1 nonvanishing; re ≤ 0 only trivial zeros — the classification AGAIN). Ugh — so \"E closed\" needs the classification. OR avoid it: at good s I don't need a ball avoiding E; I need G =ᶠ F_expr near s: G y = F_expr y holds at all GOOD y; near a good s, is every nearby y good? s good = s ∉ E. Need ball ⊆ Eᶜ ⟺ Eᶜ is a nhd ⟺ E closed. Hmm. OR: G y = F_expr y holds also at bad y?? No — at bad y, G y = A_y(y) ≠ F_expr y (junk) in general.\n   \n   So for good s I need nearby points good — E closed/discrete — which requires the zero classification (any zero is nontrivial or trivial). FINE — the classification lemma it is. Actually wait: is that right? E = {nontrivial} ∪ {0,1} ∪ {−2n}. Eᶜ = {good}. If there were an exotic zero ρ* (ζ ρ* = 0, not nontrivial, not −2n, not 0/1) — it's not in E; it's \"good\"; but F_expr is NOT analytic at ρ* (logDeriv blows up) — and worse, ζ zeros accumulate?? no. So I MUST exclude exotic zeros — classification: ζ s = 0 ⟹ s ∈ E (i.e. nontrivial ∨ trivial ∨ 0/1-junk). With that, zeros ⊆ E and:\n   - At good s: ζ s ≠ 0 ⟹ (s ≠ 1: differentiability; s = 1 ∈ E excluded ✓) continuity ball ζ ≠ 0 nearby ⟹ nearby zeros none ⟹ nearby points: could a nearby y be in E via being nontrivial/trivial/0/1? zeros excluded by the ball; {0,1} two points: choose ball smaller than dist to {0,1} ✓. So ball avoiding E ✓ WITHOUT closedness of the nontrivial set — direct: ball₁ from ζ ≠ 0 continuity (avoids ALL zeros hence all nontrivial/trivial zeros) ∩ ball₂ avoiding {0,1} (finite set, s ∉ it) ✓. Then on ball: every y good ⟹ G y = F_expr y ✓ ⟹ G =ᶠ F_expr ⟹ AnalyticAt G s ✓. And the classification is used only at... hmm wait — do I even need the classification anywhere?? At good s: ζ s ≠ 0 directly ⟹ the continuity ball avoids all zeros — no classification needed! At bad s (the splits): s ∈ E means s ∈ {nontrivial} ∪ {0} ∪ {1} ∪ {−2n} — each case's split argument is local (isolation from 5e-iii for nontrivial; for −2n: near −2n, other points: the ball around −2n of radius < 1... the OTHER bad points near −2n: nontrivial zeros? re near −2n is < −1 — no nontrivial zeros (re > 0 needed) ✓ direct; other −2m: distance ≥ 2 ✓; 0,1 far ✓. So ball(−2n, min(1, ...)) avoids E\\{−2n} ✓ no classification needed!). At 0: ball(0, 1/2): zeros in it? ζ(0) ≠ 0 continuity ball avoids zeros ✓; −2n: |−2n| ≥ 2 ✓; 1: distance 1 ✓. At 1: zetaA ball (ζ ≠ 0 punctured ✓); avoids 0, −2n by size ✓. At nontrivial ρ₀: 5e-iii's isolation ball ∩ avoid {0,1,−2n}: re ρ₀ ∈ (0,1) ⟹ small ball keeps re ∈ (0,1) avoiding 0,1,−2n ✓ and ζ-zeros in the ball: only ρ₀ — wait the isolation was among NONTRIVIAL zeros; the ball could contain TRIVIAL zeros? re near ρ₀ ∈ (0,1) — trivial zeros have re = −2n ≤ −2 — no ✓. Any zero in the ball is either trivial (no) or nontrivial (only ρ₀ ✓)... hmm — any zero in the ball: could be nontrivial (only ρ₀) or trivial (re excluded) — but \"any zero is nontrivial or trivial\" — the CLASSIFICATION again! A zero in the ball around ρ₀ (re ∈ (0,1)-ish... say re ∈ (ρ₀.re±δ)): an exotic zero would have... exotic = ζ zero with re ∉ (0,1) and ∉ {−2n} — the classification says none exist. Do I need it? The ball around ρ₀ has re ⊂ (0,1) (small enough); any ζ-zero there with re ∈ (0,1) IS nontrivial by DEFINITION ✓✓ — no classification needed! Similarly for the generic case: continuity ball avoids zeros entirely ✓. For −2n ball: re < −1: any zero with re < −1: is it trivial? classification needed?? If exotic zero ρ* with re = −3.5 existed inside ball(−2n, 1)... the classification (re ≤ 0 ⟹ −2m) is needed to rule it out. Hmm — BUT: do I need the ball around −2n to avoid ALL zeros? For the split at −2n: F = [ζ′/ζ − 1/(s+2n)] − [series] + [elems...]: seriesFun analytic at −2n needs −2n ∉ {nontrivial} ✓ (re < 0) — seriesFun_analyticAt needs ¬IsNontrivialZero (−2n) ✓ direct. The pieces: [ζ′/ζ − 1/(s+2n)] analytic AT −2n via NF + zeroMult = 1 ✓ (pointwise statement, no ball classification needed). The EVENTUAL EQUALITY F = A−B near −2n needs: the punctured equality F_expr y = (A−B)(y) for y near −2n, y ≠ −2n — pointwise algebra: F_expr y = logDeriv ζ y − seriesFun y + ... and A−B built from pieces agreeing pointwise — the equality at each good y is pure algebra ✓ no classification. And G =ᶠ A−B near −2n needs G y = F_expr y for y ≠ −2n near — G y = F_expr y for good y; bad y near −2n: other bad points could lurk (another −2m? distance ≥ 2 ✓ excluded; nontrivial? re < −1 ✓ excluded by def; exotic zeros?? — an exotic zero y* near −2n is NOT in E ⟹ \"good\" ⟹ G y* = F_expr y* — but F_expr is fine there? G y* = F_expr y* requires y* good ⟹ G = limUnder = value needs F_expr CONTINUOUS at y* — fails (pole) — my (1) proof would fail at y*... (1) says: at good s, F_expr analytic ⟹ continuous ⟹ limUnder = F_expr s — the analyticity of F_expr at good s is proved per-point (generic case: ζ s ≠ 0 needed! — at an exotic zero y*, ζ = 0 ⟹ logDeriv junk/pole ⟹ F_expr NOT analytic at y* — but y* is \"good\" (∉ E) — CONTRADICTION with my generic-case proof which requires ζ s ≠ 0 — I'd have to prove ζ y* ≠ 0 — i.e., rule out exotic zeros — CLASSIFICATION NEEDED for the generic case after all: generic s: s ∉ E ⟹ ζ s ≠ 0 requires \"ζ s = 0 ⟹ s ∈ E\".)\n\nOK so the classification lemma IS needed, once, for the generic case: `riemannZeta_eq_zero_imp`: ζ s = 0 → IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n ≥ 1, s = −2n. (With s = 0/1 vacuous but convenient.) Build via: re s ≥ 1 → nonvanishing (Mathlib) ⟹ re < 1; 0 < re: nontrivial ✓; re ≤ 0: FE argument ⟹ s ∈ {−2m, m ≥ 0} ∪ ... s = 0 case: m = 0; re ≤ 0 & ζ s = 0 ⟹ Gammaℝ s = 0 (else Λ s = ΓR s · ζ s... need the product identity valid: `completedRiemannZeta`... hmm — hold on, what did LiDisc's zeroDisc_isNontrivial actually do? It handled \"re ≤ 0 via ΓR-pole/FE\" inside the disc. Let me read that proof — it may already contain a reusable global lemma or be directly generalizable.\n\nLet me now also plan 5e-iv's file structure (LiFEntire.lean):\n\nPieces:\nP1. `riemannZeta_zero_classification`: ζ s = 0 → IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n ≥ 1, s = −2·n. [new build ~80-150 lines; check LiDisc first]\n\nP2. Nontrivial-zero split: at ρ₀: \n   - `logDeriv_zeta_sub_mult_div_analyticAt` : AnalyticAt ℂ (fun s => logDeriv riemannZeta s - (zeroMult ρ₀:ℂ)/(s - ρ₀)) ρ₀. Via the NF: ζ = (z−ρ₀)^m • h near ρ₀; logDeriv ζ = m/(z−ρ₀) + logDeriv h punctured; so the difference = logDeriv h punctured; logDeriv h analytic at ρ₀ (h analytic, h ρ₀ ≠ 0); the difference function at ρ₀: junk value vs logDeriv h ρ₀ — SAME point-value problem at the piece level!! Ugh. Handle: prove the PUNCTURED eventual equality only, and feed pieces into the global limUnder-G construction. So the splits produce: ∃ A, AnalyticAt A ρ₀ ∧ logDerivζ−m/(·−ρ₀) =ᶠ[𝓝[≠] ρ₀] A. That's all I need locally!\n\nSo per bad point ρ₀: ∃ (A : ℂ → ℂ), AnalyticAt ℂ A ρ₀ ∧ F_expr =ᶠ[𝓝[≠] ρ₀] A. Build A as the explicit combination:\nA := (fun s => logDeriv_h...) — the cleanest: A := [witness from logDeriv-NF at ρ₀] − [seriesFun − m/(·−ρ₀)] + [elems] where:\n- witness₁: AnalyticAt ℂ W ρ₀ ∧ (fun s => logDeriv ζ s − m/(s−ρ₀)) =ᶠ[𝓝[≠] ρ₀] W — from NF + logDeriv h.\n- seriesFun_sub_polar_analyticAt (5e-iii) gives AnalyticAt (seriesFun − m/(·−ρ₀)) ρ₀ — but I need punctured equality of seriesFun − m/(·−ρ₀) with itself — trivial (rfl agreement ✓ it's already analytic, no junk issue? seriesFun − m/(s−ρ₀) AT ρ₀: seriesFun ρ₀ = junk mult/ρ₀; m/(ρ₀−ρ₀) = m/0 = 0 junk; so the expression at ρ₀ = mult/ρ₀ − 0 = mult/ρ₀. The analytic function (from 5e-iii) at ρ₀ has the correct limit value. So as FUNCTIONS they differ at ρ₀. But for the punctured agreement I only need 𝓝[≠] ✓ fine.)\n- elems: −1/s−1/(s−1)+(logπ)/2−ψ(s/2)/2 — analytic at ρ₀ (re ∈ (0,1)): 1/s analytic (s ≠ 0 ✓ re > 0), 1/(s−1) (re < 1 ✓), ψ(s/2): s/2 ∉ {0,−1,...} ✓ re(s/2) ∈ (0,1/2) — digamma analytic off nonpositive integers: Mathlib `analyticAt_digamma`? hmm — what do we have for digamma analyticity? LiDigamma proved `digamma_analyticOn : AnalyticOnNhd ℂ Complex.digamma dpsiDomain` where dpsiDomain = ball(1/2, 1/2)?? That's just the unit ball around 1/2. For general points: Mathlib `Complex.analyticAt_digamma (hs : s ∉ {0,-1,-2,...})`? hmm — Zeta23 DigammaSeries? There might be `Complex.differentiableAt_digamma` / analyticity: Mathlib has `Complex.differentiableAt_digamma (h : ∀ n : ℕ, s ≠ -n)`?? I recall `differentiableAt_digamma : (∀ n : ℕ, s ≠ -↑n) → DifferentiableAt ℂ digamma s`? Hmm wait — differentiableAt implies analyticAt? NO — DifferentiableAt.analyticAt does NOT exist (banked session-026 gotcha!). DifferentiableOn on an open set gives analyticOnNhd. So for a point: differentiableAt at all nearby points (neighborhood) ⟹ DifferentiableOn a ball ⟹ analyticOnNhd ⟹ AnalyticAt. So: DifferentiableAt digamma at every point of a ball around ρ₀/2 (the condition ∀ n, y ≠ −n is open-ish: the set {y | ∀ n:ℕ, y ≠ −n} = complement of −ℕ∪{0} — closed discrete complement ⟹ open ✓) ⟹ DifferentiableOn ball ⟹ AnalyticAt ✓. Need the differentiability lemma name — grep Zeta23/Mathlib for differentiableAt_digamma.\n\nP3. s = 1 split: witness W₁ := logDeriv zetaA: AnalyticAt at 1 (zetaA analytic, zetaA 1 = 1 ≠ 0 ⟹ logDeriv = deriv/zetaA analytic: AnalyticAt.div needs zetaA ≠ 0 AT 1 — AnalyticAt.deriv + AnalyticAt.div (denominator nonzero at the point ✓ then nonzero nearby — but AnalyticAt.div only needs the value nonzero at the point ✓)). Punctured agreement: logDeriv ζ + 1/(s−1) = logDeriv zetaA on 𝓝[≠] 1: logDeriv zetaA s = zetaA' s/zetaA s; zetaA s = (s−1)ζ s punctured; logDeriv of product punctured: logDeriv ((s−1)ζ s) = 1/(s−1) + logDeriv ζ s ✓ (logDeriv_mul, needs (s−1) ≠ 0 ✓ punctured, ζ s ≠ 0 punctured — zetaA-ne-zero ball ⟹ ζ s = zetaA s/(s−1) ≠ 0 punctured ✓). So logDeriv ζ s = logDeriv zetaA s − 1/(s−1) punctured ✓. Then F_expr = logDeriv ζ − seriesFun + 1/s + 1/(s−1) − c + ψ/2 = [logDeriv zetaA] − seriesFun + 1/s − c + ψ(s/2)/2 punctured — all analytic at 1 ✓ (seriesFun: 1 not nontrivial ✓ (re = 1); ψ(1/2): fine; 1/s fine).\n\nP4. s = 0 split: F_expr = logDeriv ζ + [1/s + ψ(s/2)/2] − seriesFun + 1/(s−1) − c. The bracket: ψ(s/2)/2 + 1/s analytic at 0: ψ(w) = −1/w − γ + (series part) — the digamma series: from Zeta23 DigammaSeries.digamma_series: ψ(z) = −γ − 1/z + Σ'_{n} (1/(n+1) − 1/(z+n+1)) for z ∈ integerComplement. So ψ(s/2)/2 + 1/s = −γ/2 + ½Σ'(1/(n+1) − 1/(s/2+n+1)) for s/2 ∈ integerComplement — near 0 (ball(0,1): s/2 ∈ ball(0,1/2) ⊆ integerComplement ✓ since integers in ball(0,1/2): only 0 — excluded punctured ✓... wait integerComplement := {z | ∀ n:ℤ, z ≠ n}? or {z | z ∉ ℤ}? For s/2 with 0 < |s/2| < 1/2: s/2 not an integer ✓ (|s/2| < 1/2 ⟹ s/2 ∈ ℤ ⟹ s/2 = 0 ⟹ s = 0 excluded punctured ✓). So punctured agreement with A₀ := −γ/2 + ½·(the series function) + logDeriv ζ − seriesFun + 1/(s−1) − c pieces:\n   A₀ := (fun s => logDeriv riemannZeta s) [analytic at 0: ζ(0) = −1/2 ≠ 0 ⟹ AnalyticAt.div — need ζ analytic at 0 ✓ (0 ≠ 1) and ζ 0 ≠ 0: Mathlib `riemannZeta_zero : riemannZeta 0 = -1/2`? I recall riemannZeta_zero exists ✓] + (digamma-series analytic part) − seriesFun + 1/(s−1) − c. The series part analytic at 0: the 5e-iii Weierstrass machinery on ball(0, 1/2): terms 1/(n+1) − 1/(w+n+1) = w/((n+1)(w+n+1)): ‖w‖ ≤ 1/2 ⟹ ‖w+n+1‖ ≥ n+1/2 ≥ (n+1)/2 ⟹ |term| ≤ 2‖w‖/(n+1)² ≤ 1/(n+1)² — M-test Σ 1/(n+1)² ✓ (summable_div_add_one_sq from LiDigamma ✓ banked). Punctured agreement: from digamma_series (needs s/2 ∈ integerComplement ✓ punctured ball) — the equality digamma = −γ − 1/z + series: so ψ(s/2)/2 = −γ/2 − 1/s + ½·series(s/2) ⟹ 1/s + ψ(s/2)/2 = −γ/2 + ½series(s/2) ✓.\n\n   Hmm wait — Zeta23's digamma_series: `theorem digamma_series {z : ℂ} (hz : z ∈ Complex.integerComplement) : ...` — let me check its exact form (LiDigamma used it — the series was dpsiTermC-related: `Complex.digamma z = -γ - 1/z + ∑' m, dpsiTermC z m`? something like that). Check LiDigamma's usage.\n\nP5. s = −2n split (n ≥ 1): witness: [logDeriv ζ − 1/(s+2n)] analytic at −2n: NF at −2n: ζ = (z+2n)¹ • h (zeroMult_neg_two_mul = 1 — analyticOrderNatAt = 1); logDeriv ζ = 1/(z+2n) + logDeriv h punctured ⟹ difference = logDeriv h analytic ✓. And [−ψ(s/2)/2 − ...]: −(−1/(s+2n)) — wait F_expr has +ψ(s/2)/2; ψ(s/2) at s = −2n: w = s/2 = −n: ψ(w) = −1/(w+n) + (analytic at −n) — from the series: ψ(w) = −γ − 1/w + Σ'_{j}(1/(j+1) − 1/(w+j+1)): the j = n−1 term: −1/(w+n) — split it off: ψ(w) = −1/(w+n) + H_n(w), H_n analytic at −n (the remaining series + the −γ − 1/w: 1/w analytic at −n ✓; remaining series terms analytic: poles at w = −(j+1) ≠ −n for j ≠ n−1 ✓ and the M-test on a small ball around −n avoiding all −(j+1)... the ball(−n, 1/2) contains no other nonpositive integer ✓ uniform bound: ‖term‖ = ‖1/(j+1) − 1/(w+j+1)‖ = ‖w‖/((j+1)‖w+j+1‖): ‖w+j+1‖ ≥ |j+1−n| − 1/2 ≥ 1/2 for j ≠ n−1; ‖w‖ ≤ n+1/2: |term| ≤ (n+1/2)·2/(j+1)... that gives ~2n/(j+1) NOT summable!! Need the j+1 in the denominator squared: |term| ≤ ‖w‖/((j+1)·‖w+j+1‖): for j ≥ 2n+2: ‖w+j+1‖ ≥ (j+1)/2 ⟹ ≤ 2‖w‖/(j+1)² ✓ summable tail; finite head j ≤ 2n+1, j ≠ n−1: bounded terms ✓ (eventually-form M-test: cofinite head ✓ — use of_norm_le_summable_eventually again: for j ≥ 2n+2 the uniform bound 2(n+1)/(j+1)²... wait ‖w‖ ≤ n + 1/2 ≤ 2n for n ≥ 1: 2‖w‖/(j+1)² ≤ 4n/(j+1)²? Hmm — but the majorant must not depend on the ball... it's fine: u j := 2(n+1)/(j+1)² for j ≥ 2n+2 — summable ✓ (p-series)). So H_n(w) analytic at −n, ψ(w) + 1/(w+n) = H_n(w) punctured ⟹ ψ(s/2)/2 = −1/(s+2n) + H_n(s/2)/2·... wait: w = s/2: ψ(s/2) = −1/(s/2+n) + H_n(s/2) = −2/(s+2n) + H_n(s/2). So ψ(s/2)/2 = −1/(s+2n) + H_n(s/2)/2 ✓ punctured. Then F_expr = [logDeriv ζ − 1/(s+2n)] − seriesFun + 1/s + 1/(s−1) − c + [−1/(s+2n) + H_n(s/2)/2]... wait F_expr = logDerivζ − series + 1/s + 1/(s−1) − c + ψ(s/2)/2: substitute: = [logDerivζ − 1/(s+2n)] − series + 1/s + 1/(s−1) − c + H_n(s/2)/2 + [1/(s+2n) − 1/(s+2n)]... hold on: logDerivζ = [logDerivζ − 1/(s+2n)] + 1/(s+2n); ψ/2 = −1/(s+2n) + H_n/2: sum: the ±1/(s+2n) cancel ✓. So A_{−2n} := W_triv − seriesFun + 1/s + 1/(s−1) − c + H_n(s/2)/2 analytic at −2n ✓ (seriesFun: −2n not nontrivial ✓; 1/s, 1/(s−1) fine; H_n(s/2) analytic at −n ✓ comp with s/2 ✓).\n\nP6. Generic case: s ∉ E: ζ s ≠ 0 (by P1 classification + ∉ E... wait: classification: ζ s = 0 ⟹ nontrivial ∨ 0 ∨ 1 ∨ −2n: all in E ⟹ s ∉ E ⟹ ζ s ≠ 0 ✓). And s ≠ 1 ✓. logDeriv ζ analytic at s: AnalyticAt.div (deriv: AnalyticAt.deriv of analyticAt_riemannZeta (s ≠ 1)) (ζ s ≠ 0) ✓. seriesFun analytic (5e-iii, s not nontrivial ✓). 1/s: s ≠ 0 ✓. 1/(s−1): s ≠ 1 ✓. ψ(s/2): s/2 ∉ {0}∪−ℕ: s/2 = −m ⟺ s = −2m: m = 0: s = 0 ∈ E ✓ excluded; m ≥ 1: −2m ∈ E ✓. So s/2 satisfies the digamma differentiability condition ⟹ AnalyticAt via the ball argument ✓. So F_expr analytic at s — and G s = F_expr s (limUnder = value, continuity) — for the G-construction.\n\nP7. The G assembly: G := fun s => limUnder (𝓝[≠] s) F_expr.\n   - At good s: F_expr analytic at s (P6) ⟹ continuous ⟹ Tendsto (𝓝[≠] s) → 𝓝 (F_expr s) ⟹ G s = F_expr s — need NeBot (𝓝[≠] s) and the limUnder API: `Filter.Tendsto.limUnder_eq`? Let me check the exact name: `Tendsto.limUnder_eq [NeBot l] [T2Space] (hf : Tendsto f l (𝓝 a)) : limUnder l f = a`? I think there's `Tendsto.limUnder_eq` ✓ or `limUnder_eq_of_tendsto`. Check.\n   - G analytic at good s: need G =ᶠ[𝓝 s] F_expr: ball avoiding E (from the ζ≠0-continuity ball + avoiding {0,1}): on the ball every y: ζ y ≠ 0 ⟹ y ∉ {nontrivial} by def; y ∉ {0,1} by size; y ∉ {−2n}: ζ(−2n) = 0 excluded ✓. So all y good ⟹ G y = F_expr y on the ball (full nhd) ✓ AnalyticAt.congr ✓.\n   - At bad s ∈ E: the witness A (analytic at s, punctured agreement F_expr =ᶠ[𝓝[≠]s] A): G =ᶠ[𝓝 s] A: full-nhd agreement: at s: G s = limUnder = A s (uniqueness: Tendsto F_expr (𝓝[≠]s) (𝓝 (A s)) from punctured agreement + A continuous) ✓; at y ≠ s near: y good (ball avoiding E\\{s} — need per-case: nontrivial ρ₀: isolation-ball ∩ re-strip-ball (avoid 0,1,−2n via re ∈ (0,1)... the isolation ball from 5e-iii avoids other nontrivial zeros; intersect with ball(ρ₀, min(re ρ₀, 1−re ρ₀)) ⟹ re ∈ (0,1) ⟹ y ∉ {0,1}: 0/1 are real with re... y = 0 has re 0 ∉ (0,1) ✓; y = 1 re 1 ✓; y = −2n re ≤ −2 ✓; y nontrivial: only ρ₀ ✓. So punctured y good ⟹ G y = F_expr y = A y ✓. Similarly at 0: ball(0, 1/2)∩(ζ≠0 continuity ball): y ≠ 0: ζ y ≠ 0 ⟹ not a zero ⟹ y ∉ nontrivial/trivial; y ≠ 1 ✓ size; y ≠ 0 ✓ punctured ⟹ good ✓. At 1: zetaA ball (ζ ≠ 0 off 1) ∩ small: ✓. At −2n: ball(−2n, 1/2): y ≠ −2n: y nontrivial? re y < −2n+1/2 < 0 ✓ no; y ∈ {−2m}? |y+2n| < 1/2 ⟹ no other even integer ✓; y ∈ {0,1} ✓ no; BUT exotic zeros with re ≤ 0?? — classification: any zero with re ≤ 0 is −2m ✓ P1. Hmm wait — for y ∈ ball(−2n, 1/2), y ≠ −2n: is y good? y ∈ E iff nontrivial (no, re) ∨ y = 0 (no) ∨ y = 1 (no) ∨ y = −2m (only −2n possible, excluded) ⟹ y good ✓ — NO classification needed here since E-membership is what matters, not zeros! ✓ (The classification is needed ONLY in P6 for ζ s ≠ 0.) \n\n   Then G =ᶠ A ⟹ AnalyticAt G s ✓.\n   \n   So G entire: `AnalyticOnNhd ℂ G Set.univ`? or ∀ s, AnalyticAt ℂ G s — package as needed for 5e-v: `fun s => ...`∀ s, AnalyticAt ℂ G s — that's \"AnalyticAt everywhere\" — 5e-v needs: G entire + G = F_expr at good points + the circle bound.\n\nP8. The capstone for 5e-iv's deliverable (per D-068 §7: 5e-iv = F entire; the ∃ B identity is 5e-v after the circle bound + squeeze). So 5e-iv's theorem: ∃ G : ℂ → ℂ, (∀ s, AnalyticAt ℂ G s) ∧ (∀ s, s ∉ E → G s = F_expr s). Where F_expr s := logDeriv riemannZeta s − seriesFun s + 1/s + 1/(s−1) − (Real.log π)/2 + digamma(s/2)/2 and E-membership phrased as (¬IsNontrivialZero s) ∧ s ≠ 0 ∧ s ≠ 1 ∧ (∀ n ≥ 1, s ≠ −2n).\n\nHmm — actually for 5e-v's circle bound I'll bound F_expr on the circles (good points) = G on circles ✓ via P7's equality.\n\nLet me now scope the digamma analyticity lemma. Check: Mathlib `Complex.differentiableAt_digamma`? Let me grep. Also `Complex.integerComplement` and the Zeta23 digamma_series exact statement. And check LiDisc's zeroDisc_isNontrivial for the classification pieces. And check Mathlib for Gammaℝ_eq_zero_iff and completedRiemannZeta one_sub / nonvanishing of Λ.\n\nThis is a big build (~0.5–1 session per D-068's estimate). Let me start by checking all the pieces.","signature":""},{"type":"text","text":"Continuing the route: **ii′-5e-iv** (F entire by principal-part splits, D-068 §4). Let me first inventory the pieces I'll need: the digamma analyticity API, the Zeta23 digamma series statement, the LiDisc zero-classification argument, and the limUnder API."},{"type":"tool_use","id":"Bash_100","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"differentiableAt_digamma\\|analyticAt_digamma\\|differentiable_digamma\" Mathlib/Analysis/SpecialFunctions/Gamma/*.lean Mathlib/NumberTheory/ -r 2>/dev/null | head -6; echo ===; grep -rn \"integerComplement\" Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean | head -5; echo ===; grep -rn \"limUnder_eq\\|theorem.*limUnder\" Mathlib/Topology/Basic.lean Mathlib/Order/Filter/*.lean -r 2>/dev/null | grep -i \"tendsto\\|eq_of\" | head -8","description":"Check digamma differentiability and limUnder API"},"extra_content":null}]