[{"type":"thinking","thinking":"- `AnalyticAt.deriv` ✓ (fun_prop, protected — use `hf.deriv`).\n- `nhdsNE_neBot (x : α) : NeBot (𝓝[≠] x)` in Normed/Field/Basic.lean:248 — for a nontrivially normed field α — is it an instance? Line 248 `theorem nhdsNE_neBot` — if not an instance, I provide it: `nhdsNE_neBot s`. Check if it's an instance: let me just check quickly... I'll write `haveI := nhdsNE_neBot s` if needed.\n\nAll pieces confirmed. Now write the plan as tasks and start LiFEntire.lean. Given the size (~800 lines), I'll build it in two stages with an intermediate compile:\n\nStage A: helpers (A1 digamma analyticAt, A2 classification, the digamma series parts + M-tests, the per-point punctured identities).\nStage B: the G assembly + capstone.\n\nActually let me structure the file top-down and fill in. Sections:\n\n§0 Fexpr, badPoint defs.\n§1 analyticAt_digamma.\n§2 zeta_zero_classification.\n§3 the logDeriv-at-zero witness (nontrivial zeros + trivial zeros, unified): \n   lemma logDeriv_zeta_sub_order_div_eventually {ρ₀ : ℂ} (hρ : riemannZeta ρ₀ = 0) (hρ1 : ρ₀ ≠ 1) :\n     ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧ ∀ᶠ s in 𝓝[≠] ρ₀, logDeriv riemannZeta s - (zeroMult ρ₀ : ℂ)/(s - ρ₀) = W s\n   — unified for both nontrivial and trivial zeros! (zeroMult(−2n) = 1 known but not needed for THIS lemma; the mult is symbolic.) Build via NF + logDeriv_mul (the LiSides Rfun_residue_at block pattern).\n   W := logDeriv h where h from the NF.\n§4 the s=1 witness:\n   lemma Fexpr_eventually_one : ∃ W, AnalyticAt ℂ W 1 ∧ Fexpr =ᶠ[𝓝[≠] 1] W\n   W := fun s => logDeriv zetaA s - seriesFun s + 1/s - (log π)/2 + digamma(s/2)/2\n   pieces analytic at 1: logDeriv zetaA ✓; seriesFun (¬IsNontrivialZero 1: re 1 = 1 not < 1 ✓); 1/s ✓ (1 ≠ 0); digamma(1/2): ∀ m, 1/2 ≠ −m ✓ analyticAt_digamma; composition s ↦ s/2 ✓.\n   punctured: near 1 (zetaA ball, s ≠ 1): Fexpr s = W s: logDeriv ζ s = logDeriv zetaA s − 1/(s−1) ⟹ Fexpr = logDeriv zetaA − 1/(s−1) − series + 1/s + 1/(s−1) − c + ψ/2 = W ✓ ring.\n§5 the s=0 witness:\n   digammaSeriesPart w := ∑' j : ℕ, (1/((j:ℂ)+1) − 1/(w+j+1))\n   digammaSeriesPart_analyticOn : AnalyticOnNhd on ball(0, 1/2) — M-test (of_norm_le_summable, all-terms form: ‖term‖ ≤ 1/(j+1)² for ‖w‖ ≤ 1/2 — wait the domain is the OPEN ball(0,1/2): ‖w‖ < 1/2: ‖w+j+1‖ ≥ (j+1) − ‖w‖ > (j+1) − 1/2 ≥ (j+1)/2 (since j+1 ≥ 1 > 1/2... (j+1) − 1/2 ≥ (j+1)/2 ⟺ j+1 ≥ 1 ✓). ‖term‖ = ‖w‖/((j+1)‖w+j+1‖) ≤ (1/2)/((j+1)(j+1)/2) = 1/(j+1)² ✓. summable: LiDigamma's `summable_div_add_one_sq 1` — check its statement: Summable fun m => 1/((m:ℝ)+1)^2? presumably ✓.\n   Algebra: 1/(j+1) − 1/(w+j+1) = w/((j+1)(w+j+1)): needs j+1 ≠ 0 (nat cast ✓), w+j+1 ≠ 0 (ball(0,1/2): ‖w+j+1‖ > (j+1)−1/2 ≥ 1/2 ✓).\n   digamma_series_eq : for w ∈ ball(0,1/2), w ≠ 0: digamma w = −γ − 1/w + digammaSeriesPart w — via digamma_series (integerComplement: w with ‖w‖ < 1/2, w ≠ 0: w = (k:ℤ) ⟹ |k| < 1/2 ⟹ k = 0 ⟹ w = 0 contra).\n   W₀ := fun s => logDeriv riemannZeta s − seriesFun s + 1/(s−1) − c + (−γ + digammaSeriesPart (s/2))/2\n     wait: Fexpr = logDerivζ − series + 1/s + 1/(s−1) − c + ψ(s/2)/2; ψ(s/2) = −γ − 2/s + dsp(s/2) ⟹ 1/s + ψ(s/2)/2 = 1/s − γ/2 − 1/s + dsp(s/2)/2 = −γ/2 + dsp(s/2)/2 ✓.\n     W₀ := logDerivζ s − seriesFun s + 1/(s−1) − c + (−eulerMascheroniConstant + digammaSeriesPart (s/2))/2 — analytic at 0: logDeriv ζ at 0: ζ 0 = −1/2 ≠ 0 (riemannZeta_zero ✓) + analyticAt_riemannZeta (0 ≠ 1) ⟹ AnalyticAt.div (.deriv) ✓; seriesFun: ¬IsNontrivialZero 0 (re 0 = 0 not > 0 ✓); 1/(s−1): s−1 ≠ 0 at 0 ✓ (AnalyticAt: 1/(s−1) analytic at 0: (analyticAt_const).div (analyticAt_id.sub analyticAt_const) (by norm_num : (0:ℂ)−1 ≠ 0)); dsp(s/2): AnalyticAt.comp of dsp analytic at 0/2 = 0 ✓ and s/2 linear ✓; const pieces ✓.\n   punctured: s near 0, s ≠ 0: need s/2 ∈ ball(0, 1/2) ⟺ ‖s‖ < 1 — take ball(0, 1/2) for s ⟹ ‖s/2‖ < 1/4 < 1/2 ✓ and s/2 ≠ 0 (s ≠ 0) ✓ ⟹ digamma series applies ✓ ⟹ Fexpr s = W₀ s by the algebra ✓.\n§6 the −2n witness (n ≥ 1):\n   digammaSeriesPartSub n w := ∑' j, if j = n−1 then 0 else (1/(j+1) − 1/(w+j+1))\n   analytic on ball(−n, 1/2) — eventually M-test: for j ≥ 2n: uniform 4n/(j+1)²-ish; hmm let me redo: w ∈ ball(−(n:ℂ), 1/2): ‖w‖ ≤ n + 1/2 ≤ 3n/2 (n ≥ 1: n + 1/2 ≤ 3n/2 ⟺ 1 ≤ n ✓); ‖w+j+1‖ ≥ |j+1−n| − 1/2... for j+1 ≥ 2n+2 (j ≥ 2n+1): ‖w+j+1‖ ≥ (j+1) − ‖w‖ ≥ (j+1) − 3n/2 ≥ (j+1)/4 ⟺ 3(j+1)/4 ≥ 3n/2 ⟺ j+1 ≥ 2n ✓ — so for j ≥ 2n+1: ‖w+j+1‖ ≥ (j+1)/4: ‖term‖ ≤ (3n/2)·4/(j+1)² = 6n/(j+1)² ✓ summable. Eventually-form ✓.\n   ALSO need: each term's poles avoided on the whole ball: w + j + 1 ≠ 0 for w ∈ ball(−n, 1/2), j ≠ n−1: w = −(j+1) would need |n − (j+1)| < 1/2 ⟹ j+1 = n ⟹ j = n−1 excluded ✓.\n   The single-term split: digammaSeriesPart w = digammaSeriesPartSub n w + (1/n − 1/(w+n)) for w ∈ ball(−n, 1/2): tsum split via the 5e-iii single-pattern: full = sub + single where single j = if j = n−1 then (1/(j+1) − 1/(w+j+1)) else 0: tsum = 1/n − 1/(w+n) (tsum_eq_single n−1: needs the term at n−1 = 1/((n−1)+1) − 1/(w+(n−1)+1) = 1/n − 1/(w+n) ✓ cast arithmetic (n−1)+1 = n for n ≥ 1: Nat.sub_add_cancel). Summability: full (from A6-0's... wait digammaSeriesPart summable on ball(−n,1/2)? The M-test for the full series on ball(−n, 1/2): same eventually bound ✓ (the j = n−1 term: pole at −n IS in the ball — the term 1/n − 1/(w+n) is unbounded on the ball! So the M-test for the FULL series on ball(−n,1/2) FAILS at that term — that's exactly why we subtract. For the SPLIT at a FIXED w ≠ −n: summability of the full series at w (from digamma_series's summable_digamma_series? or direct tail bound at the point) + sub-series summable at w (M-test on the ball gives HasSumUniformlyOn ⟹ pointwise HasSum at w... w ∈ ball ✓ (if w ≠ −n... the M-test domain includes −n! the sub-series is fine at −n ✓). So: Summable (sub) at each w ∈ ball via the uniform convergence; Summable (full) at w ≠ −n via... digamma_series gives the HasSum at w ∈ integerComplement — w ∈ ball(−n,1/2), w ≠ −n ⟹ w ∉ ℤ ✓ (integers within 1/2 of −n: only −n). So full summable via (summable_digamma_series hz) ✓ Zeta23. single summable ✓. Then full = sub + single via Summable.tsum_add on (sub + single = full pointwise) ✓.\n   Hmm wait — simpler: define sub-series and prove its summability directly (M-test ball). The full-series summability at the specific w: could ALSO get from the digamma_series's HasSum — but actually easiest: Summable (full at w) ⟸ the M-test on ball(0-ish)?? no. Use summable_digamma_series (Zeta23, exists for w ∈ integerComplement) ✓.\n   Then H_n w := −γ − 1/w + digammaSeriesPartSub n w + 1/n: analytic at −n (1/w at −n ✓ nonzero; the rest ✓).\n   Punctured: digamma w = −1/(w+n) + H_n w for w ∈ ball(−n,1/2), w ≠ −n:\n   digamma w = −γ − 1/w + full = −γ − 1/w + sub + (1/n − 1/(w+n)) = [−1/(w+n)] + [−γ − 1/w + sub + 1/n] = −1/(w+n) + H_n w ✓ ring.\n   Then for s near −2n (s ≠ −2n): digamma(s/2)/2 = −1/(s+2n)·... 1/(s/2+n) = 2/(s+2n): digamma(s/2)/2 = −1/(s+2n) + H_n(s/2)/2 ✓.\n   W_{−2n} := fun s => (logDeriv ζ s − 1/(s+2n)-corrected...) hmm — the witness: from §3's unified lemma at ρ₀ = −2n: W_triv with logDeriv ζ − (zeroMult(−2n))/(s+2n) =ᶠ W_triv; zeroMult(−2n) = 1 ⟹ logDeriv ζ = W_triv + 1/(s+2n) punctured. Fexpr = W_triv + 1/(s+2n) − series + 1/s + 1/(s−1) − c + [−1/(s+2n) + H_n(s/2)/2] = W_triv − series + 1/s + 1/(s−1) − c + H_n(s/2)/2 ✓ analytic at −2n: seriesFun (¬nontrivial: re = −2n < 0 ✓), 1/s (−2n ≠ 0 ✓), 1/(s−1) ✓, H_n(s/2) comp ✓.\n§7 nontrivial-zero witness:\n   From §3 at ρ₀ (IsNontrivialZero ρ₀: ζ ρ₀ = 0, ρ₀ ≠ 1 ✓ re < 1): logDeriv ζ = W_{ρ₀} + m/(s−ρ₀) punctured. Fexpr = [W_{ρ₀} + m/(s−ρ₀)] − series + 1/s + 1/(s−1) − c + ψ/2. And seriesFun = [seriesFun − m/(s−ρ₀)] + m/(s−ρ₀) — so Fexpr = W_{ρ₀} − [seriesFun − m/(s−ρ₀)] + 1/s + 1/(s−1) − c + ψ(s/2)/2 punctured. Witness W := W_{ρ₀} − (fun s => seriesFun s − m/(s−ρ₀)) + elems: analytic at ρ₀: seriesFun_sub_polar_analyticAt (5e-iii ✓); 1/s (re ρ₀ > 0 ⟹ ρ₀ ≠ 0 ✓); 1/(s−1) (re < 1 ⟹ ρ₀ ≠ 1 ✓); ψ(s/2): s/2 = ρ₀/2: ∀ m, ρ₀/2 ≠ −m: re(ρ₀/2) > 0 > −m's re... ρ₀/2 = −m ⟹ re = −m ≤ 0 contra re > 0 ✓ analyticAt_digamma ✓ comp /2 ✓.\n§8 generic case:\n   lemma Fexpr_analyticAt_of_not_bad {s} (hs : ¬ badPoint s) : AnalyticAt ℂ Fexpr s:\n   ζ s ≠ 0 (classification: ζ s = 0 ⟹ badPoint: nontrivial ✓ / s=0 ✓ / −2n ✓ — my classification disjuncts match badPoint ✓); s ≠ 1 ✓; s ≠ 0 ✓; s/2 ∉ {0}∪−ℕ: s/2 = −m ⟺ s = −2m: m = 0 ⟹ s = 0 ✓; m ≥ 1 ⟹ bad ✓.\n   Fexpr = combination of analytic pieces ✓.\n   ALSO continuity for limUnder: AnalyticAt ⟹ continuousAt ✓.\n§9 G assembly:\n   def Gentire : ℂ → ℂ := fun s => limUnder (𝓝[≠] s) Fexpr\n   lemma Gentire_eq_Fexpr {s} (hs : ¬ badPoint s) : Gentire s = Fexpr s:\n     Tendsto Fexpr (𝓝[≠] s) (𝓝 (Fexpr s)) := (Fexpr_analyticAt_of_not_bad hs).continuousAt.tendsto... ContinuousAt.tendsto_nhdsWithin? ContinuousAt: Tendsto f (𝓝 s) (𝓝 (f s)) ⟹ nhdsWithin version: `ContinuousAt.tendsto_nhdsWithin`? hmm: Tendsto f (𝓝[≠] s) (𝓝 (Fexpr s)) from ContinuousAt: `ContinuousAt.tendsto` : Tendsto f (𝓝 s) ... then `.mono (nhdsWithin_le_nhds)`? 𝓝[≠] s ≤ 𝓝 s: nhdsWithin_le_nhds ✓: (hc.tendsto).mono (nhdsWithin_le_nhds)?? ContinuousAt unfolds to Tendsto f (𝓝 s) (𝓝 (f s)) ✓ so (hc).mono nhdsWithin_le_nhds... Tendsto.mono : Tendsto f l₁ L → l₂ ≤ l₁ → Tendsto f l₂ L ✓.\n     Then limUnder (𝓝[≠] s) Fexpr = Fexpr s: tendsto_nhds_unique (NeBot) (tendsto_nhds_limUnder ⟨Fexpr s, h⟩) h: tendsto_nhds_limUnder gives Tendsto Fexpr (𝓝[≠]s) (𝓝 (limUnder ...)); uniqueness with h ⟹ limUnder = Fexpr s ✓ — wait direction: tendsto_nhds_unique (h₁ : Tendsto f l (𝓝 a)) (h₂ : Tendsto f l (𝓝 b)) : a = b: so tendsto_nhds_unique (tendsto_nhds_limUnder ⟨...⟩) h : limUnder = Fexpr s ✓.\n   lemma Gentire_analyticAt (s : ℂ) : AnalyticAt ℂ (Gentire) s:\n     by_cases badPoint s:\n     - bad: obtain the witness W (case split on the 4 disjuncts): Gentire =ᶠ[𝓝 s] W:\n       full-nhd EventualEq: from Metric eventually-ball: take the punctured agreement ball ε₁ (Fexpr = W on 𝓝[≠] s via eventually_nhdsWithin... get ball form: ∀ y, 0 < dist y s < ε₁ → Fexpr y = W y) and the E-avoidance ball ε₂ (every y ≠ s in ball ε₂ is good — per-case: nontrivial: 5e-iii isolation ∩ re-strip; 0: ball(0, 1/2) + ζ-continuity... wait for s = 0 bad-case: y ≠ 0 in ball(0, 1/2): good? y nontrivial? then ζ y = 0... could a nontrivial zero be near 0? |ρ| ≥ ... nontrivial zeros have re ∈ (0,1) — |im| ≥ ... no: zeros near 0? The FIRST zero is at 14.13 — but formally: y nontrivial ⟹ re y ∈ (0,1) — possible in ball(0,1/2)?? re ∈ (0,1), e.g. 0.4+0.001i — is it a zero? Unknown locally! I need: ball(0, δ) contains no nontrivial zeros — from ζ(0) = −1/2 ≠ 0 + continuity: ball with ζ ≠ 0 ✓ excludes ALL zeros ✓. So for s = 0: ε₂-ball = ζ-continuity ball ∩ ball(0,1/2): y in it, y ≠ 0: ζ y ≠ 0 ⟹ y not nontrivial (∈ zeros contra), not −2n (ζ(−2n) = 0 contra), y ≠ 1 (‖y‖ < 1/2), y ≠ 0 (punctured) ⟹ good ✓.\n       s = 1: zetaA ball: y ≠ 1 in it: zetaA y ≠ 0 ⟹ ζ y = zetaA y/(y−1) ≠ 0 ⟹ y not a zero ⟹ not nontrivial, not −2n; y ≠ 0 (|y−1| small) ✓ good.\n       s = −2n: ball(−2n, 1/2): y ≠ −2n: y nontrivial: re y > 0 vs re y < −2n+1/2 ≤ −3/2 ✓ no; y = 0,1 ✓ no; y = −2m: dist ≥ 1... |−2m − (−2n)| = 2|m−n| ≥ 2 for m ≠ n ✓ no ⟹ good ✓.\n       s = ρ₀ nontrivial: isolation ball (5e-iii, avoids other nontrivial zeros) ∩ re-ball (re ∈ (0,1)-strip around ρ₀: radius min(re ρ₀, 1 − re ρ₀)... re ρ₀ ∈ (0,1): r₀ := min (re ρ₀) (1 − re ρ₀) > 0: ball(ρ₀, r₀): re y ∈ (0,1) ⟹ y ≠ 0 (re 0 = 0... y = 0 ⟹ re y = 0 ∉ (0,1) ✓), y ≠ 1 (re 1 = 1 ✓), y ≠ −2n (re ≤ −2 ✓), y ≠ other nontrivial (isolation ✓) ⟹ y ≠ ρ₀ ⟹ good ✓.\n       Then on ball(min ε₁ ε₂): G y = if y = s then (limUnder = W s: Tendsto Fexpr (𝓝[≠]s) (𝓝 (W s)): from punctured agreement + W continuous: Tendsto W (𝓝[≠] s) (𝓝 (W s)) + Fexpr =ᶠ[𝓝[≠]s] W ⟹ Tendsto Fexpr (𝓝[≠]s) (𝓝 (W s)) via Tendsto.congr' (the EventuallyEq symmetric form: h.congr' : f =ᶠ[l] g → Tendsto g ... → Tendsto f ...) ✓ then limUnder = W s by uniqueness ✓) else (y good ⟹ G y = Fexpr y = W y ✓).\n       So: ∀ y ∈ ball(min): G y = W y — by_cases y = s ⟹ EventualEq on the ball ⟹ G =ᶠ[𝓝 s] W (eventually_nhds_iff_ball.mpr) ✓ AnalyticAt.congr (W analytic) ✓.\n     - good: Gentire =ᶠ[𝓝 s] Fexpr: ball of good points (above) ⟹ G y = Fexpr y on it (Gentire_eq_Fexpr) ✓ AnalyticAt.congr (Fexpr_analyticAt_of_not_bad hs) ✓.\n   theorem: ∃ G, (∀ s, AnalyticAt ℂ G s) ∧ ∀ s ∉ bad-set, G s = Fexpr s — package.\n\nHmm — one subtlety in §9-bad-case: \"Gentire =ᶠ[𝓝 s] W\" needs G y = W y for y in a FULL ball including s. At y = s: G s = limUnder (𝓝[≠]s) Fexpr = W s ✓ (uniqueness). ✓.\n\nAnother subtlety: for the punctured Tendsto: Tendsto Fexpr (𝓝[≠] s) (𝓝 (W s)) : from W continuous at s (analytic): Tendsto W (𝓝 s) (𝓝 (W s)) → restrict: Tendsto W (𝓝[≠]s) (𝓝 (W s)) (mono nhdsWithin_le_nhds) → Tendsto.congr' h (this) where h : Fexpr =ᶠ[𝓝[≠] s] W: Tendsto.congr' : f =ᶠ[l] g → (Tendsto g l L → Tendsto f l L)? signature: `Filter.Tendsto.congr' (h : f₁ =ᶠ[l] f₂) (hf : Tendsto f₁ l l') : Tendsto f₂ l l'`?? direction care: I have Tendsto W and want Tendsto Fexpr: h : Fexpr =ᶠ[𝓝[≠]s] W: Tendsto.congr' h : Tendsto Fexpr ... → Tendsto W ...?? wrong direction: use h.symm : W =ᶠ Fexpr: Tendsto.congr' h.symm (tendsto_W) : Tendsto Fexpr ✓. Check: `Filter.Tendsto.congr' (hl : f₁ =ᶠ[l] f₂) (hf : Tendsto f₁ l l₂) : Tendsto f₂ l l₂` — so hl : W =ᶠ Fexpr, hf : Tendsto W ⟹ Tendsto Fexpr ✓ = h.symm.\n\nOK. And §3's unified NF lemma — check the analyticOrderAt_ne_top.mp destructure again from LiSides 371: `obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ)` — so `AnalyticAt.analyticOrderAt_ne_top : ...`: hfh : riemannZeta =ᶠ[𝓝 ρ] fun z => (z − ρ)^analyticOrderNatAt riemannZeta ρ • h z ✓.\n\nzeroMult ρ₀ = analyticOrderNatAt riemannZeta ρ₀ by rfl (LiSides 401 hmz := rfl) ✓ so the NF exponent IS zeroMult ρ₀ ✓.\n\nFor §3's W := logDeriv h analytic at ρ₀: hh.deriv.div hh0 — AnalyticAt.deriv (protected, fun_prop): hh.deriv : AnalyticAt ℂ (deriv h) ρ₀ ✓; AnalyticAt.div (hh.deriv) hh hh0 : AnalyticAt ℂ (fun x => deriv h x / h x) ρ₀ — and logDeriv h = fun x => deriv h x / h x ✓ (logDeriv rfl? logDeriv f x := deriv f x / f x — `logDeriv_apply` is rfl? In LiResidue they used `logDeriv_apply` rewrites; logDeriv f = fun x => deriv f x / f x definitionally — the def: logDeriv f := fun x => deriv f x / f x probably ✓).\n\nThe punctured equality: from LiSides' hld block: for s ∈ 𝓝[≠] ρ₀ with hfh at s (ζ =ᶠ[𝓝 s] the NF), h s ≠ 0, h analytic at s: logDeriv ζ s = m/(s−ρ₀) + logDeriv h s. I'll clone lines 373–397 (the hexp/hld block) adapted.\n\nThen the §3 statement's equality: logDeriv ζ s − m/(s−ρ₀) = logDeriv h s punctured ✓ from hld by sub.\n\nAlright — also §4 needs: logDeriv zetaA analytic at 1: zetaA_analyticAt_one.deriv.div (zetaA_one ▸ ne): `(zetaA_analyticAt_one.deriv).div zetaA_analyticAt_one (by rw [zetaA_one]; norm_num)` ✓.\n\nAnd the punctured identity at 1: for s ≠ 1, zetaA s ≠ 0 (from zetaA_ne_zero_near_one ball), ζ s ≠ 0 (follows: ζ s = zetaA s/(s−1)):\nlogDeriv zetaA s = logDeriv ((·−1)·ζ) s (via zetaA =ᶠ[𝓝 s] (w−1)*ζ w — eventually_eq from zetaA_apply + s ≠ 1 neighborhood... zetaA_apply hz : zetaA z = (z−1)·ζ z for z ≠ 1: at s ≠ 1, eventually (eventually_ne_nhds) ⟹ =ᶠ[𝓝 s] ✓) = logDeriv (·−1) s + logDeriv ζ s (logDeriv_mul: (s−1) ≠ 0, ζ s ≠ 0, differentiables ✓) = 1/(s−1) + logDeriv ζ s (logDeriv of (w−1): deriv = 1: (logDeriv_apply + deriv (w−1) = 1) ✓).\nSo logDeriv ζ s = logDeriv zetaA s − 1/(s−1) ✓ then Fexpr s = W s by ring.\n\nNow — the logDeriv ζ at 0 analyticity: analyticAt_riemannZeta (0 ≠ 1) ✓; ζ 0 = −1/2: `riemannZeta_zero` ✓ (LiDisc used it).\n\nOne more check — `Complex.Gammaℝ_eq_zero_iff` exact form: LiDisc: `rw [Complex.Gammaℝ_eq_zero_iff] at hG; obtain ⟨n, hn⟩ := hG` then `rw [hn]` and computed `ρ.re = -2*(n:ℝ)` — so hn : ρ = -2 * (n : ℂ)?? or ρ = -(2*↑n)? From hre' computation `simp [neg_re, mul_re]` got −2n: the form is likely `ρ = -2 * n` with the cast ↑n. I'll write the classification's third disjunct as `∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ)` and adapt with push_cast as needed.\n\nLet me also double check `badPoint`'s −2n form vs what 5e-v needs: the capstone identity excludes s = −2n for n ≥ 1 — form `s = -2 * (n:ℂ)` fine.\n\nAlso — the Series part at 0: digammaSeriesPart w := ∑' j : ℕ, (1/((j:ℂ)+1) − 1/(w + j + 1)) — matches the digamma_series statement's form `∑' n : ℕ, (1 / ((n : ℂ) + 1) - 1 / (z + n + 1))` ✓ EXACTLY (so the agreement is direct).\n\nWait, careful: digamma_series says `digamma z = −γ − 1/z + ∑' n, (1/(n+1) − 1/(z+n+1))` — so digammaSeriesPart z := ∑' ... and the agreement: digamma z = −γ − 1/z + digammaSeriesPart z — direct rw [digammaSeriesPart] into digamma_series ✓.\n\nSub-series at n: digammaSeriesPartSub (n : ℕ) w := ∑' j, if j = n−1 then 0 else (1/((j:ℂ)+1) − 1/(w+j+1))... for the split at w (w ≠ −n, w in ball): digammaSeriesPart w = digammaSeriesPartSub n w + (1/n − 1/(w+n)):\nterms: full j = sub j + single j pointwise: if j = n−1: full = 1/n − 1/(w+n) = 0 + single ✓; else: full = sub + 0 ✓.\ntsum: ∑' full = ∑' sub + ∑' single: need Summable full at w (from summable_digamma_series — wait that gives Summable of the digamma-series terms at w ∈ integerComplement ✓ — its exact statement: `summable_digamma_series (hz : z ∈ integerComplement) : Summable (fun n => ...)`? presumably the summand form matches ✓) and Summable sub at w (from the ball M-test pointwise: HasSumUniformlyOn on ball(−n,1/2) ⟹ HasSum at w... how to extract: HasSumUniformlyOn f g s with w ∈ s ⟹ HasSum (f · w) (g w)? `HasSumUniformlyOn.hasSum`? or via the TendstoUniformlyOn: pointwise tendsto. There should be `HasSumUniformlyOn.hasSum (h) (hw : w ∈ s)`. Hmm — alternatively prove Summable (sub at w) by comparison with full: ‖sub j‖ ≤ ‖full j‖ pointwise ✓ (if-zero) ⟹ Summable.of_norm_bounded (full summable).norm... ✓ cleaner — reuse seriesTermSub-style. But the M-test is still needed for ANALYTICITY of sub on the ball. For summability at w: comparison ✓. single: summable_of_hasFiniteSupport ✓. tsum congr ✓.\n\nWait, actually — for the M-test on sub-series I need a summable REAL majorant: u j := if j ≥ 2n+1 then 6n/(j+1)² else (anything)... `of_norm_le_summable_eventually` with u j := 6n/(j+1)²: summable (p-series via the LiDigamma summable_div_add_one_sq scaled: Summable fun j => 6n/((j:ℝ)+1)^2 = (summable_div_add_one_sq 1).mul_left (6n)? depends on its exact form — check). And the eventual: for j ≥ 2n+1: ∀ w ∈ ball: ‖sub-term‖ ≤ u j: if j = n−1 (impossible since j ≥ 2n+1 > n−1 for n ≥ 1: 2n+1 > n−1 ⟺ n > −2 ✓): so sub-term = full term: bound as computed ✓.\n\nHmm — j ≥ 2n+1 suffices. u j := 6·n/((j:ℝ)+1)^2: Summable: need `Summable fun j : ℕ => 6*n/((j:ℝ)+1)^2`: from summable_div_add_one_sq: check LiDigamma's exact lemma: `summable_div_add_one_sq 1 : Summable fun m => 1/((m:ℝ)+1)^2`? Let me check.\n\nLet me now check these last names then write the file. Also `HasSumUniformlyOn` pointwise extraction if needed.\n\nGiven the size, let me create the task list and start writing. I'll write the file in pieces and compile iteratively per section (write §0–§2 first, compile; then §3–§4; etc.) — actually more efficient: write the whole file, then fix errors in batches. But risk of cascading errors is higher. Middle ground: two writes.\n\nLet me check summable_div_add_one_sq.","signature":""},{"type":"text","text":"All pieces confirmed. Setting up the 5e-iv tasks and checking the last summability lemma."},{"type":"tool_use","id":"TodoWrite_110","name":"TodoWrite","input":{"todos":[{"content":"LiFEntire §0–§2: Fexpr/badPoint defs, analyticAt_digamma, zero classification","status":"in_progress","activeForm":"Building helpers (digamma analyticAt, classification)"},{"content":"§3–§4: unified logDeriv-NF witness at zeros + s=1 witness","status":"pending","activeForm":"Building zero/one witnesses"},{"content":"§5–§6: digamma series parts (0 and −n) + s=0 and s=−2n witnesses","status":"pending","activeForm":"Building digamma splits"},{"content":"§7–§9: nontrivial-zero witness, generic case, G assembly + capstone","status":"pending","activeForm":"Assembling G entire"},{"content":"Build GREEN + root import + axiom audit","status":"pending","activeForm":"Building and auditing"},{"content":"Session-end protocol (journal-029, STATE, NGUYEN, db, commit)","status":"pending","activeForm":"Closing session 029"}]},"extra_content":null}]