[{"type":"thinking","thinking":"Now I have the full picture of the vendored machinery. Let me now review the plan for ii′-1b(iii) from STATE.md:\n\n```\nSession 017: **sub-stage ii′-1b(iii) — the rectangle residue theorem\nfor J** (D-064 §4 R1): R := J − ppart n, shown holomorphic on\nRectangle \\ ({zeros} ∪ {−2}) (meromorphic order at 1 ≥ 0 via\nTaylor-remainder: (w−1)^{n+1}·R = F − Tayl_n F vanishes to order n+1 —\nuse `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`); simple\npoles at zeros with residue mult·(1−(ρ/(ρ−1))ⁿ) (via logDeriv NF\ncomputation; multiple zeros OK — logDeriv poles are always simple) and\nat −2 (residue 1−(2/3)ⁿ); apply vendored `residueTheorem_finset`\n(Zeta23/Analytic/RectangleLogDeriv.lean); assemble\nsides(T) = ResW1 n + Σ_{|γ|<T} mult·[1−(ρ/(ρ−1))ⁿ] + triv(n).\n```\n\nLet me think about the math here carefully.\n\n**The integrand J.** From D-064: J(w) = k_n(w−1)·(−ζ′/ζ(w)) where k_n(s) = (1+1/s)ⁿ−1.\n\nHmm, wait. Let me get the exact shape of J. In D-064 §2:\n- J(w) = k_n(w−1)(−ζ′/ζ(w)), k_n(s) = (1+1/s)ⁿ−1 — pole of order n+1 at w=1... \n\nWait: k_n(w−1) = (1+1/(w−1))ⁿ−1 = (w/(w−1))ⁿ − 1. So J(w) = [(w/(w−1))ⁿ − 1]·(−ζ′/ζ(w)).\n\nCheck: (w−1)^{n+1}·J = (w−1)^{n+1}·[(wⁿ−(w−1)ⁿ)/(w−1)ⁿ]·(−ζ′/ζ) = (w−1)(wⁿ−(w−1)ⁿ)(−ζ′/ζ) = [wⁿ−(w−1)ⁿ]·h(w) where h(w) = (w−1)(−ζ′/ζ(w)). ✓ That matches the design and LiResidue.lean's ResW1 definition.\n\n**Poles of J:**\n1. At w = 1: order n+1 (from k_n(w−1) ~ n/(w−1) times −ζ′/ζ's simple pole... wait let me recount. k_n(w−1) = (w/(w−1))ⁿ−1 has a pole of order n at w=1. −ζ′/ζ has a simple pole at w=1 (residue +1... actually −ζ′/ζ has residue +1 at w=1 since ζ has a simple pole with residue 1, so ζ′/ζ has a simple pole with residue −1, hence −ζ′/ζ has residue +1). So J has a pole of order n+1 at w=1. The residue there is ResW1 n = Σ_{j=1}^n C(n,j)·lcoeff(j−1) — PROVED in LiResidue.lean.\n\n2. At nontrivial zeros ρ of ζ: −ζ′/ζ has a simple pole with residue −mult(ρ)... wait: near a zero ρ of order m, ζ(w) = (w−ρ)^m·g(w), so ζ′/ζ = m/(w−ρ) + g′/g, so −ζ′/ζ has residue −m at ρ. And k_n(w−1) is analytic at ρ (ρ ≠ 1, in fact ρ has Re ∈ (0,1) and ρ ≠ 1). So J has a simple pole at ρ with residue k_n(ρ−1)·(−mult) = −mult·[(ρ/(ρ−1))ⁿ−1] = mult·[1−(ρ/(ρ−1))ⁿ].\n\n   Note: 1−1/ρ = (ρ−1)/ρ, so (1−1/ρ)ⁿ = ((ρ−1)/ρ)ⁿ. And (ρ/(ρ−1))ⁿ = 1/((ρ−1)/ρ)ⁿ = 1/(1−1/ρ)ⁿ. Hmm wait, that's not the same.\n\n   Hold on. Let me recompute. k_n(ρ−1) = (1+1/(ρ−1))ⁿ−1 = (ρ/(ρ−1))ⁿ−1.\n\n   Residue of J at ρ = k_n(ρ−1)·Res(−ζ′/ζ at ρ) = [(ρ/(ρ−1))ⁿ−1]·(−mult) = mult·[1−(ρ/(ρ−1))ⁿ].\n\n   But D-064 says λ_n(T) = Σ_{|γ|<T} mult·[1−(1−1/ρ)ⁿ] is \"a finite reindexing of the reflected residues via ρ ↦ 1−ρ\". So under ρ ↦ 1−ρ: 1−(1−1/(1−ρ))ⁿ... let me check: 1 − 1/(1−ρ) = (1−ρ−1)/(1−ρ) = −ρ/(1−ρ) = ρ/(ρ−1). Yes! So 1−(ρ/(ρ−1))ⁿ = 1−(1−1/(1−ρ))ⁿ, and the reflected zero 1−ρ is also a zero with the same multiplicity (by the functional equation / conjugate symmetry). So the sum over zeros of mult·[1−(ρ/(ρ−1))ⁿ] equals the sum over zeros of mult·[1−(1−1/ρ)ⁿ] by reindexing ρ ↦ 1−ρ. That's the \"finite reindexing\" remark. OK.\n\n   So for the residue theorem itself, what we need is: residue of J at zero ρ = mult·[1−(ρ/(ρ−1))ⁿ]. And in STATE.md: \"simple poles at zeros with residue mult·(1−(ρ/(ρ−1))ⁿ) (via logDeriv NF computation; multiple zeros OK — logDeriv poles are always simple)\".\n\n3. At trivial zeros of ζ: −ζ′/ζ has simple poles at w = −2, −4, −6, … with residue −1 each (trivial zeros are simple). k_n(w−1) is analytic there. So J has a simple pole at w = −2k with residue 1−(−2k/(−2k−1))ⁿ = 1−(2k/(2k+1))ⁿ. For the rectangle σ ∈ [−5/2, 2√n], only −2 is inside (the next is −4 < −5/2). So triv(n) = 1−(2/3)ⁿ.\n\n   Wait, sign check: residue of −ζ′/ζ at a simple zero p is −1. k_n(p−1) = (p/(p−1))ⁿ−1. Product: −[(p/(p−1))ⁿ−1] = 1−(p/(p−1))ⁿ. At p = −2: 1−(−2/−3)ⁿ = 1−(2/3)ⁿ. ✓.\n\n4. Does J have any other poles? k_n(w−1) = (w/(w−1))ⁿ−1: pole only at w=1. −ζ′/ζ: poles at w=1 (simple, res +1), at nontrivial zeros (res −mult), at trivial zeros −2,−4,... (res −1 each... wait need to double check whether trivial zeros are simple in the Lean/Mathlib formalization — `riemannZeta` vanishes at −2,−4,..., these are simple zeros). Also, is −ζ′/ζ analytic elsewhere? ζ is analytic on ℂ∖{1}, so −ζ′/ζ is meromorphic on ℂ∖{1} with poles exactly at zeros of ζ (including trivial). So J = k_n(w−1)·(−ζ′/ζ) is meromorphic on ℂ with poles at {1} ∪ {zeros of ζ} = {1} ∪ {nontrivial zeros} ∪ {−2, −4, ...}.\n\n**The plan per STATE.md:**\n\nR := J − ppart n, shown holomorphic on Rectangle ∖ ({zeros} ∪ {−2}):\n- J − ppart n at w=1: ppart n is the principal part of J's Laurent expansion at 1, so R has a removable singularity at 1. The suggested formalization: (w−1)^{n+1}·R = (w−1)^{n+1}·J − (w−1)^{n+1}·ppart = F(w) − Σ_{i=1}^{n+1} A_i (w−1)^{n+1−i} = F(w) − Tayl_n F(w) where F(w) = (wⁿ−(w−1)ⁿ)·hLi(w)... \n\n  Hmm wait. Let me check: (w−1)^{n+1}·ppart n (w) = Σ_{i=1}^{n+1} A_i·(w−1)^{n+1−i} = Σ_{i} A_{n+1−i}... With A_i = F^{(n+1−i)}(1)/(n+1−i)!, setting j = n+1−i: Σ_{j=0}^{n} F^{(j)}(1)/j!·(w−1)^j = Taylor polynomial of F of order n at 1. And (w−1)^{n+1}J = F near 1 (punctured). So (w−1)^{n+1}R = F − Tayl_n F, which vanishes to order ≥ n+1 at 1 (all iterated derivs up to n vanish). Hence R = (F − Tayl_n F)/(w−1)^{n+1} has a removable singularity at 1 — analytic order of numerator ≥ n+1 means R extends analytically.\n\n  The suggested lemma: `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` — analyticOrderAt ≥ n+1 iff iteratedDeriv i = 0 for all i ≤ n... something like that.\n\n- Then apply `residueTheorem_finset` with S = (zeros in rectangle) ∪ {−2} and A(p) = residue. Note: residueTheorem_finset only handles simple poles (f − A p/(s−p) bounded near p). R is holomorphic at 1 (removable), so 1 is NOT in S — good, that's exactly why we subtract ppart first. At zeros ρ and at −2, R has simple poles with the same residues as J (ppart n is analytic at those points — ppart's only pole is at 1).\n\n  Wait, but ppart n is analytic at ρ and −2 (its pole is at 1 only). So R = J − ppart has at ρ: simple pole with residue = residue of J at ρ. ✓. And at −2 similarly. ✓.\n\n- The rectangle integral: RectangleIntegral' J = RectangleIntegral' (R + ppart) = RectangleIntegral' R + RectangleIntegral' ppart = [Σ zeros residues + triv] + ResW1 n.\n\n  Where RectangleIntegral' R = Σ_{p ∈ S} A(p) by residueTheorem_finset, and RectangleIntegral' (ppart n) = ResW1 n by rectInt'_ppart (session 016).\n\n  So sides(T) := RectangleIntegral' J z w = ResW1 n + Σ_{|γ|<T} mult·[1−(ρ/(ρ−1))ⁿ] + (1−(2/3)ⁿ).\n\n**What exactly should be proved in this sub-stage?**\n\nPer STATE.md NEXT ACTION:\n1. R := J − ppart n holomorphic on Rectangle ∖ ({zeros} ∪ {−2}) — meromorphic order at 1 ≥ 0 via Taylor-remainder.\n2. Simple poles at zeros with residue mult·(1−(ρ/(ρ−1))ⁿ) — via logDeriv NF computation.\n3. At −2: residue 1−(2/3)ⁿ.\n4. Apply vendored residueTheorem_finset.\n5. Assemble sides(T) = ResW1 n + Σ + triv.\n\nNow, an important design question: how do we encode \"the zeros in the rectangle\"? Options:\n(a) Take an arbitrary finite set S of zeros — prove R is holomorphic off {zeros of ζ} ∪ {1 is removable}... Actually the cleanest: prove J is holomorphic on ℂ ∖ ({1} ∪ ζ⁻¹{0}), R holomorphic on ℂ ∖ ζ⁻¹{0} (with 1 removable). Then for ANY rectangle and ANY finite S ⊂ zeros ∩ interior, residueTheorem_finset applies.\n\nActually, residueTheorem_finset needs:\n- hS : ∀ p ∈ S, Rectangle z w ∈ 𝓝 p (all interior)\n- fHolo : HolomorphicOn f (Rectangle z w \\ S)\n- near : ∀ p ∈ S, (f − A p/(s−p)) =O[𝓝[≠] p] 1\n\nFor fHolo with f = R: we need R holomorphic on Rectangle ∖ S. If S is exactly \"all zeros of ζ in the rectangle plus −2\", then on Rectangle ∖ S, ζ has no zeros (except... hmm, we need ζ ≠ 0 on Rectangle ∖ S — that requires S to capture ALL zeros in the rectangle). The cleanest is: S := (Rectangle ∩ ζ⁻¹'{0}).toFinset ∪ {−2}? But −2 IS a zero of ζ... so S := (Rectangle ∩ ζ⁻¹'{0}).toFinset might already include −2 if −2 ∈ Rectangle.\n\nHmm, but wait: is 1 ∈ Rectangle ∩ ζ⁻¹'{0}? No — ζ(1) is undefined/∞ (pole), not 0. Actually `riemannZeta 1` in Mathlib is defined by the analytic continuation; riemannZeta is defined as... In Mathlib, `riemannZeta` is an entire-function-style definition with the pole at 1; `riemannZeta 1` gives some junk value? Actually Mathlib defines riemannZeta via `completedRiemannZeta` division; at s = 1, completedRiemannZeta has a pole... Let me not worry; the point is 1 is a pole of ζ, ζ(1) in Mathlib is defined as... hmm, actually in Mathlib riemannZeta is defined as an entire function minus... I recall `riemannZeta` is defined via the completed zeta divided by the Gamma factor, and it IS defined at 1 as some value (it's totalized). But differentiability fails at 1.\n\nFor our purposes: J(w) = k_n(w−1)·(−ζ′/ζ(w)) involves deriv ζ / ζ. R = J − ppart.\n\nStrategy for fHolo: show R is differentiable on {w : w ≠ 1 ∧ riemannZeta w ≠ 0}... then Rectangle ∖ S ⊆ that set requires: every point of Rectangle ∖ S is ≠ 1 (needs 1 ∉ Rectangle ∖ S, i.e., either 1 ∉ Rectangle or 1 ∈ S) and ζ ≠ 0 there (needs all zeros in Rectangle to be in S).\n\nSimplest robust approach: S := zeros.toFinset ∪ {−2} where zeros := Rectangle ∩ {ρ : IsNontrivialZero ρ}? But nontrivial zeros in Lean are defined via the subtype in LiSkeleton ({ρ // IsNontrivialZero ρ}). Hmm. Actually maybe simpler: S := (Rectangle z w ∩ riemannZeta ⁻¹' {0}).toFinset — all zeros of ζ in the rectangle (this automatically includes −2 if present, and nontrivial zeros present; and 1 is not a zero of ζ in the Mathlib sense? Let me check: what is riemannZeta 1 in Mathlib? \n\nIn Mathlib, riemannZeta is defined as `completedRiemannZeta s * (s * (s - 1)) / ... ` hmm I don't remember exactly. There is `riemannZeta_def_of_ne_zero`... Actually: `riemannZeta s = completedRiemannZeta s * s * (s - 1) / (2 * π ^ (s/2) * Γ(s/2))`-ish. At s = 1: completedRiemannZeta has a simple pole with residue 1... no wait. Mathlib: `completedRiemannZeta` is entire except poles at 0 and 1. `riemannZeta s := completedRiemannZeta s / Gammaℝ s` where Gammaℝ s = π^{s/2} Γ(s/2)... something like that. At s=1, completedRiemannZeta has a pole, so the quotient riemannZeta has a pole — but as a function ℂ → ℂ it's totalized somehow. The value riemannZeta 1 is defined but the function is not continuous there. I believe Mathlib sets it up so riemannZeta is differentiable exactly on {1}ᶜ (differentiableAt_riemannZeta requires s ≠ 1). The VALUE at 1: `riemannZeta_one`... I recall riemannZeta 1 might be defined as γ (Euler–Mascheroni)? Hmm no. Let me not guess — I'll check in the code when needed.\n\nKey question for fHolo: is 1 ∈ (Rectangle ∩ riemannZeta ⁻¹' {0})? If riemannZeta 1 ≠ 0 in Mathlib's totalization, then 1 is not in the zero preimage, good — then S := zeros-toFinset covers all actual zeros, and R is holomorphic on Rectangle ∖ S provided (i) R holomorphic at 1 (removable — the main work), (ii) R holomorphic wherever ζ ≠ 0 and w ≠ 1.\n\nHmm wait, but actually if riemannZeta 1 = 0 in Mathlib's totalization (junk value), then 1 ∈ S which breaks the residue computation (R is holomorphic at 1, so the \"near\" condition at 1 would need A(1) = 0 — actually if R is holomorphic at 1, then R − 0/(s−1) is bounded near 1, so A(1) = 0 works! The residue at a removable point is 0). That's fine either way, but cleaner to exclude 1 explicitly.\n\nLet me check what Mathlib says about riemannZeta 1. I'll grep.\n\nActually, let me think about the overall structure of what to build in this session:\n\n**File: LiSides.lean (new file, per freeze protocol — new files are fine, no edits to existing proofs).**\n\nContents:\n1. `Jlag n w := ((w/(w−1))ⁿ − 1) * (−deriv ζ w / ζ w)` — the Lagarias-kernel integrand. \n\n   Hmm, wait — should J be defined with k_n(w−1) = (w/(w−1))ⁿ−1? Yes: k_n(s) = (1+1/s)ⁿ−1, so k_n(w−1) = (1+1/(w−1))ⁿ−1 = (w/(w−1))ⁿ−1.\n\n   Actually, hold on. Let me double check against LiResidue.lean's ResW1: \"the residue at w = 1 of J(w) = k_n(w−1)·(−ζ′/ζ(w)), packaged as (1/n!)·(d/dw)ⁿ[(wⁿ−(w−1)ⁿ)·hLi] at w = 1\". So (w−1)^{n+1}·J = [wⁿ−(w−1)ⁿ]·hLi punctured near 1. Check: (w−1)^{n+1}·[(w/(w−1))ⁿ−1]·(−ζ′/ζ) = (w−1)^{n+1}·[(wⁿ−(w−1)ⁿ)/(w−1)ⁿ]·(−ζ′/ζ) = (w−1)·(wⁿ−(w−1)ⁿ)·(−ζ′/ζ) = (wⁿ−(w−1)ⁿ)·[(w−1)(−ζ′/ζ)] = [wⁿ−(w−1)ⁿ]·hLi (punctured, where ζ ≠ 0). ✓\n\n2. `Rfun n := Jlag n − ppart n` (or as a lambda).\n\n3. Holomorphicity lemmas:\n   - `Jlag` holomorphic (DifferentiableOn) on {w ≠ 1 ∧ ζ w ≠ 0}: product of (w/(w−1))ⁿ−1 (holomorphic off {1}) and −ζ′/ζ (holomorphic off {1} ∪ zeros).\n   - ppart n holomorphic off {1}.\n   - So R holomorphic off {1} ∪ zeros.\n   - **The removable singularity at 1**: R extends analytically across 1. Per STATE.md: use `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero`. \n\n     The math: define F̃(w) := (wⁿ−(w−1)ⁿ)·hLi(w) (analytic at 1 — hLi analytic at 1 PROVED). On a punctured neighborhood of 1 (where additionally ζ(w) ≠ 0), (w−1)^{n+1}·R(w) = F̃(w) − Σ_{i=1}^{n+1} A_i (w−1)^{n+1−i}.\n\n     Note Σ_{i=1}^{n+1} A_i (w−1)^{n+1−i} = Σ_{j=0}^{n} A_{n+1−j} (w−1)^j where A_{n+1−j} = F̃^{(j)}(1)/j! (since Acoeff n i = iteratedDeriv (n+1−i) F 1 / (n+1−i)!, so Acoeff n (n+1−j) = iteratedDeriv j F 1 / j!). So the subtracted polynomial is exactly the n-th Taylor polynomial of F̃ at 1, i.e., F̃ − Tayl_n F̃ vanishes to order ≥ n+1 at 1.\n\n     In Lean: show `analyticOrderAt (fun w => F̃ w − Tayl) 1 ≥ n+1` via `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` (iff all iteratedDeriv j for j ≤ n vanish — true since F̃ − Tayl_n F̃ has the same derivs up to order n... wait, derivs of order ≤ n of F̃ − Tayl_n F̃ at 1 are zero by construction of the Taylor polynomial).\n\n     Then R(w) = (F̃ − Tayl)/(w−1)^{n+1} near 1 (punctured), and analyticOrderAt of numerator ≥ n+1 ⟹ R bounded near 1 ⟹ removable (differentiableOn_update trick as in zetaA).\n\n     Alternatively — and maybe simpler — directly show R is *bounded* near 1 on a punctured neighborhood, then use the same `differentiableOn_update_limUnder_of_bddAbove` machinery as zetaA. Boundedness: (F̃ − Tayl_n F̃)(w) = O((w−1)^{n+1}) — this is the Taylor-remainder bound. In Mathlib, for an analytic function, `AnalyticAt` gives a power series; the remainder after subtracting the n-th Taylor polynomial is O((w−1)^{n+1}). There should be a lemma like `AnalyticAt.exists_hasSum`... or use `iteratedDeriv` Taylor theorem. Hmm, actually the cleanest might be via analyticOrderAt: if g is analytic at 1 with analyticOrderAt g 1 ≥ n+1, then g(w)/(w−1)^{n+1} is analytic at 1 — there's a lemma about dividing out the order: `(hf.analyticOrderAt_ne_top.mp ...)`: f = (s−q)^ord • h with h analytic, h(q) ≠ 0. That's the `AnalyticAt.analyticOrderAt_ne_top` decomposition used in the vendored file (line 241: `obtain ⟨h, hh, hh0, hfh⟩ := (hf q hρRP).analyticOrderAt_ne_top.mp htop`).\n\n     So: g(w) := F̃(w) − Tayl_n(w), analytic at 1 (both pieces analytic: F̃ by hLi_analyticAt_one; Tayl is a polynomial). If g ≡ 0 near 1, then R = 0 near 1 punctured... trivial case. Otherwise analyticOrderAt g 1 = some finite m; g = (w−1)^m·h with h analytic, h(1) ≠ 0. Show m ≥ n+1 via the iteratedDeriv criterion. Then R(w) = (w−1)^{m−(n+1)}·h(w) near 1 punctured — analytic continuation across 1 explicit. This gives not just boundedness but an explicit analytic extension.\n\n     Hmm, but the case g ≡ 0: then R = 0 on the punctured neighborhood — fine, R extends by 0... Actually if g ≡ 0 near 1 then R(w) = 0/(w−1)^{n+1} = 0 on the punctured neighborhood, and R extends by R(1) := 0. Both cases: R is bounded near 1. Maybe simplest: prove `R =O[𝓝[≠] 1] 1` (bounded), then removable-singularity. \n\n     For boundedness: |g(w)| ≤ C|w−1|^{n+1} near 1. In Mathlib: `AnalyticAt` + order ≥ n+1... There's `AnalyticAt.isBigO...`? Hmm. Alternative: use the decomposition g = (w−1)^m h with m ≥ n+1, then g(w)/(w−1)^{n+1} = (w−1)^{m−n−1} h(w) → continuous. But the order-decomposition needs the ≠ top case.\n\n     Actually, you know what? There's an even more elementary route: **Taylor's theorem with iterated derivative integral remainder** might be overkill. Let me think about what Mathlib has for \"f analytic, first n derivs vanish ⟹ f(w) = O((w−1)ⁿ⁺¹)\".\n\n     Search candidates: `analyticOrderAt` lemmas: `natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero` — hmm, STATE.md explicitly names this lemma, so session-014's design presumably found it in Mathlib. Its likely statement: `(n : ℕ∞) ≤ analyticOrderAt f z ↔ ∀ i < n, iteratedDeriv i f z = 0` or `∀ i, i < n → ...`. Let me verify by grepping Mathlib.\n\n     Then with order m ≥ n+1: use `AnalyticAt.analyticOrderAt_eq_natCast` + the factorization... Actually there's a cleaner lemma: `AnalyticAt.exists_analyticAt...`? Or `MeromorphicAt` machinery: `MeromorphicAt.order...`? \n\n     Simplest robust plan: \n     g analytic at 1, order ≥ n+1 (in ℕ∞ sense, where ⊤ case = identically zero nearby — then the goal is trivial since g = 0 eventually, so R = 0 eventually on the punctured nhd, certainly bounded).\n     \n     For the ≠ ⊤ case: obtain h analytic with g = (w−1)^m • h, h(1) ≠ 0, m = order ≥ n+1. Then for w ≠ 1: R(w) = g(w)/(w−1)^{n+1} = (w−1)^{m−(n+1)}·h(w). As w → 1, this → 0·h(1) = 0 if m > n+1, or h(1) if m = n+1. Either way R is continuous-at-1 after extension by the right value; in particular bounded. \n\n     Then: define Rext := Function.update R 1 (limUnder ...), prove differentiableOn punctured + bounded ⟹ differentiableOn extension, as in zetaA_analyticAt_one. Actually — even better, we can avoid Function.update: we only need `HolomorphicOn R (Rectangle ∖ S)` where S is a Finset of zeros with 1 ∉ S... wait no, 1 might be in the rectangle's interior and R (as defined) is not differentiable AT 1 (it's not even defined nicely at 1 — well, it IS defined: Jlag at 1 involves division by ζ(1)... ζ(1) — hmm, what's deriv ζ / ζ at 1 in Mathlib? deriv riemannZeta 1 — since riemannZeta is not differentiable at 1, deriv gives the junk value 0? Mathlib's `deriv` is totalized: deriv f x = 0 if f is not differentiable at x. So Jlag 1 = ((1/0)ⁿ−1)·(0/ζ(1))... (1−1) = 0, so w/(w−1) at w=1 is 1/0 = 0 in field-with-zero-division convention! ℂ has `instInv` with 0⁻¹ = 0. So (1/0)ⁿ = 0, Jlag 1 = (0−1)·(0/ζ 1) = −0/... = 0. And ppart n 1 = Σ A_i/(1−1)^i = Σ A_i/0 = 0 (0^i = 0 for i ≥ 1, x/0 = 0). So R(1) = 0 by junk. Not analytic at 1 as a bare function (derivative at 1 doesn't exist in the usual sense since the function isn't even continuous at 1 from the punctured side... or IS it? If R(w) → L ≠ 0 as w → 1, w ≠ 1, but R(1) = 0, then R is discontinuous at 1 — not differentiable).\n\n     So for `HolomorphicOn R (Rectangle ∖ S)` to hold with 1 ∈ Rectangle, we MUST have 1 ∈ S (so that 1 is excluded from the domain), OR work with the extension Rext. But residueTheorem_finset's `near` hypothesis at 1 would then require (R − A(1)/(s−1)) bounded near 1 — with R bounded near 1 and A(1)/(s−1) unbounded unless A(1) = 0... with A(1) = 0: R − 0 = R bounded ✓. So including 1 in S with A(1) = 0 works for `near`, BUT fHolo needs HolomorphicOn R (Rectangle ∖ S) which excludes 1 — fine! And hS needs Rectangle ∈ 𝓝 1 — fine if 1 interior.\n\n     Hmm wait, but actually if 1 ∈ S, the sum Σ_{p∈S} A(p) includes A(1) = 0 — harmless.\n\n     But wait, there's a subtlety: `near` at OTHER points p ∈ S requires R − A(p)/(s−p) bounded near p. At zeros ρ: R = J − ppart; ppart is continuous at ρ (analytic away from 1); J − mult·[1−(ρ/(ρ−1))ⁿ]/(s−ρ) bounded — this is the simple-pole residue computation. OK.\n\n     Alternatively cleaner: use the EXTENSION Rext (defined everywhere, analytic at 1) and S = zeros only. But then Rext's values at 1 are the limUnder, and we need RectangleIntegral' of Rext = integral of R (they agree on the border since 1 ∉ border) — fine via RectangleIntegral'_congr.\n\n     Hmm, actually, let me reconsider. What does the FINAL assembly need? sides(T) := RectangleIntegral' (Jlag n) z w. We have:\n     - Jlag = R + ppart (everywhere, by definition of R as Jlag − ppart).\n     - RectangleIntegral' Jlag = RectangleIntegral' R + RectangleIntegral' ppart (linearity — needs both border-integrable).\n     - RectangleIntegral' ppart = ResW1 n (session 016, needs 1 interior).\n     - RectangleIntegral' R = Σ_{p∈S} A(p) (residueTheorem_finset).\n\n     For the last: S must include ALL zeros of ζ in the rectangle interior (else fHolo fails: at an interior zero not in S, R blows up). And border must avoid zeros AND 1 (border integrability needs continuity on the border; residueTheorem_finset internally handles integrability from holomorphicity — looking at the vendored proof: it builds integrability from hf₂holo.continuousOn — so no separate border-nonvanishing hypothesis needed for residueTheorem_finset; but hS requires all S interior, i.e., not on the border; and fHolo on Rectangle ∖ S — points of the border are in Rectangle ∖ S automatically if S is interior... wait Rectangle includes its border; S interior ⟹ border ⊆ Rectangle ∖ S ✓; zeros on the border would violate... they're excluded from S only if we choose S = interior zeros; a border zero ρ₀ would then be in Rectangle ∖ S where R is not holomorphic (blows up) — so we need the border to avoid all zeros. In the final application (ii′-4), T is chosen zero-avoiding. For THIS sub-stage, the theorem should take hypotheses: rectangle with 1 interior, no zeros on the border, and S := the finite set of zeros inside (produced via finite_zeros_rectangle or supplied).\n\n     Also −2: it's a zero of ζ (riemannZeta_neg_two_mul_nat_add_one or similar in Mathlib: ζ(−2n) = 0). So −2 ∈ zeros automatically if inside the rectangle. The residue at −2: mult is 1 (trivial zeros are simple — do we have that in Mathlib/Zeta23? `analyticOrderNatAt riemannZeta (−2) = 1`? Hmm — Zeta23 might have trivial-zero simplicity; or we can compute the residue directly: R − A/(s+2) bounded. The residue of −ζ′/ζ at −2 is −1 — needs simplicity of the trivial zero. Alternatively avoid needing simplicity: the residue formula mult·[1−(ρ/(ρ−1))ⁿ] with mult := analyticOrderNatAt ζ ρ covers ALL zeros uniformly — at −2 it gives analyticOrderNatAt ζ (−2)·[1−(2/3)ⁿ]. Then the \"triv(n) = 1−(2/3)ⁿ\" simplification needs order = 1 at −2. \n\n     Mathlib: is there a lemma that trivial zeros are simple? I recall `riemannZeta` vanishing at negative even integers via `riemannZeta_neg_two_mul_nat_add_one`... and simplicity? There might be something in Mathlib about ζ(−2n) = 0 and deriv ζ (−2n) ≠ 0? Not sure. Zeta23 may have it. This can be deferred: for THIS sub-stage, state the residue at each zero ρ as `analyticOrderNatAt ζ ρ · [1−(ρ/(ρ−1))ⁿ]` uniformly. The specialization triv = 1−(2/3)ⁿ (order-1 at −2) can be a small separate lemma if the order-1 fact is available; otherwise leave the order in (the downstream assembly ii′-6 needs the value 1−(2/3)ⁿ — we can discharge `analyticOrderNatAt riemannZeta (-2) = 1` when we get there; STATE.md explicitly says \"at −2 (residue 1−(2/3)ⁿ)\" so the design expects the simplicity fact — let me look for it during implementation).\n\n**Let me now also check**: what does `liSummand`/liCoeff look like now in LiSkeleton (session 015's fix), since sides assembly relates to λ_n(T)? For THIS sub-stage, the zero-sum Σ_{|γ|<T} is over a Finset of zeros in the rectangle — I should define it matching whatever ii′-6 will need. Let me keep it generic: the theorem concludes\n\n  RectangleIntegral' (Jlag n) z w = ResW1 n + Σ ρ ∈ S, (mult ρ : ℂ)·(1 − (ρ/(ρ−1))ⁿ)\n\nwhere S = zeros of ζ in the rectangle (as a Finset via finite_zeros_rectangle or supplied with an iff characterization), EXCLUDING... hmm wait: does S include 1? 1 is not a zero of ζ (ζ has a pole at 1). Need: riemannZeta 1 ≠ 0 in Mathlib. Let me check what riemannZeta 1 is. I believe in Mathlib, `riemannZeta` is defined as an entire function... no wait. Let me grep Mathlib for `riemannZeta` definition and value at 1.\n\nAlso need: IsNontrivialZero characterization to connect to zeroMult/zero subtype later (ii′-6). For now, generic.\n\n**Plan for the proof of the residue at a zero ρ (the \"near\" condition):**\n\nGoal: (R − fun s => A ρ/(s−ρ)) =O[𝓝[≠] ρ] 1, where A ρ = (analyticOrderNatAt ζ ρ : ℂ)·(1−(ρ/(ρ−1))ⁿ)... \n\nwait sign: residue of −ζ′/ζ at ρ is −(order of zero) = −m. Residue of J = k_n(ρ−1)·(−m) = [(ρ/(ρ−1))ⁿ−1]·(−m) = m·[1−(ρ/(ρ−1))ⁿ]. Yes, A ρ = m·(1−(ρ/(ρ−1))ⁿ) with m = analyticOrderNatAt riemannZeta ρ. ✓ (matches STATE.md).\n\nProof: R − A/(s−ρ) = J − ppart − A/(s−ρ). ppart is continuous at ρ (analytic, since ρ ≠ 1). So suffices: J − A/(s−ρ) bounded near ρ.\n\nJ(s) − A/(s−ρ) = k_n(s−1)·(−ζ′/ζ(s)) − m·k_n(ρ−1)/(s−ρ)\n= k_n(s−1)·[−ζ′/ζ(s) + m/(s−ρ)]... hmm, cleaner:\n= k_n(s−1)·[−logDeriv ζ s − (−m)/(s−ρ)] + [k_n(s−1) − k_n(ρ−1)]·(−m)/(s−ρ)? \n\nLet me do it properly:\nJ(s) − A/(s−ρ) = k(s)·L(s) − m·k(ρ)/(s−ρ), where k(s) := k_n(s−1) = (s/(s−1))ⁿ−1, L(s) := −logDeriv ζ s.\n\nWrite k(s)L(s) − m k(ρ)/(s−ρ) = k(s)·[L(s) + m/(s−ρ)] − m·[k(s) − k(ρ)]/(s−ρ).\n\nTerm 2: [k(s)−k(ρ)]/(s−ρ) → k′(ρ) (slope; k analytic at ρ since ρ ≠ 1). Bounded ✓.\n\nTerm 1: L(s) + m/(s−ρ) = −[ζ′/ζ(s) − m/(s−ρ)]. Since ζ has a zero of order m at ρ: ζ = (s−ρ)^m·h, h analytic, h(ρ) ≠ 0. Then logDeriv ζ = m/(s−ρ) + h′/h. So L(s) + m/(s−ρ) = −h′/h(s) → −h′(ρ)/h(ρ). Bounded ✓. Then k(s) continuous at ρ. So Term 1 bounded. ✓\n\nIn Lean, the factorization (hf.analyticOrderAt_ne_top) gives h. Then assemble with Tendsto/IsBigO as in the vendored rectangleIntegral'_mul_logDeriv_of_poles (lines 227–280 have EXACTLY this pattern for g·logDeriv f − A/(s−q)!). In fact the vendored code at line 246–279 does: (analyticOrderNatAt f q : ℂ)·((g s − g q)/(s−q)) + g s·logDeriv h s = (g·logDeriv f − A q/(s−q)) s — with A q = ord·g(q). Our case: g := −k (i.e., the weight), f := ζ, A := ord·(−k(ρ))·(−1)... let me just mirror that proof.\n\nActually WAIT. Even better: can we reuse the vendored `rectangleIntegral'_mul_logDeriv` DIRECTLY on J = k·(−ζ′/ζ) = (−k)·logDeriv ζ? The vendored theorem: RectangleIntegral' (g·logDeriv f) = Σ ord·g(ρ) for f, g analytic on the rectangle, f ≠ 0 on border. Take f = riemannZeta — NOT analytic on the rectangle (pole at 1, and not analytic at 1). So no, can't use it directly — the pole at 1 with order n+1 from k is exactly what forces the ppart subtraction. Also g = −k_n(s−1) has a pole at 1 too. So the ppart-subtraction route is necessary. Right.\n\n**And the \"near\" at zeros uses the logDeriv NF computation** (per STATE.md \"via logDeriv NF computation; multiple zeros OK — logDeriv poles are always simple\") — exactly the vendored pattern above. Good.\n\n**The −2 residue**: same formula with ρ = −2, m = analyticOrderNatAt ζ (−2). If we can prove m = 1, then A(−2) = 1·(1−(−2/−3)ⁿ) = 1−(2/3)ⁿ. Let me check Mathlib for trivial-zero simplicity... Zeta23 might have it. I'll search during implementation. If unavailable, leave as order·(1−(2/3)ⁿ) and note for ii′-4/6. Actually — hmm, D-064's assembly wants triv(n) = 1−(2/3)ⁿ exactly. The simplicity of trivial zeros: Mathlib has `riemannZeta_neg_two_mul_nat_add_one : riemannZeta (-2 * (n+1)) = 0`? and deriv nonzero? I recall a recent Mathlib addition `deriv_riemannZeta_neg_two_mul_nat_add_one_ne_zero` or via the functional equation: ζ(−2k) relates to ζ(2k+1) ≠ 0 times nonzero factors... The functional equation route: completedRiemannZeta has poles only at 0,1; ζ(s) = Λ(s)/Gammaℝ(s)... the zero of ζ at −2k comes from the pole of Γ(s/2) at −k... Simplicity = the Γ pole is simple + Λ(−2k) ≠ 0 (Λ(s) = Λ(1−s), Λ(1+2k) = finite nonzero since ζ(2k+1) ≠ 0... hmm Λ at 2k+1: completedRiemannZeta (2k+1) = π^{−(2k+1)/2}Γ((2k+1)/2)ζ(2k+1) ≠ 0 ✓). This might not be in Mathlib. Defer — keep m symbolic; the ii′-6 assembly can discharge it (or a mini-lemma later). Actually, let me search Zeta23/Mathlib quickly during implementation; if not found in ~10 min, proceed symbolic.\n\nHmm wait, actually for the ASSEMBLY in this sub-stage per STATE.md: \"assemble sides(T) = ResW1 n + Σ_{|γ|<T} mult·[1−(ρ/(ρ−1))ⁿ] + triv(n)\". So the final theorem should have the zero sum over nontrivial zeros and the triv separate. That requires splitting S into nontrivial zeros ∩ rectangle and {−2} (and asserting −4, −6, ... are outside the rectangle — the rectangle in question has Re ≥ −5/2; but our theorem should be generic: maybe hypothesis that the only trivial zero inside is −2? For genericity, I could state the main theorem with S = ALL zeros (including trivial), sum over all of them — and then a corollary for the specific rectangle shape. Let me think about what ii′-6 needs:\n\nD-064: rectangle σ ∈ [−5/2, 2√n], |Im| ≤ T, T zero-avoiding in [√n, √n+1]. Inside: 1 (pole), −2 (trivial zero), nontrivial zeros with |γ| < T (and Re ∈ (0,1) ⊆ [−5/2, 2√n] ✓ all nontrivial zeros with |Im| < T are inside — need Re ∈ (0,1) which is the zero-free... no wait, nontrivial zeros have Re ∈ [0,1] — actually IsNontrivialZero in Zeta23: 0 ≤ Re ≤ 1, Im ≠ 0, ζ = 0 — need to check the exact def; anyway all nontrivial zeros with |γ| < T are in the rectangle since Re(ρ) ∈ [0,1] ⊆ (−5/2, 2√n) for n ≥ ... 2√n ≥ 1 iff n ≥ 1/4 ✓).\n\nSo ii′-6 needs: sides = ResW1 + Σ_{nontrivial, |γ|<T} mult·[1−(ρ/(ρ−1))ⁿ] + (1−(2/3)ⁿ).\n\nPlan: \n- **Main theorem (generic)**: for a rectangle with 1 interior, ζ ≠ 0 on border, S := (Rectangle ∩ ζ⁻¹'{0}) finite set: RectangleIntegral' (Jlag n) = ResW1 n + Σ_{ρ∈S} (analyticOrderNatAt ζ ρ : ℂ)·(1−(ρ/(ρ−1))ⁿ).\n- Wait — but hold on: are there zeros of ζ with Re(ρ) = ρ.re where the formula 1−(ρ/(ρ−1))ⁿ needs ρ ≠ 1? All zeros ρ ≠ 1 ✓ (ζ(1) is a pole). Fine.\n- **Corollary (D-064 rectangle)**: with the specific rectangle, S = nontrivial zeros inside ∪ {−2}, and if analyticOrderNatAt ζ (−2) = 1 available, split the sum.\n\nHmm, actually, is riemannZeta 1 = 0 a worry for S := Rectangle ∩ ζ⁻¹'{0}? If Mathlib totalizes riemannZeta 1 := 0 (junk), then 1 ∈ S and the sum gets a spurious term analyticOrderNatAt ζ 1 ·(1−(1/0)ⁿ)... 1/(1−1) = 1/0 = 0, 0ⁿ = 0 (n ≥ 1), so the term would be order·(1−0) = order at 1 = junk. DANGER. So I MUST check: what is riemannZeta 1 in Mathlib? \n\nI recall: Mathlib's riemannZeta is defined via `riemannZeta s = completedRiemannZeta s / Gammaℝ s`? Hmm, no — actually I think it's defined as the analytic continuation via the Dirichlet eta or via the completed function divided by the gamma factor. At s = 1, completedRiemannZeta has a simple pole (residue 1), Gammaℝ 1 = π^{1/2}Γ(1/2) = π ≠ 0, so the quotient has a pole at 1 — as a ℂ-valued function it's totalized; the pole means the function is Λ/Γ with Λ(1) = ∞ — no wait, these are all ℂ → ℂ total functions; the \"pole\" is in the sense of limits. The VALUE: completedRiemannZeta 1 = limUnder? No — completedRiemannZeta is DEFINED as an entire-ish function via the Mellin transform formula valid for Re s > 1, then... Mathlib defines `completedRiemannZeta` via `Function.update` at 0 and 1? I genuinely don't remember. There IS a lemma `riemannZeta_one`? Hmm. I think I recall `riemannZeta 1 = γ`?? No, that's not right either... Actually! I do recall: in Mathlib, since riemannZeta is defined as `completedRiemannZeta s / Gammaℝ s` and completedRiemannZeta at 1 is totalized to its... hmm.\n\nLet me just grep during implementation. Simple defensive approach regardless: define S := (Rectangle z w ∩ riemannZeta ⁻¹' {0}) \\ {1} as a Set.Finite toFinset, or add hypothesis 1 ∉ zero preimage... cleanest: prove `riemannZeta 1 ≠ 0`? If Mathlib has riemannZeta 1 = some explicit nonzero value — hmm, actually now I really do recall: Mathlib defines riemannZeta via the Hurwitz zeta or via `completedRiemannZeta`, and there's a simp lemma `riemannZeta_one : riemannZeta 1 = ...`? I'll check.\n\nHmm, hold on — I realize I should check how Zeta23's IsNontrivialZero is defined and whether there's an existing \"zeros in rectangle\" finset for ζ in Zeta23 (the RvM proof counts zeros in rectangles!). `riemannVonMangoldt` counts nontrivial zeros in a rectangle — there's likely existing machinery: the zero-counting uses rectangleIntegral'_mul_logDeriv on completedRiemannZeta or Λ. The zeros of completedRiemannZeta ARE the nontrivial zeros (completed has no trivial zeros — they're cancelled by Γ poles). Zeta23's WeilEF.zero_sum_inv_sq is over the subtype {ρ // IsNontrivialZero ρ}. Let me look at Zeta23.Statement to see IsNontrivialZero and zeroMult.\n\nAlso LiSkeleton.lean (session 015) has the paired liSummand machinery with the subtype — I should read the current LiSkeleton to match conventions.\n\nOK — enough design in the head. Let me now:\n1. Read LiSkeleton.lean (current state, conventions for zeros subtype, zeroMult).\n2. Grep Mathlib for riemannZeta at 1 (value, differentiability), trivial zero simplicity.\n3. Grep Zeta23 for IsNontrivialZero, zero_sum_inv_sq, EF_lit_zeta context.\n\nThen write LiSides.lean.\n\nLet me also set up the task list since this is a multi-step sub-stage.","signature":""},{"type":"text","text":"Context loaded. Now let me look at the current LiSkeleton (session 015 conventions) and check key Mathlib/Zeta23 facts I'll need."},{"type":"tool_use","id":"TodoWrite_11","name":"TodoWrite","input":{"todos":[{"content":"Inventory: LiSkeleton conventions, Mathlib riemannZeta@1, zero finiteness machinery","status":"in_progress","activeForm":"Inventorying LiSkeleton conventions and Mathlib facts"},{"content":"Build LiSides.lean: Jlag def + holomorphicity off {1}∪zeros","status":"pending","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":"Grep_12","name":"Grep","input":{"pattern":"IsNontrivialZero|zeroMult|def liCoeff|liSummand","path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","output_mode":"content","-n":true,"head_limit":40},"extra_content":null}]