[{"type":"thinking","thinking":"Key facts confirmed:\n1. `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (hf : AnalyticAt 𝕜 f z₀) : (n : ℕ∞) ≤ analyticOrderAt f z₀ ↔ ∀ i < n, iteratedDeriv i f z₀ = 0`\n2. `analyticOrderAt_ne_top_of_isPreconnected (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : analyticOrderAt f x ≠ ⊤) : analyticOrderAt f y ≠ ⊤`\n3. `AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero` — for trivial zero simplicity, would need deriv ζ (−2) ≠ 0.\n\nFor the identity principle at zeros: use analyticOrderAt_ne_top_of_isPreconnected with U = {1}ᶜ, f = riemannZeta, x = 2 (need analyticOrderAt ζ 2 ≠ ⊤: ζ(2) ≠ 0 ⟹ order = 0 ≠ ⊤ via analyticOrderAt_eq_zero.mpr), y = ρ. Need: IsPreconnected {1}ᶜ — ℂ minus a point is preconnected: `isPreconnected_compl_singleton`? hmm, does that exist... In ℂ (dimension 2), punctured space is connected. Mathlib: `isConnected_compl_singleton`? Let me search. There's `isPreconnected_compl_singleton_of_...`? Hmm. Alternatively use U := univ ∖ {1}... same thing. If no direct lemma: isPreconnected of {1}ᶜ in ℂ — I recall `isPreconnected_compl_singleton` might not exist but there's stuff about punctured neighborhoods... Let me search for it.\n\nAlternatively, avoid the identity principle entirely: for ρ a zero with order ⊤, ζ ≡ 0 near ρ. I need a contradiction. Zeros of ζ near ρ... Actually here's a slicker approach using Zeta23: `ZetaSeam.one_le_mult_holds : ∀ ρ, IsNontrivialZero ρ → 1 ≤ zeroMult ρ` — for NONTRIVIAL zeros this gives order ≠ ⊤ directly (toNat ≥ 1 ⟹ ≠ ⊤). For TRIVIAL zeros in the rectangle — hmm.\n\nWait, actually, let me reconsider. Do I even need to handle arbitrary zeros? In the generic theorem, S = all zeros of zetaA in the rectangle. These include trivial zeros (−2, −4, ... if in range). For each such ρ, I need analyticOrderAt ζ ρ ≠ ⊤ for the residue computation. \n\nOption A: identity principle on {1}ᶜ — need IsPreconnected ({1}ᶜ : Set ℂ). Search Mathlib: `isPreconnected_compl_singleton`... I believe there IS `isPreconnected_compl_singleton_of_dimension...`? In a 2-dim real space, complement of a point is (pre)connected. There might be `isConnected_compl_singleton` somewhere. I'll grep.\n\nOption B: for trivial zeros specifically, use simplicity (order = 1 ≠ ⊤). Needs deriv ζ (−2k) ≠ 0 — via functional equation. Heavier.\n\nOption C: use zetaA's analyticity: at a zero ρ ≠ 1 of ζ, analyticOrderAt zetaA ρ = analyticOrderAt ζ ρ (zetaA = (w−1)ζ near ρ, (w−1) nonzero analytic ⟹ same order). And analyticOrderAt zetaA ρ ≠ ⊤ because zetaA is ENTIRE (analytic on all of ℂ, univ preconnected ✓ trivially — `isPreconnected_univ`) and zetaA 1 = 1 ≠ 0. Then order zetaA ρ = order ((w−1)·ζ) ρ = order (w−1) ρ + order ζ ρ = 0 + order ζ ρ. Need `analyticOrderAt_mul : analyticOrderAt (f*g) z = analyticOrderAt f z + analyticOrderAt g z` — saw at line 250-251 the context of a mul lemma ✓ exists. And analyticOrderAt (fun w => w−1) ρ = 0 since value ≠ 0: `analyticOrderAt_eq_zero.mpr (.inr h)` — saw that form: analyticOrderAt_eq_zero.mpr (.inr hfz-ne) ✓.\n\nOption C is clean and avoids the punctured-plane connectedness question! zetaA is analytic on univ: need AnalyticOnNhd ℂ zetaA univ := fun s _ => by_cases s = 1. analyticOrderAt zetaA 1 ≠ ⊤: zetaA 1 = 1 ≠ 0 ⟹ analyticOrderAt_eq_zero ⟹ = 0 ≠ ⊤ ✓. Then analyticOrderAt_ne_top_of_isPreconnected (U := univ) (isPreconnected_univ) mem_univ mem_univ. ✓\n\nSo: `zeta_order_ne_top : ∀ ρ, analyticOrderAt riemannZeta ρ ≠ ⊤`? NO wait — at ρ = 1, analyticOrderAt ζ 1... ζ is not analytic at 1, analyticOrderAt for non-analytic... Mathlib's analyticOrderAt f z when f not analytic: it's defined via... hmm, analyticOrderAt might be ⊤ or 0 by junk at non-analytic points. I only need ρ ≠ 1 anyway. So: `zeta_order_ne_top_of_ne {ρ : ℂ} (hρ : ρ ≠ 1) : analyticOrderAt riemannZeta ρ ≠ ⊤`.\n\nProof: analyticOrderAt zetaA ρ ≠ ⊤ (entire + nonzero at 1). zetaA =ᶠ[𝓝 ρ] (fun w => (w−1) * riemannZeta w) (eventually since ρ ≠ 1). analyticOrderAt_congr: order respects eventually-eq? There should be `analyticOrderAt_congr : f =ᶠ[𝓝 z] g → analyticOrderAt f z = analyticOrderAt g z`? Let me check. If exists: analyticOrderAt zetaA ρ = analyticOrderAt ((w−1)·ζ) ρ = analyticOrderAt (w−1) ρ + analyticOrderAt ζ ρ = 0 + analyticOrderAt ζ ρ. Need the mul lemma's hypotheses (analyticity of both factors — (w−1) analytic ✓, ζ analytic at ρ ≠ 1 ✓).\n\nCheck names: `analyticOrderAt_mul` — from Order.lean around line 250. Let me look at its signature. Also `analyticOrderAt_congr`.\n\nThen, for the residue at a zero ρ (≠ 1): the factorization from `(analyticAt_riemannZeta hρ).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ)` gives ⟨h, hh, hh0, hfh⟩: ζ =ᶠ[𝓝 ρ] (s−ρ)^(analyticOrderNatAt ζ ρ) • h.\n\nWait — analyticOrderNatAt vs the exponent in the factorization: `AnalyticAt.analyticOrderAt_ne_top : analyticOrderAt f z₀ ≠ ⊤ ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ (analyticOrderNatAt f z₀) • g z`? Let me check the exact form at Order.lean:113. From the vendored usage (line 241): `obtain ⟨h, hh, hh0, hfh⟩ := (hf q hρRP).analyticOrderAt_ne_top.mp htop` then uses `f =ᶠ[𝓝 s] (fun s => (s - q) ^ analyticOrderNatAt f q • h s)` (line 243: hfh.eventually_nhds... with analyticOrderNatAt f q as the exponent). ✓ \n\nNow the residue computation at ρ (zero, m := analyticOrderNatAt ζ ρ ≥ 1 — actually the computation works for any m):\n\nGoal: ((Rfun n) − fun s => A ρ / (s − ρ)) =O[𝓝[≠] ρ] (1 : ℂ → ℂ), A ρ = (m : ℂ)·(1 − (ρ/(ρ−1))ⁿ).\n\nRfun n s = Jlag n s − ppart n s. Since ppart is continuous at ρ (ρ ≠ 1): ppart =O[𝓝[≠] ρ] 1 via ContinuousAt.tendsto... So suffices: (Jlag n − fun s => A ρ/(s−ρ)) =O[𝓝[≠] ρ] 1, then sub and add.\n\nHmm — IsBigO.sub: (f − g) where both =O 1: IsBigO.add: f =O 1, g =O 1 ⟹ f + g =O 1; and Rfun − A/(s−ρ) = (Jlag − A/(s−ρ)) − ppart. ✓ IsBigO.sub exists.\n\nJlag n s − A ρ/(s−ρ):\nJlag n s := ((s/(s−1))ⁿ − 1) * (−(deriv riemannZeta s / riemannZeta s)) =: kFun n s * (−logDeriv ζ s).\n\nWait, should I write Jlag with logDeriv or with −(deriv/·)? logDeriv f s = deriv f s / f s (logDeriv_apply). So −(deriv ζ s / ζ s) = −logDeriv ζ s. Define Jlag n s := kFun n s * (−logDeriv riemannZeta s)? Cleaner for the NF computation (logDeriv_mul etc. as in vendored). But for the w=1 residue connection (ResW1), session 016 used (w−1)·(−ζ′/ζ) with explicit deriv/quotient — hLi_eq_of_ne : hLi w = (w−1)·(−deriv ζ w/ζ w). The (w−1)^{n+1}·Jlag = F bridge needs Jlag in the −deriv/· form. Fine — logDeriv ζ s = deriv ζ s / ζ s by logDeriv_apply (simp lemma), so both forms bridge trivially.\n\nAlgebra (near ρ, using ζ = (s−ρ)^m·h(s)):\nlogDeriv ζ s = m/(s−ρ) + logDeriv h s (vendored pattern, logDeriv_mul + logDeriv of (s−ρ)^m).\n\nHmm wait, the exponent m as ℕ: (s−ρ)^m with m : ℕ — logDeriv_pow gives logDeriv ((s−ρ)^m) = m·logDeriv (s−ρ) = m·(1/(s−ρ)) = m/(s−ρ). In the vendored code (line 259–264): logDeriv ((s−q)^analyticOrderNatAt f q) s = (analyticOrderNatAt f q : ℂ)/(s−q) via logDeriv_comp + logDeriv_pow. ✓ mirror that.\n\nThen:\nJlag n s − A ρ/(s−ρ)\n= k(s)·(−logDeriv ζ s) − m·k(ρ)/(s−ρ)    [A ρ = m·k(ρ) since k(ρ) = (ρ/(ρ−1))ⁿ−1... \n\nWAIT. Sign check again. A ρ := m·(1−(ρ/(ρ−1))ⁿ). And k(ρ) = (ρ/(ρ−1))ⁿ − 1 = −(1−(ρ/(ρ−1))ⁿ). So A ρ = −m·k(ρ). Residue of Jlag at ρ = k(ρ)·Res(−ζ′/ζ at ρ) = k(ρ)·(−m) = −m·k(ρ) ✓ consistent.\n\nJlag n s − A ρ/(s−ρ) = −k(s)·logDeriv ζ s + m·k(ρ)/(s−ρ)\n= −k(s)·[m/(s−ρ) + logDeriv h s] + m·k(ρ)/(s−ρ)\n= −m·[k(s) − k(ρ)]/(s−ρ) − k(s)·logDeriv h s.\n\nTerm 1: (k(s)−k(ρ))/(s−ρ) → deriv k ρ (slope; k differentiable at ρ since ρ ≠ 1). Tendsto ✓.\nTerm 2: k(s)·logDeriv h s → k(ρ)·logDeriv h ρ (continuous; h analytic at ρ, h(ρ) ≠ 0) ✓.\n\nSo Jlag n s − A ρ/(s−ρ) → −m·deriv k ρ − k(ρ)·logDeriv h ρ — a concrete limit. Tendsto ⟹ =O 1 ✓.\n\nIn Lean, mirror the vendored structure:\n- hexp : ∀ᶠ s in 𝓝[≠] ρ, (−m·(k s − k ρ)/(s−ρ) − k s·logDeriv h s) = (Jlag n − A ρ/(s−ρ)) s — by algebra with the logDeriv expansion.\n- hslope : Tendsto ((k s − k ρ)/(s−ρ)) (𝓝[≠] ρ) (𝓝 (deriv kFun ρ)) — hasDerivAt_iff_tendsto_slope.\n- hcont : Tendsto (k s·logDeriv h s) (𝓝[≠] ρ) (𝓝 (k ρ·logDeriv h ρ)) — ContinuousAt.\n- combine: ((−m)·slope + ...).isBigO_one, then .congr' hexp.\n\nk differentiability at ρ: kFun n s = (s/(s−1))ⁿ − 1 — differentiable at ρ ≠ 1: div (id, sub const, denom ≠ 0), pow, sub_const ✓ fun_prop-able probably.\n\nNow the main removable-singularity lemma at 1 (near condition, A 1 = 0):\n\nGoal: (Rfun n) =O[𝓝[≠] 1] 1.\n\nRfun n s = Jlag n s − ppart n s.\n\nOn 𝓝[≠] 1 eventually: ζ s ≠ 0 (riemannZeta_residue_one.eventually_ne with (w−1) factor: gives (w−1)·ζ w ≠ 0 ⟹ ζ w ≠ 0 ✓ as in hLi_eq_near_one) and s ≠ 1.\n\nFor such s: (s−1)^{n+1}·Rfun n s = (s−1)^{n+1}·Jlag n s − (s−1)^{n+1}·ppart n s = F(s) − TP(s) where:\n- (s−1)^{n+1}·Jlag n s = (sⁿ−(s−1)ⁿ)·hLi s =: F s: proof: Jlag n s = kFun n s·(−logDeriv ζ s); kFun n s = (sⁿ−(s−1)ⁿ)/(s−1)ⁿ (field_simp with s−1 ≠ 0); so (s−1)^{n+1}·Jlag = (s−1)(sⁿ−(s−1)ⁿ)(−ζ′/ζ s) = (sⁿ−(s−1)ⁿ)·hLi s by hLi_eq_of_ne (s ≠ 1, ζ s ≠ 0) ✓.\n- (s−1)^{n+1}·ppart n s = Σ_{i=1}^{n+1} Acoeff n i·(s−1)^{n+1−i} = TP(s) := Σ_{j=0}^{n} (iteratedDeriv j F 1/j!)·(s−1)^j — polynomial identity via reindexing j = n+1−i and Acoeff def ✓.\n\nSo Rfun n s = (F s − TP s)/(s−1)^{n+1} on the punctured eventually-nhd.\n\ng := F − TP: AnalyticAt ℂ g 1 (F: polynomial × hLi_analyticAt_one; TP: polynomial) ✓.\n\nOrder: ∀ i < n+1, iteratedDeriv i g 1 = 0:\niteratedDeriv i F 1 = iteratedDeriv i TP 1 for i ≤ n.\nTP(w) = Σ_{j∈range(n+1)} c_j·(w−1)^j, c_j = iteratedDeriv j F 1 / j!.\niteratedDeriv i TP 1 = Σ_j c_j·iteratedDeriv i ((w−1)^j) 1.\niteratedDeriv i (fun w => (w−1)^j) 1 = j.descFactorial i·(0)^{j−i} (A_iter's h2 pattern: iteratedDeriv_comp_sub_const + iteratedDeriv_pow).\n  For i ≤ n: j ranges over [0, n]; j < i: descFactorial... wait j.descFactorial i for j < i is 0 (descFactorial j i = 0 when i > j). j = i: i.descFactorial i·0⁰ = i!. j > i: j.descFactorial i·0^{j−i} = 0 (0^{positive} = 0).\n  So the sum reduces to c_i·i! = iteratedDeriv i F 1 ✓.\nThen iteratedDeriv i g 1 = iteratedDeriv i F 1 − iteratedDeriv i TP 1 = 0 (needs ContDiffAt to split: F, TP both ContDiffAt ✓; iteratedDeriv_sub ✓ used in A_iter).\n\nThen natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (g analytic) : (n+1 : ℕ∞) ≤ analyticOrderAt g 1.\n\nCases on analyticOrderAt g 1 = ⊤ or not:\n- ⊤: analyticOrderAt_eq_top.mp : ∀ᶠ s in 𝓝 1, g s = 0. Then on 𝓝[≠] 1: Rfun n s = g s/(s−1)^{n+1} = 0 eventually ⟹ Tendsto to 0 ⟹ =O 1. Hmm wait — Rfun n s = g s/(s−1)^{n+1} holds only on the eventually-set where ζ s ≠ 0 ∧ s ≠ 1. Intersect with g = 0 eventually: on the intersection, Rfun n s = 0/(s−1)^{n+1} = 0 ✓. So Rfun =ᶠ[𝓝[≠] 1] 0 ⟹ isBigO: EventuallyEq ⟹ IsBigO: (0 function) =O 1 (isBigO_zero), .congr' ✓.\n- ≠ ⊤: obtain ⟨h, hh, hh0, hfh⟩ := g-analytic.analyticOrderAt_ne_top.mp — g =ᶠ[𝓝 1] (s−1)^m • h, m := analyticOrderNatAt g 1, h analytic, h(1) ≠ 0. From (n+1) ≤ order = m (order is finite so the ℕ∞ inequality gives n+1 ≤ m as nats: analyticOrderAt_eq_natCast? For finite order, analyticOrderAt g 1 = (m : ℕ∞) — there's `AnalyticAt.analyticOrderAt_eq_natCast`? The factorization gives order = m... hmm: from hfh, analyticOrderAt g 1 = analyticOrderNatAt g 1 casted — I think `AnalyticAt.analyticOrderAt_eq_natCast` or from the factorization directly. Let me just derive: n+1 ≤ analyticOrderAt g 1 and analyticOrderAt g 1 ≠ ⊤ ⟹ n+1 ≤ analyticOrderNatAt g 1: since analyticOrderAt = ((toNat) : ℕ∞) when ≠ ⊤ for analytic? There's `AnalyticAt.analyticOrderAt_eq_natCast : analyticOrderAt f z₀ ≠ ⊤ → analyticOrderAt f z₀ = analyticOrderNatAt f z₀`? Something like that should exist. Then n+1 ≤ m in ℕ via Nat.cast_le.\n  Then for s ≠ 1 (and in the eventually sets): Rfun n s = g s/(s−1)^{n+1} = (s−1)^m·h s/(s−1)^{n+1} = (s−1)^{m−(n+1)}·h s. As s → 1: if m > n+1: (s−1)^{positive}·h s → 0·h(1) = 0; if m = n+1: → h(1). Tendsto Rfun n (𝓝[≠] 1) (𝓝 L) with L = if m = n+1 then h 1 else 0... uniform: Tendsto (fun s => (s−1)^{m−(n+1)}·h s) (𝓝[≠] 1) (𝓝 ((1−1)^{m−(n+1)}·h 1))? 0^{m−n−1}·h(1): if m = n+1, 0⁰ = 1, L = h(1) ✓; if m > n+1, 0 ✓. So L = (0:ℂ)^(m−n−1)·h(1) — with 0⁰ = 1 convention ✓. Tendsto: (s−1)^{m−n−1} continuous as a function of s (polynomial/power with natural exponent ✓ continuous everywhere including at 1) → composed: ContinuousAt (fun s => (s−1)^(m−n−1)·h s) 1 (h continuous at 1) ⟹ Tendsto on 𝓝 1, restrict to 𝓝[≠] ✓. Then Rfun =ᶠ[𝓝[≠] 1] that-function ⟹ Tendsto Rfun (𝓝[≠] 1) (𝓝 L) via Tendsto.congr'. Then .isBigO_one.\n\nWait — m−(n+1) : ℕ subtraction ✓ since n+1 ≤ m ✓. And (s−1)^(m−n−1) with s near 1: continuous ✓ (it's a polynomial function: (w−1)^k).\n\nHmm — careful with Rfun n s = g s/(s−1)^{n+1} on 𝓝[≠] 1 eventually: the chain of eventuallys:\n- eventually ζ s ≠ 0 on 𝓝[≠] 1 (from residue_one.eventually_ne).\n- s ≠ 1 on 𝓝[≠] 1 (self_mem_nhdsWithin).\n- g = (s−1)^m•h eventually on 𝓝 1, pulled to 𝓝[≠] (mem_nhdsWithin_of_mem_nhds).\n- The Jlag/ppart identities hold for all s ≠ 1 with ζ s ≠ 0 (not eventually — pointwise given those conditions) ✓.\n\nSo ∀ᶠ s in 𝓝[≠] 1, Rfun n s = (s−1)^(m−n−1)·h s. Then Tendsto.congr' ✓.\n\nThe algebra: g s/(s−1)^{n+1} = (s−1)^m h s/(s−1)^{n+1} = (s−1)^{m}·h s·(s−1)^{-(n+1)}... in Lean: (s−1)^m = (s−1)^{n+1}·(s−1)^{m−(n+1)} (pow_add with m = n+1 + (m−n−1) ✓). Then g s/(s−1)^{n+1} = (s−1)^{n+1}·((s−1)^{m−n−1}·h s)/(s−1)^{n+1} = (s−1)^{m−n−1}·h s (mul_div_cancel_left, (s−1)^{n+1} ≠ 0 since s ≠ 1 ✓).\n\nAlso the F − TP = g and Rfun = g/(s−1)^{n+1} derivation:\n(s−1)^{n+1}·Rfun n s = F s − TP s:\n  (s−1)^{n+1}·Jlag n s: kFun n s = (s/(s−1))ⁿ − 1. (s−1)^{n+1}·((s/(s−1))ⁿ−1) = (s−1)·sⁿ/(s−1)ⁿ·... let me redo: (s/(s−1))ⁿ = sⁿ/(s−1)ⁿ (div_pow). (s−1)^{n+1}·(sⁿ/(s−1)ⁿ − 1) = (s−1)^{n+1}·sⁿ/(s−1)ⁿ − (s−1)^{n+1} = (s−1)·sⁿ − (s−1)^{n+1} = (s−1)(sⁿ − (s−1)ⁿ). ✓ Then times (−logDeriv ζ s) = −deriv ζ s/ζ s: (s−1)(sⁿ−(s−1)ⁿ)·(−deriv ζ s/ζ s) = (sⁿ−(s−1)ⁿ)·[(s−1)·(−deriv ζ s/ζ s)] = (sⁿ−(s−1)ⁿ)·hLi s by hLi_eq_of_ne ✓.\n  (s−1)^{n+1}·ppart n s = Σ_{i∈Icc 1 (n+1)} Acoeff n i·(s−1)^{n+1−i}: (s−1)^{n+1}·(Acoeff n i/(s−1)^i) = Acoeff n i·(s−1)^{n+1−i}: (s−1)^{n+1}/(s−1)^i = (s−1)^{n+1−i} via pow_sub_of... for s−1 ≠ 0: zpow or: (s−1)^{n+1} = (s−1)^i·(s−1)^{n+1−i} (pow_add, i ≤ n+1 ✓) then mul_div_cancel_left... Actually the term is Acoeff n i/(s−1)^i, times (s−1)^{n+1}: = Acoeff n i·(s−1)^{n+1}/(s−1)^i = Acoeff n i·(s−1)^{n+1−i} via pow_sub (s−1 ≠ 0) (i ≤ n+1) ✓. `pow_sub : a ≠ 0 → m ≤ n... ` hmm `pow_sub (a : M) (h : n ≤ m) ...`? There's `pow_sub_of...`? In a field: `pow_sub₀ : a ≠ 0 → n ≤ m → a^(m−n) = a^m/a^n`. ✓\n  Then reindex Σ_{i∈Icc 1 (n+1)} f(i) = Σ_{j∈range(n+1)} f(n+1−j) — Finset.sum_bij or: Icc 1 (n+1) maps j = n+1−i to range(n+1)... i ∈ [1, n+1] ⟹ j = n+1−i ∈ [0, n] ✓. Reindexing via Finset.sum_bij (pattern in ResW1_eq_sum ✓).\n  And Acoeff n (n+1−j) = iteratedDeriv (n+1−(n+1−j)) F 1/(n+1−(n+1−j))! = iteratedDeriv j F 1/j! (j ≤ n ⟹ n+1−(n+1−j) = j ✓ omega). So TP s := Σ_{j∈range(n+1)} (iteratedDeriv j F 1/j!)·(s−1)^j ✓ matches.\n\nThen Rfun n s = (F s − TP s)/(s−1)^{n+1}: from (s−1)^{n+1}·Rfun = F − TP and (s−1)^{n+1} ≠ 0: eq_div_of_mul_eq... ✓.\n\nGreat, the plan is solid. Now — where to put this? New file `NguyenRH1/LiSides.lean` importing LiResidue + LiPrincipal + the vendored RectangleLogDeriv.\n\nStructure of LiSides.lean:\n1. `kFun (n : ℕ) (s : ℂ) : ℂ := (s/(s−1))ⁿ − 1`\n2. `Jlag (n : ℕ) (s : ℂ) : ℂ := kFun n s * (−logDeriv riemannZeta s)` — hmm or with explicit −(deriv ζ s/ζ s)? logDeriv_apply makes them equal by rfl-ish (logDeriv f s = deriv f s / f s — logDeriv_apply is a simp lemma: `logDeriv_apply : logDeriv f a = deriv f a / f a`). So Jlag n s := kFun n s * (−(deriv riemannZeta s / riemannZeta s)) and use logDeriv_apply to bridge. Let me use the explicit form for consistency with hLi_eq_of_ne.\n\n3. `Rfun (n : ℕ) : ℂ → ℂ := Jlag n − ppart n` (Pi subtraction).\n\n4. Helper: `rectangle_mem_nhds_of_mem_not_border` — extract the vendored hZint argument (lines 184–197 of RectangleLogDeriv) as a standalone lemma: (hmem : s ∈ Rectangle z w) (hb : s ∉ RectangleBorder z w) : Rectangle z w ∈ 𝓝 s. Wait — the vendored one derives it under hre/him (z.re ≤ w.re etc.). General statement: for z w with z.re ≤ w.re, z.im ≤ w.im: s ∈ Rectangle ∖ border ⟹ Rectangle ∈ 𝓝 s. Via rectangle_mem_nhds_iff (needs the Ioo conditions). The vendored proof: rw [rectangle_mem_nhds_iff, mem_reProdIm, uIoo_of_le hre, uIoo_of_le him] then strict inequalities from not-border. I'll mirror it.\n\n5. `zeta_order_ne_top_of_ne {ρ : ℂ} (hρ : ρ ≠ 1) : analyticOrderAt riemannZeta ρ ≠ ⊤`.\n   - zetaA_analytic : AnalyticOnNhd ℂ zetaA univ.\n   - h1 : analyticOrderAt zetaA 1 ≠ ⊤: zetaA 1 = 1 ≠ 0 ⟹ analyticOrderAt_eq_zero (needs: analyticOrderAt_eq_zero.mpr — the form seen: analyticOrderAt_eq_zero.mpr (.inr hfz) — so analyticOrderAt_eq_zero : analyticOrderAt f z = 0 ↔ (¬analytic? or f z ≠ 0)... the .inr suggests: (order = 0) ↔ (f not analytic at z) ∨ (f z ≠ 0)?? Hmm interesting — for non-analytic f, order is 0 by junk. So analyticOrderAt zetaA 1 = 0 since zetaA 1 = 1 ≠ 0 ✓ then ≠ ⊤ by simp.\n   - hρz : analyticOrderAt zetaA ρ ≠ ⊤ := analyticOrderAt_ne_top_of_isPreconnected (U := univ) zetaA_analytic isPreconnected_univ (mem_univ 1) (mem_univ ρ) h1.\n   - Bridge: analyticOrderAt zetaA ρ = analyticOrderAt riemannZeta ρ:\n     zetaA =ᶠ[𝓝 ρ] fun w => (w−1)·ζ w (eventually, ρ ≠ 1 ✓ zetaA_apply).\n     Need `analyticOrderAt_congr : f =ᶠ[𝓝 z] g → analyticOrderAt f z = analyticOrderAt g z`? Hmm — does it exist? Analytic order is defined via... let me check. If not, route through the mul: analyticOrderAt (fun w => (w−1)·ζ w) ρ = analyticOrderAt (w−1) ρ + analyticOrderAt ζ ρ via `analyticOrderAt_mul` (hopes: (hf : AnalyticAt) (hg : AnalyticAt) hypotheses). analyticOrderAt (fun w => w−1) ρ = 0 (value ρ−1 ≠ 0, analyticOrderAt_eq_zero.mpr (.inr ...)). So order of the mul = order of ζ. Then congr with zetaA.\n     Let me grep for analyticOrderAt_congr and analyticOrderAt_mul signatures.\n\n6. `Rfun_bounded_near_one (n : ℕ) : Rfun n =O[𝓝[≠] 1] (1 : ℂ → ℂ)` — the removable singularity (main work, steps above).\n\n7. `Rfun_residue_at_zero {ρ : ℂ} (hρ1 : ρ ≠ 1) (hρ0 : riemannZeta ρ = 0)`: ((Rfun n) − fun s => (zeroMult ρ : ℂ)·(1 − (ρ/(ρ−1))ⁿ)/(s−ρ)) =O[𝓝[≠] ρ] 1.\n   Wait — I realize the residue statement doesn't even need hρ0 (works for m = 0 too as noted). But our application has ζ ρ = 0. Keep the hypothesis minimal: just hρ1 : ρ ≠ 1. Then A ρ := (analyticOrderNatAt riemannZeta ρ : ℂ)·(1−(ρ/(ρ−1))ⁿ) — and for non-zero points it's 0 anyway. Fine, minimal hypotheses: ρ ≠ 1.\n\n8. Main: `rectInt'_Jlag` (n : ℕ) (z w : ℂ) (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (h1 : Rectangle z w ∈ 𝓝 1) (hborder : ∀ s ∈ RectangleBorder z w, riemannZeta s ≠ 0) :\n   RectangleIntegral' (Jlag n) z w = ResW1 n + Σ ρ ∈ Sz, (zeroMult ρ : ℂ)·(1 − (ρ/(ρ−1))ⁿ)\n   where Sz := (finite_zeros_rectangle zetaA_analyticOnNhd (mem_of_mem_nhds h1) (zetaA 1 ≠ 0)).toFinset.\n\n   Assembly as planned. The A function for residueTheorem_finset: A : ℂ → ℂ := fun p => if p = 1 then 0 else (zeroMult p : ℂ)·(1−(p/(p−1))ⁿ). Since 1 ∉ Sz, on Sz it's the formula ✓.\n\n   residueTheorem_finset needs hS : ∀ p ∈ insert 1 Sz, Rectangle z w ∈ 𝓝 p:\n   - p = 1: h1 ✓.\n   - p ∈ Sz: p ∈ Rectangle ∩ zetaA⁻¹'0 (mem_toFinset) ⟹ p ∈ Rectangle; p ∉ border: if p ∈ border then ζ p ≠ 0 (hborder) but zetaA p = 0 and p ≠ 1 (1 ∉ Sz since zetaA 1 = 1 ≠ 0... need 1 ∉ Sz: if 1 ∈ Sz then zetaA 1 = 0, contra zetaA_one) — so zetaA p = (p−1)·ζ p = 0 with p ≠ 1 ⟹ ζ p = 0 — contradiction with hborder. So p ∉ border ⟹ Rectangle ∈ 𝓝 p by helper ✓.\n\n   fHolo: HolomorphicOn (Rfun n) (Rectangle z w \\ ↑(insert 1 Sz)):\n   s ∈ Rectangle ∖ S ⟹ s ≠ 1 ∧ s ∉ Sz. ζ s ≠ 0: if ζ s = 0 then zetaA s = (s−1)·0 = 0 (s ≠ 1 ⟹ zetaA_apply) ⟹ s ∈ Rectangle ∩ zetaA⁻¹'0 ⟹ s ∈ Sz (mem_toFinset) — contra. So DifferentiableAt (Rfun n) s:\n   - kFun n differentiable at s (s ≠ 1): fun_prop-ish.\n   - −(deriv ζ/ζ) differentiable at s: analyticAt_riemannZeta (s≠1).deriv.div ... ✓.\n   - ppart n differentiable at s: sum of const/(s−1)^i ✓.\n   Combine ✓ then .differentiableWithinAt.\n\n   near: ∀ p ∈ insert 1 Sz, ...:\n   - p = 1: A 1 = 0 (if_pos rfl) ⟹ Rfun − 0/(s−1) = Rfun — need Rfun =O[𝓝[≠] 1] 1 — Rfun_bounded_near_one ✓. Careful: the near statement is ((Rfun n) − fun s => A p/(s−p)) =O ... with A 1 = 0: (fun s => (0:ℂ)/(s−1)) = 0 function; Rfun − 0 = Rfun: need a congr/simp to bridge ✓.\n   - p ∈ Sz: A p = formula (if_neg: p ≠ 1 since 1 ∉ Sz) ⟹ Rfun_residue_at_zero (p ≠ 1 ✓) ✓.\n\n   Then residueTheorem_finset hre him (insert 1 Sz) A hS fHolo near : RectangleIntegral' (Rfun n) z w = Σ_{p ∈ insert 1 Sz} A p = A 1 + Σ_{p ∈ Sz} A p (sum_insert, 1 ∉ Sz) = 0 + Σ formula ✓.\n\n   Assembly:\n   RectangleIntegral' (Jlag n) z w = RectangleIntegral' (Rfun n + ppart n) z w (congr: Rfun + ppart = Jlag − ppart + ppart = Jlag ✓ sub_add_cancel as functions: (Jlag n − ppart n) + ppart n = Jlag n by sub_add_cancel ✓ (Pi instSub/add group ✓)).\n   = RectangleIntegral' (Rfun n) + RectangleIntegral' (ppart n) (RectangleIntegral'_add — needs RectangleBorderIntegrable each:\n   - Rfun: ContinuousOn.rectangleBorder_integrable: Rfun continuous on Rectangle ∖ S ⊇ border: border ∩ S = ∅: s ∈ border ⟹ s ≠ 1?? WAIT — is 1 on the border possible? h1 : Rectangle ∈ 𝓝 1 ⟹ 1 ∉ border (not_mem_rectangleBorder_of_rectangle_mem_nhds ✓ used in LiPrincipal). And s ∈ border ⟹ ζ s ≠ 0 (hborder) ⟹ s ∉ Sz (as above) ⟹ s ∈ Rectangle ∖ S ✓ (border ⊆ Rectangle ✓ rectangleBorder_subset_rectangle). ContinuousOn (Rfun n) (Rectangle ∖ S) from HolomorphicOn.continuousOn ✓ .mono ✓.\n   - ppart: HolomorphicOn.rectangleBorderIntegrable' with h1 (LiPrincipal's hAint/hGint pattern — actually I proved integrability of the two pieces; ppart = A_1/(w−1) + deriv Gprim: hAint + hGint both proved in rectInt'_ppart — but they're local haves. I need a standalone `ppart_borderIntegrable` lemma: HolomorphicOn (ppart n) (Rectangle ∖ {1}) ⟹ rectangleBorderIntegrable' h1. The HolomorphicOn: s ≠ 1 ⟹ each Acoeff n i/(s−1)^i differentiable ✓ (pattern from tail_continuousAt/hAint).\n   )\n   = Σ formula + ResW1 n (rectInt'_ppart hre him h1 ✓)\n   = ResW1 n + Σ formula (add_comm) ✓.\n\nWait — RectangleIntegral'_add signature (LiPrincipal): RectangleIntegral'_add (f g : ℂ → ℂ) (z w : ℂ) (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) : RectangleIntegral' (f + g) z w = ... ✓.\n\nOne more check — `RectangleIntegral'_congr`: used in LiPrincipal (line 276): takes Set.EqOn on the border ✓ (from ResidueCalcOnRectangles presumably) — for Jlag = Rfun + ppart I have actual function equality, so plain rw/congr works.\n\nAlso `ResidueTheoremInRectangle hre him h1` — used inside rectInt'_ppart ✓ already compiled.\n\nNow — the logDeriv NF computation details for the residue at ρ:\n\nobtain ⟨h, hh, hh0, hfh⟩ := (analyticAt_riemannZeta hρ1).analyticOrderAt_ne_top.mp (zeta_order_ne_top_of_ne hρ1)\n\nhfh : riemannZeta =ᶠ[𝓝 ρ] fun s => (s − ρ) ^ analyticOrderNatAt riemannZeta ρ • h s\n\n(Signature check needed: AnalyticAt.analyticOrderAt_ne_top : analyticOrderAt f z₀ ≠ ⊤ → ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ (f =ᶠ[𝓝 z₀] fun z => (z − z₀)^analyticOrderNatAt f z₀ • g z) — from vendored usage ✓ roughly; I'll check exact statement.)\n\nThen near ρ, s ≠ ρ:\nlogDeriv ζ s = logDeriv ((s−ρ)^m • h) s = logDeriv ((s−ρ)^m) s + logDeriv h s = m/(s−ρ) + logDeriv h s.\n- logDeriv_mul needs: (s−ρ)^m ≠ 0 (s ≠ ρ ✓), h s ≠ 0 (eventually near ρ since h(ρ) ≠ 0 ✓ hh.continuousAt.eventually_ne hh0), differentiability: (s−ρ)^m fun_prop ✓, h differentiable at s (hh.eventually_analyticAt ✓).\n- logDeriv ((s−ρ)^m) s = m/(s−ρ): vendored pattern: rw [show (fun s => (s−ρ)^m) = (fun x => x^m) ∘ (fun s => s−ρ) from rfl, logDeriv_comp (by fun_prop) (by fun_prop), logDeriv_pow]; simp — logDeriv (x^m) x = m/x ✓ then comp gives m/(s−ρ)·deriv(s−ρ) = m/(s−ρ)·1 ✓ (the vendored simp handles it).\n- Also need ζ s ≠ 0 at the evaluation point for logDeriv_mul... logDeriv_mul (f ...) (g ...) s (hf : f s ≠ 0) (hg : g s ≠ 0) differentiabilities — vendored line 257: logDeriv_mul (f := fun s => (s−q)^ord) (g := h) s (pow_ne_zero _ hsq) hhs (by fun_prop) hhas.differentiableAt ✓.\n- And logDeriv ζ s = logDeriv ((s−ρ)^m•h) s via hfh.deriv_eq + self_of_nhds at s: vendored line 254-256: simp only [logDeriv_apply, hfs.deriv_eq, hfs.self_of_nhds, smul_eq_mul] where hfs : riemannZeta =ᶠ[𝓝 s] ... (hfh.eventually_nhds at s ∈ nhd) ✓.\n\nThen the expansion identity (vendored hexp pattern):\n∀ᶠ s in 𝓝[≠] ρ, (−(m:ℂ)·((kFun n s − kFun n ρ)/(s−ρ)) − kFun n s·logDeriv h s) = ((Rfun n) − fun s => A ρ/(s−ρ)) s\n\nLHS − RHS: Rfun n s = Jlag n s − ppart n s; Jlag n s = −kFun n s·logDeriv ζ s = −k(s)·(m/(s−ρ) + logDeriv h s) = −m·k(s)/(s−ρ) − k(s)·logDeriv h s. So Rfun n s − A ρ/(s−ρ) = −m·k(s)/(s−ρ) − k(s)·logDeriv h s − ppart(s) − (−m·k(ρ))/(s−ρ) = −m·(k(s)−k(ρ))/(s−ρ) − k(s)·logDeriv h s − ppart(s).\n\nHmm — I forgot ppart in the LHS. So LHS := −m·(k s − k ρ)/(s−ρ) − k s·logDeriv h s − ppart n s. Then:\n- Tendsto (slope) (𝓝[≠] ρ) (𝓝 (deriv (kFun n) ρ)): hasDerivAt_iff_tendsto_slope.mp (kFun-differentiable.hasDerivAt) — vendored line 268-270 ✓ (slope_fun_def_field simpa).\n- Tendsto (k·logDeriv h) (𝓝[≠] ρ) (𝓝 (k ρ·logDeriv h ρ)): ContinuousAt: k continuous at ρ (differentiable), logDeriv h continuous at ρ (hh.deriv.continuousAt.div hh.continuousAt hh0) ✓ mul.\n- Tendsto (ppart n) (𝓝[≠] ρ) (𝓝 (ppart n ρ)): ContinuousAt — sum of Acoeff/(s−1)^i continuous at ρ ≠ 1 — tail_continuousAt pattern but for Icc 1 (n+1)... need a `ppart_continuousAt` lemma: same proof as tail_continuousAt with Icc 1. Minor.\n- Combine: Tendsto LHS (𝓝[≠] ρ) (𝓝 (−m·deriv k − k ρ·logDeriv h ρ − ppart n ρ)) ⟹ .isBigO_one ℂ ⟹ .congr' hexp EventuallyEq.rfl ✓.\n\nThe hexp eventually: needs s ≠ ρ (𝓝[≠]), ζ =ᶠ[𝓝 s] factorization (hfh.eventually_nhds — s ∈ nhd where hfh holds: mem_nhdsWithin_of_mem_nhds (hfh.eventually_nhds)), h s ≠ 0 (hh.continuousAt.eventually_ne hh0 pulled in), h analytic at s (hh.eventually_analyticAt), and k/ppart pointwise — pure algebra at s given logDeriv ζ s = m/(s−ρ) + logDeriv h s. Note: also need deriv ζ s — logDeriv_apply handles. And Jlag n s unfolds: kFun n s * (−(deriv ζ s/ζ s)) = −k s·logDeriv ζ s ✓ (logDeriv_apply simp).\n\nThe algebra in Lean:\nhave hld : logDeriv riemannZeta s = (m : ℂ)/(s−ρ) + logDeriv h s — as vendored.\ngoal: −m·(k s − k ρ)/(s−ρ) − k s·logDeriv h s − ppart n s = (Jlag n − ppart n) s − A ρ/(s−ρ)\nRHS = kFun n s·(−logDeriv ζ s) − ppart n s − (−(m:ℂ)·kFun n ρ)/(s−ρ)   [A ρ = −m·k ρ: m·(1−(ρ/(ρ−1))ⁿ) = −m·((ρ/(ρ−1))ⁿ−1) = −m·k ρ ✓ — wait: kFun n ρ = (ρ/(ρ−1))ⁿ − 1; A ρ := m·(1−(ρ/(ρ−1))ⁿ) = −m·kFun n ρ ✓ by ring]\n= −k s·logDeriv ζ s − ppart n s + m·k ρ/(s−ρ)\nsub hld: = −k s·(m/(s−ρ) + logDeriv h s) − ppart n s + m·k ρ/(s−ρ)\n= −m·k s/(s−ρ) − k s·logDeriv h s − ppart n s + m·k ρ/(s−ρ)\n= −m·(k s − k ρ)/(s−ρ) − k s·logDeriv h s − ppart n s ✓ ring (field_simp for the /(s−ρ) with s−ρ ≠ 0).\n\nLet me define A ρ directly as −(m:ℂ)·kFun n ρ?? NO — the theorem statement should present 1−(ρ/(ρ−1))ⁿ (matches D-064/λ_n assembly downstream). I'll define the residue function as A ρ := (zeroMult ρ : ℂ)·(1 − (ρ/(ρ−1))ⁿ) and prove A ρ = −m·kFun n ρ as a rewrite in the proof.\n\nEdge: m = analyticOrderNatAt ζ ρ vs zeroMult ρ — defeq (both (analyticOrderAt ζ ρ).toNat) — bridge by rfl/show.\n\nAlso n = 0 edge: Jlag 0 = kFun 0·(−logDeriv ζ) = (1−1)·(...) = 0! ResW1 0 = iteratedDeriv 0 (fun w => (w⁰−(w−1)⁰)·hLi w) 1/0! = (1−1)·hLi 1 /1 = 0 ✓. Sum: Σ zeroMult·(1−(ρ/(ρ−1))⁰) = Σ zeroMult·(1−1) = 0 ✓. So theorem holds for n = 0 trivially-ish (0 = 0 + 0). The proofs should go through uniformly (kFun 0 = 0 differentiable ✓; slope trivial ✓). Actually careful: hLi machinery etc. all fine at n=0. OK.\n\nNow — the boundedness at 1 (near condition at 1) — sub-steps in Lean:\n\n(a) `Ffun (n : ℕ) (w : ℂ) : ℂ := (wⁿ − (w−1)ⁿ)·hLi w` — wait, ResW1's function: `fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w` — reused in Acoeff. Define `Ffun n` := that and rewrite ResW1/Acoeff in terms? NO — freeze protocol: don't touch existing files. Define Ffun in LiSides and prove Ffun = the lambda (rfl) to bridge: iteratedDeriv j Ffun 1 = iteratedDeriv j (fun w => ...) 1 by rfl ✓ (defeq). Acoeff n i = iteratedDeriv (n+1−i) Ffun 1/(n+1−i)! by rfl ✓.\n\n(b) `TaylP (n : ℕ) (w : ℂ) : ℂ := Σ j ∈ Finset.range (n+1), (iteratedDeriv j (Ffun n) 1 / j !)·(w−1)^j`.\n\n(c) `ppart_mul_pow : ∀ s, (s−1)^{n+1}·ppart n s = TaylP n s`? Careful — ppart n s = Σ Acoeff n i/(s−1)^i: for s = 1, division by 0 gives 0 (junk): LHS at s=1: 0^{n+1}·(Σ A_i/0^i) = 0·(Σ A_i/0) = 0·0 = 0?? 0^{n+1} = 0 (n+1 ≥ 1) ✓, and ppart n 1 = Σ A_i/(1−1)^i = Σ A_i/0^i: 0^i = 0 for i ≥ 1 ✓, A_i/0 = 0 ✓ so ppart n 1 = 0; LHS = 0·0 = 0. RHS TaylP n 1 = Σ_j c_j·0^j = c_0·0⁰ = c_0 = iteratedDeriv 0 Ffun 1/0! = Ffun 1 = (1−0)·hLi 1 = 1·1 = 1?? WAIT: Ffun 1 = (1ⁿ−(1−1)ⁿ)·hLi 1 = (1−0ⁿ)·1. 0ⁿ: for n ≥ 1: 0; so Ffun 1 = 1. For n = 0: 1⁰−0⁰ = 1−1 = 0, Ffun 1 = 0. Hmm so TaylP n 1 = c_0 = Ffun 1 ≠ 0 for n ≥ 1 — but LHS = 0 at s = 1. So the identity (s−1)^{n+1}·ppart n s = TaylP n s FAILS at s = 1 (junk division). So state it for s ≠ 1 only: `ppart_mul_pow {s : ℂ} (hs : s ≠ 1) : (s−1)^{n+1}·ppart n s = TaylP n s`. Fine — we only need it on 𝓝[≠] 1 anyway. (Alternatively define things to avoid the junk, but s ≠ 1 hypothesis is cleanest.)\n\nHmm wait, actually — for (c) at s ≠ 1: (s−1)^{n+1}·ppart n s = Σ_{i∈Icc 1 (n+1)} Acoeff n i·(s−1)^{n+1}/(s−1)^i = Σ Acoeff n i·(s−1)^{n+1−i} (pow_sub₀ (sub_ne_zero hs) (i ≤ n+1 ✓)). Then reindex j := n+1−i ∈ [0, n] = range(n+1): term becomes Acoeff n (n+1−j)·(s−1)^j = (iteratedDeriv j Ffun 1/j!)·(s−1)^j ✓ (Acoeff n (n+1−j): n+1−(n+1−j) = j for j ≤ n ✓). Finset.sum_bij (i ↦ n+1−i) from Icc 1 (n+1) to range(n+1) ✓ (pattern from ResW1_eq_sum).\n\n(d) `Jlag_mul_pow {s : ℂ} (hs1 : s ≠ 1) (hs0 : riemannZeta s ≠ 0) : (s−1)^{n+1}·Jlag n s = Ffun n s`:\n(s−1)^{n+1}·kFun n s·(−logDeriv ζ s): kFun n s = (s/(s−1))ⁿ−1 = (sⁿ−(s−1)ⁿ)/(s−1)ⁿ (field_simp, div_pow). (s−1)^{n+1}·that = (s−1)·(sⁿ−(s−1)ⁿ). Then ·(−deriv ζ s/ζ s) — via logDeriv_apply. = (sⁿ−(s−1)ⁿ)·[(s−1)·(−deriv ζ s/ζ s)] = (sⁿ−(s−1)ⁿ)·hLi s [hLi_eq_of_ne hs1 hs0] = Ffun n s ✓. In Lean: field_simp + ring + hLi_eq_of_ne. Manageable.\n\n(e) `Rfun_eq_div_near_one`: ∀ᶠ s in 𝓝[≠] 1, Rfun n s = (Ffun n s − TaylP n s)/(s−1)^{n+1}:\neventually ζ s ≠ 0: from riemannZeta_residue_one.eventually_ne (show (1:ℂ) ≠ 0): gives ∀ᶠ w in 𝓝[≠] 1, (w−1)·ζ w ≠ 0 ⟹ ζ w ≠ 0 (mul_ne_zero) — as in hLi_eq_near_one ✓.\nFor such s (≠ 1, ζ ≠ 0): Rfun n s = Jlag n s − ppart n s; (s−1)^{n+1}·Rfun n s = Ffun n s − TaylP n s [by (d), (c)] ⟹ Rfun n s = (Ffun n s − TaylP n s)/(s−1)^{n+1} (eq_div_of_mul_eq, (s−1)^{n+1} ≠ 0) ✓.\n\n(f) `Ffun_sub_TaylP_order : (n+1 : ℕ∞) ≤ analyticOrderAt (Ffun n − TaylP n) 1`:\nAnalyticAt: Ffun n analytic at 1: ((analyticAt_id.pow n).sub ((analyticAt_id.sub analyticAt_const).pow n)).mul hLi_analyticAt_one ✓. TaylP: finite sum of const·(w−1)^j analytic ✓ (DifferentiableAt/AnalyticAt.sum patterns; analyticAt: AnalyticAt.mul (analyticAt_const) (((analyticAt_id.sub analyticAt_const).pow j))... use Finset AnalyticAt.sum? There's `AnalyticAt.sum`? maybe `analyticAt_sum`? If not: Finset.induction like tail_continuousAt. Minor work.\niteratedDeriv i (Ffun n − TaylP n) 1 = 0 for i < n+1:\n  ContDiffAt both (analytic ⟹ ContDiffAt: AnalyticAt.contDiffAt ✓ (with ⊤ withTop... contDiffAt of order i: hAnalyticAt.contDiffAt — signature: AnalyticAt.contDiffAt : ContDiffAt 𝕜 n f z? in LiResidue: hLi_analyticAt_one.contDiffAt used with iteratedDeriv_mul hA hh where hA : ContDiffAt ℂ n ... 1 — so .contDiffAt gives ContDiffAt ℂ ↑n? There was a coercion — in ResW1_eq_sum: `have hA : ContDiffAt ℂ n (fun w : ℂ => w ^ n - (w - 1) ^ n) 1 := (...).contDiffAt` where (...) : ContDiff ℂ _ _ → contDiffAt — hmm that one built ContDiff directly from contDiff_id.pow. For analytic: AnalyticAt.contDiffAt exists (used at LiResidue:200: hh := hLi_analyticAt_one.contDiffAt : ContDiffAt ℂ n hLi 1 ✓).\n  iteratedDeriv_sub hF hT ✓ (used in A_iter).\n  iteratedDeriv i (TaylP n) 1 = iteratedDeriv i (Ffun n) 1 for i ≤ n:\n    iteratedDeriv over the sum: `iteratedDeriv_sum`? Does that exist? Hmm — iteratedDeriv is iterated deriv; deriv_sum exists (used in deriv_Gprim: `deriv_sum (fun i hi => ?_)` — signature deriv_sum (h : ∀ i ∈ s, DifferentiableAt ℂ (f i) x) : deriv (∑ i ∈ s, f i) x = ∑ i ∈ s, deriv (f i) x? roughly). iteratedDeriv_sum: might exist `iteratedDeriv_sum (h : ∀ i ∈ s, ContDiffAt ... )`. If not, induct manually or use iteratedDeriv = deriv^i via iteratedDeriv_eq... Alternative: avoid the sum-deriv lemma by a different characterization: TaylP n w = Σ_j c_j (w−1)^j is a POLYNOMIAL in (w−1) — rewrite as `Polynomial.eval`? Heavier. Try `iteratedDeriv_sum` first; grep Mathlib.\n\n    Actually — better idea: there might be direct Mathlib machinery for the Taylor polynomial: `Mathlib.Analysis.Calculus.Taylor`? or `AnalyticAt` has `hasSum...`? Hmm, alternatively use the FORMAL MULTILINEAR SERIES machinery: Ffun analytic at 1 ⟹ HasFPowerSeriesAt... the order criterion via `HasFPowerSeriesAt` coefficients: `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` needs iteratedDeriv — stick with the plan. For the sum: I'll check for iteratedDeriv_sum; else prove by induction on the finset (like tail_continuousAt) using iteratedDeriv_add (needs ContDiffAt of each piece — fine).\n\n    Term: iteratedDeriv i (fun w => c_j·(w−1)^j) 1 = c_j·iteratedDeriv i (fun w => (w−1)^j) 1 (iteratedDeriv_const_mul — exists? `iteratedDeriv_const_mul`... there's `iteratedDeriv_const_mul`? For deriv: deriv_const_mul ✓ (used). iterated version: `iteratedDeriv_const_mul` probably exists (ContDiff hypothesis needed). Then iteratedDeriv i (fun w => (w−1)^j) 1 = if i = j then j! else 0 (for i ≤ n, j ≤ n): from A_iter's h2: iteratedDeriv i (fun w => (w−1)^j) 1 = j.descFactorial i·(0:ℂ)^{j−i}:\n      - j < i: j.descFactorial i = 0 (Nat.descFactorial_eq_zero_iff_lt: i > j ⟹ 0) ✓ term 0.\n      - j = i: i.descFactorial i = i! (Nat.descFactorial_self), 0⁰ = 1 ⟹ j! ✓.\n      - j > i: 0^{j−i} = 0 ⟹ 0 ✓.\n    So Σ_j c_j·(term) = c_i·i! = (iteratedDeriv i Ffun 1/i!)·i! = iteratedDeriv i Ffun 1 (i! ≠ 0) ✓.\n  So iteratedDeriv i (Ffun − TaylP) 1 = 0 ✓. Then (f) via natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero (the analytic at 1) — ∀ i < n+1 ✓.\n\n(g) `Rfun_tendsto_one`: ∃ L, Tendsto (Rfun n) (𝓝[≠] 1) (𝓝 L):\n  g := Ffun n − TaylP n; hg : AnalyticAt ℂ g 1; hord := (f).\n  by_cases htop : analyticOrderAt g 1 = ⊤:\n  - analyticOrderAt_eq_top.mp htop : ∀ᶠ s in 𝓝 1, g s = 0. Pull to 𝓝[≠] (mem_nhdsWithin_of_mem_nhds), combine with (e): ∀ᶠ s in 𝓝[≠] 1, Rfun n s = g s/(s−1)^{n+1} = 0/(...) = 0. So Rfun n =ᶠ[𝓝[≠] 1] 0 ⟹ Tendsto ... (𝓝 0) := tendsto_congr' ... tendsto_const_nhds. ⟨0, ...⟩ ✓.\n  - ≠ ⊤: obtain ⟨h, hh, hh0, hfh⟩ := hg.analyticOrderAt_ne_top.mp htop. m := analyticOrderNatAt g 1. Order cast: analyticOrderAt g 1 = (m : ℕ∞): `AnalyticAt.analyticOrderAt_eq_natCast`? grep. Or: from hfh factorization, analyticOrderAt g 1 = m — there might be a lemma `analyticOrderAt_eq_natCast_of_...`. If missing: analyticOrderNatAt g 1 = (analyticOrderAt g 1).toNat and for ≠ ⊤, toNat then cast = id: `ENat.toNat_coe`/`ENat.coe_toNat`: (h : a ≠ ⊤) : (a.toNat : ℕ∞) = a — `ENat.coe_toNat h` ✓. So (m : ℕ∞) = analyticOrderAt g 1 by ENat.coe_toNat htop. Then (n+1 : ℕ∞) ≤ (m : ℕ∞) ⟹ n+1 ≤ m by Nat.cast_le (ENat cast mono: `Nat.cast_le`? for ℕ∞: WithTop... `Nat.cast_le : (m : ℕ∞) ≤ n ↔ m ≤ n`? there's `Nat.cast_le` for ordered semirings; for ℕ∞ (WithTop ℕ): `Nat.cast_le : (↑m ≤ ↑n) ↔ m ≤ n`? should exist as `Nat.cast_le` via WithTop... might be `WithTop.coe_le_coe`... ℕ∞ = WithTop? NO — ℕ∞ = ENat = WithTop ℕ ✓ actually yes, ℕ∞ notation for ENat which is WithTop ℕ? ENat is defined as WithTop ℕ ✓. Nat.cast to WithTop ℕ: the coercion... `Nat.cast_le` might not directly apply; there's `WithTop.coe_le_coe : (↑m : WithTop ℕ) ≤ ↑n ↔ m ≤ n` ✓ and the cast (m : ℕ∞) vs (↑m : WithTop ℕ) — ENat instNatCast: (m : ℕ∞) = (m : WithTop ℕ)? ENat's NatCast instance is defined via WithTop.some ✓ defeq-ish; the natCast_le_analyticOrderAt lemma uses `n ≤ analyticOrderAt` with n : ℕ casted into ℕ∞ presumably (Nat.cast). Bridging: Nat.cast_le for ℕ∞: I recall `Nat.cast_le (α := ℕ∞)`? ENat has `ENat.coe_le_coe`? hmm, there are lemmas `ENat.coe_le_coe : (m : ℕ∞) ≤ n ↔ m ≤ n`? I'll figure it out — standard.\n  Then hm : n+1 ≤ m.\n  ∀ᶠ s in 𝓝[≠] 1: Rfun n s = g s/(s−1)^{n+1} [by (e)] = (s−1)^m·h s/(s−1)^{n+1} [hfh.eventually_nhds pulled in + smul_eq_mul] = (s−1)^{m−(n+1)}·h s [pow_add + mul_div_cancel_left, s ≠ 1].\n  Let φ(s) := (s−1)^{m−(n+1)}·h s: ContinuousAt φ 1 (h continuous: hh.continuousAt; (s−1)^k continuous) ⟹ Tendsto φ (𝓝 1) (𝓝 (φ 1)); restrict 𝓝[≠] (mono_left nhdsWithin_le_nhds); Tendsto.congr' (eventually-eq) ⟹ Tendsto (Rfun n) (𝓝[≠] 1) (𝓝 (φ 1)) ✓ ⟨φ 1, ...⟩.\n  \n(h) `Rfun_bounded_near_one : Rfun n =O[𝓝[≠] 1] (1 : ℂ → ℂ)` := obtain ⟨L, hL⟩ := (g); hL.isBigO_one ℂ ✓.\n\nThat's the full plan for the near-at-1 piece.\n\nNow fHolo differentiability of Jlag at s (s ≠ 1, ζ s ≠ 0):\n- kFun n: DifferentiableAt ℂ (fun s => (s/(s−1))ⁿ − 1) s: (differentiableAt_id.div (differentiableAt_id.sub (differentiableAt_const 1)) (sub_ne_zero hs1)).pow n |>.sub (differentiableAt_const 1) — or fun_prop (disch := assumption) — the vendored code used fun_prop with disch. fun_prop might work: `fun_prop (disch := assumption)` where the side goal s − 1 ≠ 0 solved from context? Side conditions like `s − 1 ≠ 0` — fun_prop's discharger `assumption`... the hypothesis in context is hs1 : s ≠ 1 — need s − 1 ≠ 0 — assumption won't close it directly (needs sub_ne_zero.mpr hs1). So provide explicitly or `fun_prop (disch := simp_all [sub_ne_zero])`... safer: manual composition as in LiResidue (differentiableAt_id.sub ...).mul etc. Manual is verbose but reliable. For kFun: \n  have h1d : DifferentiableAt ℂ (fun s : ℂ => s - 1) s := differentiableAt_id.sub (differentiableAt_const 1)\n  have h2d : DifferentiableAt ℂ (fun s : ℂ => s / (s - 1)) s := differentiableAt_id.div h1d (sub_ne_zero.mpr hs1)\n  have hkd : DifferentiableAt ℂ (fun s : ℂ => (s / (s - 1)) ^ n - 1) s := (h2d.pow n).sub (differentiableAt_const 1)\n- logDeriv part: DifferentiableAt ℂ (fun s => -(deriv riemannZeta s / riemannZeta s)) s: (analyticAt_riemannZeta hs1).deriv : AnalyticAt ℂ (deriv riemannZeta) s ⟹ .differentiableAt; analyticAt_riemannZeta hs1 .differentiableAt; div with hs0; neg. ✓\n- Jlag = mul ✓. Rfun = sub with ppart differentiable ✓ (ppart: Finset sum of div-pow: DifferentiableAt.sum with each (differentiableAt_const _).div ((differentiableAt_id.sub (differentiableAt_const _)).pow _) (pow_ne_zero _ (sub_ne_zero.mpr hs1)) ✓).\n\nNow — is `HolomorphicOn` the right target? residueTheorem_finset's fHolo : HolomorphicOn f (Rectangle z w \\ ↑S). HolomorphicOn f s := DifferentiableOn ℂ f s (def). DifferentiableAt ⟹ DifferentiableWithinAt ✓.\n\nNow the Sz characterization and 1 ∉ Sz:\nSz := hfin.toFinset where hfin := finite_zeros_rectangle hzetaA (mem_of_mem_nhds h1) hzetaA1.\n- mem: s ∈ Sz ⟺ s ∈ Rectangle z w ∧ zetaA s = 0 (Set.Finite.mem_toFinset, mem_inter_iff, mem_preimage, mem_singleton_iff).\n- 1 ∉ Sz: zetaA 1 = 1 ≠ 0 ✓.\n- s ∈ Sz ⟹ s ≠ 1 (from above).\n- s ∈ Sz ⟹ ζ s = 0: zetaA s = 0, s ≠ 1 ⟹ zetaA_apply: (s−1)·ζ s = 0 ⟹ ζ s = 0 (s−1 ≠ 0) ✓.\n- s ∈ Rectangle, s ≠ 1, ζ s = 0 ⟹ s ∈ Sz: zetaA s = (s−1)·ζ s = 0 ✓ mem_toFinset.\n\nWhere does `hzetaA : AnalyticOnNhd ℂ zetaA (Rectangle z w)` come from: intro s hs; by_cases s = 1: zetaA_analyticAt_one / zetaA_analyticAt_of_ne ✓.\n\nhzetaA1 : zetaA 1 ≠ 0 := by rw [zetaA_one]; norm_num ✓.\n\nNow, potential blocker check: `analyticOrderAt_mul` — exact name/hypotheses; `analyticOrderAt_congr`; `AnalyticAt.analyticOrderAt_ne_top` exact statement; `analyticOrderAt_eq_top`; `analyticOrderAt_eq_zero`. Let me grep these in Mathlib/Analysis/Analytic/Order.lean.\n\nAlso `iteratedDeriv_sum` / `iteratedDeriv_const_mul` existence.\n\nAlso `pow_sub₀` name; `mul_div_cancel_left₀`? (mul_div_cancel_left : a·b/a = b with a ≠ 0 — `mul_div_cancel_left₀`?).\n\nAlso ENat cast lemma: `ENat.coe_toNat`/`Nat.cast_le`.\n\nLet me batch-grep these.","signature":""},{"type":"text","text":"Plan is clear. Let me verify the remaining Mathlib lemma names before writing."},{"type":"tool_use","id":"Bash_21","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -n \"theorem analyticOrderAt_mul\\|lemma analyticOrderAt_mul\\|analyticOrderAt_congr\\|theorem analyticOrderAt_eq_top\\|lemma analyticOrderAt_eq_top\\|analyticOrderAt_eq_zero \\|analyticOrderAt_eq_zero\\b\" Mathlib/Analysis/Analytic/Order.lean | head -12; echo ---; sed -n '105,130p' Mathlib/Analysis/Analytic/Order.lean","description":"Check analyticOrderAt lemma signatures"},"extra_content":null},{"type":"tool_use","id":"Bash_22","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"theorem iteratedDeriv_sum\\|lemma iteratedDeriv_sum\\|theorem iteratedDeriv_const_mul\\|lemma iteratedDeriv_const_mul\" Mathlib/ | head -5; echo ---; grep -rn \"theorem pow_sub₀\\|lemma pow_sub₀\" Mathlib/Algebra/ | head -3; echo ---; grep -rn \"coe_toNat\\b\" Mathlib/Data/ENat/Basic.lean | head -5","description":"Check iteratedDeriv/pow/ENat lemma names"},"extra_content":null}]