[{"type":"thinking","thinking":"CanonicalDecomposition.lean is about FINITE Blaschke products on disks — not the Weierstrass infinite product. So Mathlib does NOT have the Hadamard/Weierstrass infinite product factorization, the minimum-modulus theorem, or the order-implies-genus theory. Building those is a MAJOR undertaking (this is what D-064 called \"heavy but self-contained\" — but on inspection, it's really: infinite-product infrastructure (partial), log-existence on simply connected domains (partial via HasPrimitives), minimum-modulus for canonical products (MISSING — this is the hard analytic core), order theory (MISSING)).\n\nHmm wait — but hold on. Let me reconsider. For the COEFFICIENT identity, maybe I don't need the full \"ξ/Z = e^{A+Bs}\" global statement. What I need: σ_k = −g^{(k−1)}(0)/(k−1)! for k ≥ 1 where g = ξ′/ξ. Equivalent: log ξ(s) = log ξ(0) − Σ_{m≥1} σ_m s^m/m on a disk around 0. \n\nDIFFERENT IDEA — the ARGUMENT-PRINCIPLE generating function, but with the kernel chosen to produce the FULL generating series in one shot: consider, for fixed s with |s| small, the function w ↦ log(1 − s/w) + s/w (analytic in w off {0, s} and the zeros...). The contour identity: (1/2πi)∮ [log(1−s/w) + s/w]·g(w)dw over the zero-avoiding rectangle [−2,3]×[−T,T]:\n= Σ_{|γ|<T} mult·[log(1−s/ρ) + s/ρ] + [contribution from w = 0: g = ξ′/ξ analytic at 0; the kernel log(1−s/w) + s/w has... at w = 0: log(1−s/w) = log(−s/w) + log(1 − w/s)?? — log(1−s/w) is NOT analytic at 0 — it blows up like log(1/w) — the residue of log(1−s/w)·g(w) at 0 — the log singularity is integrable but the residue... The residue of a log singularity: ∮ around 0 of log(1−s/w)g(w)dw — the log has a branch — UGH. The classical approach takes REAL kernels.\n\nHonestly — the classical proof of (4.1) IS the Hadamard product, and the minimum-modulus machinery is the price. D-064's β1 said \"Heavy but self-contained\" with `MeromorphicOn.extract_zeros_poles` as the seed — but on inspection that lemma is finite-only. So β1 as scoped in D-064 was OPTIMISTIC about Mathlib coverage. The real Mathlib gap: (i) infinite Weierstrass products; (ii) order theory / minimum modulus; (iii) digamma series.\n\nHmm — wait wait wait. Let me step WAY back. Let me reconsider what's actually needed by the ASSEMBLY (ii′-6). The crux: Sf(n) = ResW1 n for n ≥ 1, i.e.\n\n  SInfty n + 1 − (liCoeff n).re = (ResW1 n).re\n\nNow — here's a thought: BOTH SIDES are now built from proved pieces:\n- liCoeff n = Σ_j (−1)^{j+1}C(n,j)σ_j [PROVED ii′-2]\n- SInfty n = Σ_j (−1)^j C(n,j) a_j [PROVED ii′-2]\n- ResW1 n = Σ_j C(n,j)·lcoeff(j−1) [PROVED ii′-1b(i)]\n\nCrux ⟺ Σ_j C(n,j)[(−1)^j a_j + (−1)^{j+1} σ_j] + 1 = Σ_j C(n,j)·(lcoeff(j−1)).re.\nSufficient per-term: (lcoeff(j−1)).re = (−1)^j a_j + (−1)^{j+1}σ_j + δ_j where Σ_j C(n,j)δ_j = −1... — the per-term sufficient condition is exactly the (4.10)-a-form with the (−1)^{j−1} = −(−1)^j piece: (lcoeff(j−1)).re = (−1)^j a_j + (−1)^{j+1}σ_j + (−1)^{j−1}·[j...] — wait the full statement had the +1 canceling via Σ C(n,j)(−1)^j = −1. So the per-term identity c_{j−1} = (−1)^j(a_j + σ_j) + (−1)^{j−1} summed: Σ C(n,j)c_{j−1} = Σ C(n,j)(−1)^j(a_j+σ_j) + Σ C(n,j)(−1)^{j−1} = Σ C(n,j)(−1)^j(a_j+σ_j) + 1 − ... Σ_{j=1}^n C(n,j)(−1)^{j−1} = −Σ C(n,j)(−1)^j = −((1−1)^n − 1) = 1 (n ≥ 1). So Σ C(n,j)c_{j−1} = Σ C(n,j)(−1)^j(a_j+σ_j) + 1 — then the crux: S_∞ + 1 − λ = Σ C(n,j)(−1)^j a_j + 1 − Σ C(n,j)(−1)^{j+1}σ_j = Σ C(n,j)(−1)^j(a_j + σ_j) + 1 ✓ = Σ C(n,j)c_{j−1} ✓✓ consistent.\n\nNow — the lcoeff are defined via hLi's iterated derivatives at 1. And hLi(w) = 1 − (w−1)(zetaA′/zetaA)(w). Consider instead working with **ξ** directly: hXi(s) := −ξ′/ξ(1+s)·... — the identity (4.10) is the coefficient comparison of two expressions for ξ′/ξ(1+s). The ξ logDeriv decomposition: ξ′/ξ(1+s) = ΓR-piece + ζ-piece + pole pieces. What if I DEFINE nothing new and prove the per-k identity via the CONTOUR for σ_k but with the ARCHIMEDEAN and ζ-Laurent pieces computed via the SAME integrals?\n\nActually — you know what, let me look at this from the σ_k-closed-form angle ONE more time, because there IS a classical closed form for σ_k that bypasses everything: **the power sums σ_k are determined by the Taylor coefficients of log ξ at 0 — AND log ξ's Taylor coefficients at 0 are explicit from the FE + the values of ζ at positive integers!** Let me redo this carefully:\n\nlog ξ(s) = log(s(s−1)/2) + log ΓR(s) + log ζ(s) — as Taylor series at 0... each piece has a known expansion:\n- log(s(s−1)/2): log s + log(1−s) − log 2 — singular log s — ugh, ξ(0) = 1/2 — ξ is nonzero at 0 but the FACTORS are singular — the standard move: ξ(s) = ξ(1−s) and expand at 1... same pole issue at 1 (ζ's pole). Lagarias handles it via the σ-side absorbing it.\n\nOK here's yet another angle — THE DIRECT TAYLOR-COEFFICIENT attack on (4.10)-a-form via the FE, avoiding both products and contours:\n\nWe want: for k ≥ 1: c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1}.\n\nWhat are the objects?\n- c_{k−1} = lcoeff(k−1): Taylor coefficient of hLi at 1 (k ≥ 1: index k−1 ≥ 0; lcoeff(k−1) = hLi^{(k)}(1)/k!).\n- a_k: archimedean odd-zeta values (a₁ = (log4π+γ)/2, a_k = (1−2^{−k})ζ(k) for k ≥ 2).\n- σ_k: paired zero power sums.\n\nAnd the ξ decomposition: ξ′/ξ(w) = 1/w + 1/(w−1) + ΓR′/ΓR(w) + ζ′/ζ(w) — evaluate at w = 1+s:\nξ′/ξ(1+s) = 1/(1+s) + 1/s + ΓR′/ΓR(1+s) + ζ′/ζ(1+s).\nThe LHS via the FE: ξ′/ξ(1+s) = −ξ′/ξ(−s) (from ξ(1+s) = ξ(−s)... ξ(w) = ξ(1−w): set w = 1+s: ξ(1+s) = ξ(−s) ✓; differentiate: ξ′(1+s) = −ξ′(−s) ✓; so ξ′/ξ(1+s) = −ξ′/ξ(−s) ✓).\n\nSo: −ξ′/ξ(−s) = 1/(1+s) + 1/s + ΓR′/ΓR(1+s) + ζ′/ζ(1+s).\n⟹ −[ξ′/ξ(−s) + ζ′/ζ(1+s)·...] — collect: −ξ′/ξ(−s) − 1/(1+s) − ΓR′/ΓR(1+s) = 1/s + ζ′/ζ(1+s).\nThe RHS: 1/s + ζ′/ζ(1+s) = 1/s − [1/s + Σ_j c_j s^j] = −Σ_j c_j s^j (via piece B: −ζ′/ζ(1+s) = 1/s + Σ c_j s^j — i.e. ζ′/ζ(1+s) = −1/s − Σ c_j s^j ✓). So:\n  RHS = −Σ_{j≥0} c_j s^j — analytic at 0, value −c₀.\n  LHS = −ξ′/ξ(−s) − 1/(1+s) − ΓR′/ΓR(1+s) — each piece's Taylor series at 0:\n    −1/(1+s) = Σ_j (−1)^{j+1} s^j.\n    −ΓR′/ΓR(1+s) = −Σ_j τ_j s^j (τ_j = its Taylor coefficients — piece A).\n    −ξ′/ξ(−s): Taylor coefficients: (−ξ′/ξ(−·))^{(j)}(0)/j! = + (ξ′/ξ)^{(j)}(0)·(−1)^{j+1}·... (d/ds)^j [−g(−s)] = −(−1)^j g^{(j)}(−s) = (−1)^{j+1}g^{(j)}(−s); at 0: (−1)^{j+1}g^{(j)}(0). So −ξ′/ξ(−s) = Σ_j (−1)^{j+1} g^{(j)}(0)/j! · s^j where g = ξ′/ξ.\n  Coefficient of s^j in LHS: (−1)^{j+1}g^{(j)}(0)/j! + (−1)^{j+1} − τ_j.\n  Equate with RHS's −c_j:\n    −c_j = (−1)^{j+1} g^{(j)}(0)/j! + (−1)^{j+1} − τ_j   ... (*)\n  For j = k−1: −c_{k−1} = (−1)^k g^{(k−1)}(0)/(k−1)! + (−1)^k − τ_{k−1}.\n  Compare with the target c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1} = (−1)^k a_k + (−1)^k σ_k − (−1)^k:\n    −c_{k−1} = −(−1)^k a_k − (−1)^k σ_k + (−1)^k.\n  So (*) + target ⟺ (−1)^k g^{(k−1)}(0)/(k−1)! + (−1)^k − τ_{k−1} = −(−1)^k a_k − (−1)^k σ_k + (−1)^k\n    ⟺ (−1)^k g^{(k−1)}(0)/(k−1)! = −(−1)^k a_k − (−1)^k σ_k + τ_{k−1}\n    ⟺ g^{(k−1)}(0)/(k−1)! = −a_k − σ_k + (−1)^k τ_{k−1}\n  With τ_{k−1} = (−1)^k a_k (piece A): RHS = −a_k − σ_k + a_k = −σ_k ✓. So everything ⟺ **(M): g^{(k−1)}(0)/(k−1)! = −σ_k for k ≥ 1** — the moment identity (4.1) at 0. As expected — (M) is the irreducible core.\n\nSo the whole thing ⟺ (M) + (A: τ_j evaluation) + (B: lcoeff reading ✓ done). (M) is the content; (A) is the digamma work.\n\n**For (M): the generating-function contour identity.** Consider for fixed s (|s| < 1, say) the function of w:\n  K_s(w) := log(1 − s/w) + s/w  — NO. Branch hell.\n\n**The clean classical alternative for (M): differentiate a DIFFERENT global object.** Hmm.\n\nWhat about proving (M) from Zeta23's EF after all? The EF gives Σ mult·h(γ) for h = paperFT(k), k ∈ C²_c. I want the moment σ_k = Σ mult·ρ^{−k}, ρ = 1/2 + iγ. Now: ρ^{−k} = (1/2+iγ)^{−k} — as a function of γ: φ(γ) := (1/2+iγ)^{−k} — is φ a paperFT of some C²_c k? paperFT k(z) = ∫ k(u)e^{izu}du — entire, exp type, decay on ℝ like 1/u² (C² ⟹ h(u) = O(1/u²) on ℝ). φ(z) = (1/2+iz)^{−k} — NOT entire. NO.\n\nWhat about σ_k via RESIDUE of Zeta23's WeilEF zero-sum machinery at a finer level — the ZeroSumLimit.lean file (\"zero sum limit\") — maybe they have Σ mult·h(γ) for MORE general h (L² or Schwartz)? The EF extension classes: Schwartz h? If the EF held for h(z) = e^{-z²}·... no — (1/2+iz)^{−k} isn't Schwartz-entire either.\n\nOK here's ANOTHER thought — the σ_k are moments of 1/ρ. The function 1/w on the zeros. Consider the contour integral with kernel 1/(w−z) (Cauchy kernel) at z near 0: (1/2πi)∮ (1/(w−z))·g(w) dw... = Σ mult/(ρ−z) + ... — the generating function of the σ's: Σ_k σ_k z^{k−1} = Σ_ρ mult·1/(ρ−z)... indeed 1/(ρ−z) = Σ_k z^{k−1}/ρ^k for |z| < |ρ|. So the generating function G(z) := Σ_ρ mult/(ρ−z) (converges absolutely for z not a zero: |1/(ρ−z)| ≤ C/|ρ|² for |ρ| ≥ 2|z| ✓) — and G(z) = Σ_{k≥1} σ_k z^{k−1} for |z| small ✓ — and the CLAIM (M): G(z) = −g(z) − σ₁ + ... hmm: −g(z) = Σ σ_{k+1} z^k — i.e. G(z) = σ₁ + Σ_{k≥2} σ_k z^{k−1} = −g(z) ⟺ g(z) = −G(z)... — wait is the claim g(z) = −Σ_ρ mult/(ρ−z)?? Let me sanity check via the Hadamard product: g = ξ′/ξ = B + Σ mult·(1/(s−ρ) + 1/ρ) [logDeriv of (1−s/ρ)e^{s/ρ} = −1/(ρ−s)·... (log(1−s/ρ) + s/ρ)′ = −1/(ρ−s) + 1/ρ ✓]. So g(z) = B + Σ mult·(1/ρ − 1/(ρ−z)) = B + Σ mult·(z)/(ρ(ρ−z))·... = B − Σ mult·(1/(ρ−z) − 1/ρ). And Σ mult·(1/(ρ−z) − 1/ρ) = G(z) − G(0) — so g(z) = B − G(z) + G(0). (M) at order 0: g(0) = −σ₁: B + G(0)·... g(0) = B − G(0) + G(0) = B ⟹ B = g(0) = −σ₁ (the m=0 case). And then g(z) = −G(z) + G(0) − σ₁·... wait: g(z) = B − (G(z) − G(0))·... hmm: g(z) = B − Σ mult(1/(ρ−z) − 1/ρ) = B − G(z) + G(0). If B = −σ₁ and G(0) = Σ mult/ρ = σ₁ (k=1 — conditionally convergent!! G(0) = Σ mult/ρ — NOT absolutely convergent — the same k=1 subtlety) — with the PAIRED understanding G(0) := sigmaP 1 = σ₁: g(z) = −G(z) + σ₁ − σ₁ = −G(z)?? Hmm: B − G(z) + G(0) = −σ₁ − G(z) + σ₁ = −G(z) ✓. So (M) ⟺ g(z) = −G(z) on the disk ⟺ **ξ′/ξ(z) = −Σ_ρ mult/(ρ−z)** — the \"ξ′/ξ = sum over zeros\" identity — which is EXACTLY the partial-fraction expansion of ξ′/ξ — the standard content of the Hadamard product's logDeriv. Of course.\n\nAnd G(z) = Σ mult/(ρ−z) = Σ mult·(1/(ρ−z) − 1/ρ) + σ₁·... — the convergent form: G(z) = Σ mult·[1/(ρ−z) − 1/ρ] + σ₁ = Σ mult·z/(ρ(ρ−z))·... whatever.\n\nSo (M) ⟺ ξ′/ξ = −G on a disk. Both sides meromorphic on ℂ... The difference D(z) := ξ′/ξ(z) + G(z): analytic on the small disk (G analytic there ✓; ξ′/ξ analytic since ξ ≠ 0 ✓). Need D ≡ 0 on the disk. Hmm — what's D's behavior as |z| → ∞? ξ′/ξ(z) for z = 2+it... this still needs global input. The identity can't be bootstrapped locally. RIGHT — this is a theorem, not a coincidence.\n\nOK so let me now seriously cost the MINIMUM path. The claim (M): ξ′/ξ(z) = −Σ_ρ mult·(1/(ρ−z) − 1/ρ) + g(0)−ish... Let me restate cleanly:\n\n(M*) On |z| < r₀ (some zero-free disk at 0): ξ′/ξ(z) = ξ′/ξ(0) − Σ_ρ mult·[1/(ρ−z) − 1/ρ]  — with the bracketed series absolutely convergent. AND the k=1 fact: ξ′/ξ(0) = −σ₁ (paired).\n\nHmm — actually, from the *-symmetry the k=1 fact ξ′/ξ(0) = −σ₁: ξ′/ξ(0) = −ξ′/ξ(1) (FE) — and via the decomposition at 1: ξ′/ξ(1) = [1/w + 1/(w−1) + ΓR′/ΓR + ζ′/ζ]_{w=1}: 1 + [1/(w−1) + ζ′/ζ(w)]_{w=1} + ΓR′/ΓR(1) = 1 + c₀' + τ₀ where [1/(w−1) + ζ′/ζ(w)]_{w=1} =: the finite part = −c₀·... ζ′/ζ(w) = 1/(w−1)·[ζ′/ζ(w)·(w−1)] = −hLi(w)/(w−1): so 1/(w−1) + ζ′/ζ(w) = (1 − hLi(w))/(w−1) — at w = 1: (1−hLi(w))/(w−1) → −hLi′(1) (since hLi(1) = 1) = −lcoeff(0)·1!·... hLi′(1) = iteratedDeriv 1 hLi 1 = lcoeff 0 · 1! = c₀·... lcoeff 0 := iteratedDeriv 1 hLi 1/1! = hLi′(1) ✓ so the value = −lcoeff 0 = −c₀. So ξ′/ξ(1) = 1 − c₀ + τ₀ — wait sign: (1 − hLi(w))/(w−1) at w→1: 1−hLi(w) ≈ −hLi′(1)(w−1): ratio → −hLi′(1) = −c₀ ✓. So ξ′/ξ(0) = −(1 − c₀ + τ₀) = −1 + c₀ − τ₀ = −1 + c₀ + a₁ (τ₀ = −a₁). And the claim: ξ′/ξ(0) = −σ₁ ⟺ σ₁ = 1 − c₀ − a₁·... −ξ′/ξ(0) = 1 − c₀ − a₁·... σ₁ = −ξ′/ξ(0) = 1 − c₀ + τ₀ = 1 − c₀ − a₁ — CHECK numerically: 1 − (−γ) − (log4π+γ)/2 = 1 + γ − (log 4π)/2 − γ/2 = 1 + γ/2 − (log 4π)/2 ✓✓ the Davenport value ✓.\n\nSo (M) at order 0 (k=1: σ₁ = −ξ′/ξ(0)) — is ITSELF the identity σ₁ = 1 − c₀ − a₁ — which is EXACTLY the k=1 case of the a-form (4.10)!! (c₀ = 1 − a₁ − σ₁ ⟺ (4.10)-a at k=1 ✓). So k=1 is self-referential in this packaging — it must come from an independent argument (the symmetrized-kernel contour integral, which works: the kernel 1/(w(1−w)) decays quadratically ✓).\n\nAnd for k ≥ 2, the contour with w^{−k}... earlier concern was the vertical lines' survival. Let me redo it RIGHT: the rectangle [−2, 3] × [−T, T] with kernel w^{−k}, k ≥ 2:\n(1/2πi)∮ = Σ_{|γ|<T} mult·ρ^{−k} + Res_{w=0} w^{−k}g(w).\nAs T → ∞ (zero-avoiding): top/bottom → 0 ✓ (R-bound). Verticals: (1/2πi)[∫_{3−i∞}^{3+i∞} − ∫_{−2−i∞}^{−2+i∞}] w^{−k}g(w)dw. So:\nΣ_ρ mult·ρ^{−k} + g^{(k−1)}(0)/(k−1)! = (1/2πi)[V(3) − V(−2)] where V(a) := ∫_{a−i∞}^{a+i∞} w^{−k}g(w)dw.\nFor this to give (M) I need (1/2πi)[V(3) − V(−2)] = 0?? That's only true if the vertical integrals cancel — they DON'T in general. Hmm — UNLESS we also shift: V(a) for a > 1: as a → +∞, V(a) → 0? |g(a+it)| on the right: |ζ′/ζ| ≤ ΣΛ(n)n^{−a} ≤ C·2^{−a}-ish (dominated by n=2 term) → 0 as a → ∞ ✓; |ΓR′/ΓR(a+it)| ~ (1/2)log|a/2+it/2| — GROWS — with w^{−k}: V(a) ~ ∫ log(a+|t|)(a²+t²)^{−k/2}dt ~ log a·a^{1−k} → 0 for k ≥ 2 ✓. So V(a) → 0 as a → ∞ for k ≥ 2 ✓. And V(3) − V(−2) = (2πi)·[sum of residues of w^{−k}g between Re −2 and Re 3] — the residues: zeros of ξ (the ρ's — those are the ones inside already counted...) — hold on, I'm double counting. Let me restart the contour bookkeeping cleanly:\n\nActually the classical statement (Davenport Ch. 12 style): for k ≥ 2,\n  Σ_ρ mult·ρ^{−k} = −(1/2πi)∫_{(c)} w^{−k}·(ξ′/ξ)(w) dw − (Taylor piece at 0)\nwhere (c) is a vertical line with 0 < ... no wait. The clean classical identity: for k ≥ 2, take the contour = vertical line Re = c (c > 1) closed to the LEFT via the T-rectangles: (1/2πi)∫_{(c)} w^{−k}g(w)dw − [residues to the right of... g has no poles to the right of Re = 1 except... ξ′/ξ poles: zeros of ξ (the ρ's, 0 < re < 1) and... ξ entire ⟹ g = ξ′/ξ meromorphic with poles ONLY at the ρ's. Plus the kernel's pole at 0. So between Re = −2 and Re = 3: poles = {ρ's} ∪ {0}.\nClosing V(3) to the left (T → ∞ then the line moves left across everything): \n(1/2πi)V(3) = Σ_{all ρ} mult·ρ^{−k} + Res_0[w^{−k}g] + (1/2πi)V(−2)?? — NO: V(3) − V(−2) = 2πi·(Σ residues between) only if the top/bottom vanish — they do (k ≥ 2). So:\n(1/2πi)(V(3) − V(−2)) = Σ_{ρ in strip −2<re<3} mult ρ^{−k} + Res_0.\nThe ρ's all have 0 < re < 1 ⊆ (−2, 3) ✓ ALL of them. So (1/2πi)(V(3) − V(−2)) = Σ_ρ mult·ρ^{−k} + g^{(k−1)}(0)/(k−1)!.\nNow ALSO: V(−2): reflect via FE: g(−2+it) = −g(3−it): V(−2) = ∫ g(−2+it)(−2+it)^{−k}dt = −∫ g(3−it)(−2+it)^{−k}dt — substitute t ↦ −t: = −∫ g(3+it)(−2−it)^{−k}dt = −∫ g(3+it)·(−1)^k(2+it)^{−k}dt. Hmm — so V(−2) = −(−1)^k∫ g(3+it)(2+it)^{−k}dt = (−1)^{k+1}·Ṽ(2) where Ṽ(a) := ∫ g(a+it)(a+it)^{−k}dt with a = 2... not the same kernel position as V(3) — (2+it) vs (3+it). So V(3) − V(−2) = V(3) + (−1)^k Ṽ(2) — NOT zero. So:\n  Σ mult·ρ^{−k} + g^{(k−1)}(0)/(k−1)! = (1/2πi)[V(3) + (−1)^k Ṽ(2)].\nFor (M) I'd need the RHS = 0 — it ISN'T obviously. Hmm — BUT WAIT: is (M) even TRUE as I stated? Test with the known numbers: σ₂ = Σ 1/ρ² = 1 − π²/8 + ... hmm let me recall: σ₁ = 0.02309570896612103 (Davenport); σ₂ = 1 − γ²... no. Known: Σ_ρ 1/ρ² = 1 − (π²/8) + ...? I recall σ₂ = 1 − π²/8 + log²(2π)/...? not offhand. The relation (4.1): −ξ′/ξ(s) = Σ σ_{m+1}s^m near 0 — at s = 0: −ξ′/ξ(0) = σ₁ ✓ (Lagarias 4.1 with A = −σ₁). So (M) as Lagarias states it is right, and my contour derivation must be missing that V(3) + (−1)^k Ṽ(2) = −g^{(k−1)}(0)/(k−1)! + ... — no wait — the point is that V(3)−V(−2) is NOT zero, and its evaluation gives exactly the Hadamard content by a DIFFERENT grouping. The evaluation of V(3): split g = ΓR′/ΓR + (ζ′/ζ + 1/(w−1)) + 1/w·... each piece's vertical integral: ∫(3+it)^{−k}·(1/(3+it))dt = ∫(3+it)^{−(k+1)}dt = 0 for k+1 ≥ 2 (Jordan: the integral of w^{−m} over a vertical line is 0 for m ≥ 2 — close left or right, no poles... w^{−m} has pole at 0 — closing to the RIGHT (Re → +∞) encloses no poles ⟹ 0 ✓ but the closing needs |integrand| decay ✓ m ≥ 2 ✓). So ∫_{(3)} w^{−k}/w dw = 0. Similarly 1/(w−1) piece: w^{−k}/(w−1) — pole at w = 1 — closing right encloses 1: residue 1/1^k = 1 — so (1/2πi)∫_{(3)} w^{−k}/(w−1)dw = 1? sign/orientation — closing to the right: the line oriented upward + right closure = CLOCKWISE around the right half-plane — gives −residues... I'll nail signs later. The ζ′/ζ piece: −Σ Λ(n)/n^w integrated: (1/2πi)∫_{(3)} w^{−k}(−Σ Λ(n)n^{−w})dw = −Σ Λ(n)·(1/2πi)∫_{(3)} w^{−k}n^{−w}dw — and (1/2πi)∫_{(3)} w^{−k}n^{−w}dw = (log n)^{k−1}/(k−1)!·n^{0}·[n > 1 indicator...] hmm — the standard: (1/2πi)∫_{(c)} x^w/w^{k} dw = (log x)^{k−1}/(k−1)! for x ≥ 1, 0 for 0 < x < 1 (close right for x<1: x^w → 0 for Re → +∞ when x < 1 ✓ no poles right ⟹ 0 ✓; for x ≥ 1 close left: picks the residue at 0: (log x)^{k−1}/(k−1)! ✓). With x = 1/n ≤ 1/2 < 1 for n ≥ 2: the integral = 0!!! So the ζ′/ζ piece VANISHES at Re = 3 ✓✓ (that's why c > 1 with n^{−w}: all terms close right). Similarly the ΓR′/ΓR piece: (1/2πi)∫_{(3)} w^{−k}ΓR′/ΓR(w)dw — closing to the right: ΓR′/ΓR(w) has poles at w = 2,4,6,...? no wait — ΓR(w) = π^{−w/2}Γ(w/2): poles of Γ(w/2) at w/2 = 0,−1,−2,... i.e. w = 0,−2,−4,... — LEFT half — closing RIGHT: no poles; decay: |ΓR′/ΓR(a+it)| ~ (1/2)log(|w|/2) — the closing at Re → +∞: the log grows, w^{−k} decays — Jordan on the right quarter-circle: |w^{−k}ΓR′/ΓR| ~ log R·R^{−k}·(arc R) = log R·R^{1−k} → 0 for k ≥ 2 ✓ so the ΓR piece at (3) also vanishes?? Then V(3) = 0 + 0 + (the 1/(w−1) piece) + ... hmm wait but then where does σ_k's true value come from? Let me recount: (1/2πi)V(3) = Σ_{ρ} mult·ρ^{−k} + Res_0 + (1/2πi)V(−2) — I had it backwards. Let me FIX the bookkeeping with the push-V(3)-right idea:\n\nPush the line Re = 3 to Re = +∞: V(3) − V(A) for A → ∞ = 2πi·(residues between 3 and A) — g has NO poles with re > 1... the ρ's have re < 1 < 3 — none between 3 and A. The kernel pole at 0 — not in (3, A). So V(3) = V(A) + 0 → 0. So **V(3) = 0** — let me verify with the piecewise computation: V(3) = ∫ w^{−k}g = ∫ w^{−k}ΓR′/ΓR + ∫ w^{−k}ζ′/ζ + ∫ w^{−k}/w + ∫ w^{−k}/(w−1). First three → 0 as computed (ζ piece termwise 0 for the x = 1/n < 1 reason ✓; the 1/w piece: ∫ w^{−(k+1)} = 0 ✓). The 1/(w−1) piece: ∫_{(3)} w^{−k}/(w−1)dw: close right: encloses w = 1? The region right of Re=3 contains NO w=1 (re 1 < 3) — close LEFT then: encloses 0 and 1: residues: at 1: 1/1^k = 1; at 0: w^{−k}/(w−1) has order-k pole: residue = (1/(k−1)!)·(d/dw)^{k−1}[1/(w−1)]_{w=0} = (1/(k−1)!)·(−1)^{k−1}(k−1)!/(0−1)^k·... (d/dw)^{k−1}(w−1)^{−1} = (−1)^{k−1}(k−1)!(w−1)^{−k}; at 0: (−1)^{k−1}(k−1)!/(−1)^k = −(k−1)!. So residue at 0 = −1. Sum of left residues: 1 + (−1) = 0. Either way the piece contributes 0 if closed right... closing right encloses nothing (poles at 0, 1 are LEFT of Re=3)... wait w = 1 has re 1 < 3 ✓ left. So closing right: 0 ✓. So V(3) = 0 ✓ consistently.\n\nNow V(−2): close LEFT (Re → −∞): (1/2πi)V(−2) = −[residues with re < −2] (orientation)... g's poles with re < −2: NONE (ρ's have re > 0). Kernel w^{−k} pole at 0: re 0 > −2 not counted. But ΓR′/ΓR's poles at −2,−4,...: those are INSIDE g = ξ′/ξ?? — NO: ξ is ENTIRE — g = ξ′/ξ's only poles are at ξ's zeros = the ρ's. The ΓR poles are CANCELED in ξ by ζ's trivial zeros ✓. So g has no poles at −4, −6, ... ✓. So closing V(−2) left encloses NO poles ⟹ V(−2) = 0?? Then V(3) − V(−2) = 0 ⟹ Σ mult·ρ^{−k} + Res_0 = 0 ⟹ Σ mult·ρ^{−k} = −g^{(k−1)}(0)/(k−1)! = (M) for k ≥ 2!!! ✓✓✓\n\nWait — but closing V(−2) to the left requires the LEFTWARD decay of w^{−k}g(w) — g(−A+it) = −g(1+A−it) (FE) — for A → ∞: 1+A has re > 1: |g(1+A−it)| = |ΓR′/ΓR| + |ζ′/ζ| + small ~ (1/2)log|w| + O(1) ✓ same as right ✓ so the left closure's arcs vanish like log A·A^{1−k} → 0 ✓ and the line-to-line difference encloses the poles with re ∈ (−A, −2)... g has no poles there but the TOP/BOTTOM horizontal segments at Im = ±T need the R-bound argument as T → ∞ FIRST (the order of limits: T → ∞ with zero-avoiding T_j, then A → ∞... or the rectangle at once). The honest assembly: rectangle [−A, 3]×[−T, T]: (1/2πi)∮ = Σ_{|γ|<T, all ρ since re ∈ (0,1) ⊂ (−A,3)} mult·ρ^{−k} + Res_0. As T → ∞ (avoiding): top/bottom → 0 (R-bound on |g| = O(log²T)... wait the R-bound is for ζ′/ζ — g = ξ′/ξ = ΓR′/ΓR + ζ′/ζ + 1/w + 1/(w−1): |ΓR′/ΓR(σ±iT)| ~ (1/2)log|w| ✓ O(log T); the ζ′/ζ on the horizontal: the R-bound (D-056: |ζ′/ζ(w) − Σ_{|γ−T|<1}1/(w−ρ)| ≤ A log(T+2) + B₀ for σ ∈ [−5/2, 4]... wait D-056's range: −5/2 ≤ σ ≤ 4 — my rectangle has Re from −A to 3 with A → ∞!! The R-bound covers σ ∈ [−5/2, 4] only. For σ < −5/2: use the FE: g(σ ± iT) = −g(1−σ ∓ iT) with 1−σ > 7/2 ∈ [−5/2, 4]? 1−σ for σ ≤ −5/2: ≥ 7/2 ≤ 4 only if σ ≥ −3. Hmm — σ ∈ [−A, −5/2]: 1−σ ∈ [7/2, 1+A] — OUTSIDE [−5/2, 4] for A > 1/2. The R-bound's range is limited. For re ≥ 4-ish: direct Euler-product bound: |ζ′/ζ(w)| ≤ Σ Λ(n)n^{−σ} ≤ ζ′/ζ(σ)-ish ≤ small for σ ≥ 4 ✓ (n^{−σ} ≤ n^{−4}, Σ Λ(n)n^{−4} converges ✓) and |ΓR′/ΓR| ~ log|w| ✓. So split the top side: σ ∈ [−5/2, 4] via R-bound; σ outside via direct (right) / FE-to-the-right (left: 1−σ ≥ 7/2 — the Euler bound needs re > 1 strictly ✓ 7/2 > 1 ✓ but the Euler bound |ζ′/ζ| ≤ Σ Λ(n)n^{−σ} needs re > 1 ✓ — for re = 7/2 ✓ fine — actually for re ≥ 4 I said but 7/2 works too — any re > 1: Σ Λ(n)n^{−re} converges ✓ bounded by its value at 7/2 say). So the top side bound: max over σ ∈ [−A, 3] of |g(σ+iT)| ≤ C log²T (R-bound zone) ∨ C log T (elsewhere) — with the zero-avoiding T ✓. Then top side integral: ≤ (A+3)·T^{−k}·C log²T — hmm (A+3) — A is FIXED per rectangle then A → ∞ AFTER T → ∞: order: first T → ∞ (fixed A): top/bottom → 0 ✓; then A → ∞: left side V(−A) → 0 (same bound: |g(−A+it)| ~ log(A+|t|), kernel (A²+t²)^{−k/2} — ∫ log(A+|t|)(A²+t²)^{−k/2}dt ~ log A·A^{1−k} → 0 ✓). So the two-stage limit gives Σ mult·ρ^{−k} + Res_0 = 0 ✓ — wait the LEFT side as A → ∞ with the T-limit already taken: the vertical line integral V(−A) is the T → ∞ limit of the left segment — converges (k ≥ 2 ✓) — then A → ∞ kills it ✓. ORDER: for each A, T → ∞ gives Σ_{all ρ} + Res_0 = V(3) − V(−A) = −V(−A) (V(3) = 0 shown) — wait V(3) = 0 was the A-STYLE push argument — let me redo: rectangle [−A, 3]: (1/2πi)∮_T = Σ_{|γ|<T} mult ρ^{−k} + Res_0(w^{−k}g). T → ∞: Σ + Res_0 = (1/2πi)(V(3) − V(−A)). Then A → ∞: V(−A) → 0 (the integrability+decay) and V(3) = 0?? — hmm V(3) is independent of A — is V(3) = 0? Push V(3) RIGHT to V(A'), A' → ∞: V(A') → 0 ✓ and the strip (3, A') contains no poles of the INTEGRAND w^{−k}g(w) (g's poles = ρ's with re < 1 < 3 ✓; kernel pole at 0 < 3 ✓) — so V(3) = V(A') for all A' — BUT WAIT the horizontal segments between Re=3 and Re=A' at Im = ±T — as T → ∞ — the R-bound on g there ✓ (σ ∈ [3, A']: right-zone direct bound ✓) — vanish ✓. So V(3) = lim V(A') = 0 ✓. Similarly V(−A) → 0 as A → ∞ (push left: no poles with re < −A... g's poles: ρ's re > 0 ✓; kernel pole 0 ✓ — none left of −A ✓; the horizontal segments at ±T between −A and −A': ζ′/ζ via FE → 1−σ ≥ ... for σ ∈ (−A', −A) with A ≥ 2: 1−σ ∈ (1+A, 1+A') ⊂ (3, ∞): direct Euler bound ✓ + ΓR log ✓ — vanish as T → ∞ ✓; then V(−A) as A → ∞ → 0 by the log·t^{−k} integrability ✓).\n\nCONCLUSION: Σ_ρ mult·ρ^{−k} = −Res_0[w^{−k}g] = −g^{(k−1)}(0)/(k−1)! for k ≥ 2 — the moment identity (M) for k ≥ 2, via:\n- the rectangle residue computation (have the machinery: rectangleIntegral'_mul_logDeriv_of_poles handles f = ξ with poles?? ξ is ENTIRE — P = ∅ — and g := w^{−k}... the weight must be analytic on the rectangle — w^{−k} isn't at 0! — so use the ppart-subtraction (my ii′-1b(ii) trick): the integrand w^{−k}g(w) has poles at the ρ's (simple, residue mult·ρ^{−k} — via logDeriv NF — my Rfun_residue_at pattern) and at 0 (order k, residue g^{(k−1)}(0)/(k−1)! — via the ppart subtraction: the principal part of w^{−k}g at 0 = Σ_{i=1}^{k} (g^{(k−i)}(0)/(k−i)!)·w^{−i} — integrate: the w^{−1} coefficient = g^{(k−1)}(0)/(k−1)! ✓ — SAME machinery as LiPrincipal but centered at 0 — my ppart/Acoeff/rectInt'_ppart are written for the point 1 and the specific F — need a small generalization: ppart at a general point p with a general analytic F — the LiPrincipal proofs were written for F = (wⁿ−(w−1)ⁿ)hLi at 1 — generalize the statements to (F, p) — moderate port).\n- The T → ∞ limit with zero-avoidance: the R-BOUND — ii′-5's content (D-056 route R3)! and the zero-counting for the pigeonhole (Trudgian N(T) — perimeter!). Hmm — actually the pigeonhole for a zero-avoiding T in [T₀, T₀+1] needs N(T+1)−N(T) = O(log T) — the C₀ bound — from Trudgian (perimeter, declared) ✓.\n- The vertical-line evaluations: V(3) = 0, V(−A) → 0 — the integrability of w^{−k}g(a+it) in t and the decay — the |g(a+it)| ≤ C log(a+|t|) for a ≥ 3 (Euler bound for ζ′/ζ + digamma growth for ΓR′/ΓR — the digamma bound |ψ(w)| ≤ C log|w| for re w ≥ 3/2 — is THAT in Mathlib? `Complex.digamma` asymptotics? Probably NOT directly. Hmm — the bound |ΓR′/ΓR(w)| ≤ C log(2+|w|) for re w ≥ 3: ψ(w) = log w − 1/(2w) + O(1/w²) (Stirling-series) — Mathlib has Stirling for complex? There's `Complex.Gamma... stirling`? Let me check — `tendsto_log_Gamma...`? For the vertical-line decay I need |ψ(a+it)| = O(log(a+|t|)) for a ≥ 3 — the crude bound from the series ψ(w) = ... hmm — or via `Complex.digamma` = logDeriv Gamma with the Stirling asymptotic — Mathlib's Stirling: `Real.stirling` / `Complex... stirling`? there's Stirling's formula in Mathlib (Real.Stirling) and for complex Gamma: `Complex.Gamma` Stirling — I recall `Complex.tendsto_...`? Not sure. Alternative: bound ψ via the series ψ(s) = −γ − 1/s + Σ_{m≥1}(1/m − 1/(s+m))·... — the series I might build for (III) anyway — from it: |ψ(a+it)| ≤ |γ| + 1/|s| + Σ |1/m − 1/(s+m)| = γ + 1/|s| + Σ |s|/(m|s+m|) — Σ_m |s|/(m|s+m|) for re s ≥ 3: |s+m| ≥ m+3, and |s+m| ≥ |t|: |s|/(m|s+m|) ≤ |s|/(m(m+3)) for |t| small and |s|/(m|t|) for |t| large: Σ_m min(...) ~ log(1+|t|) ✓ the standard estimate — derivable from the series with elementary bounds ✓. So if I build the ψ series for (III), the growth bound comes along ✓.\n\nSo — REVISED ii′-3 architecture (call it route β4, \"contour moments + Lagarias coefficient split\"):\n\nFor k ≥ 2 (and k = 1 via the symmetrized kernel):\n(S1) σ_k = −g^{(k−1)}(0)/(k−1)! for k ≥ 2 [contour: rectangle + R-bound T-limit + vertical evaluations]; and σ₁ = −g(0) via the paired kernel 1/(w(w−1))·(−1/2)... wait k=1: symmetrized: Σ mult/(ρ(1−ρ))·(1/2)·... = −g(0)? Earlier: sigmaP 1 = Σ mult/(2ρ(1−ρ)) = (g(1)−g(0))/2·... = −g(0) (FE) ✓ — via the kernel K(w) = 1/(2w(1−w))·g(w): poles: zeros ρ (residue mult/(2ρ(1−ρ))); w = 0: residue g(0)/2; w = 1: residue −g(1)/2·... 1/(2w(1−w)) at w=1: write = −1/(2w(w−1)): residue −1/2·g(1)·... hmm: 1/(2w(1−w)) = (1/2)(1/w + 1/(1−w)): at w=1: (1/2)·1/(1−w) = −(1/2)/(w−1): residue −g(1)/2. Total: Σ_{|γ|<T} mult/(2ρ(1−ρ)) + g(0)/2 − g(1)/2 → 0 as T → ∞?? — kernel ~ 1/T² ✓ top/bottom vanish (R-bound O(log²T)/T²·length-fixed... the rectangle [−2,2]×[−T,T] is FIXED in re — top side length 4 fixed — |integrand| ≤ C log²T/T² → 0 ✓). Verticals: V(2) − V(−2): NOT zero a priori!! Hmm — for the k=1 kernel: V(a) = ∫ (2a...)|kernel·g| ~ log|t|·t^{−2} — integrable ✓ nonzero. So Σ mult/(2ρ(1−ρ)) + g(0)/2 − g(1)/2 = (1/2πi)(V(2) − V(−2)). Evaluate: V(2): pieces: ∫ K(w)ΓR′/ΓR(w)dw etc. — the ζ′/ζ piece: −Σ Λ(n)·(1/2πi)∫_{(2)} K(w)n^{−w}dw — the K-kernel Laplace integrals: ∫_{(2)} n^{−w}/(2w(1−w))dw — computable but not zero (kernel poles at 0, 1 — LEFT of 2 — close right: 0? n^{−w} → 0 right for n ≥ 2 ✓ and K's poles at 0,1 are left of the line — closing right encloses nothing ⟹ the ζ-piece = 0 ✓ hmm wait but then the integral of just K(w)n^{−w} over Re=2 line closing right: the closure at +∞ — |K·n^{−w}| ~ |w|^{−2}n^{−re w} → 0 ✓ encloses no poles (K's poles at 0, 1 have re < 2 ✓ — wait closing RIGHT from Re=2: the region re > 2 contains no poles of K (0, 1 < 2 ✓) and n^{−w} entire ✓ so 0 ✓). The 1/w-piece of g: g has 1/w + 1/(w−1) + ΓR′/ΓR + ζ′/ζ — the polynomial pieces: ∫_{(2)} K(w)/w dw = ∫ 1/(2w²(1−w)) — close right: poles of the whole at 0, 1 — left — 0?? then V(2) = ∫ K·ΓR′/ΓR + 0 = the digamma integral — closing right: ΓR′/ΓR poles at −2,−4.. left; K poles at 0,1 left; decay: |K·ΓR′/ΓR| ~ t^{−2}log t integrable ✓ so V(2) = 0?? and V(−2) by FE-symmetry: K(w) = 1/(2w(1−w)): K(1−w) = 1/(2(1−w)w) = K(w) ✓ SYMMETRIC! So V(−2) = ∫ K(−2+it)g(−2+it)dt = −∫ K(−2+it)g(3−it)dt [FE] = ... substitute w' = 1−w: −2+it ↦ 3−it: dt ↦ −dt': −∫ K(1−w')g(w')·(−dt')·... let me just: V(−2) = ∫_{t} K(−2+it)g(−2+it)dt = −∫_t K(−2+it)g(3−it)dt; sub t = −u: = ∫_u K(−2−iu)g(3+iu)du; K(−2−iu) vs K(3+iu): not equal. Hmm so V(2) − V(−2) = 0 − V(−2) ≠ 0. Ugh. The symmetrization works around w = 1/2: use the line Re = 1/2?? poles on it (the zeros... no zeros ON the line necessarily... off RH zeros could be on the critical line — they ARE on it... wait RH isn't assumed! zeros have re ∈ (0,1) — the line re = 1/2 has zeros (most) — the contour must avoid them... classical k=1 proof: Davenport Ch. 12: Σ 1/ρ = 1 + γ/2 − (1/2)log 4π is proved via... the integral (1/2πi)∫ (ξ′/ξ)(w)·d... Let me look at how Davenport does Σ 1/ρ: he uses the partial fractions of ξ′/ξ = B + Σ(1/(s−ρ) + 1/ρ) — the HADAMARD product again — and evaluates B = −σ₁ via ξ′/ξ(0) = −ξ′/ξ(1) and the decomposition. So even Davenport's σ₁ uses Hadamard's B-evaluation. Hmm — BUT actually the evaluation B = −σ₁ is precisely the m=0 case of the moment series and Lagarias derives it via the *-rearrangement — which is a REARRANGEMENT argument, not a contour one: A = −Σ′ 1/ρ. Lagarias's \"one can also deduce by a ∗-convergent rearrangement that A = −Σ′_ρ 1/ρ\": the product ξ(s) = e^{B}e^{As}Π(1−s/ρ)e^{s/ρ} — take s = 1: ξ(1) = e^B e^A Π(1−1/ρ)e^{1/ρ} — and ξ(1) = ξ(0) = e^B Π 1·... at s=0: ξ(0) = e^B Π (1)·e^0 = e^B — hmm the product at 0 is Π 1 = 1 — so ξ(1)/ξ(0) = 1 = e^A Π_ρ (1−1/ρ)e^{1/ρ} = e^A Π_ρ (−1/ρ)·e^{1/ρ}·(ρ/(ρ−1))... (1−1/ρ) = (ρ−1)/ρ. Pair ρ ↔ 1−ρ̄: the *-pairing makes the product converge *-conditionally... this rearrangement computation yields e^A = e^{σ₁}-ish. It's a delicate but ELEMENTARY argument (no contour) — pairing factors. Hmm.\n\nOK — I've spent a lot of exploration. Let me consolidate the DESIGN DECISION for D-066. The honest cost map:\n\nRoute β1-full-Hadamard: Weierstrass product for ξ from scratch + minimum modulus + order theory — NOT in Mathlib — 4+ sessions, high risk.\n\nRoute β4-contour-moments (k ≥ 2): rectangle machinery ✓ HAVE; ppart at 0 generalization (small port from LiPrincipal); R-bound T-limit (ii′-5 machinery — SHARED); vertical evaluations (Euler/digamma growth bounds — moderate); k = 1 via... the paired kernel — the vertical evaluation for k=1 has the same \"V(2) = 0 and V(−2) → ?\" structure — let me recheck k=1's verticals: kernel K(w) = 1/(2w(1−w)) — rectangle [−A, 2]×[−T,T] hmm the poles at 0 and 1 are inside — fine they're the explicit residues. T → ∞: Σ_{all ρ} mult·K(ρ) + g(0)/2 − g(1)/2 = (1/2πi)(V(2) − V(−A)). V(2): as computed the ζ-piece vanishes (x = 1/n < 1 closes right ✓) — wait NO — for K the analysis: (1/2πi)∫_{(2)} K(w)n^{−w}dw — close right — K's poles at 0,1 are at re < 2 ✓ left — and n^{−w} entire ✓ — encloses NOTHING ⟹ 0 ✓; the 1/w + 1/(w−1) pieces of g: K(w)/w = 1/(2w²(1−w)): close right: poles at 0,1 — left — 0 ✓; K(w)/(w−1): same 0 ✓; the ΓR piece: close right: ΓR′/ΓR's poles at −2,−4,... left ✓; decay |K·ΓR′/ΓR| ~ log R/R² ✓ 0 ✓. So V(2) = 0 ✓. V(−A) as A → ∞: push left: V(−A) = V(−A') + 2πi·(poles of K·g between −A' and −A) — g's poles: ρ's (re > 0 ✓ not there); K's poles 0, 1 (re ≥ 0 ✓ not there) — so V(−A) → 0 IF the horizontal decay holds (FE-reflected bounds ✓) and the vertical decay |V(−A)| ~ log A·A^{−1}·... |K(−A+it)g(−A+it)| ~ (1/A²)·log(A+|t|) — ∫ ~ log A/A → 0 ✓✓. So k=1: Σ mult/(2ρ(1−ρ)) = (g(1) − g(0))/2·(−1)... sign: Σ + g(0)/2 − g(1)/2 = 0 ⟹ Σ mult/(2ρ(1−ρ)) = (g(1)−g(0))/2 = (−g(0)−g(0))/2 = −g(0) ✓ so sigmaP 1 = Σ mult/(2ρ(1−ρ)) [the reflect-pairing = conj-pairing equality — a separate rearrangement lemma ✓ sketched earlier] = −g(0) ✓✓ k=1 WORKS with the same machinery!\n\nSo route β4 gives ALL moments: σ_k = −g^{(k−1)}(0)/(k−1)! (k ≥ 2) and σ₁ = −g(0) — i.e. UNIFORMLY: σ_k = −g^{(k−1)}(0)/(k−1)! for k ≥ 1 (k=1: g^{(0)}(0)/0! = g(0) ✓). THIS IS (M)!! And the proof needs:\n- (β4-i) The rectangle residue theorem for w^{−k}g(w) (k ≥ 2) and K(w)g(w) (k=1): the logDeriv-of-poles machinery + the ppart-at-0 port + the residue-at-zeros computations. MODERATE (we have the patterns).\n- (β4-ii) The T → ∞ horizontal decay: |g(σ±iT)| = O(log²T) on the R-zone + O(log T) off it; zero-avoiding T via Trudgian (perimeter). This is SHARED with ii′-5 (the R-bound route R3) — the R-bound for ζ′/ζ (D-056, A = 10.5, B₀ = 48) — in Lean: Borel–Carathéodory (Mathlib ✓) + Jensen (Mathlib ✓) + Blaschke (StrongPNTPrefix ✓) + FE strip bound + digamma Lemma D — as mapped in D-064 R3. For β4 I need it only on the HORIZONTAL segments as an O(log T)·(clearance) bound — actually the full R-bound then the sum over |γ−T|<1 with the gap clearance. This is the ii′-5 content anyway.\n- (β4-iii) The vertical evaluations: V(3) = 0 / V(2)-type lines: decay of the pieces + the \"close right ⟹ 0\" argument (Jordan-style on rectangles to +∞: |piece| bounds: ζ′/ζ Euler bound (Σ Λ(n)n^{−re} — needs the Euler-product series for −ζ′/ζ on re > 1 — Mathlib: `riemannZeta_logDeriv...`? there's `logDeriv_riemannZeta_eq_...`? the Dirichlet series of −ζ′/ζ: `LSeries (−Λ)` — Mathlib has `riemannZeta_logDeriv`? hmm — there's `neg_logDeriv_riemannZeta`? I recall the LSeries machinery: `LSeries_vonMangoldt`? — Zeta23 uses the Euler product (riemannZeta_ne_zero_of_one_lt_re etc.) — the logDeriv series: `logDeriv_zeta_eq_neg...`? need to find. MODERATE.)\n- (β4-iv) The paired-sum rearrangement for k=1 (reflect-pair = conj-pair) — elementary mult-preservation reindexing. SMALL-MODERATE.\n- (β4-v) The FE reflection of derivatives: g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1): from completedRiemannZeta_one_sub (Mathlib ✓) — deriv of the FE: g(s) = −g(1−s): logDeriv of ξ(1−s): deriv (ξ∘(1−·)) s = −ξ′(1−s) — chain rule ✓ then iterated: iteratedDeriv of s ↦ g(1−s) at 0 = (−1)^{k−1}g^{(k−1)}(1) — `iteratedDeriv_comp_sub...`? the comp with 1−s: iteratedDeriv m (g ∘ (1 − ·)) 0 = (−1)^m g^{(m)}(1) — there should be iteratedDeriv_comp_sub_left or via iteratedDeriv_comp_sub_const pattern (LiResidue used iteratedDeriv_comp_sub_const) — there's `iteratedDeriv_comp_neg`? — derivable. SMALL.\n\nThen (4.10)-a-form follows: c_{k−1} = τ_{k−1} + (−1)^k σ_k + (−1)^{k−1} via the coefficient split at 1 (the algebra verified above) + τ-evaluation (piece A) + lcoeff reading (piece B ✓).\n\nWAIT — actually hold on: with (M) in hand (σ_k = −g^{(k−1)}(0)/(k−1)!), the cleanest finish: (V): g^{(k−1)}(0) = (−1)^k g^{(k−1)}(1) — so σ_k = −(−1)^k g^{(k−1)}(1)/(k−1)! = (−1)^{k+1} g^{(k−1)}(1)/(k−1)!.\nAnd g(1+s)'s Taylor coefficient of s^{k−1}: from g(1+s) = 1/(1+s) + [1/s + ζ′/ζ(1+s)] + ΓR′/ΓR(1+s) = Σ_j (−1)^j s^j + (−Σ_j c_j s^j) + Σ_j τ_j s^j: coefficient of s^{k−1}: (−1)^{k−1} − c_{k−1} + τ_{k−1}. So g^{(k−1)}(1)/(k−1)! = (−1)^{k−1} − c_{k−1} + τ_{k−1} and:\nσ_k = (−1)^{k+1}[(−1)^{k−1} − c_{k−1} + τ_{k−1}] = 1 + (−1)^k c_{k−1}... let me recompute: (−1)^{k+1}(−1)^{k−1} = (−1)^{2k} = 1; (−1)^{k+1}(−c_{k−1}) = (−1)^{k+2}c_{k−1} = (−1)^k c_{k−1}; (−1)^{k+1}τ_{k−1}. So σ_k = 1 + (−1)^k c_{k−1} + (−1)^{k+1}τ_{k−1}. Solve: (−1)^k c_{k−1} = σ_k − 1 − (−1)^{k+1}τ_{k−1} = σ_k − 1 + (−1)^k τ_{k−1}; c_{k−1} = (−1)^k σ_k − (−1)^k + τ_{k−1} = (−1)^k σ_k + τ_{k−1} + (−1)^{k−1} ✓. With τ_{k−1} = (−1)^k a_k: c_{k−1} = (−1)^k(a_k + σ_k) + (−1)^{k−1} ✓✓✓ TARGET.\n\nThe τ-evaluation (piece A): τ_j = (−1)^{j+1}a_{j+1}: the digamma work:\n- j = 0: τ₀ = −(log π)/2 + (1/2)ψ(1/2) = −(log 4π + γ)/2 = −a₁ ✓ via Complex.digamma_one_half ✓ MATHLIB HAS IT.\n- j ≥ 1: τ_j = ψ^{(j)}(1/2)/(j!·2^{j+1})·... = (−1)^{j+1}a_{j+1} via the ψ^{(j)}(1/2) formula — needs the digamma series / polygamma at 1/2 — the BohrMollerup-route build. MODERATE-HEAVY (but self-contained real analysis).\n\nHmm — can I avoid the polygamma-at-1/2 build? Alternative for τ_j (j ≥ 1): the generating function: Σ_j τ_j s^j = ΓR′/ΓR(1+s) — I need its coefficients = (−1)^{j+1}a_{j+1} with a_{j+1} = Σ_{m odd} m^{−(j+1)}. Equivalent: ΓR′/ΓR(1+s) = −a₁ + Σ_{j≥1} (−1)^{j+1}a_{j+1}s^j = −a₁ + Σ_{m odd ≥ 1} Σ_{j≥1} (−1)^{j+1}m^{−(j+1)}s^j — inner: Σ_{j≥1} (−1)^{j+1}(s/m)^j/m·... = (1/m)·(s/m)/(1+s/m) = s/(m(m+s))·... Σ_{j≥1} (−1)^{j+1}(s/m)^j = (s/m)·Σ_{j≥0}(−s/m)^j = (s/m)/(1+s/m) = s/(m+s). So the formal answer: ΓR′/ΓR(1+s) = −a₁ + Σ_{m odd ≥ 1} s/(m(m+s))·(1/m)?? let me recompute: a_{j+1} = Σ_{m odd} m^{−(j+1)} — so Σ_{j≥1}(−1)^{j+1}a_{j+1}s^j = Σ_{m odd} Σ_{j≥1}(−1)^{j+1}m^{−j−1}s^j = Σ_{m odd} (1/m)·(s/m)/(1+s/m) = Σ_{m odd} s/(m(m+s)). And the digamma partial fractions: ΓR′/ΓR(1+s) = −(log π)/2 + (1/2)ψ((1+s)/2): ψ((1+s)/2) = ψ(1/2 + s/2): the series ψ(1+z) = −γ + Σ_{m≥1} z/(m(m+z)) (the (4.19) rewritten: 1/m − 1/(z+m) = z/(m(z+m)) ✓). ψ(1/2+s/2) = ψ(1 + (s−1)/2) = −γ + Σ_m ((s−1)/2)/(m(m + (s−1)/2)) = −γ + Σ_m (s−1)/(m(2m+s−1)). At s = 0: −γ + Σ_m (−1)/(m(2m−1)) = −γ − 2log2 ✓ (the 2log2 sum ✓ consistent with digamma_one_half!). So ΓR′/ΓR(1+s) = −(log π)/2 − γ/2 + (1/2)Σ_{m≥1} (s−1)/(m(2m+s−1)) — and the claim decomposes: −(log π)/2 − γ/2 =? −a₁ + ... hmm let me just verify the generating identity: need (1/2)Σ_m (s−1)/(m(2m+s−1)) − γ/2 − (log π)/2 = −a₁ + Σ_{m odd ≥ 1} s/(m(m+s)). At s = 0: (1/2)Σ_m (−1)/(m(2m−1)) − γ/2 − (log π)/2 = (1/2)(−2log2)·(−1)?? Σ 1/(m(2m−1)) = 2log2 ✓ so (1/2)·(−2log2) − γ/2 − (log π)/2 = −log2 − γ/2 − (log π)/2 = −(2log2 + γ + log π)/2 = −(log4 + log π + γ)/2 = −(log 4π + γ)/2 = −a₁ ✓. And the s-dependent parts: (1/2)Σ_m [(s−1)/(m(2m+s−1)) + 1/(m(2m−1))] = Σ_{m odd} s/(m(m+s))?? — this is the identity to prove — a partial-fraction rearrangement: (s−1)/(m(2m+s−1)) + 1/(m(2m−1)) = [(s−1)(2m−1)·... common denom m(2m+s−1)(2m−1)... let me: = [(s−1)(2m−1) + (2m+s−1)]/(m(2m−1)(2m+s−1))·... hmm (1/2)·that sum = Σ_odd s/(m(m+s))?? The even/odd split: Σ_{m≥1} F(m) where F involves (2m−1) and (2m+s−1)... set n = 2m−1 (odd): Σ_{n odd ≥ 1} (1/2)·[(s−1)/( ((n+1)/2)·(n+s)) + 1/(((n+1)/2)·n)] = Σ_{n odd} [(s−1)/(n(n+s)) + 1/(n(n+1))] — so need Σ_{n odd} [(s−1)/(n(n+s)) + 1/(n(n+1))] = Σ_{n odd} s/(n(n+s)) ⟺ Σ_odd [1/(n(n+1))] = Σ_odd [s/(n(n+s)) − (s−1)/(n(n+s))] = Σ_odd 1/(n(n+s)) — so need Σ_{n odd ≥ 1} [1/(n(n+1)) − 1/(n(n+s))] = 0?? That's NOT zero... I must have mis-stepped. Let me just directly verify the coefficient identity at j = 1 numerically: τ₁ =? a₂ = (1−1/4)ζ(2) = (3/4)(π²/6) = π²/8 ≈ 1.2337; (−1)^{1+1}a₂ = +π²/8. And τ₁ = coefficient of s in ΓR′/ΓR(1+s) = (d/ds)|₀ ΓR′/ΓR(1+s) = (1/4)ψ′(1/2)·... ΓR′/ΓR(1+s) = −(log π)/2 + (1/2)ψ((1+s)/2); d/ds: (1/4)ψ′((1+s)/2); at 0: (1/4)ψ′(1/2) = (1/4)·(π²/2) (ψ′(1/2) = π²/2 — classical trigamma value) = π²/8 ✓✓. So τ₁ = π²/8 ✓ and ψ′(1/2) = π²/2 = Σ_{m≥0}(m+1/2)^{−2}·(−1)^{1+1}·1! = Σ (m+1/2)^{−2} = 4Σ(2m+1)^{−2} = 4·(π²/8) = π²/2 ✓ consistent with a₂ = Σ_{odd ≥ 1} m^{−2} = π²/8 ✓.\n\nSo no escape from the polygamma values for the per-k identity. The generating function identity is equivalent content.\n\nSo the remaining big rocks for ii′-3 via β4:\n(Rock-1) The moment contour identities (M): σ_k = −g^{(k−1)}(0)/(k−1)! for k ≥ 1. Sub-rocks: (i) rectangle residue for w^{−k}g (ppart port to 0 — moderate); (ii) R-bound horizontal decay (SHARED ii′-5 content — needs building: Borel–Carathéodory/Jensen/Blaschke chain — the D-064 R3 estimate said 2–3 sessions); (iii) vertical-line evaluations V(3) = 0-type (Euler-product logDeriv series + digamma growth + Jordan-on-rectangles — moderate); (iv) k=1 paired kernel + reflect/conj rearrangement (moderate).\n(Rock-2) The digamma series & polygamma at 1/2 (for τ_j, j ≥ 1): from BohrMollerup's logGammaSeq (real) + deriv-under-limit + iterated — moderate-heavy, self-contained real analysis. (Or possibly find another Mathlib backdoor — check for `Real.digamma` and polygamma once more.)\n\nHmm — Rock-1(ii) (the R-bound) being ii′-5's content means ii′-3 and ii′-5 SHARE the R-bound build. That's a significant dependency insight for the design note: maybe do the R-bound FIRST (it serves both)?\n\nHmm, wait — actually, let me reconsider whether (M) even needs the R-bound. The horizontal decay: |g(σ + iT)| for σ ∈ [−A, 3], T zero-avoiding: |g| = |ΓR′/ΓR + ζ′/ζ + 1/w + 1/(w−1)| — the ζ′/ζ piece needs the R-bound |ζ′/ζ(w) − Σ_{|γ−T|<1} 1/(w−ρ)| ≤ A log T + B₀ — the Σ over near zeros with the T-gap clearance δ: |Σ| ≤ (count)·(1/δ) ~ C₀ log T · C₀ log T = O(log²T) ✓. So yes the R-bound (the FULL D-056 statement) is needed. ii′-5 dependency confirmed. Alternatively — hmm — is there a weaker input? The classical Davenport approach for the horizontal bound uses exactly ζ′/ζ = Σ_{near} 1/(s−ρ) + O(log T) — the R-bound. No weaker path.\n\nBUT — actually — wait. For the MOMENT identity at k ≥ 2, there's the T-AVERAGED variant: instead of choosing a zero-avoiding T, integrate over T ∈ [T₀, T₀+1]: the pigeonhole picks a good T; the horizontal integrals with |g| ≤ C log²T·T^{−k} → 0. The R-bound is genuinely needed. OK.\n\nSo the ii′-3 design has a sequencing consequence: the R-bound (ii′-5/R3) is a SHARED prerequisite for the moment identities. Options:\n(a) Do the R-bound as part of ii′-3 (pull ii′-5's main content forward).\n(b) Reorder: ii′-4 (L3 zero-avoiding T + L1 kernel bounds) → ii′-5 (R-bound) → ii′-3 (needs R-bound) → ii′-6 → ii′-7.\nD-064's map had ii′-3 before 4/5 because the crux was thought to feed ii′-6's L0 assembly — but the ASSEMBLY needs ALL of them regardless; the order among 3/4/5 is flexible. Option (b) is attractive: ii′-4's L3 (zero-avoiding T via pigeonhole on the perimeter zero count) and L1 (kernel bounds |k_n| ≤ 2 etc.) are elementary; ii′-5 (R-bound) is the analytic core; ii′-3 then uses both. Hmm — but ii′-5's R-bound proof (D-056) itself needs the partial-fractions of ζ′/ζ — D-056's proof is via the reference-point trick + Borel–Carathéodory — self-contained per D-064 R3's inventory (Mathlib borelCaratheodory ✓, Jensen circleAverage ✓, Blaschke StrongPNTPrefix ✓, FE strip bound via riemannZeta_one_sub + Stirling, digamma Lemma D).\n\nWait — actually, D-056's R-bound proof — let me recall what it needs: |ζ′/ζ(w) − Σ_{|γ−t|<1} 1/(w−ρ)| ≤ A log(|t|+2) + B₀ for σ ∈ [−5/2, 4], |t| ≥ 10. The proof (D-056): reference-point trick — ζ′/ζ(w) − ζ′/ζ(2+it₀-ish)... via the partial fraction... hmm — the partial fractions of ζ′/ζ = B + Σ(1/(s−ρ)+1/ρ) − ... — THE HADAMARD PARTIAL FRACTION AGAIN?! D-056's R-bound proof — from session 009: \"reference-point R-bound PROVED (A = 10.5, B₀ = 48, honest C₀ incl. log log term)\" — its proof route: D-036 §0 — the Davenport Ch. 15 route: from the partial fractions?? If D-056's proof itself uses ζ′/ζ partial fractions (Hadamard content), then... D-064 R3 said \"D-056's proof uses partial fractions, but the same bound is provable by the Davenport-Ch.-15 local route... for which the machinery EXISTS: Mathlib Complex.borelCaratheodory, MeromorphicOn.circleAverage_log_norm (Jensen), and FromPNTPlus StrongPNTPrefix (BorelCaratheodoryDeriv, LogOfAnalyticFunction, Blaschke factors, ZerosBound)\" — the LOCAL route avoids partial fractions: on a disc around s₀ = 2+it, log ζ bounded via Borel–Carathéodory from the upper bound of ζ (strip bound) — then deriv bound via Blaschke/zero-counting. That's the R3 route — independent of Hadamard ✓. Good — so the R-bound does NOT depend on (M). And (M)'s proof via contour needs the R-bound. And the R-bound needs only the LOCAL machinery. ✓ No circularity.\n\nSo the design: REORDER to put the R-bound before the moments? The dependency: (M) needs [rectangles ✓ have] + [R-bound = ii′-5] + [vertical evaluations] + [FE ✓ Mathlib]. The archimedean piece (A) needs [digamma series from logGammaSeq — independent]. Piece B ✓ done. So ii′-3 splits naturally:\n- ii′-3a: piece A (archimedean τ-evaluation) — independent, self-contained.\n- ii′-3b: piece B formalization (the lcoeff reading at 1 — mostly done in LiResidue; need the coefficient-extraction packaging: hLi(1+s)/s etc.).\n- ii′-3c: piece C (the moment identities) — DEPENDS on the R-bound (ii′-5) + vertical evaluations.\n- ii′-3d: the (4.10) assembly.\n\nGiven the freeze and the size, the design note D-066 should record this architecture and recommend the reordered pipeline: ii′-3a (archimedean) can start immediately; ii′-3c slots after the R-bound.\n\nHmm — wait, actually, let me reconsider once more whether the vertical-line evaluations can be avoided. In the k ≥ 2 contour argument, I claimed V(3) = 0 by pushing right. The push-right argument needs: (i) no poles of w^{−k}g(w) with re > 1 ✓ (g's poles are ξ's zeros = ρ's, re < 1; the kernel's pole at 0); (ii) horizontal decay at ±T between re 3 and re A (direct Euler bound — need −ζ′/ζ's Dirichlet series: Mathlib: `logDeriv_riemannZeta_eq`? — there IS `riemannZeta_logDeriv_eq_...`? — hmm — need: for re s > 1: −ζ′/ζ(s) = Σ_n Λ(n)n^{−s} — Mathlib has this? `LSeries_vonMangoldt`...? I recall `riemannZeta_logDeriv...` not sure. Zeta23's MediumPNT/... uses prime-side line integrals — `prime_side_line` in WeilEF — they have the Euler-logDeriv series SOMEWHERE. Let me check quickly.); (iii) the line integrability of w^{−k}g(a+it) — needs |g(a+it)| = O(log|t|) for a ≥ 3 — the digamma growth bound + the ζ′/ζ bound ✓ via the series.\n\nSo the vertical evaluation needs the −ζ′/ζ Dirichlet series in Lean. Let me check Zeta23/Mathlib for it.","signature":""},{"type":"text","text":"The infrastructure picture is clear. Let me check two more pieces — the −ζ′/ζ Dirichlet series (for vertical-line evaluations) and how Zeta23 handles the prime-side line."},{"type":"tool_use","id":"Bash_177","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean\" && grep -rn \"logDeriv riemannZeta\\|logDeriv_zeta\\|vonMangoldt.*tsum\\|LSeries.*vonMangoldt\" Zeta23/FromPNTPlus/MediumPNT.lean Zeta23/WeilEF/Contour.lean 2>/dev/null | head -8; echo ===MATHLIB===; cd .lake/packages/mathlib && grep -rn \"theorem.*logDeriv_riemannZeta\\|riemannZeta.*logDeriv.*sum\\|neg_logDeriv\" Mathlib/NumberTheory/LSeries/RiemannZeta.lean Mathlib/NumberTheory/LSeries/VonMangoldt.lean 2>/dev/null | head -6","description":"Find the -ζ′/ζ Dirichlet series in Zeta23/Mathlib"},"extra_content":null}]