[{"type":"thinking","thinking":"Now §7–§9. Write:\n\n§7: Fexpr_eventually_nontrivial (the nontrivial-zero witness).\n§8: Fexpr_analyticAt_of_not_bad + exists_ball_good_of_not_bad.\n§9: Gentire + gentire_eq_Fexpr + gentire_analyticAt + the capstone exists.\n\n§7 details:\n```lean\n/-! ## 7. The witness at a nontrivial zero -/\n\nlemma Fexpr_eventually_nontrivial {ρ₀ : ℂ} (hρ : IsNontrivialZero ρ₀) :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W ρ₀ ∧ ∀ᶠ s in 𝓝[≠] ρ₀, Fexpr s = W s := by\n  have hρ1 : ρ₀ ≠ 1 := by\n    intro h\n    rw [h] at hρ\n    have hlt := hρ.2.2\n    rw [Complex.one_re] at hlt\n    exact lt_irrefl 1 hlt\n  obtain ⟨W0, hW0, hW0eq⟩ := logDeriv_zeta_sub_mult_div_eventually hρ.1 hρ1\n  -- series minus its polar term, analytic at ρ₀ (5e-iii)\n  have hS : AnalyticAt ℂ (fun s => seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) ρ₀ :=\n    seriesFun_sub_polar_analyticAt ⟨ρ₀, hρ⟩\n  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) ρ₀ := by\n    apply AnalyticAt.div analyticAt_const analyticAt_id (by\n      intro hh\n      rw [hh] at hρ... -- ρ₀ = 0 contra re > 0: hρ.2.1 : 0 < ρ₀.re: rw [hh, Complex.zero_re] at hρ... \n      have hpos := hρ.2.1\n      rw [hh, Complex.zero_re] at hpos\n      exact lt_irrefl 0 hpos)\n  have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) ρ₀ := by\n    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hρ1)\n    exact analyticAt_id.sub analyticAt_const\n  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) ρ₀ := analyticAt_const\n  have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) ρ₀ := by\n    apply analyticAt_digamma_div_two\n    intro m h\n    -- ρ₀/2 = −↑m: re: re ρ₀ / 2 = −m ≤ 0 contra re ρ₀ > 0\n    have hre := congrArg Complex.re h\n    have h1 : (ρ₀ / 2).re = ρ₀.re / 2 := by simp [Complex.div_re, ...]?? — (ρ₀/2).re = ρ₀.re/2: `Complex.div_re`: (a/b).re = (a.re*b.re + a.im*b.im)/(b.re²+b.im²)... messy. Better: from h : ρ₀/2 = −↑m: ρ₀ = −2↑m via linear_combination 2*h — then re: ρ₀.re = −2m ≤ 0 contra hρ.2.1:\n    have h2 : ρ₀ = -2 * (m : ℂ) := by linear_combination 2 * h\n    have h3 : ρ₀.re = -2 * (m : ℝ) := by rw [h2]; simp\n    have h4 : (0 : ℝ) ≤ (m : ℝ) := Nat.cast_nonneg m\n    linarith [hρ.2.1]\n  refine ⟨fun s => W0 s - (seriesFun s - (zeroMult ρ₀ : ℂ) / (s - ρ₀)) + 1 / s + 1 / (s - 1)\n      - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2, ?_, ?_⟩\n  · exact ((((hW0.sub hS).add hC).add hC1).sub hD).add hE\n  · filter_upwards [hW0eq] with s hs\n    -- hs : logDeriv ζ s − m/(s−ρ₀) = W0 s\n    show logDeriv riemannZeta s - seriesFun s + 1/s + 1/(s-1) - c + digamma(s/2)/2\n        = W0 s - (seriesFun s - m/(s-ρ₀)) + 1/s + 1/(s-1) - c + digamma(s/2)/2\n    linear_combination hs\n```\nThe final: from hs : logDeriv ζ s − m/(s−ρ₀) = W0 s: LHS − RHS = (logDerivζ − series) − (W0 − (series − m/(s−ρ₀))) = logDerivζ − W0 − m/(s−ρ₀) = 0 ✓ linear_combination hs ✓ (atoms: m/(s−ρ₀) both sides ✓).\n\nWait — the show RHS: the W lambda applied is a beta-redex `(fun s => ...) s` — show's RHS is the reduced form ✓ defeq ✓.\n\nhS's statement: seriesFun_sub_polar_analyticAt ⟨ρ₀, hρ⟩ : AnalyticAt ℂ (fun s => seriesFun s − (↑(zeroMult ↑(⟨ρ₀, hρ⟩)))/(s − ↑(⟨ρ₀,hρ⟩))) ↑(⟨ρ₀,hρ⟩) — coercions ↑⟨ρ₀,hρ⟩ reduce to ρ₀ definitionally ✓ ascription defeq ✓.\n\n§8:\n```lean\n/-! ## 8. The generic point -/\n\nlemma not_badPoint_of_not_bad {s : ℂ} ... — skip\n\nlemma Fexpr_analyticAt_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :\n    AnalyticAt ℂ Fexpr s := by\n  have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))\n  have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n  have hζ : riemannZeta s ≠ 0 := by\n    intro hz\n    apply hs\n    rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩\n    · exact Or.inl h\n    · exact Or.inr (Or.inl h)\n    · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))\n  have hnontriv : ¬ IsNontrivialZero s := fun h => hs (Or.inl h)\n  have hA : AnalyticAt ℂ (logDeriv riemannZeta) s :=\n    ((analyticAt_riemannZeta hs1).deriv).div (analyticAt_riemannZeta hs1) hζ\n  have hB : AnalyticAt ℂ seriesFun s := seriesFun_analyticAt hnontriv\n  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) s :=\n    analyticAt_const.div analyticAt_id hs0\n  have hC1 : AnalyticAt ℂ (fun s : ℂ => 1 / (s - 1)) s := by\n    apply AnalyticAt.div analyticAt_const (g := fun s : ℂ => s - 1) _ (sub_ne_zero.mpr hs1)\n    exact analyticAt_id.sub analyticAt_const\n  have hD : AnalyticAt ℂ (fun _ : ℂ => (Real.log Real.pi : ℂ) / 2) s := analyticAt_const\n  have hE : AnalyticAt ℂ (fun s => Complex.digamma (s / 2) / 2) s := by\n    apply analyticAt_digamma_div_two\n    intro m h\n    apply hs\n    have h2 : s = -2 * (m : ℂ) := by linear_combination 2 * h\n    rcases Nat.eq_zero_or_pos m with hm0 | hm\n    · subst hm0\n      simp at h2\n      exact Or.inr (Or.inl h2)\n    · exact Or.inr (Or.inr (Or.inr ⟨m, hm, h2⟩))\n  show AnalyticAt ℂ (fun s => logDeriv riemannZeta s - seriesFun s + 1 / s + 1 / (s - 1)\n      - (Real.log Real.pi : ℂ) / 2 + Complex.digamma (s / 2) / 2) s\n  exact ((((hA.sub hB).add hC).add hC1).sub hD).add hE\n```\nCheck the show: Fexpr s unfolds to the lambda applied — defeq ✓.\n\nhC's hg0: analyticAt_id hs0?? — AnalyticAt.div (hf) (hg) (hg0 : g x ≠ 0): g = id: g s = id s — defeq s: hs0 : s ≠ 0 ✓ exact-defeq. But `analyticAt_const.div analyticAt_id hs0` as a TERM with the Pi-div type vs the ascribed lambda — risk (session gotcha). Use apply-form to be safe:\n```lean\n  have hC : AnalyticAt ℂ (fun s : ℂ => 1 / s) s := by\n    apply AnalyticAt.div analyticAt_const analyticAt_id hs0\n```\napply unifies conclusion fun x => f x / g x with fun s => 1/s ✓ hg0 := hs0 : s ≠ 0 vs id s ≠ 0 defeq ✓.\n\nThe m=0 case: h2 : s = -2 * ((0:ℕ):ℂ): simp at h2: Nat.cast_zero, mul_zero, neg_zero: h2 : s = 0 ✓ Or.inr (Or.inl h2) ✓.\n\n§8b the good ball:\n```lean\n/-- Around a good point there is a ball of good points (ζ ≠ 0 ball ∩\navoidance of {0, 1}). -/\nlemma exists_ball_good_of_not_bad {s : ℂ} (hs : ¬ badPoint s) :\n    ∃ δ : ℝ, 0 < δ ∧ ∀ y ∈ Metric.ball s δ, ¬ badPoint y := by\n  have hs0 : s ≠ 0 := fun h => hs (Or.inr (Or.inl h))\n  have hs1 : s ≠ 1 := fun h => hs (Or.inr (Or.inr (Or.inl h)))\n  have hζ : riemannZeta s ≠ 0 := by\n    intro hz\n    apply hs\n    rcases zeta_zero_classification hz with h | h | ⟨n, hn, h⟩\n    · exact Or.inl h\n    · exact Or.inr (Or.inl h)\n    · exact Or.inr (Or.inr (Or.inr ⟨n, hn, h⟩))\n  obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n    ((analyticAt_riemannZeta hs1).continuousAt.eventually_ne hζ)\n  have hs0n : (0 : ℝ) < ‖s‖ := norm_pos_iff.mpr hs0\n  have hs1n : (0 : ℝ) < ‖s - 1‖ := norm_pos_iff.mpr (sub_ne_zero.mpr hs1)\n  refine ⟨min ε₁ (min (‖s‖ / 2) (‖s - 1‖ / 2)), ?_, ?_⟩\n  · positivity  -- min of positives: lt_min hε₁ (lt_min (half_pos hs0n) (half_pos hs1n)): positivity can't use hyps: exact lt_min hε₁ (lt_min (half_pos hs0n) (half_pos hs1n))\n  · intro y hy\n    -- y ≠ 0, y ≠ 1, ζ y ≠ 0\n    have hε₁y : dist y s < ε₁ := lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_left _ _)\n    have hζy : riemannZeta y ≠ 0 := hball₁ y (Metric.mem_ball.mpr hε₁y)\n    have hδs : dist y s < ‖s‖ / 2 := lt_of_lt_of_le (Metric.mem_ball.mp hy)\n      ((min_le_right _ _).trans (min_le_left _ _))\n    have hδ1 : dist y s < ‖s - 1‖ / 2 := lt_of_lt_of_le (Metric.mem_ball.mp hy)\n      ((min_le_right _ _).trans (min_le_right _ _))\n    have hy0 : y ≠ 0 := by\n      intro h\n      rw [h, dist_zero_right] at hδs  -- dist 0 s = ‖s‖: wait dist y s with y = 0: dist 0 s = ‖0 − s‖ = ‖s‖: dist_zero_right : dist 0 s?? dist_eq_norm: dist 0 s = ‖0 − s‖ = ‖−s‖ = ‖s‖: hδs : ‖s‖ < ‖s‖/2 contra: \n      have : (dist (0:ℂ) s) = ‖s‖ := by rw [Complex.dist_eq]; simp\n      rw [h, this] at hδs\n      linarith\n    have hy1 : y ≠ 1 := by\n      intro h\n      rw [h] at hδ1  -- dist 1 s = ‖s − 1‖: dist_eq_norm: ‖1 − s‖ = ‖s−1‖ (norm_sub_rev):\n      have : (dist (1:ℂ) s) = ‖s - 1‖ := by rw [Complex.dist_eq, ← norm_neg]; ring_nf?? ‖1 − s‖ = ‖−(s−1)‖ = ‖s−1‖: rw [Complex.dist_eq]; conv_lhs...: (1 − s) = -(s−1): rw [show (1:ℂ) − s = -(s − 1) by ring, norm_neg] ✓\n      rw [h, this] at hδ1\n      linarith\n    rintro (h | h | h | ⟨n, hn, h⟩)\n    · exact hζy h.1\n    · exact hy0 h\n    · exact hy1 h\n    · rw [h] at hζy\n      exact hζy (riemannZeta_neg_two_mul hn)\n```\n\n§9 G assembly:\n```lean\n/-! ## 9. The entire extension -/\n\n/-- The entire extension of Fexpr: the punctured-limit value. -/\ndef Gentire : ℂ → ℂ := fun s => limUnder (𝓝[≠] s) Fexpr\n\n/-- At a good point, Gentire = Fexpr (continuity ⟹ punctured limit = value). -/\nlemma gentire_eq_Fexpr {s : ℂ} (hs : ¬ badPoint s) : Gentire s = Fexpr s := by\n  haveI := nhdsNE_neBot s\n  have hcont := (Fexpr_analyticAt_of_not_bad hs).continuousAt\n  have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (Fexpr s)) :=\n    hcont.tendsto.mono nhdsWithin_le_nhds\n  exact tendsto_nhds_unique (tendsto_nhds_limUnder ⟨Fexpr s, hlim⟩) hlim\n```\nWait — `ContinuousAt.tendsto`?? ContinuousAt unfolds to Tendsto f (𝓝 s) (𝓝 (f s)) — `hcont : ContinuousAt Fexpr s` — ContinuousAt is DEFINED as Tendsto f (𝓝 s) (𝓝 (f s)) ✓ so hcont is the Tendsto — `hcont.mono nhdsWithin_le_nhds` ✓ (Tendsto.mono (hf : Tendsto f l₁ L) (hl : l₂ ≤ l₁) : Tendsto f l₂ L ✓).\n\ntendsto_nhds_unique (tendsto_nhds_limUnder ⟨Fexpr s, hlim⟩) hlim : first arg : Tendsto Fexpr (𝓝[≠]s) (𝓝 (limUnder (𝓝[≠]s) Fexpr)); second hlim : Tendsto Fexpr (𝓝[≠]s) (𝓝 (Fexpr s)): tendsto_nhds_unique : a = b where first's target = limUnder, second's = Fexpr s: so gives limUnder (𝓝[≠] s) Fexpr = Fexpr s ✓ and Gentire s unfolds to exactly that ✓ — the goal Gentire s = Fexpr s — `show limUnder (𝓝[≠] s) Fexpr = Fexpr s`? defeq unfold of Gentire s ≡ limUnder... ✓ exact accepts.\n\nnhdsNE_neBot : (x : α) → NeBot (𝓝[≠] x) — from Normed/Field/Basic.lean:248 — for α a NontriviallyNormedField? ℂ ✓. Is it an instance? The line said `theorem nhdsNE_neBot` — probably not an instance (name-based). `haveI := nhdsNE_neBot s` ✓. Hmm wait — actually there might be a proper instance `instNeBot...`: Module.punctured_nhds_neBot was an instance-ish. Whatever, haveI works.\n\n```lean\n/-- The local eventual agreement: at a bad point, Gentire agrees (on a\nfull neighborhood) with the analytic witness. -/\nlemma gentire_eventually_eq_witness {s : ℂ} (hbad : badPoint s) :\n    ∃ W : ℂ → ℂ, AnalyticAt ℂ W s ∧ Gentire =ᶠ[𝓝 s] W := by\n  -- the witness from the case split\n  obtain ⟨W, hW, hWeq⟩ : ∃ W, AnalyticAt ℂ W s ∧ ∀ᶠ y in 𝓝[≠] s, Fexpr y = W y := by\n    rcases hbad with h | h | h | ⟨n, hn, h⟩\n    · exact Fexpr_eventually_nontrivial h\n    · subst h; exact Fexpr_eventually_zero\n    · subst h; exact Fexpr_eventually_one\n    · subst h; exact Fexpr_eventually_neg_two_mul hn\n  -- the avoidance ball: every y ≠ s near s is good\n  obtain ⟨δ₂, hδ₂, hgood⟩ : ∃ δ₂ > 0, ∀ y ∈ Metric.ball s δ₂, y ≠ s → ¬ badPoint y := by\n    rcases hbad with h | h | h | ⟨n, hn, h⟩\n    · -- nontrivial ρ₀: isolation ∩ re-strip\n      obtain ⟨δ, hδ, hiso⟩ := nontrivialZero_isolated ⟨s, h⟩\n      -- re strip radius\n      have hr0 : (0 : ℝ) < s.re := h.2.1\n      have hr1 : (0 : ℝ) < 1 - s.re := by linarith [h.2.2]\n      refine ⟨min δ (min s.re (1 - s.re)), lt_min hδ (lt_min hr0 hr1), fun y hy hyne hby => ?_⟩\n      -- re y ∈ (0, 1)\n      have hrey : (0 : ℝ) < y.re ∧ y.re < 1 := by\n        have hd := Metric.mem_ball.mp hy\n        rw [Complex.dist_eq] at hd\n        have hre_le : |y.re - s.re| ≤ ‖y - s‖ := by\n          have : (y - s).re = y.re - s.re := Complex.sub_re\n          rw [← this]\n          exact Complex.abs_re_le_norm _\n        have hlt : ‖y - s‖ < min s.re (1 - s.re) :=\n          lt_of_lt_of_le hd (min_le_right _ _)\n        rcases abs_lt.mp (lt_of_le_of_lt hre_le hlt) with ⟨h1, h2⟩\n        constructor <;> linarith\n      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n      · -- another nontrivial zero: distance ≥ δ contra\n        have hle := hiso ⟨y, hb⟩ (by\n          intro heq\n          apply hyne\n          exact Subtype.ext_iff.mp?? — ⟨y, hb⟩ = ⟨s, h⟩ ⟹ y = s: Subtype.ext_iff: ⟨y,hb⟩ = ⟨s,h⟩ ↔ y = s: `Subtype.ext_iff.mp heq`? heq : (⟨y, hb⟩ : subtype) = ⟨s, h⟩: Subtype.ext_iff.mp heq : y = s?? Subtype.ext_iff : ⟨a, ha⟩ = ⟨b, hb⟩ ↔ a = b ✓: exact hyne (Subtype.ext_iff.mp heq))\n        -- hle : δ ≤ ‖y − s‖; but dist y s < δ (ball, min_left): contra\n        have hd := Metric.mem_ball.mp hy\n        rw [Complex.dist_eq] at hd\n        linarith [lt_of_lt_of_le hd (min_le_left _ _), hle]\n      · rw [hb, Complex.zero_re] at hrey; exact lt_irrefl 0 hrey.1\n      · rw [hb, Complex.one_re] at hrey; exact lt_irrefl 1 hrey.2\n      · -- y = −2m: re = −2m ≤ 0 contra hrey.1\n        have hre : y.re = -2 * (m : ℝ) := by rw [hb]; simp\n        have hm1 : (1 : ℝ) ≤ (m : ℝ) := by exact_mod_cast hm\n        linarith [hrey.1, hre, hm1]\n    · subst h\n      -- s = 0: ball(0, 1/2) ∩ ζ-continuity ball\n      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp\n        ((analyticAt_riemannZeta (by norm_num : (0:ℂ) ≠ 1)).continuousAt.eventually_ne\n          (by rw [riemannZeta_zero]; norm_num))\n      refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩\n      have hy0 : y ≠ 0 := hyne\n      have hε₁y : y ∈ Metric.ball 0 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n      have hζy : riemannZeta y ≠ 0 := hball₁ y hε₁y\n      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n      · exact hζy hb.1\n      · exact hy0 hb\n      · rw [hb] at hy  -- y = 1: dist 1 0 < 1/2 contra\n        have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n        rw [Complex.dist_eq] at hd\n        norm_num at hd  -- ‖1 − 0‖ < 1/2: ‖1‖ = 1: 1 < 1/2 false ✓ norm_num: ‖(1:ℂ) − 0‖ = 1? simp: sub_zero, norm_one: norm_num at hd might reduce to 1 < 1/2 → closes False goal ✓ (norm_num at h with a false hypothesis closes the goal ✓)\n      · exact hζy (hb ▸ riemannZeta_neg_two_mul hm)  -- hb : y = −2m: ζ(−2m) = 0: `hb ▸ ...`? rw [hb] at hζy; exact hζy (riemannZeta_neg_two_mul hm) ✓ cleaner\n    · subst h\n      -- s = 1: zetaA ball\n      obtain ⟨ε₁, hε₁, hball₁⟩ := Metric.eventually_nhds_iff_ball.mp zetaA_ne_zero_near_one\n      refine ⟨min ε₁ (1 / 2), lt_min hε₁ (by norm_num), fun y hy hyne hby => ?_⟩\n      have hε₁y : y ∈ Metric.ball 1 ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n      have hZA : zetaA y ≠ 0 := hball₁ y hε₁y\n      have hy1 : y ≠ 1 := hyne\n      have hζy : riemannZeta y ≠ 0 := by\n        have e := zetaA_apply hy1\n        intro hz\n        rw [hz, mul_zero] at e\n        exact hZA e.symm  -- wait direction: e : zetaA y = (y−1)*0 = 0: hZA e? e.symm : 0 = zetaA y... hZA : zetaA y ≠ 0: hZA e where e : zetaA y = 0 ✓ — after rw [hz, mul_zero] at e: e : zetaA y = 0 ✓ hZA e ✓ (no .symm)\n      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n      · exact hζy hb.1\n      · -- y = 0: dist 0 1 < 1/2 contra\n        rw [hb] at hy\n        have hd := Metric.mem_ball.mp (Metric.ball_subset_ball (min_le_right _ _) hy)\n        rw [Complex.dist_eq] at hd\n        norm_num at hd\n      · exact hy1 hb\n      · rw [hb] at hζy\n        exact hζy (riemannZeta_neg_two_mul hm)\n    · subst h\n      -- s = −2n: ball(−2n, 1/2)\n      refine ⟨1 / 2, by norm_num, fun y hy hyne hby => ?_⟩\n      have hrey : y.re < 0 := by\n        have hd := Metric.mem_ball.mp hy\n        rw [Complex.dist_eq] at hd\n        have hre_le : |y.re - (-2 * (n : ℝ))| ≤ ‖y - -2 * (n : ℂ)‖ := by\n          have h1 : (y - -2 * (n : ℂ)).re = y.re - (-2 * (n : ℝ)) := by\n            simp [Complex.sub_re, Complex.mul_re]  -- hmm (−2↑n).re = −2n: simp [Complex.neg_re, Complex.mul_re, Complex.natCast_re, Complex.ofNat_re]\n          rw [← h1]\n          exact Complex.abs_re_le_norm _\n        have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n        rcases abs_lt.mp (lt_of_le_of_lt hre_le hd) with ⟨h1, h2⟩\n        linarith\n      rcases hby with hb | hb | hb | ⟨m, hm, hb⟩\n      · have hpos := hb.2.1\n        linarith\n      · rw [hb, Complex.zero_re] at hrey; exact lt_irrefl 0 hrey\n      · rw [hb, Complex.one_re] at hrey; exact lt_irrefl 0 hrey  -- hrey : 1 < 0 after rw: (1:ℂ).re = 1: rw [hb] at hrey: hrey : (1:ℂ).re < 0: rw [Complex.one_re] at hrey: 1 < 0 ✓ lt_irrefl 0 hrey?? 1 < 0: `norm_num at hrey` ✓ better\n      · -- y = −2m, y ≠ −2n ⟹ m ≠ n ⟹ |y − (−2n)| ≥ 1 contra dist < 1/2\n        have hd := Metric.mem_ball.mp hy\n        rw [hb, Complex.dist_eq] at hd\n        -- ‖−2m + 2n‖ = 2|m − n| ≥ 2 (m ≠ n)\n        have hmn : m ≠ n := by\n          intro hmn\n          apply hyne\n          rw [hb, hmn]\n        ...\n```\nHmm the −2n case's last sub-case needs |−2m − (−2n)| ≥ 2 > 1/2: ‖(−2↑m) − (−2↑n)‖ = 2|↑m − ↑n|: m ≠ n: |m − n| ≥ 1 (integers): 2·1 = 2 > 1/2 ✓. Chain: (−2↑m) − (−2↑n) = −(2↑m − 2↑n)... = 2(↑n − ↑m): ‖·‖ = 2·‖↑n − ↑m‖: ‖↑n − ↑m‖ = |↑n − ↑m| via... the re-trick again: |(↑n − ↑m).re| ≤ ‖·‖: re = ↑n − ↑m: |↑n − ↑m| ≥ 1 (distinct nats: |↑n − ↑m| = ↑|n − m... in ℝ: |↑n − ↑m| ≥ 1 from m ≠ n: n < m or >: exact_mod_cast with Int... \n\nSimpler: use the factored integerComplement-style: actually simplest: \n```lean\n        have hnorm : (2 : ℝ) ≤ ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ := by\n          have e : (-2 * (m : ℂ)) - -2 * (n : ℂ) = ((2 * ((n : ℝ) - (m : ℝ))) : ℂ) := by\n            push_cast; ring\n          rw [e, RCLike.norm_ofReal]?? — the cast-matching risk again... use abs_re:\n          have h6 : |((-2 * (m : ℂ)) - -2 * (n : ℂ)).re| ≤ ‖(-2 * (m : ℂ)) - -2 * (n : ℂ)‖ :=\n            Complex.abs_re_le_norm _\n          have hre : ((-2 * (m : ℂ)) - -2 * (n : ℂ)).re = 2 * ((n : ℝ) - (m : ℝ)) := by simp\n          rw [hre] at h6\n          have hmn' : (1 : ℝ) ≤ |(n : ℝ) - (m : ℝ)| := by\n            rcases lt_or_gt_of_ne hmn?? — hmn : m ≠ n: lt_or_gt_of_ne hmn : n < m ∨ n > m?? lt_or_gt_of_ne (h : a ≠ b) : a < b ∨ a > b: hmn : m ≠ n gives m < n ∨ m > n: adapt:\n            rcases lt_or_gt_of_ne hmn with hlt | hgt\n            · -- m < n: ↑n − ↑m ≥ 1\n              have : (m : ℝ) + 1 ≤ (n : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hlt\n              rw [abs_of_nonneg (by linarith)]  -- ↑n − ↑m ≥ 0\n              linarith\n            · have : (n : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hgt\n              rw [abs_of_nonpos (by linarith)]\n              linarith\n          rw [abs_mul] at h6?? — h6 : |2·(↑n−↑m)| ≤ ‖·‖: |2·x| = 2|x|: abs_mul: |2*x| = |2|*|x| = 2|x| (abs_ofNat...): \n          rw [abs_mul, abs_ofNat...]?? messy: have h7 : |2 * ((n:ℝ) - (m:ℝ))| = 2 * |(n:ℝ) - (m:ℝ)| := by rw [abs_mul]; norm_num\n          rw [h7] at h6\n          linarith [h6, hmn']\n        linarith [hd, hnorm]\n```\nOK. This is all mechanical. Then the final assembly:\n\n```lean\n  -- hWeq : ∀ᶠ y in 𝓝[≠] s, Fexpr y = W y — ball form:\n  rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff_ball] at hWeq\n  obtain ⟨ε₁, hε₁, hWeq⟩ := hWeq\n  refine ⟨W, hW, ?_⟩\n  -- Gentire =ᶠ[𝓝 s] W: on ball(min ε₁ δ₂): y = s: limUnder = W s; y ≠ s: good ⟹ G y = Fexpr y = W y\n  rw [Metric.eventually_nhds_iff_ball]\n  refine ⟨min ε₁ δ₂, lt_min hε₁ hδ₂, fun y hy => ?_⟩\n  have hε₁y : y ∈ Metric.ball s ε₁ := Metric.ball_subset_ball (min_le_left _ _) hy\n  have hδ₂y : y ∈ Metric.ball s δ₂ := Metric.ball_subset_ball (min_le_right _ _) hy\n  by_cases hye : y = s\n  · subst hye\n    -- Gentire s = W s: limUnder uniqueness\n    haveI := nhdsNE_neBot s\n    have hWcont : Tendsto W (𝓝[≠] s) (𝓝 (W s)) :=\n      hW.continuousAt.mono nhdsWithin_le_nhds  -- ContinuousAt.mono?? hW.continuousAt : ContinuousAt W s = Tendsto W (𝓝 s) (𝓝 (W s)) ✓ .mono nhdsWithin_le_nhds ✓\n    have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (W s)) := hWeq'.symm... — Tendsto.congr' : f₁ =ᶠ f₂ → Tendsto f₁ → Tendsto f₂: I have hWeq : ∀ᶠ, Fexpr y = W y i.e. Fexpr =ᶠ[𝓝[≠]s] W; and Tendsto W: want Tendsto Fexpr: Tendsto.congr' h.symm hWcont?? — Tendsto.congr' (hl : f₁ =ᶠ[l] f₂) (hf : Tendsto f₁ l l₂) : Tendsto f₂ l l₂: so hl := hWeq.symm : W =ᶠ Fexpr, hf := hWcont : Tendsto W: gives Tendsto Fexpr ✓: `hWeq.symm... wait hWeq after the rw is in ball-form — keep the original! Don't rw hWeq; keep it as the EventuallyEq and obtain the ball separately: Filter.Eventually + ball: I need both: the EventuallyEq for the Tendsto.congr' AND the pointwise at y. Keep hWeq as the eventual form; get the pointwise via hWeq.self_of... no — pointwise at y ≠ s in the ball: from the Eventually: (hWeq.filter_mono nhdsWithin_le_nhds)... converts to 𝓝 s — loses the ≠ . Use the ball form for pointwise (after rw) and reconstruct Tendsto via the ball form? Alternative: obtain the ball form FIRST into a separate hypothesis:\n```\nRestructure: keep hWeq (the ∀ᶠ in 𝓝[≠]). For the pointwise at y: `Filter.EventuallyEq` — from hWeq and y ≠ s close to s: (hWeq.eventually_nhds... no: ∀ᶠ in 𝓝[≠] s ⟹ ∃ ball: rw at a COPY: `have hWeqBall := hWeq; rw [...] at hWeqBall; obtain ⟨ε₁, ...⟩ := hWeqBall` — have hWeqBall := hWeq creates a copy ✓ then rw at the copy ✓.\n\nThen:\n```lean\n    have hlim : Tendsto Fexpr (𝓝[≠] s) (𝓝 (W s)) := Tendsto.congr' hWeq.symm hWcont\n    -- hmm: Tendsto.congr' signature: (hl : f₁ =ᶠ[l] f₂) (hf : Tendsto f₁ l l₂) : Tendsto f₂ l l₂ — hWeq.symm : W =ᶠ[𝓝[≠]s] Fexpr; hWcont : Tendsto W (𝓝[≠]s) (𝓝 (W s)) ⟹ Tendsto Fexpr ... ✓\n    show limUnder (𝓝[≠] s) Fexpr = W s\n    exact tendsto_nhds_unique (tendsto_nhds_limUnder ⟨W s, hlim⟩) hlim\n  · -- y ≠ s: good ⟹ G y = Fexpr y; ball ⟹ Fexpr y = W y\n    have hygood : ¬ badPoint y := hgood y hδ₂y hye\n    rw [gentire_eq_Fexpr hygood]  -- goal Gentire y = W y → Fexpr y = W y\n    exact hWeqBallPt y hε₁y hye  -- the pointwise from the ball form: hWeqBall : ∀ y ∈ ball s ε₁, y ∈ {s}ᶜ → Fexpr y = W y: apply: hWeqBall y hε₁y (Set.mem_compl_singleton_iff.mpr hye)\n```\nWait — goal: Gentire y = W y (from the refine's fun y hy => ?_: after rw [Metric.eventually_nhds_iff_ball] the goal is ∀ y ∈ ball s (min...), Gentire y = W y — intro y hy: goal Gentire y = W y). `rw [gentire_eq_Fexpr hygood]` — gentire_eq_Fexpr hygood : Gentire y = Fexpr y: rw rewrites Gentire y → Fexpr y ✓ goal Fexpr y = W y ✓.\n\nAnd the case y = s: goal Gentire s = W s — after subst hye (y := s): show limUnder ... — Gentire s unfolds: `show limUnder (𝓝[≠] s) Fexpr = W s` — Gentire s ≡ limUnder (𝓝[≠] s) Fexpr: defeq ✓ show accepts.\n\nHmm wait — Tendsto.congr' argument order — check: `theorem Filter.Tendsto.congr' {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) (hf : Tendsto f₁ l₁ l₂) : Tendsto f₂ l₁ l₂` ✓.\n\nCapstone:\n```lean\n/-- The ii′-5e-iv capstone: Fexpr extends to an entire function agreeing\nwith it at every good point. -/\ntheorem exists_entire_Gentire :\n    (∀ s : ℂ, AnalyticAt ℂ Gentire s) ∧ ∀ s : ℂ, ¬ badPoint s → Gentire s = Fexpr s := by\n  refine ⟨fun s => ?_, fun s hs => gentire_eq_Fexpr hs⟩\n  by_cases hs : badPoint s\n  · obtain ⟨W, hW, hWeq⟩ := gentire_eventually_eq_witness hs\n    exact hW.congr hWeq  -- AnalyticAt.congr (hf : AnalyticAt f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt g x — hW : AnalyticAt W s; hWeq : Gentire =ᶠ W: need W =ᶠ Gentire: hWeq.symm: exact hW.congr hWeq.symm?? — hWeq : Gentire =ᶠ[𝓝 s] W: AnalyticAt.congr hW hWeq.symm : AnalyticAt Gentire s ✓\n  · exact (Fexpr_analyticAt_of_not_bad hs).congr (Filter.Eventually.of_forall fun y => ?_)  \n    -- need Gentire =ᶠ[𝓝 s] Fexpr: full-nhd agreement on the good ball:\n    obtain ⟨δ, hδ, hgood⟩ := exists_ball_good_of_not_bad hs\n    exact (Fexpr_analyticAt_of_not_bad hs).congr (by\n      rw [Metric.eventually_nhds_iff_ball]\n      exact ⟨δ, hδ, fun y hy => gentire_eq_Fexpr (hgood y hy)⟩)\n```\nCareful with AnalyticAt.congr direction: `AnalyticAt.congr (hf : AnalyticAt 𝕜 f x) (hg : f =ᶠ[𝓝 x] g) : AnalyticAt 𝕜 g x` — so to prove AnalyticAt Gentire s from AnalyticAt W s: need W =ᶠ[𝓝 s] Gentire: hWeq.symm ✓. For the good case: AnalyticAt.congr (Fexpr-analytic) (hg : Fexpr =ᶠ[𝓝 s] Gentire): the ball gives Gentire y = Fexpr y: so hg : Fexpr =ᶠ Gentire: ⟨δ, hδ, fun y hy => (gentire_eq_Fexpr (hgood y hy)).symm⟩ ✓.\n\nAlso note gentire_eq_Fexpr's statement IS Gentire s = Fexpr s ✓ used directly in the second component.\n\nOne more check — `hW.continuousAt` : AnalyticAt.continuousAt ✓ (used in LiResidue). Tendsto.mono: `Filter.Tendsto.mono (hf : Tendsto f l₁ l₂) (hl : l' ≤ l₁) : Tendsto f l' l₂`? name: `Tendsto.mono`? or `tendsto.mono_right`... For shrinking the source filter: `Filter.Tendsto.mono_left : Tendsto f l l' → l'' ≤ l → Tendsto f l'' l'`? Hmm — direction: I have Tendsto W (𝓝 s) ... and want Tendsto W (𝓝[≠] s): source shrink: nhdsWithin_le_nhds : 𝓝[≠] s ≤ 𝓝 s: the lemma: `Tendsto.mono_left (hf : Tendsto f l₁ l₂) (hl : l₂ ≤ l₁)?? names clash with l₂. It's `Filter.Tendsto.mono_left`?? Let me check quickly. Actually in 5e-iii-ish code... I haven't done this yet in the project. Check: `tendsto_nhdsWithin_of_tendsto_nhds`? `Tendsto.mono_left`? grep.","signature":""},{"type":"text","text":"Now §7–§9. Checking the source-filter restriction lemma name first."},{"type":"tool_use","id":"Bash_195","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem Tendsto.mono_left\\|lemma Tendsto.mono_left\\|tendsto_nhdsWithin_of_tendsto_nhds\\b\" Mathlib/Order/Filter/ Mathlib/Topology/ -r --include=*.lean | head -4; grep -rn \"nhdsWithin_le_nhds\" Mathlib/Topology/ -r --include=*.lean | head -2","description":"Source-filter restriction lemma"},"extra_content":null}]