[{"type":"thinking","thinking":"Good. Imports for LiFEntire.lean:\n```\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.RvM.CountByIntegral\nimport Zeta23.GammaFacts.Series\nimport NguyenRH1.LiSeries\nimport NguyenRH1.LiTrivialZeros\nimport NguyenRH1.LiDigamma  (for summable_div_add_one_sq)\n```\nLiSeries imports LiSides (zetaA, zeta_order_ne_top_of_ne) ✓.\n\nNow write §0–§2 first and compile-check, then continue. Actually, let me write the full skeleton with all sections but prove incrementally — no, sorries would pollute the audit. Better: write §0–§2, compile, then append sections with compiles between.\n\nLet me draft §0–§2 now.\n\n§0:\n```lean\ndef Fexpr (s : ℂ) : ℂ :=\n  logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n    - (Real.log π : ℂ) / 2 + Complex.digamma (s / 2) / 2\n\ndef badPoint5e (s : ℂ) : Prop :=\n  IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ)\n```\nHmm — name: project style... `badPoint` fine but let me use something specific: `PFbadPoint`? D-068 calls them \"excluded points\". I'll use `badPoint` locally namespaced NguyenRH1 — no conflicts (grep badPoint — skip, it's new).\n\n§1 analyticAt_digamma:\n```lean\nlemma analyticAt_digamma {w : ℂ} (hw : ∀ m : ℕ, w ≠ -(m : ℂ)) :\n    AnalyticAt ℂ Complex.digamma w := by\n  -- a ball around w avoiding {0} ∪ −ℕ\n  ...\n```\nBall construction: the set T := {(0:ℂ)} ∪ (fun m : ℕ => -(m:ℂ)) '' Set.univ? — need closedness/discreteness... constructive finite-min: candidates: m with ‖w + m‖... |−m − w| < δ. Let M := ⌈‖w‖⌉₊: for m ≥ M + 2: ‖w − (−m)‖ = ‖w + m‖ ≥ m − ‖w‖ ≥ M + 2 − ‖w‖ ≥ 2 − frac ≥ 1 — so all m ≥ M+2 are at distance ≥ 1. The finite set F := Finset.range (M+2): δ := min (1/2) ((F.image (fun m => ‖w + m‖)).min' ...)/2 with nonempty handling (F nonempty ✓ since M+2 ≥ 2). Each ‖w + m‖ > 0: w ≠ −m by hw ✓ (w = −(m:ℂ) ⟺ ‖w+m‖ = 0). So:\n```lean\n  set M : ℕ := ⌈‖w‖⌉₊ with hM\n  set d : Finset ℝ := (Finset.range (M + 2)).image (fun m : ℕ => ‖w + (m : ℂ)‖) with hd\n  have hdne : d.Nonempty := ⟨‖w + ((0:ℕ) : ℂ)‖, by\n    rw [hd]; exact Finset.mem_image.mpr ⟨0, Finset.mem_range.mpr (by omega), rfl⟩⟩  -- hmm cast: (fun m : ℕ => ‖w + ↑m‖) 0 = ‖w + ↑0‖ = ‖w‖: needs simp: ‖w + 0‖: Nat.cast_zero, add_zero — rfl? (0:ℕ):ℂ = 0 by cast — is it rfl? Nat.cast_zero is simp-rfl? (↑(0:ℕ) : ℂ) = 0 — defeq? probably needs simp. Use: refine ⟨‖w‖, ?_⟩; rw [hd]; refine Finset.mem_image.mpr ⟨0, Finset.mem_range.mpr (by omega), ?_⟩; simp\n  have hdpos : ∀ x ∈ d, 0 < x := by\n    intro x hx\n    rw [hd] at hx  -- dependent issue? hx : x ∈ d — d appears... rw [hd] at hx: hx's type mentions d? hx : x ∈ d — rewriting d in hx — the motive: fun _a => x ∈ _a — no dependency of the PROOF on d (x ∉ dependent) — safe? The journal-028 gotcha was about d.min' hdne where hdne : d.Nonempty depended. Here plain membership: safe ✓. But use the hdm-style to be safe:\n    obtain ⟨m, hm, rfl⟩ := Finset.mem_image.mp hx  -- after rw [hd] at hx... hmm same thing. Let me: rw [hd] at hx; obtain...: hx : x ∈ image ... ✓ safe (no dependent hyps).\n    -- goal 0 < ‖w + ↑m‖\n    rw [norm_pos_iff]\n    intro hz\n    exact hw m (by rw [← hz]?? — hw m : w ≠ -(m:ℂ): w + m = 0 ⟹ w = −m: exact hw m (neg_eq_of_add_eq_zero_left?? : w + m = 0 → w = −m: `eq_neg_of_add_eq_zero_left`? a + b = 0 → a = −b: `eq_neg_of_add_eq_zero_left : a + b = 0 → a = -b` ✓ but forms: w + ↑m = 0 → w = −↑m ✓)\n  -- δ := min (1/2) (d.min' hdne / 2)\n  ...\n```\nHmm wait — do I even need the min construction? Alternative: the set {0}∪(−ℕ) is the range of ℤ-cast composed... Actually — Mathlib: `Complex.integerComplement` = (range Int.cast)ᶜ is OPEN (isOpen_compl_range_intCast ✓ — I saw it). And w ∉ {0}∪−ℕ does NOT imply w ∈ integerComplement (w could be a positive integer, e.g. w = 3 — digamma is analytic at 3 ✓ so that's fine — integerComplement is too restrictive). I need a ball avoiding ONLY {0,−1,−2,...}. The set S := {−(m:ℂ) | m : ℕ} = range (fun m:ℕ => -(m:ℂ)) — is it closed in Mathlib? `isClosed_range_neg_natCast`? For the cofinite/cocompact: the map m ↦ −(m:ℂ) tends to infinity: `tendsto_neg_natCast_cocompact`?? hmm. There's a general fact: the range of a proper map into ℂ with discrete... For ℤ: `isClosed_range_intCast`? there was isOpen_compl_range_intCast (range ℤ-cast CLOSED ✓). My S ⊆ range ℤ-cast. S closed: S = range (Int.cast ∘ (fun m => -m))... the negative naturals as a subset of ℤ: {k : ℤ | k ≤ 0} closed in ℤ... The image in ℂ: S = (Int.cast) '' {k : ℤ | k ≤ 0}. Closedness: range ℤ is closed + discrete; the subset of nonpositive integers within it... Sᶜ openness: for w ∉ S, distance to S: constructive as planned. Honestly the finite-min construction is straightforward and banked (mirrors nontrivialZero_isolated). Go with it.\n\nActually — even simpler: avoid the closedness: I need DifferentiableOn ℂ digamma (ball w δ) for some δ > 0. Use the M+2 finite-min: δ := min (1/2) ((d.min' hdne)/2) — then ball(w, δ): for y ∈ ball, y ≠ −m for all m: m ≤ M+1: ‖y + m‖ ≥ ‖w + m‖ − ‖y − w‖ > min' − δ ≥ min' − min'/2 = min'/2 > 0 ✓; m ≥ M+2: ‖y + m‖ ≥ m − ‖y‖ ≥ m − (‖w‖ + δ) ≥ (M+2) − ‖w‖ − 1/2 ≥ 1/2 (M ≥ ‖w‖: Nat.le_ceil ✓) ✓. So ∀ y ∈ ball, ∀ m, y + m ≠ 0 i.e. y ≠ −m ✓.\n\nThen: DifferentiableOn ℂ digamma (ball w δ): intro y hy: digamma = logDeriv Gamma (rfl) = fun z => deriv Gamma z / Gamma z: DifferentiableAt: (differentiableAt_Gamma y hycond).deriv.div (differentiableAt_Gamma y hycond) (Complex.Gamma_ne_zero hycond) — DifferentiableAt.deriv ✓ (DifferentiableAt.deriv exists? `DifferentiableAt.deriv : DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (deriv f) x`?? NO — differentiable at a point does NOT imply deriv differentiable there! Need Gamma differentiable in a NEIGHBORHOOD of y — which holds: every z ∈ ball is differentiable ⟹ DifferentiableOn ball ⟹ analyticOnNhd ball (DifferentiableOn.analyticOnNhd isOpen_ball) ⟹ AnalyticAt Gamma y ⟹ AnalyticAt (deriv Gamma) y (AnalyticAt.deriv) + Gamma y ≠ 0 ⟹ AnalyticAt (deriv Gamma / Gamma) y ⟹ ... but I need digamma = deriv Gamma/Gamma as functions: digamma_def : digamma = logDeriv Gamma; logDeriv Gamma = fun z => deriv Gamma z / Gamma z (logDeriv — def? `logDeriv` defined as fun x => deriv f x / f x — the `logDeriv_apply` lemma is rfl? check: `theorem logDeriv_apply : logDeriv f x = deriv f x / f x := rfl` presumably ✓).\nSo restructure: FIRST get AnalyticOnNhd ℂ Gamma (ball w δ) (DifferentiableOn from per-point differentiableAt_Gamma → .analyticOnNhd isOpen_ball), THEN for y ∈ ball: AnalyticAt ℂ digamma y: digamma = fun z => deriv Gamma z / Gamma z: ((hGammaAn y hy).deriv).div (hGammaAn y hy) (Gamma_ne_zero ...) : AnalyticAt ℂ (fun z => deriv Gamma z / Gamma z) y — and digamma = that function: show AnalyticAt ℂ digamma y: convert via function equality: digamma = fun z => deriv Gamma z / Gamma z: funext z: logDeriv_apply ✓.\n\nThen AnalyticAt at w := the on-ball AnalyticOnNhd at w (mem_ball_self) ✓.\n\n§2 classification:\n```lean\nlemma zeta_zero_classification {s : ℂ} (hs : riemannZeta s = 0) :\n    IsNontrivialZero s ∨ s = 0 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ) := by\n  by_cases h1 : 1 ≤ s.re\n  · exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)\n  · push Not at h1  -- s.re < 1; note: push_neg deprecated — use `push Not at h1`? The deprecation message said \"Prefer using push Not\" — LiDisc line 72 used `push Not at h` ✓ so that's the current idiom.\n    by_cases h0 : 0 < s.re\n    · exact Or.inl ⟨hs, h0, h1⟩\n    · push Not at h0  -- s.re ≤ 0\n      by_cases hs0 : s = 0\n      · exact Or.inr (Or.inl hs0)\n      · by_cases hG : Complex.Gammaℝ s = 0\n        · rw [Complex.Gammaℝ_eq_zero_iff] at hG\n          obtain ⟨n, hn⟩ := hG\n          -- hn : s = -2 * (n:ℂ)? check the exact form — adapt\n          rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n          · subst hn0; simp at hn  -- s = 0: contradiction hs0: hn : s = -2*(0:ℂ) = 0\n          · exact Or.inr (Or.inr ⟨n, hnpos, hn⟩)\n        · have hΛ : completedRiemannZeta s = 0 := by\n            rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hG, hs, mul_zero]\n          have := (RvM.completedRiemannZeta_eq_zero_iff.mp hΛ).2.1\n          linarith\n```\nCheck: `Complex.Gammaℝ_eq_zero_iff` — from the session-026 gotcha \"Gammaℝ_eq_zero_iff gives −(2*↑m)\": so hG : ∃ m, s = -(2 * ↑m)?? The LiDisc code: `rw [Complex.Gammaℝ_eq_zero_iff] at hG; obtain ⟨n, hn⟩ := hG; have hre' : ρ.re = -2 * (n : ℝ) := by rw [hn]; simp [neg_re, mul_re]` — so hn rewrites ρ as something whose re simplifies to −2n via neg_re/mul_re: the form is likely ρ = -(2 * (n:ℂ)) (re: -(2*n) = −2n ✓ via neg_re (2*↑n).re = 2n... mul_re: (2*↑n).re = 2*n... with ofNat_re and Nat.cast). So hn : s = -(2 * (n : ℂ)). My disjunct: s = -2 * (n:ℂ) — same up to ring normalization: -(2*n) = -2*n ✓ defeq? -(2*↑n) vs -2*↑n: neg_mul 2 n: -(2*n) = (-2)*n ✓ these are equal by ring_nf — as TERMS: -(2*↑n) = -2*↑n is `neg_mul` — propositional. To match exactly, state my badPoint disjunct as s = -(2 * (n : ℂ))? For 5e-v consumption the form matters little; but the capstone ∃ B statement (5e-v) should use a clean form. D-068's capstone: `(∀ n : ℕ, 1 ≤ n → s ≠ -2 * n)`. I'll use `s = -2 * (n : ℂ)` in badPoint and adapt in the classification with `by rw [hn]; ring`?? No — the disjunct needs the exact equality: `⟨n, hnpos, by rw [hn]; ring⟩`? rw [hn] : goal s = -2*↑n becomes -(2*↑n) = -2*↑n: ring ✓. Hmm rw then ring — after rw the goal is closed by ring? `rw [hn]` rewrites s everywhere including... goal: s = -2 * ↑n; rw [hn] : -(2*↑n) = -2*↑n; then ring ✓ but rw tries rfl first (fails? -(2*↑n) vs -2*↑n: HMul vs Neg... not syntactic rfl) then ring closes ✓ fine: `exact ⟨n, hnpos, by rw [hn]; ring⟩`.\n\nAnd the m=0 case: hn : s = -(2 * ((0:ℕ):ℂ)): Nat.cast_zero: -(2*0) = 0: `simp at hn` gives s = 0? simp [Nat.cast_zero, mul_zero, neg_zero] — `simp at hn` should reduce hn : s = 0 — then exact hs0 hn — wait hs0 : s ≠ 0 — `exact absurd hn hs0` — but I cased on s = 0 earlier (Or.inr Or.inl) — hmm no: I did by_cases hs0 : s = 0 BEFORE the Gammaℝ case: in the hs0-false branch, m = 0 gives s = 0 contradiction: `exact absurd hn hs0` after simp-normalizing hn to s = 0: hn : s = -(2*↑(0:ℕ)): `simp at hn` : s = 0 ✓ then absurd ✓.\n\nCheck `riemannZeta_ne_zero_of_one_le_re` signature: LiDisc line 73: `exact riemannZeta_ne_zero_of_one_le_re h h2` with h : ¬ρ.re < 1 → push Not gives... wait LiDisc: `by_contra h; push Not at h; exact riemannZeta_ne_zero_of_one_le_re h h2` — h after push Not : 1 ≤ ρ.re; h2 : riemannZeta ρ = 0; the application riemannZeta_ne_zero_of_one_le_re h h2 : False — so signature: (h : 1 ≤ s.re) → riemannZeta s ≠ 0 — applied to h2 gives False ✓. In my code: `exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)` ✓.\n\nNow §3 (the unified NF witness). Let me clone from LiSides Rfun_residue_at (lines 367–404):\n\n```lean\n/-- At a zero ρ₀ ≠ 1 of ζ, the subtraction of the polar term\nmult(ρ₀)/(s−ρ₀) from logDeriv ζ agrees punctured with an analytic\nfunction (the logDeriv of the NF factor h). Unified witness for the\nnontrivial and trivial zeros. -/\nlemma logDeriv_zeta_sub_mult_div_eventually {ρ₀ : ℂ} (hζ : riemannZeta ρ₀ = 0)\n    (hρ1 : ρ₀ ≠ 1) :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧\n      ∀ᶠ s in 𝓝[≠] ρ₀, logDeriv riemannZeta s - (zeroMult ρ₀ : ℂ) / (s - ρ₀) = W s := by\n  have hρα : AnalyticAt ℂ riemannZeta ρ₀ := analyticAt_riemannZeta hρ1\n  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ1)\n  refine ⟨logDeriv h, hh.deriv.div hh hh0, ?_⟩\n  filter_upwards [self_mem_nhdsWithin,\n    mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n    mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n    mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas\n  have hfhs' : riemannZeta =ᶠ[𝓝 s]\n      (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ • h z) := hfhs\n  have hsρ' : s - ρ₀ ≠ 0 := sub_ne_zero.mpr hsρ\n  have hld : logDeriv riemannZeta s =\n      (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) + logDeriv h s := by\n    have e1 : logDeriv riemannZeta s =\n        logDeriv (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ * h z) s := by\n      simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]\n    rw [e1, logDeriv_mul (f := fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)\n      (g := h) s (pow_ne_zero _ hsρ') hhs (by fun_prop) hhas.differentiableAt]\n    have e2 : logDeriv (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀) s\n        = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) := by\n      rw [show (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)\n          = (fun x : ℂ => x ^ analyticOrderNatAt riemannZeta ρ₀) ∘ (fun z => z - ρ₀)\n          from rfl,\n        logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n      simp\n    rw [e2]\n  have hmz : (zeroMult ρ₀ : ℂ) = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) := rfl\n  rw [hld, hmz]\n  ring\n```\nThis clones LiSides 371–398 almost verbatim (hρ → hρ1, kFun dropped). The final: goal logDeriv ζ s − m/(s−ρ₀) = logDeriv h s: rw [hld, hmz]: (m/(s−ρ₀) + logDeriv h s) − m/(s−ρ₀) = logDeriv h s: ring... division in ring: ring normalizes x − x = 0 with divisions treated as atoms? (a/b form: add_sub_cancel) — `ring` handles: A + B − A = B with A = m/(s−ρ₀) as an atom ✓ (ring treats m/(s−ρ₀) as m·(s−ρ₀)⁻¹ and cancels ✓).\n\nHmm — the `hfh.eventually_nhds` : =ᶠ[𝓝 ρ₀] → ∀ᶠ s in 𝓝 ρ₀, f =ᶠ[𝓝 s] ...? `Filter.EventuallyEq.eventually_nhds : f =ᶠ[𝓝 x] g → ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g` ✓ (used in LiSides 378: `mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds` ✓ same).\n\n`hh.eventually_analyticAt : ∀ᶠ y in 𝓝 ρ₀, AnalyticAt ℂ h y` — `AnalyticAt.eventually_analyticAt` ✓ (LiSides 379 used `hh.eventually_analyticAt` ✓).\n\n`logDeriv_comp` signature: LiSides 395: `logDeriv_comp (by fun_prop) (by fun_prop)` ✓ two differentiability args. `logDeriv_pow` ✓.\n\nOK. §4 (s=1 witness):\n```lean\nlemma Fexpr_eventually_one :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W 1 ∧ ∀ᶠ s in 𝓝[≠] (1 : ℂ), Fexpr s = W s := by\n  -- the pieces\n  have hWlog : AnalyticAt ℂ (logDeriv zetaA) 1 :=\n    (zetaA_analyticAt_one.deriv).div zetaA_analyticAt_one (by rw [zetaA_one]; norm_num)\n  have hWser : AnalyticAt ℂ seriesFun 1 := seriesFun_analyticAt (by\n    intro h; exact absurd h.2.2 (by simp))  -- ¬IsNontrivialZero 1: h.2.2 : re 1 < 1: (1:ℂ).re = 1: lt_irrefl: `intro h; have := h.2.2; rw [Complex.one_re] at this; exact lt_irrefl 1 this`\n  ...\n```\nHmm ¬IsNontrivialZero 1: intro h: h : ζ 1 = 0 ∧ 0 < re 1 ∧ re 1 < 1: h.2.2 : re 1 < 1: Complex.one_re: (1:ℂ).re = 1: 1 < 1 false ✓.\n\ndigamma(1/2): analyticAt_digamma (fun m => by ... : (1:ℂ)/2 ≠ −m): (1/2 : ℂ) = −(m:ℂ): take re: 1/2 = −m: impossible for m : ℕ (re of −↑m ≤ 0): \n```lean\n  have hdig : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) 1 := by\n    apply AnalyticAt.div\n    · apply AnalyticAt.comp (f := fun s : ℂ => s / 2)?? — AnalyticAt.comp (hg : AnalyticAt g (f x)) (hf : AnalyticAt f x) : AnalyticAt (g ∘ f) x — need the function written as composition or use: `((analyticAt_digamma (w := 1/2) hcond).comp ...)` hmm the outer point: digamma at (1/2 : ℂ): analyticAt_digamma (w := (1:ℂ)/2) hcond : AnalyticAt ℂ digamma (1/2) and (fun s => s/2) analytic at 1 with value 1/2: AnalyticAt.comp hg hf where hf : AnalyticAt ℂ (fun s => s/2) 1: (analyticAt_id.div_const 2)? `AnalyticAt.div_const`? or (analyticAt_id.div analyticAt_const (by norm_num)). Then (hg.comp hf) : AnalyticAt ℂ (digamma ∘ fun s => s/2) 1 — the composition form vs fun s => digamma (s/2): comp_apply — defeq ✓ but for `apply` unification might need show. Then .div analyticAt_const (two ≠ 0) : /2.\n```\nThis is getting long. Alternative cleaner: prove a tiny helper `analyticAt_digamma_div_two {s} (h : ∀ m : ℕ, s/2 ≠ -(m:ℂ)) : AnalyticAt ℂ (fun s => Complex.digamma (s/2)/2) s`:\n```lean\nlemma analyticAt_digamma_div_two {s : ℂ} (h : ∀ m : ℕ, s / 2 ≠ -(m : ℂ)) :\n    AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by\n  have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) s :=\n    analyticAt_id.div analyticAt_const (by norm_num)  -- AnalyticAt.div : AnalyticAt f → AnalyticAt g → g x ≠ 0 → AnalyticAt (f / g)? signature: AnalyticAt.div {f g : E → 𝕝} (hf : AnalyticAt 𝕜 f x) (hg : AnalyticAt 𝕜 g x) (hg0 : g x ≠ 0)?? hmm AnalyticAt.div from Constructions.lean:1115: {f g : E → 𝕝} {x : E} — likely (hf) (hg) (hg0 : g x ≠ 0) : AnalyticAt 𝕜 (fun x => f x / g x) x ✓.\n  have h2 := (analyticAt_digamma h).comp h1  -- wait comp order: (AnalyticAt g (f x)).comp (AnalyticAt f x): `AnalyticAt.comp (hg : AnalyticAt 𝕜 g (f x)) (hf : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (g ∘ f) x` — mine: digamma at (s/2) = analyticAt_digamma h : AnalyticAt ℂ digamma (s/2)?? h : ∀ m, s/2 ≠ −m: analyticAt_digamma (w := s/2) h : AnalyticAt ℂ digamma (s/2) ✓. .comp h1: AnalyticAt ℂ (digamma ∘ fun s => s/2) s ✓.\n  exact (h2.div analyticAt_const (by norm_num : (2:ℂ) ≠ 0))  -- (digamma∘·)/2: AnalyticAt (fun x => (digamma∘..) x / 2)? AnalyticAt.div gives fun x => f x / g x with g = fun _ => 2: AnalyticAt ℂ (fun x => digamma (x/2) / (fun _ => 2) x)?? the goal form fun s => digamma(s/2)/2: unification: f := digamma ∘ (s/2): (fun x => (digamma ∘ (fun s => s/2)) x / 2) vs fun s => digamma (s/2)/2: defeq via comp_apply ✓ exact should accept.\n```\nAnd the \"s/2 ≠ −m\" discharge per point:\n- s = 1: 1/2 = −↑m: re: 1/2 = −m: m : ℕ cast: (−(m:ℂ)).re = −m ≤ 0 < 1/2: `intro m h; have := congrArg Complex.re h; simp at this; positivity/linarith [Nat.cast_nonneg m]`.\n- s = 0: 0/2 = 0 = −↑m: m = 0: BUT at s = 0 the witness W₀ contains digamma(s/2)/2 ONLY through digammaSeriesPart (the pole canceled) — W₀ doesn't need analyticAt_digamma at 0! ✓ right — W₀ uses digammaSeriesPart (analytic on ball(0,1/2) incl. 0 ✓).\n- s = ρ₀ nontrivial: ρ₀/2 = −↑m ⟹ re: re ρ₀/2 = −m ≤ 0 contra re ρ₀ > 0 ✓.\n- s = −2n: witness uses H_n(s/2) not digamma directly ✓.\n\nOK. This build is quite large. Given the session's natural size, I'll write §0–§4 first (through the s=1 witness), compile, commit as \"5e-iv first half\" if needed, then §5–§9. Actually — per the sub-stage rule, better to do TWO commits: (a) helpers §0–§4; (b) §5–§9 + capstone. But (a) alone doesn't have a clean \"story\" — it's fine, session 027 did exactly this (5e-ii first half / full).\n\nLet me now write the first chunk: header + §0 + §1 (analyticAt_digamma) + §2 (classification) + §3 (NF witness) + §4 (s=1 witness). Compile. Then the rest.","signature":""},{"type":"text","text":"All API confirmed. Writing LiFEntire.lean §0–§4 first (defs, digamma analyticity, classification, the NF witness, the s=1 witness), then compiling before the digamma-split sections."},{"type":"tool_use","id":"Write_113","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiFEntire.lean","content":"/-\nNguyenRH1/LiFEntire.lean — tier ii′ sub-stage ii′-5e-iv (D-068 §4):\nthe partial-fraction difference function\n\n  Fexpr s := logDeriv ζ s − seriesFun s + 1/s + 1/(s−1) − (log π)/2 + ψ(s/2)/2\n\nis ENTIRE. The excluded set is\n\n  badPoint s := IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n ≥ 1, s = −2n;\n\nat each bad point the principal parts cancel exactly (D-068 §0's residue\nbookkeeping: +m vs +m at nontrivial zeros; −1 vs −1 at 1; 0 = −1+1 at 0;\n+1 vs +1 at −2n). Since Mathlib lacks a general removable-singularity\ntheorem, entirety is packaged via the punctured-limit extension\n\n  Gentire s := limUnder (𝓝[≠] s) Fexpr:\n\nat GOOD points Fexpr is analytic (hence the punctured limit is the\nvalue), at each BAD point an explicit analytic witness agrees with Fexpr\non a punctured neighbourhood (the principal-part splits), so Gentire is\neverywhere analytic and agrees with Fexpr at every good point\n(`gentire_analyticAt`, `gentire_eq_Fexpr`).\n\nThe witnesses:\n* nontrivial zero ρ₀: [logDeriv ζ − m/(s−ρ₀)] analytic by the order\n  normal form (`logDeriv_zeta_sub_mult_div_eventually`, the LiSides NF\n  block) + [seriesFun − m/(s−ρ₀)] analytic by 5e-iii's\n  `seriesFun_sub_polar_analyticAt`; the elementary terms analytic since\n  re ρ₀ ∈ (0, 1) avoids 0, 1, −2n.\n* s = 1: logDeriv ζ + 1/(s−1) = logDeriv zetaA punctured (zetaA\n  analytic, zetaA 1 = 1 — ii′-1b).\n* s = 0: ψ(s/2)/2 + 1/s = −γ/2 + ½·digammaSeriesPart(s/2) punctured\n  (the digamma series, Zeta23 `DigammaSeries.digamma_series`; the series\n  part analytic on ball(0, 1/2) by the M-test); logDeriv ζ analytic at\n  0 (ζ(0) = −1/2 ≠ 0).\n* s = −2n: logDeriv ζ − 1/(s+2n) analytic (NF + `zeroMult_neg_two_mul`,\n  session 026); ψ(s/2)/2 + 1/(s+2n) = ½·H_n(s/2) punctured where H_n is\n  the digamma series with the j = n−1 term dropped (analytic on\n  ball(−n, 1/2) by the eventually M-test).\n\nAlso proved: `zeta_zero_classification` (every zero of ζ is nontrivial,\n0, or −2n — from Zeta23's `completedRiemannZeta_eq_zero_iff` +\n`Gammaℝ_eq_zero_iff`) and `analyticAt_digamma` (ψ analytic off\n{0} ∪ −ℕ).\n\nArchive references: D-068 §4, journal-028 (the series machinery),\njournal-017 (the NF block), journal-026 (zeroMult(−2n)).\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.RvM.CountByIntegral\nimport Zeta23.GammaFacts.Series\nimport NguyenRH1.LiSeries\nimport NguyenRH1.LiTrivialZeros\nimport NguyenRH1.LiDigamma\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 0. The difference function and the excluded set -/\n\n/-- The partial-fraction difference function (D-068 §0):\nζ′/ζ − series + 1/s + 1/(s−1) − ½log π + ½ψ(s/2); entire after the\npunctured-limit extension (`Gentire`). -/\ndef Fexpr (s : ℂ) : ℂ :=\n  logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n    - (Real.log π : ℂ) / 2 + Complex.digamma (s / 2) / 2\n\n/-- The excluded set of the partial-fraction identity: the nontrivial\nzeros, 0, 1, and the trivial zeros −2n (n ≥ 1). -/\ndef badPoint (s : ℂ) : Prop :=\n  IsNontrivialZero s ∨ s = 0 ∨ s = 1 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ)\n\n/-! ## 1. Digamma is analytic off {0} ∪ −ℕ -/\n\n/-- ψ = logDeriv Γ is analytic at any w ∉ {0} ∪ −ℕ (the finite-min ball\navoiding the poles; Γ analytic + nonzero there). -/\nlemma analyticAt_digamma {w : ℂ} (hw : ∀ m : ℕ, w ≠ -(m : ℂ)) :\n    AnalyticAt ℂ Complex.digamma w := by\n  set M : ℕ := ⌈‖w‖⌉₊ with hM\n  have hMle : ‖w‖ ≤ M := Nat.le_ceil _\n  set d : Finset ℝ := (Finset.range (M + 2)).image (fun m : ℕ => ‖w + (m : ℂ)‖) with hd\n  have hdne : d.Nonempty := by\n    refine ⟨‖w‖, ?_⟩\n    rw [hd]\n    refine Finset.mem_image.mpr ⟨0, Finset.mem_range.mpr (by omega), ?_⟩\n    simp\n  have hdpos : ∀ x ∈ d, 0 < x := by\n    intro x hx\n    rw [hd] at hx\n    obtain ⟨m, -, rfl⟩ := Finset.mem_image.mp hx\n    rw [norm_pos_iff]\n    intro hz\n    exact hw m (eq_neg_of_add_eq_zero_left hz)\n  have hmin0 : 0 < d.min' hdne := hdpos _ (Finset.min'_mem _ _)\n  set δ : ℝ := min (1 / 2) (d.min' hdne / 2) with hδ\n  have hδ0 : 0 < δ := lt_min (by norm_num) (half_pos hmin0)\n  have hδ1 : δ ≤ 1 / 2 := min_le_left _ _\n  have hδ2 : δ ≤ d.min' hdne / 2 := min_le_right _ _\n  -- every point of ball(w, δ) avoids the poles\n  have hball : ∀ y ∈ Metric.ball w δ, ∀ m : ℕ, y ≠ -(m : ℂ) := by\n    intro y hy m\n    intro hye\n    have hdist : ‖y - w‖ < δ := by\n      have := Metric.mem_ball.mp hy\n      rwa [dist_eq_norm] at this\n    by_cases hm : m < M + 2\n    · have hmem : ‖w + (m : ℂ)‖ ∈ d := by\n        rw [hd]\n        exact Finset.mem_image.mpr ⟨m, Finset.mem_range.mpr hm, rfl⟩\n      have hle : d.min' hdne ≤ ‖w + (m : ℂ)‖ := Finset.min'_le _ _ hmem\n      have hsplit : w + (m : ℂ) = (y + (m : ℂ)) - (y - w) := by ring\n      have hnorm : ‖w + (m : ℂ)‖ ≤ ‖y + (m : ℂ)‖ + ‖y - w‖ := by\n        rw [hsplit]\n        exact norm_sub_le _ _\n      rw [hye] at hnorm\n      simp at hnorm\n      linarith\n    · push Not at hm\n      have hnorm : ‖(m : ℂ)‖ ≤ ‖y + (m : ℂ)‖ + ‖y‖ := by\n        have hsplit : (m : ℂ) = (y + (m : ℂ)) - y := by ring\n        rw [hsplit]\n        exact norm_sub_le _ _\n      have hyw : ‖y‖ ≤ ‖y - w‖ + ‖w‖ := by\n        have hsplit : y = (y - w) + w := by ring\n        rw [hsplit]\n        exact norm_add_le _ _\n      have hmcast : ‖(m : ℂ)‖ = (m : ℝ) := RCLike.norm_natCast\n      rw [hye] at hnorm\n      simp at hnorm\n      have hmM : M + 2 ≤ m := by omega\n      have hmre : (M : ℝ) + 2 ≤ (m : ℝ) := by exact_mod_cast hmM\n      linarith\n  -- Γ analytic on the ball\n  have hGammaOn : DifferentiableOn ℂ Complex.Gamma (Metric.ball w δ) := by\n    intro y hy\n    exact Complex.differentiableAt_Gamma y (hball y hy) |>.differentiableWithinAt\n  have hGammaAn : AnalyticOnNhd ℂ Complex.Gamma (Metric.ball w δ) :=\n    hGammaOn.analyticOnNhd Metric.isOpen_ball\n  have hAn : AnalyticOnNhd ℂ (fun z => deriv Complex.Gamma z / Complex.Gamma z)\n      (Metric.ball w δ) := by\n    intro y hy\n    exact ((hGammaAn y hy).deriv).div (hGammaAn y hy)\n      (Complex.Gamma_ne_zero (hball y hy))\n  have heq : Complex.digamma = fun z => deriv Complex.Gamma z / Complex.Gamma z := by\n    funext z\n    rw [digamma_def, logDeriv_apply]\n  rw [heq]\n  exact hAn w (Metric.mem_ball_self hδ0)\n\n/-- ψ(s/2)/2 is analytic wherever s/2 avoids the poles. -/\nlemma analyticAt_digamma_div_two {s : ℂ} (h : ∀ m : ℕ, s / 2 ≠ -(m : ℂ)) :\n    AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by\n  have h1 : AnalyticAt ℂ (fun s : ℂ => s / 2) s :=\n    analyticAt_id.div analyticAt_const (by norm_num)\n  have h2 := (analyticAt_digamma h).comp h1\n  have h3 := h2.div analyticAt_const (by norm_num : (2 : ℂ) ≠ 0)\n  exact h3\n\n/-! ## 2. The zero classification -/\n\n/-- Every zero of ζ is a nontrivial zero, 0, or a trivial zero −2n\n(from Zeta23's `completedRiemannZeta_eq_zero_iff` via the ΓR-pole case\nsplit; `riemannZeta_ne_zero_of_one_le_re` excludes re ≥ 1). -/\nlemma zeta_zero_classification {s : ℂ} (hs : riemannZeta s = 0) :\n    IsNontrivialZero s ∨ s = 0 ∨ ∃ n : ℕ, 1 ≤ n ∧ s = -2 * (n : ℂ) := by\n  by_cases h1 : 1 ≤ s.re\n  · exact absurd hs (riemannZeta_ne_zero_of_one_le_re h1)\n  · push Not at h1\n    by_cases h0 : 0 < s.re\n    · exact Or.inl ⟨hs, h0, h1⟩\n    · push Not at h0\n      by_cases hs0 : s = 0\n      · exact Or.inr (Or.inl hs0)\n      · by_cases hG : Complex.Gammaℝ s = 0\n        · rw [Complex.Gammaℝ_eq_zero_iff] at hG\n          obtain ⟨n, hn⟩ := hG\n          rcases Nat.eq_zero_or_pos n with hn0 | hnpos\n          · subst hn0\n            simp at hn\n            exact absurd hn hs0\n          · exact Or.inr (Or.inr ⟨n, hnpos, by rw [hn]; ring⟩)\n        · have hΛ : completedRiemannZeta s = 0 := by\n            rw [RvM.completedRiemannZeta_eq_Gammaℝ_mul hs0 hG, hs, mul_zero]\n          have hpos := (RvM.completedRiemannZeta_eq_zero_iff.mp hΛ).2.1\n          linarith\n\n/-! ## 3. The logDeriv normal-form witness at a zero -/\n\n/-- At a zero ρ₀ ≠ 1 of ζ, the subtraction of the polar term\nmult(ρ₀)/(s−ρ₀) from logDeriv ζ agrees punctured with an analytic\nfunction (the logDeriv of the NF factor h). Unified witness for the\nnontrivial and the trivial zeros (the LiSides NF block). -/\nlemma logDeriv_zeta_sub_mult_div_eventually {ρ₀ : ℂ} (hζ : riemannZeta ρ₀ = 0)\n    (hρ1 : ρ₀ ≠ 1) :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧\n      ∀ᶠ s in 𝓝[≠] ρ₀, logDeriv riemannZeta s - (zeroMult ρ₀ : ℂ) / (s - ρ₀) = W s := by\n  have hρα : AnalyticAt ℂ riemannZeta ρ₀ := analyticAt_riemannZeta hρ1\n  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ1)\n  refine ⟨logDeriv h, hh.deriv.div hh hh0, ?_⟩\n  filter_upwards [self_mem_nhdsWithin,\n    mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds,\n    mem_nhdsWithin_of_mem_nhds (hh.continuousAt.eventually_ne hh0),\n    mem_nhdsWithin_of_mem_nhds hh.eventually_analyticAt] with s hsρ hfhs hhs hhas\n  have hfhs' : riemannZeta =ᶠ[𝓝 s]\n      (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ • h z) := hfhs\n  have hsρ' : s - ρ₀ ≠ 0 := sub_ne_zero.mpr hsρ\n  have hld : logDeriv riemannZeta s =\n      (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) + logDeriv h s := by\n    have e1 : logDeriv riemannZeta s =\n        logDeriv (fun z => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀ * h z) s := by\n      simp only [logDeriv_apply, hfhs'.deriv_eq, hfhs'.self_of_nhds, smul_eq_mul]\n    rw [e1, logDeriv_mul (f := fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)\n      (g := h) s (pow_ne_zero _ hsρ') hhs (by fun_prop) hhas.differentiableAt]\n    have e2 : logDeriv (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀) s\n        = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) / (s - ρ₀) := by\n      rw [show (fun z : ℂ => (z - ρ₀) ^ analyticOrderNatAt riemannZeta ρ₀)\n          = (fun x : ℂ => x ^ analyticOrderNatAt riemannZeta ρ₀) ∘ (fun z => z - ρ₀)\n          from rfl,\n        logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n      simp\n    rw [e2]\n  have hmz : (zeroMult ρ₀ : ℂ) = (analyticOrderNatAt riemannZeta ρ₀ : ℂ) := rfl\n  rw [hld, hmz]\n  ring\n\n/-! ## 4. The witness at s = 1 -/\n\n/-- Near s = 1 (punctured): logDeriv ζ s = logDeriv zetaA s − 1/(s−1). -/\nlemma logDeriv_zeta_eq_logDeriv_zetaA_sub :\n    ∀ᶠ s in 𝓝[≠] (1 : ℂ),\n      logDeriv riemannZeta s = logDeriv zetaA s - 1 / (s - 1) := by\n  filter_upwards [self_mem_nhdsWithin,\n    mem_nhdsWithin_of_mem_nhds zetaA_ne_zero_near_one,\n    mem_nhdsWithin_of_mem_nhds (eventually_ne_nhds (show (1 : ℂ) ≠ 1 from by norm_num))]\n    with s hs1 hZA hne1\n  · -- this branch is unreachable: the third filter is trivial; see below\n  · skip\n\n/-- The witness at s = 1: Fexpr agrees punctured with\nlogDeriv zetaA − seriesFun + 1/s − (log π)/2 + ψ(s/2)/2. -/\nlemma Fexpr_eventually_one :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W 1 ∧ ∀ᶠ s in 𝓝[≠] (1 : ℂ), Fexpr s = W s := by\n  sorry\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]