Session 26 — Go-ahead for ii′-5c

The user says "Yes let's do it" — presumably in response to something from a previous conversation. I need to check STATE.md to see what the next action is. Per the session start protocol: read STATE.md first, then latest journal entry + results/index.md. The last session (024) ended with ii′-5c COMPLETE, next: ii′-5d (FE-reflection + left digamma bound). The user is likely approving continuing to the next sub-stage: ii′-5d. Let me read STATE.md first.

Good. Key seams found: - `RvM.completedRiemannZeta_eq_Gammaℝ_mul` (CountByIntegral.lean:41) - `completedRiemannZeta_one_sub` (Mathlib) - `completedRiemannZeta_eq_zero_iff` (CountByIntegral.lean:65) — likely `completedRiemannZeta s = 0 ↔ (riemannZeta s = 0 ∧ 0 < s.re ∧ s.re < 1)` or similar. Let me check. - `RvM.GammaSide.logDeriv_Gammaℝ` (GammaSide.lean:65) and `WeilEF.GammaRBracket.logDeriv_Gammaℝ` (GammaRBracket.lean:53) — two versions; GammaRBracket.lean is probably the bracket form I need. - `StirlingVert.digamma_stirling` (StirlingVert.lean:483): `(hw : 0 < w.re) (ht : 1/2 ≤ |w.im|) : ‖digamma w - log w + 1/(2w)‖ ≤ 3/w.im²` — need exact statement. Let me read these key files. Also check `zeroMult` definition and `zeroDiscFinset`, plus LiContour's `zeroMult_neg_two` for the trivial-zero generalization. And the GammaRBracket theorem.

Excellent! Mathlib has `AnalyticAt.analyticOrderAt_comp` and `AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero` (line 565 of Order.lean context). Let me read that section to get exact signatures.

