[{"type":"thinking","thinking":"Mathlib's `completedRiemannZeta₀` (Λ₀) is the ENTIRE function with Λ₀(s) = Λ(s) + 1/(s−1) − 1/s wherever defined — this is a DIFFERENT entire completion than ξ = (1/2)s(s−1)Λ! Λ₀ = Λ + 1/(s−1) − 1/s — the \"subtract the polar parts\" completion. And ξ = (1/2)s(s−1)·Λ. Both entire; different normalizations: ξ(0) = 1/2; Λ₀(0) = ? \n\nHmm — so the Lagarias ξ = (1/2)s(s−1)Λ is NOT directly a Mathlib object; but Λ₀ is, and entire ✓ (`differentiable_completedZeta₀` : entire ✓). The zeros of Λ₀ = zeros of ξ = nontrivial zeros ✓ (for s ∉ {0,1}: Λ₀ = Λ + (1/(s−1) − 1/s) = Λ − 1/(s(s−1))... hmm wait: 1/(s−1) − 1/s = (s − (s−1))/(s(s−1)) = 1/(s(s−1)). So Λ₀(s) = Λ(s) + 1/(s(s−1)). And ξ = (1/2)s(s−1)Λ = (1/2)s(s−1)(Λ₀ − 1/(s(s−1))) = (1/2)s(s−1)Λ₀ − 1/2. So ξ = (s(s−1)/2)·Λ₀ − 1/2. Zeros of ξ: (s(s−1)/2)Λ₀ = 1/2 ⟺ ... NOT the same as zeros of Λ₀ directly!? ξ(ρ) = 0 ⟺ (ρ(ρ−1)/2)Λ₀(ρ) = 1/2 — hmm that's not Λ₀(ρ) = 0. WAIT — that's wrong: ξ = (1/2)s(s−1)Λ and Λ₀ = Λ + 1/(s(s−1)): at a zero ρ of ζ (nontrivial): Λ(ρ) = ΓR(ρ)·ζ(ρ) = 0 ✓ so Λ₀(ρ) = 0 + 1/(ρ(ρ−1)) ≠ 0?!?! That can't be right — Λ₀ is supposed to be entire with the same zeros... no wait: Λ₀ = Λ + 1/(s−1) − 1/s: at a nontrivial zero ρ: Λ(ρ) = 0 (Gamma finite nonzero at ρ ✓ ζ(ρ) = 0) so Λ₀(ρ) = 0 + 1/(ρ−1) − 1/ρ = 1/(ρ(ρ−1))·... = (ρ − (ρ−1))/(ρ(ρ−1)) = 1/(ρ(ρ−1)) ≠ 0. So Λ₀(ρ) ≠ 0!!! So Λ₀'s zeros are NOT the nontrivial zeros of ζ!! Λ₀ is entire but its zero set differs. Hmm wait — that contradicts \"completedRiemannZeta₀ the entire function\" being the useful completion... Let me recompute: Λ₀(s) = Λ(s) + 1/(s−1) − 1/s. Λ(ρ) = ΓR(ρ)ζ(ρ) — at a nontrivial zero ρ (0 < re < 1): ΓR(ρ) finite nonzero (ΓR poles at 0,−2,−4,... ✓ ρ not there) and ζ(ρ) = 0 ⟹ Λ(ρ) = 0 ✓. Then Λ₀(ρ) = 0 + 1/(ρ−1) − 1/ρ = [ρ − (ρ−1)]/(ρ(ρ−1)) = 1/(ρ(ρ−1)) — nonzero ✓. So YES Λ₀(ρ) ≠ 0 — Λ₀ has DIFFERENT zeros than ξ. Wait — that means Mathlib's Λ₀ ≠ (1/2)s(s−1)Λ and its zeros are shifted. Hmm — that makes Λ₀ the WRONG object for us!?\n\nHold on — let me recompute what Λ₀ is: \"Λ₀(s) = Λ(s) + 1/(s−1) − 1/s\". Is this entire? Λ has poles at 0 (residue −1) and 1 (residue +1). 1/(s−1) has pole at 1 with residue +1; −1/s has pole at 0 with residue −1. So Λ₀ = Λ + 1/(s−1) − 1/s at 1: residue 1 + 1 = 2?!? That's not cancelled! Hmm — wait — Λ's residue at 1 is +1 (completedRiemannZeta_residue_one ✓); adding 1/(s−1) (residue +1) gives residue 2 — NOT entire at 1?? That contradicts \"differentiable_completedZeta₀ : entire\". Let me recheck the sign: maybe it's Λ₀ = Λ − 1/(s−1) + 1/s? The doc says \"Λ₀(s) = Λ(s) + 1/(s − 1) − 1/s\". Λ at 1: residue +1. 1/(s−1): residue +1. Sum residue +2. That's NOT holomorphic at 1. Contradiction with the claimed entireness — so either Λ's residue at 1 is −1 in Mathlib's convention... completedRiemannZeta_residue_one : Tendsto (fun s ↦ (s − 1) * completedRiemannZeta s) (𝓝[≠] 1) (𝓝 1) — residue +1 at 1. And at 0: residue? (s·Λ(s) → ? at 0) — Λ(s) = ΓR(s)ζ(s): ΓR(s) ~ 2/s·π^0... Γ(s/2) ~ 2/s so ΓR(s) ~ 2/s, ζ(0) = −1/2: s·Λ(s) → 2·(−1/2) = −1 ✓ residue −1 at 0. So Λ + 1/(s−1) − 1/s: at 1: +1 +1 = 2 — NOT holomorphic. UNLESS the doc has the sign flipped and the real def is Λ₀ = Λ − 1/(s−1) + 1/s: at 1: +1 −1 = 0 ✓; at 0: −1 + 1 = 0 ✓ ENTIRE ✓. So probably the actual relation is Λ₀(s) = Λ(s) − 1/(s−1) + 1/s (doc typo or my misreading — line 86 shows: completedRiemannZeta s = completedRiemannZeta₀ s − 1/s − 1/(1−s) — so Λ = Λ₀ − 1/s − 1/(1−s) = Λ₀ − 1/s + 1/(s−1) — so Λ₀ = Λ + 1/s − 1/(s−1) — at 0: Λ residue −1 plus 1/s residue +1 → 0 ✓; at 1: +1 −1 = 0 ✓ ENTIRE ✓. OK so Λ₀ = Λ + 1/s − 1/(s−1) (the line-86 display is authoritative: Λ = Λ₀ − 1/s − 1/(1−s)).\n\nThen at a nontrivial zero ρ: Λ₀(ρ) = 0 + 1/ρ − 1/(ρ−1) = [(ρ−1) − ρ]/(ρ(ρ−1)) = −1/(ρ(ρ−1)) ≠ 0. STILL not vanishing at the ρ's!! So Λ₀'s zeros ≠ ζ's nontrivial zeros. Hmm!! So Mathlib's Λ₀ is the entire function that is NOT ξ. That's the \"subtract polar parts\" completion — its zeros are genuinely different.\n\nLet me double-check with a value: Λ₀(1/2) = Λ(1/2) + 2 − (−2)... = Λ(1/2) + 4: Λ(1/2) = π^{−1/4}Γ(1/4)ζ(1/2) ≈ (0.751)(3.626)(−1.460) ≈ −3.98; Λ₀(1/2) ≈ 0.02?? Hmm that gives a near-zero at 1/2 — suspicious. Whatever — the KEY question: which entire function does Zeta23 use for the zero machinery? CountByIntegral.lean:66 said `completedRiemannZeta s = 0 ↔ IsNontrivialZero s` — for Λ (the non-entire one) ✓ — its zeros (where defined) = nontrivial zeros ✓. So Zeta23's counting works with Λ (poles at 0,1 included in the argument principle via the of_poles theorem ✓ that's why rectangleIntegral'_mul_logDeriv_of_poles exists with P = {0,1}!). \n\nFor MY purposes: the ξ function = (1/2)s(s−1)Λ(s) — I can DEFINE it: `xiLagarias s := (s * (s - 1)) / 2 * completedRiemannZeta s` — entire? s(s−1)/2·Λ: at 0: (s(s−1)/2)·Λ(s) → (1/2)(−1)·(−1) = 1/2 ✓ (removable); at 1: (1/2)(1)(0)·... s(s−1)/2 → 0 and Λ has a simple pole — product → (1/2)·1·(s−1)Λ(s) → (1/2)(1)(1) = 1/2 ✓ removable. So xiLagarias extends to an entire function with the update trick (same as zetaA) — need to PROVE entireness (removable singularities at 0, 1 — same machinery as zetaA_analyticAt_one ✓ we have the pattern). Its zeros: for s ∉ {0,1}: xiLagarias s = 0 ⟺ Λ(s) = 0 ⟺ IsNontrivialZero s (Zeta23 ✓); at 0,1: value 1/2 ≠ 0 ✓. FE: xiLagarias(1−s) = ((1−s)(−s)/2)Λ(1−s) = (s(s−1)/2)Λ(s) = xiLagarias(s) ✓ from completedRiemannZeta_one_sub ✓ EASY.\n\nSo define `xiL` (or reuse a name) := (s(s−1)/2)·completedRiemannZeta with updates at 0,1. Then:\n- (4.2)-decomposition: logDeriv xiL (1+s) = 1/(1+s) + 1/s + ΓR′/ΓR(1+s) + ζ′/ζ(1+s) — wait: logDeriv of s(s−1)/2·Λ: Λ = ΓR·ζ: logDeriv Λ = logDeriv ΓR + logDeriv ζ (where nonvanishing ✓); logDeriv (s(s−1)/2) = 1/s + 1/(s−1) ✓. At 1+s: 1/(1+s) + 1/s ✓✓.\n- FE: xiL(1−s) = xiL(s) ✓.\n- xiL(0) = xiL(1) = 1/2 (via the residue lemmas: (s−1)Λ(s) → 1 at 1 ✓ Mathlib has completedRiemannZeta_residue_one; at 0: s·Λ(s) → −1 — is `completedRiemannZeta_residue_zero` in Mathlib? — hmm — need s·Λ(s) → −1 at 0. From the FE: Λ(1−s) = Λ(s): s·Λ(s) at 0: −s·Λ(1−s)·... let u = 1−s: s·Λ(s) = (1−u)·Λ(u) → as u → 1: (1−u)Λ(u) = −(u−1)Λ(u) → −1 ✓ via residue_one transported ✓ provable.)\n\nSo piece C's contour works on xiL with:\n- zeros = {IsNontrivialZero} ✓ (Zeta23's CountByIntegral for Λ + the factor nonvanishing at 0,1).\n- g := logDeriv xiL — poles exactly at the ρ's with residue = mult ✓ (zeros of xiL of order = analyticOrderAt ζ ρ... — order transfer: xiL = (s(s−1)/2)·Λ, factor nonzero at ρ ⟹ same order ✓; Λ = ΓR·ζ with ΓR(ρ) ≠ 0 ⟹ order = order of ζ at ρ ✓ = zeroMult ρ ✓).\n\nOK. Now — the estimate for the R-bound and vertical decay for g = logDeriv xiL: logDeriv xiL = 1/s + 1/(s−1) + logDeriv ΓR + logDeriv ζ — the trivial pieces explicit ✓; logDeriv ΓR = −(log π)/2 + (1/2)ψ(s/2) — the digamma growth |ψ(s/2)| = O(log|s|) for re s ≥ 3 — needs the digamma growth bound — from the series (Rock-2) or Stirling. And logDeriv ζ's R-bound (ii′-5 content). So same dependencies as mapped.\n\nAlright — I now have a COMPLETE architecture. Let me also quickly reconsider the k=1 case's reflect-pair rearrangement and confirm sigmaP 1 = −ξ′/ξ(0) via the kernel K(w) = 1/(2w(1−w))·... wait — earlier I derived: Σ_ρ mult/(2ρ(1−ρ)) = −g(0) where the sum is absolutely convergent ✓. And sigmaP 1 = Σ mult·Re(1/ρ) = Σ mult·re/|ρ|². And Σ mult/(2ρ(1−ρ)) = Σ mult·re/|ρ|² via the reindex: shown earlier ✓ (both equal (1/2)Σ mult(re/|ρ|² + (1−re)/|1−ρ|²)... let me redo: Σ mult/(2ρ(1−ρ)) — take its REAL part: Re[1/(2ρ(1−ρ))] — the sum is real (conj-invariant) so = Σ mult·Re[1/(2ρ(1−ρ))] = Σ mult·(1/2)[re/|ρ|² + Re(1/(1−ρ))]... 1/(2ρ(1−ρ)) = (1/2)(1/ρ + 1/(1−ρ)) ✓; Re(1/(1−ρ)) = (1−re)/|1−ρ|² ✓. Σ mult·(1/2)(re/|ρ|² + (1−re)/|1−ρ|²) = (1/2)Σ mult·re/|ρ|² + (1/2)Σ mult·(1−re)/|1−ρ|² — the second sum reindex ρ ↦ 1−ρ (bijection on zeros with mult preservation — need the mult-preservation under ρ ↦ 1−ρ: reflect (1−ρ̄) mult ✓ (Zeta23 seam mult_reflect) and conj mult ✓ (need: zeroMult (conj ρ) = zeroMult ρ — the conj mult-preservation — hmm is that in the seam? The seam has reflect_zero/mult_reflect for reflect ρ = 1 − conj ρ. Conj: IsNontrivialZero (conj ρ) ✓ (zeta_reflect... — from ii′-1a's liSummand work — did they need conj invariance? The PAIRED liSummand doesn't need invariance (it's a symmetric sum by construction). Hmm — for the reindex ρ ↦ 1−ρ = reflect(conj ρ): need mult(conj ρ) = mult(ρ): analyticOrderAt ζ (conj ρ) = analyticOrderAt ζ ρ — from ζ(conj s) = conj ζ(s) (Mathlib: `riemannZeta_conj`? `Complex... ` — Mathlib: riemannZeta (conj s) = conj (riemannZeta s) — I think `riemannZeta_conj` exists? or via `Complex.conj` map — let me assume findable) ⟹ orders equal (analyticOrderAt under conj — provable via the NF: if ζ = (s−ρ)^m h near ρ then ζ(conj...)... — moderate but fine).\nThen Σ_ρ mult(ρ)(1−re(ρ))/|1−ρ|² = Σ_{ρ'} mult(1−ρ')·re(ρ')/|ρ'|² [1−re(1−ρ') = re(ρ') ✓] = Σ mult(ρ')·re(ρ')/|ρ'|² ✓. So the reflect-paired sum = (1/2)Σ + (1/2)Σ = Σ mult·re/|ρ|² = sigmaP 1 ✓ — as REAL numbers (sigmaP 1 is real-valued as a complex number — the identity is between ℂ values: Σ mult/(2ρ(1−ρ)) is ℂ; sigmaP 1 is ℂ with zero im part — the equality: Re(Σ mult/(2ρ(1−ρ))) = sigmaP 1 and Im = 0 by conj symmetry... — hmm the contour gives the ℂ sum Σ mult/(2ρ(1−ρ)) = −g(0) which is... g(0) = ξ′/ξ(0) — REAL? ξ is real on the real axis (Λ of real = real ✓ via conj-reflection) so g(0) real ✓. So the ℂ identity Σ mult/(2ρ(1−ρ)) = −g(0) ∈ ℝ forces the sum to be real ✓ consistent. And sigmaP 1 = the same real number via the rearrangement ✓.\n\nHmm wait — one more check on this: sigmaP 1 = Σ mult·re/|ρ|² — as a ℂ it's Σ (mult/2)(1/ρ + 1/ρ̄) — my PROVED form (LiSwaps). And liCoeff_eq_sum_sigma uses sigmaP j. So the crux needs sigmaP 1 = 1 + γ/2 − ½log4π eventually (through the a-form (4.10)) ✓ consistent with the contour value −g(0) = −ξ′/ξ(0) = 1 − c₀ − a₁... — as computed: σ₁ = 1 − c₀ + τ₀ = 1 − c₀ − a₁ ✓ and with c₀ = −γ, a₁ = (log4π+γ)/2: 1 + γ − (log4π+γ)/2 = 1 + γ/2 − (log4π)/2 ✓✓.\n\nBUT — hmm — for the k=1 case of (M), the contour gives sigmaP 1 = −g(0) DIRECTLY (not via (4.10)) — and the (4.10)-a-form at k=1 is c₀ = 1 − a₁ − σ₁ ⟺ σ₁ = 1 − a₁ − c₀ — and from the coefficient split: σ₁ = −g(0) = g(1)·... = 1 − c₀ + τ₀. So with τ₀ = −a₁ (the digamma_one_half evaluation): consistent ✓. So the final assembly uses (M) for all k ≥ 1 and the τ-evaluation for all j ≥ 0 — no circularity: (M) is proved by contour; τ's by digamma work; the coefficient split is algebra + (B) ✓.\n\nNOW — the dependency on the R-bound (ii′-5): the horizontal decay for the contour limits. Let me look at exactly what's needed: for the T → ∞ limit with zero-avoiding T (Trudgian pigeonhole — perimeter): the bound |g(σ + iT)| ≤ C·log²T for σ ∈ [−5/2, 4] (R-zone) — via D-056's R-bound for ζ′/ζ + digamma growth + trivial pieces. The R-bound's Lean proof (D-064 R3, 2–3 sessions estimate) is the big shared rock. \n\nDECISION POINT for the design note — three options for ii′-3 sequencing:\n(α) ii′-3 first with the R-bound built inside it (merging ii′-5's main content).\n(β) Reorder: ii′-4 (L3+L1 elementary) → ii′-5 (R-bound) → ii′-3 (moments + archimedean + assembly) → ii′-6 → ii′-7.\n(γ) ii′-3a (archimedean piece — independent of R-bound) first, then ii′-4, ii′-5, then ii′-3bc.\n\nAlso NOTE: ii′-6's L0 assembly (the sides identity + bridge |λ_n(T)| ≤ 2FAlt + |Sf| ≤ Bn) uses rectInt'_Jlag (✓ done) + the crux (ii′-3) + the R-bound for the sides estimates (ii′-5) + L3/L1 (ii′-4). So the R-bound is needed by BOTH ii′-3 and ii′-6 — building it as ii′-5 BEFORE ii′-3 (option β/γ) is the natural order. And ii′-4 (L3 zero-avoiding T) is also needed by both.\n\nSo my recommendation: **option (β/γ)**: next sub-stage = ii′-3a (archimedean τ-evaluation — self-contained, no contour dependencies) OR ii′-4. Since ii′-3a is self-contained real/complex analysis (digamma series from logGammaSeq + coefficient extraction + the odd-series reindexing), and ii′-4 is elementary (pigeonhole on the perimeter N(T) + kernel bounds), either can go first. Actually — per D-064's original order ii′-3 was flagged as long pole; doing ii′-3a now keeps momentum on the pole while the contour pieces queue.\n\nHmm — wait, actually, let me reconsider the digamma-series build once more, because THAT's also a nontrivial rock. The needed facts:\n(A-i) For real x > 0: ψ̃(x) := (log Γ)'(x) = −γ − 1/x + Σ_{m≥1} (1/m − 1/(x+m))... — do I even need the REAL digamma as a separate object? What I need: the COMPLEX Taylor coefficients of ΓR′/ΓR(1+s) at s = 0. Alternative path avoiding ψ series: the ΓR logDeriv as a MEROMORPHIC function has a partial-fraction expansion: ΓR′/ΓR(w) = −(log π)/2 + (1/2)ψ(w/2) and ψ(w) = −γ + Σ_{m≥1}(1/m − 1/(w−1+m))·... — the partial fraction series of ψ — the DIRECT complex build: from the Weierstrass product of 1/Γ: 1/Γ(w) = w e^{γw} Π(1+w/m)e^{−w/m} — NOT in Mathlib (no Weierstrass for Gamma).\n\nHmm — so the digamma series must be built from logGammaSeq (BohrMollerup — REAL). The route: \n- logGammaSeq x n = x log n + log(n!) − Σ_{m=0}^n log(x+m) (real x > 0) — Mathlib HAS: tendsto_log_gamma : Tendsto (logGammaSeq x) atTop (𝓝 (log (Real.Gamma x))) ✓ (line 293).\n- Define ψ_real x := deriv (Real.log ∘ Real.Gamma) x (or deriv (fun x => Real.log (Real.Gamma x)) x). Need: Real.Gamma differentiable on (0,∞) ✓ (`Real.differentiableAt_Gamma`? exists probably) and Real.Gamma x ≠ 0 for x > 0 ✓ (Real.Gamma_pos... `Real.Gamma_pos_of_pos`?).\n- The deriv-under-limit: logGammaSeq' x n = log n − Σ_{m=0}^n 1/(x+m) — converges to ψ_real(x) — the interchange: uniform convergence of the derivative sequence on compacts + pointwise convergence of logGammaSeq — Mathlib real: `Tendsto.deriv`? there's `tendsto_deriv`? For real: `hasDerivAt_of_tendsto_locally_uniform...`? There IS `tendsto_locally_uniform...deriv`? For ℝ: `deriv` of a locally uniform limit: hmm — the complex version exists (TendstoLocallyUniformlyOn.differentiableOn is for ℂ); for ℝ there's `TendstoLocallyUniformly.hasDerivAt`? Let me think — Mathlib real: `hasDerivAt_of_tendstoLocallyUniformlyOn`? or via the FTC route: uniform limit of derivatives + pointwise limit ⟹ deriv limit — `tendsto_deriv_of_...`? There are lemmas like `hasDerivAt_of_tendsto_locally_uniform` (one variable, real) — I believe something usable exists (`tendsto_locally_uniformly_on...`). And for the ITERATED derivatives: apply the same j times (each derivative series uniformly convergent by M-test ✓).\n- Then ψ_real^{(j)}(1/2) = (−1)^{j+1}j!Σ_{m≥0}(1/2+m)^{−(j+1)} — by termwise j-fold derivation of the series −γ − 1/x + Σ_m(1/m − 1/(x+m)) — hmm wait the series form: log n − Σ_{m=0}^n 1/(x+m) = log n − H_n + Σ_{m=1}^n (1/m − 1/(x+m)) − 1/x — limit: −γ + Σ_{m≥1}(1/m − 1/(x+m)) − 1/x. Termwise j-deriv (j ≥ 1): the −γ vanishes; Σ_m (−1)^{j+1}j!/(x+m)^{j+1} + (−1)^{j+1}j!/x^{j+1}·... = (−1)^{j+1}j! Σ_{m≥0}(x+m)^{−(j+1)} ✓.\n- Then the complex-analytic bridge: iteratedDeriv of the COMPLEX ΓR′/ΓR(1+·) at 0 = the real-line derivatives: the complex function F(s) := ΓR′/ΓR(1+s) is analytic near 0; its restriction to the real line near 0: F(↑r) = −(log π)/2 + (1/2)·digamma(↑((1+r)/2)) — and digamma(↑x) = ↑(ψ_real x)? — digamma = logDeriv Complex.Gamma; Complex.Gamma ↑x = ↑(Real.Gamma x) (`Complex.Gamma_ofReal`? need the name — probably `Complex.Gamma_ofReal` exists? or `Complex.ofReal_Gamma`) — then deriv of the composition... — the relation iteratedDeriv j F 0 (complex) vs iteratedDeriv j (F∘ofReal) 0 (real→complex function's iteratedDeriv): `Complex.iteratedDeriv_ofReal...`? There's `iteratedDeriv_comp_...`? For ofReal: deriv (F ∘ ofReal) x = deriv F (x) · 1 — via HasDerivAt.comp with ofRealCLM (LiPrincipal used Complex.ofRealCLM.hasDerivAt ✓!). Iterated: a small induction or a comp lemma. MODERATE fiddliness.\n\nOK — it's all doable; the digamma piece (piece A) is maybe 1.5–2 sessions of focused Lean. \n\nFINAL DESIGN for D-066. Let me also reconsider — is there any way to AVOID the R-bound for the moments? ... The k ≥ 2 horizontal decay needs |g(σ±iT)| = O(T^θ) with θ < k−1 — i.e. O(T) suffices for k ≥ 3, O(1) for k = 2 — the R-bound gives O(log²T) which is plenty. Weaker alternatives? |ζ′/ζ(σ+iT)| = O(T^ε) on zero-avoiding lines — any proof needs the zero-count + the partial-fraction-OR-Borel–Carathéodory input. The Borel–Carathéodory route (D-064 R3) is the Mathlib-supported one. It's ~2–3 sessions as estimated. It serves ii′-3c AND ii′-6. Fine.\n\nActually — hmm, ONE more thought on avoiding the R-bound for (M): the contour identity for the moment σ_k — Lagarias's generating identity −ξ′/ξ(s) = Σ σ_{m+1}s^m is REALLY equivalent to the FULL product — but wait, there's a subtlety: is it? (M) at 0 only uses values/derivatives AT 0. The Taylor coefficients of g at 0 are determined by the germ. And σ_k are global sums. The identity links global (zeros) to local (germ at 0) — that's precisely what contour integration does. The contour proof I sketched IS the proof. The R-bound is the price of the horizontal segments. No way around it. Confirmed.\n\nHmm — although — actually, let me double-check the horizontal-decay need: k ≥ 2 with kernel w^{−k}: the top side ∫_{−A}^{3} (σ+iT)^{−k} g(σ+iT) dσ — with |g| ≤ C log²T (R-bound zone) — the integral ≤ C·log²T·T^{−k}·(A+3) → 0 ✓ for k ≥ 2 as T → ∞ with A FIXED. Then A → ∞. Yes the R-bound is used only for σ ∈ [−5/2, 4]; outside via direct bounds. ✓.\n\nFor k = 1's kernel 1/(2w(1−w)): top side ≤ C log²T·T^{−2}·(A+3) → 0 ✓ same.\n\nOK — one more sanity check on the D-064 scope estimate: ii′-3 was estimated 2–4 sessions (R2(iii)). With the full inventory:\n- Piece A (archimedean τ's): ~1.5 sessions (digamma series build + coefficient extraction + reindexing + j=0 via digamma_one_half).\n- Piece B (lcoeff reading): ~0.3 session (mostly done; coefficient-extraction packaging).\n- Piece C (moments via contour): needs the R-bound first (ii′-5 content, 2–3 sessions per D-064) + vertical evaluations (~0.5–1) + the rectangle residue for w^{−k}g (ppart port ~0.5) + k=1 kernel + rearrangement (~0.5).\n- Piece D (assembly (4.10)-a-form): ~0.3.\n\nSo the honest sequencing: ii′-3a (pieces A+B) → ii′-4 (L3+L1) → ii′-5 (R-bound, ALSO serving ii′-6) → ii′-3b (piece C moments) → ii′-3c (piece D assembly) → ii′-6 → ii′-7. This KEEPS D-064's sub-stage granularity and just inserts the moment work after the R-bound. The reordering is justified by the shared R-bound dependency.\n\nHmm — wait, actually, let me reconsider once more whether to put piece A before or after ii′-4/ii′-5. Piece A is independent and self-contained — doing it next session keeps ii′-3 moving and is lower-risk than the R-bound. But ii′-4 is SHORT (1 session) and elementary. Either order works. My recommendation in the design note: do ii′-3a (Piece A+B) next — it's the part of the long pole that needs no contour machinery.\n\nHmm, hold on — actually wait. Let me reconsider the possibility of avoiding the digamma series build for Piece A. The claim: for j ≥ 1, Taylor coefficient of s^j of ΓR′/ΓR(1+s) at 0 = (−1)^{j+1} a_{j+1}. \n\nWhat if I use the FUNCTIONAL EQUATION of ΓR + the recurrence instead? ΓR(s+2) = ΓR(s)·s/(2π) (Gammaℝ_add_two ✓ saw it in Deligne.lean:55!). So ΓR′/ΓR(s+2) = ΓR′/ΓR(s) + 1/s. Iterating: ΓR′/ΓR(s) = ΓR′/ΓR(s+2N) − Σ_{j=0}^{N−1} 1/(s+2j)... The asymptotic of ΓR′/ΓR(s+2N) as N → ∞: (1/2)ψ((s+2N)/2) − (log π)/2 ~ (1/2)log(N) — hmm the asymptotic of ψ at infinity — ψ(z) ~ log z — needs Stirling for the complex Gamma — Mathlib: `Complex.Gamma` Stirling? There's `Complex.Gamma_stirling`? hmm — I recall Mathlib has Stirling's formula for the complex Gamma function: `Complex.tendsto_...`? Let me check for Stirling in Mathlib quickly. If the ψ-asymptotic is available, then: ψ(w/2) = ψ((w+2N)/2) − Σ_{j<N} 2/(w+2j)·... — take the Taylor coefficient at w near 2... — ψ(1+s) = ψ(1+s+2N) − Σ_{j=0}^{N−1} 2/(1+s+2j+...): as N → ∞, ψ(1+s+2N) = log(2N) + o(1) — the constant-in-s part diverges but the TAYLOR COEFFICIENTS at order ≥ 1 converge: coefficient of s^j (j ≥ 1) in −Σ_{j'=0}^{N−1} 2/(1+s+2j'+...)·... = −Σ_{j'=0}^{N−1} 2·(−1)^j/(2j'+2)^{j+1}·... 1/(1+s+2j') = (1/(2j'+1))·1/(1 + s/(2j'+1)) = Σ_j (−1)^j s^j/(2j'+1)^{j+1} — so coefficient of s^j in −Σ_{j'} 2/(1+s+2j')·(1/2)·... — wait I need to be careful with factors. ΓR′/ΓR(1+s) = −(log π)/2 + (1/2)ψ((1+s)/2). Hmm the recurrence for ψ: ψ(z+1) = ψ(z) + 1/z (digamma_apply_add_one ✓ Mathlib!). So ψ((1+s)/2) = ψ((1+s)/2 + N) − Σ_{j'=0}^{N−1} 1/((1+s)/2 + j') = ψ((1+s)/2 + N) − Σ_{j'} 2/(1+s+2j'). Coefficient of s^j (j ≥ 1) in −Σ_{j'=0}^{N−1} 2/(1+s+2j'): 1/(1+s+2j') = 1/(1+2j')·1/(1 + s/(1+2j')) = Σ_j (−s)^j/(1+2j')^{j+1}: coefficient: −2·(−1)^j/(1+2j')^{j+1} = 2(−1)^{j+1}/(2j'+1)^{j+1}. Sum over j' = 0..N−1: 2(−1)^{j+1} Σ_{j'=0}^{N−1} (2j'+1)^{−(j+1)} → 2(−1)^{j+1}·(odd sum) = 2(−1)^{j+1}·lagariasA(j+1) as N → ∞ ✓!! And the ψ((1+s)/2+N) term: its j-th derivative at s = 0 for j ≥ 1: (1/2)^j ψ^{(j)}(1/2 + N)·... → 0 as N → ∞ IF ψ^{(j)}(x) → 0 as x → ∞ (real) — ψ'(x) ~ 1/x → 0 ✓ higher: ψ^{(j)}(x) ~ (−1)^{j+1}(j−1)!/x^j-ish → 0 ✓ — the asymptotic needed: ψ^{(j)}(x) → 0 as x → ∞ for j ≥ 1 — from... the digamma asymptotic ψ(x) = log x − 1/(2x) + O(1/x²) and derivatives — needs SOME asymptotic — hmm — OR: bound ψ^{(j)}(1/2+N) via the series I don't have... circular again? NO — via the recurrence itself: ψ^{(j)}(1/2+N) = ψ^{(j)}(1/2) + Σ... no. Hmm — the decay ψ^{(j)}(x) → 0: from ψ(x) = log x + O(1) (Mathlib? `Real.digamma`... does Mathlib even have Real.digamma?). Hmm.\n\nOK — but actually this recurrence route still needs ψ^{(j)} asymptotics. The cleanest remains the series. Fine — the series build it is: from logGammaSeq. Actually — hold on, let me check: does Mathlib have `Real.digamma` or digamma's series somewhere unexpected? Let me do one final check for digamma series/asymptotics, then write the design note.","signature":""},{"type":"text","text":"Let me do a final check for digamma series/asymptotics and Stirling availability, then write the design note."},{"type":"tool_use","id":"Bash_182","name":"Bash","input":{"command":"cd \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib\" && grep -rn \"Real.digamma\\|tendsto.*digamma\\|digamma.*tendsto\" Mathlib/ --include=\"*.lean\" | head -6; echo ===STIRLING===; grep -rln \"stirling\\|Stirling\" Mathlib/Analysis/SpecialFunctions/Gamma/ Mathlib/Analysis/Complex/ 2>/dev/null | head -4; echo ===LOGGAMMASEQ===; grep -n \"def logGammaSeq\\|theorem tendsto_log_gamma\" Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean","description":"Final checks: digamma asymptotics, Stirling, logGammaSeq"},"extra_content":null}]