[{"type":"thinking","thinking":"`riemannZeta 1 = (γ − log(4π))/2` — a real number ≈ (0.5772 − 2.5310)/2 ≈ −0.977 ≠ 0. So riemannZeta 1 ≠ 0 (it's a junk/totalized value, but nonzero). Good — 1 ∉ ζ⁻¹'{0}, so S := Rectangle ∩ ζ⁻¹'{0} does NOT contain 1. But to be safe in Lean I'd need to prove riemannZeta 1 ≠ 0 — from riemannZeta_one and γ − log(4π) ≠ 0. That's provable: log(4π) > log(e²) = 2 > γ? Hmm, γ < 1 and log(4π) > log 4 > 1... Provable with some numeric bounds. Might be slightly annoying but doable. Alternatively, define S := Rectangle ∩ ζ⁻¹'{0} ∩ {1}ᶜ — no wait, if riemannZeta 1 ≠ 0 then 1 ∉ the preimage anyway.\n\nHmm wait, actually — is it important? If 1 ∈ S (if ζ(1) were 0), the sum term at 1 would be wrong. Since ζ(1) = (γ−log 4π)/2 ≠ 0, 1 ∉ ζ⁻¹'{0} — so S automatically excludes 1. I need this as a lemma: `riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0`. To prove: rw riemannZeta_one, then show (γ − log(4π))/2 ≠ 0, i.e., γ ≠ log(4π). There should be bounds: Real.eulerMascheroniConstant_lt_one or similar; log(4π) ≥ log 12 > 1... Need `Real.log` lower bound: 4π > e? 4π > 12 > e? log(4π) > 1 iff 4π > e — π > e/4, true since π > 3. Mathlib has `Real.pi_gt_314` etc. So: log(4π) = log 4 + log π ≥ ... 4π ≥ 12 > e ⟹ log(4π) > 1 ≥ γ ⟹ ≠. Mathlib: `Real.eulerMascheroniConstant_lt_one`? Let me check during implementation.\n\nWait, actually — hmm, but hold on. Do I even want S := Rectangle ∩ ζ⁻¹'{0}? This includes ALL zeros: nontrivial AND trivial (−2, −4, ...). For the generic theorem that's fine. The residue formula analyticOrderNatAt ζ ρ · (1−(ρ/(ρ−1))ⁿ) applies to all of them uniformly. But wait — for the formula to be right, I need analyticOrderAt ζ ρ ≠ ⊤ (i.e., ζ not locally ≡ 0). Since ζ is not identically zero on any open set (analytic on ℂ∖{1}, and e.g. ζ(2) ≠ 0... more precisely analyticOrderAt_ne_top needs ζ to not vanish on a neighborhood of ρ — from the identity principle; Zeta23's one_le_mult gives 1 ≤ zeroMult ρ for nontrivial zeros — which itself encodes analyticOrderAt ≠ ⊤... toNat of ⊤ is 0, so 1 ≤ toNat means order ≠ ⊤ AND ≠ 0... wait zeroMult ρ = (analyticOrderAt ζ ρ).toNat; 1 ≤ that requires analyticOrderAt ≠ ⊤ and ≠ 0).\n\nFor an ARBITRARY zero ρ ∈ ζ⁻¹'{0} (not necessarily nontrivial, could be trivial −2k), I need analyticOrderAt ζ ρ ≠ ⊤ as well. Same argument: if ζ vanished on a neighborhood of ρ, by the identity theorem on the connected open ℂ∖{1}, ζ ≡ 0 on ℂ∖{1}, contradicting ζ(2) ≠ 0 (say). In Lean: `analyticOrderAt_eq_top` gives ∀ᶠ s in 𝓝 ρ, ζ s = 0. Then... the identity principle: AnalyticOnNhd ζ (ℂ∖{1}) (connected) + vanishing on a nhd of a point in it ⟹ vanishes everywhere on it — but ζ(2) ≠ 0 (from the Euler product or the series: ζ(2) = π²/6 ≠ 0 — Mathlib has `riemannZeta_two`? There's `riemannZeta_two : riemannZeta 2 = π^2/6` I believe... or use hasSum_zeta_nat... there might be `riemannZeta_ne_zero_of_one_lt_re`? Actually simpler: for Re s > 1, ζ s ≠ 0 — Mathlib: `riemannZeta_ne_zero_of_one_le_re`? or via the Euler product `riemannZeta_eulerProduct`... I recall `riemannZeta_ne_zero_of_one_lt_re : 1 < s.re → riemannZeta s ≠ 0` exists in Mathlib. Yes, I'm fairly confident that exists.\n\nBut the identity-principle route for generic zeros: is there a Zeta23 lemma? Zeta23 has the zero set with finite_window etc. via a structure... Actually for the trivial zeros, is there `analyticOrderAt riemannZeta (-2k)` known? Hmm.\n\nAlternative cleaner approach: instead of ALL zeros in the rectangle, use S := {nontrivial zeros in rectangle} ∪ {trivial zeros −2k in rectangle}. Both need the order-≠-⊤ fact at trivial zeros.\n\nEven simpler: **prove the residue lemma at any point ρ with ρ ≠ 1 and analyticOrderAt ζ ρ ≠ ⊤** — that's all the \"near\" condition needs:\n- At such ρ: near ρ, ζ = (s−ρ)^m·h, h analytic h(ρ) ≠ 0 (m could be 0 — then ζ(ρ) ≠ 0 and R is analytic at ρ, residue 0 = m·(...) ✓ still consistent!). \n\nOh nice — the \"near\" condition at a point where ζ(ρ) ≠ 0: R − 0/(s−ρ) = R bounded near ρ ✓ (R continuous there since ρ ≠ 1 and ζ(ρ) ≠ 0). So the residue formula A(ρ) = m·(1−(ρ/(ρ−1))ⁿ) is valid for ALL ρ ≠ 1 with order ≠ ⊤, including non-zeros (m = 0). So S can be ANY finset of interior points avoiding... hmm no — fHolo needs R holomorphic on Rectangle ∖ S; R is holomorphic at all points except 1 and zeros; so Rectangle ∖ S must avoid 1 and all zeros — i.e., S must contain ALL zeros in the rectangle. And S must not contain 1 (else... actually 1 ∈ S would break fHolo? No: 1 ∈ S EXCLUDES 1 from the domain Rectangle ∖ S — that HELPS because R isn't holomorphic at 1 (as a bare function with junk value at 1)). Wait wait.\n\nHold on — R at 1: R(1) = Jlag(1) − ppart(1) = junk. Is R differentiable at 1? R is \"meromorphic with removable singularity\" at 1 but the bare definition gives R(1) = 0 (junk) while lim R = L (the true value). Unless L = 0, R is not continuous at 1, hence not holomorphic at 1. So for `HolomorphicOn R (Rectangle ∖ S)`: if 1 ∈ Rectangle, we NEED 1 ∈ S (to exclude it from the domain). \n\nSo: S := {1} ∪ (zeros in rectangle). Then:\n- fHolo: HolomorphicOn R (Rectangle ∖ ({1} ∪ zeros)): at s ∈ Rectangle ∖ ({1} ∪ zeros): s ≠ 1 and ζ(s) ≠ 0 ⟹ R differentiable at s ✓ (product/quotient rule, plus need ζ differentiable at s ✓ since s ≠ 1).\n- near at 1: (R − A(1)/(s−1)) with A(1) := 0: R bounded near 1 ⟺ the removable singularity — the MAIN lemma. ✓ (needs proof)\n- near at zeros ρ: (R − m(1−(ρ/(ρ−1))ⁿ)/(s−ρ)) bounded — the logDeriv NF computation. ✓\n- hS: all of S interior.\n- Conclusion: RectangleIntegral' R = Σ_{ρ ∈ zeros} m_ρ·(1−(ρ/(ρ−1))ⁿ) + 0.\n\nThen sides: RectangleIntegral' J = RectangleIntegral' R + RectangleIntegral' ppart = Σ + ResW1 n. \n\nHmm, but wait — for the zeros to form a FINITE set (Finset S), I need finiteness of zeros of ζ in the rectangle. Use `finite_zeros_rectangle`? That requires f analytic on the rectangle — but ζ is NOT analytic at 1 (if 1 ∈ rectangle). Hmm. finite_zeros_rectangle (hf : AnalyticOnNhd ℂ f (Rectangle z w)) — ζ fails at 1. \n\nAlternative: the zeros of ζ in the rectangle = zeros of zetaA in the rectangle? zetaA(w) = (w−1)ζ(w) — analytic EVERYWHERE including 1 (zetaA_analyticAt_one + zetaA_analyticAt_of_ne). Zeros of zetaA: at 1, zetaA(1) = 1 ≠ 0; at w ≠ 1: zetaA(w) = 0 ⟺ ζ(w) = 0. So Rectangle ∩ ζ⁻¹'{0} = Rectangle ∩ zetaA⁻¹'{0} — and zetaA is analytic on the whole rectangle ⟹ finite_zeros_rectangle applies (needs zetaA nonzero at one point of the rectangle — e.g. at 1, zetaA(1) = 1 ≠ 0, if 1 ∈ Rectangle ✓).\n\nSo: S_zeros := (finite_zeros_rectangle zetaA_analyticOnNhd (1 ∈ Rectangle) (zetaA 1 = 1 ≠ 0)).toFinset, and S := {1} ∪ S_zeros... \n\nhmm, wait: but analyticOrderAt ζ ρ vs analyticOrderAt zetaA ρ: for ρ ≠ 1, they're equal (zetaA = (w−1)·ζ, (w−1) analytic nonzero at ρ ⟹ orders add: order zetaA = order ζ + 0). Fine — the residue formula uses analyticOrderNatAt riemannZeta ρ; I'll just need analyticOrderAt ζ ρ ≠ ⊤ which follows from order zetaA ρ ≠ ⊤ (zetaA analytic ⟹ order is finite... analytic function has analyticOrderAt ≠ ⊤ iff not locally zero — at a zero of an analytic function on a connected set, order < ⊤ unless locally identically zero; zetaA(1) = 1 ≠ 0 and the rectangle is connected... the vendored code handles this: (hf q hρRP).analyticOrderAt_ne_top.mp htop gives the factorization directly — AnalyticAt.analyticOrderAt_ne_top : analyticOrderAt ≠ ⊤ ↔ ∃ h, AnalyticAt h ∧ h q ≠ 0 ∧ f =ᶠ (s−q)^ord • h. And for the ⊤ case, analyticOrderAt_eq_top gives local vanishing. For ζ at ρ ≠ 1: if analyticOrderAt ζ ρ = ⊤ then ζ ≡ 0 near ρ, then zetaA ≡ 0 near ρ, then order zetaA = ⊤, contradicting... hmm, I need zetaA order ≠ ⊤ at every point of the rectangle: from the identity principle (analytic on connected open ⊇ rectangle, nonzero at 1). Is there a clean Mathlib lemma? `AnalyticOnNhd.analyticOrderAt_ne_top`? Hmm, maybe: if f analytic on connected open U and ∃ x ∈ U, f x ≠ 0, then ∀ y ∈ U, analyticOrderAt f y ≠ ⊤. I recall something like `AnalyticOnNhd.exists_...`... The vendored `finite_zeros_rectangle` internally does this (isDiscrete_of_codiscreteWithin). For the residue computation I need the factorization at each zero ρ: (analytic at ρ).analyticOrderAt_ne_top.mp (proof that order ≠ ⊤). \n\nThe cleanest: order_zetaA_at_ρ ≠ ⊤ because: analyticOrderAt_eq_top ↔ ∀ᶠ s in 𝓝 ρ, zetaA s = 0 — if so, then zetaA ≡ 0 on the connected component — hmm, need \"codiscreteWithin\" machinery. Mathlib has: `AnalyticOnNhd.eq_zero_of_preconnected_of_eventuallyEq_zero`? or the zeros-are-codiscrete lemma `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` used in finite_zeros_rectangle. From codiscreteness: if order = ⊤ at ρ then zetaA ≡ 0 on a nhd of ρ, but zeros are codiscrete (discrete-ish), contradiction with... Actually more directly: analyticOrderAt_eq_top.mp gives ∀ᶠ s in 𝓝 ρ, zetaA s = 0. The zeros set is codiscreteWithin the rectangle... a set that contains a neighborhood of ρ can't be codiscrete-ish discrete... `isDiscrete_of_codiscreteWithin`... Let me look for a direct Mathlib lemma: `AnalyticAt.analyticOrderAt_ne_top` is the iff with the factorization; the ⊤-exclusion for a globally-analytic nonzero function might be `AnalyticOnNhd.analyticOrderAt_ne_top_of_...`. I'll search Mathlib during implementation.\n\nAlternatively — bypass zetaA and work with ζ directly: at a zero ρ ≠ 1 of ζ, analyticOrderAt ζ ρ = ⊤ means ζ ≡ 0 near ρ. ζ is analytic on ℂ∖{1} (connected, since ℂ minus a point is connected) and ζ(2) ≠ 0 (one_lt_re lemma). Identity principle: `AnalyticOnNhd.eq_zero_on_...`. So analyticOrderAt ζ ρ ≠ ⊤ directly. This avoids zetaA order comparisons. But for FINITENESS of the zero set in the rectangle I still want zetaA (analytic across 1). Hmm, but wait — can I get finiteness another way? zeros in rectangle = {nontrivial zeros} ∪ {trivial −2k in rectangle}. Nontrivial: Re ∈ (0,1) — a sub-rectangle [0,1]×[z.im,w.im] on whose closure ζ is analytic (1 not in it since Re ≤ 1... 1 has Re = 1 and Im = 0 — Im 0 ∈ [z.im, w.im] possible! (1 : ℂ) has re = 1; if the rectangle has Re up to ≥ 1 and Im ∋ 0, then 1 ∈ sub-rectangle...). Ugh — 1 has Re exactly 1; nontrivial zeros have Re < 1 strictly (IsNontrivialZero: 0 < re ∧ re < 1). So nontrivial zeros ⊆ {re < 1} and 1 ∉ {re < 1} — but the closure for analyticity: I'd take rectangle [0,1]×[...] which contains 1 if 0 ∈ im-range. Then ζ not analytic at 1 fails finite_zeros_rectangle again. Take [0, 1−ε]? No, zeros accumulate toward Re = 1? They don't accumulate anywhere (discrete), but their Re can approach 1. Simplest: use zetaA — one clean finiteness for ALL zeros at once. \n\nAnd for the order-≠⊤ at each zero ρ ≠ 1: analyticOrderAt ζ ρ = analyticOrderAt zetaA ρ? Since zetaA =ᶠ[𝓝 ρ] (w−1)·ζ(w) (punctured agreement, both sides... hmm zetaA is defined via Function.update at 1 only; for ρ ≠ 1, zetaA = (w−1)ζ(w) on a nhd of ρ). Order of product = sum of orders: analyticOrderAt (f·g) = order f + order g (Mathlib: `analyticOrderAt_mul`? if exists). order of (w−1) at ρ ≠ 1 is 0 (nonzero analytic). So order zetaA ρ = order ζ ρ. Then order ζ ρ ≠ ⊤ ⟸ order zetaA ρ ≠ ⊤ ⟸ (finiteness machinery / identity principle on zetaA). Or directly for ζ via the ℂ∖{1} identity principle. Either way I need an identity-principle lemma. Let me search Mathlib for the right form.\n\nAlso needed: `analyticOrderNatAt` — the vendored theorem uses analyticOrderNatAt f ρ := (analyticOrderAt f ρ).toNat? (line 177: (analyticOrderNatAt f ρ : ℂ) — that's Mathlib's analyticOrderNatAt). And zeroMult ρ = (analyticOrderAt riemannZeta ρ).toNat = analyticOrderNatAt riemannZeta ρ presumably (Mathlib def: analyticOrderNatAt f z = (analyticOrderAt f z).toNat? let me confirm — yes I believe analyticOrderNatAt is defined as toNat of analyticOrderAt). So the sum terms will read (zeroMult ρ : ℂ)·(1−(ρ/(ρ−1))ⁿ) after bridging zeroMult = analyticOrderNatAt — zeroMult is DEFitionally toNat, and analyticOrderNatAt is probably defeq. Good.\n\nNow, the near-1 lemma (removable singularity of R). Plan:\n- F(w) := (wⁿ − (w−1)ⁿ)·hLi(w) — analytic at 1 (ContDiffAt etc. — actually AnalyticAt: (analytic polynomial)·hLi_analyticAt_one ✓).\n- Taylor poly: TP(w) := Σ_{j=0}^{n} (iteratedDeriv j F 1 / j!)·(w−1)^j — a polynomial, analytic everywhere.\n- Key: TP = (w−1)^{n+1}·ppart n (w) for ALL w (polynomial identity):\n  (w−1)^{n+1}·ppart n w = Σ_{i=1}^{n+1} Acoeff n i ·(w−1)^{n+1−i}; substitute j = n+1−i ∈ [0,n]: Acoeff n (n+1−j) = iteratedDeriv j F 1 / j! — wait: Acoeff n i = iteratedDeriv (n+1−i) F 1 /(n+1−i)! where F here = fun w => (wⁿ−(w−1)ⁿ)·hLi w ✓ same F. With j := n+1−i: iteratedDeriv j F 1 / j! ✓. So (w−1)^{n+1} ppart n w = Σ_{j=0}^{n} (iteratedDeriv j F 1/j!)(w−1)^j = TP(w) ✓.\n- On punctured nhd of 1 with ζ ≠ 0: (w−1)^{n+1}·Jlag n w = F(w) — check: Jlag n w = ((w/(w−1))ⁿ−1)·(−ζ′/ζ w); (w−1)^{n+1}·((w/(w−1))ⁿ−1) = (w−1)·(wⁿ − (w−1)ⁿ)·... let me redo: (w/(w−1))ⁿ − 1 = (wⁿ − (w−1)ⁿ)/(w−1)ⁿ. So (w−1)^{n+1}·Jlag = (w−1)·(wⁿ−(w−1)ⁿ)·(−ζ′/ζ w) = (wⁿ−(w−1)ⁿ)·hLi(w) by hLi_eq_near_one / hLi_eq_of_ne ✓.\n- Hence on the punctured nhd: R(w) = Jlag − ppart = [F(w) − TP(w)]/(w−1)^{n+1}.\n- F − TP is analytic at 1 with iteratedDeriv j (F − TP) 1 = 0 for all j ≤ n (derivs of TP match F up to order n — need: iteratedDeriv j TP 1 = iteratedDeriv j F 1 for j ≤ n; TP is the Taylor poly so yes: standard computation — deriv of Σ_{k} a_k (w−1)^k at 1 to order j is j!·a_j... in Lean this is a polynomial/iteratedDeriv computation: iteratedDeriv j (fun w => Σ k ∈ range(n+1), c k * (w−1)^k) 1 = j!·c j for j ≤ n. There might be Mathlib support: `iteratedDeriv_eq_...` hmm; or compute via TaylorSeries... Alternatively use analyticOrderAt via the power series of F directly! \n\n  Alternative slicker route: F is AnalyticAt 1. Its power series: F(w) = Σ_{k} p_k (w−1)^k (hasSum on a ball). TP = partial sum. F − TP = tail = (w−1)^{n+1}·(analytic tail series). AnalyticAt gives `AnalyticAt.exists_hasSum`... and there are lemmas about factoring out (w−1)^{n+1} from the tail of a power series: `HasSum` tail factoring. Hmm — formalizing the tail-factoring of a formal power series is doable: p as a FormalMultilinearSeries; F(w) = Σ p_k (w−1)^k on ball; define q = \"shifted\" series... Mathlib has `FormalMultilinearSeries.shift`? There IS something: `p.shift`? I recall `FormalMultilinearSeries.shift (p) : ...` hmm not sure.\n\n  The analyticOrderAt route per STATE.md seems most robust: \n  (1) g := F − TP analytic at 1.\n  (2) ∀ j ≤ n: iteratedDeriv j g 1 = 0.\n  (3) `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`-type lemma ⟹ (n+1 : ℕ∞) ≤ analyticOrderAt g 1.\n  (4) Case order = ⊤: g ≡ 0 near 1 ⟹ R = 0 on punctured nhd ⟹ R bounded (by 0... well R = 0/(w−1)^{n+1}... wait if g =ᶠ[𝓝 1] 0 then on punctured nhd R = g/(w−1)^{n+1} = 0 ✓ bounded).\n  (5) Case finite order m ≥ n+1: g = (w−1)^m·h, h analytic, h(1) ≠ 0. Then on punctured nhd: R(w) = (w−1)^{m−n−1}·h(w) → tendsto (if m = n+1: → h(1); else → 0). So R converges ⟹ bounded on punctured nhd ✓.\n  (6) Conclude: (R − 0/(s−1)) =O[𝓝[≠] 1] 1 via tendsto → isBigO_one. That directly gives the `near` hypothesis at 1 with A(1) = 0!\n\n  Oh nice — for residueTheorem_finset I don't even need the analytic extension: `near` at 1 just needs R bounded on the punctured nhd (R − 0/(s−1) = R). And fHolo excludes 1. So NO Function.update extension needed at all! Great simplification.\n\n  For step (3), let me check the exact Mathlib lemma name: STATE.md says `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`. Let me grep Mathlib.\n\n  For step (2): iteratedDeriv j TP 1 = iteratedDeriv j F 1 for j ≤ n. TP(w) = Σ_{k=0}^{n} c_k (w−1)^k with c_k = iteratedDeriv k F 1 / k!. Compute iteratedDeriv j (Σ c_k (w−1)^k) 1: linearity (iteratedDeriv_sum — needs ContDiffAt of each term ✓ polynomial), then iteratedDeriv j ((w−1)^k) at 1: = k.descFactorial j · (1−1)^{k−j} = k.descFactorial j · 0^{k−j}. For j < k: 0^{k−j} = 0 → term vanishes. j = k: k.descFactorial k · 0⁰ = k!. j > k: descFactorial = 0 (for k < j, k.descFactorial j = 0). So iteratedDeriv j TP 1 = j! · c_j (for j ≤ n; for j > n it's 0 but we don't care). Then = j!·(iteratedDeriv j F 1/j!) = iteratedDeriv j F 1 ✓.\n\n  We already have similar computations in LiResidue.lean (A_iter uses iteratedDeriv_pow and iteratedDeriv_comp_sub_const). iteratedDeriv j (fun w => (w−1)^k) 1 = k.descFactorial j · (0)^{k−j} — exactly the h2 computation in A_iter. Reusable pattern ✓.\n\n  Alternatively, maybe Mathlib has Taylor-polynomial machinery: `taylorWithinEval`... the iteratedDeriv of a Taylor polynomial — there might be something in Mathlib.Analysis.Calculus.Taylor? There's `taylorCoeff`, `taylorWithin`... probably easier to just compute directly with the sum/descFactorial pattern.\n\n- The boundedness from Tendsto: Tendsto R (𝓝[≠] 1) (𝓝 L) ⟹ R =O[𝓝[≠] 1] 1 — `.isBigO_one ℂ` on the tendsto (mono_left nhdsWithin_le_nhds) — pattern from vendored code line 117: `(hc.tendsto.mono_left nhdsWithin_le_nhds).isBigO_one ℂ` ✓.\n\n  Wait, in case (4) (g ≡ 0 near 1): R = 0 on punctured nhd: Tendsto R (𝓝[≠] 1) (𝓝 0) via tendsto_of_eventuallyEq... ✓.\n\n  Actually, unify: in both cases, define L := (the limit) — case ⊤: 0; case m: (m = n+1 ? h(1) : 0). Hmm, actually simpler: in both cases R(w) = (w−1)^{m−n−1}·h(w) where for ⊤ case h ≡ 0... Let me handle separately, it's fine.\n\n  Hmm wait, actually for case (5): R(w) = g(w)/(w−1)^{n+1} holds where? On the punctured nhd where (w−1)^{n+1}Jlag = F — i.e., where w ≠ 1 AND ζ(w) ≠ 0. But g = (w−1)^m h on a FULL nhd of 1 (including zeros of ζ!). And ppart identity (w−1)^{n+1} ppart = TP holds everywhere. So R(w) = g(w)/(w−1)^{n+1} holds on {w ≠ 1, ζ(w) ≠ 0} ∩ nhd(1). For the Tendsto of R as w → 1 along 𝓝[≠] 1: zeros of ζ near 1 — there are none close enough! ζ ≠ 0 on a punctured nhd of 1: riemannZeta_residue_one.eventually_ne gives (w−1)ζ(w) ≠ 0 eventually on 𝓝[≠] 1 (that's hne in hLi_eq_near_one). So on 𝓝[≠] 1 eventually: ζ(w) ≠ 0 AND w ≠ 1 ⟹ R = g/(w−1)^{n+1} eventually on 𝓝[≠] 1. Then Tendsto R = Tendsto of (w−1)^{m−n−1}h(w) ✓. \n\n- The residue at a zero ρ: per the algebra above:\n  R(s) − A(ρ)/(s−ρ) where A(ρ) = m·(1−(ρ/(ρ−1))ⁿ), m = analyticOrderNatAt ζ ρ (zeroMult ρ).\n  R(s) − A/(s−ρ) = Jlag(s) − ppart(s) − A/(s−ρ).\n  Jlag(s) − A/(s−ρ) = k(s)·L(s) − m·k(ρ)/(s−ρ) [k := fun s => (s/(s−1))ⁿ−1, L := −logDeriv ζ]\n    = k(s)·(L(s) + m/(s−ρ)) − m·(k(s)−k(ρ))/(s−ρ).\n  L(s) + m/(s−ρ) = −(logDeriv ζ s − m/(s−ρ)) = −logDeriv h(s) [ζ = (s−ρ)^m·h near ρ] → −logDeriv h(ρ) continuous ✓.\n  (k(s)−k(ρ))/(s−ρ) → k′(ρ) slope ✓ (k analytic at ρ since ρ ≠ 1).\n  ppart(s) → ppart(ρ) continuous ✓ (ρ ≠ 1).\n  All terms bounded/Tendsto ⟹ IsBigO 1 ✓.\n\n  This mirrors the vendored proof (lines 227–280) closely. I'll mirror it.\n\n  Edge: ρ with m = 0 (ζ(ρ) ≠ 0)? In our S, all ρ are zeros so m ≥ 1 — but m ≥ 1 needs order ≠ ⊤ and ≠ 0: ζ(ρ) = 0 ⟹ order ≥ 1 (for analytic ζ at ρ — Mathlib: `analyticOrderAt_pos_iff`? there's `analyticOrderAt_eq_zero_iff`? something like order > 0 iff f z = 0 — `AnalyticAt.analyticOrderAt_pos`... I'll find it). Actually for the near-condition proof, I don't need m ≥ 1! The factorization ζ = (s−ρ)^m·h with h(ρ) ≠ 0 works for m = 0 too (h = ζ). And A(ρ) = 0·(...) = 0 ✓ consistent. So the residue lemma can be stated for ANY ρ ≠ 1 with analyticOrderAt ζ ρ ≠ ⊤ — uniform. But m = 0 can't happen for ρ ∈ S anyway. Fine either way.\n\n  The needed order-≠-⊤ at zeros: as discussed. For nontrivial zeros: Zeta23's `one_le_mult`? That's a structure field (zetaZeros hs).one_le_mult — hmm, it's bundled in a structure `ZeroCountingData`? Let me look at Statement.lean more carefully — one_le_mult is a field of some structure (line 77), maybe an assumption rather than a proved fact. In LiSkeleton, liSummable used Zeta23's zero_sum_inv_sq (proved). For order ≠ ⊤ at a nontrivial zero: zeroMult ρ ≥ 1 means toNat ≥ 1 means analyticOrderAt ∉ {0, ⊤}... but one_le_mult is a structure field (hypothesis), not a theorem. Hmm — but there's the direct route: analyticOrderAt ζ ρ = ⊤ ⟹ ζ ≡ 0 near ρ ⟹ (identity principle on ℂ∖{1}, connected, ζ(2) ≠ 0) contradiction. This works for ALL ρ ≠ 1 uniformly, including trivial zeros. So prove ONE lemma: ∀ ρ ≠ 1, analyticOrderAt riemannZeta ρ ≠ ⊤.\n\n  Mathlib identity principle: `AnalyticOnNhd.eq_of_eventuallyEq`? or for order: maybe `AnalyticOnNhd.analyticOrderAt_ne_top`? Let me search: candidates — Mathlib.Analysis.Analytic.IsolatedZeros: `analyticOrderAt_eq_top` ... `AnalyticOnNhd.exists_ne_zero_of_...`. I recall: `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` (used in vendored finite_zeros_rectangle). From codiscrete: if ∀ᶠ s in 𝓝 ρ, ζ s = 0, then... the zeros contain a nhd of ρ; codiscreteWithin sets have discrete complement... A nhd of ρ minus {ρ} intersected... hmm: codiscreteWithin U means complement is discrete-ish: ∃ nhd, ∀ x in nhd ∩ U, x ≠ ρ... no wait: codiscreteWithin U ↔ ∀ x ∈ U, ∃ nhd of x, ∀ y in nhd ∩ U, y ≠ x → y ∈ set... i.e., near each point of U, all punctured-nearby points of U are in the set. If zeros ⊇ nhd of ρ: then complement (nonzeros) ∩ U is empty near ρ — but codiscreteness says nonzeros are codense... Let me use it contrapositively: ζ ≡ 0 on nhd V of ρ. Pick x ∈ V ∩ U with x ≠ ρ (V is a nhd, U open ∋ ρ... need x ≠ ρ in V ∩ (ℂ∖{1})). CodiscreteWithin applied at x: all sufficiently close points y ≠ x (in U) are NON-zeros. But y ∈ V close to x are zeros (V open ∋ x, ζ ≡ 0 on V). Contradiction. OK, workable but fiddly.\n\n  Is there a cleaner Mathlib form? `AnalyticOnNhd.eq_zero_of_isPreconnected_of_eventuallyEq_zero`? Something like: if f analytic on preconnected open U, and f = 0 on a set with a limit point / on an open subset, then f = 0 on U. I believe there's `AnalyticOnNhd.eq_zero_of_preconnected_of_mem_nhds` hmm. Names to try: `AnalyticOnNhd.eq_on_of_preconnected_of_eventuallyEq`, `AnalyticOnNhd.eq_zero_of_eventuallyEq_zero`... Let me grep during implementation.\n\nThen: eventually ζ ≠ 0 on 𝓝[≠] 1 — from riemannZeta_residue_one.eventually_ne (already used in LiResidue) ✓.\n\nNow the ASSEMBLY:\n\nTheorem `rectInt'_Jlag` (n : ℕ) (z w : ℂ) (hre) (him) (h1 : Rectangle z w ∈ 𝓝 1) (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0):\n  RectangleIntegral' (Jlag n) z w = ResW1 n + Σ ρ ∈ Szeros, (zeroMult ρ : ℂ)·(1 − (ρ/(ρ−1))ⁿ)\nwhere Szeros := (zeros of ζ in rectangle).toFinset via finite_zeros_rectangle on zetaA.\n\nProof sketch:\n- S := insert 1 Szeros. Note 1 ∉ Szeros (ζ(1) ≠ 0).\n- hS: ∀ p ∈ S, Rectangle ∈ 𝓝 p: for 1: h1 ✓. For zeros: interior ⟸ not on border (hborder: ζ ≠ 0 on border; ρ zero ⟹ ρ ∉ border; ρ ∈ Rectangle; Rectangle ∈ 𝓝 ρ ⟺ interior point — need the equivalence: Rectangle z w ∈ 𝓝 ρ iff ρ strictly inside — the vendored proof at line 184–197 does exactly this (hZint) — extract as helper: mem_rectangle_interior... The vendored code does it via rectangle_mem_nhds_iff. I'll write a helper lemma `rectangle_mem_nhds_of_mem_of_not_border`.)\n- fHolo: HolomorphicOn R (Rectangle ∖ ↑S): s ∈ Rectangle ∖ S ⟹ s ≠ 1 ∧ s ∉ Szeros. Need ζ(s) ≠ 0: if ζ(s) = 0 then s ∈ Rectangle ∩ ζ⁻¹'0 = Szeros (as sets) — need Szeros.toFinset membership ⟺ s ∈ Rectangle ∩ zetaA⁻¹'0, and bridge zetaA s = 0 ⟺ ζ s = 0 for s ≠ 1 ✓. Then R differentiable at s: Jlag differentiable (product: (w/(w−1))ⁿ−1 differentiable at s ≠ 1: div, pow, sub ✓; −ζ′/ζ differentiable at s: ζ differentiable (s ≠ 1), deriv ζ differentiable (needs ζ twice-differentiable — analytic ⟹ deriv differentiable: (differentiableAt_riemannZeta hs).deriv? hmm — DifferentiableAt.deriv requires... `DifferentiableAt.deriv : DifferentiableAt ℂ f z → DifferentiableAt ℂ (deriv f) z`? No — that's not true in general; for ℂ-analytic functions yes: AnalyticAt.deriv : AnalyticAt ℂ f z → AnalyticAt ℂ (deriv f) z ✓ (used in LiResidue hLi_analyticAt_one: ha.deriv). analyticAt_riemannZeta hs : AnalyticAt ℂ riemannZeta s for s ≠ 1 ✓ (used in zetaA_analyticAt_of_ne). Then div by ζ(s) ≠ 0 ✓.) ppart differentiable at s ≠ 1: sum of A_i/(w−1)^i ✓ (pattern exists in LiPrincipal: Gprim_differentiableAt / the hAint proof).\n  So R = Jlag − ppart differentiable at s. HolomorphicOn = DifferentiableOn... (HolomorphicOn is defeq DifferentiableOn ℂ? In Mathlib, HolomorphicOn f s := DifferentiableOn ℂ f s ✓.)\n- near at 1: A(1) := 0 — the removable-singularity boundedness (main lemma above).\n- near at ρ ∈ Szeros: residue formula (the logDeriv NF lemma).\n- residueTheorem_finset gives: RectangleIntegral' R z w = Σ_{p ∈ insert 1 Szeros} A p = A 1 + Σ_{ρ∈Szeros} A ρ = 0 + Σ zeroMult·(1−(ρ/(ρ−1))ⁿ).\n- Jlag = R + ppart; border integrability of each: from HolomorphicOn.rectangleBorderIntegrable' (as in LiPrincipal) — needs the functions differentiable on a nhd of each border point... Actually HolomorphicOn.rectangleBorderIntegrable' _ h1? In LiPrincipal: `HolomorphicOn.rectangleBorderIntegrable' _ h1` where h1 : Rectangle ∈ 𝓝 1 — hmm, that lemma's signature: HolomorphicOn.rectangleBorderIntegrable' (hf : HolomorphicOn f (Rectangle z w \\ {c})) (hc : Rectangle z w ∈ 𝓝 c)? It was used with the function holomorphic on Rectangle ∖ {1}. Let me check its exact signature when I get there — from LiPrincipal usage: `apply HolomorphicOn.rectangleBorderIntegrable' _ h1; intro s hs; ...` with hs : s ∈ Rectangle z w \\ {1} presumably — so signature (hf : HolomorphicOn f (Rectangle \\ {c})) (hc : Rectangle ∈ 𝓝 c) : RectangleBorderIntegrable f z w. So for R: holomorphic on Rectangle ∖ S — hmm, but rectangleBorderIntegrable' wants complement of a SINGLETON. R on Rectangle ∖ S with S = insert 1 Szeros... I can get RectangleBorderIntegrable R from residueTheorem_finset's internals? No — its conclusion is about RectangleIntegral' (the primed, normalized version)... wait no, residueTheorem_finset CONCLUDES RectangleIntegral' f z w = Σ A p — the primed integral — and RectangleIntegral' is DEFINED as (1/2πi) • RectangleIntegral — but RectangleIntegral requires integrability? RectangleIntegral is defined via interval integrals — totalized, no integrability needed for the STATEMENT... but for additivity (RectangleBorderIntegrable.add) we need integrability.\n\n  For the final assembly: RectangleIntegral' (Jlag) = RectangleIntegral' (R + ppart) — need RectangleBorderIntegrable R and RectangleBorderIntegrable (ppart n).\n  - ppart: LiPrincipal already did this (hAint/hGint pattern, or directly: ppart holomorphic on Rectangle ∖ {1} ⟹ rectangleBorderIntegrable' h1).\n  - R: holomorphic on Rectangle ∖ S. Get integrability via ContinuousOn on the border: border ⊆ Rectangle ∖ S (S interior ⟹ border ∩ S = ∅), R continuous on Rectangle ∖ S (holomorphic ⟹ continuous) ⟹ ContinuousOn.rectangleBorder_integrable (used in vendored line 129: `ContinuousOn.rectangleBorder_integrable (hf₂holo.continuousOn.mono hbS)`) ✓.\n  Then RectangleIntegral'_add (LiPrincipal) gives the split; Jlag = R + ppart pointwise (funext: Jlag = R + ppart ⟺ R = Jlag − ppart ✓ by definition Pi.sub_apply).\n  \n- Final: RectangleIntegral' Jlag = RectangleIntegral' R + RectangleIntegral' ppart = Σ + ResW1 n. ✓\n\nWait — one problem: RectangleIntegral'_add from LiPrincipal takes (hf : RectangleBorderIntegrable f) (hg : RectangleBorderIntegrable g) and concludes RectangleIntegral' (f + g) = ... So I need Jlag = R + ppart as a function eq: R + ppart = (Jlag − ppart) + ppart = Jlag ✓ (sub_add_cancel). So RectangleIntegral' Jlag = RectangleIntegral' (R + ppart) by congr. ✓\n\nAlso — Szeros as toFinset of finite_zeros_rectangle applied to zetaA: need zetaA AnalyticOnNhd on Rectangle: zetaA_analyticAt_one + zetaA_analyticAt_of_ne ⟹ AnalyticOnNhd ℂ zetaA (Rectangle z w) := fun s hs => by_cases s = 1 ... ✓. And need a point where zetaA ≠ 0: 1 ∈ Rectangle (from h1 : Rectangle ∈ 𝓝 1 ⟹ 1 ∈ Rectangle) with zetaA 1 = 1 ≠ 0 ✓.\n\nHmm — zetaA zeros = ζ zeros inside rectangle: s ≠ 1: zetaA s = (s−1)ζ(s) = 0 ⟺ ζ s = 0 (s−1 ≠ 0) ✓; s = 1: zetaA 1 = 1 ≠ 0 ✓. So Rectangle ∩ zetaA⁻¹'0 = Rectangle ∩ ζ⁻¹'0 (as sets, since 1 ∉ RHS too because ζ 1 ≠ 0... wait — do I even need ζ 1 ≠ 0 then? The SETS Rectangle ∩ zetaA⁻¹'0 and Rectangle ∩ ζ⁻¹'0: at s = 1: LHS: 1 ∉ (zetaA 1 = 1). RHS: 1 ∈ iff ζ 1 = 0 — junk value (γ−log4π)/2 ≠ 0. To avoid proving ζ 1 ≠ 0, just define Szeros via zetaA zeros and characterize membership as: ρ ∈ Szeros ⟺ ρ ∈ Rectangle ∧ ρ ≠ 1 ∧ ζ ρ = 0? For the near-condition and sum, what matters: Szeros contains every s ∈ Rectangle with ζ s = 0, s ≠ 1 (for fHolo), and each member has ζ = 0... wait actually members of Szeros: zetaA zeros could include... at s ≠ 1 they're exactly ζ zeros ✓. And 1 ∉ Szeros ✓ (zetaA 1 = 1). So the sum Σ over Szeros = sum over all ζ-zeros in Rectangle, with 1 excluded automatically. And fHolo: s ∈ Rectangle ∖ S, need ζ s ≠ 0: if ζ s = 0, then since s ≠ 1 (s ∉ S ∋ 1), zetaA s = (s−1)·0 = 0 ⟹ s ∈ Szeros ⊆ S — contradiction ✓. No need for ζ(1) ≠ 0! The junk value never enters. \n\nBUT the membership bridge: s ∈ (finite_zeros_rectangle ...).toFinset ⟺ s ∈ Rectangle ∩ zetaA⁻¹'{0} — Set.Finite.mem_toFinset. And finite_zeros_rectangle produces (Rectangle ∩ zetaA⁻¹'{0}).Finite. ✓\n\nSo Szeros := hfin.toFinset where hfin := finite_zeros_rectangle zetaA_analytic h1mem zetaA_one_ne_zero... signature: finite_zeros_rectangle (hf : AnalyticOnNhd ℂ f (Rectangle z w)) {x : ℂ} (hx : x ∈ Rectangle z w) (hfx : f x ≠ 0) : (Rectangle z w ∩ f ⁻¹' {0}).Finite. With x := 1, hx := mem_of_mem_nhds h1, hfx : zetaA 1 ≠ 0 (zetaA_one ▸ one_ne_zero) ✓.\n\nThe residue at each ρ ∈ Szeros: A ρ := (zeroMult ρ : ℂ) * (1 − (ρ/(ρ−1))ⁿ). Since zeroMult ρ = analyticOrderNatAt riemannZeta ρ (defeq? zeroMult := (analyticOrderAt riemannZeta ρ).toNat; Mathlib analyticOrderNatAt f x := (analyticOrderAt f x).toNat — likely defeq ✓, can use `rfl` or unfold).\n\nThen the final sum: Σ ρ ∈ Szeros, (zeroMult ρ : ℂ)·(1−(ρ/(ρ−1))ⁿ). \n\nFor the D-064 assembly shape, ii′-6 will want to split Szeros into nontrivial zeros and {−2}. I could provide the generic theorem now + optionally the specialization. Let me ALSO check: does the rectangle in D-064 contain −4? σ ∈ [−5/2, 2√n]: −4 < −5/2 ✓ outside. −2: Re −2 ∈ (−5/2, ...) ✓ inside if |Im| range ∋ 0 ✓ (T > 0). So Szeros = {nontrivial zeros with |γ| < T} ∪ {−2}. The specialization needs: trivial zeros of ζ are exactly at negative even integers (Mathlib: `riemannZeta_eq_zero_iff`? Hmm — there IS a characterization: `riemannZeta_ne_zero_of_one_le_re`... zeros for Re ≤ 0: via functional equation: ζ(s) = 0 ∧ Re s ≤ 0 ⟺ s = −2k — is that in Mathlib? I recall `riemannZeta_eq_zero_of_...` for negative even; the converse (no other zeros with Re ≤ 0) needs the functional equation + ζ ≠ 0 for Re ≥ 1: `riemannZeta_ne_zero_of_one_le_re`? and completedRiemannZeta zeros = nontrivial... This might exist as part of the PNT formalization: `riemannZeta_ne_zero_of_one_le_re` (Mathlib has this I think, from Euler product for re > 1 and... re = 1 needs more (PNT-level: ζ(1+it) ≠ 0 — that IS in Mathlib now, used for PNT). For Re ≤ 0 zeros ⟺ negative even: needs functional equation + Gamma poles. Search Zeta23: they proved RvM and the EF — they must have a trivial-zero characterization somewhere. If available, great; the specialization corollary can be part of ii′-4 (zero-avoiding T) anyway — STATE.md lists the triv residue under THIS sub-stage: \"at −2 (residue 1−(2/3)ⁿ)\". The RESIDUE at −2 needs analyticOrderNatAt ζ (−2) = 1. Hmm. Let me search for trivial-zero simplicity in Zeta23/Mathlib now-ish; if it's not readily available, I'll state the generic theorem (with analyticOrderNatAt at all zeros) and add the −2 specialization as a lemma with the order-1 fact proved if feasible, else defer with a note. Actually — for the generic theorem the triv split is not needed. Let me keep this sub-stage to the generic theorem + try the −2 order-1 lemma as a bonus.\n\nHmm, wait. Let me reconsider: is the order at −2 provable cheaply? analyticOrderNatAt riemannZeta (−2) = 1 ⟺ ζ(−2) = 0 ∧ deriv ζ (−2) ≠ 0. ζ(−2) = 0: Mathlib `riemannZeta_neg_two_mul_nat_add_one`? or `riemannZeta_neg_nat_eq_bernoulli`... there's `riemannZeta_neg_nat_eq_...`: ζ(−n) = −B_{n+1}/(n+1) — ζ(−2) = −B₃/3 = 0 (B₃ = 0). And deriv ζ (−2) ≠ 0: via functional equation — ζ(s) = χ(s)ζ(1−s), χ(s) = 2^s π^{s−1} sin(πs/2)Γ(1−s): near s = −2: sin(πs/2) has a simple zero, ζ(1−s) = ζ(3) ≠ 0 analytic, other factors nonzero ⟹ simple zero of ζ at −2 with deriv = χ-factors·(π/2)cos(−π)·ζ(3) ≠ 0. In Mathlib: `riemannZeta_one_sub` (functional equation) exists (saw it at RiemannZeta.lean:178). Computing deriv from the FE: doable but a chunk of work. Zeta23's PNT-related files might have trivial-zero simplicity (needed for the explicit formula with trivial-zero sum!). Zeta23 has WeilEF — the explicit formula sums over trivial zeros too? Let me grep Zeta23 for trivial zero lemmas.\n\nOK let me also read the rest of LiSkeleton to see the Sf/SInfty/Bn definitions (for the eventual assembly context) — actually not needed for this sub-stage. Skip.\n\nLet me now check a few Mathlib lemma names:\n1. `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` (STATE.md named it — verify exact form)\n2. Identity principle form\n3. analyticOrderNatAt def\n4. trivial zero simplicity in Zeta23\n5. HolomorphicOn.rectangleBorderIntegrable' signature\n\nLet me grep.","signature":""},{"type":"text","text":"Good — `riemannZeta 1 = (γ − log(4π))/2 ≠ 0` (junk value but nonzero; I'll avoid needing it by routing finiteness through `zetaA`). Now checking the key Mathlib lemma names for the order machinery."},{"type":"tool_use","id":"Bash_17","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"natCast_le_analyticOrderAt_iff\\|le_analyticOrderAt_iff\" Mathlib/Analysis/Analytic/ | head -5; echo ---; grep -rn \"theorem.*analyticOrderAt_eq_top\\|analyticOrderAt_ne_top\" Mathlib/Analysis/Analytic/Order.lean | head -10; echo ---; grep -rn \"def analyticOrderNatAt\" Mathlib/ | head -3","description":"Find analyticOrderAt lemma names in Mathlib"},"extra_content":null},{"type":"tool_use","id":"Bash_18","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean\" && grep -rn \"trivial\" Zeta23/ --include=\"*.lean\" -il | head; echo ---; grep -rn \"riemannZeta_neg_two\\|neg_two_mul\\|trivialZero\\|trivial_zero\" Zeta23/ --include=\"*.lean\" | head -20","description":"Search Zeta23 for trivial zero lemmas"},"extra_content":null}]