[{"type":"thinking","thinking":"Now the ii′-5e design doc (D-068). Let me gather what I need to pin it precisely:\n\n1. The exact identity form. D-067 §6 wrote: ζ′/ζ(s) = B + Σ_ρ m_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2). Let me verify this is the correct form (residue bookkeeping):\n   - At a nontrivial zero ρ (mult m): ζ′/ζ has residue +m; the series term m(1/(s−ρ)+1/ρ) has residue +m ✓ cancel.\n   - At s = 1: ζ′/ζ has residue −1 (pole of ζ, order 1, logDeriv residue = −order = −1); −1/(s−1) has residue −1 ✓ cancel.\n   - At s = 0: ζ(0) = −1/2 ≠ 0, so ζ′/ζ analytic at 0. The RHS terms at 0: −1/s has residue −1; −½ψ(s/2): ψ(s/2) near s = 0: ψ(w) ~ −1/w − γ... wait ψ(w) at w → 0: ψ(w) = −1/w − γ + O(w) (residue −1 at 0). So −½ψ(s/2) ~ −½·(−1/(s/2)) = 1/s: residue +1. Sum of residues at 0: −1 (from −1/s) + 1 (from −½ψ(s/2)) = 0 ✓ cancel. Good — but wait, ζ′/ζ at 0 is analytic so F's residue at 0: 0 − (0) = 0 ✓ consistent.\n   - At s = −2n (n ≥ 1): ζ′/ζ residue +1 (simple zero — zeroMult(−2n) = 1 ✓ session 026!); RHS: −½ψ(s/2) at s = −2n: ψ(w) at w = −n: residue −1 in w; in s: ψ(s/2): residue −2 (chain: w = s/2, dw = ds/2, residue in s = 2·(−1) = −2); so −½ψ(s/2) has residue +1 ✓ cancel. The zero-sum Σ_ρ is over NONTRIVIAL zeros only ✓.\n   \n   So the identity form balances at every pole. The constant B = ζ′/ζ(0) = log(2π) classically? Actually B in Davenport = log 2π − 1 − γ/2... whatever — the identity gives F = const and the constant is then evaluated at s = 0: F(0) = ζ′/ζ(0) − [0 + Σ m(1/(0−ρ) + 1/ρ) − 0... let me not bother; F ≡ const ⟹ ζ′/ζ(s) = RHS(0-form) + const; the const folds into B. For 5f (the tight analysis) what matters is the DIFFERENCE R(s) = ζ′/ζ(s) − Σ_near m/(s−ρ) evaluated via the identity at s and at a reference point — D-056's analysis. The constant B cancels in the difference evaluation at two points. OK.\n\n2. Series convergence: Σ_ρ m_ρ |1/(s−ρ) + 1/ρ| over nontrivial zeros. For fixed s (not a zero): |1/(s−ρ) + 1/ρ| = |s/(ρ(s−ρ))|. Split: |ρ| ≤ 2|s|: finite (zeros discrete... need finiteness of zeros in any disc — have it: inter_riemannZetaZeros_finite pattern / zerosIn_finite); |ρ| > 2|s|: |s−ρ| ≥ |ρ|/2 ⟹ term ≤ 2|s|/|ρ|²; m_ρ-weighted Σ 1/|ρ|² converges (Zeta23 zero_sum_inv_sq — is it mult-weighted? ii′-1a's dominator used \"Zeta23 zero_sum_inv_sq comparison\" — that was Σ 1/(1+|γ|²) mult-weighted? The ii′-1a summability used `Zeta23 zero_sum_inv_sq` with the (9/2)n²·mult/(1+‖γ‖²) dominator — so the mult-weighted version exists or was built in ii′-1a (liSummable). Pin at build: likely `Zeta23.zero_sum_inv_sq : Summable (fun ρ ↦ (zeroMult ρ : ℝ) / ‖ρ‖^2)`-ish over the zero set — check exact form at build (LiSkeleton's liSummable proof has the comparison chain to clone).\n   For Lean: the series is over a SET of zeros (not a finset) — encode like liSummand's paired form? For the identity we need the series as a FUNCTION of s with analyticity properties... The cleanest Lean encoding: the sum over the full zero set as a tsum over an enumeration? The zeros are countable (discrete subset of ℂ). Hmm — how did ii′-1a handle the sum over all zeros? liCoeff := tsum over the paired liSummand via some encodable structure? Let me recall LiSkeleton's liCoeff: `liCoeff = ∑' over ...`? It used liSummand with tsum — over what index? Probably `tsum (fun ρ : riemannZetaZeros)` — the TYPE of zeros (subtype) with tsum over it. That's the pattern: the zero set as a subtype of ℂ with Summable instances. For the identity's series: Summable (fun ρ : zeros ↦ m_ρ(1/(s−ρ)+1/ρ)) — via the comparison with m/‖ρ‖²: need ‖1/(s−ρ)+1/ρ‖ ≤ C(s)/‖ρ‖² for ‖ρ‖ > 2‖s‖ and the finite-ball part handled — Summable.comparison with the subtype split... The subtype sum splits via summable_iff_on_... : Summable over the subtype ⟺ summable on the ball-part (finite subtype — automatically summable) + the outside (comparison). There are Mathlib lemmas: `Summable.add_compl`? or summable_subtype_iff... manageable.\n\n   BUT — for F entire, we need the series to be analytic in s (on ℂ minus the zeros, and the cancellation at zeros). The series Σ m(1/(s−ρ)+1/ρ) converges LOCALLY UNIFORMLY in s on compact sets avoiding the zeros (same 2R-comparison uniformly on |s| ≤ R). Local uniform limits of analytic functions are analytic (Mathlib: `TendstoLocallyUniformlyOn.analyticOn`? or the Weierstrass theorem — journal gotcha mentioned TendstoLocallyUniformlyOn.differentiableOn — exists). The partial sums over finite zero sets are analytic (finite sums of 1/(s−ρ) terms). So the series function is analytic on ℂ ∖ {zeros} with the local-uniform machinery — need the zeros set to be closed/discrete (it is: zero set of analytic ζ restricted... the nontrivial zeros form a closed discrete set — need `DiscreteTopology` instance or the closedness: {ρ : IsNontrivialZero ρ} — hmm: is it closed in ℂ? The zeros of Λ are closed (preimage of 0 under continuous Λ restricted... Λ is entire? completedRiemannZeta analytic on ℂ∖{0,1} hmm — Mathlib's completedRiemannZeta has junk at 0,1 but IsNontrivialZero excludes those neighborhoods anyway. The set {IsNontrivialZero} = {ζ = 0} ∩ {0 < re} ∩ {re < 1} — {ζ = 0} ∩ open strip: closed in the strip... For the F-entirety argument: F = ζ′/ζ − [series + elem] is analytic on ℂ ∖ ({zeros} ∪ {1} ∪ {0} ∪ {−2n}) and has removable singularities at each excluded point ⟹ extends to entire. Removable singularity: in Lean, `AnalyticAt` extension — the residue cancellation gives boundedness near each point ⟹ Riemann removable singularity theorem. Does Mathlib have the removable singularity theorem for analytic functions? `AnalyticOnNhd.insert`? or `DifferentiableOn.insert...`: there's `DifferentiableOn.differentiableAt_of...`? The cleanest available: if f is analytic on a punctured neighborhood and BOUNDED near the point (or tends to a limit), then extends — Mathlib: `AnalyticAt` of the extension... I recall `Complex.differentiableOn_update_...`? or `Differentiable.insert`? Hmm — there's `DifferentiableOn.insert` in recent Mathlib? and for analytic: the standard route is: bounded + analytic on punctured ball ⟹ differentiable at the point after redefinition ⟹ analyticAt via `Complex.analyticAt_iff_eventually_differentiableAt`. The bounded-near-pole ⟹ removable: Mathlib has `isRemovableSingularity` machinery? I don't think Mathlib has the full Riemann removable singularity theorem for ℂ. Alternative: residue-cancellation gives F(s) → finite limit as s → ρ (the principal parts cancel exactly: F = (ζ′/ζ − m/(s−ρ)) − [other series terms + elem] where the bracket is analytic at ρ and ζ′/ζ − m/(s−ρ) is analytic at ρ by the logDeriv-NF machinery (ii′-1b built exactly this: logDerivResidue / the Ffun−TaylP order argument). So F = (analytic at ρ) − (analytic at ρ) — if we can WRITE F as the difference of two functions analytic at ρ, then F is analytic at ρ DIRECTLY (no removable-singularity theorem needed!). The decomposition: F(s) = [ζ′/ζ(s) − m_ρ/(s−ρ)] − [Σ_{ρ'≠ρ} m(1/(s−ρ')+1/ρ') − 1/s − 1/(s−1) + ½logπ − ½ψ(s/2) + m_ρ/ρ]: the first bracket analytic at ρ (ii′-1b logDeriv machinery: logDeriv ζ minus its principal part is analytic — that's `logDerivResidue`-adjacent; ii′-1b proved residue facts which need exactly this analyticity — check what's available: LiSides' rectInt'_Jlag used \"logDeriv NF residues at zeros\" — the underlying analyticity of logDeriv ζ s − m/(s−ρ) at ρ should be extractable); the second bracket analytic at ρ (the series over ρ' ≠ ρ converges locally uniformly near ρ since the nearest other zero is a positive distance away — zeros discrete! Need: ρ isolated among zeros — discreteness of the zero set: the zero set of Λ in the strip is discrete (zeros of analytic function, not identically zero) — Mathlib: `AnalyticOnNhd.isolated_zeros`? there's the discrete-zero-set machinery (isCompact...inter_riemannZetaZeros_finite used everywhere — implies local finiteness ⟹ isolation). And the elementary terms at ρ: 1/s, 1/(s−1), ψ(s/2) all analytic at ρ (re ρ ∈ (0,1) — away from 0, 1, and −2n) ✓.\n\n   This \"split the principal part\" route avoids the removable-singularity theorem entirely. \n\n3. The growth bound on γ-gap circles |s| = R_k:\n   Choose R_k → ∞ with the circle crossing the strip at ordinates ±t, |t − γ| ≥ δ_k for ALL zero ordinates γ — via the perimeter pigeonhole on unit windows: exists_zero_avoiding_T (ii′-4) gives T ∈ [a, a+1] with |T − γ| ≥ 1/(3·C₀(a+1)) for all γ in... wait — exists_zero_avoiding_T gives clearance from zeros with ordinate in the WINDOW. The circle |s| = R_k crosses the strip at t ≈ ±R_k; zeros with ordinate near ±R_k: the gap needs |t − γ| ≥ δ for ALL γ — the zeros with |γ| near R_k are finitely many (in the window [R_k−2, R_k+2]) and the pigeonhole gives t ∈ [R_k−1, R_k+1]-ish avoiding them... The classical choice: T_k ∈ [k, k+1] (integer k) with clearance 1/(A log k)-ish from all ordinates in that window, and the circle radius R_k = T_k (or the horizontal LINE im = ±T_k — Davenport uses horizontal lines for the Γ-factor estimate and circles for the Liouville part... hmm). Actually for the Liouville argument (F const): need |F(z)| = o(|z|) on |z| = R_k → ∞. On the circle: |F| ≤ |ζ′/ζ| + |series| + |elem|. The 5c/5d bounds need |t| ≥ 10 — the circle parts with |im s| < 10: near s = ±R real: re s ≈ ±R: at re s ≈ +R: ζ′/ζ = O(1) (Dirichlet series, re > 1 — hmm re s ≥ 2 say: |ζ′/ζ| ≤ Σ Λ(n)/n^σ ≤ C for σ ≥ 2 ✓ elementary, or via the 5c bound at... 5c needs re ∈ [1/2, 7/2] — for re s > 7/2 use the Dirichlet series bound |ζ′/ζ(s)| ≤ |ζ′(2)|/|ζ(2)|-ish for re ≥ 2: the Dirichlet series Σ Λ(n)n^{−s} converges absolutely for re > 1 — Mathlib LSeries vonMangoldt: `LSeries_vonMangoldt_eq` : −ζ′/ζ = Σ Λ(n)/n^s for re > 1 — inventory confirmed \"LSeries vonMangoldt ✓\" in session 019). At re s ≈ −R (leftmost): FE-reflection (5d) needs |t| ≥ 10 too! For |t| < 10, re s ≈ −R: the FE directly: ζ′/ζ(s) = −ζ′/ζ(1−s) − [ΓR-bracket] — 1−s has re ≈ 1+R (Dirichlet O(1)) and the bracket: logDeriv ΓR(1−s) = O(log R) (digamma_stirling at re > 0, |im| < 10 — the StirlingVert needs |im| ≥ 1/2! For |im| < 1/2: ψ(w) with re w ≈ R/2 real-ish: ψ(w) = log w + O(1) for re w large positive — the REAL Stirling for digamma at real arguments: is there a Mathlib/Zeta23 bound? re_digamma_stirling (StirlingVert:550) is for a ∈ (0,1]... hmm. For w real large: ψ(w) ~ log w — via the digamma series or the recurrence from a fixed window: ψ(w) = ψ(w−⌊w⌋+⌊w⌋)... Actually for re w ≥ 2, ANY im: digamma_stirling needs |im| ≥ 1/2; for |im| < 1/2 and re w ≥ 2: shift w → w+1 doesn't help (im unchanged). Use the SERIES (Zeta23 digamma_series — works for all z off the integers!): ψ(w) = −γ − 1/w + Σ_n (1/(n+1) − 1/(w+n+1)): the sum: Σ [1/(n+1) − 1/(w+n+1)] = Σ w/((n+1)(w+n+1)): bound: |w/((n+1)(w+n+1))| ≤ |w|/((n+1)|w+n+1|): split n ≤ 2|w| (n+1 > ... hmm |w+n+1| ≥ re w + n + 1 ≥ 2 (re w ≥ 2 ⟹ wait for the LEFT point w = s/2 with re s ≈ −R: re w ≈ −R/2 NEGATIVE large. Let me redo: the bracket at s (re ≈ −R, |im| < 10): logDeriv ΓR(s) = −(logπ)/2 + ½ψ(s/2) — needs the SHIFTED form (re(s/2) ≈ −R/2 < 0!): the +4 shift of 5d only helps FIXED shifts; for re s ~ −R need the general left-plane bound — THIS is what the 5d left-plane digamma bound is for! ‖ψ(w) − log w‖ ≤ 3 for |im w| ≥ 2 — but here |im w| = |im s|/2 < 5 possibly < 2! The near-axis case again. And w = s/2 near the negative real axis at re ≈ −R/2: the circle |s| = R crosses the negative real axis at s = −R exactly: w = −R/2: for R = 2k+1 odd: w = −k−1/2 half-integer ✓ away from poles by 1/2. So the near-axis left-plane bound needs: ‖ψ(w)‖ ≤ C log(2+‖w‖) for w with dist(w, {0,−1,−2,...}) ≥ 1/4 — via the Weierstrass series (Zeta23 digamma_series!): ψ(w) + γ + 1/w = Σ_{n} w/((n+1)(w+n+1)): |Σ| ≤ |w| Σ_n 1/((n+1)|w+n+1|): split n+1 ≤ 2‖w‖: |w+n+1| ≥ 1/4 (distance condition): term ≤ 4/((n+1))·... wait: |w|/((n+1)·(1/4)) = 4|w|/(n+1) — sum over n+1 ≤ 2‖w‖: 4|w|·O(log‖w‖) = O(R log R) — TOO BIG?! Hmm no wait: |w/((n+1)(w+n+1))| with |w+n+1| ≥ 1/4: ≤ |w|·4/(n+1): Σ_{n<2|w|} 4|w|/(n+1) ≈ 4|w|·log(2|w|) = O(R log R). That's too big — the bound must use cancellation better: |1/(n+1) − 1/(w+n+1)| = |w/((n+1)(w+n+1))| — for n+1 ≤ 2|w| there's no cancellation help; the true size: Σ_{n<2|w|} |w|/((n+1)|w+n+1|): for w near −k−1/2 (half-integer): |w + n+1| for n+1 near k: ~1/2: those terms: |w|/((n+1)·(1/2)) ~ 2|w|/(n+1) ~ 2|w|/k ~ O(1) each for n+1 ~ k — and O(1) many such n... hmm no: |w+n+1| ≥ 1/4-ish for ALL n (distance condition) but |w+n+1| is SMALL (~1/2) for the O(1)-many n near −re w. Let me recount the sum: Σ_{n=0}^{2|w|} |w|/((n+1)|w+n+1|) ≤ Σ |w|·4/(n+1) = 4|w|·H_{2|w|} ~ 4|w| log|w| — that's the crude bound; but the terms with n+1 NOT near k have |w+n+1| ≥ |n+1−k|−1: for n+1 ≤ k/2: |w+n+1| ≥ k/2 − 1 ≥ |w|/3: term ≤ |w|/((n+1)·|w|/3) = 3/(n+1): Σ_{n<k/2} 3/(n+1) = O(log k) ✓; for n+1 ∈ [k/2, 2k]: |w+n+1| ≥ 1/4: term ≤ 4|w|/(n+1) ≤ 4|w|/(k/2) = 8|w|/k ≈ 16 (since |w| ≈ k): and there are ~3k/2 such terms ⟹ ≈ 16·(3k/2) = O(k) = O(R) — TOO BIG. Hmm — wait that's wrong: for n+1 ∈ [k/2, 2k], |w + n+1| ≥ ...: w ≈ −k−1/2: w + n+1 ≈ n+1−k−1/2 = n−k+1/2: for n ∈ [k/2, 2k]: n−k+1/2 ranges over [−k/2, k+1/2]-ish: |n−k+1/2| ≥ 1/2 (half-integers!) — the distance from half-integers: n − k + 1/2 is a half-integer, |·| ≥ 1/2 ✓. So |w+n+1| ≥ |re(w+n+1)| − ... ≥ 1/2 − |im w|. With |im w| < 1/2 − δ... ugh — the distance condition dist(w, −ℕ) ≥ 1/4 gives |w+n+1| ≥ 1/4 pointwise but the sum Σ_{n ≤ 2k} 4|w|/(n+1) is what it is. The issue: for n in the range where |w+n+1| is small but nonzero (≥1/4), the term 4|w|/(n+1) summed over n ∈ [k/2, 2k] gives 4|w|·(H_{2k} − H_{k/2}) = 4|w|·log 4 = O(|w|) = O(R). TOO BIG.\n\n   Hmm — but the TRUE ψ at half-integers: ψ(−k−1/2) — via the recurrence ψ(−k−1/2) = ψ(1/2) − Σ_{j=0}^{k} 1/(−k−1/2+j)·(−1)... ψ(z+1) = ψ(z) + 1/z: ψ(1/2) = ψ(−1/2) + 1/(−1/2) = ψ(−1/2) − 2: so ψ(−1/2) = ψ(1/2) + 2; ψ(−3/2) = ψ(−1/2) + 1/(−3/2)... wait recurrence backward: ψ(z) = ψ(z+1) − 1/z: ψ(−1/2) = ψ(1/2) − 1/(−1/2) = ψ(1/2) + 2; ψ(−3/2) = ψ(−1/2) + 2/3; ψ(−k−1/2) = ψ(1/2) + Σ_{j=1}^{k} 2/(2j−1) = ψ(1/2) + 2H_{2k} − H_k ≈ ψ(1/2) + log k + ... = O(log k) ✓. So the TRUE value is O(log R) — my crude sum bound was just lossy. The right bound: ψ(w) = ψ(w+m) − Σ_{j=0}^{m−1} 1/(w+j) with m chosen so re(w+m) ∈ [1,2]: Σ_j 1/(w+j): for w near −k−1/2 real: the sum Σ_{j=0}^{m−1} 1/(w+j) with w+j ∈ [−k−1/2+j...]: values −k−1/2, −k+1/2, ..., — the terms 1/(w+j) = 2/(2(w+j)): the 2(w+j) are odd integers (for w exactly −k−1/2): Σ 2/(odd integer from −2k−1 to −1)·(−)... all NEGATIVE halves: 1/(w+j) = −2/(2k+1−2j): Σ_{j=0}^{m−1} −2/(2(k−j)+1) = −Σ_{i} 2/(2i+1) = −(2H_{2k}−H_k) = −log k − ... ✓ O(log k). For the bound: |Σ_{j} 1/(w+j)| = Σ 2/|2(w+j)| ≤ Σ 2/(2i+1) = O(log m) — using that the 2(w+j) are 2-separated reals with |2(w+j)| ≥ 1: Σ_j 1/|w+j| ≤ Σ_j 2/(1+2·dist_j)... with 1-separated |w+j| values ≥ 1/2: Σ_j 1/|w+j| ≤ 2·Σ_{i≥0} 1/max(1/2, i) = 2(2 + H_m) = O(log m) ✓✓. So the KEY elementary fact: for 1-separated points w+j each with |w+j| ≥ 1/2 (or 1/4), Σ_{j=0}^{m−1} 1/|w+j| ≤ C·log(m+1) — a clean real estimate (pairing j's into unit bins). So the near-axis left-plane bound: ‖ψ(w) − ψ(w+m)‖ = ‖Σ 1/(w+j)‖ ≤ C log m and ‖ψ(w+m)‖ ≤ C' log‖w+m‖-ish (right-half StirlingVert or... re(w+m) ∈ [1,2], |im(w+m)| < 1/2 possibly: digamma_stirling needs |im| ≥ 1/2! For |im| < 1/2 with re ∈ [1,2]: ψ is continuous on the COMPACT set {re ∈ [1,2], |im| ≤ 1/2} — uniformly bounded there! ✓ (ContinuousOn.compact). So: ‖ψ(w)‖ ≤ C + C log m + (compact bound) ≤ C log(2+‖w‖) for dist(w, −ℕ) ≥ 1/2·... \n\n   OK — so the near-axis digamma piece: ψ(w) = ψ(w+m) − Σ_{j<m} 1/(w+j) with: (i) the reciprocal-sum estimate Σ_{j<m} 1/|w+j| ≤ C log(m+1) for {w+j} 1-separated and |w+j| ≥ 1/4; (ii) ψ(w+m) bounded via compactness (|im| < 1/2) or StirlingVert (|im| ≥ 1/2). This is a SECOND left-plane digamma bound, distinct from 5d's (which needed |im| ≥ 2 for the slit-plane FTC). The design doc should include it as a 5e sub-build: `norm_digamma_le_log_of_memintegerComplement_ball`... call it the \"near-axis digamma bound\".\n\n   Actually WAIT — let me reconsider. Do we even need the near-axis case? The γ-gap circles: |s| = R_k with R_k chosen odd (R_k = 2k+1) so the negative crossing is at half-integers. The points on the circle with |im s| < 10: s ≈ ±R_k. At the LEFT point (re s ≈ −R_k): the FE-reflection sends s ↦ 1−s with re ≈ 1+R_k: and ζ′/ζ(s) = −ζ′/ζ(1−s) − [logDeriv ΓR(1−s) + logDeriv ΓR(s)]: logDeriv ΓR(s) with re s ≈ −R_k, |im s| < 10: w = s/2: re w ≈ −R_k/2, |im w| < 5 — the near-axis left-plane case (could have |im w| < 2) ⟹ need the near-axis bound with the half-integer distance condition: dist(s/2, −ℕ) ≥ 1/4: s/2 near −(k+1/2): |s/2 − (−k)| = |s/2 + k| where s on the circle near −R_k = −(2k+1): s/2 + k ≈ −1/2 + (s+R_k)/2: |s + R_k| on the circle near the crossing: can be up to... the circle points near −R_k: |s/2 + k| ≥ |re(s/2) + k| — for s with |im s| < 10 on the circle of radius 2k+1: re s ∈ [−(2k+1), −√((2k+1)²−100)]: re(s/2)+k ∈ [−1/2, −1/2 + (2k+1−√((2k+1)²−100))/2] = [−1/2, −1/2 + 50/(2(2k+1)+...)] ≈ [−1/2, −1/2+25/(2k)]: so |re(s/2)+k| ∈ [1/2 − 25/(2k), 1/2] ≥ 1/4 for k ≥ 25 ✓. And similarly dist to OTHER −m: |re(s/2)+m| ≥ 1/2 − 25/(2k) ≥ 1/4 ✓ for all m. So on the circle's near-axis left part: dist(s/2, −ℕ) ≥ 1/4 ✓ (for R_k = 2k+1, k large). The near-axis digamma bound applies.\n\n   Also — hmm, actually, wait. Let me reconsider the circle choice. Davenport's classical argument (Ch. 15) uses |s| = R with R chosen among odd INTEGERS also avoiding the zero ordinates: R must satisfy BOTH: (a) R odd (trivial-zero clearance on the negative real part), (b) |R − γ| ≥ c/log R for all zero ordinates γ (nontrivial-zero clearance at the strip crossings). A radius satisfying both: pick the odd integer in [T, T+2] and then adjust within a unit window for the γ-gap... the pigeonhole (exists_zero_avoiding_T, ii′-4) gives T ∈ [a, a+1] with clearance 1/(3C₀(a+1)) from the window ordinates; take the odd integer nearest... hmm — an odd INTEGER can't be adjusted continuously. The classical trick: circles of radius R_k where R_k ∈ [2k+1, 2k+3] is chosen in a γ-gap (pigeonhole on the window), NOT necessarily an odd integer — then the negative-real crossing at −R_k is NOT a half-integer... The trivial-zero clearance: dist(−R_k/2, −ℕ) ≥ 1/4: R_k/2 ∈ [(2k+1)/2, (2k+3)/2] = [k+1/2, k+3/2]: dist to integers ≥ ... R_k/2 ∈ [k+1/2, k+1/2+... hmm R_k ∈ [2k+1, 2k+3] ⟹ R_k/2 ∈ [k+0.5, k+1.5]: if R_k/2 ∈ [k+0.75, k+1.25] problem (near integer k+1 within 1/4). The pigeonhole window for R can be chosen within [2k+1, 2k+1.9] ∪... — actually just: choose the unit window [a, a+1] for the γ-gap with a = 2k+1: R ∈ [2k+1, 2k+2] ⟹ R/2 ∈ [k+0.5, k+1]: dist(R/2, ℤ) ≥ ... R/2 near k+1 when R near 2k+2 — restrict R ∈ [2k+1, 2k+1.5] ⟹ R/2 ∈ [k+0.5, k+0.75] ⟹ dist to ℤ ≥ 1/4 ✓. But the γ-gap pigeonhole needs a full unit window to work (k+1 midpoints at spacing 1/(k+1)-ish... exists_zero_avoiding_T's window form: clearance 1/(3·C0hat(a+1)) in ANY unit window [a, a+1] — can I use a HALF window [2k+1, 2k+1.5]? The midpoint pigeonhole on k+1 midpoints inside a window of length 1/2: spacing 1/(2(k+1))-ish — the argument scales: with M window-ordinates and window length L: clearance L/(2(M+1))-ish by the same midpoint trick. The C₀ count scales with the window position (~log a) not length ✓. So a flexible-window pigeonhole variant of exists_zero_avoiding_T gives R ∈ [2k+1, 2k+1.5] with γ-clearance ≍ 1/log k AND R/2 ∈ [k+0.5, k+0.75] giving the ℤ-clearance 1/4 ✓. Or simpler: take the unit-window T from exists_zero_avoiding_T directly and set R := 2T? R/2 = T ∈ [k+... hmm R = 2T with T ∈ [a, a+1]: R ∈ [2a, 2a+2], R/2 = T arbitrary real — dist(T, ℤ) uncontrolled. No. Use the flexible window. Design note: \"the radius R_k ∈ [2k+1, 2k+3/2] chosen by the midpoint pigeonhole to avoid all zero ordinates in [2k, 2k+3] by ≍ 1/log k; then R_k/2 ∈ [k+1/2, k+3/4] has dist(·, ℤ) ≥ 1/4\" — need exists_zero_avoiding_T generalized to arbitrary windows [a, a+L] with L ∈ [1/2, 1] say — a small variant (the current one is unit-window specific; the proof scales). Pin in the design as sub-build (5e-i).\n\n   And the ORDINATE-clearance needed on the circle: at the strip crossings (re s ∈ [−1/2, 2]-ish, |s| = R): t = ±√(R²−σ²): |t − R| ≤ 1/R (computed earlier: R − √(R²−σ²) ≤ σ²/(2R)·2 = σ²/R ≤ 4/R for |σ| ≤ 2); so |t − γ| ≥ |R − γ| − 4/R ≥ c/log R − 4/R ≥ c/(2 log R) for R large ✓. THEN: the near-zero sum Σ_{|γ−t|<1} m/(s−ρ): each |s−ρ| ≥ |t−γ| ≥ c/(2log R)?? no wait — the near zeros ρ have |γ − t| < 1; the bound |s − ρ| ≥ |im(s−ρ)| = |t − γ| ✓ ≥ c/(2 log R) for those with |γ−t| < 1 — hmm but |t − γ| ≥ c/log R only for γ in the WINDOW [R−1, R+1]-ish... the pigeonhole gave clearance from ordinates in [a, a+1] ∋ R — zeros with |γ − R| ≤ 2: the window [R−1, R+1] ⊂ [a−... the pigeonhole on [a, a+1] with a = 2k+1 and R ∈ [2k+1, 2k+1.5]: zeros with ordinate in [2k, 2k+3]: does exists_zero_avoiding_T's clearance cover γ ∈ [a−1, a+2]? The midpoint argument: k+1 midpoints in [a, a+1]; a midpoint is BAD if within-clearance of some γ; each γ makes ≤ ... midpoints bad — the clearance needed is from γ's in a WIDER range [a−1, a+2] (since |t−γ| with t ∈ [a,a+1] and clearance c covers γ up to a+1+c...). The zeros with |γ − t| < 1 for t ∈ [a, a+1] have γ ∈ (a−1, a+2): the badness count must include those: M' = zeros in [a−1, a+2] ≤ 3·C₀(a+2)-ish (three unit windows) — the current exists_zero_avoiding_T might already do exactly this (it was designed for the contour application with clearance against the right range). D-067/ii′-4: \"exists_zero_avoiding_T — clearance 1/(3·C0hat(a+1)) in any unit window [a, a+1]\" — the C0hat form suggests the count bound used covers the needed range (it was built for the rectangle residue theorem where the horizontal edges at height T must avoid ALL zeros — same requirement!). So exists_zero_avoiding_T likely already gives |T − γ| ≥ 1/(3·C0hat(a+1)) for ALL zeros γ (not just window ones — a zero with |γ − T| < clearance is within the relevant windows automatically). Check at build: if its statement covers all zeros, use directly with R ∈ unit window; the R/2-ℤ-clearance then needs R/2 ∈ half-integer ± 1/4: choose the window [a, a+1] with a ≡ adjusted... T ∈ [a, a+1] arbitrary real ⟹ T/2 arbitrary — no ℤ-clearance. So EITHER flexible-window pigeonhole OR: two-step — pick window [4k+2, 4k+3]?? T ∈ [4k+2, 4k+3] ⟹ T/2 ∈ [2k+1, 2k+1.5]: dist(T/2, ℤ) ≥ 0? T/2 could be 2k+1 exactly (integer!) or near — no control. Hmm — T/2 ∈ [2k+1, 2k+1.5] — the ℤ-distance is ≤ 1/2 always and could be 0 (T = 4k+2 ⟹ T/2 = 2k+1 ∈ ℤ — but then s = −T at... wait the crossing point is −R = −T: −T/2 = −(2k+1) EXACTLY an odd negative integer IF T = 4k+2: that's a TRIVIAL ZERO location −(2k+1)?? no — trivial zeros are at −2n (EVEN negative integers). −(2k+1) is an ODD negative integer — ζ(−(2k+1)) = −Bernoulli... ζ at odd negative integers is NONZERO (ζ(−1) = −1/12). And ψ(s/2) at s/2 = −(2k+1)/2 = −k−1/2: half-integer — regular ✓. The dist condition needed for the digamma bound is dist(s/2, {0,−1,−2,...}) = dist(s/2, −ℕ) ≥ 1/4: s/2 = −T/2 ∈ [−(2k+1.5), −(2k+1)]: dist to −ℕ: T/2 ∈ [2k+1, 2k+1.5]: the nearest nonnegative integers: 2k+1 (distance T/2−(2k+1) ∈ [0, 0.5]) and 2k+2 (distance ∈ [0.5, 1]): so dist(T/2, ℕ) = T/2 − (2k+1) ∈ [0, 1/2] — can be 0 if T = 4k+2 exactly! So I need T bounded AWAY from 4k+2 by ≥ 1/2·... T/2 − (2k+1) ≥ 1/4 ⟺ T ≥ 4k+2.5; and T ≤ 4k+3 gives T/2 ≤ 2k+1.75: dist to 2k+2 ≥ 0.25 ✓. So choose the γ-gap T in the HALF-window [4k+2.5, 4k+3] (length 1/2) — needs the flexible-window pigeonhole (window length 1/2): clearance ≍ (1/2)/(2(M+1)) with M ~ C₀(4k+3)-ish ~ log k ✓ same order. OK so: sub-build (5e-i): the flexible/half-window version of exists_zero_avoiding_T. The midpoint argument generalizes: in a window of length L with M bad points, k+1 midpoints spaced L/(2(M+1))-ish... the existing proof used the unit window's specifics; the generalization is a thin wrapper (rescale like session-024's ×10 trick! apply the unit-window lemma to the scaled zero set — the ×10-rescale trick from 5c: exists_avoiding_midpoint at a = 23 on the ×10 image... — the same trick applies: scale by 2: T ∈ [4k+2.5, 4k+3] ⟺ 2T ∈ [8k+5, 8k+6] unit window ⟹ apply exists_zero_avoiding_T at a = 8k+5 to the ×2-scaled ordinate set {2γ}: clearance 1/(3C₀(8k+6)) in the 2γ-scale ⟹ T-clearance half that. Clean — the ×2-rescale trick, zero new pigeonhole).\n\n   Hmm wait — but the ×2-scaled zero set {2γ}: exists_zero_avoiding_T is about ZETA's zeros (it takes the ZeroCountProp perimeter + the actual zero set). Scaling the zero set means applying the lemma to a DIFFERENT function's zeros... In 5c, the ×10 trick worked because the midpoint pigeonhole `exists_avoiding_midpoint` was a GENERAL combinatorial lemma (any finite set of reals), applied to the scaled norm set. Is exists_zero_avoiding_T built on a general midpoint lemma? ii′-4: \"the midpoint pigeonhole exists_avoiding_midpoint (k+1 midpoints, injective-badness)\" — YES it's a general lemma about finite sets in a window, and exists_zero_avoiding_T = the general lemma + the zero-count bound. So the flexible version = exists_avoiding_midpoint on the ×2-scaled ordinate finset + the count bound on the scaled window (which maps back to a unit-window count at a different position: {γ : 2γ ∈ [8k+5, 8k+6]} = {γ ∈ [4k+2.5, 4k+3]} ⊆ two unit windows' count ✓ via ZeroCountProp at 4k+2 and 4k+3... the perimeter count is per unit window — the half-window is inside [4k+2, 4k+3]∪[4k+3,4k+4]: two applications ✓). Fine — sub-build (5e-i) is a thin wrapper ~0.25 sess.\n\n4. F const via Liouville: F entire + |F(z)| ≤ C(log R)² on |z| = R_k → ∞: G(z) := (F(z) − F(0))/z entire (removable at 0: G(0) = F′(0)... G is analytic on ℂ∖{0}, and near 0: (F(z)−F(0))/z → F′(0): G extends: Mathlib — is there a lemma for this? `Complex.differentiable_divide...`? The standard: if F analytic with F(0) = 0 then F(z)/z analytic: `AnalyticAt.zpow...`? There's `AnalyticAt.div` needs denom nonzero; the removable-z case: `AnalyticOnNhd.exists_...`? Hmm — Mathlib HAS the removable singularity for THIS special case: `Complex.differentiableAt_of_...`? Let me think: F(z) = Σ a_n z^n power series (analyticAt gives the power series!): F(z) − F(0) = z·Σ a_{n+1}z^n: G(z) = Σ_{n≥0} a_{n+1} z^n analytic by the power-series manipulation — `AnalyticAt` has `AnalyticAt.exists_...`? There should be a lemma: `(hf : AnalyticAt ℂ f z) : AnalyticAt ℂ (fun w => (f w - f z)/(w - z)) z`? — the \"difference quotient is analytic\" — I don't remember its exact name; might need to build via the power series (AnalyticAt gives HasFPowerSeriesAt; the tail series: `HasFPowerSeriesAt` manipulation — there might be `HasFPowerSeriesAt.div_sub...`? or use `Complex.differentiableAt_...`. Alternatively AVOID G: use the Cauchy estimate directly: F(z) − F(0) = (1/2πi)∮ ... — or the classical: |F(z) − F(0)| ≤ max_{|w|=R} |F(w)−F(0)| · |z|/(R−|z|) via the maximum modulus on (F(w)−F(0))/w... — that's the same thing. The cleanest Lean route may be: Mathlib's `Complex.liouville` exists? There's `Differentiable.liouville`? Mathlib has Liouville's theorem: `Differentiable.liouville : Differentiable ℂ f → (∃ C, ∀ z, ‖f z‖ ≤ C) → f = const`? — I recall `Differentiable.apply_eq_apply_of_bounded`? or `Differentiable.liouville`? Something like: bounded entire functions are constant — Mathlib: `Differentiable.apply_eq_apply_of_bounded (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) : f z = f w`? There's definitely SOME Liouville in Mathlib (used for fundamental theorem of algebra). For the o(R) version: G(z) = (F(z)−F(0))/z entire + bounded (|G| ≤ C(log R)²/R + |F(0)|/R → bounded on the circles R_k, hence by max-modulus on the discs, hence globally by R_k → ∞) ⟹ G const ⟹ F(z) = F(0) + c·z; then |F(R_k)| ≤ |F(0)| + |c|R_k vs |F| ≤ C(log R_k)² on the circle ⟹ |c| ≤ C(log R_k)²/R_k → 0 ⟹ c = 0 ⟹ F ≡ F(0) =: −B... So I need: (a) the difference-quotient analyticity, (b) Liouville, (c) the max-modulus transfer (have it? Zeta23 has AnalyticOn.norm_le_of_norm_le_on_sphere — used in 5c ✓ — \"AnalyticOn.norm_le_of_norm_le_on_sphere\" on balls: |G| ≤ circle-max inside ✓). For (a): check Mathlib for the difference quotient; if missing, build via power series (HasFPowerSeriesAt.tail? — there might be `HasFPowerSeriesAt.eq_sub...`? hmm).\n\n   Let me note (a) as an inventory question in the design.\n\n5. The series-on-circle bound (dyadic split): Σ_ρ m_ρ |1/(s−ρ) + 1/ρ| on |s| = R: split zeros by |ρ|: |ρ| ≤ 2R: |1/(s−ρ) + 1/ρ| = |s|/(|ρ||s−ρ|) ≤ R/(|ρ|·|s−ρ|): for |s−ρ|: ≥ |t−γ| ≥ c/(2 log R) for the strip-ordinates near t... hmm — this mixes. Actually the classical: |Σ m(1/(s−ρ)+1/ρ)| ≤ Σ_{|ρ|≤2R} m·R/(|ρ||s−ρ|) + Σ_{|ρ|>2R} 2mR/|ρ|². The far sum: ≤ 2R·Σ_{|ρ|>2R} m/|ρ|² ≤ 2R·C/(2R)·log... Σ_{|ρ|>X} m/|ρ|² ≤ C log X/X·... via the count C₀: Σ_{|ρ|>X} m/|ρ|² ≍ Σ_{k>X} (log k)/k² = O(log X/X) ⟹ far sum = O(log R) ✓. The near sum: Σ_{|ρ|≤2R} m·R/(|ρ||s−ρ|): |s−ρ| ≥ |t−γ| ≥ c/(2log R) for ALL ρ on the circle — wait that's only for the strip zeros near the crossing heights; zeros at OTHER ordinates have |s−ρ| ≥ ... |s − ρ| ≥ ||s| − |ρ|| hmm no. For |ρ| ≤ 2R and s on the circle: |s − ρ| ≥ |im s − γ| — but γ far from t: |im s − γ| = |t − γ| ≥ 1 if |γ − t| ≥ 1 ✓. Only the zeros with |γ − t| < 1 (near the crossing ordinate) are dangerous, and those have |t − γ| ≥ c/(2 log R) by the gap choice ⟹ |s−ρ| ≥ c/(2log R) ⟹ those terms ≤ m·R·(2log R)/(c·|ρ|). And |ρ| ≥ ... for the near-crossing zeros |ρ| ≥ |γ| ≥ R−2: 1/|ρ| ≤ 1/(R−2): terms ≤ m·R·2logR/(c(R−2)) ≍ m·2logR/c; summed over ≍ C₀ ≍ log R zeros: O((log R)²) ✓. The middle zeros (|γ−t| ∈ [1, ...]): |s−ρ| ≥ 1: terms ≤ mR/|ρ|: Σ_{|ρ|≤2R, |γ−t|≥1} m/|ρ| ≍ Σ_{k≤2R} (log k)/k = O((log R)²) ⟹ ·R?? NO: m·R/|ρ| summed = R·Σ m/|ρ| = R·O((log R)²) — TOO BIG! Hmm. Wait — the classical bound: the series Σ m(1/(s−ρ)+1/ρ) — the +1/ρ terms matter: |1/(s−ρ) + 1/ρ| = |s|/(|ρ||s−ρ|)... for |s−ρ| ≥ 1 that's ≤ R/|ρ| — summed over the ≍ R log R zeros up to 2R — R·Σ_{k} (log k)/k ≍ R(log R)² — that's O(R(log R)²) which is NOT o(R)!! Hmm — something's off vs the classical argument. Let me recheck: Davenport's Ch. 15/16 argument for the partial fraction formula... The classical proof of ζ′/ζ(s) = B + Σ_ρ(1/(s−ρ)+1/ρ) + ... does NOT go through the circle-Liouville on the FULL series — it truncates: ζ′/ζ(s) = Σ_{|γ−T|<1...}... Actually the classical proof (Davenport Ch. 12 for ξ): ξ′/ξ(s) = B + Σ_ρ(1/(s−ρ) + 1/ρ) via the HADAMARD PRODUCT — which we ruled out (no Weierstrass/order theory in Mathlib). D-067 §6's route avoids Hadamard by the circle argument on F = ζ′/ζ − Σ − elem. The circle bound on the series: hmm — maybe the split should be at |ρ| ≤ R/2 (not 2R): |1/(s−ρ)+1/ρ| = |s/(ρ(s−ρ))| ≤ R/(|ρ|·(R−|ρ|)) ≤ R/(|ρ|·R/2) = 2/|ρ| for |ρ| ≤ R/2: Σ_{|ρ|≤R/2} 2m/|ρ| = O((log R)²) ✓!! (the |s−ρ| ≥ R − |ρ| ≥ R/2 uses |ρ| ≤ R/2 — the CIRCLE radius vs the zero moduli!) For R/2 < |ρ| ≤ 2R: |s−ρ| ≥ |im difference| or the gap... these zeros have |ρ| ≍ R: |s−ρ| ≥ |t−γ| and |t−γ| for γ with |γ| ∈ (R/2, 2R]: hmm — t ≈ ±R and γ ∈ (R/2, 2R]: |t−γ| can be small only for γ ≈ R: within the gap window: |t−γ| ≥ c/(2logR) for |γ−R| ≤ 2 (the pigeonhole window) and ≥ ... for γ ∈ (R/2, R−2]: |t−γ| ≥ |R−γ| − 4/R ≥ 2 − 4/R ≥ 1 ✓. So: zeros with |ρ| ∈ (R/2, 2R]: the dangerous ones are |γ−R| ≤ 2 (count ≍ log R via C₀, each term ≤ m·R/(|ρ|·c/(2logR)) ≤ m·2logR/c·(R/(R−2)) ≍ 2m logR/c) ⟹ O((log R)²); the rest |s−ρ| ≥ 1: terms ≤ m·R/|ρ| ≤ m·R/(R/2) = 2m: Σ_{R/2<|ρ|≤2R} 2m ≍ 2·(zeros in annulus) ≍ 2·C₀·... zeros with |ρ| ∈ (R/2, 2R]: ~ R log R?!?! NO — the zeros with MODULUS in (R/2, 2R] have ORDINATES in that range: count ≍ R log R (that's the zero density N(T) ~ T log T). 2m summed over R log R zeros = O(R log R) — TOO BIG again!! \n\n   Hmm wait — that can't be right classically. Let me recompute: the term for |ρ| ∈ (R/2, 2R] with |s−ρ| ≥ 1: |1/(s−ρ) + 1/ρ| = |s/(ρ(s−ρ))| ≤ R/(|ρ|·1) ≤ R/(R/2) = 2. Number of such zeros (mult-weighted): zeros with modulus in (R/2, 2R] — the zeros in the strip with |γ| ∈ (R/2, 2R] but also |β| ≤ 1: |ρ| ≍ |γ| so γ ∈ (R/2, 2R] ∪ [−2R, −R/2): count ≍ 2R·log R − (R/2)log(R/2) ≍ R log R. So the sum ≍ 2·R log R = O(R log R) — NOT o(R). PROBLEM.\n\n   So the naive |1/(s−ρ)+1/ρ| ≤ R/(|ρ||s−ρ|) bound is too lossy — the classical argument must use cancellation: 1/(s−ρ) + 1/ρ = s/(ρ(s−ρ)): for |s−ρ| ≥ 1 the term is s/(ρ(s−ρ)) = s/ρ²·(ρ/(s−ρ)) = s/ρ²·(−1 + s/(s−ρ))... hmm: ρ/(s−ρ) = −1/(1−s/ρ)·... For |s−ρ| ≥ 1: |s/(ρ(s−ρ))| ≤ R/|ρ| — but sum over the annulus zeros of 1/|ρ|: Σ m/|ρ| ≍ Σ_{k∈(R/2,2R]} log k/k ≍ log R · (1/R)·(R log R)?? no: Σ_{|ρ|∈(R/2,2R]} m/|ρ| ≍ (2/R)·(count)/... ≍ (2/R)(R log R)/1 hmm = 2 log R? Let me redo: Σ_{R/2<|ρ|≤2R} m/|ρ| ≤ (2/R)·Σ_{|ρ|≤2R} m = (2/R)·N(2R)-ish ≍ (2/R)·(R log R/2π) ≍ (log R)/π·... hmm N(T) ≍ T log T/(2π): so ≍ (2/R)·(2R·log(2R)/(2π)) = 2 log(2R)/π = O(log R) ✓!! So Σ_{annulus} m·R/(|ρ|·|s−ρ|) ≤ R·(max 1/|s−ρ|)·Σ m/|ρ| — no wait: R/(|ρ||s−ρ|) with |s−ρ| ≥ 1: ≤ R/|ρ|: summed = R·O(log R)/... hold on: R·Σ_{annulus} m/|ρ| = R·O(log R)?? From above Σ_{annulus} m/|ρ| ≍ (1/(R/2))·(# zeros) — # zeros in the annulus ≍ R log R — so Σ m/|ρ| ≍ R log R/(R/2) = 2 log R — then R·Σ m/|ρ| — NO: the term bound is R/(|ρ||s−ρ|) ≤ R/|ρ|·1 (|s−ρ| ≥ 1) — so the SUM is ≤ R·Σ_{annulus} m/|ρ|·... NO: Σ (R/(|ρ||s−ρ|)) ≤ Σ R/|ρ| = R·Σ 1/|ρ| — wait that's R · Σ_{annulus} m/|ρ| = R · O(log R) = O(R log R). Hmm no!! Σ_{annulus} m/|ρ|: each term m/|ρ| ≤ m/(R/2) = 2m/R: sum = (2/R)·Σm = (2/R)·O(R log R) = O(log R). Then the total Σ terms ≤ R·... I keep confusing myself. TERM: |s/(ρ(s−ρ))| = R/(|ρ|·|s−ρ|) ≤ R/(|ρ|·1) = R/|ρ|. SUM: Σ_{annulus} R·m/|ρ| = R·Σ_{annulus} m/|ρ| = R·O(log R)·(1/R)?? — Σ_{annulus} m/|ρ|: with |ρ| ≍ R: m/|ρ| ≍ m/R: Σ ≍ (1/R)·Σm ≍ (1/R)·R log R = log R. So SUM of TERMS = R · (Σ m/|ρ|)?? NO — the term is R/(|ρ||s−ρ|), so the sum is Σ R·m/(|ρ||s−ρ|) ≤ Σ R·m/|ρ| = R·Σ m/|ρ| ≍ R·(log R)/R·... AAAARGH. Σ_{annulus} m/|ρ| where each |ρ| ∈ (R/2, 2R]: 1/|ρ| ≤ 2/R: Σ m/|ρ| ≤ (2/R)·Σ m = (2/R)·O(R log R) = O(log R). Then the term-sum Σ R·m/(|ρ||s−ρ|) ≤ R·Σ m/|ρ|·(1/1) = R·O(log R)/... = R · O(log R)?? NO: Σ R·m/|ρ| = R · Σ (m/|ρ|) = R · O(log R)/1?? The Σ m/|ρ| = O(log R) — then R times that = O(R log R)?? That's the same circular mistake. Let me be very careful:\n\nT_ρ := |1/(s−ρ) + 1/ρ| = |s|/(|ρ|·|s−ρ|) = R/(|ρ||s−ρ|).\nFor annulus zeros (|ρ| ∈ (R/2, 2R], |s−ρ| ≥ 1): T_ρ ≤ R/(|ρ|·1) ≤ R/(R/2) = 2.\nNumber of annulus zeros (mult-weighted): ≍ R log R.\nSum: ≤ 2 · R log R = O(R log R). — NOT o(R). CONFIRMED PROBLEM.\n\nSo D-067 §6's sketch \"the series on the circle is O((log R)²) by the dyadic split\" is WRONG as stated?? Or the classical argument differs. Let me think about what the classical argument actually is... \n\nThe classical Hadamard-free route to the partial fractions (e.g., via the \"F is a polynomial of degree ≤ 1\" argument): F entire with |F| = O(R^ε)... hmm. Actually — maybe the classical argument applies the circle bound to F(z)/(z) or uses the SMARTER combination: the series' s-DERIVATIVE: d/ds Σ m(1/(s−ρ)+1/ρ) = −Σ m/(s−ρ)²: |Σ_{annulus} m/(s−ρ)²| ≤ Σ m/|s−ρ|²: |s−ρ| ≥ 1 for annulus zeros: ≤ Σ m ≍ R log R — still big. Hmm.\n\nWait — actually I think the right classical statement: on the circle |s| = R (R in a γ-gap), |ζ′/ζ(s)| = O(log² R) and the PARTIAL SUMS Σ_{|γ|≤T} are handled at height T separately — the FULL-series-on-circle bound isn't the classical step. The classical step (Davenport Ch. 12, for the HADAMARD form): different argument entirely (Hadamard product exists ⟹ series). For the Hadamard-free route: maybe use the TRUNCATED identity: define F_T(s) = ζ′/ζ(s) − Σ_{|ρ|≤T} m(1/(s−ρ)+1/ρ) − elem(s) and bound F_T on |s| = R with T ≍ R... F_T has poles at the zeros |ρ| ≤ T inside — entire? no — F_T is meromorphic with poles at the un-subtracted zeros (|ρ| > T) AND removable at the subtracted ones. On the circle |s| = R < T: F_T is analytic on and inside the circle except at... poles at zeros with T < |ρ|: outside the circle ✓; at |ρ| ≤ T zeros: the subtraction kills them ✓; at 1, 0, −2n: the elem terms ✓. So F_T analytic on |s| ≤ R. Bound on the circle: |ζ′/ζ| ≤ C(log R)² (5c/5d + near-sum-via-gap); |Σ_{|ρ|≤T} m(1/(s−ρ)+1/ρ)|: same problem zeros... \n\nHmm hmm. Let me look at how the identity is ACTUALLY proved without Hadamard... Standard alternative: Mittag-Leffler for ζ′/ζ directly: ζ′/ζ is meromorphic with poles at zeros/pole with KNOWN principal parts; the series Σ [m/(s−ρ) + m/ρ·corrections] converges to a meromorphic function G; then ζ′/ζ − G is ENTIRE and one shows it's 0 (or a constant) by... the growth estimate on the difference on circles. The difference ENTIRE function: ζ′/ζ − G: on the circle |s| = R in the gap: |ζ′/ζ| = O((log R)²) ✓ and |G| = |Σ m(1/(s−ρ)+1/ρ)| = ??? — same estimation problem. UNLESS the gap condition is used for ALL annulus zeros: |s−ρ| ≥ c/log R not just for the near-crossing ones! Is that possible? |s−ρ| for ρ in the annulus (R/2, 2R]: s on the circle, ρ INSIDE-ish: |s−ρ| ≥ ||s|−|ρ|| = |R − |ρ|| — for |ρ| ∈ (R/2, R−2]: ≥ 2 ✓; for |ρ| ∈ [R−2, R+2]: |s−ρ| ≥ |t−γ| ≥ c/(2 log R) via the gap (these have γ ≈ R — within the pigeonhole window [R−2, R+2]-ish ✓). For |ρ| ∈ [R+2, 2R]: |s−ρ| ≥ |ρ| − R ≥ 2 ✓. So ALL annulus zeros have |s−ρ| ≥ min(2, c/(2 log R)) = c/(2 log R) for large R!! Then: T_ρ ≤ R/(|ρ|·c/(2logR)) = 2R log R/(c·|ρ|) ≤ 2R log R/(c·R/2) = (4 log R)/c ≍ (log R)². And there are ≍ R log R annulus zeros: sum ≍ R(log R)³ — WORSE. The count kills it. Ugh — no: the point is NOT to bound each term by the worst case; split the annulus finely: |s−ρ| ≥ |R − |ρ|| for |ρ| away from R: zeros with |ρ| ∈ [R−2, R+2] (count ≍ log R): each term ≤ 2R log R/(c·R/2) ≍ (log R)²/c — subtotal O((log R)³) ✓; zeros with |ρ| ∈ (R/2, R−2): |s−ρ| ≥ R−|ρ| ≥ 2... more finely |s−ρ| ≥ R − |ρ|: terms ≍ R/(|ρ|(R−|ρ|)) ≍ 2/(R−|ρ|): Σ ≍ Σ_{j=2}^{R/2} (count at |ρ| ≍ R−j)·(1/j) ≍ Σ_j (log R)·(1/j)·... count of zeros with |ρ| ∈ [R−j−1, R−j] ≍ log R·(1)·... hmm the ordinate count in a unit window ≍ C₀ ≍ log R: so Σ_{j=2}^{R/2} (log R)/j ≍ (log R)² ✓!! Similarly |ρ| ∈ [R+2, 2R]: |s−ρ| ≥ |ρ|−R: same O((log R)²). And |ρ| ≤ R/2: |s−ρ| ≥ R/2: terms ≍ R/(|ρ|R/2) = 2/|ρ|: Σ ≍ Σ m/|ρ| ≍ (log R)² ✓. And |ρ| > 2R: |s−ρ| ≥ |ρ|/2: terms ≍ R/|ρ|²·2: Σ ≍ R·Σ_{|ρ|>2R} m/|ρ|² ≍ R·(log R)/R = log R ✓. TOTAL: O((log R)³) — GOOD ENOUGH for o(R)!! The key was using |s−ρ| ≥ ||s|−|ρ|| for the bulk and the γ-gap only in the [R±2] critical annulus. \n\n   So D-067's \"dyadic split\" intuition is right but the correct splitting is by the RADIAL distance ||s|−|ρ|| (with the gap handling the critical annulus), giving O((log R)³) on the circle — fine for o(R). The design doc must record this corrected split (the §6 sketch's \"O((log R)²)\" was off but the conclusion o(R) survives with (log R)³).\n\n   Similarly |ζ′/ζ(s)| on the circle: 5c/5d give ‖ζ′/ζ − Σ_{near,|γ−t|<1} m/(s−ρ)‖ ≤ C(log|t|)²; the near sum: zeros with |γ−t| < 1 (count ≍ log R): each |s−ρ| ≥ |t−γ| ≥ c/(2log R) (the gap, since these γ are within [t±1] ⊂ the critical window as t ≈ R)... wait |t−γ| < 1 and t ≈ R ⟹ γ ∈ (R−2, R+2) ✓ gap applies: each term ≤ m·2logR/c: sum ≍ (log R)·2logR/c = O((log R)²) ✓. So |ζ′/ζ| = O((log R)²) on the circle ✓ (also need |t| ≥ 10 for 5c/5d; the |t| < 10 parts: near +R: Dirichlet series O(1) (re ≥ R−δ... for |t| < 10 and |s| = R: re s = ±√(R²−t²) ≈ ±R: right point: re s ≥ R−1 > 7/2 for R > 10: NOT covered by 5c (re ≤ 7/2)! Use the Dirichlet-series bound |ζ′/ζ(s)| ≤ Σ Λ(n)/n^{re s} ≤ C for re s ≥ 2 (LSeries vonMangoldt + comparison with Σ Λ(n)/n² — Zeta23 has the LSeries machinery; the bound Σ Λ(n)/n² converges: via LSeries.absSummable? — pin at build). Left point: re s ≈ −R: FE-reflect: ζ′/ζ(s) = −ζ′/ζ(1−s) − bracket: 1−s has re ≈ 1+R: Dirichlet O(1); bracket: logDeriv ΓR(1−s) = O(log R) (digamma_stirling: re(1−s) > 0, |im(1−s)/2| = |t|/2 < 5 — hmm |im| ≥ 1/2 needed: for |t| < 1: ψ((1−s)/2) with re ≈ R/2 large, |im| < 1/2: the digamma bound via... the same near-axis issue. ψ(w) for re w ≥ 2 large, |im w| ≤ 5: digamma_stirling needs |im| ≥ 1/2. For |im w| < 1/2, re w ≥ 2: ψ is... not on a compact set (re → ∞). Bound: ψ(w) − log w → 0 as re w → ∞ uniformly in |im| ≤ 1/2? Via the series: ψ(w) + γ + 1/w = Σ_n w/((n+1)(w+n+1)): |Σ| ≤ |w|·Σ 1/((n+1)(re w+n+1)) (since |w+n+1| ≥ re w+n+1 ≥ ...): ≤ |w|·Σ 1/((n+1)(re w + n + 1)): the sum Σ_n 1/((n+1)(A+n+1)) with A = re w ≥ 2: ≤ Σ_n 1/(n+1)² · ... ≤ π²/6·... hmm: 1/((n+1)(A+n+1)) ≤ 1/(n+1)²: sum ≤ π²/6 ✓ O(1): so |ψ(w)+γ+1/w| ≤ |w|·π²/6?? that's O(R) — too big. Better: Σ 1/((n+1)(A+n+1)): split n+1 ≤ A: 1/((n+1)·A): sum ≍ (log A)/A; n+1 > A: 1/(n+1)²-ish: sum ≍ 1/A: total ≍ (log A)/A ⟹ |Σ| ≤ |w|·(log A)/A ≍ log R ✓ (|w|/A ≍ 1). So ψ(w) = O(log R) for re w ≥ 2, |im w| ≤ 5 — via the series split — elementary. And for logDeriv ΓR(s) with re s ≈ −R (the near-axis left case): w = s/2, re w ≈ −R/2, |im w| ≤ 5: the NEAR-AXIS LEFT-PLANE bound (the recurrence + separated reciprocal sum + compact/StirlingVert at the shifted point) ⟹ O(log R). So the near-axis digamma bound needs: re w arbitrary negative, |im w| ≤ 5, dist(w, −ℕ) ≥ 1/4: ψ(w) = ψ(w+m) − Σ_{j<m} 1/(w+j): (i) Σ_{j<m} 1/|w+j| ≤ C log(m+1) via 1-separation + |w+j| ≥ 1/4 (elementary bin-packing: at most 2 per unit interval... with |im w| ≤ 5 the \"1-separation\" of |w+j|... |w+j| for real parts spread 1 apart: the values |w+j| ≥ max(|re(w+j)| − 0, |im w|)... hmm: |w+j|² = (re w+j)² + (im w)²: with |im w| ≤ 5 and re(w+j) 1-separated: |w+j| ≥ |re(w+j)|: the re values hit near-zero for one/two j's: there |w+j| ≥ dist(w,−ℕ) ≥ 1/4 ✓; other j: |re(w+j)| ≥ 1/2, 3/2, ...: Σ_j 1/|w+j| ≤ 2·(4 + 2/3 + 2/5 + ...) ≍ 2·(4 + 2·H_m) = O(log m) ✓. (ii) ψ(w+m) with re(w+m) ∈ [1,2]: |im| ≤ 5: digamma_stirling if |im| ≥ 1/2: O(log) ✓; if |im| < 1/2: ψ on the compact {re ∈ [1,2], |im| ≤ 1/2} — continuous ⟹ bounded by a constant C₀ — but wait — is that a Lean-available fact? Continuous on a compact ⟹ bounded: `IsCompact.exists_bound_of_continuousOn`? or `IsCompact.exists_forall_le` (norm version): `IsCompact.exists_forall_ge`? There are Mathlib lemmas: IsCompact.exists_sSup_image.../Bounded: `IsCompact.bddAbove_image`? For norms: `IsCompact.exists_bound_of_continuousOn`? I'll find one. So the near-axis digamma bound: ‖ψ(w)‖ ≤ C·log(2+‖w‖) for dist(w, −ℕ) ≥ 1/4 — that's 5e sub-build (ii). NOTE: this SUBSUMES the usage I planned for 5d's bound in the near-axis region; 5d's |im|≥2 bound covers the complementary case. Both feed 5e.)\n\n6. Then F constant: |F(s)| on the circle ≤ |ζ′/ζ| + |series| + |elem| = O((log R)²) + O((log R)³) + O(log R) = O((log R)³) ⟹ o(R) ⟹ F ≡ const c₀; then B := c₀ − (0-eval adjustments)... The final identity with the constant: ζ′/ζ(s) = B + Σ − 1/s − 1/(s−1) + ½logπ − ½ψ(s/2) — with B := F's constant value (whatever falls out; for 5f only the DIFFERENCE structure matters, B cancels). Hmm — actually for the THEOREM statement we need the exact identity with a named constant or an existential: \"∃ B : ℂ, ∀ s (not a zero/pole), ζ′/ζ s = ...\". The tight analysis (5f) needs B explicitly? D-056's analysis: the reference-point trick: R(s) = R(s₀) + [identity(s) − identity(s₀)] — B cancels in the difference ✓. So the existential-B form suffices. \n\n7. 5f preview (for completeness of the map): D-056's six pieces: the near sum ≤ C₀(t); the far difference ≤ 12.73C₀ + 7.06 via Σ 1/(k(k+1)) = 1; Z₂ ≤ 0.65; the ψ-difference via digamma_stirling ⟹ |R| ≤ 13.73 C₀(t) + 7.97 ≤ 10.5 log(|t|+2) + 48. This needs the perimeter ZeroCountProp (C₀) — first use of the perimeter in the R-bound chain! (5c avoided it via Jensen; 5f's tight constants need C₀.) Fine — the perimeter is declared.\n\nSo the 5e sub-builds:\n- 5e-0: ✔ zeroMult(−2n) = 1 (session 026, DONE).\n- 5e-i: the ×2-rescaled midpoint pigeonhole: T ∈ [4k+2.5, 4k+3] with γ-clearance ≍ 1/log k against ALL zeros (from exists_avoiding_midpoint + ZeroCountProp on two unit windows) ⟹ radius R_k with both the ordinate-gap and dist(R_k/2, ℤ) ≥ 1/4... wait R_k = T directly: the circle radius is T ∈ [4k+2.5, 4k+3]: R/2 ∈ [2k+1.25, 2k+1.5]: dist(R/2, ℤ) ≥ min(0.25, 0.5) = 1/4 ✓. \n- 5e-ii: the near-axis digamma bound: ‖ψ(w)‖ ≤ C log(2+‖w‖) + C for dist(w, −ℕ) ≥ 1/4 (recurrence + separated reciprocal sum + compactness/StirlingVert at the shift). ALSO the right-half mild version: ψ(w) = O(log‖w‖) for re w ≥ 2 (any im) — hmm actually that's for the logDeriv ΓR(1−s) at the right circle point... re(1−s) ≈ 1+R: ψ((1−s)/2): re ≈ (1+R)/2 ≥ 2 ✓ |im| < 5: covered by the series-split bound (sub-case of 5e-ii or direct).\n- 5e-iii: the series machinery: Summable (fun ρ ↦ m_ρ(1/(s−ρ)+1/ρ)) for s ∉ zeros (via the 2‖s‖-split + mult-weighted zero_sum_inv_sq + finite balls); locally-uniform convergence on compacts avoiding zeros ⟹ analytic (Weierstrass: TendstoLocallyUniformlyOn → analytic); the series-on-circle O((log R)³) bound (the radial split + gap).\n- 5e-iv: F entire: at each nontrivial zero ρ: split the ρ-term out of the series (Summable.diff / the finite-ball split contains ρ: the series minus the ρ-term is analytic at ρ: locally-uniform machinery on a small ball containing only ρ — need zero isolation: ball around ρ containing no other zero — discreteness: from isCompact...zeros_finite + the zero set closed: get δ > 0 with no other zero in ball(ρ, δ): standard from discreteness); ζ′/ζ − m/(s−ρ) analytic at ρ (ii′-1b logDeriv-NF); the rest analytic at ρ. Similarly at 1 (residue −1 both sides — ζ′/ζ + 1/(s−1) analytic at 1: from the ζ pole structure — Mathlib has riemannZeta_residue_one? There's `riemannZeta_residue`... Zeta23 surely has ζ′/ζ + 1/(s−1) analytic at 1 — used in PNT stuff: StrongPNTPrefix? \"riemannZeta_residue_one\"? check); at 0 (−1/s vs −½ψ(s/2): ψ(s/2) = −2/s + O(1): ψ near 0: ψ(w)+1/w analytic at 0 — from the digamma series (ψ(w) = −γ −1/w + Σ(...): Σ analytic at 0 (each term 1/(n+1)−1/(w+n+1) analytic and the sum converges uniformly near 0 — locally uniform machinery again) ⟹ −½ψ(s/2) = −½(−2/s + h(s)) = 1/s − h(s)/2 with h analytic at 0 ⟹ −1/s − ½ψ(s/2) analytic at 0 hmm: −1/s + 1/s − h(s)/2 ✓ analytic); at −2n (zeroMult = 1 ⟹ ζ′/ζ − 1/(s+2n) analytic at −2n [ii′-1b logDeriv-NF + session-026's zeroMult_neg_two_mul]; −½ψ(s/2) − 1/(s+2n) analytic at −2n [ψ(s/2) + 2/(s+2n): ψ(w) + 1/(w+n) analytic at w = −n via the series: the n-th term's singular part... ψ(w) = −γ −1/w + Σ_j(1/(j+1) − 1/(w+j+1)): at w = −n: the term j = n−1: −1/(w+n) is the pole; the rest analytic — split it out: ψ(w) = [−γ − 1/w + Σ_{j≠n−1}(...)] − 1/(w+n): the bracket analytic at −n (locally uniform conv away from the single excluded pole — hmm the uniform convergence near −n of the series MINUS one term: fine (same machinery with the tail from n+1 + the finite head); so −½ψ(s/2) − 1/(s+2n): ψ(s/2) = h(s) − 1/(s/2+n) = h(s) − 2/(s+2n): −½ψ(s/2) = −h(s)/2 + 1/(s+2n) ⟹ −½ψ − 1/(s+2n)... wait sign: −½ψ(s/2) = −½h(s) + 1/(s+2n): the +1/(s+2n) term: and the ζ side has −1/(s+2n)... let me redo: F = ζ′/ζ − Σ − [−1/s − 1/(s−1) + ½logπ − ½ψ(s/2)]: at −2n: ζ′/ζ has residue +1 (simple zero); the bracket has −½ψ(s/2) with residue −½·(−2) = +1 hmm wait: −½ψ(s/2): ψ(s/2) near s=−2n: ψ(s/2) = −1/(s/2+n) + h(s) = −2/(s+2n) + h(s): −½ψ(s/2) = +1/(s+2n) − h(s)/2: so the bracket's residue at −2n is +1; F = ζ′/ζ − Σ − bracket: residue: +1 − 0 − (+1) = 0 ✓ removable. The analyticity: ζ′/ζ − 1/(s+2n) analytic at −2n; bracket − 1/(s+2n) = −1/s − 1/(s−1) + ½logπ − ½ψ(s/2) − 1/(s+2n) = [−1/s − 1/(s−1) + ½logπ − h(s)/2·...]: with −½ψ(s/2) − 1/(s+2n) = −½h(s) analytic ✓ so F = [ζ′/ζ − 1/(s+2n)] − Σ − [bracket − 1/(s+2n)]... wait the bracket −1/(s+2n) requires s ≠ −2n form; the identity manipulation: F(s) = [ζ′/ζ(s) − 1/(s+2n)] − Σ(s) − [elem(s) − 1/(s+2n)] where elem(s) − 1/(s+2n) is analytic at −2n ✓ — all three pieces analytic at −2n ⟹ F analytic at −2n ✓.\n- 5e-v: F constant: the difference-quotient analyticity (inventory question), Liouville (Mathlib), max-modulus on discs (Zeta23 has it), the (log R)³/R → 0 limit.\n- 5e-vi: the Dirichlet-series bound |ζ′/ζ| = O(1) for re s ≥ 2 (LSeries vonMangoldt — for the circle's right near-axis part).\n\nEstimated total: ~2 sessions (matches D-067's ~1 sess estimate for 5e being optimistic; the survey revealed the extra near-axis digamma sub-build + the corrected (log R)³ split).\n\nAlso — the F-entirety at ALL points needs covering: ℂ = strip-zeros ∪ {0,1} ∪ {−2n} ∪ {everything else}: at \"everything else\" points (s not a zero, not 0/1/−2n): ζ′/ζ analytic (ζ ≠ 0 there, differentiable), the series analytic (locally uniform), elem analytic (ψ(s/2) analytic off the poles: s/2 ∉ −ℕ: s ∉ {0,−2,−4,...} ✓ excluded; 1/s at s ≠ 0 ✓; 1/(s−1) at s ≠ 1 ✓). ✓.\n\nOne more inventory question: does Zeta23 have \"ζ′/ζ(s) + 1/(s−1) analytic at 1\"? StrongPNTPrefix surely has the Laurent/pole machinery (the residue at 1 is used in PNT): look for `riemannZeta_residue` or logDeriv analyticity at 1. The ii′-1b LiResidue.lean built \"zetaA = (w−1)ζ analytic at 1 via removable singularity; hLi analytic\" — so (s−1)ζ(s) analytic at 1 with value 1: ζ′/ζ + 1/(s−1) = (logDeriv of (s−1)ζ(s))... logDeriv ζ + 1/(s−1) = logDeriv((s−1)ζ)?? logDeriv((s−1)ζ) = 1/(s−1) + ζ′/ζ ✓ — and (s−1)ζ(s) is analytic NONZERO at 1 (value 1) ⟹ its logDeriv is analytic at 1 (deriv/analytic with nonvanishing) ✓✓ — so \"ζ′/ζ + 1/(s−1) analytic at 1\" = logDeriv of zetaA — one line from ii′-1b's zetaA analyticity + AnalyticAt.logDeriv? hmm — logDeriv f = deriv f / f: analytic at 1 if f analytic and f(1) ≠ 0: AnalyticAt.div (deriv analytic — `AnalyticAt.deriv` exists) ✓.\n\nGood. Now — also the identity's EXACT constant-form: for the theorem statement: ∃ B : ℂ, ∀ s ∈ ℂ ∖ (zeros ∪ {0,1} ∪ −2ℕ·...): ζ′/ζ s = B + Σ − 1/s − 1/(s−1) + ½logπ − ½ψ(s/2). Fine.\n\nTime to write D-068 with all of this. It's a design doc — markdown in research/derivations/. Also update the derivations index.md? Let me check the convention — D-067 was registered via db.py add-derivation + index.md entry. Let me look at the index entry format quickly, then write D-068 and register.","signature":""},{"type":"text","text":"Build green and audit clean. Now the ii′-5e design doc — the survey surfaced two corrections to D-067's sketch that the design must record. Let me check the derivations index format, then write D-068."},{"type":"tool_use","id":"Bash_203","name":"Bash","input":{"command":"tail -12 /d/Python/Quantum/research/derivations/index.md && cd /d/Python/Quantum && ./.venv/Scripts/python.exe research/numerics/scripts/db.py add-derivation --help 2>/dev/null | head -20","description":"Check derivations index format and db.py signature"},"extra_content":null}]