[{"type":"thinking","thinking":"I have the capstone. Now, the ii′-5d target (from D-067 §3 and §6):\n\n**Target theorem:** for s with s.im = t, re s ∈ [−5/2, 1/2], |t| ≥ 10, ζ s ≠ 0:\n  ‖logDeriv riemannZeta s − Σ_{ρ ∈ nearZeros t} (zeroMult ρ)/(s−ρ)‖ ≤ C·(log|t|)² (some loose constant, e.g. 200000 or 300000·(log|t|)², folding).\n\nProof plan:\n1. FE logDeriv identity: ζ′/ζ(s) = −ζ′/ζ(1−s) − [logDeriv ΓR(1−s) + logDeriv ΓR(s)].\n\nDerivation: Λ(s) = ΓR(s)·ζ(s) and Λ(1−s) = Λ(s). So logDeriv Λ(s) = logDeriv ΓR(s) + logDeriv ζ(s). Also Λ(s) = Λ(1−s), so logDeriv Λ(s) = −logDeriv Λ(1−s) (chain rule: deriv of s ↦ Λ(1−s) is −Λ′(1−s)).\n\nThus logDeriv ΓR(s) + logDeriv ζ(s) = −[logDeriv ΓR(1−s) + logDeriv ζ(1−s)]\n⟹ logDeriv ζ(s) = −logDeriv ζ(1−s) − logDeriv ΓR(s) − logDeriv ΓR(1−s). ✓\n\nIn Lean: take logDeriv of both sides of completedRiemannZeta_eq_Gammaℝ_mul: at points where things are nonzero and differentiable. logDeriv (f·g) s = logDeriv f s + logDeriv g s when f s ≠ 0, g s ≠ 0, both differentiable at s.\n\nConditions for s in our region (re s ∈ [−5/2, 1/2], s.im = t, |t| ≥ 10, ζ s ≠ 0):\n- s ≠ 0 ✓ (|im| ≥ 10)\n- ΓR(s) ≠ 0: ΓR zeros are at −2n (n ≥ 0)? Gammaℝ_eq_zero_iff says ΓR(s) = 0 ↔ ∃ n, s = −2n. Our s has im = t ≠ 0, so not a negative even integer. ✓\n- ζ(s) ≠ 0 ✓ hypothesis\n- Differentiability of ΓR at s: Complex.differentiableAt_Gammaℝ? Need to check. In Mathlib/Zeta23: differentiableAt completedZeta (s ≠ 0, s ≠ 1). For Gammaℝ: it should be differentiable everywhere (it's entire? No — ΓR(s) = π^{−s/2}Γ(s/2) has poles at −2n). At our s (im ≠ 0), differentiable. Let me check what Zeta23/Mathlib provides. `differentiableAt_Gammaℝ`? I saw `Complex.Gammaℝ_ne_zero_of_re_pos` and `Complex.Gammaℝ_eq_zero_iff`. Need differentiability. Probably `differentiableAt_Gammaℝ` exists in Mathlib (Mathlib.Analysis.SpecialFunctions.Gamma.Basic?). Actually Complex.Gammaℝ differentiability — Zeta23 uses `hd.div hA.differentiableOn ...` in logDeriv_Gammaℝ_differentiableOn with some differentiability. Let me search later.\n\n- For 1−s: re(1−s) ∈ [1/2, 7/2], im(1−s) = −t. ζ(1−s) ≠ 0: since Λ(1−s) = Λ(s) = ΓR(s)ζ(s) ≠ 0... wait: Λ(1−s) = Λ(s) (completedRiemannZeta_one_sub — Mathlib, for all s). And Λ(s) = ΓR(s)·ζ(s) ≠ 0 (both factors nonzero). So Λ(1−s) ≠ 0, and Λ(1−s) = ΓR(1−s)·ζ(1−s) (needs 1−s ≠ 0 ✓ and ΓR(1−s) ≠ 0: re(1−s) > 0 so by Gammaℝ_ne_zero_of_re_pos ✓). Hence ζ(1−s) ≠ 0. ✓\n\n2. The right-half bound applies at s′ = 1−s with t′ = −t: re(s′) ∈ [1/2, 7/2] ⟺ re(s) ∈ [−5/2, 1/2] ✓; im(s′) = −t, |−t| = |t| ≥ 10 ✓; ζ(s′) ≠ 0 ✓. So:\n  ‖logDeriv ζ(1−s) − Σ_{ρ′ ∈ nearZeros(−t)} m(ρ′)/(1−s−ρ′)‖ ≤ 100000·(log|t|)².\n\n3. Zero-sum cancellation: \n  Σ_{ρ′ ∈ nearZeros(−t)} m(ρ′)/(1−s−ρ′) = −Σ_{ρ ∈ nearZeros(t)} m(ρ)/(s−ρ).\n  \n  Via the map ρ ↦ 1−ρ : nearZeros(t) → nearZeros(−t):\n  - well-defined: ρ ∈ nearZeros(t) ⟹ ζ(ρ) = 0, 0 < re ρ < 1 (nontrivial), |im ρ − t| < 1. Then 1−ρ: ζ(1−ρ) = 0 (analyticOrderAt_zeta_one_sub gives order preserved ≥ 1... actually need to derive ζ(1−ρ) = 0; simpler: IsNontrivialZero (1−ρ) — Zeta23 might have a lemma. zeta_reflect_zero is for reflect ρ = 1 − conj ρ. Hmm, I need 1−ρ not 1−conj ρ.\n  \n  Wait. Let me reconsider. The FE symmetry: ζ(1−s) = (prefactor)·ζ(s) where prefactor is nonvanishing in the strip. So ζ(ρ) = 0 with 0 < re ρ < 1 ⟹ ζ(1−ρ) = 0. That's analyticOrderAt_zeta_one_sub: analyticOrderAt ζ (1−w) = analyticOrderAt ζ w for 0 < re w < 1. Since ρ is a zero, order at ρ ≥ 1 (analyticOrderAt ≥ 1 iff vanishes, given analyticity), so order at 1−ρ ≥ 1, so ζ(1−ρ) = 0. Hmm, need \"analyticOrderAt f z ≥ 1 → f z = 0\" — there's `analyticOrderAt_eq_zero`? Actually f z = 0 ↔ analyticOrderAt f z ≠ 0 when analytic (Mathlib: `AnalyticAt.analyticOrderAt_eq_zero`? no...). There's `AnalyticAt.order_eq_zero_iff`? Hmm. In Mathlib: `analyticOrderAt_eq_zero_iff`? Let me remember: Mathlib has `AnalyticAt.analyticOrderAt_eq_zero` : analyticOrderAt f z = 0 ↔ f z ≠ 0. So f z = 0 → analyticOrderAt f z ≠ 0 → (with toNat) ... zeroMult ρ = (analyticOrderAt ζ ρ).toNat. If analyticOrderAt ζ ρ ≠ 0 and ≠ ⊤, then zeroMult ρ ≥ 1.\n\n  Also need membership in zeroDiscFinset(−t): ‖1−ρ − discCenter(−t)‖ ≤ 5/2. Compute: 1−ρ − (2 − it) = −1 − ρ + it = −(1 + ρ − it). ‖1 + ρ − it‖² = (1 + re ρ)² + (im ρ − t)²·... wait: ρ = x + iy, 1 + ρ − it = (1+x) + i(y−t). ‖·‖² = (1+x)² + (y−t)². With 0 < x < 1 and |y−t| < 1: ≤ 4 + 1 = 5 < 6.25 ✓. So ‖1−ρ − discCenter(−t)‖ < √5 < 5/2 ✓ (need strict/non-strict: closedBall, ≤; √5 ≤ 5/2 since 5 ≤ 25/4 ✓).\n\n  And |im(1−ρ) − (−t)| = |−y + t| = |y − t| < 1 ✓.\n\n  So the map ι : ρ ↦ 1 − ρ sends nearZeros(t) into nearZeros(−t). It's involutive (1−(1−ρ) = ρ), hence a bijection nearZeros(t) ≃ nearZeros(−t). Use Finset.sum_bij or sum_image with injectivity (1−ρ is injective).\n\n  Multiplicity: zeroMult (1−ρ) = zeroMult ρ for ρ ∈ nearZeros(t): from analyticOrderAt_zeta_one_sub (needs 0 < re ρ < 1 — have it from zeroDisc_isNontrivial) + toNat of both sides. Wait — but analyticOrderAt could be ⊤? If ζ were identically 0 in a neighborhood... no, analyticOrderAt_zeta_one_sub is an EQUALITY of orders (both ∞-valued), so toNat of both sides is equal regardless. Actually if both are ⊤, toNat ⊤ = 0 = toNat ⊤ ✓. The equality transports directly: zeroMult (1−ρ) = (analyticOrderAt ζ (1−ρ)).toNat = (analyticOrderAt ζ ρ).toNat = zeroMult ρ. \n\n  And the summand: m/(1−s−(1−ρ)) = m/(−(s−ρ)) = −m/(s−ρ) ✓.\n\n4. ΓR-bracket: logDeriv ΓR(1−s) + logDeriv ΓR(s).\n   - logDeriv_Gammaℝ requires re > 0. re(1−s) ∈ [1/2, 7/2] ✓ direct. re(s) ∈ [−5/2, 1/2] — NOT > 0. So for the s-side, we need logDeriv ΓR at s with re s possibly ≤ 0!\n   \n   Hmm, the design says: ΓR′/ΓR(s) — shift the s/2 argument by +2 via digamma recurrence. But that's for the DIGAMMA evaluation. The logDeriv_Gammaℝ identity itself (logDeriv ΓR(s) = −(log π)/2 + ½ψ(s/2)) is stated for re s > 0 only.\n   \n   For re s ≤ 0 (but s not a pole of ΓR, i.e., s ∉ {−2n}): the identity extends. How to prove in Lean?\n   \n   Option A: use the ΓR recurrence. ΓR(s) = π^{−s/2}Γ(s/2). There's a functional equation for ΓR? In Mathlib: `Complex.Gammaℝ`... The reflection: ΓR(s)·ΓR(2−s) = ... hmm. Actually the cleanest: Γ(s/2) with re(s/2) ∈ [−5/4, 1/4]. Use Gamma recurrence: Γ(z+2) = (z+1)zΓ(z) ⟹ Γ(z) = Γ(z+2)/(z(z+1)). So ΓR(s) = π^{−s/2}Γ(s/2+2)/((s/2)(s/2+1)).\n   \n   Then logDeriv ΓR(s) = logDeriv of RHS. Or define via the digamma identity directly.\n   \n   Option B: extend logDeriv_Gammaℝ by identity principle? No — logDeriv ΓR and the RHS are both meromorphic; equality on re > 0 extends to wherever both sides are analytic... The identity theorem for meromorphic functions is awkward in Lean. Better: prove the identity directly at the point s using the factorization.\n   \n   Option C (cleanest): derive the pointwise identity at our specific s via the shift FIRST, then apply logDeriv_Gammaℝ at s+4 (re(s+4) ∈ [3/2, 9/2] > 0):\n   \n   ΓR(s) relation to ΓR(s+4): ΓR(s) = π^{−s/2}Γ(s/2), ΓR(s+4) = π^{−s/2−2}Γ(s/2+2) = π^{−s/2}·π^{−2}·(s/2+1)(s/2)Γ(s/2).\n   So ΓR(s+4) = π^{−2}·(s/2)(s/2+1)·ΓR(s), i.e., ΓR(s) = π²·ΓR(s+4)/((s/2)(s/2+1)).\n   \n   Then logDeriv ΓR(s) = logDeriv ΓR(s+4) − 1/(s/2)·(1/2)... let me compute: log ΓR(s) = 2log π + log ΓR(s+4) − log(s/2) − log(s/2+1). d/ds: logDeriv ΓR(s+4)·1 − (1/2)/(s/2) − (1/2)/(s/2+1) = logDeriv ΓR(s+4) − 1/s − 1/(s+2).\n   \n   In Lean, this would be: deriv (ΓR) s / ΓR s. Getting deriv of ΓR at s directly is the issue; instead use: ΓR = fun s => π² · ΓR(s+4) / ((s/2)(s/2+1)) in a NEIGHBORHOOD of s (need the recurrence as a local identity), then logDeriv rules (div, mul, comp) apply pointwise.\n   \n   The recurrence Γ(z+1) = zΓ(z): Mathlib `Complex.Gamma_add_one` (s ≠ 0). As local identity: ΓR(s+4) = π^{−2}(s/2)(s/2+1)ΓR(s) holds for all s with s/2 ≠ 0, s/2+1 ≠ 0 (i.e., s ≠ 0, −2)... Actually Gamma_add_one needs the argument ≠ 0: Γ(w+1) = w Γ(w) for w ≠ 0. So Γ(s/2+1) = (s/2)Γ(s/2) for s/2 ≠ 0; Γ(s/2+2) = (s/2+1)Γ(s/2+1) for s/2+1 ≠ 0. Combined: Γ(s/2+2) = (s/2+1)(s/2)Γ(s/2) for s ∉ {0, −2}.\n   \n   Hmm wait, actually we need this as an EventuallyEq in a neighborhood of s to use logDeriv rules. Since s ∉ {0, −2} (s has im ≠ 0... for our region im = t, |t| ≥ 10, so s is never 0 or −2), the identity holds on the open set ℂ ∖ {0, −2} which is a neighborhood of s. ✓\n   \n   Then: logDeriv ΓR s = logDeriv (fun s => ΓR(s+4)) s − logDeriv (fun s => (s/2)(s/2+1)) s... hmm, careful with the div. Let me structure:\n   \n   ΓR =ᶠ[𝓝 s] fun s => (π² : ℂ) * ΓR(s+4) / ((s/2)*(s/2+1))  — hmm division. Or:\n   ΓR =ᶠ[𝓝 s] fun s => (π² : ℂ) * ΓR (s + 4) * (((s/2)*(s/2+1))⁻¹)... \n   \n   Alternatively set it up as: ΓR(s) · ((s/2)(s/2+1)) = π²·ΓR(s+4) locally, then logDeriv (mul): logDeriv ΓR s + logDeriv P s = logDeriv (ΓR(·+4)) s, where P(s) = (s/2)(s/2+1) ≠ 0 at s. Then logDeriv P s = P′(s)/P(s) computed directly, logDeriv (ΓR(·+4)) s = logDeriv ΓR (s+4) (deriv comp with s+4, deriv 1). And logDeriv ΓR (s+4) via logDeriv_Gammaℝ (re(s+4) > 0 ✓).\n   \n   That gives: logDeriv ΓR s = −(log π)/2 + ½ψ((s+4)/2) − P′(s)/P(s), where P′(s)/P(s) = 1/s + 1/(s+2)... let me verify: P(s) = s²/4 + s/2, P′(s) = s/2 + 1/2. P′/P = (s/2+1/2)/((s/2)(s/2+1)) = (s+1)/(s(s+2)/2)·... P = (s/2)(s/2+1) = s(s+2)/4. P′ = (2s+2)/4 = (s+1)/2. P′/P = 2(s+1)/(s(s+2)). And 1/s + 1/(s+2) = (s+2+s)/(s(s+2)) = 2(s+1)/(s(s+2)) ✓. Good.\n   \n   And digamma recurrence: ψ((s+4)/2) = ψ(s/2 + 2) = ψ(s/2) + 1/(s/2) + 1/(s/2+1) (digamma_apply_add_one twice; needs s/2 ≠ 0, s/2+1 ≠ 0). So ½ψ((s+4)/2) − 1/s − 1/(s+2) = ½ψ(s/2) + ½(2/s + 2/(s+2)) − 1/s − 1/(s+2) = ½ψ(s/2) + (1/s − 1/s) + (1/(s+2) − 1/(s+2)) = ½ψ(s/2). \n   \n   So logDeriv ΓR s = −(log π)/2 + ½ψ(s/2) — the SAME formula, now valid at our s. \n\n   So plan for the bracket:\n   - logDeriv_Gammaℝ_neg_shift (or a general \"logDeriv_Gammaℝ of re ≤ 0 away from poles\" lemma): logDeriv ΓR s = −(log π)/2 + ½ ψ(s/2) for s ∉ {0, −2} (or maybe just under our hypotheses: s.im ≠ 0 suffices to avoid poles... poles of ΓR are {−2n}, all real. So im s ≠ 0 ⟹ ΓR analytic and nonzero at s).\n   \n   Actually — wait. Let me reconsider: do I even need the identity at re s ≤ 0? The bracket is logDeriv ΓR(1−s) + logDeriv ΓR(s). For the bound, I can bound each piece: logDeriv ΓR(1−s) = −(logπ)/2 + ½ψ((1−s)/2) via logDeriv_Gammaℝ directly (re(1−s) > 0 ✓). For logDeriv ΓR(s), apply the shift: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)), then logDeriv ΓR(s+4) = −(logπ)/2 + ½ψ((s+4)/2) via logDeriv_Gammaℝ (re > 0 ✓). So I DON'T need the general shifted identity — just the local computation. That's cleaner.\n\n5. Bounds on the digamma terms:\n   - ψ((1−s)/2): w = (1−s)/2, re w ∈ [1/4, 7/4] > 0 ✓, |im w| = |t|/2 ≥ 5 ≥ 1/2 ✓. digamma_stirling: ‖ψ(w) − log w + 1/(2w)‖ ≤ 3/(im w)² = 12/t². Then ‖ψ(w)‖ ≤ ‖log w‖ + 1/(2‖w‖) + 12/t² ≤ (log‖w‖ + π) + small. ‖log w‖ ≤ |log‖w‖| + π (Complex.norm_log_le? Mathlib: ‖Complex.log z‖ ≤ |log ‖z‖| + |arg z|? There's `Complex.norm_log_le`? hmm, or abs_log... Let me recall: Complex.norm_log... There is `Complex.norm_log_le : ‖Complex.log x‖ ≤ |Real.log ‖x‖| + Real.pi`? I think there might be something in Zeta23's Y.lean: norm_digamma_le ‖ψ(w)‖ ≤ ‖w‖+8 — too lossy? ‖w‖ ~ |t|/2, so ‖ψ‖ ≤ |t|/2 + 8 — that's O(|t|), WAY too big for a C·log|t| bracket... but wait — D-067 §6 says \"fold loosely — constants don't propagate\". But an O(|t|) term would change the SHAPE: the final left-half bound would be 100000(log|t|)² + C|t|. Since (log|t|)² grows slower than |t|... the final statement shape needs to absorb: ≤ 200000·(log|t|)² fails if bracket ~ |t|. Hmm, but actually — does it matter? The 5e use: |F| = o(R) on circles of radius R. ζ′/ζ on the left half ≤ C(log|t|)² + C′|t|... on a circle of radius R, |t| ≤ R, so |F| ≤ C·R on the circle — that's O(R), NOT o(R). The proof needs o(R) to conclude F constant via (F(z)−F(0))/z bounded → Liouville. Hmm, O(R) gives (F(z)−F(0))/z = O(1) bounded on circles of radius R_k →∞... Actually the standard argument: if |F(z)| ≤ C·R on |z| = R for a sequence R_k → ∞, then (F(z) − F(0))/z is bounded on those circles (for |z| ≥ 1), hence by max modulus bounded everywhere, hence constant by Liouville... wait: (F(z)−F(0))/z is entire (removable at 0) and bounded on |z| = R_k; by max modulus, bounded on |z| ≤ R_k; since R_k → ∞, bounded everywhere; Liouville ⟹ constant; so F(z) = F(0) + c·z. Then need to rule out c ≠ 0: |F| ≤ C·R doesn't rule out linear growth! Hmm. But the actual ζ′/ζ bound IS logarithmic-ish, so the digamma ψ(s/2) ~ log(s/2) ~ log|t| is fine. The point: ψ grows like log, NOT like |w|. norm_digamma_le (‖ψ(w)‖ ≤ ‖w‖ + 8) is too lossy — I must use digamma_stirling + log bound: ‖ψ(w)‖ ≤ ‖log w‖ + ‖1/(2w)‖ + 3/(im w)².\n\n   ‖Complex.log w‖: Mathlib has `Complex.norm_log_le`? Hmm... I recall `Complex.abs_log`? No. There IS `Complex.norm_log (z : ℂ) : ‖Complex.log z‖ = ...`? Let me think: Complex.log z = Real.log ‖z‖ + i·arg z. So ‖log z‖ ≤ |Real.log ‖z‖| + |arg z| ≤ |log‖z‖| + π. There might be a lemma. In StirlingVert.lean itself there's `log_one_add_sub_log` etc. Zeta23 Y.lean probably has bounds on log. Let me check for existing helpers: grep \"norm_log\" in Zeta23.\n\n   For our w's: ‖w‖ ≤ C|t| and ‖w‖ ≥ |im w| = |t|/2 ≥ 5, so log‖w‖ ≤ log(C|t|) = log C + log|t| (for |t| ≥ 10 > 0), and ‖log w‖ ≤ log‖w‖ + π ≤ log|t| + O(1). \n\n   - ψ((s+4)/2): w = (s+4)/2, re w = (re s + 4)/2 ∈ [3/4, 9/4] > 0 ✓, |im w| = |t|/2 ≥ 5 ✓. Same treatment.\n\n   So the ΓR-bracket: ‖−log π − ... ‖ hmm let me redo:\n   logDeriv ΓR(1−s) + logDeriv ΓR(s) = [−(logπ)/2 + ½ψ((1−s)/2)] + [−(logπ)/2 + ½ψ((s+4)/2) − 2(s+1)/(s(s+2))]\n   = −log π + ½ψ((1−s)/2) + ½ψ((s+4)/2) − 2(s+1)/(s(s+2)).\n   \n   Norm: ≤ log π + ½(log|t| + O(1)) + ½(log|t| + O(1)) + O(1/|t|)... The last term: ‖2(s+1)/(s(s+2))‖ ≤ 2(‖s‖+1)/(‖s‖·‖s+2‖) ≤ C/|t| for |t| large (‖s‖ ≥ |t|... ‖s‖ ≥ |im s| = |t| ≥ 10; ‖s+2‖ ≥ |t| as well (im(s+2) = t); ‖s+1‖ ≤ ‖s‖ + 1 ≤ |t|·2 for large t, more carefully ‖s+1‖ ≤ |re s| + ... ≤ 5/2 + 1 + |t| ≤ 2|t| for |t| ≥ ... whatever, O(1/|t|) ≤ O(1)).\n   \n   So bracket ≤ log π + log|t| + O(1) ≤ C·log|t| for |t| ≥ 10 (log|t| ≥ log 10 > 2.3). Fold: bracket ≤ 100·log|t| say, or even 100·(log|t|)² to fold trivially.\n\n6. Assembly:\n   R(s) := logDeriv ζ s − Σ_{ρ ∈ nearZeros t} m(ρ)/(s−ρ).\n   logDeriv ζ s = −logDeriv ζ(1−s) − bracket.\n   Write B := logDeriv ζ(1−s) − Σ_{ρ′ ∈ nearZeros(−t)} m(ρ′)/(1−s−ρ′), ‖B‖ ≤ 100000·(log|t|)² (5c at −t).\n   −logDeriv ζ(1−s) = −B − Σ_{ρ′} m(ρ′)/(1−s−ρ′) = −B + Σ_{ρ ∈ nearZeros(t)} m(ρ)/(s−ρ) (by cancellation).\n   R(s) = −B + Σ m/(s−ρ) − bracket − Σ m/(s−ρ) = −B − bracket.\n   ‖R(s)‖ ≤ ‖B‖ + ‖bracket‖ ≤ 100000·(log|t|)² + C·log|t| ≤ 100001·(log|t|)² or so (fold: C·log|t| ≤ C·(log|t|)²·... for log|t| ≥ log 10 > 2, log|t| ≤ (log|t|)²/2, so C·log|t| ≤ (C/2)(log|t|)². Total ≤ (100000 + C/2)·(log|t|)². Choose the final loose constant, e.g., 200000·(Real.log |t|)². Clean.\n\n7. The left-plane uniform digamma bound |ψ(w) − log w| ≤ C away from poles — needed in 5e. Design: \"recurrence + series-vs-log comparison, O(1) in the chain length\". Region needed in 5e: on γ-gap circles, s in the left plane with re s ≥ −(2k+1)-ish? Actually for 5e the circles have radius R_k → ∞ and the leftmost point reaches re ~ −R_k. Hmm, that needs the digamma bound at LARGE negative real parts — via the recurrence ψ(w) = ψ(w+n) − Σ_{j<n} 1/(w+j), with n ~ R. The sum Σ 1/(w+j) vs log... \"series-vs-log comparison, O(1) in the chain length\" — the design says the error is O(1) per... hmm, actually let me think: ψ(w) − log w: with w = −R + it, shift by n ≈ R: ψ(w+n) − log(w+n) is bounded (Stirling), log(w+n) − log(w) is the log difference ~ log((w+n)/w) which is NOT bounded as R → ∞ if t is fixed... but on the circle |t| can be ~ R. Hmm. This needs care. Let me not over-plan 5e's needs here; the design says this bound is part of 5d. Let me define the exact statement:\n\n   Goal (from STATE.md): \"the left-plane uniform digamma bound |ψ(w) − log w| ≤ C away from poles (needed in 5e too) is part of this sub-stage (recurrence + series-vs-log comparison)\".\n\n   Precise formulation: For w with re w ≥ −A (any A), w avoiding neighborhoods of {0,−1,−2,...} (poles), |im w| ≥ 1/2 (say): |ψ(w) − log w| ≤ C(A)? or C uniform with the shift count? \"O(1) in the chain length\" — the error per shift step is O(1) total, i.e., independent of how many shifts.\n   \n   Actually let me think about what 5e needs exactly. D-067 §6: \"(iii) |F| = o(R) on a γ-gap circle sequence ... |ζ′/ζ| ≤ C log R on the circle by 5c on the right + 5d reflection on the left\". So on the LEFT part of the circle (re s very negative, down to −R), we need |ζ′/ζ(s)| ≤ C log R. Via FE: ζ′/ζ(s) = −ζ′/ζ(1−s) − [logDeriv ΓR(1−s) + logDeriv ΓR(s)]. The first two are fine (right half-plane, log bounds). The problematic term: logDeriv ΓR(s) = −(logπ)/2 + ½ψ(s/2) with re(s/2) ~ −R/2 large negative. ψ(s/2) ~ log(s/2) needs the left-plane digamma bound with error UNIFORM (or O(log R)) over the region. \n   \n   ψ(w) = ψ(w + n) − Σ_{j=0}^{n−1} 1/(w+j) for w+j ≠ 0. Choose n = ⌈|re w|⌉ + 2 so re(w+n) ∈ [1, 3]. Then ψ(w) − log w = [ψ(w+n) − log(w+n)] + [log(w+n) − log w] − Σ_j 1/(w+j).\n   - First bracket: O(1) by digamma_stirling (re(w+n) > 0, |im(w+n)| = |im w| ≥ 1/2). Actually the bound 3/(im)² + |1/(2(w+n))| ≤ small, so ‖ψ(w+n)‖ ≈ ‖log(w+n)‖ ≤ log‖w+n‖ + π. Hmm that's O(log R) not O(1). But we want ψ(w) − log w overall.\n   - log(w+n) − log w = log((w+n)/w): for w in the left plane with |im w| ≥ 1/2, (w+n)/w has argument bounded... ‖log(w+n) − log w‖ ≤ ‖log(w+n)‖ + ‖log w‖ ≤ log‖w+n‖ + |log‖w‖| + 2π = O(log R) (since ‖w‖ ≥ 1/2, |log‖w‖| ≤ log R + log 2... if ‖w‖ ≤ R then log‖w‖ ≤ log R; ‖w‖ ≥ |im| ≥ 1/2 so log‖w‖ ≥ −log 2... wait need lower bound on ‖w‖: if ‖w‖ ≥ 1/2, log‖w‖ ≥ log(1/2) = −log 2). So this is O(log R).\n   - The sum Σ_{j=0}^{n−1} 1/(w+j): each term |1/(w+j)| ≤ 1/|im w| ≤ 2 (if |im w| ≥ 1/2), n terms ⟹ ≤ 2n = O(R). TOO BIG. Need cancellation: Σ 1/(w+j) ≈ Σ d/dj log(w+j) = log(w+n) − log(w) + O(?)... The sum minus the log difference: Σ_{j} 1/(w+j) − [log(w+n) − log w] = Σ_j [1/(w+j) − log(1 + 1/(w+j−1}))]... this is the classic harmonic-vs-log: Σ_{j=0}^{n-1} [1/(w+j)] − log((w+n)/w) = Σ_j [1/(w+j) − log(w+j+1) + log(w+j)] and each summand is O(1/(w+j)²) = O(1/(j² + (im w)²)) — summable uniformly! Σ_j 1/(j²+c²) ≤ π²/6-ish, uniformly in c. YES — that's the \"O(1) in the chain length\": the total discrepancy is uniformly bounded.\n   \n   So: ψ(w) − log w = [ψ(w+n) − log(w+n)] + [log(w+n) − log w − Σ_j 1/(w+j)] and BOTH brackets are uniformly bounded (first by digamma_stirling + small terms, second by the 1/(w+j)² telescope) PROVIDED |im w| ≥ 1/2 and w+j stays away from 0 (poles). The condition \"away from poles\": with |im w| ≥ 1/2, w+j ≠ 0 automatically and |w+j| ≥ 1/2.\n   \n   Then |ψ(w) − log w| ≤ C uniformly ⟹ |ψ(w)| ≤ |log w| + C ≤ log|w| + C′ = O(log R). \n\n   This gives the needed 5e bound. In Lean, this is a real analysis estimate: Σ_j ‖1/(w+j) − log(1 + 1/(w+j))‖... hmm, log(w+j+1) − log(w+j) = log(1 + 1/(w+j)) needs care with complex log branches (the sum telescopes only with consistent branches). Alternative: bound Σ_j ‖1/(w+j) − (log(w+j+1) − log(w+j))‖ termwise via the Taylor bound ‖log(1+u) − u‖ ≤ ‖u‖² for ‖u‖ ≤ 1/2 (Complex.log(1+u) − u ≤ u²·something — Mathlib: `Complex.norm_log_one_add_sub_self_le`? hmm there's `Complex.norm_log_one_add_le : ‖Complex.log (1 + z)‖ ≤ ...`. There is `Complex.norm_log_sub_self_le`? Let me check: Mathlib has `Complex.norm_log_one_add_sub_self_le : ‖z‖ ≤ 1/2 → ‖Complex.log (1 + z) - z‖ ≤ ‖z‖^2`? I believe something like this exists for real... For complex: `Complex.norm_log_one_add_sub_self_le`? I need to check. If not, prove via the series or via norm_log_one_add_le and more work.\n   \n   Also the branch issue: log(w+j+1) − log(w+j) = log(1 + 1/(w+j)) holds when the args align — for w+j in the right half-plane it's fine, but for re(w+j) < 0... e.g., w = −5.5 + 10i, j = 0: w+1 = −4.5+10i, w = −5.5+10i, both in left half-plane, ratio = (−4.5+10i)/(−5.5+10i) — is log(ratio) = log(w+1) − log(w)? The difference of args: arg(w+1) − arg(w) — both args near π (upper half), the difference is small, and log(w+1) − log(w) = (log‖w+1‖ − log‖w‖) + i(arg(w+1) − arg(w)); log(1+1/w) has imaginary part arg(1+1/w) ∈ (−π, π]; 1+1/w = (w+1)/w; arg((w+1)/w) ≡ arg(w+1) − arg(w) mod 2π; since both args are in (π/2, π) their difference is in (−π/2, π/2), and arg of the ratio is the representative in (−π, π] — equal to the difference if the difference is in (−π, π] ✓. So log(w+1) − log(w) = log((w+1)/w) = log(1 + 1/w) as long as arg(w+1) − arg(w) ∈ (−π, π], which holds when... both in same open half-plane (upper or lower) suffices? If im w > 0 and im(w+1) > 0 (same as im w), args in (0, π), difference in (−π, π) ✓. So for |im w| ≥ 1/2, all w+j have the same sign of imaginary part ⟹ branch consistent ✓. In Lean: `Complex.log_div`? Mathlib: `Complex.log_div (hx : x.im ≠ 0 or ...)`. Hmm, there's `Complex.log_div_of_ne_zero`? The cleanest: `Complex.log_div (hxi : x.im ≠ 0) (hyi : y.im ≠ 0)`? I don't remember exactly. There is Complex.log_div in Mathlib with hypotheses about imaginary parts having the same sign? Let me check at build time: `Complex.log_div (hx : x.im ≠ 0) (hy : y.im ≠ 0)`? Hmm, I recall `Complex.log_div (h₁ : x.im ≠ 0) (h₂ : y.im ≠ 0) : log (x / y) = log x - log y`? Not sure. There's also `Complex.log_div'`? I'll check.\n\n   Alternatively, avoid the telescope: bound ‖Σ_j 1/(w+j)‖ directly against the integral/log via a summability comparison. Actually the cleanest Lean route might be:\n   ‖ψ(w) − log w‖ ≤ ‖ψ(w+n) − log(w+n)‖ + ‖Σ_j [1/(w+j)] − (log(w+n) − log w)‖ and write the second as ‖Σ_{j=0}^{n−1} (1/(w+j) − log(1 + 1/(w+j)))‖ ≤ Σ_j ‖1/(w+j) − log(1+1/(w+j))‖ ≤ Σ_j ‖1/(w+j)‖² (via the Taylor bound, valid since ‖1/(w+j)‖ ≤ 2/|im w|... hmm need ‖u‖ ≤ 1/2: ‖1/(w+j)‖ ≤ 1/|im w|; if |im w| ≥ 2, then ≤ 1/2 ✓. Take |im w| ≥ 2 as the hypothesis).\n   Then Σ_j ‖w+j‖⁻² ≤ Σ_j 1/((re w + j)² + (im w)²)... this needs a uniform-in-c bound for Σ_{j=0}^{n−1} 1/((j−a)² + c²) where a = |re w| ~ n. The terms where j ≈ a: 1/c² ≤ 1/4. Terms away: Σ 1/(j−a)² converges: Σ_{k≠0} 1/k²-type ≤ 2·(π²/6)·... but careful, j − a ranges over roughly [−a, n−a] integers; Σ over integers k in a range of 1/(k² + c²) ≤ Σ_{k∈ℤ} 1/(k² + c²) ≤ 1/c² + 2Σ_{k≥1} 1/k² = 1/c² + π²/3. With c ≥ 2: ≤ 1/4 + π²/3 < 4. But j−a is NOT an integer (a = |re w| arbitrary real). Σ_{j=0}^{n−1} 1/((j−a)² + c²) — shift: let δ = a − ⌊a⌋; the terms are 1/((j − ⌊a⌋ − δ)² + c²); reindex k = j − ⌊a⌋: Σ_k 1/((k−δ)² + c²). Bound: (k−δ)² ≥ (|k|−1)² for |k| ≥ 1... standard comparison. This is all elementary but fiddly in Lean. Alternatively compare with an integral: Σ 1/((j−a)²+c²) ≤ 1/c² + ∫_{−∞}^{∞} dx/(x²+c²)·... = 1/c² + π/c ≤ 1/4 + π/2 < 2. The integral comparison in Lean: could use `sum_le_integral_of_decreasing`-type lemmas but two-sided (peak at j=a) complicates. Simpler: split at k=0: Σ_{k≥1} 1/((k−1)² + c²)... hmm.\n\n   Honestly, this left-plane digamma bound might be the trickiest part of 5d. Let me consider a cleaner approach: maybe Zeta23 already has something? GammaFacts/Series.lean has the digamma series: ψ(w) = −γ + Σ_{k≥0} (1/(k+1) − 1/(k+w)) — the Weierstrass series! With that: ψ(w) − log w = −γ + Σ_k [1/(k+1) − 1/(k+w)] − log w. Hmm, the series vs log comparison again — same issue.\n\n   Alternative cleaner approach: ψ(w) = ψ(w+n) − Σ_{j=0}^{n−1} 1/(w+j), and bound ‖Σ_j 1/(w+j) − (log(w+n) − log w)‖ via the SUM-INTEGRAL: actually, maybe simplest to bound each piece differently: instead of telescoping, use:\n   Σ_{j=0}^{n−1} 1/(w+j) = Σ_j ∫_0^1 ... hmm.\n\n   OK here's another thought — Euler–Maclaurin again! Σ_{j=0}^{n−1} f(j) with f(x) = 1/(w+x): EM gives Σ = ∫₀ⁿ f + (f(n)−f(0))/2·... plus the B̃₁ integral remainder: Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f(x)dx − (f(n)−f(0))/2 + ∫ B̃₁ f′. ∫₀ⁿ dx/(w+x) = log(w+n) − log w (continuous antiderivative along the path — since re(w+x) for x ∈ [0,n] may cross... w+x for x real ≥ 0: im = im w ≠ 0, so the path stays in ℂ∖(−∞,0]; log is an antiderivative of 1/· on that path ✓ — in Lean, ∫ over a real interval of 1/(w+x) dx = log(w+n) − log w via FTC with Complex.log ∘ (w+·) differentiable with derivative 1/(w+x) ✓). And f′(x) = −1/(w+x)², so the remainder ∫₀ⁿ B̃₁(x)·(−1/(w+x)²)dx has norm ≤ (1/2)∫₀ⁿ dx/|w+x|² ≤ (1/2)∫_{−∞}^∞ dx/((x−a)² + c²) = (1/2)·(π/c) ≤ π/4 for c ≥ 2. And |(f(n)−f(0))/2| ≤ (1/2)(1/|w+n| + 1/|w|) ≤ (1/2)(2 + 2) = 2 (since |w+j| ≥ |im| ≥ 2 ⟹ each ≤ 1/2). \n   \n   So ‖Σ_{j=0}^{n−1} 1/(w+j) − (log(w+n) − log w)‖ ≤ π/4 + 1. CLEAN and uniform! And we HAVE the EM machinery (Zeta23 EulerMaclaurin.lean B̃₁ + IBP helpers, used in ii′-5b). The formula: Σ_{j=0}^{n-1} f(j) = ∫₀ⁿ f + ... let me get the exact B̃₁ EM identity: Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f(x)dx + (f(0)−f(n))/2 + ∫₀ⁿ B̃₁(x) f′(x) dx. Check sign: ∫₀ⁿ B̃₁ f′ = [B̃₁ f]₀ⁿ − ∫₀ⁿ f (B̃₁′ = 1 a.e.) = −(1/2)(f(n)−f(0))·... B̃₁(0) = −1/2, B̃₁ at integer n: B̃₁(n) = −1/2 (periodic, B̃₁(0)=−1/2). So [B̃₁f]₀ⁿ = −f(n)/2 + f(0)/2. ∫₀ⁿ B̃₁ f′ = f(0)/2 − f(n)/2 − ∫₀ⁿ f. So ∫₀ⁿ f = f(0)/2 − f(n)/2 − ∫B̃₁f′. And Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f + ... standard: Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f(x) dx + (f(0) − f(n))/2·(−1)... let me just redo: Euler summation: Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f(x)dx + ... Take f(j) = ∫_j^{j+1} f(j) dx; f(x) = f(j) + ∫_j^x f′; ∫_j^{j+1} f(x) dx = f(j) + ∫_j^{j+1} (x−j−1)·... I'll trust: Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f(x) dx + (f(0)−f(n))/2 + ∫₀ⁿ B̃₁(x) f′(x) dx where B̃₁(x) = x − ⌊x⌋ − 1/2. Sanity f = 1: LHS n, RHS n + 0 + 0 ✓. f(x) = x: LHS n(n−1)/2; ∫₀ⁿ x = n²/2; (0−n)/2 = −n/2; ∫ B̃₁ ·1 = 0. Total n²/2 − n/2 ✓. \n\n   In Lean: does Zeta23 EulerMaclaurin.lean have this summed form, or just per-interval IBP? ii′-5b used `integral_deriv_mul_add_const` IBP helper per unit interval. So I'd build: Σ_j f(j) − ∫₀ⁿ f = Σ_j [f(j) − ∫_j^{j+1} f] and per interval: f(j) − ∫_j^{j+1} f(x) dx = −∫_j^{j+1} (f(x) − f(j)) dx = −∫_j^{j+1} ∫_j^x f′(u) du dx... or directly per-interval IBP: ∫_j^{j+1} (x − j − 1/2) f′(x) dx = [(x−j−1/2)f(x)]_j^{j+1} − ∫_j^{j+1} f = (1/2)(f(j+1) + f(j)) − ∫_j^{j+1} f. Hmm that gives the trapezoid form: ∫_j^{j+1} f = (f(j)+f(j+1))/2 − ∫_j^{j+1} B̃₁(x) f′(x) dx. Sum over j: ∫₀ⁿ f = (f(0)+f(n))/2 + Σ_{j=1}^{n−1} f(j) − ∫₀ⁿ B̃₁ f′ = Σ_{j=0}^{n−1} f(j) − (f(0)−f(n))/2 − ∫₀ⁿ B̃₁ f′. So Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f + (f(0)−f(n))/2 + ∫₀ⁿ B̃₁ f′ ✓ matches.\n   \n   This is very doable with the existing machinery. The f here: f(x) = 1/(w + x) = (w + ↑x)⁻¹ as a function of REAL x — need real-interval differentiability and the IBP on each unit interval — the existing helpers should adapt (they were built for the ζ kernel, probably with general f or specific?). `integral_deriv_mul_add_const` — sounds general. Let me check EulerMaclaurin.lean.\n\n   Then: ‖ψ(w) − log w‖ ≤ ‖ψ(w) − ψ(w+n)‖ + ... wait I need to restructure: ψ(w) − log w = [ψ(w+n) − log(w+n)] + [log(w+n) − log w − Σ_j 1/(w+j)]. ✓ as before.\n   - ‖ψ(w+n) − log(w+n)‖ ≤ 3/(im)² + ‖1/(2(w+n))‖ ≤ 3/4 + 1/4 = 1 (for |im| ≥ 2, ‖w+n‖ ≥ |im| ≥ 2). From digamma_stirling: ‖ψ(v) − log v + 1/(2v)‖ ≤ 3/(im v)², so ‖ψ(v) − log v‖ ≤ 3/c² + 1/(2‖v‖) with v = w+n, |im v| = c ≥ 2, ‖v‖ ≥ c ≥ 2: ≤ 3/4 + 1/4 = 1 ✓.\n   - Second bracket: ≤ 1 + π/4 (the (f(0)−f(n))/2 term: ‖f(0)‖ = 1/‖w‖ ≤ 1/2, ‖f(n)‖ ≤ 1/2 ⟹ ≤ 1/2; wait: ‖(f(0)−f(n))/2‖ ≤ (1/2)(1/2 + 1/2) = 1/2. And the B̃₁ integral: ≤ (1/2)·∫₀ⁿ dx/‖w+x‖² ≤ (1/2)·∫_ℝ dx/((x−a)²+c²) = π/(2c) ≤ π/4 (c ≥ 2). Total ≤ 1/2 + π/4 < 1.3.)\n   \n   So ‖ψ(w) − log w‖ ≤ 1 + 1/2 + π/4 < 3 for |im w| ≥ 2. Uniform constant C = 3 (say). \n   \n   Actually wait — also need ‖log(w+n) − log w‖ handled INSIDE the second bracket — yes it's the EM comparison. Good.\n   \n   But hmm, one more subtlety: the telescoped expression needs EXACTLY Σ 1/(w+j) = [log(w+n) − log w] + error — I have ‖Σ − (log diff)‖ ≤ 1/2 + π/4 ✓.\n\n   Then in 5e the usage: ψ(s/2) with s on the circle, |im s| could be SMALL (circle crosses the real axis!). Hmm — on a circle of radius R, the points with re s very negative have |im s| up to R, but the circle also passes near the negative real axis where im s ≈ 0! There the digamma bound |im w| ≥ 2 FAILS. How does D-056/Davenport handle the negative-real part of the circle? The classical device: circles cross the real axis at points BETWEEN consecutive trivial zeros (i.e., at odd negative integers −(2k+1)), where ζ′/ζ is bounded directly (the trivial zeros at −2k are at distance ≥ 1). For the digamma at w = s/2 near a negative odd half-integer... hmm, ψ(s/2) with s/2 near −(2k+1)/2 = half-integer: ψ is analytic there (poles only at non-positive INTEGERS), so ψ(s/2) is fine pointwise but our bound needs uniformity. For w near the negative real axis at half-integers: |im w| < 2 but w stays away from integers (re w half-integer ±): the shift argument still works: ψ(w) = ψ(w+n) − Σ 1/(w+j) — now w+j can cross... the terms 1/(w+j): when re w = −m−1/2, the term j = m: w + m ≈ −1/2 + i·(small im) — |w+m| ≥ 1/2 since re(w+m) = −1/2 exactly if re w = −m − 1/2... In general \"away from poles\" means |w + j| ≥ δ for all j — that's the real condition. So the right hypothesis: |w + j| ≥ δ for all j ∈ ℕ (equivalently dist(w, {0,−1,−2,...}) ≥ δ), NO im condition; then:\n   - digamma_stirling at v = w+n needs |im v| ≥ 1/2 — FAILS on the real axis! Hmm. But for w real-ish near −m−1/2, w+n is real-ish near +1/2 — digamma_stirling needs |im| ≥ 1/2. For real v > 0, ψ(v) − log v is bounded by the REAL Stirling (Mathlib: real digamma? hmm, Mathlib has Real.digamma? There's `Real.digamma`? I don't think so. There's Complex.digamma only, I believe. But there might be a real Stirling for ψ in Zeta23? Or use the series).\n   \n   OK — this is getting deep into 5e's actual needs. The 5e circle argument: circles |s| = R_k crossing the negative real axis at odd integers... the full 5e design will need the digamma bound in TWO regions: |im w| ≥ 2 (this sub-stage's version) and near the negative real axis at half-integer points (a separate small argument: ψ continuous on compact + explicit recurrence — ψ(w) = ψ(w+m) − Σ 1/(w+j) with denominators ≥ 1/2 in absolute value... m terms each ≤ 2, that's O(m) = O(R) — TOO BIG again; need the EM comparison but with the integral ∫ dx/(w+x)² having singularities? No: |w+x| ≥ 1/2 (distance from poles), so ∫₀ⁿ dx/|w+x|² ≤ ∫ over the range where... hmm, when w ≈ −m − 1/2 real, |w + x| ≥ |re(w+x)| and the integral ∫₀ⁿ dx/(w+x)² CONVERGES as an improper... it's fine: ∫ dx/(w+x)² = −1/(w+x) evaluated = 1/w − 1/(w+n) — bounded by 2+2 = 4. But the BOUND ‖∫ B̃₁/(w+x)²‖ ≤ (1/2)∫ dx/|w+x|² — with w real negative half-integer, |w+x|² = (w+x)² real, ∫₀ⁿ dx/(w+x)² blows up near x = −w... wait no: w+x = 0 when x = −w = m+1/2 ∈ [0,n] — the INTEGRAND f(x) = 1/(w+x) has a POLE on the integration path! But wait — that's only if m + 1/2 is hit exactly: w = −m−1/2 exactly real, then w + (m+1/2) = 0 with m+1/2 ∈ (0, n). The real integral ∫₀ⁿ dx/(w+x) diverges! So the EM comparison FAILS for real w — of course: log(w+n) − log w for real negative w involves the branch jump iπ, and Σ 1/(w+j) is real — the difference is ~iπ, still bounded actually! Hmm, but the real integral diverges so EM doesn't apply directly (f not continuous on [0,n]).\n   \n   Resolution: keep |im w| ≥ δ > 0 as the hypothesis (circles avoid the real axis? No — circles cross it). The classical 5e argument (Davenport Ch 15/16): on the circle |s| = R, split into |im s| ≥ 1 and |im s| < 1 parts; near the real axis use the explicit value/different bound. I'll defer that exact split to 5e; for 5d, deliver the uniform bound with hypothesis |im w| ≥ 2 (or ≥ 1): \"away from poles\" via imaginary part. STATE.md says exactly: \"the left-plane uniform digamma bound |ψ(w) − log w| ≤ C away from poles (recurrence + series-vs-log)\". I'll formulate: for w with 2 ≤ |im w| (away from poles via im), ‖digamma w − log w‖ ≤ 3 (or whatever falls out). And ALSO the half-integer real-axis variant can come later if 5e needs it.\n\nLet me now also check: does LiContour.lean have ZeroCountProp / exists_avoiding_midpoint — not needed for 5d actually. The 5d ingredients:\n\n(A) FE logDeriv identity at the point s (with ζ s ≠ 0, im s = t, |t| ≥ 10 — so s ∉ {0,1}, ΓR s ≠ 0, all differentiability fine).\n(B) The reflected 5c bound at (1−s, −t).\n(C) Zero-sum cancellation via ρ ↦ 1−ρ bijection nearZeros(t) → nearZeros(−t) + zeroMult invariance.\n(D) ΓR-bracket evaluation + bound.\n(E) Left-plane digamma bound (separate theorem, for 5e).\n\nLet me now check the needed Mathlib/Zeta23 APIs:\n\n1. `logDeriv` rules: logDeriv_mul (hf : DifferentiableAt ℂ f x) (hg : ...) (hx : f x ≠ 0) (hy : g x ≠ 0)? Let me check the exact signature: `logDeriv_mul (hf : f x ≠ 0) (hg : g x ≠ 0) : logDeriv (f * g) x = logDeriv f x + logDeriv g x`? Hmm, logDeriv is defined as deriv f x / f x — no differentiability needed in the DEF, but the mul rule: deriv (f*g) = deriv f * g + f * deriv g needs differentiability; divided by f*g gives logDeriv f + logDeriv g. Mathlib: `logDeriv_mul (hx : f x ≠ 0) (hy : g x ≠ 0) (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : logDeriv (f * g) x = logDeriv f x + logDeriv g x`. I think the arg order is (hf hg hfd hgd) or similar — check at build.\n\n2. `logDeriv_comp`? For Λ(1−s): deriv (fun s => Λ (1 − s)) s = −deriv Λ (1−s) via deriv.comp or HasDerivAt. There might be `logDeriv_comp_sub`... I'll do it manually: logDeriv (Λ ∘ (1−·)) s = deriv (Λ ∘ (1−·)) s / Λ(1−s); deriv (Λ ∘ (1−·)) s = deriv Λ (1−s) · deriv (1−·) s = −deriv Λ (1−s) (via DifferentiableAt.comp + deriv_const_sub). Then logDeriv Λ s = logDeriv (fun s => Λ (1−s)) s (from Λ = Λ∘(1−·) via completedRiemannZeta_one_sub funext) = −logDeriv Λ (1−s) ✓.\n\n3. `completedRiemannZeta_one_sub : completedRiemannZeta (1 - s) = completedRiemannZeta s` (Mathlib) ✓.\n\n4. Differentiability: `differentiableAt_completedZeta (hs₀ : s ≠ 0) (hs₁ : s ≠ 1)` (used in CountByIntegral). For ΓR: search `differentiableAt_Gammaℝ` or differentiable_Gammaℝ. Zeta23 GammaSide.lean had `hd.div hA.differentiableOn ...` — let me look at what's there (line 56 logDeriv_Gammaℝ_differentiableOn). I'll grep for the differentiability lemma names.\n\n5. `Complex.Gammaℝ_ne_zero_of_re_pos` (0 < re) ✓ used. `Complex.Gammaℝ_eq_zero_iff : Gammaℝ s = 0 ↔ ∃ n : ℕ, s = -2 * n` ✓ (used in zeroDisc_isNontrivial).\n\n6. `digamma_apply_add_one (s : ℂ) (hs : s ≠ 0) : digamma (s + 1) = digamma s + 1 / s` — hmm wait actually Mathlib: `Complex.digamma_apply_add_one (hs : ∀ n : ℕ, s ≠ -n)`? No — I recall `Complex.digamma_apply_add_one (s : ℂ) (h : s ≠ 0) : digamma (s + 1) = digamma s + s⁻¹`? Let me check at build. Actually I think it's `(hs : s ≠ 0)`. Hmm — digamma has poles at 0, −1, −2, ...; the recurrence ψ(s+1) = ψ(s) + 1/s holds for s ≠ 0 (s ≠ 0 ensures both sides defined? s = −1: ψ(0) is junk... but s = −1 ≠ 0 and ψ(s+1) = ψ(0) junk = ψ(−1) + 1/(−1)? In Mathlib the identity might be stated for s ≠ 0 with junk values matching, or with the stronger hypothesis. D-067 says Mathlib `digamma_apply_add_one` — verified live in session 022. I'll check the exact form.\n\n7. Reflection: `analyticOrderAt_zeta_one_sub (h0 : 0 < w.re) (h1 : w.re < 1) : analyticOrderAt riemannZeta (1 - w) = analyticOrderAt riemannZeta w` — check exact statement at line 224.\n\n8. ζ(1−s) ≠ 0 from ζ s ≠ 0 (s in our left region): via Λ: Λ(1−s) = Λ(s) = ΓR(s)ζ(s) ≠ 0 and Λ(1−s) = ΓR(1−s)ζ(1−s) with ΓR(1−s) ≠ 0 (re(1−s) ≥ 1/2 > 0) ⟹ ζ(1−s) ≠ 0. Need 1−s ≠ 0 for completedRiemannZeta_eq_Gammaℝ_mul: 1−s = 0 ⟺ s = 1, but im s = t ≠ 0 ✓.\n\n9. For (C), the bijection sum: `Finset.sum_bij` or map to an image finset: Σ_{ρ' ∈ nearZeros(−t)} g(ρ') = Σ_{ρ ∈ nearZeros(t)} g(1−ρ) needs nearZeros(−t) = (nearZeros t).image (1 − ·) and injectivity. I'll prove `nearZeros_neg_t_eq_image : nearZeros (−t) = (nearZeros t).image fun ρ => 1 − ρ`.\n   - ⊆: ρ' ∈ nearZeros(−t) ⟹ ρ' = 1−(1−ρ') and 1−ρ' ∈ nearZeros(t): needs ζ(1−ρ') = 0 (order transport), ‖1−ρ' − discCenter t‖ ≤ 5/2 (compute: 1−ρ' − (2+it) = −(1 + ρ' − it)... ‖1 + ρ' − it‖² = (1 + re ρ')² + (im ρ' − t)². ρ' ∈ zeroDiscFinset(−t): re ρ' ∈ [−1/2, 9/2] hmm — the disc bound gives re ∈ [−1/2, 9/2]; but ρ' is a zero in the disc ⟹ nontrivial ⟹ 0 < re ρ' < 1 ✓ (zeroDisc_isNontrivial). |im ρ' − (−t)| < 1 ⟹ |im ρ' + t| < 1. So (1+re ρ')² ≤ 4, (im ρ' − t)² ≤ 1 ⟹ ‖·‖² ≤ 5 < 6.25 ✓; |im(1−ρ') − t| = |−im ρ' − t| = |im ρ' + t| < 1 ✓.\n   - ⊇: ρ ∈ nearZeros(t) ⟹ 1−ρ ∈ nearZeros(−t): symmetric (‖1−ρ − discCenter(−t)‖² = ‖−1 −ρ + it‖² = (1+re ρ)² + (im ρ − t)² ≤ 5 ✓; |im(1−ρ) + t| = |−im ρ + t| < 1 ✓; ζ(1−ρ) = 0 ✓).\n   - zeroMult (1−ρ) = zeroMult ρ: from analyticOrderAt_zeta_one_sub with 0 < re ρ < 1 ✓ (toNat congruence).\n   \n   Wait — analyticOrderAt_zeta_one_sub gives analyticOrderAt ζ (1−w) = analyticOrderAt ζ w — but as ℂ∞ (WithTop ℕ)? toNat of both sides equal ✓. But CAREFUL: zeroMult (1−ρ) uses analyticOrderAt ζ (1−ρ) — is 1−ρ in the strip for the lemma's hypotheses? The lemma is stated as: for w with 0 < re w < 1: analyticOrderAt ζ (1−w) = analyticOrderAt ζ w. So apply with w = ρ ✓.\n\n   Also need ζ(1−ρ) = 0: analyticOrderAt ζ (1−ρ) = analyticOrderAt ζ ρ ≠ 0 (since ζ ρ = 0 and analytic... hmm: analyticOrderAt f z ≠ 0 ↔ f z = 0 given AnalyticAt: Mathlib `AnalyticAt.analyticOrderAt_ne_zero`? There's `AnalyticAt.analyticOrderAt_eq_zero : analyticOrderAt f z = 0 ↔ f z ≠ 0`? Let me check the name — might be `analyticOrderAt_eq_zero_iff` or via `AnalyticAt.order_eq_zero_iff` (older). Zeta23 used analyticOrderAt extensively; there's surely a helper. Alternatively: ζ(1−ρ) = 0 via the FE directly: Λ(1−ρ) = Λ(ρ) = ΓR(ρ)ζ(ρ) = 0... wait Λ(ρ) = ΓR(ρ)·ζ(ρ) needs ρ ≠ 0 and ΓR ρ ≠ 0 — both fine (0 < re ρ < 1). So Λ(1−ρ) = Λ(ρ) = 0. Then Λ(1−ρ) = ΓR(1−ρ)·ζ(1−ρ) with ΓR(1−ρ) ≠ 0 (re(1−ρ) > 0) ⟹ ζ(1−ρ) = 0 ✓. Clean, avoids order lemmas. (Need 1−ρ ≠ 0: re(1−ρ) > 0 ✓.)\n\n10. digamma bounds: `StirlingVert.digamma_stirling (hw : 0 < w.re) (ht : 1/2 ≤ |w.im|) : ‖digamma w − log w + (1/2)/w‖ ≤ 3 / w.im^2` ✓ (namespace? It's in Zeta23 namespace per grep: Zeta23/GammaFacts/StirlingVert.lean line 483, theorem digamma_stirling — inside `namespace Zeta23`? Need to check. LiDigamma.lean may already open something. It's likely `Zeta23.StirlingVert.digamma_stirling` or just in Zeta23 namespace. Check the namespace in the file.)\n\n11. ‖Complex.log w‖ bound: search for existing helpers in Zeta23 (Y.lean? StirlingVert has log_one_add_sub_log). Let me grep \"norm_log\" in Zeta23 and Mathlib: Mathlib has `Complex.norm_log_le : ‖Complex.log z‖ ≤ Complex.abs (Real.log ‖z‖) + Real.pi`? Hmm... I recall `Complex.abs_log_eq...` no. There's `Complex.norm_log (z) : ‖log z‖ = sqrt ((Real.log ‖z‖)^2 + (arg z)^2)`? not sure. Let me grep.\n\n12. `Complex.Gamma_add_one (s : ℂ) (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s` ✓ (Mathlib).\n\n13. For the local ΓR recurrence: ΓR(s) = π^{−s/2}Γ(s/2) (Complex.Gammaℝ_def). So ΓR(s+4) = π^{−(s+4)/2}Γ((s+4)/2) = π^{−s/2}·π^{−2}·Γ(s/2+2). And Γ(s/2+2) = (s/2+1)Γ(s/2+1) = (s/2+1)(s/2)Γ(s/2) (two Gamma_add_one applications: Γ(s/2+1) = (s/2)Γ(s/2) needs s/2 ≠ 0; Γ(s/2+2) = (s/2+1)Γ(s/2+1) needs s/2+1 ≠ 0).\n    ⟹ ΓR(s+4) = π^{−2}(s/2)(s/2+1)·ΓR(s) for s ∉ {0, −2}.\n    \n    For logDeriv at s: I want logDeriv ΓR s. Route: ΓR =ᶠ[𝓝 s] (fun s => (π² : ℂ) * ΓR (s+4) * ((s/2)*(s/2+1))⁻¹)? Hmm, actually cleaner to write ΓR =ᶠ[𝓝 s] fun s => ΓR (s + 4) / ((π : ℂ)⁻¹² ... let me define P s := (s/2)*(s/2+1) and c := (Real.pi : ℂ)^(-2 : ℝ)... ΓR(s) = ΓR(s+4)/(π^{−2}·P(s)) = π²·ΓR(s+4)/P(s). \n    \n    logDeriv ΓR s = logDeriv (fun s => π² * ΓR (s+4) / P s) s — via EventuallyEq.logDeriv? There IS `Filter.EventuallyEq.logDeriv`? Hmm — logDeriv f s = deriv f s / f s; EventuallyEq in 𝓝 s gives deriv equality (EventuallyEq.deriv_eq is the pointwise one — journal-024: \"EventuallyEq.deriv is the EVENTUALLY version; the pointwise one is Filter.EventuallyEq.deriv_eq\"). So: (h : f =ᶠ[𝓝 s] g) : deriv f s = deriv g s (h.deriv_eq) and f s = g s (h.eq_of_nhds) ⟹ logDeriv f s = logDeriv g s directly by rw. \n    \n    Then logDeriv of the product/quotient at s:\n    logDeriv (fun s => c * ΓR (s+4) / P s) s = logDeriv (fun s => c * ΓR (s+4)) s − logDeriv P s (logDeriv_div needs nonzero + differentiability) = logDeriv (ΓR ∘ (·+4)) s + logDeriv (const c)... const has logDeriv 0 (deriv const = 0). logDeriv (fun s => ΓR (s+4)) s = deriv ΓR (s+4) / ΓR (s+4) = logDeriv ΓR (s+4) (chain rule, deriv (s+4) = 1).\n    And logDeriv P s = deriv P s / P s; P s = (s/2)(s/2+1) = s²/4 + s/2; deriv P s = s/2 + 1/2 (compute via deriv rules). So logDeriv P s = (s/2 + 1/2)/((s/2)(s/2+1)) = 2(s+1)/(s(s+2)) (field_simp with s ≠ 0, s+2 ≠ 0).\n    \n    Then bracket bound: ‖logDeriv ΓR (1−s) + logDeriv ΓR s‖ = ‖−(logπ)/2 + ½ψ((1−s)/2) − (logπ)/2 + ½ψ((s+4)/2) − 2(s+1)/(s(s+2))‖ ≤ log π + ½‖ψ((1−s)/2)‖ + ½‖ψ((s+4)/2)‖ + ‖2(s+1)/(s(s+2))‖.\n    \n    Each ψ: ‖ψ(w)‖ ≤ ‖log w‖ + 1/(2‖w‖) + 3/(im w)² with w.im = ±t/2, |t| ≥ 10: 3/(t/2)² = 12/t² ≤ 12/100 = 0.12; 1/(2‖w‖) ≤ 1/(2·5) = 0.1; ‖log w‖ ≤ |log ‖w‖| + π: ‖w‖ ≥ 5, ‖w‖ ≤ (7/4 + 9/4... let me bound: for w = (1−s)/2: ‖w‖ ≤ (1 + ‖s‖)/2 ≤ (1 + 5/2 + |t|)/2 ≤ (2|t|)/2 = |t| for |t| ≥ ... 1 + 2.5 + |t| ≤ 2|t| ⟺ 3.5 ≤ |t| ✓ (|t| ≥ 10). So log ‖w‖ ≤ log |t| + log 2 ≤ log|t| + 1 (log 2 < 1); and log‖w‖ ≥ log 5 > 0 so |log‖w‖| = log‖w‖ ≤ log|t| + 1. ‖log w‖ ≤ log|t| + 1 + π ≤ log|t| + 5 (π < 4). Similarly for w = (s+4)/2: ‖w‖ ≤ (‖s‖+4)/2 ≤ (5/2 + |t| + 4)/2 ≤ 2|t|/2 = |t|... (6.5 + |t| ≤ 2|t| ⟺ 6.5 ≤ |t| ✓). Same bound.\n    \n    So each ‖ψ‖ ≤ log|t| + 5 + 0.1 + 0.12 ≤ log|t| + 6. The rational term: ‖2(s+1)/(s(s+2))‖ ≤ 2(‖s‖+1)/(‖s‖‖s+2‖) ≤ 2(2|t|)/(|t|·|t|) = 4/|t| ≤ 0.4 (using ‖s‖ ≥ |t| since |im s| = |t|; ‖s+2‖ ≥ |t| similarly; ‖s+1‖ ≤ ‖s‖ + 1 ≤ 5/2 + |t| + 1 ≤ 2|t| for |t| ≥ 3.5 ✓).\n    \n    Total bracket ≤ log π + (log|t| + 6) + 0.4 ≤ 2·log|t| + 12 (log π < 2, log|t| ≥ log 10 > 2). Fold: ≤ 2·log|t| + 12 ≤ 2·(log|t|)²·... for the final fold: 2log|t| + 12 ≤ C(log|t|)² with (log|t|)² ≥ 2log|t| ⟹ log|t| ≥ 2 ✓ (log 10 = 2.302): 2log|t| + 12 ≤ (log|t|)² + 6(log|t|)²/... 12 ≤ 12·(log|t|)²/(log 10)² ≤ 12/5.3·(log|t|)² ≤ 2.3(log|t|)². So bracket ≤ 3.3·(log|t|)², say ≤ 4·(log|t|)². Final: ‖R(s)‖ ≤ 100000(log|t|)² + 4(log|t|)²... hmm wait — actually ‖R(s)‖ ≤ ‖B‖ + ‖bracket‖ ≤ 100000 L² + 4 L² ≤ 100004 L². Round to a clean loose constant: 200000 · (log|t|)². Or just 100000·(log|t|)² + 4·(log|t|)² stated as is, or fold to 100010·(log|t|)². I'll fold to a round number ≥ the traced one: 110000·(log|t|)² — clean and safe. Actually, let me keep it simple: ≤ 100000·(log|t|)² + 4·(log|t|)² then ≤ 100004·(log|t|)²... For cleanliness in the theorem statement, I'll state with the folded constant 200000 (very round, obviously sufficient) or the traced 100004. Given \"constants don't propagate\", a round 200000 is fine and gives margin for proof slack. Hmm, but let me think about what 5e will use: it needs o(R) growth of F on circles; any polylog constant works. 200000 it is.\n\nNow the plan for the file: new file `LiReflect.lean` (ii′-5d) importing LiDisc. Structure:\n\n§1 FE logDeriv identity:\n- `logDeriv_completedZeta_eq_neg_logDeriv_completedZeta_one_sub`: logDeriv Λ s = −logDeriv Λ (1−s) (for s ≠ 0, 1 maybe not even needed — but deriv needs differentiability: differentiableAt_completedZeta needs s ≠ 0, s ≠ 1; at our s both fine).\n  Proof: Λ = fun s => Λ (1 − s) (funext completedRiemannZeta_one_sub — direction: completedRiemannZeta_one_sub : Λ (1−s) = Λ s; so (fun s => Λ (1−s)) = Λ). logDeriv Λ s = logDeriv (fun s => Λ (1−s)) s; deriv (fun s => Λ (1−s)) s = deriv Λ (1−s) * deriv (fun s => 1 − s) s = deriv Λ (1−s) * (−1). Hmm via `deriv.comp`: (h : DifferentiableAt ℂ Λ (1−s)) (h2 : DifferentiableAt ℂ (fun s => 1−s) s): deriv (Λ ∘ fun s => 1−s) s = deriv Λ (1−s) * deriv (fun s => 1−s) s? Actually `deriv.comp (hh : DifferentiableAt 𝕜' h (f₂ x)) (hf : DifferentiableAt 𝕜 f₂ x) : deriv (h ∘ f₂) x = deriv h (f₂ x) * deriv f₂ x`. And deriv (1 − ·) = −1: deriv_const_sub? `deriv_const_sub (hf : DifferentiableAt 𝕜 f x) : deriv (fun x => a - f x) x = -deriv f x`? with f = id: deriv (fun s => 1 − s) = fun _ => −1? There might be subtleties; journal-024 banked: deriv_add_const, deriv_const_mul, deriv_id'. For (1 − s): deriv_const_sub with differentiableAt_id. Let me just compute: show deriv (fun s : ℂ => 1 - s) s = -1. `deriv_const_sub differentiableAt_id : deriv (fun x => a - x) x = -1`? deriv_const_sub : deriv (fun x => a - f x) x = -deriv f x — check existence; else: deriv (fun s => 1 − s) = deriv ((fun _ => 1) − id)... = 0 − 1 = −1 via deriv_sub (differentiableAt_const) (differentiableAt_id) then deriv_const + deriv_id'. Fine.\n  Then logDeriv (Λ ∘ (1−·)) s = deriv(Λ∘(1−·)) s / Λ(1−s) = −deriv Λ (1−s)/Λ(1−s) = −logDeriv Λ (1−s).\n  But also Λ s = (Λ∘(1−·)) s, so logDeriv Λ s = −logDeriv Λ (1−s) ✓. (logDeriv f = deriv f / f by def — `logDeriv_def`? logDeriv f x = deriv f x / f x is the definition; simp lemma `logDeriv`... it's `logDeriv_apply`? The def unfolds via `logDeriv`.)\n\n- `logDeriv_Gammaℝ_mul_zeta`: logDeriv Λ s = logDeriv ΓR s + logDeriv ζ s for s ≠ 0, ΓR s ≠ 0, ζ s ≠ 0, differentiable. Via completedRiemannZeta_eq_Gammaℝ_mul (pointwise) + logDeriv_mul. Wait — completedRiemannZeta_eq_Gammaℝ_mul is POINTWISE (Λ s = ΓR s * ζ s), but logDeriv_mul needs the FUNCTION ΓR * ζ — logDeriv Λ s = logDeriv (ΓR * ζ) s requires Λ =ᶠ[𝓝 s] ΓR * ζ or Λ = ΓR * ζ as functions. Is Λ = ΓR * ζ globally? In Mathlib, `completedRiemannZeta s = Gammaℝ s * riemannZeta s` — actually Mathlib's riemannZeta is DEFINED via completedRiemannZeta / Gammaℝ for s ≠ 0? Mathlib: `riemannZeta_def_of_ne_zero (hs : s ≠ 0) : riemannZeta s = completedRiemannZeta s / Gammaℝ s`. So Λ s = ΓR s · ζ s whenever s ≠ 0 AND... the Zeta23 lemma does field_simp with riemannZeta_def_of_ne_zero: Λ = ΓR·(Λ/ΓR) needs ΓR ≠ 0. So globally: Λ = ΓR * ζ wherever s ≠ 0 and ΓR s ≠ 0 — but as functions they're not equal everywhere (at s = −2n). For logDeriv at our point s: need eventually-equal in 𝓝 s. Since the set {s : s ≠ 0 ∧ ΓR s ≠ 0} is open (ΓR continuous, nonzero set open) and contains our s, Λ =ᶠ[𝓝 s] ΓR * ζ? Actually equality on an open set gives EventuallyEq: h : ∀ s ∈ U, Λ s = ΓR s * ζ s, U open, s ∈ U ⟹ Λ =ᶠ[𝓝 s] (ΓR * ζ)... via `Filter.eventuallyEq_of_mem` hmm: EventuallyEq f g (𝓝 s) ↔ ∃ t ∈ 𝓝 s, ∀ x ∈ t, f x = g x: `Filter.eventuallyEq_iff_exists_mem`. Fine — small lemma: Λ =ᶠ[𝓝 s] ΓR * ζ for s ≠ 0, ΓR s ≠ 0 (continuity of ΓR: Complex.Gammaℝ continuous away from poles; is there `continuousAt_Gammaℝ`? or continuous_Gammaℝ? Actually ΓR is differentiable away from {−2n}... there should be differentiableAt_Gammaℝ. Let me grep.)\n  \n  Then: logDeriv Λ s = logDeriv (ΓR * ζ) s (EventuallyEq.logDeriv? — need EventuallyEq deriv_eq: h.deriv_eq : deriv f s = deriv g s, and h.eq_of_nhds : f s = g s, so logDeriv f s = logDeriv g s by simp [logDeriv_apply?]... logDeriv f x = deriv f x / f x definitionally: `logDeriv` def. rw [show deriv ... ] etc.)\n  = logDeriv ΓR s + logDeriv ζ s (logDeriv_mul with ΓR s ≠ 0, ζ s ≠ 0, both differentiable at s).\n  Differentiability of ΓR at s: need `differentiableAt_Gammaℝ`? In Zeta23 GammaSide: `hd.div hA.differentiableOn` where hA is... let me look at lines 40–63 of GammaSide.lean to see the differentiability lemmas used. Will grep.\n\n- Combine: logDeriv ζ s = −logDeriv ζ (1−s) − [logDeriv ΓR s + logDeriv ΓR (1−s)].\n  From: logDeriv ΓR s + logDeriv ζ s = logDeriv Λ s = −logDeriv Λ (1−s) = −(logDeriv ΓR (1−s) + logDeriv ζ (1−s)).\n  The second application needs at 1−s: 1−s ≠ 0 (re(1−s) ≥ 1/2 > 0 ✓... actually just im ≠ 0), ΓR (1−s) ≠ 0 (re > 0 ✓), ζ (1−s) ≠ 0 (proved via Λ route ✓), differentiability at 1−s (1−s ≠ 0, ≠ 1: 1−s = 1 ⟺ s = 0, but im s = t ≠ 0 ✓).\n  Then rearrange (abel/ring on ℂ).\n\n§2 zero-sum cancellation:\n- `one_sub_mem_nearZeros_neg` : ρ ∈ nearZeros t → 1 − ρ ∈ nearZeros (−t).\n- `nearZeros_neg_eq_image : nearZeros (−t) = (nearZeros t).image (fun ρ => 1 − ρ)`.\n- `zeroMult_one_sub : ρ ∈ nearZeros t → zeroMult (1 − ρ) = zeroMult ρ` (via analyticOrderAt_zeta_one_sub; need the exact Zeta23 signature).\n- `nearZero_sum_reflect : ∑ ρ' ∈ nearZeros (−t), (zeroMult ρ' : ℂ)/(s − ... )`... directly:\n  `sum_reflect_neg : ∑ ρ' ∈ nearZeros (−t), (zeroMult ρ' : ℂ) / (1 - s - ρ') = -∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)`.\n  Proof: rw [nearZeros_neg_eq_image, Finset.sum_image (injOn: (1−·) injective — `Function.Injective.injOn` with `Function.injective_iff_hasLeftInverse`... (fun ρ => 1 − ρ) is injective: add_left_injective? `fun a b h => by ...`: 1 − a = 1 − b ⟹ a = b via `sub_left_injective`? In Lean: (fun ρ : ℂ => 1 − ρ) injective: `Function.Injective` by intro a b h; linarith? No — complex: `sub_left_inj.mp`? 1 − a = 1 − b ↔ a = b: `sub_left_inj` says a − b = a − c ↔ b = c. So h : 1 − a = 1 − b, exact sub_left_inj.mp h : a = b? sub_left_inj : a − b = a − c ↔ b = c — with a := 1 ✓.)]\n  Then the sum over image: Σ_{ρ ∈ nearZeros t} zeroMult (1−ρ)/(1−s−(1−ρ)) = Σ zeroMult ρ / (−(s−ρ)) = −Σ zeroMult ρ/(s−ρ). With zeroMult_one_sub for the multiplicities and 1−s−(1−ρ) = −(s−ρ) by ring, div_neg, sum_neg. ✓\n\n§3 ΓR-bracket evaluation + bound:\n- `logDeriv_Gammaℝ_add_four` : for s with s ≠ 0, s ≠ −2 (or the specific region): logDeriv ΓR s = logDeriv ΓR (s+4) − 2*(s+1)/(s*(s+2)). Via the local product identity.\n  Actually more precisely the plan: EventuallyEq ΓR (fun s => (π:ℂ)² * ΓR (s+4) / P s) in 𝓝 s where P s = (s/2)*(s/2+1). Prove the EventuallyEq on the set U = {s | s ≠ 0 ∧ s ≠ −2} (open — complement of finite set, isOpen_compl_singleton twice; actually {0,−2}ᶜ open).\n  On U: ΓR(s+4) = π^{−(s+4)/2} Γ((s+4)/2); (s+4)/2 = s/2 + 2; Γ(s/2+2) = (s/2+1)(s/2)Γ(s/2) (two recurrences, valid since s/2 ≠ 0 (s ≠ 0) and s/2 + 1 ≠ 0 (s ≠ −2)); π^{−(s+4)/2} = π^{−s/2}·π^{−2} (cpow_add needs... π real positive: Complex.cpow_add for real base? (π:ℂ)^{a+b} = π^a · π^b when π > 0 real: `Complex.cpow_add`? general cpow_add needs conditions (arg); for positive real base use `Complex.ofReal_cpow`... hmm: (π:ℂ)^x = exp(x log π) for complex x with π real positive — via `Complex.cpow_eq_exp_log_of...`? There's `Complex.ofReal_cpow (hx : 0 ≤ x)`: ((x:ℝ):ℂ)^y = (x^y.re ...) no. Cleanest: (π:ℂ)^{w} = Real.exp (w.re · log π) · ... no. Use: for r > 0 real, (r:ℂ)^(z) = (r^(z : ℂ))... `Complex.ofReal_cpow`? I recall `Complex.ofReal_cpow (hr : 0 ≤ r) (z : ℂ) : (r : ℂ) ^ z = ↑(r ^ z.re) * ...`? Hmm no.\n  \n  Simpler: avoid cpow arithmetic by factoring: ΓR(s+4)/ΓR(s) = π^{−(s+4)/2 + s/2} · Γ(s/2+2)/Γ(s/2) = π^{−2}·(s/2+1)(s/2). The ratio form: ΓR(s+4)/ΓR(s) where ΓR s ≠ 0. π^{−(s+4)/2}/π^{−s/2} = π^{−(s+4)/2 − (−s/2)} = π^{−2}: via `Complex.cpow_sub`? Also needs conditions. For positive real base there's `Complex.ofReal_cpow_sub`? Hmm. There IS: `Complex.ofReal_cpow (hx : 0 ≤ x) (y : ℂ) : (↑x) ^ y = ↑(x ^ (y.re)) * ...`? no that's not right either.\n  \n  Cleanest known-good: (π:ℂ)^{w} = Complex.exp (w * Real.log π) when... `Complex.cpow_def_of_ne_zero`: z^w = exp(w log z) for z ≠ 0. And Complex.log (π:ℂ) = Real.log π (Complex.log_ofReal? `Complex.ofReal_log (hx : 0 ≤ x) : Complex.log ↑x = ↑(Real.log x)`). So (π:ℂ)^w = exp(w·(log π : ℝ)) for all w. Then the ratio arithmetic is pure exp: exp(a)·exp(b) = exp(a+b) (Complex.exp_add). This is the robust route: convert all (π:ℂ)^(·) to exp form. `Complex.cpow_def_of_ne_zero (x : ℂ) (hx : x ≠ 0) (y : ℂ) : x ^ y = Complex.exp (Complex.log x * y)`? signature: cpow_def_of_ne_zero (hx : x ≠ 0) (y) : x ^ y = exp (log x * y). Hmm arg order — check. Then π^{−s/2} = exp(log π · (−s/2)), π^{−(s+4)/2} = exp(log π · (−(s+4)/2)) = exp(log π · (−s/2) − 2 log π) = π^{−s/2}·exp(−2 log π) and exp(−2 log π) = π^{−2} real. OK.\n  \n  Then the logDeriv computation: ΓR =ᶠ[𝓝 s] fun s => ΓR (s+4) / (π^{−2} · P s)? or =ᶠ fun s => (π:ℂ)² * ΓR (s+4) / P s. Let me define the eventually-equal function as G s := (Real.pi : ℂ)^2 * ΓR (s + 4) / ((s/2) * (s/2 + 1))... wait, we need ΓR s = π² · ΓR(s+4)/P(s): from ΓR(s+4) = π^{−2} P(s) ΓR(s) ⟹ ΓR(s) = π² ΓR(s+4)/P(s) (field, P(s) ≠ 0 on U: s/2 ≠ 0 and s/2+1 ≠ 0 ⟹ product ≠ 0 ✓).\n  \n  logDeriv ΓR s = logDeriv G s (EventuallyEq) = logDeriv (fun s => π² * ΓR (s+4)) s − logDeriv (fun s => (s/2)*(s/2+1)) s (logDeriv_div: needs numer/denom differentiable + nonzero at s).\n  - logDeriv (π² * ΓR(s+4)) = logDeriv (const) + logDeriv (ΓR(s+4)) = 0 + logDeriv ΓR (s+4) (logDeriv_mul: π² ≠ 0; deriv comp: deriv (ΓR ∘ (·+4)) s = deriv ΓR (s+4) * deriv (·+4) s = deriv ΓR (s+4) * 1; then logDeriv (ΓR(s+4)-fn) s = deriv ΓR (s+4)/ΓR (s+4) = logDeriv ΓR (s+4)).\n    Hmm wait — logDeriv_mul : logDeriv (f * g) x = logDeriv f x + logDeriv g x. With f = const π², g = ΓR(·+4). deriv f = 0 ⟹ logDeriv f s = 0/π² = 0 ✓ (logDeriv_const? there's `logDeriv_const : logDeriv (fun _ => c) = 0`? or compute). \n  - logDeriv (fun s => (s/2)*(s/2+1)) s = deriv (...) s / ((s/2)*(s/2+1)): deriv = (1/2)(s/2+1) + (s/2)(1/2) = s/2 + 1/2 via deriv_mul (both factors differentiable). Then the ratio = (s/2+1/2)/((s/2)(s/2+1)) = 2(s+1)/(s(s+2)) (field_simp, s ≠ 0, s ≠ −2).\n  \n  So: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) — under hypotheses s ≠ 0, s ≠ −2, plus differentiability of ΓR at s+4 and ΓR (s+4) ≠ 0... For our s: re(s+4) > 0 ⟹ differentiableAt ΓR ✓ and ΓR (s+4) ≠ 0 by Gammaℝ_ne_zero_of_re_pos ✓.\n  \n  Hmm wait, one catch: the EventuallyEq.route requires ΓR differentiable at s for... no — logDeriv ΓR s = logDeriv G s via EventuallyEq.deriv_eq which needs NO differentiability (deriv f s = deriv g s when f =ᶠ[𝓝 s] g — actually is that right? Filter.EventuallyEq.deriv_eq : f =ᶠ[𝓝 x] g → deriv f x = deriv g x — yes pointwise, journal-024 banked it). ✓. Then logDeriv G s computed via rules needing G's factors differentiable at s: ΓR(·+4) at s ⟸ ΓR at s+4 ✓ (re > 0), polynomials ✓.\n  Then also the original goal \"logDeriv ΓR s\" — we never need differentiability of ΓR AT s itself! Good, because ΓR at s with re s ∈ [−5/2, 1/2] is differentiable (s ∉ {−2n}) but we might not even need to cite it.\n  \n  Wait — but in the FE identity I DO need ΓR differentiable at s for logDeriv_mul (Λ = ΓR * ζ). differentiableAt_Gammaℝ: exists? grep. If Mathlib has `differentiableAt_Gammaℝ (s : ℂ) : DifferentiableAt ℂ Gammaℝ s`?? Gammaℝ = π^{−s/2}Γ(s/2): Γ has poles; Gammaℝ differentiable at s iff s/2 not a pole... Actually Complex.Gamma differentiability: `Complex.differentiableAt_Gamma : DifferentiableAt ℂ Complex.Gamma s`? Hmm — Complex.Gamma is defined via the limit formula; Mathlib has `Complex.differentiableAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m)`? something like that. And Gammaℝ: `Complex.differentiableAt_Gammaℝ`? Let me grep both Mathlib and Zeta23.\n\n§4 digamma bounds:\n- `norm_log_le : ‖Complex.log w‖ ≤ |Real.log ‖w‖| + Real.pi`? — check Mathlib: `Complex.norm_log_le (z : ℂ) : ‖Complex.log z‖ ≤ |Real.log ‖z‖| + Real.pi`? Hmm, actually I don't think that exact one exists; there IS `Complex.norm_log (z : ℂ) : ‖Complex.log z‖ = ‖(Real.log ‖z‖, Complex.arg z)‖`? no... Let me grep. If missing: log w = ↑(Real.log ‖w‖) + ↑(arg w)·I (Complex.log_def / `Complex.log_apply`? there's `Complex.log_re : (log z).re = Real.log ‖z‖` and `Complex.log_im : (log z).im = arg z`). Then ‖log w‖ ≤ |(log w).re| + |(log w).im| (Complex.norm_le_abs_re_add_abs_im) ≤ |Real.log ‖w‖‖ + π (abs_arg_le_pi). ✓ manageable.\n- `norm_digamma_sub_log_le` : for w, 0 < re w, 1/2 ≤ |im w|: ‖ψ(w) − log w‖ ≤ 3/(im w)² + 1/(2‖w‖) — immediate from digamma_stirling + triangle.\n- Then the two instantiations + the full bracket bound `norm_GammaR_bracket_le` : ‖logDeriv ΓR (1−s) + logDeriv ΓR s‖ ≤ 2·log|t| + 12 (say), for our region.\n\n§5 left-plane digamma (separate): `norm_digamma_sub_log_le_of_im` : for w with 2 ≤ |w.im| (or maybe I should allow the shift to land with re ∈ [1,2] and use StirlingVert on w+n: needs |im| ≥ 1/2 ✓ since im(w+n) = im w):\n  ‖digamma w − Complex.log w‖ ≤ C for some explicit C (e.g., 4).\n  Steps: n := ⌈−re w⌉₊ + 2 (Nat.ceil of −re w... need w + n to have re ≥ ... let me choose n := ⌈max 0 (−re w + 2)⌉? Simpler: n := ⌈|re w|⌉₊ + 2: then re(w + n) = re w + n ≥ re w + |re w| + 2 ≥ 2 > 0 ✓. Also |im(w+n)| = |im w| ≥ 2 ≥ 1/2 ✓.\n  - ψ(w+n) = ψ(w) + Σ_{j=0}^{n−1} 1/(w+j): induction with digamma_apply_add_one; each step needs w + j ≠ 0 ✓ (|im| ≥ 2). Finset sum: digamma (w + n) = digamma w + Σ_{j ∈ range n} (w + j)⁻¹. Induction on n: base n=0 trivial; step: digamma (w + (n+1)) = digamma (w+n) + (w+n)⁻¹ = digamma w + Σ_{j<n+1}. Careful with casts: (w + (n:ℂ)) etc.\n  - EM comparison: Σ_{j=0}^{n−1} (w+j)⁻¹ = ∫₀ⁿ (w+x)⁻¹ dx + ((w)⁻¹ − (w+n)⁻¹)/2 + ∫₀ⁿ B̃₁(x)·(−(w+x)⁻²) dx.\n    In Lean: per-interval trapezoid IBP. What exists in Zeta23 EulerMaclaurin.lean: `integral_deriv_mul_add_const`? Let me look at the file and what ii′-5b used. ii′-5b built b1Fun machinery in LiRBound.lean. Let me check LiRBound.lean for reusable per-interval IBP: it has `integral_b1_cpow_eq` (specific to x^{−s−2}?). Might need a new general-ish IBP for f(x) = (w+x)⁻¹. Let me look at the existing pattern and clone.\n    The integral: ∫₀ⁿ (w+x)⁻¹ dx = Complex.log (w+n) − Complex.log w: FTC with F(x) = Complex.log (w + ↑x), F′(x) = (w+x)⁻¹ (HasDerivAt: Complex.log differentiable at w+x since w+x ∈ slit plane: im ≠ 0 ⟹ `Complex.hasDerivAt_log (h : x ∈ slitPlane)`? there's `hasDerivAt_log (hx : x ≠ 0) (hπ : x.arg ≠ π)`? or slitPlane membership: Complex.slitPlane = ℂ ∖ {x | x.im = 0 ∧ x.re ≤ 0}: `Complex.hasDerivAt_log (hx : x ∈ Complex.slitPlane)`. im(w+x) = im w ≠ 0 ⟹ w+x ∈ slitPlane ✓. deriv log = x⁻¹: `Complex.deriv_log`? hasDerivAt_log gives derivative x⁻¹ ✓.)\n    Then intervalIntegral FTC: ∫₀ⁿ (w+x)⁻¹ dx = log(w+n) − log w — real interval integral of complex function: `intervalIntegral.integral_eq_sub_of_hasDerivAt` (needs continuity of derivative + HasDerivAt on the interval). ✓ pattern exists.\n    The B̃₁ remainder integral: ‖∫₀ⁿ B̃₁(x)·(−(w+x)⁻²) dx‖ ≤ ∫₀ⁿ (1/2)·‖w+x‖⁻² dx ≤ (1/2)·∫₀ⁿ dx/((re w + x)² + (im w)²) ... hmm: ‖w + x‖² ≥ (re(w+x))² + ... we need 1/‖w+x‖² ≤ 1/((re w + x)² + (im w)²) — equality actually: ‖w+x‖² = (re w + x)² + (im w)² (normSq). So ∫₀ⁿ dx/((x+a)² + c²) where a = re w, c = |im w| ≥ 2. Bound by ∫_ℝ = π/c: `∫ (x:ℝ), 1/(x^2 + c^2) = π/c` — Mathlib: `integral_one_div_add_sq`? There is `MeasureTheory.integral_one_div_one_add_sq : ∫ x, (1:ℝ)/(1+x^2) = π` hmm or `Real.integral_...`? I recall `∫ x in , 1 / (x^2 + 1) = π` exists (`integral_one_div_one_add_sq`). For 1/((x+a)² + c²): substitute y = (x+a)/c: = (1/c)∫ dy/(y²+1) = π/c. In Lean: do the substitution via... this could be painful. ALTERNATIVE: skip the integral comparison; bound the SUM directly:\n    ‖Σ_j (w+j)⁻¹ − (log(w+n) − log w)‖ ≤ (1/2)(‖w‖⁻¹ + ‖w+n‖⁻¹) + Σ_{j=0}^{n−1} ‖(w+j)⁻¹ − (log(w+j+1) − log(w+j))‖? no — same telescope issue but now per-interval it's fine: per interval [j, j+1]: ∫_j^{j+1} (w+x)⁻¹ dx = log(w+j+1) − log(w+j) (FTC, slit plane ✓ — no pole on the path since im ≠ 0). And the per-interval EM: (w+j)⁻¹ = ∫_j^{j+1}(w+x)⁻¹dx + [boundary] + remainder... per interval trapezoid: ∫_j^{j+1} f = (f(j)+f(j+1))/2 − ∫_j^{j+1} B̃₁ f′. Sum: ∫₀ⁿ f = Σ_{j=0}^{n−1}(f(j)+f(j+1))/2 − ∫₀ⁿ B̃₁ f′ = (f(0)+f(n))/2 + Σ_{j=1}^{n−1} f(j) − ∫ B̃₁ f′. So Σ_{j=0}^{n−1} f(j) = ∫₀ⁿ f + (f(0) − f(n))/2 + ∫₀ⁿ B̃₁ f′ ✓ (same as before).\n    So I do need ∫₀ⁿ ‖B̃₁(x) (w+x)⁻²‖ dx ≤ (1/2)∫₀ⁿ ((x+a)² + c²)⁻¹ dx. For the integral bound, instead of evaluating π/c, use: ((x+a)² + c²)⁻¹ ≤ c⁻² pointwise, but ∫₀ⁿ c⁻² dx = n/c² ~ R/4 — TOO BIG (need O(1)). So the comparison must capture the peak-decay. Options: split the interval around x = −a... \n    Hmm, alternatively: bound ∫₀ⁿ ((x+a)²+c²)⁻¹ dx ≤ ∫_ℝ ((x+a)²+c²)⁻¹ dx = π/c via: the integrand is positive; ∫₀ⁿ ≤ ∫_ℝ if we can show the full-line integral exists and dominates partial ones. In Lean, the full-line integral of 1/((x+a)² + c²): substitution u = x + a: `MeasureTheory.integral_comp_add_right`? There are translation lemmas: `integral_comp_add_right (f) (a) : ∫ x, f (x + a) = ∫ x, f x`. Then ∫ (u² + c²)⁻¹ du over ℝ = π/c: via (u/c)²: ∫ 1/(u²+c²) du = (1/c)∫ 1/((u/c)²+1) du = (1/c)·c·∫ 1/(y²+1) dy (u = cy): `integral_comp_div`? `MeasureTheory.integral_comp_div (f) (hc : c ≠ 0) : ∫ x, f (x/c) = c * ∫ f`? something like that. Then `integral_one_div_one_add_sq : ∫ y, 1/(1+y²) = π`? I believe `Real.integral_one_div_one_add_sq : ∫ (x : ℝ), 1 / (1 + x^2) = Real.pi` hmm or is it `MeasureTheory.integral_one_div_one_add_sq`? I think it exists in Mathlib (used for arctan). \n    Then ∫₀ⁿ ≤ ∫_ℝ: for a nonneg integrable f, intervalIntegral ≤ full: `intervalIntegral.integral_le_integral...`? hmm: ∫ x in 0..n, f x ≤ ∫ x, f x for f ≥ 0 integrable: `intervalIntegral.integral_mono_interval`? There might be `intervalIntegral.integral_le_integral_of_nonneg`... Or: ∫₀ⁿ = ∫ indicator, ≤ ∫ f by `MeasureTheory.integral_mono_ae` with setIntegral_le_integral: `MeasureTheory.setIntegral_le_integral (hf : Integrable f) (h : 0 ≤ᵐ f) : ∫ x in s, f x ≤ ∫ x, f x` ✓ that exists. And intervalIntegral = setIntegral over Ioc/uIoc. Fine.\n    This is all doable but it's a chunk of real-analysis plumbing. Estimated: this digamma-uniform bound is maybe 300–500 lines.\n\n    Hmm wait — actually, maybe I should double check whether Zeta23 already HAS a left-plane digamma bound somewhere (ZeroCount/Y.lean or StirlingVert for the left plane). D-067 §4 inventory says: GammaFacts/Series.lean — digamma series + Weierstrass for 1/Γ (marked \"unused\"). The digamma SERIES: ψ(w) = −γ + Σ_{k≥0} (1/(k+1) − 1/(k+w))? With that, ψ(w) − log w... the series-vs-log comparison is exactly the same difficulty. Let me check what's in Series.lean and Y.lean for left-plane bounds. Actually `norm_digamma_le` (‖ψ(w)‖ ≤ ‖w‖+8) was in XiPrime/ZeroCount/Y.lean — that's right-half-plane presumably. Let me grep for left-plane digamma in Zeta23.\n\nLet me also reconsider: maybe simpler to prove the uniform bound via the recurrence + the series bound per-term with telescoping IN NORM: ‖Σ_{j=0}^{n−1} (w+j)⁻¹ − (log(w+n) − log w)‖ ≤ Σ_j ‖(w+j)⁻¹ − (log(w+j+1) − log(w+j))‖ and per-term: log(w+j+1) − log(w+j) = log((w+j+1)/(w+j)) = log(1 + (w+j)⁻¹) — branch: since im(w+j) and im(w+j+1) have the same sign (both = im w), arg difference in (−π, π) — Mathlib: `Complex.log_div (hx : x.im ≠ 0) (hy : y.im ≠ 0)`? Hmm — I recall `Complex.log_div (h₁ : x.im ≠ 0) (h₂ : y.im ≠ 0) : log (x / y) = log x - log y`?? no wait, that can't hold for x = y = −1: log(1) = 0, log(−1) − log(−1) = 0 ✓; x = −1, y = 1: log(−1) = iπ, log(−1) − log(1) = iπ ✓; x = 1, y = −1: log(−1) = iπ vs log 1 − log(−1) = −iπ ✗. So the condition must be stronger: same-sign im? x = 1·i, y = −1·i: log(−1) = iπ; log(i) − log(−i) = iπ/2 − (−iπ/2) = iπ ✓. Seems same-sign im works: arg x, arg y ∈ (0, π) or both in (−π, 0), difference in (−π, π), and log(x/y) = log‖x/y‖ + i arg(x/y) with arg(x/y) ≡ arg x − arg y (mod 2π), both in (−π, π]... the difference could be exactly π? |arg x − arg y| < π strictly when same strict sign. And arg(x/y) = the unique value in (−π, π] congruent — equal to the difference ✓. I think Mathlib has `Complex.log_div (hx : x.im ≠ 0) (hy : y.im ≠ 0)` requires SAME sign? Let me grep Mathlib for \"log_div\".\n    Then per-term: ‖(w+j)⁻¹ − log(1 + (w+j)⁻¹)‖ ≤ ‖(w+j)⁻¹‖² for ‖(w+j)⁻¹‖ ≤ 1/2 (Mathlib: `Complex.norm_log_one_add_sub_self_le`? grep \"log_one_add\" in Mathlib: `Complex.norm_log_one_add_le : ‖Complex.log (1 + z)‖ ≤ -Real.log (1 - ‖z‖)` for ‖z‖ < 1? and maybe `Complex.norm_log_one_add_sub_self_le : ‖z‖ ≤ 1/2 → ‖Complex.log (1+z) − z‖ ≤ ‖z‖^2`? I think there's something close; grep).\n    Then Σ_j ‖w+j‖⁻² ≤ Σ_j 1/((re w + j)² + (im w)²) — SAME sum bound problem as the integral. No escape from the sum/integral comparison. The integral route via EM is cleaner given machinery exists.\n\n    Actually — hmm, one more idea for the sum bound Σ_{j=0}^{n−1} 1/((j+a)² + c²) ≤ (π/c + 1/c²): the function x ↦ 1/((x+a)²+c²) is unimodal. Compare with integral: for j ≠ ⌈−a⌉... The cleanest classical: Σ_{j∈[0,n]} 1/((j+a)²+c²) ≤ 1/c² + ∫_{−∞}^{∞} du/(u²+c²) = 1/c² + π/c. In Lean via `sum_le_integral`-type: for monotone pieces. Two monotone pieces (split at the peak) — `Antitone.sum_le_integral`/`Monotone.integral_le_sum`-style lemmas exist in Mathlib (`Monotone.sum_le_integral`? in Mathlib.Analysis.SumOverInterval / `sum_le_integral_of_monotone`?). Fiddly but standard.\n\n    OR — completely sidestep: use the digamma SERIES from Zeta23 GammaFacts/Series.lean and compare Σ_k [1/(k+1) − 1/(k+w)] against log directly with the same sum-comparison problem. Same difficulty.\n\n    OR — avoid the uniform digamma bound's use of the recurrence entirely: for 5e's needs maybe |im w| ≥ 2 is automatically available? On the γ-gap circles, the left-plane points: re s ~ −R, im s = anything in [−R, R]. The circle crosses im = 0. So no.\n\n    OK let me just scope §5 honestly: it's a self-contained real/complex estimate, ~0.5 session. The main 5d theorem (A–D) doesn't depend on §5. Plan: do §1–§4 first (the FE reflection R-bound), then §5 (left-plane digamma) as time allows; it can slip to its own sub-stage per STATE.md (\"Also needed for 5d/5e: ... and zeroMult(−2n) = 1 for all n\" — the zeroMult generalization is explicitly allowed to slip: \"can slip to its own sub-stage\"). The digamma bound is listed as part of 5d. I'll attempt both; if §5 balloons, slip it.\n\nAlso the oddball: zeroMult(−2n) = 1 for all n — needed for 5e, can slip. Not in 5d critical path. STATE says \"Also in scope for 5e prep (can slip to its own sub-stage)\". OK.\n\nLet me now check the remaining API questions with greps:\n1. differentiableAt Gammaℝ / Complex.Gamma in Mathlib/Zeta23.\n2. logDeriv_mul exact signature.\n3. analyticOrderAt_zeta_one_sub exact statement (line 224 of ZetaReflect.lean).\n4. digamma_apply_add_one exact statement.\n5. Complex.log_div / norm_log_one_add lemmas.\n6. The namespace of StirlingVert.digamma_stirling.\n7. norm_digamma_le location (Y.lean) — maybe useful patterns.\n8. What ii′-5b's LiRBound.lean has for IBP helpers (integral_b1_cpow_eq — is it general?).\n9. EulerMaclaurin.lean helpers (integral_deriv_mul_add_const).\n10. logDeriv_const, logDeriv_div signatures.\n\nLet me batch these greps.","signature":""},{"type":"text","text":"All seams confirmed in Zeta23. Now let me verify the exact API signatures I'll need."},{"type":"tool_use","id":"Bash_18","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean && sed -n '220,240p' Zeta23/ZetaReflect.lean && echo === && grep -n \"namespace\\|theorem digamma_stirling\" Zeta23/GammaFacts/StirlingVert.lean | head -8 && echo === && grep -rn \"differentiableAt_Gammaℝ\\|differentiable_Gammaℝ\" --include=\"*.lean\" Zeta23/ .lake/packages/mathlib/Mathlib/Analysis/SpecialFunctions/Gamma/ 2>/dev/null | head -5","description":"Check analyticOrderAt_zeta_one_sub, StirlingVert namespace, Gammaℝ differentiability"},"extra_content":null},{"type":"tool_use","id":"Bash_19","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem logDeriv_mul\\|theorem logDeriv_div\\|theorem logDeriv_const\\b\\|lemma logDeriv_mul\\|lemma logDeriv_div\" Mathlib/Analysis/Calculus/LogDeriv.lean | head && grep -rn \"digamma_apply_add_one\" Mathlib/Analysis/SpecialFunctions/Gamma/*.lean | head -3 && grep -rn \"theorem log_div\\|lemma log_div\\b\\|norm_log_one_add\" Mathlib/Analysis/SpecialFunctions/Complex/Log*.lean Mathlib/Analysis/SpecialFunctions/Log/*.lean 2>/dev/null | head -8","description":"Check logDeriv rules, digamma recurrence, log_div and log_one_add bounds in Mathlib"},"extra_content":null}]