[{"type":"thinking","thinking":"`Complex.mem_reProdIm` ✓ (accessible as `mem_reProdIm` with `open Complex`). uIcc_of_le/uIoo_of_le are in Set namespace presumably (Set.uIcc_of_le) — vendored used bare with open Set. In my helper I'll use `Set.uIcc_of_le hre` etc. — but vendored wrote `simpa [uIcc_of_le hre] using h1` with open Set. Since LiPrincipal/LiResidue don't open Set, let me check: is `uIcc_of_le` accessible without open Set? It's `Set.uIcc_of_le` — need qualification. Hmm wait — actually in LiPrincipal: `mapsTo_rectangleBorder_left_im z w` was used bare with open Zeta23 — that's Zeta23's lemma ✓. For uIcc_of_le I'll write Set.uIcc_of_le explicitly. And `Set.uIoo_of_le`. And mem_union → Set.mem_union, mem_singleton_iff → Set.mem_singleton_iff. `not_or` is root ✓.\n\nActually, simpler: add `open Set` to my file? Risk: name clashes — `Set.Ioo`, `Set.toFinset`... The main risk: `Set.indicator`... none of my names clash. But `open Set` might make `Finset.range` ambiguous? No. Common Mathlib files open Set widely. But minimal-risk: qualify with Set. prefix. RectangleBorder is Zeta23.RectangleBorder? It's in Zeta23 namespace? Rectangle.lean — namespace? The file Zeta23/FromPNTPlus/Rectangle.lean — vendored usage `RectangleBorder` bare with open Zeta23 — so it's Zeta23.RectangleBorder or root? LiPrincipal used `RectangleBorder` bare with open Zeta23 ✓ so Zeta23.RectangleBorder (or wherever, resolved via open Zeta23). Same for Rectangle, rectangle_mem_nhds_iff, not_mem_rectangleBorder_of_rectangle_mem_nhds, rectangleBorder_subset_rectangle, mapsTo_rectangleBorder_* ✓ all resolve via open Zeta23 as in LiPrincipal.\n\n`Set.uIcc_of_le : a ≤ b → [[a, b]] = Icc a b` — hmm [[ ]] is uIcc notation — Set.uIcc_of_le ✓. `Set.uIoo_of_le : a ≤ b → [[a,b]]... uIoo` — uIoo_of_le : a ≤ b → Ιoo a b = Ioo a b ✓ Set namespace.\n\nOK. Also `mem_reProdIm` — with open Complex ✓ bare works.\n\nNow — the RectangleBorder destructuring in my helper: RectangleBorder z w := [[z.re, w.re]] ×ℂ {z.im} ∪ {z.re} ×ℂ [[z.im, w.im]] ∪ [[z.re, w.re]] ×ℂ {w.im} ∪ {w.re} ×ℂ [[z.im, w.im]] — the simp only [RectangleBorder, ...] at hb — RectangleBorder is a def — simp only [RectangleBorder] unfolds via equation lemma ✓ (vendored did simp only [RectangleBorder, mem_union, mem_reProdIm, mem_singleton_iff, not_or] at hρB ✓ — I'll qualify: simp only [RectangleBorder, Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff, not_or] at hb — wait, with open Complex, `mem_reProdIm` resolves; with open Set absent, mem_union needs Set. prefix. Mixed qualification in one simp call is fine.)\n\nHmm — actually mem_reProdIm: membership z ∈ s ×ℂ t — the sides are like [[z.re, w.re]] ×ℂ {z.im} — p ∈ that ↔ p.re ∈ [[z.re,w.re]] ∧ p.im ∈ {z.im} — then Set.mem_singleton_iff: p.im ∈ {z.im} ↔ p.im = z.im ✓.\n\nWait, one subtlety: {z.re} ×ℂ [[z.im, w.im]] — p ∈ it ↔ p.re ∈ {z.re} ∧ p.im ∈ [[z.im,w.im]] → p.re = z.re ∧ p.im ∈ uIcc ✓.\n\nSo hb after simp: ¬(p.re ∈ uIcc ∧ p.im = z.im) ∧ ¬(p.re = z.re ∧ p.im ∈ uIcc) ∧ ¬(p.re ∈ uIcc ∧ p.im = w.im) ∧ ¬(p.re = w.re ∧ p.im ∈ uIcc) — destructured ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ ✓ matches vendored.\n\nThe simp only normal form of ¬(A ∪ B): not_or : ¬(a ∨ b) ↔ ¬a ∧ ¬b — membership in A ∪ B is A-mem ∨ B-mem via Set.mem_union ✓ so ¬(mem ∨ mem) → ∧ via not_or ✓. But simp only [not_or] rewrites ¬(a∨b) to ¬a ∧ ¬b ✓ repeated ✓. The nesting: ((S1 ∪ S2) ∪ S3) ∪ S4 — mem: (((m1 ∨ m2) ∨ m3) ∨ m4) — negated: ¬(((m1∨m2)∨m3)∨m4) → not_or: ¬((m1∨m2)∨m3) ∧ ¬m4 → (¬(m1∨m2) ∧ ¬m3) ∧ ¬m4 → ((¬m1 ∧ ¬m2) ∧ ¬m3) ∧ ¬m4 ✓ ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ ✓.\n\nBUT — simp only might further simplify ¬(p.im = z.im) to p.im ≠ z.im (ne_eq?) — with only the listed lemmas, no ne_eq included — stays ¬(... = ...) ✓ (vendored didn't include ne_eq and destructured fine ✓).\n\nThe final rw [rectangle_mem_nhds_iff, mem_reProdIm, uIoo_of_le hre, uIoo_of_le him]: goal Rectangle z w ∈ 𝓝 p → after rw [rectangle_mem_nhds_iff]: p ∈ uIoo z.re w.re ×ℂ uIoo z.im w.im → rw [Complex.mem_reProdIm]: p.re ∈ uIoo ... ∧ p.im ∈ uIoo ... → rw [Set.uIoo_of_le hre, Set.uIoo_of_le him]: p.re ∈ Ioo z.re w.re ∧ p.im ∈ Ioo z.im w.im — then mem_Ioo: the refine ⟨⟨_, _⟩, ⟨_, _⟩⟩ — vendored's refine produced the structure directly: ⟨⟨lt..., lt...⟩, ⟨lt..., lt...⟩⟩ — mem_Ioo is defeq to the pair ✓ anonymous constructor ✓ copy.\n\nuIoo_of_le signature: Set.uIoo_of_le (h : a ≤ b) : uIoo a b = Ioo a b ✓.\n\nNow, let me also confirm `Set.uIcc_of_le`: vendored `simpa [uIcc_of_le hre] using h1` — h1 : p.re ∈ [[z.re, w.re]] — [[ ]] = Set.uIcc — uIcc_of_le hre : uIcc z.re w.re = Icc z.re w.re — simpa [Set.uIcc_of_le hre] using h1 : z.re ≤ p.re ∧ p.re ≤ w.re — after rewriting uIcc → Icc, h1 : p.re ∈ Icc ... — simp [mem_Icc] gives the ∧ — vendored's simpa [uIcc_of_le hre] using h1 produced h1' : z.re ≤ p.re ∧ p.re ≤ w.re directly — the simp must also unfold mem_Icc — simpa [uIcc_of_le hre] using h1 — h1 : p.re ∈ uIcc — after simp with uIcc_of_le: p.re ∈ Icc — and then simp's default lemmas include Set.mem_Icc? mem_Icc is a simp lemma ✓ (iff form) — simpa uses full simp with the given lemmas + default simp set? NO — simpa [X] using e = simp [X] at e ⊢ then match — full simp ✓ includes mem_Icc ✓. OK so `simpa [Set.uIcc_of_le hre] using h1` ✓.\n\nLet me now write the complete file. One more scan of the main theorem for the `exacts [h1, hSzint p hp]` — after rcases with rfl | hp: first goal: Rectangle z w ∈ 𝓝 1 — wait NO: the rcases pattern `rcases hp with rfl | hp` where hp : p = 1 ∨ p ∈ Sz — the rfl: p = 1 substituted — goal: Rectangle z w ∈ 𝓝 1 ✓ exact h1. Hmm — but with `insert 1 Sz`, mem_insert gives p = 1 ∨ p ∈ Sz ✓ — rfl substitutes p := 1 ✓ (or 1 := p — p is a local var so p := 1 ✓ — wait hp : p = 1 — rfl can substitute either direction; Lean picks subst p (replacing p by 1) ✓ since p is a free local and 1 is not).\n\nexacts [h1, hSzint p hp] — after rcases the second branch's hp : p ∈ Sz — hSzint p hp ✓. But wait — in the second branch, is p still named p? Yes ✓.\n\nFor the hS argument I wrote it inline as (by intro p hp; rw [Finset.mem_insert] at hp; rcases hp with rfl | hp; exacts [h1, hSzint p hp]) — fine.\n\nresidueTheorem_finset explicit args: theorem residueTheorem_finset {f : ℂ → ℂ} {z w : ℂ} (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (S : Finset ℂ) (A : ℂ → ℂ) (hS : ...) (fHolo : ...) (near : ...) — so: Analytic.residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A hS fHolo near ✓.\n\nNamespace: residueTheorem_finset is inside `namespace Zeta23 / namespace Analytic` — full name Zeta23.Analytic.residueTheorem_finset — with open Zeta23: Analytic.residueTheorem_finset ✓.\n\nNow write the file. Also update NguyenRH1.lean root to import LiSides (add after LiBasePoints — wait, actually LiResidue/LiPrincipal aren't in the root either! The root imports LiSkeleton, LiBasePoints, SuzukiSkeleton, ValleySkeleton — LiResidue/LiPrincipal (session 016) were NOT added to the root! Let me check how session 016 built — maybe they build files individually with `lake env lean`. The root NguyenRH1.lean doesn't import LiResidue/LiPrincipal — interesting. For the full `lake build` to check LiSides, either add to root or build the file directly. Session 016's commit — did they add to root? The root shown above (read just now) has only 4 imports — so LiResidue/LiPrincipal are NOT in the root. They must build via `lake env lean NguyenRH1/LiResidue.lean`. Hmm — but a full `lake build` builds the library target — does the library target include all files or just the root closure? Lean builds only what's imported from the root lib target. So LiResidue/LiPrincipal might not be covered by lake build! Session 016's handoff says \"Iterate single-file with lake env lean NguyenRH1/LiSkeleton.lean from the package dir\" — they iterate single-file. And session 015 did \"Full rebuild GREEN (8741 jobs, zero downstream changes)\" — 8741 jobs — probably `lake build` after adding liSummable to LiSkeleton (which IS in the root closure). LiResidue/LiPrincipal (session 016, 2 commits) — possibly only single-file checked!\n\nFor robustness I should: (1) add LiResidue, LiPrincipal, LiSides to the root NguyenRH1.lean (that's adding imports — allowed; not editing proofs), (2) run full lake build to verify everything green.\n\nWait — freeze protocol: \"no edits to existing Lean proofs except the liCoeff correctness fix\". Adding import lines to the root file is not editing a proof ✓. And session 016 presumably intended the root to eventually include them. Adding all three imports keeps the full build honest. Let me do that (add LiResidue, LiPrincipal, LiSides imports to the root).\n\nHmm — but let me first check whether session 016 added them elsewhere... the root file I just read has only 4 imports, dated from session 012-ish. I'll add the 3 missing ones (order: LiSkeleton, LiBasePoints, LiResidue, LiPrincipal, LiSides, ...). \n\nNow write LiSides.lean.","signature":""},{"type":"text","text":"Now writing `LiSides.lean` — the rectangle residue theorem for J. Marking inventory done."},{"type":"tool_use","id":"TodoWrite_31","name":"TodoWrite","input":{"todos":[{"content":"Inventory: LiSkeleton conventions, Mathlib riemannZeta@1, zero finiteness machinery","status":"completed","activeForm":"Inventorying LiSkeleton conventions and Mathlib facts"},{"content":"Build LiSides.lean: Jlag def + holomorphicity off {1}∪zeros","status":"in_progress","activeForm":"Building Jlag definition and holomorphicity lemmas"},{"content":"Prove R = J − ppart holomorphic at 1 (removable, Taylor-remainder order)","status":"pending","activeForm":"Proving removability of R at w=1"},{"content":"Prove residue-at-zero lemma (logDeriv NF, simple poles, residue mult·(1−(ρ/(ρ−1))ⁿ))","status":"pending","activeForm":"Proving residue at zeros"},{"content":"Assemble rectangle residue theorem for J via residueTheorem_finset + rectInt'_ppart","status":"pending","activeForm":"Assembling sides(T) theorem"},{"content":"Build green + axiom audit + commit; journal/STATE/checklist updates","status":"pending","activeForm":"Building, auditing, committing"}]},"extra_content":null},{"type":"tool_use","id":"Write_32","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSides.lean","content":"/-\nNguyenRH1/LiSides.lean — tier ii′ sub-stage ii′-1b(iii) (D-064 §4 R1):\nthe rectangle residue theorem for the Lagarias-kernel integrand\n\n  J(w) = kFun n w · (−ζ′/ζ(w)),   kFun n w = (w/(w−1))ⁿ − 1   (= k_n(w−1)).\n\nJ is meromorphic on ℂ with: a pole of order n+1 at w = 1 (residue `ResW1 n`,\nsession 016), simple poles at every zero ρ of ζ with residue\nmult(ρ)·(1 − (ρ/(ρ−1))ⁿ) (logDeriv poles are simple; multiple zeros OK).\n\nMethod (D-064 §4 R1): subtract the explicit principal part `ppart n` at 1\n(session 016). The remainder R = J − P is:\n* holomorphic off {1} ∪ {zeros of ζ} (product/quotient rule),\n* BOUNDED near 1 (`Rfun_bounded_near_one`): on a punctured neighbourhood,\n  (w−1)^{n+1}·R = F − TaylₙF where F(w) = (wⁿ−(w−1)ⁿ)·hLi(w) is analytic\n  at 1 (`hLi_analyticAt_one`), and F − TaylₙF vanishes to order ≥ n+1\n  (`Ffun_sub_TaylP_order`, via `natCast_le_analyticOrderAt_iff_\n  iteratedDeriv_eq_zero`), so R extends continuously across 1;\n* simple-poled at each zero ρ with the residue above (`Rfun_residue_at`,\n  via the analytic-order normal form ζ = (w−ρ)^m·h, h(ρ) ≠ 0).\n\nThen the vendored `residueTheorem_finset` (Zeta23.Analytic.RectangleLogDeriv)\nplus session 016's `rectInt'_ppart` give `rectInt'_Jlag`:\nfor any rectangle with 1 interior and no zeros of ζ on the border,\n\n  RectangleIntegral' (Jlag n) z w\n    = ResW1 n + Σ_{ρ ∈ Sz} (zeroMult ρ)·(1 − (ρ/(ρ−1))ⁿ),\n\nwhere Sz is any finset exactly capturing the zeros of zetaA (equivalently,\noff 1, of ζ) inside the rectangle — produced downstream by the vendored\n`finite_zeros_rectangle` (zetaA is entire, `zetaA_analyticAt_one`).\n\nNOTE (deferred): the value mult(−2) = 1 (simplicity of the trivial zeros)\nis NOT proved here; the sum keeps `zeroMult ρ` symbolic at trivial zeros.\nThe split Sz = {nontrivial zeros} ∪ {−2} on the D-064 rectangle\n(σ ∈ [−5/2, 2√n]) is ii′-4 territory.\n\nArchive references: D-036, D-037, D-064 (R1), journal-015/016.\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/-! ## 1. The integrand: kFun, Jlag, Rfun -/\n\n/-- The kernel factor kFun n w = (w/(w−1))ⁿ − 1 (= k_n(w−1) with\nk_n(x) = (1+1/x)ⁿ − 1). Pole of order n at w = 1, analytic elsewhere. -/\ndef kFun (n : ℕ) (s : ℂ) : ℂ := (s / (s - 1)) ^ n - 1\n\n/-- The Lagarias-kernel integrand J(w) = kFun n w · (−ζ′/ζ(w)) (D-064 §2). -/\ndef Jlag (n : ℕ) (s : ℂ) : ℂ := kFun n s * (-(deriv riemannZeta s / riemannZeta s))\n\n/-- The remainder R = J − P with P the principal part at 1 (LiPrincipal). -/\ndef Rfun (n : ℕ) : ℂ → ℂ := Jlag n - ppart n\n\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\nlemma ppart_differentiableAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    DifferentiableAt ℂ (ppart n) s := by\n  rw [show (ppart n) = ∑ i ∈ Finset.Icc 1 (n + 1),\n      (fun w : ℂ => Acoeff n i / (w - 1) ^ i) from by\n    funext w; simp [ppart, 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\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\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\nlemma ppart_continuousAt {n : ℕ} {s : ℂ} (hs : s ≠ 1) :\n    ContinuousAt (ppart n) s := by\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 =>\n      simp only [Finset.sum_empty]\n      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/-! ## 2. Finite order of ζ at every point ≠ 1 (via the entire zetaA) -/\n\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\n/-- ζ has finite analytic order at every ρ ≠ 1 (identity principle through\nthe entire function zetaA = (w−1)ζ, which is nonzero at 1). -/\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\n/-! ## 3. Interior points from border avoidance -/\n\n/-- A point of the rectangle not on its border is interior (the rectangle is\na neighbourhood of it). Extracted from the vendored hZint argument. -/\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 [Set.uIcc_of_le hre] using h1\n  have h2' : z.im ≤ p.im ∧ p.im ≤ w.im := by simpa [Set.uIcc_of_le him] using h2\n  simp only [RectangleBorder, Set.mem_union, Complex.mem_reProdIm, Set.mem_singleton_iff,\n    not_or] at hb\n  obtain ⟨⟨⟨hb1, hb2⟩, hb3⟩, hb4⟩ := hb\n  rw [rectangle_mem_nhds_iff, Complex.mem_reProdIm, Set.uIoo_of_le hre, Set.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\n/-! ## 4. The removable singularity of R at w = 1 -/\n\n/-- F(w) = (wⁿ−(w−1)ⁿ)·hLi(w) — the analytic-at-1 numerator (w−1)^{n+1}·J\n(punctured). Same function as in `ResW1`/`Acoeff` (defeq). -/\ndef Ffun (n : ℕ) (w : ℂ) : ℂ := (w ^ n - (w - 1) ^ n) * hLi w\n\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\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\nlemma TaylP_analyticAt (n : ℕ) (w : ℂ) : AnalyticAt ℂ (TaylP n) w := by\n  have hterm : ∀ j : ℕ, AnalyticAt ℂ\n      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w :=\n    fun j => analyticAt_const.mul ((analyticAt_id.sub analyticAt_const).pow j)\n  have : ∀ t : Finset ℕ, AnalyticAt ℂ\n      (fun w : ℂ => ∑ j ∈ t, (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) w := by\n    intro t\n    induction t using Finset.induction with\n    | empty =>\n      simp only [Finset.sum_empty]\n      exact analyticAt_const\n    | insert a t hat ht =>\n      simp_rw [Finset.sum_insert hat]\n      exact (hterm a).add ht\n  exact this _\n\n/-- (w−1)^{n+1}·ppart n w is the Taylor polynomial of Ffun n at 1 (w ≠ 1). -/\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  show (s - 1) ^ (n + 1) * (∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (s - 1) ^ i) =\n    ∑ j ∈ Finset.range (n + 1), (iteratedDeriv j (Ffun n) 1 / j !) * (s - 1) ^ j\n  rw [Finset.mul_sum]\n  apply Finset.sum_bij (fun i _ => n + 1 - i)\n  · intro i hi\n    rw [Finset.mem_Icc] at hi\n    rw [Finset.mem_range]\n    omega\n  · intro a₁ ha₁ a₂ ha₂ h\n    rw [Finset.mem_Icc] at ha₁ ha₂\n    omega\n  · intro j hj\n    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    have hA : Acoeff n i = iteratedDeriv (n + 1 - i) (Ffun n) 1 / (n + 1 - i) ! := rfl\n    rw [hA]\n    have e : (s - 1) ^ (n + 1) = (s - 1) ^ i * (s - 1) ^ (n + 1 - i) := by\n      rw [← pow_add]; congr 1; omega\n    have key : ∀ C : ℂ, (s - 1) ^ (n + 1) * (C / (s - 1) ^ i) = C * (s - 1) ^ (n + 1 - i) := by\n      intro C\n      have hi' : (s - 1) ^ i ≠ 0 := pow_ne_zero i hs1\n      rw [e]\n      field_simp [hi']\n      ring\n    exact key _\n\n/-- (w−1)^{n+1}·Jlag n w = Ffun n w off 1 and off the zeros of ζ. -/\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 h2 : (s - 1) ^ n ≠ 0 := pow_ne_zero n h1\n  have hk : kFun n s = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n := by\n    show (s / (s - 1)) ^ n - 1 = (s ^ n - (s - 1) ^ n) / (s - 1) ^ n\n    rw [div_pow]\n    field_simp [h2]\n  show (s - 1) ^ (n + 1) * (kFun n s * (-(deriv riemannZeta s / riemannZeta s))) =\n    (s ^ n - (s - 1) ^ n) * hLi s\n  rw [hk, hLi_eq_of_ne hs1 hs0, pow_succ]\n  field_simp [h2, hs0]\n  ring\n\n/-- On a punctured neighbourhood of 1, R n = (Ffun n − TaylP n)/(w−1)^{n+1}. -/\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 := hs1\n  have h1 : (s - 1) ^ (n + 1) ≠ 0 := pow_ne_zero _ (sub_ne_zero.mpr hs1')\n  have e : (s - 1) ^ (n + 1) * Rfun n s = Ffun n s - TaylP n s := by\n    have e1 := Jlag_mul_pow hs1' hs0\n    have e2 := ppart_mul_pow hs1'\n    show (s - 1) ^ (n + 1) * (Jlag n s - ppart n s) = Ffun n s - TaylP n s\n    rw [mul_sub, e1, e2]\n  exact eq_div_of_mul_eq h1 (by rw [mul_comm]; exact e)\n\n/-- The i-th iterated derivative of the Taylor polynomial at 1 matches\nFfun's (i ≤ n): the j ≠ i summands vanish by the descFactorial/0^k split. -/\nlemma iteratedDeriv_TaylP {n i : ℕ} (hi : i ≤ n) :\n    iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1 := by\n  have hterm : ∀ j ∈ Finset.range (n + 1),\n      ContDiffAt ℂ i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 :=\n    fun j _ => contDiffAt_const.mul (((contDiff_id.sub contDiff_const).pow j).contDiffAt)\n  have hdp : ∀ j : ℕ, iteratedDeriv i (fun w : ℂ => (w - 1) ^ j) (1 : ℂ) =\n      (j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i) := by\n    intro j\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  rw [show (TaylP n) = ∑ j ∈ Finset.range (n + 1),\n      (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) from by\n    funext w; simp [TaylP, Finset.sum_apply]]\n  rw [iteratedDeriv_sum hterm]\n  have hpoint : ∀ j ∈ Finset.range (n + 1),\n      iteratedDeriv i (fun w : ℂ => (iteratedDeriv j (Ffun n) 1 / j !) * (w - 1) ^ j) 1 =\n        (iteratedDeriv j (Ffun n) 1 / j !) * ((j.descFactorial i : ℂ) * (0 : ℂ) ^ (j - i)) := by\n    intro j hj\n    rw [iteratedDeriv_const_mul_field, hdp j]\n  rw [Finset.sum_congr rfl hpoint]\n  rw [Finset.sum_eq_single i]\n  · have hfi : ((i ! : ℕ) : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero i)\n    rw [Nat.descFactorial_self]\n    simp only [Nat.sub_self, pow_zero, mul_one]\n    exact div_mul_cancel₀ _ hfi\n  · intro j hj hji\n    rw [Finset.mem_range] at hj\n    by_cases hlt : j < i\n    · have h0 : (j.descFactorial i : ℂ) = 0 := by\n        have h := Nat.descFactorial_eq_zero_iff_lt.mpr hlt\n        exact_mod_cast h\n      simp [h0]\n    · have h0 : (0 : ℂ) ^ (j - i) = 0 := zero_pow (by omega)\n      simp [h0]\n  · intro hi'\n    rw [Finset.mem_range] at hi'\n    omega\n\n/-- Ffun n − TaylP n vanishes to order ≥ n+1 at 1. -/\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, iteratedDeriv_TaylP hi, sub_self]\n\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  exact Ffun_sub_TaylP_iteratedDeriv n i (Nat.lt_succ_iff.mp hi)\n\n/-- R converges at 1 along the punctured filter (the would-be residue value). -/\nlemma Rfun_tendsto_one (n : ℕ) :\n    ∃ L : ℂ, Tendsto (Rfun n) (𝓝[≠] (1 : ℂ)) (𝓝 L) := by\n  have hgan : AnalyticAt ℂ (Ffun n - TaylP n) 1 :=\n    (Ffun_analyticAt_one n).sub (TaylP_analyticAt n 1)\n  have hord : ((n + 1 : ℕ) : ℕ∞) ≤ analyticOrderAt (Ffun n - TaylP n) 1 :=\n    Ffun_sub_TaylP_order n\n  by_cases htop : analyticOrderAt (Ffun n - TaylP n) 1 = ⊤\n  · refine ⟨0, ?_⟩\n    have h0 : ∀ᶠ s in 𝓝 (1 : ℂ), (Ffun n - TaylP n) 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, mem_nhdsWithin_of_mem_nhds h0] with s hs hg0\n      have hg0' : Ffun n s - TaylP n s = 0 := hg0\n      rw [hs, hg0']\n      exact zero_div _\n    exact tendsto_const_nhds.congr' hev.symm\n  · obtain ⟨h, hh, hh0, hfh⟩ := hgan.analyticOrderAt_ne_top.mp htop\n    have hnm : n + 1 ≤ analyticOrderNatAt (Ffun n - TaylP n) 1 := by\n      rw [← Nat.cast_analyticOrderNatAt htop] at hord\n      exact ENat.natCast_le_natCast.mp hord\n    have hev : ∀ᶠ s in 𝓝[≠] (1 : ℂ),\n        Rfun n s = (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (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 := hs1\n      have hs1n : s - 1 ≠ 0 := sub_ne_zero.mpr hs1'\n      rw [hs]\n      have hgs : (Ffun n - TaylP n) s =\n          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := by\n        have h2 := hgf.self_of_nhds\n        rwa [smul_eq_mul] at h2\n      have hgs' : Ffun n s - TaylP n s =\n          (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 * h s := hgs\n      rw [hgs']\n      have e : (s - 1) ^ analyticOrderNatAt (Ffun n - TaylP n) 1 =\n          (s - 1) ^ (n + 1) *\n            (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) := by\n        rw [← pow_add]\n        congr 1\n        omega\n      rw [e, mul_assoc, mul_div_cancel_left₀ (pow_ne_zero (n + 1) hs1n)]\n    refine ⟨(1 - 1 : ℂ) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h 1, ?_⟩\n    have hcont : ContinuousAt\n        (fun s : ℂ => (s - 1) ^ (analyticOrderNatAt (Ffun n - TaylP n) 1 - (n + 1)) * h s) 1 :=\n      ((continuousAt_id.sub continuousAt_const).pow _).mul hh.continuousAt\n    exact (hcont.tendsto.mono_left nhdsWithin_le_nhds).congr' hev.symm\n\n/-- The near-condition at 1 with residue 0: R is bounded on the punctured\nneighbourhood (the singularity is removable). -/\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\n/-! ## 5. The residue at a zero of ζ -/\n\n/-- At any ρ ≠ 1, R has at worst a simple pole with residue\nzeroMult(ρ)·(1 − (ρ/(ρ−1))ⁿ) (zero if ζ(ρ) ≠ 0). Via the order normal form\nζ = (w−ρ)^m·h near ρ: −ζ′/ζ = −m/(w−ρ) − h′/h, and the kFun slope and the\nprincipal part are continuous at ρ. -/\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  have hkd : DifferentiableAt ℂ (kFun n) ρ := kFun_differentiableAt hρ\n  have hexp : ∀ᶠ s in 𝓝[≠] ρ,\n      (-(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))\n          - 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 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 hA : (zeroMult ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =\n        -(analyticOrderNatAt riemannZeta ρ : ℂ) * kFun n ρ := by\n      have hmz : (zeroMult ρ : ℂ) = (analyticOrderNatAt riemannZeta ρ : ℂ) := rfl\n      rw [hmz]\n      show (analyticOrderNatAt riemannZeta ρ : ℂ) * (1 - (ρ / (ρ - 1)) ^ n) =\n        -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((ρ / (ρ - 1)) ^ n - 1)\n      ring\n    simp only [Pi.sub_apply, Rfun, Jlag, hA]\n    rw [← logDeriv_apply, hld]\n    field_simp [hsρ']\n    ring\n  have hslope : Tendsto (fun s => (kFun n s - kFun n ρ) / (s - ρ)) (𝓝[≠] ρ)\n      (𝓝 (deriv (kFun n) ρ)) := by\n    have h2 := hasDerivAt_iff_tendsto_slope.mp hkd.hasDerivAt\n    simpa only [slope_fun_def_field] using h2\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 * (deriv h s / h s)) ρ :=\n      hkd.continuousAt.mul (hh.deriv.continuousAt.div hh.continuousAt hh0)\n    simpa only [logDeriv_apply] using 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 hT : Tendsto\n      (fun s => -(analyticOrderNatAt riemannZeta ρ : ℂ) * ((kFun n s - kFun n ρ) / (s - ρ))\n        - kFun n s * logDeriv h s - ppart n s)\n      (𝓝[≠] ρ)\n      (𝓝 (-(analyticOrderNatAt riemannZeta ρ : ℂ) * deriv (kFun n) ρ\n        - kFun n ρ * logDeriv h ρ - ppart n ρ)) :=\n    ((hslope.const_mul _).sub hcont1).sub hcont2\n  exact (hT.isBigO_one ℂ).congr' hexp EventuallyEq.rfl\n\n/-! ## 6. The rectangle residue theorem for J -/\n\n/-- **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\n    = ResW1 n + Σ_{ρ ∈ Sz} (zeroMult ρ)·(1 − (ρ/(ρ−1))ⁿ),\nwhere Sz captures exactly the zeros of zetaA (⟺ zeros of ζ off 1) inside. -/\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  classical\n  have hzA1 : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num\n  have h1notSz : (1 : ℂ) ∉ Sz := fun h => hzA1 ((hSz 1).mp h).2\n  have hSz_ne_one : ∀ ρ ∈ Sz, ρ ≠ 1 := fun ρ hρ h => h1notSz (h ▸ hρ)\n  have hSz_zeta : ∀ ρ ∈ Sz, riemannZeta ρ = 0 := by\n    intro ρ hρ\n    have hρ1 := hSz_ne_one ρ hρ\n    have h2 := ((hSz ρ).mp hρ).2\n    rw [zetaA_apply hρ1, mul_eq_zero] at h2\n    rcases h2 with h | h\n    · exact absurd (sub_eq_zero.mp h) hρ1\n    · exact h\n  have hSzint : ∀ ρ ∈ Sz, Rectangle z w ∈ 𝓝 ρ := by\n    intro ρ hρ\n    exact rectangle_mem_nhds_of_mem_not_border hre him ((hSz ρ).mp hρ).1\n      (fun hb => hborder ρ hb (hSz_zeta ρ hρ))\n  set A : ℂ → ℂ := fun p => if p = 1 then 0 else (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n)\n    with hAdef\n  have fHolo : HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert (1 : ℂ) Sz)) := by\n    intro s hs\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    have hs0 : riemannZeta s ≠ 0 := by\n      intro h0\n      exact hsSz ((hSz s).mpr ⟨hs.1, by rw [zetaA_apply hs1, h0, mul_zero]⟩)\n    exact (Rfun_differentiableAt hs1 hs0).differentiableWithinAt\n  have key := Analytic.residueTheorem_finset (f := Rfun n) hre him (insert 1 Sz) A\n    (by\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    fHolo\n    (by\n      intro p hp\n      rw [Finset.mem_insert] at hp\n      rcases hp with rfl | hp\n      · simpa [hAdef] using Rfun_bounded_near_one n\n      · have hp1 : p ≠ 1 := hSz_ne_one p hp\n        have hAp : A p = (zeroMult p : ℂ) * (1 - (p / (p - 1)) ^ n) := by simp [hAdef, hp1]\n        rw [hAp]\n        exact Rfun_residue_at n hp1)\n  have hsum : ∑ p ∈ insert 1 Sz, A p =\n      ∑ ρ ∈ 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  have hRint : RectangleBorderIntegrable (Rfun n) z w := by\n    apply ContinuousOn.rectangleBorder_integrable\n    apply fHolo.continuousOn.mono\n    intro s hs\n    have hsR : s ∈ Rectangle z w := rectangleBorder_subset_rectangle z w hs\n    refine ⟨hsR, fun hsc => ?_⟩\n    rw [Finset.mem_coe, Finset.mem_insert] at hsc\n    rcases hsc with h | h\n    · exact not_mem_rectangleBorder_of_rectangle_mem_nhds h1 (h ▸ hs)\n    · exact hborder s hs (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  have heq : Jlag n = Rfun n + ppart n := (sub_add_cancel _ _).symm\n  rw [heq, RectangleIntegral'_add _ _ _ _ hRint hPint, key, rectInt'_ppart hre him h1]\n  ring\n\nend NguyenRH1\n"},"extra_content":null}]