All seams confirmed: - `Complex.Gamma_add_one (s : ℂ) (h2 : s ≠ 0) : Gamma (s+1) = s * Gamma s` — only needs s ≠ 0! Interesting — so Mathlib's Gamma recurrence holds at all s ≠ 0 (junk-consistent). - `Complex.digamma_apply_add_one (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m) : digamma (s+1) = digamma s + 1/s` presumably. Let me check the exact RHS. Line 55 of Digamma.lean. - `Complex.Gamma_ne_zero {s} (hs : ∀ m, s ≠ -m) : Gamma s ≠ 0`. - `Complex.differentiableAt_Gamma (s) (hs : ∀ m, s ≠ -m)`. - `digamma_stirling (hw : 0 < w.re) (ht : 1/2 ≤ |w.im|) : ‖digamma w − log w + (1/2)/w‖ ≤ 3/w.im²`. Note the `+ (1/2)/w` form. For Gammaℝ differentiability: need `differentiableAt Complex.Gammaℝ s` for s/2 ∉ −ℕ. Is there `differentiableAt_Gammaℝ`? Zeta23 used `differentiable_Gammaℝ_inv` (the inverse is entire). For Γℝ itself: Gammaℝ s = π^{−s/2} Γ(s/2) — differentiable when Γ(s/2) is, i.e. s/2 ∉ {0,−1,…}. Let me grep for a Mathlib/Zeta23 differentiableAt_Gammaℝ. In GammaRBracket.lean they proved logDeriv_Gammaℝ with explicit differentiability of the factors. There's likely `Complex.differentiableAt_Gammaℝ`. Let me check. Also need `digamma_apply_add_one`'s exact statement, and to check `logDeriv_mul`, `logDeriv_comp` signatures (used in GammaRBracket — they exist). And `Complex.Gammaℝ_def`. Let me also check what LiContour.lean's zeroMult_neg_two looks like for the trivial-zero generalization, and check `analyticOrderAt_comp_of_deriv_ne_zero` usability: it needs `[CompleteSpace 𝕜] [CharZero 𝕜]` — fine for ℂ. And f doesn't even need to be analytic! Great: analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) with g = fun s => 1 − s, deriv = −1. Wait, one subtlety: analyticOrderNatAt = (analyticOrderAt ...).toNat. zeroMult ρ := (analyticOrderAt riemannZeta ρ).toNat. For Λ: analyticOrderNatAt_completedRiemannZeta says analyticOrderNatAt Λ ρ = zeroMult ρ where analyticOrderNatAt Λ ρ := (analyticOrderAt Λ ρ).toNat. Fine. Plan for zeroMult_one_sub {ρ} (hρ : IsNontrivialZero ρ) : zeroMult (1−ρ) = zeroMult ρ: - have h1 : analyticOrderNatAt Λ (1−ρ) = zeroMult (1−ρ) := analyticOrderNatAt_completedRiemannZeta (re(1−ρ) = 1−re ρ > 0 since re ρ < 1) (1−ρ ≠ 1 since ρ ≠ 0 — ρ ≠ 0 from re ρ > 0). - have h2 : analyticOrderNatAt Λ ρ = zeroMult ρ := analyticOrderNatAt_completedRiemannZeta hρ.2.1 (ρ ≠ 1 from re ρ < 1). - key: analyticOrderAt Λ (1−ρ) = analyticOrderAt Λ ρ: Λ = (fun s => Λ (1−s)) pointwise (completedRiemannZeta_one_sub s : Λ (1−s) = Λ (s) — check direction: Mathlib `completedRiemannZeta_one_sub (s : ℂ) : completedRiemannZeta (1 - s) = completedRiemannZeta s` ✓). So analyticOrderAt Λ ρ = analyticOrderAt (fun s => Λ (1−s)) ρ = analyticOrderAt (Λ ∘ (fun s => 1−s)) ρ = analyticOrderAt Λ (1−ρ) by analyticOrderAt_comp_of_deriv_ne_zero (g = fun s => 1−s analytic, deriv = −1 ≠ 0). - Then toNat of both sides: analyticOrderNatAt Λ (1−ρ) = analyticOrderNatAt Λ ρ ⟹ zeroMult (1−ρ) = zeroMult ρ. ✓ Wait — is analyticOrderAt_comp_of_deriv_ne_zero in the root namespace or AnalyticAt? Line 561: `lemma analyticOrderAt_comp_of_deriv_ne_zero` — appears to be root namespace (no prefix). ✓. Its f has no analytic hypothesis — perfect, applies to Λ which IS analytic at 1−ρ anyway (re(1−ρ) ∈ (0,1), so ≠ 0, 1 ⟹ analyticAt_completedRiemannZeta). Also g = fun s : ℂ => 1 − s: AnalyticAt: analyticAt_const.sub analyticAt_id; deriv: deriv (1−·) ρ = −1: deriv_const_sub deriv_id' or hasDerivAt. deriv g ρ ≠ 0: compute via HasDerivAt.deriv: (hasDerivAt_id ρ).const_sub 1 → deriv = −1. Now the logDeriv FE identity. Exact Mathlib name for Λ's FE: `completedRiemannZeta_one_sub`. ✓ (used in Zeta23). **Lemma (logDeriv_zeta_FE)**: {s : ℂ} (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) (hζ1 : riemannZeta (1−s) ≠ 0) (hG : Complex.Gammaℝ s ≠ 0) (hG1 : Complex.Gammaℝ (1−s) ≠ 0) (hGdiff : DifferentiableAt ℂ Complex.Gammaℝ s) (hGdiff1 : DifferentiableAt ℂ Complex.Gammaℝ (1−s)): logDeriv riemannZeta s = −logDeriv riemannZeta (1−s) − (logDeriv Complex.Gammaℝ s + logDeriv Complex.Gammaℝ (1−s)). Proof: - Λs ≠ 0: Λ s = Γℝ s · ζ s (completedRiemannZeta_eq_Gammaℝ_mul hs0 hG) ≠ 0 by mul_ne_zero hG hζ. - deriv equality: Λ =ᶠ[𝓝 s] (Λ ∘ (1−·))? Actually pointwise everywhere: (fun w => Λ (1−w)) = Λ by funext + one_sub. So deriv Λ s = deriv (fun w => Λ (1−w)) s. Compute deriv (Λ ∘ (1−·)) s via deriv.comp: deriv Λ (1−s) · deriv (1−·) s = −deriv Λ (1−s). Needs DifferentiableAt Λ (1−s): (1−s) ≠ 0 (s ≠ 1), (1−s) ≠ 1 (s ≠ 0) ⟹ differentiableAt_completedZeta. And differentiableAt (1−·). Mathlib `deriv.comp` : deriv (h ∘ h₂) x = deriv h (h₂ x) * deriv h₂ x needs DifferentiableAt at the points. There's `deriv_comp`? In Mathlib: `deriv.comp (hh : DifferentiableAt 𝕜 h (h₂ x)) (hh₂ : DifferentiableAt 𝕜 h₂ x) : deriv (h ∘ h₂) x = deriv h (h₂ x) * deriv h₂ x`. ✓ - So logDeriv Λ s = deriv Λ s / Λ s = (−deriv Λ (1−s))/Λ(1−s) = −logDeriv Λ (1−s). (Λ s = Λ (1−s) by one_sub.) - logDeriv Λ s = logDeriv Γℝ s + logDeriv ζ s: logDeriv_mul s hG hζ hGdiff (differentiableAt_riemannZeta hs1?) — need DifferentiableAt ℂ riemannZeta s: `differentiableAt_riemannZeta (hs : s ≠ 1)` ✓ (used in Zeta23 as analyticAt_riemannZeta_of_ne_one; there's differentiableAt_riemannZeta in Mathlib ✓). logDeriv_mul signature (from GammaRBracket usage): `logDeriv_mul s hpow_ne hGne hdiff_pow hdiff_G : logDeriv (f * g) s = logDeriv f s + logDeriv g s` — but Λ s = Γℝ s * ζ s is only proved as a pointwise eq at s, not an eventual eq of functions! logDeriv_mul applies to the PRODUCT FUNCTION (fun w => Γℝ w * ζ w). Its logDeriv at s: deriv (Γℝ * ζ) s / (Γℝ s * ζ s). Is deriv of the product function equal to deriv Λ at s? Need Λ =ᶠ[𝓝 s] (Γℝ * ζ as functions). completedRiemannZeta_eq_Gammaℝ_mul holds at every w ≠ 0 with Γℝ w ≠ 0. Γℝ w ≠ 0 on a neighborhood? Γℝ zeros: Gammaℝ_eq_zero_iff says Γℝ w = 0 ↔ ∃ n, w = −2n (from usage at line 80: `Complex.Gammaℝ_eq_zero_iff` gives ⟨n, hn⟩ with ρ = −2n... let me double check what it states: probably Gammaℝ s = 0 ↔ ∃ n : ℕ, s = -2n. Yes, that's the Γ pole set). So on the punctured neighborhood of s avoiding {0} ∪ {−2n}: if s ∉ {0,−2,−4,…}, there's a neighborhood avoiding that discrete set where Γℝ w ≠ 0 and w ≠ 0, so Λ =ᶠ[𝓝 s] (fun w => Γℝ w * ζ w). Then EventuallyEq.deriv_eq (pointwise, banked gotcha) gives deriv Λ s = deriv (Γℝ*ζ) s, and eq_of_nhds gives value equality. Then logDeriv Λ s = logDeriv (Γℝ*ζ) s = logDeriv Γℝ s + logDeriv ζ s. For the (1−s) side similarly: logDeriv Λ (1−s) = logDeriv Γℝ (1−s) + logDeriv ζ (1−s), needs 1−s ∉ {0} ∪ {−2n}: 1−s = 0 ⟺ s = 1 excluded; 1−s = −2n: in our application re(1−s) ≥ 1/2 so fine, but for the general lemma I'll add hypothesis. Simplify: since the final application has |s.im| ≥ 10, s and 1−s are never in {0} ∪ −2ℕ. State hypotheses: (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hG : Gammaℝ s ≠ 0) (hG1 : Gammaℝ (1−s) ≠ 0) — from these, the EventuallyEq neighborhoods: need Γℝ w ≠ 0 near s. Γℝ s ≠ 0 + continuity of Γℝ at s ⟹ ≠ 0 in a neighborhood IF Γℝ continuous at s. Γℝ continuous at s when s/2 ∉ −ℕ (differentiableAt_Gammaℝ...). Hmm, but hG : Gammaℝ s ≠ 0 alone with s possibly = −2n+... if s = −2n then Γℝ s = 0 (excluded by hG); if s/2 ∈ −ℕ\{...}: s/2 = −m ⟺ s = −2m ⟹ Γℝ s = 0. So hG + Gammaℝ_eq_zero_iff ⟹ s ∉ {−2n} ⟹ differentiableAt Γℝ s (needs the Mathlib lemma) ⟹ continuous ⟹ nonzero nearby ✓. And w ≠ 0 near s since s ≠ 0. But wait: also need w avoiding zeros of Γℝ in the neighborhood to APPLY completedRiemannZeta_eq_Gammaℝ_mul at w: the formula needs (w ≠ 0) (Gammaℝ w ≠ 0) — both hold on the neighborhood ✓. So the identity lemma hypotheses: (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hζ : riemannZeta s ≠ 0) (hζ1 : riemannZeta (1−s) ≠ 0) (hG : Gammaℝ s ≠ 0) (hG1 : Gammaℝ (1−s) ≠ 0). From these derive differentiability of Γℝ at s, 1−s: need s/2, (1−s)/2 ∉ −ℕ: if s/2 = −m then s = −2m then Γℝ s = 0 contradiction. Need the direction: Gammaℝ s ≠ 0 ⟹ ∀ m, s/2 ≠ −m. From Gammaℝ_eq_zero_iff: Γℝ s = 0 ↔ ∃ n, s = −(2n)? Let me verify the exact statement of `Complex.Gammaℝ_eq_zero_iff`. grep Mathlib. Then in the assembly for our strip: hG : Gammaℝ s ≠ 0 with s.im = t, |t| ≥ 10: if Γℝ s = 0 then s = −2n real, im = 0 ≠ t... contradiction with |t| ≥ 10. ✓ hζ1 : ζ(1−s) ≠ 0: Λ(1−s) = Γℝ(1−s)·ζ(1−s); if ζ(1−s) = 0 then Λ(1−s) = 0 = Λ(s) = Γℝ(s)ζ(s) ≠ 0 contradiction. ✓ (needs 1−s ≠ 0 for the mul formula at 1−s: s ≠ 1 ✓ from im; Γℝ(1−s) ≠ 0: re(1−s) ∈ [1/2, 7/2] > 0 ⟹ Gammaℝ_ne_zero_of_re_pos ✓.) **Lemma (logDeriv_Gammaℝ shifted)**: for s with re s ≥ −5/2 (any), s ≠ 0, s ≠ −2 (junk-avoidance), Γℝ s ≠ 0, Γℝ (s+4) ≠ 0: logDeriv Γℝ s = logDeriv Γℝ (s+4) − (1/s + 1/(s+2)). Proof via the recurrence Γℝ(w+2) = (w/(2π))·Γℝ(w): - Gammaℝ_add_two : ∀ w with w ≠ 0...: Γℝ(w+2) = (w/(2π)) Γℝ(w). From def: Γℝ(w+2) = π^{−(w+2)/2} Γ((w+2)/2) = π^{−1}π^{−w/2} Γ(w/2+1) = π^{−1}π^{−w/2}(w/2)Γ(w/2) [Gamma_add_one needs w/2 ≠ 0] = (w/(2π))Γℝ(w). Need cpow algebra: π^{−(w+2)/2} = π^{−w/2}·π^{−1}: Complex.cpow_add? For real base: (π:ℂ)^(a+b) = π^a · π^b — `Complex.ofReal_cpow`? There's `Real.cpow_add`? For complex exponent with real base: `(x : ℂ)^(y+z) = x^y * x^z` when x real positive: `Complex.ofReal_cpow`... the lemma is `Real.cpow_add (hx : 0 < x) (y z : ℂ) : x^(y+z) = x^y * x^z`? Hmm — Real.cpow with complex exponent: rpow is for real exponent. For real base complex exponent, Mathlib: `Complex.ofReal_cpow (hx : 0 ≤ x)...`? Actually Zeta23's logDeriv_Gammaℝ proof used `Complex.cpow_def_of_ne_zero`. There's `Complex.cpow_add (x y : ℂ) (z : ℂ) (hx : x ≠ 0) : x ^ (y + z) = x ^ y * x ^ z`? I believe `Complex.cpow_add` exists with hx. Let me just grep when writing. - Then: Γℝ =ᶠ[𝓝 s] (fun w => (2π/w) · Γℝ(w+4)) — two-step recurrence composed; or directly prove Γℝ(w) = (2π/w)·(2π/(w+2))·Γℝ(w+4) for w avoiding {0,−2,−4} neighborhood. Actually cleaner: prove pointwise local identity Γℝ(w) = c(w)·Γℝ(w+4) with c(w) = (2π)²/(w(w+2)) on a neighborhood of s avoiding {0, −2}, then: logDeriv Γℝ s = logDeriv (c · (Γℝ∘(+4))) s = logDeriv c s + logDeriv (Γℝ∘(+4)) s. logDeriv c s where c(w) = 4π²·(w(w+2))⁻¹: logDeriv (w(w+2))⁻¹ = −logDeriv (w(w+2)) = −(1/w + 1/(w+2))... need logDeriv_inv: logDeriv f⁻¹ s = −logDeriv f s (Mathlib: `logDeriv_inv`? grep). And constant factor: logDeriv (const·f) = logDeriv f for const ≠ 0 (`logDeriv_const_mul`? grep). logDeriv (Γℝ∘(+4)) s = logDeriv Γℝ (s+4) · deriv(+4) = logDeriv Γℝ (s+4) (logDeriv_comp from GammaRBracket usage: `logDeriv_comp (g := ...) (x := s) hΓdiff hhalf : logDeriv (f ∘ g) s = logDeriv f (g s) * deriv g s`? The usage in GammaRBracket: `logDeriv_comp (g := fun s : ℂ => s / 2) (x := s) hΓdiff hhalf` then multiplied by deriv — the conclusion should be logDeriv (f∘g) x = (logDeriv f (g x)) * deriv g x. With g = (·+4), deriv = 1. So logDeriv Γℝ s = −(1/s + 1/(s+2)) + logDeriv Γℝ (s+4). ✓ (Sign check: c(w)·Γℝ(w+4) = Γℝ(w) with c = 4π²/(w(w+2)) ⟹ log c + log Γℝ(w+4) derivative: c'/c + logDeriv Γℝ(s+4) = logDeriv Γℝ s; c'/c = −(1/s+1/(s+2)) ✓.) Then plug logDeriv Γℝ (s+4) = −(log π)/2 + ½ψ((s+4)/2) (re(s+4) ≥ 3/2 > 0, Zeta23 WeilEF.logDeriv_Gammaℝ or RvM.GammaSide.logDeriv_Gammaℝ — two copies! Use Zeta23.WeilEF.logDeriv_Gammaℝ from GammaRBracket.lean which we just read: `logDeriv_Gammaℝ {s} (hs : 0 < s.re)`). And ψ((s+4)/2) = ψ(s/2 + 2) = ψ(s/2) + 1/(s/2) + 1/(s/2+1) via digamma_apply_add_one twice (needs s/2 ∉ −ℕ and (s/2+1) ∉ −ℕ: from |s.im| ≥ 10, s/2 has im ≠ 0, so s/2 ≠ −m real ✓... s/2 = −m would force im = 0 ✓ contradiction). So in the assembly I don't need the digamma recurrence separately if I just bound ‖logDeriv Γℝ s‖ via the SHIFTED form directly: ‖logDeriv Γℝ s‖ ≤ (log π)/2 + ½‖ψ((s+4)/2)‖ + ‖1/s‖ + ‖1/(s+2)‖ and bound ψ((s+4)/2) by Stirling directly (re((s+4)/2) ≥ 3/4 > 0 ✓, |im| = |t|/2 ≥ 5 ✓). That's cleaner — no digamma recurrence needed for 5d's ΓB bound! The digamma recurrence is still needed for the LEFT-PLANE digamma bound (5e prep, separate lemma). Hmm wait — but for 5e I'll want ψ(w)−log w bounds in the left half-plane. That DOES need the recurrence + Stirling. OK, separate lemma as planned. **Assembling the ΓB bound** (step 3): ΓB(s) := logDeriv Γℝ s + logDeriv Γℝ (1−s). ‖ΓB(s)‖ ≤ ‖logDeriv Γℝ s‖ + ‖logDeriv Γℝ (1−s)‖. For logDeriv Γℝ (1−s) = −(log π)/2 + ½ψ((1−s)/2), w₁ = (1−s)/2, re w₁ ∈ [1/4, 7/4], |im w₁| = |t|/2 ≥ 5: Stirling: ‖ψ(w₁) − log w₁ + 1/(2w₁)‖ ≤ 3/(im w₁)² = 12/t² ≤ 12/100. ‖ψ(w₁)‖ ≤ ‖log w₁‖ + ‖1/(2w₁)‖ + 12/100 ≤ (log ‖w₁‖ + π) + 1/(2·5) + 0.12. ‖w₁‖ ≤ (|1−s.re| + |t|)... ‖w₁‖ = ‖1−s‖/2 ≤ (‖1−s‖)/2 ≤ (|1−s.re| + |t|)/2 ≤ (7/2 + |t|)/2 ≤ |t| (for |t| ≥ 10: (3.5+|t|)/2 ≤ |t| ⟺ 3.5 ≤ |t| ✓). And ‖w₁‖ ≥ |im w₁| = |t|/2 ≥ 5 > 0, log ‖w₁‖ ≤ log |t|. So ‖ψ(w₁)‖ ≤ log|t| + π + 0.1 + 0.12 ≤ log|t| + 3.4. ‖logDeriv Γℝ (1−s)‖ ≤ (log π)/2 + ½(log|t| + 3.4) ≤ ½ log|t| + 0.58 + 1.7 = ½ log|t| + 2.3. For logDeriv Γℝ s via shift: w₂ = (s+4)/2 = s/2 + 2, re w₂ ∈ [3/4, 9/4], |im w₂| ≥ 5: same bound ‖ψ(w₂)‖ ≤ log ‖w₂‖ + π + 0.22; ‖w₂‖ ≤ ‖s‖/2 + 2 ≤ (|s.re| + |t|)/2 + 2 ≤ (5/2 + |t|)/2 + 2 = |t|/2 + 3.25 ≤ |t| (|t| ≥ 6.5 ✓). So ‖ψ(w₂)‖ ≤ log|t| + 3.4. ‖logDeriv Γℝ s‖ ≤ (log π)/2 + ½‖ψ(w₂)‖ + ‖1/s‖ + ‖1/(s+2)‖ ≤ 0.58 + ½ log|t| + 1.7 + 1/10 + 1/10 = ½ log|t| + 2.5. (‖s‖ ≥ |t| ≥ 10 ⟹ 1/‖s‖ ≤ 1/10; ‖s+2‖ ≥ |t| ≥ 10 ⟹ 1/10.) Total: ‖ΓB(s)‖ ≤ log|t| + 4.8 ≤ log|t| + 4.8. Since log|t| ≥ log 10 ≥ 2: 4.8 ≤ 2.4 log|t|. ‖ΓB‖ ≤ 3.4 log|t|... hmm let me just say ≤ log|t| + 5. Final: ‖R(s)‖ ≤ 100000 L² + L + 5 where L = log|t| ≥ 2. L + 5 ≤ (5/2)L... 5 ≤ 2.5L ✓ so L+5 ≤ 3.5L ≤ (7/4)L² (L ≥ 2). So ‖R(s)‖ ≤ (100000 + 7/4)L² ≤ 100002 L². I'll fold to ≤ 100002 * (log|t|)². Or to keep it cleaner maybe state the left-half bound as 200000·(log|t|)²? Precision: let's try to assemble and see what comes out; target statement: **logDeriv_riemannZeta_sub_nearZeros_le_left {t} (ht : 10 ≤ |t|) {s} (hsim : s.im = t) (hσlo : −5/2 ≤ s.re) (hσhi : s.re ≤ 1/2) (hs0 : riemannZeta s ≠ 0) : ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} zeroMult ρ/(s−ρ)‖ ≤ 100002·(log|t|)²** — hmm, but actually what range does 5e need? D-067 §3: the partial-fraction identity needs R-bounds on the LEFT for the contour's left edge at σ = −(something). The R-bound on σ ∈ [−5/2, 1/2] per STATE.md. OK as planned. Wait — one important check on the reflection identity: I apply ii′-5c to s' = 1−s with t' = −t. But ii′-5c requires s'.im = t' i.e. (1−s).im = −t ✓ since (1−s).im = −s.im = −t. ✓. And re(1−s) ∈ [1/2, 7/2]: re(1−s) = 1−s.re ∈ [1/2, 7/2] ⟺ s.re ∈ [−5/2, 1/2] ✓. ζ(1−s) ≠ 0 ✓ shown. Then: ‖logDeriv ζ (1−s) − Σ_{ρ' ∈ nearZeros (−t)} m_{ρ'}/((1−s)−ρ')‖ ≤ 100000 (log|−t|)² = 100000 (log|t|)². ✓ (|−t| = |t|.) **Now the sum-reflection lemma** (step 2). Need: (a) characterization: ρ ∈ nearZeros t ↔ IsNontrivialZero ρ ∧ |ρ.im − t| < 1. Forward: mem_nearZeros gives zeroDiscFinset membership ⟹ zeroDisc_isNontrivial ✓. Backward: IsNontrivialZero ρ ∧ |ρ.im − t| < 1 ⟹ ‖ρ − (2+it)‖ ≤ 5/2: ‖ρ − (2+it)‖² = (ρ.re−2)² + (ρ.im−t)². re ∈ (0,1): |ρ.re − 2| < 2 hmm need ≤ : (ρ.re−2)² < 4 strict; (ρ.im−t)² < 1 strict. Sum < 5 < 25/4 ✓ so ‖·‖ < 5/2... closedBall is ≤: fine, < implies ≤. In Lean: normSq: Complex.normSq (ρ − discCenter t) = (ρ.re−2)² + (ρ.im−t)² (discCenter t = 2 + t*I: re = 2, im = t — need simp lemmas; from the code at line 1005-1008 they did `Complex.normSq_apply` + simp with discCenter). Then ‖x‖ ≤ 5/2 ⟺ normSq x ≤ 25/4 via... they used `Complex.normSq` ≤ 5 ⟹ ‖·‖ ≤ √5 at line 1004-1005 (`norm_le_sqrt_normSq`?). There's presumably a helper. I'll mimic the existing pattern from nearZeros_subset_image (lines 996–1060). Actually easier: ‖x‖² = normSq x: `Complex.normSq_eq_norm_sq`? There is `Complex.normSq_eq_abs` (normSq = ‖·‖²)... I'll find the right lemma. Standard: `Complex.normSq_eq_norm_sq : normSq z = ‖z‖^2`? Something like that exists or use abs. Let me handle when writing. (b) image equality: (nearZeros (−t)).image (fun ρ => 1 − ρ) = nearZeros t. Both inclusions via (a): - ρ' ∈ nearZeros(−t) ⟹ ρ := 1−ρ': IsNontrivialZero (1−ρ'): ζ(1−ρ') = 0: Λ(1−ρ') = Λ(ρ') = Γℝ(ρ')ζ(ρ') = 0 (ζ(ρ') = 0) — need ρ' ≠ 0 (re > 0 ✓) and then completedRiemannZeta_eq_zero_iff.mp: Λ(1−ρ') = 0 ⟹ IsNontrivialZero (1−ρ') ✓ DIRECTLY (the iff gives the full package!). |Im(1−ρ') − t| = |−ρ'.im − t| = |ρ'.im + t| < 1 ✓. - ρ ∈ nearZeros t ⟹ ρ = 1−(1−ρ) with 1−ρ ∈ nearZeros(−t): IsNontrivialZero(1−ρ) via Λ again; |Im(1−ρ) + t| = |−ρ.im + t| = |ρ.im − t| < 1 ✓. InjOn of (1−·): injective globally: add_left_injective? fun ρ => 1 − ρ injective: `sub_left_injective`? (fun ρ => 1 − ρ) = (1 − ·): injective: intro a b h; simpa using h. Finset.sum_image needs Set.InjOn ✓ trivial. (c) sum cancellation: Σ_{ρ' ∈ nearZeros (−t)} (zeroMult ρ' : ℂ)/(1−s−ρ') = Σ_{ρ' ∈ nearZeros (−t)} (zeroMult (1−ρ') : ℂ)/(1−s−ρ') [zeroMult_one_sub on each — needs IsNontrivialZero ρ' ✓ from (a)] = Σ_{ρ ∈ nearZeros t} (zeroMult ρ : ℂ)/(1−s−(1−ρ)) [sum_image with (b)] = Σ_{ρ ∈ nearZeros t} (zeroMult ρ : ℂ)/(ρ−s) = −Σ (zeroMult ρ)/(s−ρ). Algebra: 1−s−(1−ρ) = ρ−s = −(s−ρ): (m:ℂ)/(ρ−s) = −(m:ℂ)/(s−ρ): field_simp-ish: div_neg... (m)/(ρ−s) = −m/(s−ρ) by `div_neg_eq_neg_div`? ρ−s = −(s−ρ): rw [show ρ − s = −(s − ρ) by ring, div_neg, neg_div]... fine. (d) main identity: R(s) + R(1−s)·(−1)... let me define in Lean directly the final manipulation: logDeriv ζ s − S(t,s) = −[logDeriv ζ (1−s) − S(−t,1−s)] − ΓB(s) where S(t,s) := Σ_{ρ∈nearZeros t} m_ρ/(s−ρ). Proof: logDeriv_zeta_FE gives logDeriv ζ s = −logDeriv ζ (1−s) − ΓB(s). Then: LHS = −logDeriv ζ (1−s) − ΓB(s) − S(t,s). And −R(1−s) = −logDeriv ζ(1−s) + S(−t,1−s) = −logDeriv ζ(1−s) − S(t,s) by (c): S(−t,1−s) = −S(t,s). ✓ So LHS = −R(1−s) − ΓB(s). ✓ (e) bounds + fold. ‖R(s)‖ ≤ ‖R(1−s)‖ + ‖ΓB(s)‖. Now the **left-plane digamma bound** (deliverable 2, for 5e). Let me design the exact statement. In 5e, on the γ-gap circles and the reflected contour, we need |ψ(w)| controlled where w ranges over a left-half-plane region avoiding poles. Cleanest useful form: **digamma_norm_le_of_im_ge** : for w with 1 ≤ |w.im|: ‖Complex.digamma w‖ ≤ Real.log (‖w‖ + m + 2) + m + 4 where m depends on re w... a bound with an existentially-chosen m is awkward to state. Alternative formulation: state with the shift count explicit: For w with 1 ≤ |w.im| and −(K:ℝ) ≤ w.re (K ≥ 0): choose m = ⌈K⌉ + 1 (nat) so re(w + m) ≥ 1... Let me think about what 5e needs concretely: the contour for the partial-fraction identity is a big rectangle/circle; on its left edge σ = −U (U large, half-integer to avoid trivial-zero poles), |t| ≤ T. There ψ(s/2) with s/2 = −U/2 + it/2: |im| = |t|/2 could be SMALL (down to 0) when t small! "Away from poles" — on the horizontal segments t = ±T it's fine (|im| ≥ T/2). On the left vertical edge, t ranges through small values and s/2 passes near −U/2... the contour is chosen in a gap: the trivial zeros at −2n — the digamma poles at s/2 = −n i.e. s = −2n. The left edge at σ = −U with U ODD avoids {−2n}: |s/2 + n| ≥ 1/2 for all n when re(s/2) = −U/2, U odd: distance from −U/2 to nearest integer ≥ ... U odd ⟹ U/2 = k + 1/2 ⟹ −U/2 = −k−1/2, distance to integers = 1/2 ✓. So the needed bound: for w with re w half-odd-integer-ish (dist(re w, −ℕ) ≥ 1/2) and no im constraint: |ψ(w)| ≤ C log(2+|w|)-ish. That's the classical bound ψ(w) = O(log|w|) away from poles. Hmm, but pinning the exact 5e need now risks rework. The plan says: "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)". So the deliverable: a bound of the form: for w with ∀ n : ℕ, ‖w + n‖ ≥ δ (away from poles): ‖ψ(w) − log w‖ ≤ C(δ)·(something tame) — or maybe simplest: ‖ψ(w)‖ ≤ C·(log ‖w‖ + 1) + C' with explicit constants when dist(w, −ℕ) ≥ 1/2. Proof route (recurrence + Stirling): pick m : ℕ minimal with re(w + m) ≥ 1 (m ≤ max 0 (1 − re w) + 1). ψ(w) = ψ(w+m) − Σ_{j=0}^{m−1} 1/(w+j). Each term ‖1/(w+j)‖ ≤ 1/δ... but wait if w is near a pole w+j near 0 for some j — the "away from poles" hypothesis gives ‖w+j‖ ≥ δ for all j ✓. So Σ ≤ m/δ. ‖ψ(w+m)‖ ≤ ‖log(w+m)‖ + 1/(2‖w+m‖) + 3/(im)² — needs |im(w+m)| ≥ 1/2: if |im w| ≥ 1/2 ✓; but on the left edge near the real axis im w → 0! Stirling needs |im| ≥ 1/2. For real-ish w in the left plane with re w + m ≥ 1: w+m has re ≥ 1 and |im| possibly tiny. Then use instead a BOUNDED-region bound: w+m ∈ compact-ish region {1 ≤ re ≤ K+2, |im| ≤ 1/2}: ψ is continuous there (poles at −ℕ avoided) hence bounded on the compact set... but re unbounded as K grows: on {re ≥ 1, |im| ≤ 1/2}: ψ(w) − log w → 0 as |w| → ∞ uniformly (Stirling for real-ish? digamma_stirling needs |im| ≥ 1/2 ✗). Hmm. Alternative: for re z ≥ 1 (any im): |ψ(z)| ≤ log|z| + C via the series ψ(z) = −γ + Σ_{n≥0} (1/(n+1) − 1/(z+n)) hmm that's the series which converges like Σ |z−1|/(n·|z+n|)... The classical elementary bound: for re z ≥ 1: ψ(z) = −γ − 1/z + ... hmm. Simplest classical: ψ(z) = ψ(z+1) − 1/z and for re z ≥ 1: |ψ(z) − log z| ≤ C/|z|? That's Stirling with weak remainder: Zeta23 digamma_stirling needs |im| ≥ 1/2. For |im| < 1/2, re ≥ 1: bound ψ via the series directly? Hmm, actually — what does 5e really need? The digamma appears via the Γℝ bracket in the partial-fraction identity for ζ′/ζ. The identity (D-056/D-067): ζ′/ζ(s) = Σ_{|γ−t|<1} m/(s−ρ) + O(log|t|)... the 5e identity is the FULL partial fraction: ζ′/ζ(s) = B + Σ_ρ m(1/(s−ρ) + 1/ρ) − (archimedean terms)... Actually D-067's plan: "partial-fraction identity (5e: series convergence via mult-weighted zero_sum_inv_sq + F entire by residue cancellation + |F| = o(R) on γ-gap circles ⟹ F const)". So F(s) := ζ′/ζ(s) − Σ_ρ m_ρ(1/(s−ρ)+1/ρ) − (Γℝ′/Γℝ terms) − const; show F entire and F = o(R) on a sequence of circles ⟹ F constant (or 0). The digamma bound needed: |Γℝ′/Γℝ(s)| = O(log(2+|s|)) on circles |s| = R avoiding poles. The circles hit both right and left half planes, including near-real-axis left points. On a circle |s| = R: s/2 has |s/2| = R/2; if s/2 near a negative integer, the circle must avoid: choose R such that dist(R/2, ℕ) ≥ 1/4 etc. and then |w + n| ≥ ... for w = s/2 on the circle: for n ≤ R/2 hmm: |w + n| ≥ ||w| − n| ≥ ... on the circle, |w| = R/2 const; for n ≠ near R/2: |w+n| ≥ |R/2 − n| ≥ 1/4 by the radius choice for n ≤ R; for n > R: |w+n| ≥ n − R/2 ≥ R/2. OK. And for the Stirling piece on the circle: w = s/2 with re w ≥ −R/2; shift by m ≈ R/2 + 1 to reach re ≥ 1, then w + m has re ≥ 1 and |im| ≤ R/2 — Stirling with |im| ≥ 1/2 fails near the real axis AGAIN. So I need a digamma bound valid on re z ≥ 1 WITHOUT the |im| constraint. Options: (i) The series bound: for re z ≥ 1: ψ(z) = −γ + Σ_{n=0}^∞ (1/(n+1) − 1/(z+n)) — wait that's ψ(z) + γ = Σ (1/(n+1) − 1/(n+z))? The Mathlib digamma is defined via that series? Zeta23.DigammaSeries.hasSum_digamma_series: HasSum (fun n => 1/(n+1) − 1/(z+n+1)) (digamma z + γ)?? From GammaRBracket line 39: `hasSum_digamma_series hz : HasSum (fun n => 1/((n:ℂ)+1) − 1/(z+n+1)) (digamma z + γ + 1/z)`. Interesting: so ψ(z) = −γ − 1/z + Σ_{n≥0} (1/(n+1) − 1/(z+n+1)). Bound for re z ≥ 1: |1/(n+1) − 1/(z+n+1)| = |z|/( (n+1)|z+n+1| ) ≤ |z|/((n+1)(n+1)) hmm re(z+n+1) ≥ n+2 so |z+n+1| ≥ n+2... wait |z+n+1| ≥ re(z)+n+1 ≥ n+2. So term ≤ |z|/((n+1)(n+2)), sum telescopes: Σ_{n≥0} 1/((n+1)(n+2)) = 1. So |ψ(z) + γ + 1/z| ≤ |z|·1?? That gives |ψ(z)| ≤ |z| + γ + 1 — LINEAR, too weak (need log). Hmm right, the naive series bound is linear; the log bound needs the smarter comparison Σ_{n≤|z|} 1/n ≈ log. Standard approach: ψ(z) = −γ − 1/z + Σ (1/(n+1) − 1/(z+n+1)); split Σ at N ≈ |z|: for n < |z|: |1/(z+n+1)| ≤ 1/re(z+n+1) ≤ 1/(n+1) (re z ≥ ... hmm ≥ 1/(n+2)) and |1/(n+1) − 1/(z+n+1)| — for the small-n part write as 1/(n+1) − 1/(z+n+1), sum the 1/(n+1) part: ≈ log N, and Σ 1/(z+n+1) ≤ Σ 1/(n+1) ≈ log N. For n ≥ |z|: term ≤ |z|/((n+1)(n+2)) sum ≤ |z|/N ≈ 1. Total ≈ 2 log|z| + O(1). OK so a log bound via series is doable but fiddly in Lean. (ii) Alternative: avoid the near-real-axis case entirely by using the recurrence to shift into re ∈ [1,2] and then a COMPACT bound for |im| ≤ 1/2 plus digamma_stirling for |im| ≥ 1/2: for w with re(w+m) ∈ [1, 2] (choose m = that shift): if |im w| ≥ 1/2: Stirling. If |im w| < 1/2: w+m ∈ compact {1 ≤ re ≤ 2, |im| ≤ 1/2} where ψ continuous ⟹ bounded by an explicit constant? "Continuous on compact ⟹ bounded" gives EXISTENCE of a bound, not explicit. But we can get explicit via the series on the compact... ugh. Hmm, wait. Let me reconsider: is the near-real-axis left-half-plane digamma actually NEEDED for 5e? In the classical proof (Davenport Ch. 11-12), the partial-fraction bound |F| = o(R) on circles uses |ζ′/ζ| estimates on the LEFT edge derived from the FE: ζ′/ζ(s) = −ζ′/ζ(1−s) − Γbracket, and the Γbracket on the left edge at height t (including small t!) needs ψ((1−s)/2) (right half, fine) and ψ(s/2) (left half, small im possible). The standard treatment: |ψ(s/2)| = O(log|s|) uniformly on the left edge since dist(s/2, −ℕ) ≥ 1/2 (edge at odd integers). The classical proof of THAT: ψ(w) = O(log(2|w|)) for dist(w, −ℕ) ≥ δ — via ψ(w) = ψ(w+m) − Σ 1/(w+j) with m chosen so re(w+m) ∈ [1,2], and then ψ(w+m) = O(log|w+m|) via... Davenport just quotes Stirling which for BOUNDED im and re ∈ [1,2] is trivial (bounded). For Lean: the cleanest uniform statement might be: **digamma_left_plane_bound**: ∀ w : ℂ, (∀ n : ℕ, δ ≤ ‖w + n‖) → ‖Complex.digamma w‖ ≤ C₁ · Real.log (2 + ‖w‖) + C₂/δ-ish... Actually you know what — let me look at D-067 §3 to see EXACTLY what statement was designed. I should read D-067 before designing. Let me read the design doc.