[{"type":"thinking","thinking":"The user says \"Let's go\" — start session 016: ii′-1b (R1 residue machinery). Let me plan this sub-stage carefully.\n\nPer D-064 R1:\n1. **General finite-order residue** (`gresidue`): for a meromorphic f at p with order −m (m ≥ 1), residue = the coefficient of (z−p)^{-1} in the Laurent expansion = the (m−1)-th Taylor coefficient of the NF analytic part divided by (m−1)!.\n2. **Rectangle residue theorem extension**: beyond HasSimplePolesOn — principal-part decomposition; j ≥ 2 terms vanish by global primitive; j = 1 via the vendored simple-pole theorem.\n3. **Residue computations**: zeros via vendored `logDerivResidue`, w=1 by the Leibniz identity.\n\nLet me think about the cleanest path.\n\n### Design of gresidue\n\nGiven `MeromorphicAt f p` with `meromorphicOrderAt f p = -(m : ℤ)` (m : ℕ, m ≥ 1), by `meromorphicOrderAt_eq_int_iff` (exists in Mathlib, confirmed by agent):\n```\nmeromorphicOrderAt f p = (n : ℤ) ↔ ∃ g, AnalyticAt 𝕜 g p ∧ g p ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] p, f z = (z - p) ^ n • g z\n```\nSo f = (z−p)^{-m} · g near p with g analytic, g(p) ≠ 0. The residue (coefficient of (z−p)^{-1}) = the (m−1)-th Taylor coefficient of g at p = `g.iteratedDeriv (m-1) p / (m-1)!`... Actually for analytic g: g(z) = Σ a_k (z−p)^k with a_k = iteratedDeriv k g p / k!. The residue is a_{m-1} = iteratedDeriv (m−1) g p / (m−1)!.\n\nBut rather than defining gresidue via a choice of g, better to define it DIRECTLY:\n`gresidue f p := lim_{z→p} d^{m-1}/dz^{m-1} [(z−p)^m f z] / (m−1)!` — the standard higher-order residue formula. In Lean: \n```\nnoncomputable def gresidue (f : ℂ → ℂ) (p : ℂ) (m : ℕ) : ℂ :=\n  iteratedDeriv (m - 1) (fun z => (z - p) ^ m * f z) p / (m - 1)!\n```\nHmm — but (z−p)^m f z has a removable singularity when f has a pole of order ≤ m. The iterated derivative AT p requires the function to be defined (and sufficiently smooth) at p. The function h(z) = (z−p)^m f(z) is defined only off p (f undefined/unbounded at p)... in Lean, f p is some value (f is total). Actually in our application, f is a total function ℂ → ℂ (e.g., k_n(w−1)·(−ζ′/ζ) — defined everywhere except where ζ′/ζ blows up; at poles it's whatever the definitional unfolding gives — riemannZeta is total). The cleanest: define gresidue relative to the meromorphic order: \n\nAlternative cleaner definition (limit-free, derivative-free): use the meromorphic normal form directly. Mathlib has `MeromorphicAt` and `MeromorphicNFAt` with `toMeromorphicNFAt f p : ℂ → ℂ` which equals (z−p)^n • g with g analytic nonvanishing. The residue of order −1 coefficient: for the NF, residue = iteratedDeriv (m−1) g p / (m−1)! where g = (z−p)^m • toMeromorphicNFAt f p ... hmm.\n\nActually — maybe simplest for OUR purposes: we don't need a fully general residue theory. We need:\n(a) Rectangle residue theorem for our SPECIFIC integrand J(w) = k_n(w−1)(−ζ′/ζ(w)) with poles at: zeros (simple), w=1 (order n+1), trivial zero −2 (simple).\n(b) The residue VALUES at those points.\n\nPragmatic approach: prove a **\"rectangle with one higher-order pole plus simple poles\"** theorem directly:\n- Split J as J = J_simple_part + J_principal where J_principal = the principal part at w=1: Σ_{j=1}^{n} C(n,j) · c-stuff/(w−1)^{j+1}?? — hmm, the principal part at w=1 of J: J = k_n(w−1)·(−ζ′/ζ) = [Σ_{j=1}^n C(n,j)(w−1)^{-j}]·[u^{-1} + c_0 + c_1 u + ...] — the principal part is Σ over j of C(n,j)(w−1)^{-j}·(negative powers part)... The full principal part at w=1: Σ_{i=1}^{n+1} A_i (w−1)^{-i} with A_i = Σ_{j ≥ i−1} C(n,j) c_{j−i+...} — explicit but messy.\n\nCleaner decomposition: J(w) = [k_n(w−1)·(−ζ′/ζ(w)) − Σ_{j=1}^n C(n,j) c_{j−1}/(w−1)] − hmm no.\n\nStandard trick: J(w) = P(w) + R(w) where P(w) = Σ_{i=1}^{n+1} A_i (w−1)^{-i} is the principal part at w=1 (a finite RATIONAL function with pole only at w=1), and R(w) = J(w) − P(w) is holomorphic at w=1 (removable) with only SIMPLE poles elsewhere (the zeros + trivial zeros). Then:\n- ∮ J = ∮ P + ∮ R.\n- ∮ P = 2πi·A_1 = 2πi·Res₁(n) (each term A_i/(w−1)^i for i ≥ 2 integrates to 0 on the rectangle — has the global primitive −A_i/((i−1)(w−1)^{i−1}), single-valued meromorphic, so the rectangle integral vanishes by the boundary-telescoping/FTC; A_1/(w−1) gives 2πi A_1 by the vendored `ResidueTheoremInRectangle`).\n- ∮ R = 2πi·Σ residues at simple poles (zeros + trivial zero) via the vendored simple-pole rectangle theorem (R has only simple poles inside!).\n\nThe residue A_1 of J at w=1 = Res₁(n) = Σ_j C(n,j)c_{j−1} — computed by the Leibniz rule from h(w) = (w−1)(−ζ′/ζ(w)) analytic at 1 (h(1) = 1): (w−1)^{n+1}J(w) = [wⁿ − (w−1)ⁿ]h(w), and A_1 = (1/n!)(d/dw)^n[(w−1)^{n+1}J]_{w=1} = Σ_j C(n,j) h^{(j)}(1)/j! − 1... wait I did this computation in session 014: Res = (1/n!)(d/dw)ⁿ{[wⁿ−(w−1)ⁿ]h(w)}|₁ = Σ_{j=0}^n C(n,j)c_{j−1}·... = Σ_{j=1}^n C(n,j)c_{j−1} (the j=0 term cancels with the −1 from the (w−1)ⁿ part). Verified algebraically.\n\nSo the residue computation at w=1 needs: h analytic at 1 with h(1) = 1, h^{(j)}(1)/j! = c_{j−1} (the Laurent coefficients of −ζ′/ζ), and the Leibniz formula (iteratedDeriv of a product — `iteratedDeriv_mul`? — Mathlib has `iteratedDeriv_mul` for... there's `iteratedDeriv_mul` for ℂ-valued functions? There should be (iteratedDeriv within a field/algebra). Or use `iteratedDeriv_eq_iff` / `HasFPowerSeriesAt` machinery: h analytic at 1 ⟹ h has a power series; multiplication by polynomials and coefficient extraction via `HasFPowerSeriesAt` operations — the coefficients API: `HasFPowerSeriesAt.coeff`? There's `HasFPowerSeriesAt.eq_iteratedDeriv`? or `HasFPowerSeriesAt.iteratedDeriv`... The power-series route: (wⁿ−(w−1)ⁿ)h(w) = [Σ_k h_k (w−1)^k]·[wⁿ−(w−1)ⁿ], and its n-th derivative at 1: via Leibniz on the two factors: (wⁿ−(w−1)ⁿ) vanishes to order 1 at w=1 with first derivative n... Let me redo: F(w) = [wⁿ − (w−1)ⁿ]·h(w). F^{(n)}(1) = Σ_{j=0}^n C(n,j) [wⁿ−(w−1)ⁿ]^{(j)}(1) · h^{(n−j)}(1). [wⁿ−(w−1)ⁿ]^{(j)} at 1: for j = 0: 1−0 = 1. For j ≥ 1: (n!)_j·w^{n−j}|₁ − (n!)_j·(w−1)^{n−j}|₁ = (n!)_j − (n!)_j·(0 or n!·1 if j=n) = (n!)_j for j < n; for j = n: n! − n! = 0. So F^{(n)}(1) = Σ_{j=0}^{n−1} C(n,j)·(n!)_j·h^{(n−j)}(1) + 0 = Σ_{j=0}^{n−1} n!/(n−j)!·C(n,j)·h^{(n−j)}(1). Then Res = F^{(n)}(1)/n! = Σ_{j=0}^{n−1} C(n,j)·h^{(n−j)}(1)/(n−j)!. With i = n−j: Σ_{i=1}^{n} C(n,i)·h^{(i)}(1)/i! = Σ_{i=1}^n C(n,i)·c_{i−1} ✓ (h^{(i)}(1)/i! = c_{i−1} since h(w) = 1 + Σ_{k≥1} c_{k−1}(w−1)^k).\n\nHmm wait — this differs from my session-014 computation by a term: earlier I got Res = Σ_{j=1}^n C(n,j)c_{j−1} with the j=0 term = 1 canceling a −1 from the (w−1)ⁿ part. Here the j=0 term is C(n,0)·h^{(n)}(1)/n! = h^{(n)}(1)/n! = c_{n−1}, included in Σ_{i=1}^n with i = n: C(n,n)·c_{n−1} ✓ same thing — the (w−1)ⁿ part contributed 0 (its n-th derivative at 1 is n! — wait: (w−1)ⁿ's n-th derivative is n! constant, so [wⁿ−(w−1)ⁿ]^{(n)}|₁ = n! − n! = 0 ✓ but the LEIBNIZ sum is over j = derivative order on the first factor; j = n gives 0 — but the FULL n-th derivative of the product is F^{(n)} = Σ_j C(n,j) A^{(j)} h^{(n−j)} with A = wⁿ−(w−1)ⁿ — A(1) = 1, A^{(j)}(1) = (n!)_j for 1 ≤ j ≤ n−1, A^{(n)}(1) = 0. So F^{(n)}(1) = A(1)h^{(n)}(1) + Σ_{j=1}^{n−1} C(n,j)(n!)_j h^{(n−j)}(1) + 0 = h^{(n)}(1) + Σ_{j=1}^{n−1} ... = Σ_{j=0}^{n−1} C(n,j)(n!)_j h^{(n−j)}(1) (j=0 term: h^{(n)}(1) ✓ included). Dividing by n!: Σ_{j=0}^{n−1} C(n,j) h^{(n−j)}(1)/(n−j)! = Σ_{i=1}^n C(n,i) h^{(i)}(1)/i! = Σ_{i=1}^n C(n,i) c_{i−1} ✓✓ consistent with session 014's result (where the \"−1\" canceled the j=0's c_{−1} = 1... in session 014 I wrote Res = Σ_{i=0}^n C(n,i)c_{i−1} − 1 = Σ_{i=1}^n C(n,i)c_{i−1} + (c_{−1} − 1) = Σ_{i=1}^n C(n,i)c_{i−1} since c_{−1} = 1 ✓ SAME).\n\nSo the w=1 residue = Res₁(n) = Σ_{i=1}^n C(n,i)·c_{i−1} — and its Lean proof needs:\n- h(w) := (w−1)·(−ζ′/ζ(w)) — analytic at 1, h(1) = 1. From Mathlib `riemannZeta_residue_one` (Tendsto (s−1)·ζ(s) → 1) — for −ζ′/ζ: the vendored `riemannZetaLogDerivResidue` (−ζ′/ζ − 1/(s−1) bounded near 1) or `logDerivResidue` — h(w) = (w−1)(−ζ′/ζ) → 1 ✓, and analyticity at 1 of h: −ζ′/ζ = 1/(w−1) + analytic (the pole is simple with residue 1 — provable from riemannZetaResidue/logDerivResidue + MeromorphicAt API: h = (w−1)·(−ζ′/ζ) has order ≥ 0 at 1 and value 1).\n- The iterated derivative identity: F(w) = [wⁿ − (w−1)ⁿ]·h(w), F^{(n)}(1) = Σ_j C(n,j) A^{(j)}(1) h^{(n−j)}(1) — Leibniz for iteratedDeriv: `iteratedDeriv_mul`?? For scalar-valued ℂ functions — hmm, `iteratedDeriv_mul (hf : ContDiffAt ℂ n f x) (hg : ContDiffAt ℂ n g x) : iteratedDeriv n (f * g) x = Σ i ∈ antidiagonal n, (n.choose i) • (iteratedDeriv i f x * iteratedDeriv (n−i) g x)`? — there IS `iteratedDeriv_mul`? I'm not 100% sure of the name; there's `iteratedDeriv_smul`, and for products: `iteratedDeriv_mul` exists I believe (for functions into a normed algebra). ℂ is a normed algebra over ℂ? — iteratedDeriv is for functions 𝕜 → F; product in F = ℂ (algebra over itself) ✓ should exist.\n- c_{j−1} identification: h^{(i)}(1)/i! = c_{i−1} — where c_k are DEFINED as the Laurent coefficients of −ζ′/ζ at 1. Best: DEFINE c_k := iteratedDeriv (k+1) h 1 / (k+1)! — then h^{(i)}(1)/i! = c_{i−1} by definition. And separately prove −ζ′/ζ(1+u) = 1/u + Σ c_k u^k (as a power series near 0) when needed. For the residue computation, the definition via h is cleaner and avoids the Laurent-series formalization entirely!\n\nSo define: `lcoeff (k : ℕ) : ℂ := (iteratedDeriv (k + 1) (fun w => (w - 1) * (-deriv riemannZeta w / riemannZeta w)) 1) / (k + 1)!`? Hmm wait — but the RESIDUE at the w=1 needs the value (1/n!)F^{(n)}(1) where F = (wⁿ−(w−1)ⁿ)h. And the residue theorem needs A_1 = that value. Let me define:\n`ResW1 (n : ℕ) : ℂ := (iteratedDeriv n (fun w => (w^n - (w-1)^n) * h w) 1) / n!`\nand prove `ResW1 n = Σ_{i=1}^n C(n,i)·lcoeff(i−1)` via Leibniz.\n\nHmm, but actually — for the RECTANGLE theorem with the principal-part split, I need:\n- J = P + R with P(w) = Σ_{i=1}^{n+1} A_i (w−1)^{-i}: the A_i are the full principal part coefficients — for the residue theorem I need A_1 = ResW1 n. Rather than computing the FULL principal part, use a slicker split: \n  J(w) = [ResW1 n / (w−1)] + R₂(w), where R₂ = J − ResW1/(w−1) — is R₂ holomorphic at 1? No! J has a pole of order n+1; subtracting only the (w−1)^{-1} term leaves a pole of order n at 1. Doesn't work. So the principal part must be subtracted in full:\n  P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i with A_i = (1/(n+1−i)!)·(d/dw)^{n+1−i}[(w−1)^{n+1}J(w)]|₁... The i-th principal coefficient. Then R = J − P is holomorphic at 1 (all negative powers removed), and R has only simple poles (at zeros/trivial zeros) inside the rectangle. ∮ P = 2πi A_1 by the primitive argument.\n\n  The A_i's explicit form: with F := (w−1)^{n+1}J = [wⁿ−(w−1)ⁿ]h analytic: A_i = F^{(n+1−i)}(1)/(n+1−i)!. And A_1 = F^{(n)}(1)/n! = ResW1 ✓ consistent.\n\n  So P(w) = Σ_{i=1}^{n+1} [F^{(n+1−i)}(1)/(n+1−i)!]·(w−1)^{−i}.\n\n  For the residue theorem: ∮ P = 2πi·A_1: P = A_1/(w−1) + Σ_{i=2}^{n+1} A_i (w−1)^{−i}; the second sum has the global primitive G(w) = −Σ_{i=2}^{n+1} A_i/((i−1)(w−1)^{i−1}) — meromorphic, G' = the sum — so its rectangle integral is 0 (FTC/telescoping around the boundary — in Lean: `HolomorphicOn.vanishesOnRectangle` exists in the vendored Rectangle.lean? The agent reported `HolomorphicOn.vanishesOnRectangle [CompleteSpace E]` — a holomorphic function with a primitive? Let me check what that theorem says: \"theorem HolomorphicOn.vanishesOnRectangle\" — probably: if f is holomorphic on the rectangle then its rectangle integral is 0?? That can't be true without more hypotheses (1/(z−p) is holomorphic off p...). It's likely \"if f has a primitive on the rectangle\" — need to read it. Alternatively: the rectangle integral of G' = 0 because the boundary is a closed loop and G is single-valued — the standard proof: each side integral telescopes (FTC on segments: ∫_segment G' = G(endpoint) − G(startpoint), summing around = 0). In Lean: HIntegral/VIntegral of a derivative — the vendored file may have such lemmas. This is a known bounded computation.\n\n  Alternatively, avoid the primitive argument: ∮ P directly by the \"pull to small square\" lemma: `RectanglePullToNhdOfPole''` (vendored!): RectangleIntegral' f z w = RectangleIntegral' f (small square around p) eventually. Then on the small square, compute ∮ P: A_1/(w−1) via `ResidueTheoremInRectangle` (vendored: RectangleIntegral' (fun s => c/(s−p)) z w = c ✓), and the i ≥ 2 terms integrate to 0 on the small square (primitive exists on the square minus... on the small square, G is meromorphic with pole at center; G' on the boundary: the boundary integral of G' around the square = 0 by FTC on each side — same primitive argument but localized to a square of any size, so the boundary avoids the pole (pull-to-square keeps the boundary off p since the square is a neighborhood of p — wait, p is INSIDE the square; the boundary doesn't touch p ✓). FTC on each side segment: ∫_{segment} G'(s)ds = G(end) − G(start) — Mathlib has `intervalIntegral.integral_deriv` or for line segments in ℂ... the vendored Rectangle.lean has HIntegral/VIntegral as interval integrals; FTC: `intervalIntegral.integral_deriv_eq_sub` for real intervals with G differentiable — should work for the parametrized sides (HIntegral f x₁ x₂ y = ∫_x f(x+iy) dx — with f = G', the integral = G(x₂+iy) − G(x₁+iy) by FTC if G is differentiable on the segment ✓ pole-free there). This is mechanical but fiddly. Bounded.\n\nSo the rectangle theorem I actually need:\n\n**THEOREM (RectResidue-J)**: For the specific integrand J(w) = k_n(w−1)·(−ζ′/ζ(w)) and rectangle R_T (σ ∈ [−5/2, 2√n], Im ±T, T zero-avoiding):\nRectangleIntegral' J (corner1) (corner2) = Σ_{ρ zeros inside} mult·[1−(ρ/(ρ−1))ⁿ] + [1−(2/3)ⁿ] + ResW1 n.\n\nProof structure:\n1. P := principal part at 1 (explicit finite sum); J = P + R, R holomorphic at 1 with simple poles only (at the zeros inside + the trivial zero −2; note: need R's poles EXACTLY at those points — J's poles are at zeros of ζ (all nontrivial inside + trivial −2) and w=1; subtracting P removes w=1 ✓).\n2. ∮ R via the vendored simple-pole rectangle theorem (R satisfies HasSimplePolesOn inside) — residues: at each zero ρ: k_n(ρ−1)·(−mult) = mult·[1−(ρ/(ρ−1))ⁿ] via `logDerivResidue`-family + `ResidueMult` (vendored) — the residue of J at ρ: J = k_n(w−1)·(−ζ′/ζ), −ζ′/ζ has residue −mult at ρ (simple pole after R? no — −ζ′/ζ has a pole of order = zero multiplicity at ρ — WAIT: for MULTIPLE zeros (mult > 1), −ζ′/ζ has a SIMPLE pole with residue −mult (log derivative: order of pole is always 1, residue = multiplicity) ✓ so J's poles at zeros are simple regardless of zero multiplicity ✓ good (logDerivResidue handles: f'/f has simple pole with residue = analyticOrderAt ✓).\n3. ∮ P = A_1 = ResW1 n (pull-to-square + primitive-vanishing + ResidueTheoremInRectangle).\n4. ResW1 n = Σ_{i=1}^n C(n,i)·lcoeff(i−1) (Leibniz, definition of lcoeff via h).\n\nAlso the \"poles finite\" hypothesis of the vendored theorem: the zeros inside the rectangle are finite (Mathlib compact-finiteness ✓).\n\nAnd \"no poles on boundary\": T zero-avoiding (top/bottom); left/right verticals: σ = −5/2 (no zeros — trivial zeros at −2,−4: −2 IS on σ = −5/2?? NO: σ₀ = −5/2 is the real part of the left side; the trivial zero −2 has real part −2 ≠ −5/2 ✓ not on the vertical line; horizontal sides at Im = ±T: the trivial zero −2 is real (im = 0 ≠ ±T ✓); w = 1 (im 0 ✓); zeros: T zero-avoiding ✓; also need no zeros ON the left/right verticals: right vertical σ₁ = 2√n ≥ 20+ — zeros have re < 1 ✓ none; left σ₀ = −5/2: nontrivial zeros have re ∈ (0,1) ✓ none; w=1 inside ✓ (re 1 ∈ (−2.5, 2√n), im 0 ∈ (−T,T) ✓).\n\nWait — actually also ζ's pole at w = 1: J = k_n(w−1)·(−ζ′/ζ) — I need J to be meromorphic on the rectangle with the stated poles only. ζ zeros in the rectangle: nontrivial ones with |γ| < T (inside, since re ∈ (0,1) ⊂ (−2.5, 2√n)) + trivial zeros with re ∈ (−2.5, 2√n): −2 only (−4 < −2.5; 0? trivial zeros are at −2,−4,−6,... negative even integers — 0 is not a trivial zero ✓). Plus w = 1. That's the full pole set ✓.\n\nThis is a coherent plan. Estimated Lean: P-definition + holomorphic-at-1 of R (meromorphic order bookkeeping), the simple-pole rectangle application (residue computations at zeros — the k_n factor: ResidueMult (vendored): if f − A/(s−p) =O 1 and g holo at p, then f·g − A·g(p)/(s−p) =O 1 ✓ directly gives residue = A·g(p) = (−mult)·k_n(ρ−1) ✓), the principal-part integral, the Leibniz residue value. Maybe 400–600 lines. 1–2 sessions per the estimate — plausibly 2 given the fiddly bits.\n\nLet me also reconsider: do we even need the GENERAL gresidue machinery? No — the specific J decomposition approach avoids it. Good — faster.\n\nOne more piece to check: `iteratedDeriv_mul` existence and the exact form, plus `iteratedDeriv` of wⁿ and (w−1)ⁿ at 1: `iteratedDeriv n (fun w => w ^ n)` — for ℂ: iteratedDeriv k (w^n) = (n!)_k w^{n−k} (falling factorial) — via `iteratedDeriv_pow`? or compute from deriv_pow repeatedly. And A(w) = wⁿ − (w−1)ⁿ: A^{(j)}(1): via iteratedDeriv of each piece; (w−1)ⁿ's iteratedDeriv at 1: shift lemma — `iteratedDeriv (fun w => (w−1)^n) = (fun w => iteratedDeriv (w^n)) ∘ (· − 1)`... there's `iteratedDeriv_comp_sub`? Hmm — the STATE handoff warned: \"HasDerivAt.add_const adds to VALUE (use .comp for precomposition)\" — for iteratedDeriv similar subtleties. Bounded work.\n\nLet me now check the key APIs before writing code:\n- iteratedDeriv_mul existence/form\n- MeromorphicAt.order bookkeeping for R (J − P holomorphic at 1): need meromorphicOrderAt R 1 ≥ 0: R = J − P: order J at 1 = −(n+1)?? — proving J's order at 1 is −(n+1) and P's principal part matches: cleaner to show (w−1)^{n+1}·R = (w−1)^{n+1}J − (w−1)^{n+1}P = F − [its own Taylor polynomial of degree n] — and F minus its degree-n Taylor part vanishes to order n+1 at 1 (remainder of power series — `HasFPowerSeriesAt` remainder lemmas: the (n+1)-fold iterated derivative form — hmm, analytic-removable singularity: F(w) − Σ_{k=0}^n (F^{(k)}(1)/k!)(w−1)^k vanishes to order n+1 at 1 — so R = [F − TaylorPoly_n]/(w−1)^{n+1} has a removable singularity ⟹ analytic at 1 ✓. In Lean: `AnalyticAt.sub_Taylor_poly`? or via the order API: meromorphicOrderAt R 1 ≥ 0 ⟸ (w−1)^{n+1}R analytic with value... The cleanest: use `AnalyticAt.exists_...`... Mathlib: `HasFPowerSeriesAt` has `HasFPowerSeriesAt.exists_...`? There's the concept of `AnalyticAt.eq_sub_...`... Let me look for \"order of vanishing\" / `analyticOrderAt` API: analyticOrderAt of F − TaylorPoly ≥ n+1 — there might be lemmas about subtracting Taylor polynomials raising the analytic order. `AnalyticAt.order_...`? Alternatively prove R analytic at 1 via the MeromorphicAt order API directly: R = J − P with J meromorphic order −(n+1), P a rational function with the SAME principal part — order(R) ≥ 0 ⟺ principal parts match — provable by computing meromorphicOrderAt of R via the NF forms. Fiddly but standard.\n\nHmm — actually, maybe cleaner: don't define R = J − P abstractly. Instead define R(w) := J(w) − P(w) and prove `HolomorphicOn R (Rectangle z w \\ {poles})` directly + the vendored rectangle theorem's MeromorphicOn hypotheses. The vendored `RectangleIntegral'_eq_sumResiduesIn` needs: MeromorphicOn f (Rectangle), no poles on boundary, poles finite, HasSimplePolesOn. For R: meromorphic everywhere (J meromorphic − P rational), poles only at zeros/trivial (simple) — the holomorphic-at-1 needs the order computation.\n\nOK — I have a clear plan. This sub-stage (ii′-1b) has real meat; let me structure it as:\n- ii′-1b(i): the w=1 residue value theorem (ResW1 = Σ C(n,i)·lcoeff(i−1)) — Leibniz + h analyticity. [self-contained]\n- ii′-1b(ii): the principal-part integral (∮ P = ResW1).\n- ii′-1b(iii): R's holomorphic-at-1 + rectangle residue theorem for J (the full sides identity).\n\nGiven session constraints, let me start with (i) — and first check the API landscape for iteratedDeriv products/powers and the MeromorphicAt order API. Let me also check `HolomorphicOn.vanishesOnRectangle` and `ResidueTheoremInRectangle` exact statements (vendored).\n\nLet me start the session: update todos, check APIs.","signature":""},{"type":"text","text":"Session 016 — **sub-stage ii′-1b: R1 residue machinery**. Design decision (refining D-064 R1): instead of a fully general residue theory, use a **principal-part split** for our specific integrand J — J = P + R with P the explicit principal part at w=1 and R having only simple poles — reusing the vendored simple-pole rectangle theorem directly. Bounded and cleaner. Let me verify the needed APIs first."},{"type":"tool_use","id":"TodoWrite_173","name":"TodoWrite","input":{"todos":[{"content":"Verify APIs: iteratedDeriv_mul/pow, vanishesOnRectangle, ResidueTheoremInRectangle","status":"in_progress","activeForm":"Verifying residue APIs"},{"content":"ii′-1b(i): w=1 residue value (Leibniz, ResW1 = Σ C(n,i)·lcoeff(i−1))","status":"pending","activeForm":"Proving w=1 residue value"},{"content":"ii′-1b(ii): principal-part integral ∮ P = ResW1","status":"pending","activeForm":"Proving principal-part integral"},{"content":"ii′-1b(iii): R holomorphic at 1 + rectangle residue theorem for J","status":"pending","activeForm":"Proving rectangle residue theorem"},{"content":"Session-016 closure (journal, STATE, commit)","status":"pending","activeForm":"Closing session 016"}]},"extra_content":null}]