[{"type":"thinking","thinking":"I have everything. Now write LiSides.lean. Structure:\n\n```lean\n/-\nNguyenRH1/LiSides.lean — tier ii′ sub-stage ii′-1b(iii) (D-064 §4 R1):\nthe rectangle residue theorem for the Lagarias-kernel integrand...\n-/\nimport Mathlib\nimport Zeta23.Analytic.RectangleLogDeriv\nimport NguyenRH1.LiPrincipal\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n```\n\nContents:\n\n§1. kFun, Jlag, Rfun defs + differentiability.\n§2. Order facts: zetaA_analyticOnNhd_univ, zeta_order_ne_top_of_ne.\n§3. The interior helper: rectangle_mem_nhds_of_mem_not_border.\n§4. The near-at-1 boundedness:\n  - Ffun def\n  - TaylP def\n  - Ffun_analyticAt_one\n  - TaylP_analyticAt (everywhere)\n  - ppart_mul_pow (s ≠ 1)\n  - Jlag_mul_pow (s ≠ 1, ζ s ≠ 0)\n  - iteratedDeriv_TaylP (i ≤ n): iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1\n  - Ffun_sub_TaylP_order\n  - Rfun_tendsto_one : ∃ L, Tendsto (Rfun n) (𝓝[≠] 1) (𝓝 L)\n  - Rfun_bounded_near_one : (Rfun n) =O[𝓝[≠] 1] 1\n§5. Residue at a zero: Rfun_residue (ρ ≠ 1).\n§6. Main theorem rectInt'_Jlag.\n\nNow, write out all the gory Lean details. Let me be careful about every proof.\n\n**§1 defs:**\n\n```lean\n/-- The kernel factor: kFun n s = (s/(s−1))ⁿ − 1 (= k_n(s−1) with k_n(x) = (1+1/x)ⁿ−1). -/\ndef kFun (n : ℕ) (s : ℂ) : ℂ := (s / (s - 1)) ^ n - 1\n\n/-- The Lagarias-kernel integrand J(w) = k_n(w−1)·(−ζ′/ζ(w)). -/\ndef Jlag (n : ℕ) (s : ℂ) : ℂ := kFun n s * (-(deriv riemannZeta s / riemannZeta s))\n\n/-- The remainder R = J − P (P = principal part at 1). -/\ndef Rfun (n : ℕ) : ℂ → ℂ := Jlag n - ppart n\n```\n\nkFun differentiability at s ≠ 1:\n```lean\nlemma kFun_differentiableAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    DifferentiableAt ℂ (kFun n) s := by\n  have h1d : DifferentiableAt ℂ (fun w : ℂ => w - 1) s :=\n    differentiableAt_id.sub (differentiableAt_const 1)\n  have h2d : DifferentiableAt ℂ (fun w : ℂ => w / (w - 1)) s :=\n    differentiableAt_id.div h1d (sub_ne_zero.mpr hs)\n  exact (h2d.pow n).sub (differentiableAt_const 1)\n```\nNote: kFun n as a function — `kFun n` unfolds to the lambda; differentiableAt_id.div: DifferentiableAt ℂ (fun w => w / (w−1))? differentiableAt_id : DifferentiableAt ℂ (fun w => w) s ✓; .div h1d h : DifferentiableAt ℂ (fun w => w / (w - 1)) — the .div of (fun w => w) and (fun w => w−1) gives (fun w => w) / (fun w => w−1) which is Pi.div — the lambda fun w => w/(w−1) is defeq ✓ (DivisionRing π inst). Should be fine; if fussy, add show/simpa [Pi.div_apply].\n\nJlag differentiability at s ≠ 1, ζ s ≠ 0:\n```lean\nlemma Jlag_differentiableAt {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :\n    DifferentiableAt ℂ (Jlag n) s := by\n  have hζ : AnalyticAt ℂ riemannZeta s := analyticAt_riemannZeta hs1\n  have hd : DifferentiableAt ℂ (fun w : ℂ => -(deriv riemannZeta w / riemannZeta w)) s :=\n    ((hζ.deriv.differentiableAt.div hζ.differentiableAt hs0)).neg\n  exact (kFun_differentiableAt hs1).mul hd\n```\nWait — kFun n s * (…) as Jlag def: Jlag n s = kFun n s * (−(deriv ζ s/ζ s)); DifferentiableAt.mul : DifferentiableAt ℂ f s → DifferentiableAt ℂ g s → DifferentiableAt ℂ (f * g) s — (f * g) s = f s * g s ✓ Pi.mul. Jlag n as a function is fun s => kFun n s * (...) which is defeq to (kFun n) * (fun s => ...) — Pi.mul_apply defeq ✓. Might need `show` to bridge. I'll write `exact (kFun_differentiableAt hs1).mul hd` and hope defeq works; if not, convert.\n\nppart differentiability at s ≠ 1:\n```lean\nlemma ppart_differentiableAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    DifferentiableAt ℂ (ppart n) s := by\n  unfold ppart\n  rw [show (fun w : ℂ => ∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i) =\n    ∑ i ∈ Finset.Icc 1 (n + 1), (fun w : ℂ => Acoeff n i / (w - 1) ^ i) from by\n    funext w; simp [Finset.sum_apply]]\n  apply DifferentiableAt.sum\n  intro i hi\n  exact (differentiableAt_const _).div\n    (((differentiableAt_id.sub (differentiableAt_const 1))).pow i)\n    (pow_ne_zero _ (sub_ne_zero.mpr hs))\n```\n(following Gprim_differentiableAt pattern ✓)\n\nRfun differentiable:\n```lean\nlemma Rfun_differentiableAt {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :\n    DifferentiableAt ℂ (Rfun n) s :=\n  (Jlag_differentiableAt hs1 hs0).sub (ppart_differentiableAt hs1)\n```\nRfun n = Jlag n − ppart n as Pi.sub ✓ defeq; DifferentiableAt.sub gives (fun w => Jlag n w − ppart n w)? No — .sub : DifferentiableAt (f − g) — (f − g) s = f s − g s ✓ = Rfun n s ✓ defeq.\n\n**§2 order facts:**\n\n```lean\nlemma zetaA_analyticOnNhd_univ : AnalyticOnNhd ℂ zetaA Set.univ := by\n  intro s _\n  by_cases hs : s = 1\n  · subst hs; exact zetaA_analyticAt_one\n  · exact zetaA_analyticAt_of_ne hs\n\nlemma zeta_order_ne_top_of_ne {ρ : ℂ} (hρ : ρ ≠ 1) :\n    analyticOrderAt riemannZeta ρ ≠ ⊤ := by\n  have h0 : analyticOrderAt zetaA 1 = 0 :=\n    (zetaA_analyticAt_one.analyticOrderAt_eq_zero).mpr (by rw [zetaA_one]; norm_num)\n  have hA : analyticOrderAt zetaA ρ ≠ ⊤ :=\n    analyticOrderAt_ne_top_of_isPreconnected zetaA_analyticOnNhd_univ\n      isPreconnected_univ (Set.mem_univ 1) (Set.mem_univ ρ) (by rw [h0]; simp)\n  have hcong : zetaA =ᶠ[𝓝 ρ] (fun w : ℂ => (w - 1) * riemannZeta w) := by\n    filter_upwards [eventually_ne_nhds hρ] with w hw using (zetaA_apply hw).symm\n  rw [analyticOrderAt_congr hcong,\n    show (fun w : ℂ => (w - 1) * riemannZeta w) =\n      (fun w : ℂ => w - 1) * riemannZeta from by funext w; simp [Pi.mul_apply],\n    analyticOrderAt_mul (analyticAt_id.sub analyticAt_const) (analyticAt_riemannZeta hρ),\n    ((analyticAt_id.sub analyticAt_const).analyticOrderAt_eq_zero).mpr (sub_ne_zero.mpr hρ),\n    zero_add] at hA\n  exact hA\n```\nCareful: analyticOrderAt_congr signature — `lemma analyticOrderAt_congr (hfg : f =ᶠ[𝓝 z₀] g) : analyticOrderAt f z₀ = analyticOrderAt g z₀` presumably. The rw direction: rw [analyticOrderAt_congr hcong] turns `analyticOrderAt zetaA ρ` into `analyticOrderAt (fun w => (w−1)*ζ w) ρ` ✓.\n\n`analyticOrderAt_mul` — check it's stated for (f * g) Pi.mul: from line 497 `theorem analyticOrderAt_mul (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) : analyticOrderAt (f * g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀` — I saw the proof uses smul internally but the statement at 497... it said `theorem analyticOrderAt_mul (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) :` and got cut. It's probably about f * g. If it turns out to be about `f • g` (smul for 𝕜→E functions)... The context line 250: `obtain ⟨f', ...⟩ := hf.analyticOrderAt_ne_top.1 hf'` inside a proof about smul (analyticOrderAt_smul?). Since E = ℂ = 𝕜 here, smul vs mul — there might be both `analyticOrderAt_smul` and `analyticOrderAt_mul`. I'll check at compile time; use whichever exists.\n\nHmm — (by rw [h0]; simp) for analyticOrderAt zetaA 1 ≠ ⊤: rw [h0] turns goal into (0 : ℕ∞) ≠ ⊤ — simp: `ENat.zero_ne_top`? simp should know (0 ≠ ⊤) via `WithTop.zero_ne_top`/`ENat.zero_ne_top` ✓. Actually `ne_of_eq...` — `simp` handles (0 : ℕ∞) ≠ ⊤ I believe (ENat.zero_ne_top is simp? hopefully). Alternative: `fun h => by simpa using h` — ENat: ⊤ = 0 absurd: exact ENat.top_ne_zero.symm... hmm top_ne_zero : (⊤ : ℕ∞) ≠ 0. So `exact fun h => ENat.top_ne_zero h.symm`? If simp fails I'll adjust. Let me write `(h0.symm ▸ ENat.top_ne_zero)`... messy — h0 : order = 0; goal order ≠ ⊤: `h0 ▸ (show (0:ℕ∞) ≠ ⊤ from by simp)`? Hmm: rw [h0] at * then exact ENat.zero_ne_top? Is there ENat.zero_ne_top? WithTop.zero_ne_top exists? There's `ENat.top_ne_zero : ⊤ ≠ 0` and its symm `ENat.zero_ne_top : 0 ≠ ⊤`? Unclear. Use `by rw [h0]; exact WithTop.zero_ne_top`? Not sure that exists either. Safest: `by rw [h0]; decide`? No — ℕ∞ not DecidableEq-finite... `by simp` is likely fine: simp lemmas `ENat.natCast_ne_top`? (0 : ℕ∞) = ((0:ℕ):ℕ∞) and natCast_ne_top : (n : ℕ∞) ≠ ⊤ exists as simp lemma `ENat.natCast_ne_top` ✓ (I believe: `ENat.natCast_ne_top (n : ℕ) : (↑n : ℕ∞) ≠ ⊤`). And (0:ℕ∞) — is it Nat.cast 0 or OfNat? ℕ∞ has OfNat 0 via...? 0 might be Zero.zero not Nat.cast. simp should still close (0 ≠ ⊤) via WithTop lemmas. I'll write `by rw [h0]; simp` and fix if needed.\n\n**§3 interior helper:**\n\n```lean\nlemma rectangle_mem_nhds_of_mem_not_border {z w p : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)\n    (hmem : p ∈ Rectangle z w) (hb : p ∉ RectangleBorder z w) :\n    Rectangle z w ∈ 𝓝 p := by\n  obtain ⟨h1, h2⟩ := hmem\n  have h1' : z.re ≤ p.re ∧ p.re ≤ w.re := by simpa [uIcc_of_le hre] using h1\n  have h2' : z.im ≤ p.im ∧ p.im ≤ w.im := by simpa [uIcc_of_le him] using h2\n  simp only [RectangleBorder, mem_union, mem_reProdIm, mem_singleton_iff, not_or] at hb\n  obtain ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ := hb\n  rw [rectangle_mem_nhds_iff, mem_reProdIm, uIoo_of_le hre, uIoo_of_le him]\n  refine ⟨⟨lt_of_le_of_ne h1'.1 (fun h => hb2 ⟨h.symm, h2⟩),\n    lt_of_le_of_ne h1'.2 (fun h => hb4 ⟨h, h2⟩)⟩,\n    ⟨lt_of_le_of_ne h2'.1 (fun h => hb1 ⟨h1, h.symm⟩),\n    lt_of_le_of_ne h2'.2 (fun h => hb3 ⟨h1, h⟩)⟩⟩\n```\nCopied from vendored hZint (lines 184–197) with p for ρ. The RectangleBorder union structure: (A ∪ B) ∪ C ∪ D — the not_or destructuring ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩: membership in (((S1 ∪ S2) ∪ S3) ∪ S4)ᶜ — not_or on ((A∪B)∪C)∪D gives (¬((A∪B)∪C) ∧ ¬D), then (¬(A∪B) ∧ ¬C) ∧ ¬D, then ((¬A ∧ ¬B) ∧ ¬C) ∧ ¬D ✓ matches ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ where:\n- hb1 : ¬(p.re ∈ [[z.re,w.re]] ∧ p.im = z.im) — wait, mem_reProdIm for [[z.re,w.re]] ×ℂ {z.im}: p ∈ it ⟺ p.re ∈ [[z.re,w.re]] ∧ p.im ∈ {z.im} — mem_singleton_iff makes it p.im = z.im. Hmm but the vendored code uses hb1 ⟨h1, h.symm⟩ where h : p.im = z.im... wait vendored: `lt_of_le_of_ne h2'.1 (fun h => hb1 ⟨h1, h.symm⟩)` — h : z.im = p.im? lt_of_le_of_ne h2'.1 : z.im < p.im needs z.im ≠ p.im; the function given: fun h => hb1 ⟨h1, h.symm⟩ with h : z.im = p.im, h.symm : p.im = z.im, ⟨h1, h.symm⟩ : p.re ∈ _ ∧ p.im = z.im ✓ contradicts hb1 (left side = reProdIm [[z.re,w.re]] {z.im}) ✓. And mem_reProdIm: p ∈ s ×ℂ t ↔ p.re ∈ s ∧ p.im ∈ t — with t = {z.im}: p.im ∈ {z.im} — after mem_singleton_iff: p.im = z.im ✓.\n\nSo the four components:\n- hb1 : ¬(p.re ∈ uIcc ∧ p.im = z.im) — bottom side [[z.re,w.re]] ×ℂ {z.im}\n- hb2 : ¬(p.re = z.re ∧ p.im ∈ uIcc) — left side {z.re} ×ℂ [[z.im,w.im]]\n- hb3 : ¬(p.re ∈ uIcc ∧ p.im = w.im) — top side\n- hb4 : ¬(p.re = w.re ∧ p.im ∈ uIcc) — right side\n\nVendored:\n```\nrefine ⟨⟨lt_of_le_of_ne h1'.1 (fun h => hb2 ⟨h.symm, h2⟩),\n  lt_of_le_of_ne h1'.2 (fun h => hb4 ⟨h, h2⟩)⟩,\n  ⟨lt_of_le_of_ne h2'.1 (fun h => hb1 ⟨h1, h.symm⟩),\n  lt_of_le_of_ne h2'.2 (fun h => hb3 ⟨h1, h⟩)⟩⟩\n```\n- z.re < p.re: from z.re ≤ p.re and z.re ≠ p.re; fun h : z.re = p.re => hb2 ⟨h.symm : p.re = z.re, h2 : p.im ∈ uIcc⟩ ✓\n- p.re < w.re: fun h : p.re = w.re => hb4 ⟨h, h2⟩ ✓\n- z.im < p.im: fun h : z.im = p.im => hb1 ⟨h1, h.symm⟩ ✓\n- p.im < w.im: fun h : p.im = w.im => hb3 ⟨h1, h⟩ ✓\n✓ copy verbatim.\n\nNote the union order in the def: [[z.re,w.re]] ×ℂ {z.im} ∪ {z.re} ×ℂ [[z.im,w.im]] ∪ [[z.re,w.re]] ×ℂ {w.im} ∪ {w.re} ×ℂ [[z.im,w.im]] — parses as ((S1 ∪ S2) ∪ S3) ∪ S4 ✓ destructuring matches.\n\nAlso — the simp only needs `mem_reProdIm` — vendored had `mem_reProdIm` in scope (open Complex? Set?). It's `Complex.mem_reProdIm`? or just mem_reProdIm with open Complex ✓ (we have open Complex).\n\nWait — h1 : p.re ∈ [[z.re, w.re]] — [[ ]] is uIcc notation. hmem : p ∈ Rectangle z w = uIcc re ×ℂ uIcc im — obtain ⟨h1, h2⟩ := hmem via mem_reProdIm defeq ✓ (vendored did obtain directly from hρR : ρ ∈ Rectangle — since Rectangle is def'd as the reProdIm, membership is defeq to the pair ✓).\n\n**§4 near-at-1.**\n\n```lean\n/-- F(w) = (wⁿ−(w−1)ⁿ)·hLi(w) — the analytic-at-1 numerator (w−1)^{n+1}·J. -/\ndef Ffun (n : ℕ) (w : ℂ) : ℂ := (w ^ n - (w - 1) ^ n) * hLi w\n```\nBridge: Acoeff n i = iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i)! — by rfl? Acoeff's def uses the lambda `fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w` — Ffun n is a def equal to that lambda; iteratedDeriv (Ffun n) vs iteratedDeriv (fun w => ...) — reducible? def Ffun is not irreducible by default, so iteratedDeriv (k) (Ffun n) 1 should unify with iteratedDeriv k (fun w => ...) 1 up to delta — `rfl` might fail if Lean doesn't unfold; `show` with unfold Ffun works. I'll add `lemma Acoeff_eq (n i : ℕ) : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i)! := rfl` — if rfl fails, `by unfold Ffun; rfl` or `by rw [Ffun]`. Actually since I can't edit LiPrincipal (freeze — wait, can I add to LiPrincipal? Freeze says no edits to EXISTING PROOFS except liCoeff fix. Adding new lemmas to existing files — session 016 added LiPrincipal.lean as a new file. The freeze: \"no edits to existing Lean proofs except the liCoeff correctness fix (ii′-1a)\". Adding a NEW file LiSides.lean is safest. All new lemmas go in LiSides.lean.)\n\n```lean\n/-- The order-n Taylor polynomial of Ffun n at 1. -/\ndef TaylP (n : ℕ) (w : ℂ) : ℂ :=\n  ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j\n```\n\nFfun analytic at 1:\n```lean\nlemma Ffun_analyticAt_one (n : ℕ) : AnalyticAt ℂ (Ffun n) 1 :=\n  ((analyticAt_id.pow n).sub ((analyticAt_id.sub analyticAt_const).pow n)).mul\n    hLi_analyticAt_one\n```\nCareful: Ffun n as function = fun w => (w^n − (w−1)^n) * hLi w — the .mul gives Pi.mul of the two lambdas: (fun w => w^n − (w−1)^n) * hLi applied at w = (w^n−(w−1)^n) * hLi w ✓ defeq. Should elaborate; else `show AnalyticAt ℂ (fun w : ℂ => _) 1`.\n\nThe .sub of analyticAt_id.pow n : AnalyticAt ℂ (fun w => w^n) 1... analyticAt_id.pow n : AnalyticAt ℂ (fun w => w)^n — (fun w => w)^n vs fun w => w^n — Pi.pow_apply defeq ✓ (this pattern worked in LiResidue's ResW1_eq_sum hA via contDiff; for analyticAt similar defeq should hold — A_iter used contDiff_id.pow; here analyticAt_id.pow n gives AnalyticAt (id^n)... id vs fun w => w defeq ✓).\n\nTaylP analytic everywhere:\n```lean\nlemma TaylP_analyticAt (n : ℕ) (w : ℂ) : AnalyticAt ℂ (TaylP n) w := by\n  unfold TaylP\n  rw [show (fun w : ℂ => ∑ j ∈ Finset.range (n + 1),\n      (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) =\n    ∑ j ∈ Finset.range (n + 1),\n      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) from by\n    funext w; simp [Finset.sum_apply]]\n  apply AnalyticAt.sum  -- does this exist?\n  intro j hj\n  exact analyticAt_const.mul (((analyticAt_id.sub analyticAt_const)).pow j)\n```\n`AnalyticAt.sum` — hmm, does it exist? There's `AnalyticAt.sum : (∀ i ∈ s, AnalyticAt 𝕜 (f i) x) → AnalyticAt 𝕜 (∑ i ∈ s, f i) x`? I think `AnalyticAt.sum` exists (Mathlib has AnalyticAt.sum? Let me think — there is `AnalyticAt.sum` in Mathlib.Analysis.Analytic.Constructions? I recall `AnalyticAt.sum` exists for finite sums ✓. If not, Finset.induction with analyticAt_const/add.) I'll try AnalyticAt.sum; fallback induction.\n\nppart_mul_pow:\n```lean\nlemma ppart_mul_pow {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    (s - 1) ^ (n + 1) * ppart n s = TaylP n s := by\n  have hs1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs\n  rw [ppart, Finset.mul_sum]\n  rw [show (∑ i ∈ Finset.Icc 1 (n + 1), (s - 1) ^ (n + 1) * (Acoeff n i / (s - 1) ^ i)) =\n    ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (s - 1) ^ j from ?_]\n  · rfl  -- TaylP unfolds\n  apply Finset.sum_bij (fun i _ => n + 1 - i)\n  · intro i hi; rw [Finset.mem_Icc] at hi; rw [Finset.mem_range]; omega\n  · intro a₁ ha₁ a₂ ha₂ h; rw [Finset.mem_Icc] at ha₁ ha₂; omega\n  · intro j hj; rw [Finset.mem_range] at hj\n    exact ⟨n + 1 - j, by rw [Finset.mem_Icc]; omega, by omega⟩\n  · intro i hi\n    rw [Finset.mem_Icc] at hi\n    -- term identity\n    have hpow : (s - 1) ^ (n + 1) * (Acoeff n i / (s - 1) ^ i) =\n        Acoeff n i * (s - 1) ^ (n + 1 - i) := by\n      rw [pow_sub₀ (s - 1) hs1 (by omega : i ≤ n + 1)]\n      field_simp [hs1]\n      ring  -- may need massaging\n    rw [hpow]\n    -- Acoeff n i with j = n+1−i: Acoeff n (n+1−j) = iteratedDeriv j Ffun 1 / j!\n    congr 1\n    · -- Acoeff n i = iteratedDeriv (n+1−i) (Ffun n) 1 / (n+1−i)! — rfl by def\n      rfl? \n    · -- exponent: n + 1 - i = j where j = n + 1 - i — rfl\n```\nHmm wait — in sum_bij, the target sum is over j ∈ range(n+1) with summand (iteratedDeriv j Ffun 1/j!)·(s−1)^j, and the map is i ↦ n+1−i. The term-identity goal: (s−1)^{n+1}·(Acoeff n i/(s−1)^i) = (iteratedDeriv (n+1−i) Ffun 1/(n+1−i)!)·(s−1)^{n+1−i}. Since Acoeff n i is DEFINED as exactly iteratedDeriv (n+1−i) (fun w => ...) 1 /(n+1−i)! and Ffun n is defeq that lambda — the Acoeff vs Ffun bridge: `Acoeff n i` unfolds to `iteratedDeriv (n+1−i) (fun w => (w^n−(w−1)^n)*hLi w) 1 / (n+1−i)!`; the target has `iteratedDeriv (n+1−i) (Ffun n) 1`. Are these syntactically equal after `unfold Acoeff`/`show`? delta-unfold Ffun gives the lambda ✓ defeq, and rw/match should work with `show` or `simp only [Acoeff, Ffun]`. I'll write the term identity as:\n```\n    have hA : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i)! := rfl\n```\nIf rfl fails due to reducibility, use `by simp only [Acoeff, Ffun]` — simp only with the defs unfolds (delta) ✓. Actually `Acoeff` is a def — `simp only [Acoeff]` unfolds via equation lemma? For a plain def, simp only [Acoeff] uses the auto-generated equation lemma Acoeff.eq_def or unfolds — `simp only [Acoeff]` works for defs (uses the definitional equation). Then both sides identical ✓. Let me preemptively structure: prove `Acoeff_eq : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i)!` by `rfl` — likely works since def Ffun's delta is semi-reducible... elaboration of `rfl : Acoeff n i = ...` requires defeq of the two sides — delta-unfold Acoeff: RHS lambda vs Ffun — delta-unfold Ffun — identical ✓. `rfl` proves defeq props with default transparency ✓ should work.\n\nFor the pow algebra: (s−1)^{n+1}·(A/(s−1)^i) = A·(s−1)^{n+1−i}:\n(s−1)^{n+1}/(s−1)^i = (s−1)^{n+1−i}: pow_sub₀ (s−1) hs1 (i ≤ n+1) : (s−1)^{n+1−i} = (s−1)^{n+1}·((s−1)^i)⁻¹. So:\n```\n      rw [pow_sub₀ (s - 1) hs1 hi.2]  -- hmm pow_sub₀ : a^(m−n) = a^m * (a^n)⁻¹\n      field_simp [hs1]\n```\nGoal: (s−1)^{n+1}·(A/(s−1)^i) = A·((s−1)^{n+1}·((s−1)^i)⁻¹). field_simp then ring. Or simpler:\n```\n    have hpow : (s - 1) ^ (n + 1) * (Acoeff n i / (s - 1) ^ i) =\n        Acoeff n i * (s - 1) ^ (n + 1 - i) := by\n      have e : (s - 1) ^ (n + 1) = (s - 1) ^ i * (s - 1) ^ (n + 1 - i) := by\n        rw [← pow_add]; congr 1; omega\n      rw [e]\n      field_simp [hs1, pow_ne_zero i hs1]\n      ring\n```\ne via pow_add: (s−1)^i·(s−1)^{n+1−i} = (s−1)^{i+(n+1−i)} = (s−1)^{n+1} (i + (n+1−i) = n+1 since i ≤ n+1 ✓ omega). Then (X^i·X^{n+1−i})·(A/X^i) = A·X^{n+1−i}: field_simp with X^i ≠ 0, then ring. ✓\n\nJlag_mul_pow:\n```lean\nlemma Jlag_mul_pow {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :\n    (s - 1) ^ (n + 1) * Jlag n s = Ffun n s := by\n  have h1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs1\n  rw [Jlag, kFun, hLi_eq_of_ne hs1 hs0]  -- hmm hLi_eq_of_ne : hLi w = (w−1)·(−ζ′/ζ)\n  -- goal: (s−1)^{n+1} * (((s/(s−1))^n − 1) * (−(ζ′ s/ζ s))) = (s^n − (s−1)^n) * ((s−1)·(−ζ′ s/ζ s))\n  field_simp [h1, hs0, pow_ne_zero n h1]\n  -- remaining polynomial identity\n  ring\n```\nCareful: Ffun n s = (s^n − (s−1)^n) * hLi s; after rw [hLi_eq_of_ne hs1 hs0] — wait, rw works on the goal: goal RHS contains `hLi s` (via Ffun) — rw replaces hLi s with the RHS form ✓ if Ffun is unfolded first: Ffun is a def — rw [Ffun]? Hmm: the goal is `(s-1)^(n+1) * Jlag n s = Ffun n s`. rw [Jlag, kFun] unfolds Jlag/kFun in goal ✓ (rw with def names uses equation lemmas — for simple defs `rw [Jlag]` works if equation lemma generated: Jlag.eq_... For non-recursive defs, `rw [Jlag]` should work via `Jlag.eq_def`? In Lean4 Mathlib, `rw [Jlag]` works when there's an equation lemma; for plain defs it usually does (auto-generated). Alternative: `unfold Jlag kFun Ffun` or `simp only [Jlag, kFun, Ffun]` — simp only unfolds defs reliably. Use `simp only [Jlag, kFun, Ffun, hLi_eq_of_ne hs1 hs0]`? simp only with a conditional lemma needs the hyps discharged — provide them: simp only [..., hLi_eq_of_ne hs1 hs0] uses the instantiated lemma ✓. But hLi_eq_of_ne RHS contains −(deriv ζ s/ζ s) while LHS of goal (Jlag unfolded) has `-(deriv riemannZeta s / riemannZeta s)` — the negation placement: Jlag: `kFun n s * (-(deriv riemannZeta s / riemannZeta s))`; hLi_eq_of_ne: hLi w = (w−1) * (-(deriv riemannZeta w)/riemannZeta w) — SAME subterm ✓. Then goal: (s−1)^{n+1}·(((s/(s−1))^n − 1)·X) = (s^n−(s−1)^n)·((s−1)·X) where X = −(deriv ζ s/ζ s). field_simp [h1, hs0, pow_ne_zero] then ring. Hmm — X involves division by ζ s: field_simp [hs0] clears it: multiply both sides... Let me instead prove via explicit steps to be safe:\n\n```lean\nlemma Jlag_mul_pow {n : ℕ} {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) :\n    (s - 1) ^ (n + 1) * Jlag n s = Ffun n s := by\n  have h1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs1\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    simp only [kFun]\n    rw [div_pow]\n    field_simp [pow_ne_zero n h1]\n  calc (s - 1) ^ (n + 1) * Jlag n s\n      = (s - 1) ^ (n + 1) * ((s ^ n - (s - 1) ^ n) / (s - 1) ^ n) *\n          (-(deriv riemannZeta s / riemannZeta s)) := by rw [Jlag, hk]; ring\n    _ = (s - 1) * (s ^ n - (s - 1) ^ n) * (-(deriv riemannZeta s / riemannZeta s)) := by\n        rw [pow_succ]  -- (s−1)^{n+1} = (s−1)^n·(s−1)? pow_succ : a^{n+1} = a^n * a ✓\n        field_simp [pow_ne_zero n h1]\n        ring\n    _ = (s ^ n - (s - 1) ^ n) * hLi s := by\n        rw [hLi_eq_of_ne hs1 hs0]; ring\n    _ = Ffun n s := rfl\n```\nhk: (s/(s−1))^n − 1 = (s^n − (s−1)^n)/(s−1)^n: div_pow: (s/(s−1))^n = s^n/(s−1)^n; then s^n/(s−1)^n − 1 = (s^n − (s−1)^n)/(s−1)^n: field_simp [pow_ne_zero n h1] closes (both sides: a/c − 1 = (a−c)/c ✓ field_simp should handle; may need `ring` after).\n\nSecond step: (s−1)^{n+1}·(X/(s−1)^n)·Y = (s−1)·X·Y: pow_succ rewrites (s−1)^(n+1) = (s−1)^n·(s−1) — then (s−1)^n·(s−1)·(X/(s−1)^n)·Y: field_simp [pow_ne_zero n h1] + ring ✓.\n\nThird: (s−1)·X·Y = X·((s−1)·Y) ring where Y = −(deriv ζ/ζ): rw [hLi_eq_of_ne hs1 hs0] rewrites hLi s on... wait the goal at that point: (s−1)·(s^n−(s−1)^n)·(−(deriv ζ s/ζ s)) = (s^n−(s−1)^n)·hLi s. rw [hLi_eq_of_ne hs1 hs0] — rewrites occurrences of hLi s in the GOAL — RHS has hLi s ✓ → RHS becomes (s^n−(s−1)^n)·((s−1)·(−(deriv ζ s/ζ s))) then ring ✓.\n\nRfun eventually-eq near 1:\n```lean\nlemma Rfun_eq_sub_div_near_one (n : ℕ) :\n    ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = (Ffun n s - TaylP n s) / (s - 1) ^ (n + 1) := by\n  have hne : ∀ᶠ s in 𝓝[≠] (1 : ℂ), riemannZeta s ≠ 0 := by\n    have h := riemannZeta_residue_one.eventually_ne (show (1 : ℂ) ≠ 0 by norm_num)\n    filter_upwards [h] with w hw\n    have h2 := hw\n    simp only [ne_eq, mul_eq_zero] at h2\n    push Not at h2\n    exact h2.2\n  filter_upwards [hne, self_mem_nhdsWithin] with s hs0 hs1\n  have hs1' : s ≠ 1 := by simpa using hs1\n  have e1 := Jlag_mul_pow hs1' hs0\n  have e2 := ppart_mul_pow hs1'\n  have h1 : (s - 1) ^ (n + 1) ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hs1')\n  -- Rfun n s = Jlag n s − ppart n s\n  have e : (s - 1) ^ (n + 1) * Rfun n s = Ffun n s - TaylP n s := by\n    rw [Rfun, Pi.sub_apply, mul_sub, e1, e2]\n  rw [eq_div_iff_mul_eq h1 |>.mpr e.symm?]...\n```\nHmm: goal Rfun n s = (Ffun − TaylP)/(s−1)^{n+1}: from (s−1)^{n+1}·Rfun = F−T: `eq_div_of_mul_eq`? The pattern: `eq_div_of_mul_eq (hc : c ≠ 0) (h : a * c = b) : a = b / c`. We have (s−1)^{n+1}·Rfun = F−T — that's c·a = b form; need a·c = b: mul_comm. So: `exact eq_div_of_mul_eq h1 (by rw [mul_comm]; exact e)` — check signature: eq_div_of_mul_eq : c ≠ 0 → a * c = b → a = b / c ✓ (used in LiPrincipal line 129: eq_div_of_mul_eq Complex.I_ne_zero (by rw [mul_comm]; exact h6) ✓ same pattern).\n\nAlso Rfun n s unfolding: Rfun n = Jlag n − ppart n (Pi.sub); Rfun n s = Jlag n s − ppart n s via Pi.sub_apply ✓ (session-016 note: simp [Pi.sub_apply] after .sub — rw [Rfun, Pi.sub_apply] should work: Rfun is def — rw [Rfun] needs equation lemma; `simp only [Rfun, Pi.sub_apply]` safer. Actually rw [show Rfun n s = Jlag n s − ppart n s from rfl] — defeq rfl ✓ cleanest.\n\nThe e step: (s−1)^{n+1}·(Jlag n s − ppart n s) = (s−1)^{n+1}·Jlag − (s−1)^{n+1}·ppart = Ffun − TaylP via mul_sub + e1 + e2 ✓.\n\nOrder of Ffun − TaylP:\n```lean\nlemma Ffun_sub_TaylP_iteratedDeriv (n i : ℕ) (hi : i ≤ n) :\n    iteratedDeriv i (Ffun n - TaylP n) 1 = 0 := by\n  have hF : ContDiffAt ℂ i (Ffun n) 1 := (Ffun_analyticAt_one n).contDiffAt\n  have hT : ContDiffAt ℂ i (TaylP n) 1 := (TaylP_analyticAt n 1).contDiffAt\n  rw [iteratedDeriv_sub hF hT]\n  -- iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1\n  rw [iteratedDeriv_TaylP hi]  -- below\n  simp\n```\nHmm — iteratedDeriv_sub: needs both ContDiffAt ✓ gives iteratedDeriv i (f−g) = iteratedDeriv i f − iteratedDeriv i g ✓ (used in A_iter ✓). Then show the TaylP deriv equals Ffun's:\n\n```lean\nlemma iteratedDeriv_TaylP {n i : ℕ} (hi : i ≤ n) :\n    iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1 := by\n  unfold TaylP\n  rw [show (fun w : ℂ => ∑ j ∈ Finset.range (n + 1),\n      (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) =\n    ∑ j ∈ Finset.range (n + 1),\n      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) from by\n    funext w; simp [Finset.sum_apply]]\n  rw [iteratedDeriv_sum (fun j hj => ?_)]\n  · -- Σ_j c_j · iteratedDeriv i ((w−1)^j) 1 = iteratedDeriv i Ffun 1\n    rw [Finset.sum_eq_single i]\n    · -- the i-th term: c_i · i! = iteratedDeriv i Ffun 1\n      have hdesc : iteratedDeriv i (fun w : ℂ => (w - 1) ^ i) (1 : ℂ) = i ! := ...\n      ...\n    · intro j hj hji\n      -- j ≠ i, j ∈ range(n+1): term = 0\n      ...\n    · intro hi'\n      -- i ∉ range(n+1): contradiction since i ≤ n\n      rw [Finset.mem_range] at hi'; omega\n  · -- ContDiffAt of each term\n    exact (contDiffAt_const).mul (((contDiff_id.sub contDiff_const).pow j).contDiffAt)? \n```\nHmm wait, iteratedDeriv_const_mul needs (c : 𝔸) with f : 𝕜 → 𝔸... iteratedDeriv_const_mul {f : 𝕜 → 𝔸} (c : 𝔸) (hf : ContDiffAt 𝕜 n f x) : iteratedDeriv n (fun y => c * f y) x = c * iteratedDeriv n f x — for 𝔸 = ℂ ✓ (normed algebra over itself). So term: iteratedDeriv i (fun w => c_j * (w−1)^j) 1 = c_j * iteratedDeriv i (fun w => (w−1)^j) 1 with ContDiffAt of (w−1)^j ✓.\n\niteratedDeriv i (fun w => (w−1)^j) 1: from A_iter's h2 pattern:\n```\nhave h2 : iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) 1 =\n    j.descFactorial i * (0 : ℂ) ^ (j - i) := by\n  have e := congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ j) (1 : ℂ)) 1\n  rw [iteratedDeriv_pow] at e\n  simpa using e\n```\nCheck iteratedDeriv_comp_sub_const signature from LiResidue usage: `congr_fun (iteratedDeriv_comp_sub_const i (fun w : ℂ => w ^ n) (1 : ℂ)) 1` : iteratedDeriv i ((fun w => w^n) ∘ (·−1))... gives iteratedDeriv i (fun w => (w−1)^n) 1 = iteratedDeriv i (fun w => w^n) (1−1) = n.descFactorial i * (1−1)^{n−i} — and iteratedDeriv_pow: iteratedDeriv i (fun w => w^n) x = n.descFactorial i * x^{n−i} ✓ then simpa turns 1−1 into 0 ✓ (A_iter did exactly this ✓ copy).\n\nSo term j (j ∈ range(n+1), j ≤ n):\n- if j = i: descFactorial i i = i! (Nat.descFactorial_self), 0^{i−i} = 0⁰ = 1: term = c_i·(i!·1) = c_i·i!.\n- if j ≠ i: j < i: Nat.descFactorial_eq_zero... `Nat.descFactorial_eq_zero_iff_lt : n.descFactorial i = 0 ↔ n < i`? I think `Nat.descFactorial_eq_zero_iff_lt : (n.descFactorial i = 0) ↔ n < i` exists ✓. So j < i ⟹ descFactorial = 0 ⟹ term 0.\n  j > i: 0^{j−i} with j−i ≥ 1: zero_pow ⟹ 0 ⟹ term 0 (mul_zero).\n\nFinset.sum_eq_single i: needs (i ∈ range(n+1) handled by third arg) and all other terms 0 ✓.\n\nThen the i-th term: c_i·(i.descFactorial i·0^{i−i}) = c_i·(i!·1): \n```\nc_i = iteratedDeriv i (Ffun n) 1 / i !\nterm = c_i * (i ! : ℂ) = iteratedDeriv i (Ffun n) 1 / i ! * i ! = iteratedDeriv i (Ffun n) 1 (div_mul_cancel₀, i! ≠ 0)\n```\nfield_simp or `div_mul_cancel₀` — `div_mul_cancel₀ : b ≠ 0 → a / b * b = a`? name might be `div_mul_cancel₀` ✓ exists.\n\nPutting it together — the sum: Σ_j c_j * (descFactorial ... ) — wait, I need to write the term after iteratedDeriv_sum + iteratedDeriv_const_mul as c_j * (j.descFactorial i * (0:ℂ)^{j−i}). Let me structure:\n\n```lean\n  trans ∑ j ∈ Finset.range (n + 1),\n      (iteratedDeriv j (Ffun n) 1 / j !) * (j.descFactorial i * (0 : ℂ) ^ (j - i))\n  · apply Finset.sum_congr rfl\n    intro j hj\n    rw [iteratedDeriv_const_mul _ ?_]  -- ContDiffAt\n    congr 1\n    exact hderiv_pow_eq j  -- the descFactorial identity\n  · rw [Finset.sum_eq_single i ...]\n```\n\nThen sum_eq_single i: term_i = c_i * (i! * 1) = iteratedDeriv i Ffun 1. Manageable. All pieces mirrored from existing session-015/016 code ✓.\n\nThen:\n```lean\nlemma Ffun_sub_TaylP_order (n : ℕ) :\n    (n + 1 : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1 := by\n  rw [natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero\n    ((Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1))]\n  intro i hi\n  rw [Nat.cast_add_one?]... \n```\nThe lemma: natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf : AnalyticAt 𝕜 f z₀) : ↑n ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0. Goal (n+1 : ℕ∞) ≤ ... — the cast of n+1: `(n+1 : ℕ∞)` — the lemma has `n ≤ analyticOrderAt` with n : ℕ and an implicit cast. So rw [...] on goal ((n+1 : ℕ) : ℕ∞) ≤ ... — does the rw match? The lemma's LHS: ↑n ≤ analyticOrderAt f z₀ — unify ↑n with ↑(n+1): n := n+1 ✓. But my goal is written (n + 1 : ℕ∞) — elaborates as Nat.cast (n+1)? `(n + 1 : ℕ∞)` with n : ℕ: n+1 computed in ℕ then cast? `(n + 1 : ℕ∞)` elaborates n+1 at ℕ∞ directly: HAdd ℕ∞... `Nat.cast_add` issues. To be safe, write the goal as `((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt ...`. Then rw gives ∀ i < n+1, iteratedDeriv i (Ffun n − TaylP n) 1 = 0 — Ffun n − TaylP n is Pi.sub; the analytic proof term: (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1) : AnalyticAt ℂ (Ffun n − TaylP n) 1 ✓ (AnalyticAt.sub gives Pi.sub form ✓ defeq with the lambda).\n  intro i hi; exact Ffun_sub_TaylP_iteratedDeriv n i (Nat.lt_succ_iff.mp hi)... wait hi : i < n+1 ⟹ i ≤ n ✓ Nat.lt_succ_iff. But careful — Ffun_sub_TaylP_iteratedDeriv is about `iteratedDeriv i (Ffun n - TaylP n) 1` — the goal after the lemma application: iteratedDeriv i (Ffun n − TaylP n) 1 = 0 ✓ matches.\n\nThen the Tendsto:\n```lean\nlemma Rfun_tendsto_one (n : ℕ) :\n    ∃ L : ℂ, Tendsto (Rfun n) (𝓝[≠] (1 : ℂ)) (𝓝 L) := by\n  set g := Ffun n - TaylP n with hg\n  have hgan : AnalyticAt ℂ g 1 := (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1)\n  have hord := Ffun_sub_TaylP_order n\n  by_cases htop : analyticOrderAt g 1 = ⊤\n  · -- g ≡ 0 near 1\n    refine ⟨0, ?_⟩\n    have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), g s = 0 := analyticOrderAt_eq_top.mp htop\n    have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = 0 := by\n      filter_upwards [Rfun_eq_sub_div_near_one n,\n        mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n      rw [hs, hg0]\n      simp  -- 0 / x = 0\n    exact tendsto_const_nhds.congr' hev.symm  -- Tendsto.congr' : f =ᶠ[l] g → Tendsto g l ... \n  · obtain ⟨h, hh, hh0, hfh⟩ := hgan.analyticOrderAt_ne_top.mp htop\n    set m := analyticOrderNatAt g 1 with hm\n    have hmcast : (m : ℕ∞) = analyticOrderAt g 1 := Nat.cast_analyticOrderNatAt htop\n    have hnm : n + 1 ≤ m := by\n      rw [hmcast] at hord  -- hmm hord : ((n+1:ℕ):ℕ∞) ≤ analyticOrderAt g 1; hmcast : (m:ℕ∞) = analyticOrderAt g 1\n      rw [← hmcast] at hord  -- (n+1:ℕ∞) ≤ (m:ℕ∞)\n      exact ENat.natCast_le_natCast.mp hord  -- need cast matching\n    -- eventually Rfun n s = (s−1)^{m−(n+1)} · h s\n    have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ), Rfun n s = (s - 1) ^ (m - (n + 1)) * h s := by\n      filter_upwards [Rfun_eq_sub_div_near_one n,\n        mem_nhdsWithin_of_mem_nhds hfh.eventually_nhds, self_mem_nhdsWithin] with s hs hgf hs1\n      have hs1' : s - 1 ≠ 0 := sub_ne_zero.mpr (by simpa using hs1)\n      rw [hs]\n      -- g s = (s−1)^m • h s (from hgf : g =ᶠ[𝓝 s] ...)\n      have hgs : g s = (s - 1) ^ m * h s := by\n        have := hgf.self_of_nhds\n        simpa [smul_eq_mul] using this  -- hgf : g =ᶠ[𝓝 s] fun z => (z−1)^m • h z; self_of_nhds : g s = (s−1)^m • h s\n      rw [hgs]\n      -- (s−1)^m * h s / (s−1)^{n+1} = (s−1)^{m−(n+1)} * h s\n      have e : (s - 1) ^ m = (s - 1) ^ (n + 1) * (s - 1) ^ (m - (n + 1)) := by\n        rw [← pow_add]; congr 1; omega\n      rw [e]\n      field_simp [hs1', pow_ne_zero (n+1) hs1']\n      ring\n    refine ⟨0 ^ (m - (n + 1)) * h 1, ?_⟩\n    have hcont : ContinuousAt (fun s : ℂ => (s - 1) ^ (m - (n + 1)) * h s) 1 :=\n      (((continuousAt_id.sub continuousAt_const).pow _).mul hh.continuousAt)\n    have hT : Tendsto (fun s : ℂ => (s - 1) ^ (m - (n + 1)) * h s) (𝓝[≠] (1 : ℂ))\n        (𝓝 ((1 - 1) ^ (m - (n + 1)) * h 1)) := hcont.tendsto.mono_left nhdsWithin_le_nhds\n    -- value at 1: (1−1)^k * h 1 = 0^k * h 1\n    have hval : ((1 : ℂ) - 1) ^ (m - (n + 1)) * h 1 = 0 ^ (m - (n + 1)) * h 1 := by norm_num\n    exact hT.congr' hev |>.congr (fun _ => rfl) ... \n```\nHmm — Tendsto.congr': (h : f =ᶠ[l] g) → Tendsto f l l' → Tendsto g l l'. Direction: we have Tendsto φ (the nice function) and Rfun =ᶠ φ (hev : Rfun n s = φ s). So Tendsto.congr' hev... hev : ∀ᶠ, Rfun n s = φ s — as EventuallyEq: Rfun n =ᶠ[𝓝[≠] 1] φ. Tendsto.congr' (h : f₁ =ᶠ f₂) (hf : Tendsto f₁ ...) : Tendsto f₂? Let me recall: `Filter.Tendsto.congr' : f₁ =ᶠ[l] f₂ → Tendsto f₁ l l' → Tendsto f₂ l l'` ✓. So Tendsto.congr' hev hT : Tendsto (Rfun n) (𝓝[≠] 1) (𝓝 ((1−1)^{m−n−1}·h 1)). Then the limit value: (1−1) = 0: simp to 0^{m−n−1}·h 1. Just use ⟨(1−1)^{m−(n+1)}·h 1, hT.congr' hev⟩ directly — no need to normalize! The existential allows any L. \n\nSimilarly case ⊤: ⟨0, _⟩: Tendsto.congr': hev : Rfun =ᶠ 0; tendsto_const_nhds : Tendsto (fun _ => 0)... `tendsto_const_nhds : Tendsto (fun _ => c) l (𝓝 c)` ✓. Tendsto.congr' hev tendsto_const_nhds : Tendsto (Rfun n) _ (𝓝 0) ✓.\n\nWait — direction check again: Tendsto.congr' signature: `theorem Filter.Tendsto.congr' {f₁ f₂ : α → β} {l₁} {l₂} (hl : f₁ =ᶠ[l₁] f₂) (h : Tendsto f₁ l₁ l₂) : Tendsto f₂ l₁ l₂` ✓. So f₁ := Rfun n (hev : Rfun n =ᶠ φ), h : need Tendsto (Rfun n)?? NO — h must be about f₁ = Rfun — but we have Tendsto φ! So I need hev.symm : φ =ᶠ Rfun, then Tendsto.congr' hev.symm hT : Tendsto (Rfun n) ✓. Careful with direction! In case ⊤: hev : Rfun =ᶠ (fun _ => 0)?? hev : ∀ᶠ s, Rfun n s = 0 — as EventuallyEq: Rfun n =ᶠ[𝓝[≠] 1] fun _ => 0 — then Tendsto.congr' hev needs Tendsto (Rfun n) — wrong again. Use hev.symm : (fun _ => 0) =ᶠ Rfun, Tendsto.congr' hev.symm tendsto_const_nhds : Tendsto (Rfun n) (𝓝[≠] 1) (𝓝 0) ✓.\n\nIn the m-case: hev : Rfun n =ᶠ[...] φ; need φ =ᶠ Rfun: hev.symm; Tendsto.congr' hev.symm hT ✓.\n\nThen:\n```lean\nlemma Rfun_bounded_near_one (n : ℕ) : (Rfun n) =O[𝓝[≠] (1 : ℂ)] (1 : ℂ → ℂ) := by\n  obtain ⟨L, hL⟩ := Rfun_tendsto_one n\n  exact hL.isBigO_one ℂ\n```\nCheck: Tendsto.isBigO_one : Tendsto f l (𝓝 c) → f =O[l] (1 : α → 𝕜) — vendored line 117: (hc.tendsto.mono_left nhdsWithin_le_nhds).isBigO_one ℂ ✓.\n\n**§5 residue at a zero:**\n\n```lean\nlemma Rfun_residue_at (n : ℕ) {ρ : ℂ} (hρ : ρ ≠ 1) :\n    ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ))\n      =O[𝓝[≠] ρ] (1 : ℂ → ℂ) := by\n  have hρα : AnalyticAt ℂ riemannZeta ρ := analyticAt_riemannZeta hρ\n  obtain ⟨h, hh, hh0, hfh⟩ := hρα.analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ)\n  set m := analyticOrderNatAt riemannZeta ρ with hm\n  have hmz : (zeroMult ρ : ℂ) = m := rfl  -- zeroMult defeq analyticOrderNatAt\n  -- k derivative value\n  have hkd : DifferentiableAt ℂ (kFun n) ρ := kFun_differentiableAt hρ\n  -- the eventual algebraic identity\n  have hexp : ∀ᶠ s in 𝓝[≠] ρ,\n      (-(m : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ)) - kFun n s * logDeriv h s - ppart n s)\n        = ((Rfun n) - fun s => ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) / (s - ρ)) s := by\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 hsρ' : s - ρ ≠ 0 := sub_ne_zero.mpr (by simpa using hsρ)\n    -- logDeriv ζ s = m/(s−ρ) + logDeriv h s\n    have hfs : riemannZeta =ᶠ[𝓝 s] fun z => (z - ρ) ^ m • h z := hfhs\n    have hld : logDeriv riemannZeta s = (m : ℂ) / (s - ρ) + logDeriv h s := by\n      have e1 : logDeriv riemannZeta s = logDeriv (fun z => (z - ρ) ^ m * h z) s := by\n        simp only [logDeriv_apply, hfs.deriv_eq, hfs.self_of_nhds, smul_eq_mul]\n      rw [e1, logDeriv_mul (f := fun z : ℂ => (z - ρ) ^ m) (g := h) s\n        (pow_ne_zero _ hsρ') hhs (by fun_prop) hhas.differentiableAt]\n      have e2 : logDeriv (fun z : ℂ => (z - ρ) ^ m) s = (m : ℂ) / (s - ρ) := by\n        rw [show (fun z : ℂ => (z - ρ) ^ m) = (fun x : ℂ => x ^ m) ∘ (fun z => z - ρ) from rfl,\n          logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]\n        simp\n      rw [e2]\n    -- algebra\n    have hA : ((zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n)) = -(m : ℂ) * kFun n ρ := by\n      rw [hmz]  -- hmz : (zeroMult ρ : ℂ) = m — hmm (m : ℂ) vs m : ℕ cast — m is ℕ, so (m:ℂ)\n      simp only [kFun]\n      ring\n    simp only [Pi.sub_apply, Rfun, Jlag, hA]\n    -- logDeriv_apply: logDeriv ζ s = deriv ζ s / ζ s — the Jlag has −(deriv/·) form\n    rw [show deriv riemannZeta s / riemannZeta s = logDeriv riemannZeta s from (logDeriv_apply ..).symm]\n    rw [hld]\n    field_simp [hsρ']\n    ring\n  ...\n```\nWait — logDeriv_apply: `logDeriv_apply : logDeriv f a = deriv f a / f a` ✓ simp lemma. Jlag n s = kFun n s * (−(deriv ζ s/ζ s)). With the rw: = kFun n s * (−logDeriv ζ s). Then hld.\n\nGoal (before field_simp/ring):\n−m·((k s − k ρ)/(s−ρ)) − k s·logDeriv h s − ppart n s\n= kFun n s·(−(m/(s−ρ) + logDeriv h s)) − ppart n s − (−m·kFun n ρ)/(s−ρ)\nfield_simp [hsρ'] then ring ✓. (ppart n s appears on both sides — ring handles.)\n\nHmm wait — the simp only [Pi.sub_apply, Rfun, Jlag, hA]: the RHS is ((Rfun n) − fun s => A/(s−ρ)) s = Rfun n s − A/(s−ρ) [Pi.sub_apply] = (Jlag n − ppart n) s − ... [Rfun] — Rfun is a def; simp only [Rfun] unfolds? Use simp only [Rfun, Jlag, Pi.sub_apply, hA] — for defs, simp only [Rfun] uses the equation lemma Rfun.eq_def / unfolds — works for plain defs in Mathlib style ✓ (used commonly). If not, `show` the unfolded form. Then Jlag unfolds to kFun n s * (−(deriv...)). OK.\n\nAlso `hhs : h s ≠ 0` — from hh.continuousAt.eventually_ne hh0 : ∀ᶠ s in 𝓝 ρ, h s ≠ 0 ✓ pulled to 𝓝[≠] ✓.\n\n`hhas : AnalyticAt ℂ h s` from hh.eventually_analyticAt : ∀ᶠ s in 𝓝 ρ, AnalyticAt ℂ h s ✓.\n\nlogDeriv_mul signature (from vendored line 257): logDeriv_mul (f := ...) (g := ...) s (hf-ne) (hg-ne) (hf-diff) (hg-diff) — vendored: `logDeriv_mul (f := fun s : ℂ => (s - q) ^ analyticOrderNatAt f q) (g := h) s (pow_ne_zero _ hsq) hhs (by fun_prop) hhas.differentiableAt` ✓ same pattern.\n\nlogDeriv_comp (by fun_prop) (by fun_prop) — vendored line 263: logDeriv_comp (by fun_prop) (by fun_prop) ✓ — signature: logDeriv_comp (hf : DifferentiableAt ℂ f (g x)?) ... vendored used it for (fun x => x^ord) ∘ (fun s => s−q) ✓ same shape.\n\nlogDeriv_pow : logDeriv (fun x => x^m) x = m/x ✓ vendored used it.\n\nThen the final simp after rw [e2]: vendored did `rw [e2]` inside hld after the logDeriv_comp + logDeriv_pow gave logDeriv (x^m) ((s−ρ)) · deriv(s−ρ)... vendored line 261-264: e2 : logDeriv (fun s => (s−q)^ord) s = (ord:ℂ)/(s−q) via rw [show ... from rfl, logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]; simp — logDeriv (x^m) at (s−q) = m·(s−q)^{m−1}/(s−q)^m? logDeriv_pow: logDeriv (f^m) = m·logDeriv f — so logDeriv (fun x => x^m) x = m·(deriv id x / x) = m/x ✓ then comp multiplies by deriv of (s−q) = 1: logDeriv_comp gives logDeriv (g∘f) x = (logDeriv g (f x))·(deriv f x) = (m/(s−q))·1 — the simp clears the ·1 and deriv ✓. OK — copy the pattern verbatim.\n\nNow the big-O assembly:\n```lean\n  -- slope tendsto\n  have hslope : Tendsto (fun s => (kFun n s - kFun n ρ) / (s - ρ)) (𝓝[≠] ρ)\n      (𝓝 (deriv (kFun n) ρ)) := by\n    have := hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt\n    simpa only [slope_fun_def_field] using this\n  have hcont1 : Tendsto (fun s => kFun n s * logDeriv h s) (𝓝[≠] ρ)\n      (𝓝 (kFun n ρ * logDeriv h ρ)) := by\n    have hc : ContinuousAt (fun s => kFun n s * logDeriv h s) ρ :=\n      hkd.continuousAt.mul (hh.deriv.continuousAt.div hh.continuousAt hh0)\n    exact hc.tendsto.mono_left nhdsWithin_le_nhds\n  have hcont2 : Tendsto (ppart n) (𝓝[≠] ρ) (𝓝 (ppart n ρ)) :=\n    (ppart_continuousAt hρ).tendsto.mono_left nhdsWithin_le_nhds\n  have hO : (fun s => -(m : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ)) - kFun n s * logDeriv h s\n      - ppart n s) =O[𝓝[≠] ρ] (1 : ℂ → ℂ) := by\n    have hT : Tendsto (fun s => -(m : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))\n        - kFun n s * logDeriv h s - ppart n s) (𝓝[≠] ρ)\n        (𝓝 (-(m : ℂ) * deriv (kFun n) ρ - kFun n ρ * logDeriv h ρ - ppart n ρ)) :=\n      ((hslope.const_mul _).sub hcont1).sub hcont2\n    exact hT.isBigO_one ℂ\n  exact hO.congr' hexp EventuallyEq.rfl\n```\nCheck IsBigO.congr' signature: from vendored line 280: `hO.congr' hexp EventuallyEq.rfl` where hO : LHS-func =O 1, hexp : ∀ᶠ, LHS-func s = RHS-func s... vendored: hexp : ∀ᶠ s, bigterm = ((g·logDeriv f) − A/(s−q)) s; then hO.congr' hexp EventuallyEq.rfl : ((g·logDeriv f) − ...) =O 1 ✓. IsBigO.congr' : f =O[l] g → f' =ᶠ[l] f → g =ᶠ[l] g' → f' =O[l] g' — signature: `Asymptotics.IsBigO.congr' (h : f =O[l] g) (hf : f' =ᶠ[l] f) (hg : g =ᶠ[l] g') : f' =O[l] g'`? From the vendored usage: hO.congr' hexp EventuallyEq.rfl with hexp : ∀ᶠ s, (bigterm) s = (target) s — as EventuallyEq: bigterm =ᶠ target. congr' wants f' =ᶠ f i.e. target =ᶠ bigterm?? vendored passed hexp directly where hexp : bigterm =ᶠ target... Hmm — so congr' (hf : f =ᶠ f')? Whatever — vendored line 280: `exact hO.congr' hexp EventuallyEq.rfl` compiles with hexp stated as `bigterm = target-func s` — so the convention works with hexp : (fun s => bigterm) =ᶠ target? Let me just mirror exactly: my hexp stated as `bigLHS = targetRHS s` — same orientation as vendored ✓ copy.\n\nAlso `ppart_continuousAt`:\n```lean\nlemma ppart_continuousAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    ContinuousAt (ppart n) s := by\n  -- mirror tail_continuousAt with Icc 1\n  have hterm : ∀ i : ℕ, ContinuousAt (fun w => Acoeff n i / (w - 1) ^ i) s := by\n    intro i\n    have hw1 : s - 1 ≠ 0 := sub_ne_zero.mpr hs\n    exact continuousAt_const.div ((continuousAt_id.sub continuousAt_const).pow _)\n      (pow_ne_zero _ hw1)\n  have : ∀ t : Finset ℕ, ContinuousAt (fun w => ∑ i ∈ t, Acoeff n i / (w - 1) ^ i) s := by\n    intro t\n    induction t using Finset.induction with\n    | empty => exact continuousAt_const\n    | insert a t hat ht =>\n      simp_rw [Finset.sum_insert hat]\n      exact ContinuousAt.add (hterm a) ht\n  exact this _\n```\n(ppart n s unfolds to the sum — `exact this _` needs the function to match: ppart n = fun w => ∑ i ∈ Icc 1 (n+1), ... by def ✓ defeq; ContinuousAt (ppart n) s — `this (Finset.Icc 1 (n+1))` : ContinuousAt (fun w => ∑ ...) s — defeq to ppart n ✓ exact should accept; if not, `show` or unfold.)\n\nSession-016 note: \"ContinuousAt of expressions containing the point variable: write the fun w => lambda EXPLICITLY\". tail_continuousAt did exactly the above pattern with explicit lambdas ✓.\n\n**§6 main theorem.**\n\n```lean\n/-- The rectangle residue theorem for the Lagarias-kernel integrand (D-064 §2):\non any rectangle with 1 interior and no zeros of ζ on the border,\n  RectangleIntegral' (Jlag n) z w = ResW1 n + Σ_{ρ ∈ zeros} mult·(1−(ρ/(ρ−1))ⁿ)\nwhere zeros = the (finite) set of zeros of ζ inside the rectangle. -/\ntheorem rectInt'_Jlag (n : ℕ) {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)\n    (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ))\n    (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0) :\n    RectangleIntegral' (Jlag n) z w =\n      ResW1 n + ∑ ρ ∈ (finite_zeros_rectangle zetaA_analyticOnNhd_rect\n          (mem_of_mem_nhds h1) (by rw [zetaA_one]; norm_num)).toFinset,\n        (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n  ...\n```\nwhere `zetaA_analyticOnNhd_rect : AnalyticOnNhd ℂ zetaA (Rectangle z w)` := zetaA_analyticOnNhd_univ.mono (subset_univ _) — AnalyticOnNhd.mono ✓ exists? AnalyticOnNhd f s is ∀ x ∈ s, AnalyticAt f x — mono: fun h hs => h x (hsub hs) ✓ define inline.\n\nLet me set up:\n```lean\n  classical\n  have h1mem : (1 : ℂ) ∈ Rectangle z w := mem_of_mem_nhds h1\n  have hzA1 : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num\n  have hzA : AnalyticOnNhd ℂ zetaA (Rectangle z w) := fun s _ => by\n    by_cases hs : s = 1\n    · subst hs; exact zetaA_analyticAt_one\n    · exact zetaA_analyticAt_of_ne hs\n  set hfin := finite_zeros_rectangle hzA h1mem hzA1 with hfin'\n  set Sz := hfin.toFinset with hSz\n  -- membership characterization\n  have hSzmem : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0 := by\n    intro s\n    rw [hSz, Set.Finite.mem_toFinset]\n    simp [hfin']  -- mem_inter_iff, mem_preimage, mem_singleton\n  have h1notSz : (1 : ℂ) ∉ Sz := by\n    intro h\n    rw [hSzmem] at h\n    exact hzA1 h.2\n  have hSz_ne_one : ∀ ρ ∈ Sz, ρ ≠ 1 := by\n    intro ρ hρ h1ρ\n    exact h1notSz (h1ρ ▸ hρ)\n  have hSz_zeta : ∀ ρ ∈ Sz, riemannZeta ρ = 0 := by\n    intro ρ hρ\n    have h1 := (hSzmem ρ).mp hρ\n    have hρ1 := hSz_ne_one ρ hρ\n    rw [zetaA_apply hρ1] at h1\n    -- h1.2 : (ρ−1)*ζ ρ = 0\n    have := h1.2\n    rw [mul_eq_zero] at this\n    rcases this with h | h\n    · exact absurd (sub_ne_zero.mpr hρ1) (by ... h : ρ − 1 = 0)  -- h : ρ−1 = 0 ⟹ ρ = 1\n    · exact h\n  -- interior of each Sz point\n  have hSzint : ∀ ρ ∈ Sz, Rectangle z w ∈ 𝓝 ρ := by\n    intro ρ hρ\n    have hmem : ρ ∈ Rectangle z w := ((hSzmem ρ).mp hρ).1\n    have hρ1 := hSz_ne_one ρ hρ\n    have hζ0 := hSz_zeta ρ hρ\n    have hnb : ρ ∉ RectangleBorder z w := fun hb => hborder ρ hb hζ0\n    exact rectangle_mem_nhds_of_mem_not_border hre him hmem hnb\n  -- the residue function\n  set A : ℂ → ℂ := fun p => if p = 1 then 0 else (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) with hAdef\n  -- main application\n  have key := residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A ?_ ?_ ?_\n  ...\n```\n\nresidueTheorem_finset args: (hre) (him) (S : Finset ℂ) (A : ℂ → ℂ) (hS : ∀ p ∈ S, Rectangle z w ∈ 𝓝 p) (fHolo : HolomorphicOn f (Rectangle z w \\ ↑S)) (near : ∀ p ∈ S, (f − fun s => A p/(s−p)) =O[𝓝[≠] p] 1).\n\nhS: ∀ p ∈ insert 1 Sz, Rectangle ∈ 𝓝 p:\n```lean\n  · intro p hp\n    rw [Finset.mem_insert] at hp\n    rcases hp with rfl | hp\n    · exact h1\n    · exact hSzint p hp\n```\n\nfHolo: HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert 1 Sz)):\n```lean\n  · intro s hs\n    have hs1 : s ≠ 1 := fun h => hs.2 (by simp [h])\n    have hsSz : s ∉ Sz := fun h => hs.2 (by simp [Finset.mem_insert, h])\n    have hs0 : riemannZeta s ≠ 0 := by\n      intro h0\n      apply hsSz\n      rw [hSzmem]\n      exact ⟨hs.1, by rw [zetaA_apply hs1, h0, mul_zero]⟩\n    exact (Rfun_differentiableAt hs1 hs0).differentiableWithinAt\n```\nhs.2 : s ∉ ↑(insert 1 Sz) — with Finset.mem_insert/coe: s ∈ insert 1 Sz ⟺ s = 1 ∨ s ∈ Sz. For hs1: if s = 1 then s ∈ insert: (Finset.mem_insert_self ...)/by simp. Careful with coe: hs : s ∈ Rectangle z w \\ (↑(insert 1 Sz) : Set ℂ); hs.2 : s ∉ (↑(insert 1 Sz) : Set ℂ). Finset.coe_insert : ↑(insert a s) = insert a ↑s (Set insert). So: hs.2 (by rw [Finset.coe_insert]; exact Set.mem_insert 1 _)... Let me write: \n```\n    have hsS : s ∉ insert (1 : ℂ) (↑Sz : Set ℂ) := by\n      rw [Finset.coe_insert] at hs  -- hmm hs.2 : s ∉ ↑(insert 1 Sz)\n      exact hs.2\n```\nSimpler: have hsc : s ∉ (↑(insert 1 Sz) : Set ℂ) := hs.2; then by_cases s = 1: if s = 1, then s ∈ ↑(insert 1 Sz): Finset.mem_coe.mpr (Finset.mem_insert_self 1 Sz) — contradiction. If s ∈ Sz: Finset.mem_coe.mpr (Finset.mem_insert_of_mem h) — contradiction. So:\n```lean\n    have hsc : s ∉ (↑(insert (1 : ℂ) Sz) : Set ℂ) := hs.2\n    have hs1 : s ≠ 1 := fun h => hsc (Finset.mem_coe.mpr (h ▸ Finset.mem_insert_self 1 Sz))\n    have hsSz : s ∉ Sz := fun h => hsc (Finset.mem_coe.mpr (Finset.mem_insert_of_mem h))\n```\n✓ clean.\n\nnear: ∀ p ∈ insert 1 Sz, ((Rfun n) − fun s => A p/(s−p)) =O[𝓝[≠] p] 1:\n```lean\n  · intro p hp\n    rw [Finset.mem_insert] at hp\n    rcases hp with rfl | hp\n    · -- p = 1: A 1 = 0\n      have hA1 : A 1 = 0 := by rw [hAdef]; simp\n      have : ((Rfun n) − fun s => A 1 / (s - 1)) = (Rfun n) := by\n        rw [hA1]; simp  -- 0/(s−1) = 0, sub_zero\n      rw [this]  -- hmm rw with function equality: goal is about the lambda — congr? \n      exact Rfun_bounded_near_one n\n    · -- p ∈ Sz\n      have hp1 : p ≠ 1 := hSz_ne_one p hp\n      have hAp : A p = (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) := by\n        rw [hAdef]; simp [hp1]\n      rw [hAp]\n      exact Rfun_residue_at n hp1\n```\nThe `rw [this]` on the goal: goal `((Rfun n) − fun s => A 1 / (s - 1)) =O[𝓝[≠] 1] 1` — rw with this : (that lambda) = Rfun n ✓ rewrites the function ✓ should work (motive IsBigO ... f ...). Or `simpa [hA1] using Rfun_bounded_near_one n` — simpler: \n```\n    · simpa [hAdef] using Rfun_bounded_near_one n\n```\nsimp [hAdef] unfolds A 1 → if 1 = 1 then 0 else ... → 0; then fun s => 0/(s−1) → 0; Rfun n − 0 → Rfun n ✓. Try simpa first.\n\nSimilarly the Sz case: `simpa [hAdef, hp1] using Rfun_residue_at n hp1` — the if p = 1 with hp1 : p ≠ 1 — simp [hp1] resolves if_neg ✓. The residue function in Rfun_residue_at's statement: ((zeroMult ρ:ℂ)·(1−(ρ/(ρ−1))^n))/(s−ρ) ✓ matches A p unfolded ✓.\n\nThen:\n```lean\n  -- conclusion of residue theorem\n  have hsum : ∑ p ∈ insert 1 Sz, A p = ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n    rw [Finset.sum_insert h1notSz]\n    have hA1 : A 1 = 0 := by simp [hAdef]\n    rw [hA1, zero_add]\n    apply Finset.sum_congr rfl\n    intro ρ hρ\n    have hρ1 := hSz_ne_one ρ hρ\n    simp [hAdef, hρ1]\n  rw [hsum] at key\n  -- Jlag = Rfun + ppart\n  have heq : Jlag n = Rfun n + ppart n := by\n    rw [Rfun]; simp [Pi.sub_apply, Pi.add_apply]  -- (Jlag − ppart) + ppart = Jlag: sub_add_cancel\n  rw [show Jlag n = Rfun n + ppart n from sub_add_cancel _ _]  -- Rfun n = Jlag n − ppart n defeq\n  ...\n```\nHmm: Rfun n = Jlag n − ppart n — so Rfun n + ppart n = Jlag n − ppart n + ppart n = Jlag n by sub_add_cancel ✓ (functions form an additive group: sub_add_cancel : a − b + b = a ✓). So `rw [show Jlag n = Rfun n + ppart n from (sub_add_cancel (Jlag n) (ppart n)).symm]`? sub_add_cancel : a − b + b = a; with a := Jlag n, b := ppart n: Jlag n − ppart n + ppart n = Jlag n — and Rfun n is DEFeq to Jlag n − ppart n (unfold). (sub_add_cancel (Jlag n) (ppart n)) : Jlag n − ppart n + ppart n = Jlag n. Hmm the subtraction is Pi.instSub — sub_add_cancel applies generically ✓. Then Rfun n + ppart n — is `Rfun n` syntactically `Jlag n − ppart n`? No — Rfun n is a def application. sub_add_cancel's LHS is `Jlag n − ppart n + ppart n`; to rewrite goal `RectangleIntegral' (Jlag n) z w = ...` I want Jlag n = Rfun n + ppart n: claim: Rfun n + ppart n = Jlag n by: show Rfun n + ppart n = Jlag n − ppart n + ppart n (defeq — rfl?) then sub_add_cancel. So: `have heq : Rfun n + ppart n = Jlag n := sub_add_cancel _ _` — does sub_add_cancel _ _ elaborate with a := Jlag n? sub_add_cancel (a b : α) : a − b + b = a. heq's LHS: Rfun n + ppart n must unify with ?a − ?b + ?b: ?b := ppart n; Rfun n =?= ?a − ppart n: Rfun n unfolds (delta) to Jlag n − ppart n ✓ defeq — elaboration of `sub_add_cancel _ _` against the stated type Rfun n + ppart n = Jlag n: unification at default transparency should unfold Rfun ✓ probably works. If not: `by rw [Rfun]; exact sub_add_cancel _ _`.\n\nThen:\n```lean\n  rw [heq]  -- goal: RectangleIntegral' (Rfun n + ppart n) z w = ResW1 n + Σ ...\n```\nwait direction: goal is RectangleIntegral' (Jlag n) z w = ResW1 n + sum. rw [← heq] : replaces Jlag n with Rfun n + ppart n ✓.\n\nIntegrability:\n```lean\n  have hRint : RectangleBorderIntegrable (Rfun n) z w := by\n    apply ContinuousOn.rectangleBorder_integrable\n    -- Rfun continuous on Rectangle ∖ S ⊇ border\n    have hhol : HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert 1 Sz)) := fHolo-proof-term\n    apply hhol.continuousOn.mono\n    intro s hs\n    have hsR : s ∈ Rectangle z w := rectangleBorder_subset_rectangle z w hs\n    refine ⟨hsR, ?_⟩\n    -- s ∉ insert 1 Sz\n    have hs1 : s ≠ 1 := fun h => not_mem_rectangleBorder_of_rectangle_mem_nhds h1 (h ▸ hs)\n    have hζs : riemannZeta s ≠ 0 := hborder s hs\n    intro hsc\n    rw [Finset.mem_coe, Finset.mem_insert] at hsc\n    rcases hsc with h | h\n    · exact hs1 h\n    · exact hζs (hSz_zeta s h)\n  have hPint : RectangleBorderIntegrable (ppart n) z w := by\n    apply HolomorphicOn.rectangleBorderIntegrable' _ h1\n    intro s hs\n    exact (ppart_differentiableAt hs.2).differentiableWithinAt\n```\nWait — HolomorphicOn.rectangleBorderIntegrable' (hf : HolomorphicOn f (Rectangle z w \\ {p})) (hp : Rectangle ∈ 𝓝 p) — the p here is inferred from hf's domain {p}: for ppart the complement {1} and hp := h1 ✓ — used identically in LiPrincipal hAint ✓. ppart_differentiableAt needs s ≠ 1: hs : s ∈ Rectangle z w \\ {1}: hs.2 : s ∉ {1} ⟹ s ≠ 1: `Set.mem_compl_singleton_iff.mp hs.2`? Rectangle ∖ {1}: hs.2 : s ∉ {1} — s ≠ 1: fun h => hs.2 (by rw [h]; exact Set.mem_singleton 1)... In LiPrincipal they wrote `have hs1 : s ≠ 1 := hs.2` (line 283) — so s ∉ {1} is defeq/coe to s ≠ 1 ✓ (Set.mem_singleton_iff defeq). Copy.\n\nHmm — the hhol term: I need the fHolo proof as a standalone term to reuse for integrability. Structure: prove `have fHolo : HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert 1 Sz)) := ...` BEFORE the residueTheorem_finset application, pass it in, and reuse for hRint ✓.\n\nThen:\n```lean\n  rw [RectangleIntegral'_add _ _ _ _ hRint hPint]\n  rw [key]  -- RectangleIntegral' (Rfun n) z w = Σ formula (after hsum rewrite)\n  rw [rectInt'_ppart hre him h1]  -- RectangleIntegral' (ppart n) z w = ResW1 n\n  ring  -- Σ + ResW1 = ResW1 + Σ: add_comm\n```\nFinal goal after rewrites: (Σ formula) + ResW1 n = ResW1 n + (Σ formula) — add_comm ✓ `rw [add_comm]` or `ring`.\n\nWait — careful: key : RectangleIntegral' (Rfun n) z w = ∑ p ∈ insert 1 Sz, A p; after rw [hsum] at key: key : RectangleIntegral' (Rfun n) z w = ∑ ρ ∈ Sz, formula ✓.\n\nAnd the theorem statement's sum: ∑ ρ ∈ (finite_zeros_rectangle hzA h1mem hzA1).toFinset, ... — I set Sz := hfin.toFinset where hfin := finite_zeros_rectangle hzA h1mem hzA1 — for the statement to match after `set`, the statement must be written with exactly that term... The theorem statement as I write it will contain the full `finite_zeros_rectangle ...` application; then in the proof `set hfin := finite_zeros_rectangle hzA h1mem hzA1 with hfin'` will fold the GOAL's occurrence if hzA h1mem hzA1 are syntactically the same terms as in the goal. The goal's term uses my inline hzA proof etc. — `set` uses syntactic matching up to instances... The proof terms hzA/h1mem/hzA1 in the goal are whatever I wrote in the theorem statement. If in the proof I `set hfin := finite_zeros_rectangle hzA h1mem hzA1` with hzA defined as a have BEFORE set — the have's term is a local hypothesis fvar, NOT syntactically equal to the proof term in the goal! Then set won't fold the goal's occurrence. PROBLEM.\n\nSolutions:\n(a) State the theorem with a let-free explicit expression and in the proof first `show` to convert... same issue.\n(b) Make Sz a VARIABLE: state the theorem as `∀ (Sz : Finset ℂ), (∀ s, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0) → ...` — a supplied-zeros form! This is cleaner and matches the vendored pattern (rectangleIntegral'_mul_logDeriv supplies Z with an iff). The finiteness construction then lives OUTSIDE (ii′-4 will supply the concrete finset). This is BETTER design — like residueTheorem_finset itself takes S supplied.\n\nActually — hmm, but then the caller needs to produce Sz with the iff. The finite_zeros_rectangle produces the .Finite set; toFinset membership iff is `Set.Finite.mem_toFinset` — the caller bridges zetaA zeros ↔ ... Actually the iff I'd require: s ∈ Sz ↔ s ∈ Rectangle ∧ zetaA s = 0. Or more usefully for downstream: s ∈ Sz ↔ s ∈ Rectangle ∧ s ≠ 1 ∧ riemannZeta s = 0? Hmm — which characterization is most convenient for ii′-4/6? The D-064 assembly: zeros of ζ in the rectangle = nontrivial zeros inside ∪ {−2} (trivial). Downstream will characterize zeros via IsNontrivialZero ∨ s = −2... For maximum flexibility, require the iff with zetaA (the actual finiteness vehicle) — downstream can produce it from finite_zeros_rectangle trivially (mem_toFinset gives EXACTLY that iff). \n\nSo main theorem:\n```lean\ntheorem rectInt'_Jlag (n : ℕ) {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)\n    (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ))\n    (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0)\n    (Sz : Finset ℂ) (hSz : ∀ s : ℂ, s ∈ Sz ↔ s ∈ Rectangle z w ∧ zetaA s = 0) :\n    RectangleIntegral' (Jlag n) z w =\n      ResW1 n + ∑ ρ ∈ Sz, (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) := by\n```\nThen hSzmem := hSz ✓, h1notSz : 1 ∉ Sz from hzA1 (needs hzA1 : zetaA 1 ≠ 0 — prove inline ✓).\n\nAnd also provide the self-contained corollary producing Sz via finite_zeros_rectangle:\n```lean\ntheorem rectInt'_Jlag' (n : ℕ) {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im)\n    (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ))\n    (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0) :\n    RectangleIntegral' (Jlag n) z w =\n      ResW1 n + ∑ ρ ∈ (finite_zeros_rectangle (fun s _ => ...) (mem_of_mem_nhds h1) ...).toFinset, ... := \n  rectInt'_Jlag n hre him h1 hborder _ (fun s => by rw [Set.Finite.mem_toFinset]; ...)\n```\nHmm — the corollary's statement needs the full finite_zeros_rectangle term with inline proofs; and rectInt'_Jlag is applied with hSz := fun s => Iff.trans (Set.Finite.mem_toFinset ...) (mem-inter-iff-simp). The membership in (Rectangle ∩ zetaA⁻¹'{0}): s ∈ Rectangle z w ∩ zetaA ⁻¹' {0} ↔ s ∈ Rectangle ∧ zetaA s ∈ {0} ↔ s ∈ Rectangle ∧ zetaA s = 0. simp [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]. OK.\n\nActually — do I even need the corollary? For THIS sub-stage the supplied-Sz form is the deliverable; ii′-4 will construct the zero-avoiding rectangle and can call rectInt'_Jlag with the toFinset directly. Skip the corollary (YAGNI; less surface for breakage). Hmm — but the \"assemble sides(T)\" instruction... The sub-stage's theorem IS the assembly (sides = ResW1 + Σ). The concrete finset comes with the concrete rectangle in ii′-4. Fine — supplied form only. Also should I ALSO handle the −2 split? STATE.md mentions \"at −2 (residue 1−(2/3)ⁿ)\". That needs analyticOrderNatAt ζ (−2) = 1. Let me try to find trivial-zero simplicity... Zeta23 grep found nothing direct. Mathlib: `deriv riemannZeta` at −2... Let me quickly check Mathlib for trivial-zero-related lemmas. Actually — for the perimeter-split sum (nontrivial ∪ {−2}), downstream needs: zeros of ζ in rectangle ⟺ IsNontrivialZero ∨ = −2 — needs \"ζ s = 0 ∧ Re s ≤ 0 ⟹ s ∈ negative even integers\" (functional-equation fact). That's ii′-4 territory (L3 zero-avoiding T + rectangle specifics). The RESIDUE at −2 = zeroMult(−2)·(1−(2/3)ⁿ) — with zeroMult(−2) = 1 needing deriv ζ (−2) ≠ 0. Check Mathlib quickly for `riemannZeta_neg_two_mul` and any deriv-nonvanishing.\n\nActually, let me defer the −2 simplicity: the generic theorem covers it with zeroMult(−2) — downstream can discharge zeroMult(−2) = 1 when needed. I'll note it in the file header as a remaining trivial-zero-simplicity fact. Actually wait — let me do a quick check if it's cheap in Mathlib.","signature":""},{"type":"text","text":"All machinery confirmed. Quick check for trivial-zero simplicity (for the −2 residue value), then I'll write the file."},{"type":"tool_use","id":"Bash_27","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"riemannZeta_neg_two\\|riemannZeta_neg_nat\" Mathlib/NumberTheory/ --include=\"*.lean\" | head -8; echo ---; grep -rn \"zeroMult.*-2\\|analyticOrder.*riemannZeta.*-\\|trivial\" Zeta23/FromPNTPlus/ZetaBounds.lean | head -5","description":"Check trivial zero lemmas availability"},"extra_content":null}]