D-068 — ii′-5e design: the partial-fraction identity in Lean

Date: 2026-08-22 | Session: 026 | Task: 5.1 tier ii′-5e (D-064 §4 R3, D-067 §6 second stage) Status: DESIGN COMPLETE (inventory verified live against Mathlib + Zeta23 where noted). Sub-stage map §7.

0. Target

The partial-fraction identity (D-067 §6's chosen form):

ζ′/ζ(s) = B + Σ_ρ m_ρ (1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2)

for s ∉ {nontrivial zeros} ∪ {0, 1} ∪ {−2n}, with:

• the sum over the nontrivial zeros with multiplicities m_ρ = zeroMult ρ;
• B : ℂ an existential constant (cancels in 5f's two-point analysis — no evaluation needed);
• proof: F := LHS − RHS is ENTIRE (residue cancellation at every excluded point) with |F| = O((log R)³) on a γ-gap circle sequence R_k → ∞ ⟹ F ≡ const (difference quotient + max-modulus + Liouville).

Residue bookkeeping (checked): at a nontrivial zero ρ: +m_ρ vs +m_ρ (the series term) ✓; at s = 1: −1 vs −1 (the −1/(s−1) term) ✓; at s = 0: 0 (ζ′/ζ analytic, ζ(0) = −1/2 ≠ 0) vs −1 + 1 = 0 (the −1/s term vs −½ψ(s/2) ~ +1/s, since ψ(w) has residue −1 at w = 0) ✓; at s = −2n: +1 (simple zero — zeroMult_neg_two_mul, session 026, the 5e-prep item — DONE) vs +1 (−½ψ(s/2), since ψ(w) has residue −1 at w = −n and w = s/2 doubles residues) ✓.

1. Corrections to the D-067 §6 sketch (found in the 5e survey)

(C1) The circle bound on the series is O((log R)³), not O((log R)²). The sketch's "dyadic split" mis-estimates the annulus |ρ| ≍ R: the naive term bound |1/(s−ρ)+1/ρ| ≤ R/(|ρ||s−ρ|) with |s−ρ| ≥ 1 gives O(1) per term over ≍ R log R annulus zeros = O(R log R) — NOT o(R). The correct split is by the RADIAL distance ||s| − |ρ||, using the γ-gap only in the critical annulus [R−2, R+2]: |ρ| ≤ R/2: |s−ρ| ≥ R/2 ⟹ term ≤ 2/|ρ|; Σ = O((log R)²) R/2 < |ρ| ≤ R−2: |s−ρ| ≥ R−|ρ| ⟹ ≤ 2/(R−|ρ|); Σ ≍ Σ_{j≥2} C₀(R)/j = O((log R)²) [R−2, R+2]: |s−ρ| ≥ |t−γ| ≥ c/(2 log R) (the gap); count ≍ C₀(R) ⟹ Σ = O((log R)³/c) [R+2, 2R]: symmetric to the second case: O((log R)²) |ρ| > 2R: |s−ρ| ≥ |ρ|/2 ⟹ ≤ 2R/|ρ|²; Σ ≍ R·(log R)/R = O(log R) Total O((log R)³/c) with c the fixed pigeonhole constant — o(R) ✓. (The tighter classical O((log R)²) for ζ′/ζ itself is unaffected.)

(C2) The near-axis left-plane digamma bound is a SEPARATE build. 5d's norm_digamma_sub_log_le_of_two_le_abs_im requires 2 ≤ |im w| (slit-plane FTC along the real path). On the circle's near-real-axis left part (re s ≈ −R, |im s| < 10) the argument w = s/2 can have |im w| < 2, and the real-path FTC hits the pole. The correct input (dist(w, −ℕ) ≥ 1/4, available on our circles, §4) is the recurrence + the separated reciprocal sum:

ψ(w) = ψ(w+m) − Σ_{j=0}^{m−1} 1/(w+j), m := ⌈−re w⌉₊ + 2

with Σ_j 1/|w+j| ≤ C·log(m+1) UNIFORMLY (the values |w+j| are 1-separated in the real part and ≥ 1/4 everywhere ⟹ at most 2 per unit bin ⟹ Σ ≤ 2·(4 + H_m) = O(log m)), and ψ(w+m) bounded by either StirlingVert (|im| ≥ 1/2) or COMPACTNESS (|im| < 1/2, re ∈ [1, 2] — ψ continuous there; IsCompact bound). Conclusion: ‖ψ(w)‖ ≤ C·log(2+‖w‖) for dist(w, −ℕ) ≥ 1/4. (~0.25 sess.)

Note the boundary case |im w| ∈ [1/2, 2), re w ≥ 2 (right circle point, for logDeriv ΓR(1−s)): digamma_stirling applies directly; |im w| < 1/2, re w ≥ 2: the series split Σ 1/((n+1)(w+n+1)) at A = re w: Σ_{n+1≤A} ≍ (log A)/A, Σ_{n+1>A} ≍ 1/A ⟹ ψ(w) = log w + O(1) — the Weierstrass-series route (Zeta23 DigammaSeries.digamma_series: ψ(z) = −γ − 1/z + Σ'_n (1/(n+1) − 1/(z+n+1)), exists, axiom-checked).

2. The γ-gap circles (sub-build 5e-i)

Radius R_k ∈ [4k+5/2, 4k+3] with |R_k − γ| ≥ 1/(6·C0hat(8k+6))-ish for ALL zero ordinates γ, via the ×2-RESCALE TRICK on ii′-4's midpoint pigeonhole (exists_avoiding_midpoint at a = 8k+5 on the ×2-scaled ordinate finset; the count input = ZeroCountProp on the two unit windows [4k+2, 4k+3] ∪ [4k+3, 4k+4] ⊃ the scaled window). Then:

• ordinate clearance at the strip crossings: t = ±√(R²−σ²), |σ| ≤ 2 ⟹ |t − R| ≤ 4/R ⟹ |t−γ| ≥ c/(2 log R) for R large;
• trivial-zero clearance: R/2 ∈ [2k+5/4, 2k+3/2] ⟹ dist(R/2, ℤ) ≥ 1/4 ⟹ dist(s/2, −ℕ) ≥ 1/4 − O(1/R) ≥ 1/8 on the near-axis left part;
• R_k ∈ [4k+2.5, 4k+3] ⟹ R_k → ∞ at linear rate. (~0.25 sess, zero new pigeonhole code — the 5c trick verbatim.)

3. The series (sub-build 5e-iii)

seriesFun s := ∑' ρ : nontrivialZeros, (zeroMult ρ : ℂ)·(1/(s−ρ) + 1/ρ) (tsum over the zero SUBTYPE, the ii′-1a liSummable pattern).

• Summability at each s ∉ zeros: |1/(s−ρ)+1/ρ| = |s|/(|ρ||s−ρ|) ≤ 2‖s‖/‖ρ‖² for ‖ρ‖ > 2‖s‖ (then |s−ρ| ≥ ‖ρ‖/2); mult-weighted Σ m_ρ/‖ρ‖² converges (the ii′-1a dominator chain → Zeta23 zero_sum_inv_sq); the finite ball part is a finite subtype sum (zeros finite in compacts — IsCompact.inter_riemannZetaZeros_finite, the 5c pattern).
• Analytic on ℂ ∖ zeros: locally uniform on each compact K ⊂⊂ ℂ ∖ zeros (same comparison with the finite-head split; zeros closed ⟹ dist(K, zeros) > 0 — wait, K compact + zeros CLOSED disjoint ⟹ positive distance: IsCompact/isClosed separation — check Mathlib's IsCompact.exists_uniform_...; else bound via the ball cover directly); partial sums are finite sums of analytic terms; locally-uniform limit analytic (TendstoLocallyUniformlyOn → the journal-020/021-banked differentiableOn form, then analyticOnNhd).
• Isolation at each zero ρ: ∃ δ > 0, ball(ρ, δ) contains no other zero (discreteness: the zero set is closed + finite in compacts — standard one-paragraph argument from zerosIn_finite/the inter finiteness) ⟹ the series minus the ρ-term is analytic at ρ (the tail over ρ′ ∉ ball converges uniformly on ball(ρ, δ/2)).

4. F entire (sub-build 5e-iv) — principal-part splitting (NO

removable-singularity theorem needed; Mathlib lacks it in general form)

At each excluded point write F as a difference of pointwise-analytic functions:

• nontrivial zero ρ (mult m): F = [ζ′/ζ − m/(s−ρ)] − [series − m/(s−ρ) − elem + m/ρ-correction] — the first bracket analytic at ρ by ii′-1b's logDeriv-NF machinery (the LiSides rectInt'_Jlag residue step already contains: logDeriv ζ − m/(s−ρ) analytic at ρ); the second by §3's isolation + the elementary terms analytic at ρ (re ρ ∈ (0,1) avoids 0, 1, −2n).
• s = 1: ζ′/ζ + 1/(s−1) = logDeriv zetaA (zetaA = (s−1)ζ analytic at 1 with zetaA 1 = 1 ≠ 0 — ii′-1b LiResidue) ⟹ analytic at 1 via AnalyticAt.deriv + AnalyticAt.div; the −1/(s−1) cancels it in F.
• s = 0: −½ψ(s/2) = 1/s − ½h₀(s) with h₀ analytic at 0 (digamma series: ψ(w) = −γ − 1/w + Σ'-part, the series analytic at 0 by the locally-uniform machinery — each term 1/(n+1)−1/(w+n+1) has |term| ≤ C/(n+1)² for ‖w‖ ≤ 1/2); so −1/s − ½ψ(s/2) analytic at 0; ζ′/ζ analytic at 0 (ζ(0) = −1/2 ≠ 0).
• s = −2n: ζ′/ζ − 1/(s+2n) analytic at −2n (ii′-1b NF + zeroMult_neg_two_mul = 1, session 026); −½ψ(s/2) − 1/(s+2n) analytic at −2n (ψ(w) + 1/(w+n) analytic at w = −n: split the j = n−1 term off the digamma series).
• all other s: direct (ζ s ≠ 0, off the pole list ⟹ every piece analytic).

5. The circle bound and Liouville close (sub-build 5e-v)

On |s| = R_k (§2):

• |ζ′/ζ|: right part (re ≥ 1/2, |t| ≥ 10): 5c; left part (re ≤ 1/2, |t| ≥ 10): 5d; the near sums inside those bounds use the gap (each |s−ρ| ≥ c/(2 log R), count ≍ C₀ ≍ log R) ⟹ O((log R)²); right near-axis (|t| < 10, re ≈ +R): Dirichlet-series bound ‖ζ′/ζ‖ ≤ Σ Λ(n)/n^{re} ≤ C for re ≥ 2 (Zeta23 LSeries vonMangoldt — inventory session 019 ✓; the Σ Λ(n)/n² majorant via LSeries absSummable); left near-axis (re ≈ −R): FE-reflect pointwise (logDeriv_zeta_fe, 5d) — ζ′/ζ(1−s) = O(1) (Dirichlet, re(1−s) ≈ 1+R)
• logDeriv ΓR(1−s) = O(log R) (digamma_stirling or the C2 right boundary case) + logDeriv ΓR(s) = O(log R) (C2 near-axis bound — needs the 5d identity logDeriv_Gammaℝ shifted: ΓR′/ΓR(s) = −(log π)/2 + ½ψ(s/2) for im ≠ 0 via 5d's +4 shift... — CAREFUL: the +4 shift only reaches re(s/2) + 2; for re s ≈ −R need ψ(s/2) directly from C2 (re(s/2) ≈ −R/2, dist(s/2, −ℕ) ≥ 1/8 ✓). For im s = 0 exactly (s = −R real): logDeriv ΓR at −R: R = R_k ∈ [4k+2.5, 4k+3] is NOT an even integer ⟹ ΓR analytic nonzero at −R; the logDeriv ΓR value via the recurrence evaluation — include s real in C2's scope (dist condition is real-checkable).
• |series|: O((log R)³/c) by §1 (C1).
• |elem|: −1/s, −1/(s−1) = O(1/R); ½log π const; ½ψ(s/2) = O(log R) (5d's bound for |im| ≥ 2; C2 for the rest). Total: |F| ≤ C(log R_k)³ on |s| = R_k.

F ≡ const: G(z) := (F(z) − F(0))/z entire (INVENTORY: the difference-quotient analyticity — check Mathlib for AnalyticAt of (f w − f z)/(w − z); if missing, build from the HasFPowerSeriesAt tail — ~30 lines); |G| ≤ C(log R)³/R + |F(0)|/R on |z| = R_k ⟹ limsup-bound 0 for any fixed z via max-modulus on the discs (Zeta23 AnalyticOn.norm_le_of_norm_le_on_sphere, the 5c pattern) ⟹ G ≡ 0 on each disc ⟹ F ≡ F(0). (No Liouville needed — the direct max-modulus squeeze suffices. If more convenient: Differentiable.apply_eq_apply_of_bounded-style Liouville on a bounded G — same content.)

Conclusion theorem (5e capstone): ∃ B : ℂ, ∀ s, (riemannZeta s ≠ 0 → s ≠ 0 → s ≠ 1 → (∀ n : ℕ, 1 ≤ n → s ≠ -2 * n) → logDeriv riemannZeta s = B + seriesFun s - 1/s - 1/(s-1) + (Real.log π)/2 - digamma (s/2)/2)

6. What 5f consumes (preview — no build in 5e)

D-056's six-piece analysis on the identity at s vs the reference point s₀ = 2+it: near sum ≤ C₀(t) (perimeter ZeroCountProp — FIRST use of the perimeter in the R-chain; 5c/5d/5e deliberately avoided it via Jensen), far difference ≤ 12.73 C₀ + 7.06 (Σ 1/(k(k+1)) = 1), Z₂ ≤ 0.65 certified, ψ-difference via digamma_stirling ⟹ |R| ≤ 13.73·C₀(t) + 7.97 ≤ 10.5·log(|t|+2) + 48 EXACTLY (the baked LiSkeleton constants). ~1 sess.

7. Sub-stage plan

Risks: (a) the locally-uniform ⟹ analytic glue is routine but laborious (Mathlib has the pieces; journal-020/021 gotchas banked); (b) the difference-quotient analyticity may need a power-series build; (c) the series-on-circle split is the only genuinely analytic estimation — the (log R)³/c form is what the pigeonhole constant supports, and o(R) has enormous room.