[{"type":"thinking","thinking":"Session 023: ii′-5c — the Davenport disc argument. Let me plan carefully.\n\nThe goal (D-067 §3): the R-bound on σ ∈ [1/2, 7/2], |t| ≥ 10:\n  R(s) := logDeriv ζ s − Σ_{|γ−t|<1} mult(ρ)/(s−ρ), bounded by A log|t| + B form.\n\nThe Davenport argument on B(2+it, 5/2):\n1. Collect zeros ρₖ in B(s₀, 2.3) with s₀ = 2+it (this includes all |γ−t|<1 zeros).\n2. g(s) := ζ(s)/∏ₖ(s−ρₖ)^{mₖ} — analytic and nonvanishing on the disc.\n3. Bound |g| on the outer circle: |g| ≤ |ζ|/∏|s−ρₖ|^{mₖ} ≤ (3/4)|t|²/(0.2)^m.\n4. Center lower bound |g(s₀)| ≥ (1/ζ(2))/∏|s₀−ρₖ|^{mₖ} ≥ 0.6/(2.3)^m.\n5. LogOfAnalyticFunction: J_g with Re J_g = log|g| − log|g(s₀)|, J_g(s₀) = 0, deriv J_g = g′/g.\n6. Re J_g ≤ log|g| + C′ log|t| ≤ A′ log|t| + B′ on the disc.\n7. BorelCaratheodoryDeriv: ‖deriv J_g‖ ≤ 16 M R²/(R−r)³ on B(s₀, r).\n8. g′/g = ζ′/ζ − Σₖ mₖ/(s−ρₖ) (logDeriv quotient/product rules).\n9. R(s) = ζ′/ζ − Σ_{|γ−t|<1} = (log g)′ + Σ_{collected, |γ−t|≥1} mₖ/(s−ρₖ); extras each ≤ mₖ·1 (im gap).\n\nThe StrongPNTPrefix lemmas are all stated for functions on discs CENTERED AT 0 with the normalization R < 1 etc. — so I apply them to a translated function. Let me check the exact signatures I'll use:\n\n- `LogOfAnalyticFunction {r R : ℝ} {B : ℂ → ℂ} (zero_lt_r : 0 < r) (r_lt_R : r < R) (BanalyticOnNhdOfDR : AnalyticOnNhd ℂ B (Metric.closedBall (0 : ℂ) R)) (Bnonzero : ∀ z ∈ Metric.closedBall (0 : ℂ) R, B z ≠ 0) : ∃ (J_B : ℂ → ℂ), AnalyticOnNhd ℂ J_B (ball 0 R) ∧ J_B 0 = 0 ∧ (∀ z ∈ closedBall 0 r, deriv J_B z = deriv B z / B z) ∧ (∀ z ∈ ball 0 R, Real.log ‖B z‖ − Real.log ‖B 0‖ = (J_B z).re)`\n\n- `BorelCaratheodoryDeriv {M r R : ℝ} {f : ℂ → ℂ} {z : ℂ} (Mpos : 0 < M) (rpos : 0 < r) (hyp_r : r < R) (analytic_f : AnalyticOn ℂ f (ball 0 R)) (zeroAtZero : f 0 = 0) (realPartBounded : ∀ z ∈ ball 0 R, (f z).re ≤ M) (hyp_z : z ∈ closedBall 0 r) : ‖deriv f z‖ ≤ 16 * M * R^2 / (R - r)^3`\n\nBoth are centered at 0. So define w := s − s₀ translation: B(w) := g(s₀ + w). Then:\n- B analytic on closedBall(0, R) ⟸ g analytic on closedBall(s₀, R).\n- B nonvanishing ⟸ g nonvanishing.\n- deriv J_B w = g′(s₀+w)/g(s₀+w) on closedBall(0, r).\n- (J_B w).re = log‖g(s₀+w)‖ − log‖g(s₀)‖.\n- BorelCaratheodoryDeriv with f := J_B (which has J_B 0 = 0 ✓).\n\nThe R-bound then at s = s₀ + w with |w| ≤ 3/2 (covering σ ∈ [1/2, 7/2]).\n\nKey sub-builds:\n(a) **The zero collection finset + g's definition + analyticity/nonvanishing.** The zeros of ζ in B(s₀, 2.3): nontrivial zeros plus possibly... wait — the disc B(2+it, 2.3) with |t| ≥ 10: contains only NONTRIVIAL zeros (re ∈ (−0.3, 4.3) — trivial zeros at −2, −4...: −2 has re −2 < −0.3 ✓ excluded; and re > 1 points: no zeros of ζ for re ≥ 1 (well re > 1: Euler product nonzero ✓; re = 1: no zeros on re = 1 (PNT — but that IS the nontrivial-zero class... IsNontrivialZero requires 0 < re < 1). Zeros of ζ in the disc: {ζ = 0} ∩ disc — all have re < 1 except... ζ zeros at re ∈ (0,1) nontrivial; zeros at re ≤ 0: trivial −2n: in the disc? re ≥ −0.3 > −2 ✓ none; re ≥ 1: ζ ≠ 0 for re ≥ 1?? re > 1: Euler product ✓ nonzero; re = 1: ζ(1+it) ≠ 0 for t ≠ 0 — that's the PNT input! Hmm — is that available? Zeta23 is a PNT repo — `riemannZeta_ne_zero_of_re_eq_one`? There's `riemannZeta_ne_zero_of_one_le_re`? For re = 1, t ≠ 0: nonzero (de la Vallée Poussin) — Mathlib has `riemannZeta_ne_zero_of_one_le_re`?? Hmm — actually for the R-bound's purpose I don't need to CLASSIFY the zeros in the disc — I just collect whatever zeros are there with their orders. The sum Σ over collected zeros with |γ−t| ≥ 1 get bounded by the im-gap (|s−ρ| ≥ |t−γ| ≥ 1). The point: the collection = {ρ ∈ disc : ζ ρ = 0} = nontrivial zeros in the disc (since the disc avoids trivial zeros and the pole at 1). Fine — I can work with the set {ρ ∈ B(s₀, 2.3) : riemannZeta ρ = 0} directly, no classification needed.\n\nFiniteness: from Zeta23's zerosIn_finite (needs IsNontrivialZero form) or the compactness: {ζ = 0} ∩ closed disc — `IsCompact.inter_riemannZetaZeros_finite`? ii′-1a used `IsCompact.inter_riemannZetaZeros_finite` per NGUYEN.md. Let me check its exact form — probably: (hs : IsCompact s) → (s ∩ {z | riemannZeta z = 0}).Finite or similar.\n\n(b) **g := ζ/∏(s−ρₖ)^{mₖ} analytic + nonvanishing on the disc.** The removal: ζ(s) = ∏(s−ρₖ)^{mₖ}·h(s) with h analytic nonvanishing... The cleanest via ZeroFactorization (StrongPNTPrefix:214): let me read its statement. It probably says: f analytic on closedBall, f(0) ≠ 0 → f = ∏(z−ρ)^{ord}·g with g analytic nonzero. Actually for g's definition I don't need it in factored form — define g(s) := ζ(s) / ∏ₖ(s−ρₖ)^{mₖ} directly; analyticity at each ρₖ via the order matching (analyticOrderNatAt), nonvanishing by construction. The quotient ζ/∏ is analytic OFF the zeros (clear) and AT each ρₖ the singularity is removable (order of ζ at ρₖ = mₖ = order of the denominator) — the extension needs: ζ(s)/∏(s−ρₖ)^{mₖ} has a removable singularity at each ρₖ — via `AnalyticAt... meromorphic... ` hmm. The cleanest formal path: use ZeroFactorization to WRITE ζ as product·nonvanishing, then g IS that nonvanishing factor. Let me read ZeroFactorization.\n\n(c) **The bounds chain**: |g| on outer circle, |g(s₀)| below, log bounds, BC.\n\n(d) **g′/g = ζ′/ζ − Σ mₖ/(s−ρₖ)**: logDeriv of quotient of products: logDeriv (ζ/∏) = logDeriv ζ − logDeriv ∏ = ζ′/ζ − Σ logDeriv (s−ρₖ)^{mₖ} = ζ′/ζ − Σ mₖ/(s−ρₖ). Mathlib: `logDeriv_div`, `logDeriv_prod`, `logDeriv_pow`?, `logDeriv_sub`? — need: logDeriv (fun s => (s−ρ)^m) = m/(s−ρ): logDeriv_pow: logDeriv (f^m) = m·f′/f = m·f^(m−1)/f^m = m/f for f = s−ρ (f′ = 1): logDeriv_pow (f^m) = m * (logDeriv f)? There should be `logDeriv_pow (hf) : logDeriv (f ^ n) = n * logDeriv f`? or logDeriv_pow : logDeriv (x^n) = n/x·... Let me check at build. logDeriv_prod: logDeriv (∏ i∈s, f i) = Σ logDeriv (f i) (needs each fi ≠ 0 at the point / differentiableAt). logDeriv_div: logDeriv (f/g) = logDeriv f − logDeriv g (g z ≠ 0, differentiable).\n\n(e) **The near-zero sum matching**: R(s)'s sum is over |γ−t|<1 zeros; g's collection is |ρ−s₀| ≤ 2.3 zeros. The extras: collected but |γ−t| ≥ 1: each term mₖ/(s−ρ): |s−ρ| ≥ |Im(s−ρ)| = |t−γ| ≥ 1 ⟹ each |term| ≤ mₖ. Number of extras ≤ total collected count. So the extras bound = Σ mₖ over extras ≤ total mult-count ≤ C·log t.\n\nWait — hmm, actually there's a subtlety: the zeros with |γ−t| < 1 might not ALL be in the collection if |ρ−s₀| > 2.3? |ρ−s₀|² = (2−β)²+(t−γ)² ≤ 4+1 = 5 < 2.3² = 5.29 ✓ all included ✓.\n\nAnd the collection might include zeros with |γ−t| ∈ [1, 2.3] — the extras ✓ bounded.\n\n(f) **Zero count with multiplicity**: Σ_{collected} mₖ ≤ ? Via the perimeter ZeroCountProp (counts distinct zeros in unit windows) + a per-zero multiplicity bound mₖ ≤ ...? Hmm — mult vs distinct: ZeroCountProp bounds the COUNT of distinct zeros (Nat.card of the subtype). The mult-weighted count: mₖ = analyticOrderNatAt ζ ρₖ. Bound mult ≤ count-with-multiplicity... circular. Options: (i) bound each mₖ by an absolute log bound via Jensen (ZerosBound gives exactly Σ mult ≤ log B / log(R/r) — the Jensen count INCLUDES multiplicities!). Actually — the cleanest: use ZerosBound (Jensen) for the mult-weighted count directly: Σ mₖ ≤ log(sup|f|)/log(R/r)-form. With the |ζ| bound (3/4)|t|² and the center lower bound: Σ_{|ρ−s₀|≤2.3} mₖ ≤ [log((3/4)|t|²·(clearance stuff)) + |log|ζ(s₀)||]/log(R/r_c)... Hmm — ZerosBound's form: ∑ ρ ∈ toFinset, analyticOrderNatAt f ρ ≤ 1/log(R/r) · log B — with f normalized f(0) = 1 — normalize by dividing by f(0)... The Jensen count bound: #zeros in B(0, r) (with mult) ≤ log(M/|f(0)|)/log(R/r) where M = max on |z| = R. With our data: M = (3/4)|t|²/(0.2)^m hmm — the circularity: M for ζ (not g): sup|ζ| on B(s₀, 5/2) ≤ (3/4)|t|² ✓ (ii′-5b); |ζ(s₀)| ≥ 1/ζ(2) ≈ 0.6. So Σ mₖ ≤ log((3/4)|t|²·ζ(2))/log(2.5/2.3) = [log(3/4) + 2log|t| + log ζ(2)]/log(25/23) ≈ (2 log|t| + 0.18)/0.083 ≈ 24 log|t| + 2.2. Fine — A′-sized. But wait — the (0.2)^m factor in |g|: m = Σ mₖ ≤ 24 log|t| + 2.2: (0.2)^m = 5^{−m} = |t|^{−24 log 5}·... — hmm — that's |g| ≤ (3/4)|t|²·5^m ≤ (3/4)|t|²·|t|^{24 log 5} = |t|^{2+38.6} — log|g| ≤ 41 log|t| — fine for the A′ log|t| + B′ shape (constants get big but that's OK — the fold to A = 10.5 needs care... hmm actually WAIT. This is a concern: the final R-bound constants from this route will be MUCH bigger than D-056's A = 10.5, B₀ = 48. D-056 got 10.5 via the tight partial-fraction route. My Davenport route gives A ~ 100·(2 + mult-count log factors...) — could be A ~ 2000+. Does that matter for ii′-6? The assembly: |Sf n| ≤ Bn FAlt n — the Bn FAlt form already encodes A = 10.5, B₀ = 48 via Hhat etc. (LiSkeleton's marginTilde uses Hhat with 10.5/48 hardcoded!). Hmm — marginTilde FAlt n = S(n) − (2F(T) + 4T((2/3)C0hat T + 10.5·log(T+2) + 48) + ...) — the 10.5 and 48 are BAKED INTO LiSkeleton's marginTilde and the proved marginTilde_convex and the certified base points! So the Lean R-bound must match A = 10.5, B₀ = 48 (or better). My Davenport route with its loose constants would need A ~ hundreds — BREAKING the baked-in constants!!\n\nHold on. Let me reconsider. Options:\n1. Tighten the Davenport route's constants to fit 10.5/48 — the constant analysis: the derivative factor 16R²/(R−r)³ with R = 5/2, r = 3/2: 16·6.25/1 = 100. M = A′log|t| + B′ with A′ ~ from the |g| log bound: log|g| ≤ 2log|t| + m·log(1/0.2) + log(3/4): m·log 5 with m ≤ 24 log|t|... — the m ≤ 24 log|t| via Jensen is LOOSE (the honest count is C₀(t) ≈ 0.433 log t — Jensen on the tiny circle ratio loses a log-factor). The tight count comes from the perimeter ZeroCountProp: #distinct ≤ C0hat·... and mult = 1 for all but... mult > 1 needs multiple zeros — a priori mult could be large at a single point. Hmm — mult at a zero ≤ count-with-mult ≤ Jensen. The mult-weighted count ≤ 24 log|t| is what breaks the constants (24 vs 0.433 — a 55× loss, ×100 from BC = 5500× the log coefficient... A ≈ 0.433·100·(small factors) ~ 50–200 would be FINE if the count is C0hat-tight; the Jensen count 24 log|t| is 55× too big).\n\nSo: to hit A = 10.5 I need the TIGHT zero count from the perimeter (Trudgian C0hat), not Jensen. The mult-weighted count Σ mₖ over the window: relate to distinct count + multiplicity excess. Hmm — actually: is there a cheap a priori bound mₖ ≤ C·log|t| per zero? That doesn't help: Σ mₖ ≤ max-mult × #distinct ≤ (C′ log t)(C₀ log t) — quadratic — too big.\n\nAlternative: ZerosBound/Jensen with a BETTER radius ratio? log(R/r) with R/r = 2.5/2.3 = 1.087: log = 0.083. Push the ratio: R = 5/2 fixed by the disc; r_c = 2.3: the Jensen count is over zeros in B(s₀, r_c) with R = 5/2 — ratio fixed by geometry. The Jensen constant 1/log(25/23) ≈ 12 is the loose factor vs Trudgian's 0.433·(window count).\n\nHmm wait — actually, hold on: is the 24 log|t| mult-count really needed, or can the Trudgian unit-window count handle multiplicities? The sum Σ_{|γ−t|<1} mₖ/(s−ρ) in R(s) — the mult-weighted sum. The near-zero sum at s₀: Σ mₖ/|s₀−ρ|: |s₀−ρ| ≥ 2−β ≥ 1 ⟹ ≤ Σ mₖ. For the Davenport g: log|g| = log|ζ| + Σ mₖ log(1/|s−ρₖ|) — the mult-weighted count is what enters. So I need Σ_{|ρ−s₀|≤2.3} mₖ ≤ C log|t| with C honest.\n\nClaim: Σ_{window} mₖ ≤ (count with multiplicity). Is there a Trudgian-style mult-weighted count? The N(T) count itself counts with multiplicity! Trudgian's N(T) = #{zeros 0<γ≤T with multiplicity}. So the unit-window count with multiplicity ≤ C0hat form is EXACTLY the perimeter's content (D-056's C₀(t) := F(t+1)−F(t)+S_b(t+1)+S_b(t) — the N(T) difference IS mult-weighted). So the perimeter Prop should be mult-weighted!! My ii′-4 ZeroCountProp used Nat.card of the DISTINCT-zero subtype — NOT mult-weighted. Hmm. For the R-bound I need the mult-weighted version:\n\nZeroCountPropMult: ∀ t ≥ 2, Σ_{ρ ∈ window} zeroMult ρ ≤ C0hat(t+1)? — as the honest perimeter form (Trudgian N(t+1)−N(t) + S_b slacks count multiplicities).\n\nHmm — but wait: is the Trudgian N(T) count with multiplicity or distinct? N(T) = #{ρ : 0 < γ ≤ T} counting multiplicity — YES standard (Riemann–von Mangoldt counts with multiplicity). So the perimeter should be mult-weighted. My ii′-4 ZeroCountProp (distinct) is actually the WEAKER statement (distinct ≤ mult-weighted). For the L3 pigeonhole, distinct-count is what's needed (gaps between distinct ordinates). For ii′-5c, need mult-weighted. Both follow from Trudgian N(T)/S(T). So: ii′-5c should ADD the mult-weighted perimeter Prop `ZeroCountMultProp` and use it. The extra zeroMult(−2)... no wait — trivial zeros aren't in these windows (γ ≥ 14 > 0, windows at t ≥ 2 hmm — window [t, t+1] with t ≥ 2: contains only nontrivial zeros (trivial zeros are real negative — im = 0 ∉ [t, t+1]) ✓.\n\nHmm — but actually, wait. Let me reconsider whether I even need the mult-weighted count, or whether the constants can be repaired differently. The Davenport log|g| bound: log|g(s)| for s on the outer circle: log|ζ(s)| + Σ mₖ log(1/|s−ρₖ|) ≤ 2log|t| + log(3/4) + Σ mₖ·log(1/0.2) = 2log|t| + log(3/4) + (log 5)·Σ mₖ. With Σ mₖ ≤ C0hat-mult(t+3)-ish ≈ 0.433 log t + ... : log|g| ≤ 2 log|t| + (log 5)(0.433 log|t| + 0.886 loglog|t| + 2.9) + ... ≈ (2 + 0.7)log|t| + 1.43 loglog + ... Then Re J_g ≤ that + |log|g(s₀)|| ≤ ... + log(ζ(2)/0.6...) + m log 2.3-ish ≈ ... So M ≈ 2.7 log|t| + 1.43 loglog|t| + const. Then BC: |(log g)′| ≤ 100M ≈ 270 log|t| + ... — A ≈ 270?!? That's WAY over 10.5!!\n\nHold on — the BC factor 16R²/(R−r)³ = 100 is brutal. D-056's A = 10.5 comes from the tight partial-fraction analysis. The Davenport route with these radii gives A ~ 270 — that does NOT fit the baked-in marginTilde constants!!\n\nHmm wait — let me recompute. 16R²/(R−r)³ with R = 5/2, r = 3/2: 16·(25/4)/(1)³ = 100. M ≈ 2.7 log|t| + ... ⟹ derivative ≤ 270 log|t|. A = 270 >> 10.5. PROBLEM.\n\nCan the geometry be improved? The 16R²/(R−r)³ factor: minimize over R, r with r_c = √5 (collection) < r... wait constraints: r_c = √5 ≈ 2.236 must be < R (zeros inside); application region needs r ≥ 3/2 (cover σ ∈ [1/2, 7/2]... hmm actually the application region for the R-bound is σ ∈ [1/2, 3] and the reflection needs [1/2, 7/2]: |s−s₀| ≤ 3/2). The BC derivative at r with the bound on R: factor 16R²/(R−r)³. With r = 3/2 fixed, minimize over R > √5: f(R) = R²/(R−1.5)³: f'(R) = [2R(R−1.5)³ − 3R²(R−1.5)²]/(R−1.5)⁶ = R(R−1.5)²[2(R−1.5) − 3R]/(R−1.5)⁶ = R(−R−3)/(R−1.5)⁴ < 0 — DECREASING in R! So bigger R is better for the factor — but bigger R dips further left (σ < −1/2) needing more EM levels, and the |ζ| bound grows like |t|^{level}. Trade: R = 3 (dips to −1, B₃-level needed): factor 16·9/(1.5)³ = 144/3.375 = 42.7. R = 7/2 (dips to −3/2, B₃ hmm B₂ covers σ > −1 only — B₃ rep σ > −2): 16·12.25/8 = 24.5. R = 4 (dips to −2, B₄): 16·16/(2.5)³ = 256/15.6 = 16.4. R = 5 (dips −3, B₅): 16·25/42.9 = 9.3. R = 6 (dips −4, B₆): 16·36/91 = 6.3. As R → ∞: 16R²/(R−1.5)³ ~ 16/R → 0. But the |ζ| bound exponent grows: |ζ| ≤ C|t|^{R−...}— the number of EM levels ⌈R−2⌉... each level adds a power: |ζ| ≤ C|t|^{k} with k = level: log|ζ| ≤ k log|t|: M ≈ (k + 0.7) log|t| + ...: total A ≈ 16R²/(R−1.5)³·(k + 0.7). R = 5, k = 4 (levels for σ > −3: B₄?): hmm the EM level for σ > −m is level m+1: |ζ| ≤ C|t|^{m+1}? Roughly level ℓ covers σ > −(ℓ−1) with |ζ| ≤ C|s|^ℓ. R = 5 needs σ ≥ −3: level 4: log|ζ| ≤ 4 log|t|: A ≈ 9.3·(4.7) ≈ 44. Still > 10.5.\n\nHmm. So the Davenport disc route CANNOT reach A = 10.5 with these simple estimates — the BC derivative factor is too lossy. D-056's 10.5 came from the partial-fraction identity (exact, no BC loss). \n\nOPTIONS:\n(A) Match D-056's constants by formalizing the PARTIAL-FRACTION route after all (needs the ξ Hadamard expansion — ruled out in D-066 as unavailable).\n(B) Change the Lean-side baked constants: marginTilde/Hhat in LiSkeleton have 10.5/48 hardcoded and marginTilde_convex + base points are PROVED with them. If the R-bound gives A′ = 300, B₀′ = 5000, then... the margiñ(n) = S(n) − B(n) + 1 with B(n) built from those bigger constants — the margin stays positive for large n (the S(n) ~ ½n log n dominates any log-power B(n)) — but the crossover N₀ and the two certified base points (margiñ(8×10⁴) ≥ 8001, margiñ(10⁵) ≥ 85501) were certified with the TIGHT constants! With A′ = 300: B(n) grows: margiñ(10⁵) = S(10⁵) − B(10⁵) + 1: the 4T·(A log T + B₀) term: T = √n+1 ≈ 317: 4·317·(300·5.9 + 5000) ≈ 4·317·6770 ≈ 8.6×10⁶ — vs the certified margiñ(10⁵) = 85501 — the bound would go NEGATIVE at n = 10⁵!! The crossover would move much higher (n ~ e^{A′·4-ish}?) — the base points and possibly the whole N₀ = 80 000 choice would need redoing — that's a big change to LiSkeleton + LiBasePoints (both proved, freeze protocol!). NO — the freeze protocol says existing proofs untouched until ii′-7. Changing the constants would violate the freeze and re-open the certified base points.\n\nHmm wait — but actually, is that right? Let me re-read what Bn/marginTilde use: from LiSkeleton line 754: marginTilde F n = S(n) − (2F(T) + 4T((2/3)C0hat T + 10.5·log(T+2) + 48) + 40·1.3352 + 2(e⁴+1)(7·Hhat T + 3.3) + IIMaj n + 1) + 1. The 10.5/48 appear in 4T·(... + 10.5 log + 48) and Hhat = 3C0hat² + 10.5 log + 48. These encode the R-bound's A, B₀. The assembly ii′-6 will need |R(s)| ≤ A log(|t|+2) + B₀ with THESE constants to instantiate marginTilde.\n\nSo the R-bound theorem must deliver A = 10.5, B₀ = 48 (or smaller). The Davenport-disc route with crude estimates gives ~10–100× bigger. To hit 10.5/48, the route needs to be TIGHT — which is exactly what D-056's partial-fraction computation achieves.\n\nHmm, wait — let me reconsider. Maybe the disc route CAN be tightened to ~10.5? The log-coefficient chain: the dominant term is 16R²/(R−r)³ × (log-coefficient of M). M's log-coefficient: from log|g| ≤ log|ζ| + Σ mₖ log(1/|s−ρₖ|): log|ζ| ≤ 2log|t| + log(3/4); Σ mₖ·log(1/0.2) with Σmₖ ≤ C₀(2t)-mult-count ≈ 0.433 log(2t)+... ≈ 0.433 log t + 0.886 loglog + 3.2: × log 5 ≈ 1.61: ≈ 0.7 log t. So M ≈ 2.7 log t + 1.26 loglog t + const. BC ×100: ≈ 270 log t. The 100× is the killer. The factor 100 = 16R²/(R−r)³ at R = 5/2, r = 3/2. The BorelCaratheodoryDeriv bound is inherently lossy (16 is not tight; the real BC-derivative bound is 2R/(R−r)²-ish — the Zeta23 DerivativeBound gives 2M(r')²/((R−r')(r'−r)²) with the intermediate r' = (R+r)/2: = 2M·((R+r)/2)²/((R−r)/2·((R−r)/2)²) = 4M(R+r)²/(R−r)³ — at R=2.5, r=1.5: 4·16/1 = 64 — still ~64×.\n\nEven with the tight BC derivative constant 2R/(R−r)² = 5: A ≈ 5·2.7 ≈ 13.5 — close-ish to 10.5 but over. Hmm — and that's not the lemma that exists (theirs is 16R²/(R−r)³ = 100).\n\nSo route (b) as-is CANNOT deliver 10.5/48. \n\nLet me reconsider. What are the options?\n\n**Option C: tighten via the R-bound's telescoped form.** The issue is BC-derivative on log g loses ~100×. But wait — D-056's proof itself: R(s) = ζ′/ζ(s₀) − Σ_near 1/(s₀−ρ) + Σ_far (s₀−s)/((s−ρ)(s₀−ρ)) − ... — the partial fractions give the EXACT decomposition with the far-sum converging tightly. The partial fractions come from the Hadamard product. D-066 said Hadamard is out because Mathlib lacks Weierstrass-product machinery. BUT — Zeta23 has `inv_gamma_eq_prod` (Weierstrass for 1/Γ)! Does Zeta23 have the ξ Hadamard product?? It's a PNT+ repo — the Hadamard product for ξ is used in the zero-counting RvM proofs usually... Let me grep Zeta23 for Hadamard/xi product.\n\nActually — hold on. Let me reconsider the exact requirement. The partial-fraction identity used in D-056: ζ′/ζ(s) = B + Σ_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2) — the FULL identity. What's actually NEEDED is only the DIFFERENCE R(s) = ζ′/ζ(s) − Σ_{near}1/(s−ρ) with the bound. The difference form needs the identity only as a black box... \n\nAlternatively — the Davenport route but bounding the RIGHT thing: instead of BC on log g giving |(log g)′|, note that we want |ζ′/ζ(s) − Σ_near 1/(s−ρ)| = |(log g)′(s) + Σ_{far-collected} mₖ/(s−ρₖ)| — the far-collected terms are the disc's annulus zeros... hmm those are only ≤ 2 per... no.\n\nHmm, wait — actually maybe reconsider the constants once more, more carefully. Is A = 10.5 REALLY unreachable? The pieces:\nM = sup_{B(s₀,R)} Re J_g = sup [log|g| − log|g(s₀)|] ≤ sup log|g| + |log|g(s₀)||.\n- sup log|g| ≤ 2 log|t| + log(3/4) + Σ mₖ log(1/clearance): clearance 0.2: ×log 5: Σ mₖ ≤ C₀-mult(t + 2.3-ish) — the Trudgian unit-window mult count: ~0.433 log t + 0.886 loglog t + 2.9 (say ×1.2 for the 2.3-width): ≈ 0.52 log t + 1.06 loglog + 3.5: ×1.61: ≈ 0.84 log t + 1.7 loglog + 5.6. So sup log|g| ≤ 2.84 log|t| + 1.7 loglog + 5.3.\n- −log|g(s₀)| = −log|ζ(s₀)| + Σ mₖ log|s₀−ρₖ| ≤ log ζ(2) + Σ mₖ log 2.3 ≈ 0.5 + 0.83·(0.52 log t + ...) ≈ 0.43 log t + 0.9 loglog + 3.4.\n- M ≤ 3.3 log t + 2.6 loglog + 9.\n- BC ×100: 330 log t + 260 loglog + 900. Fold loglog ≤ (1/e)log: ≤ (330 + 96) log t + 900 = 426 log t + 900. Yeah — A ≈ 426. No good.\n\nThe 100× BC factor is unfixable within that lemma. So to hit 10.5, one would need the derivative bound with a much better constant AND tighter geometry — even then 2.7 log t × 16R²/(R−r)³ needs 16R²/(R−r)³ ≤ 3.9 — impossible for R > √5 (min over R: as R→∞, 16/R → 0 BUT the |ζ|-bound exponent grows with R via more EM levels: log|ζ| ≤ (R-dependent level) log|t| — the level ⌈R−2⌉·... — so A ≈ 16R²/(R−1.5)³·(level + 0.7): R = 4: 16.4·(level 3? + 0.7) hmm what level for σ ≥ −2: B₃ rep (σ > −2 hmm boundary — R = 4 dips to −2 exactly — need level 4 for safety σ > −3): 16.4·4.7 ≈ 77. Still 7× over.\n\nSo the Davenport route gives A in the dozens-to-hundreds. NOT 10.5.\n\n**Decision point.** The marginTilde constants are baked in with 10.5/48 and the freeze protocol forbids touching them (they're already-proved lemmas + certified base points). So ii′-5 must deliver A ≤ 10.5, B₀ ≤ 48. The Davenport route can't. Therefore: **the route must change to the partial-fraction/reference-point proof (D-056's actual proof)** — which needs the ξ/ζ partial-fraction expansion. D-066 ruled that out as \"Mathlib has no Weierstrass product/order theory\". BUT let me re-examine: what EXACTLY is needed?\n\nR(s) = ζ′/ζ(s) − Σ_{|γ−t|<1} 1/(s−ρ). D-056's identity:\nR(s) = ζ′/ζ(s₀) − Σ_near 1/(s₀−ρ) + Σ_far (s₀−s)/((s−ρ)(s₀−ρ)) − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − ½(ψ(s/2) − ψ(s₀/2)).\n\nThis comes from the partial fraction ζ′/ζ(s) = B + Σ_ρ(1/(s−ρ)+1/ρ) − 1/s − 1/(s−1) + ½logπ − ½ψ(s/2), differenced between s and s₀. The KEY analytic content: the partial-fraction expansion of ζ′/ζ with the absolutely-convergent difference series.\n\nHmm — is there any chance Zeta23 has the ξ product? Let me grep for \"Hadamard\" or the ξ product or the partial fractions for ζ′/ζ. Actually — wait: the D-066 note said \"Mathlib has no Weierstrass product/order theory; extract_zeros_poles is finite-only\". And Zeta23 GammaFacts has inv_gamma_eq_prod (Weierstrass for 1/Γ — a SPECIFIC product, not general theory). The ξ product might exist in Zeta23 similarly as a specific? Let me check.\n\nAlso — alternative: derive the partial-fraction bound WITHOUT the full product: the difference series Σ_far (s₀−s)/((s−ρ)(s₀−ρ)) IS absolutely convergent from Σ1/|ρ|² < ∞ (Zeta23's zero_sum_inv_sq — used in ii′-1a!). The issue is identifying R(s) with that series — that identification IS the partial-fraction content.\n\nHmm, alternatively — the Mittag-Leffler route: ζ′/ζ(s) − Σ(1/(s−ρ)+1/ρ) is entire modulo... the content is that ζ′/ζ minus its principal parts converges to an entire function PLUS the elementary terms, and the entire function is CONSTANT (= B) by the order-1 growth. The order-1 growth of ξ — that's Hadamard-order theory again.\n\nOK here's another thought — the FUNDAMENTAL alternative: **change the baked-in constants**. What if the R-bound theorem delivers A′ = 500, B₀′ = 3000 (Davenport-honest), and we rework the margin? The margiñ(n) = S(n) − B(n) + 1 with B(n) bigger by ~50×: margiñ(n) > 0 needs n beyond a bigger crossover. The crossover for A′ = 500: S(n) ~ ½n log n vs B(n) ~ 4T·(A′ log T + B₀′) + ... with T = √n: B(n) ~ 4√n·(500·0.5·log n) = 1000√n log n vs S(n) ~ ½n log n: crossover when ½n log n ≈ 1000√n log n ⟹ √n ≈ 2000 ⟹ n ≈ 4×10⁶. And the finite verification goes to 5×10⁵ (LiVerifiedUpTo 5×10⁵) — N₀ must be ≤ 5×10⁵ for the finite bridge! With N₀ ≈ 4×10⁶ > 5×10⁵ — BREAKS the bridge (the finite verification coverage is only to 5×10⁵). So A′ = 500 fails the whole assembly structure. A′ must keep N₀ ≤ 5×10⁵: N₀ from crossover ½√n ≈ 2A′·... roughly √n₀ ≈ 4A′ hmm: crossover n₀ ≈ (4A′)²·... A′ = 500: n₀ ~ 4×10⁶. To keep n₀ ≤ 5×10⁵ hmm — but actually the margin has other terms; the real N₀ with A = 10.5 was 80 000. Scaling: N₀ ∝ A²: A′ = 50 ⟹ N₀ ≈ 80000·(50/10.5)² ≈ 1.8×10⁶ > 5×10⁵ — STILL breaks. A′ = 30: N₀ ≈ 80000·8 = 6.5×10⁵ — marginal. A′ ≤ ~25 needed. So even A′ = 50 breaks. The R-bound must be genuinely tight (A ≲ 20).\n\nHmm OK wait — but hold on, is the crossover really quadratic in A? margiñ(n) = S(n) − B(n) + 1: dominant S = ½n log n; B's leading: 4T·((2/3)C0hat T + A log T + B₀) ~ 4√n·A·(½ log n) = 2A√n log n. Crossover: ½n log n = 2A√n log n ⟹ √n = 4A ⟹ n₀ = 16A². A = 10.5: n₀ = 1764?? But N₀ = 80 000 was adopted — because of the OTHER terms (Hhat has 3C0hat² and the 2(e⁴+1)(7H+3.3) term ~ 114·7·3·(0.433 log)² ≈ 2400(log n)²... at n = 1764 the loglog-sized terms dominate). Anyway the quadratic-ish sensitivity N₀ ∝ A² stands: A′ ≲ 25 ⟹ N₀ ≲ 4.5×10⁵ ≈ within the 5×10⁵ bridge. A′ = 26: N₀ ≈ 80000·(26/10.5)² ≈ 4.9×10⁵ — just inside. So the target: A ≤ ~25 to be safe, matching B₀ accordingly (B₀ affects lower-order terms — less sensitive).\n\nHmm — so even A ≈ 25 could squeak through with a recomputed N₀ ≤ 5×10⁵ — BUT recomputing N₀ means re-running the margin analysis (E-028-style numerics) and REDOING the certified base points in LiBasePoints (they're proved with the CURRENT marginTilde shape!). If A changes, marginTilde's definition changes ⟹ marginTilde_convex (proved, session 011, ~1100 lines of ψ-table) and the base-point certifications (session 012) would need rework — all inside the freeze protocol's \"untouched\" zone. This is a BIG deal. The freeze protocol explicitly protects LiSkeleton/LiBasePoints proofs until ii′-7.\n\nSo the ONLY freeze-compatible outcomes: (i) A = 10.5, B₀ = 48 exactly (D-056's constants — meaning the partial-fraction route), or (ii) a SMALLER A, B₀ pair that still fits the baked forms... wait — no: the baked forms have 10.5/48 as LITERAL constants inside Hhat/marginTilde definitions. If the R-bound theorem proves |R| ≤ A′ log + B₀′ with A′ = 10.5, B₀′ = 48 exactly — the assembly matches. If A′ < 10.5, the assembly can still use 10.5 (since |R| ≤ A′·log + B₀′ ≤ 10.5 log + 48 as long as the smaller constants dominate-wise fit: A′ log(|t|+2) + B₀′ ≤ 10.5 log(|t|+2) + 48 iff (A′−10.5)log(|t|+2) ≤ 48 − B₀′ — needs A′ ≤ 10.5 AND B₀′ ≤ 48 (then ≤ holds for log ≥ 0 ✓)). So ANY tighter pair works.\n\nThe Davenport route delivers A′ ≥ ~30 at best. Not compatible. **Therefore ii′-5 must do the partial-fraction route.** Which means: the ζ′/ζ partial-fraction expansion must be built in Lean. D-066 said \"β1 (Hadamard) ruled out (Mathlib has no Weierstrass product/order theory; extract_zeros_poles is finite-only)\". \n\nHmm wait — but hold on. Let me re-examine what's really needed for the partial-fraction identity for ζ′/ζ. The classical proof: ξ entire of order 1 ⟹ Hadamard ⟹ log derivative ⟹ the series. The deep input is \"ξ has order ≤ 1\" (the growth estimate) + Hadamard factorization. Mathlib lacks Hadamard. \n\nBUT — there's a way to get the partial fractions for ζ′/ζ WITHOUT the full Hadamard machinery, used in some textbook proofs (e.g. the \"lemma\" route via the FE + Stirling + a Mittag–Leffler argument): Consider F(s) := ζ′/ζ(s) − Σ_ρ (1/(s−ρ) + 1/ρ) + 1/s + 1/(s−1) − ½logπ + ½ψ(s/2). The claim: F is entire and constant. The proof needs: (a) the Σ_ρ(1/(s−ρ)+1/ρ) converges locally uniformly (from Σ1/|ρ|² < ∞ ✓ have it), defining a meromorphic function with the right principal parts; (b) F entire after adding the elementary terms (poles cancel: ζ′/ζ's poles at zeros ρ (residue mult), at 1 (residue −1), at 0 (residue... 1/s term), ψ(s/2)'s poles at s = −2n cancel ζ's trivial-zero poles ✓); (c) F bounded/constant via growth: |F| = o(R) on a sequence of circles ⟹ F constant by Liouville-ish. Step (c) is the growth input: |ζ′/ζ(s)| ≤ C|s|^ε on far-from-zeros circles — via... the FE + Stirling — the SAME |ζ|-polynomial-bound machinery (which I'm building the EM version of!) + a digamma bound. So the partial-fraction identity is provable from: Σ1/|ρ|² + the EM-type bounds + digamma + a Mittag–Leffler convergence statement + \"entire + o(R) on circles ⟹ constant\". \n\nHmm — \"Mittag–Leffler\" in Mathlib: is there a general Mittag-Leffler theorem? There's `Mathlib/Analysis/Complex/MittagLeffler...`? I don't think Mathlib has Mittag-Leffler. But I don't need the theorem — I CONSTRUCT the meromorphic function directly: Σ_ρ(1/(s−ρ)+1/ρ) converges locally-uniformly-absolutely (from Σ 1/|ρ|² + |1/(s−ρ)+1/ρ| = |s|/|ρ(s−ρ)| ≤ 2|s|/|ρ|² for |s| ≤ |ρ|/2 — locally uniform via Weierstrass M-test with Σ|ρ|⁻²) ⟹ defines an analytic-off-poles function (via TendstoLocallyUniformlyOn.differentiableOn — the Weierstrass convergence theorem — which Mathlib HAS (used in ii′-3a: \"Weierstrass-convergence ✓\" per D-066 inventory!)). So the series defines a meromorphic function with the right principal parts — DIRECTLY, no Mittag-Leffler theorem needed. Then F = ζ′/ζ − series + elementary — entire (poles cancel — need residue matching at zeros: the series' pole at ρ has residue mult(ρ) = analyticOrderNatAt — matches ζ′/ζ's residue (logDeriv residue = order ✓ ii′-1b proved logDeriv-NF residues!) — so F extends over each zero; at 1: ζ′/ζ has residue −1, the −1/(s−1)... wait sign: ζ′/ζ ~ −1/(s−1) at 1 (simple pole of ζ with residue 1 ⟹ logDeriv has −1/(s−1)): F has −1/(s−1) term... D-056's formula: ζ′/ζ = ξ′/ξ − 1/s − 1/(s−1) + ½logπ − ½ψ(s/2). At s = 1: ξ′/ξ regular (ξ(1) = 1/2 ≠ 0); −1/(s−1) pole residue −1 ✓ matches ζ′/ζ's −1 residue ✓. At s = 0: −1/s residue −1: ζ′/ζ at 0: ζ(0) = −1/2 ≠ 0 ⟹ ζ′/ζ regular at 0?! Wait — the formula has −1/s which has a pole at 0 but ζ′/ζ doesn't — the ψ(s/2) also has a pole at 0 (ψ has pole at 0 with residue −1: −½ψ(s/2) ~ −½·(−2/s)·... ψ(w) ~ −1/w at w = 0: −½·(−1/(s/2)) = +1/s: so −1/s + ½logπ − ½ψ(s/2): the −1/s and +1/s cancel ✓. OK consistent.)\n\nThen F entire and the growth argument: |F(R)| = o(R) on circles avoiding zeros ⟹ F constant — actually the classical proof shows F ≡ B (a specific constant) via: F(s) − F(0)... hmm the cleanest: G(s) := F(s) − F(0) has G(0) = 0 and... no — the standard: F is entire with |F(s)| ≤ C log|s| on a sequence of circles |s| = R_k → ∞ ⟹ F constant (an entire function growing slower than |s| is constant — Liouville for polynomials: entire + |f| ≤ C(1+|s|^k) ⟹ polynomial of degree ≤ k — is THAT in Mathlib? `Complex... ` there's a polynomial-growth Liouville: hmm — \"an entire function bounded by C(1+|z|)^k is a polynomial\" — Mathlib: I don't recall it. Weaker k = 0 (bounded ⟹ const): `Complex.apply_eq_apply_of_bounded...` / Liouville IS in Mathlib (`Differentiable.apply_eq_apply_of_bounded`? there IS a Liouville theorem for bounded entire functions in Mathlib ✓ `Differentiable.apply_eq_apply_of_forall_norm_le`? something). For log-growth: reduce: if |F(z)| ≤ C log(2+|z|), then F is constant: consider G(z) := (F(z) − F(0))/z — entire (removable at 0) with |G| ≤ C log(R)/R → 0 on circles ⟹ G ≡ 0 by... G entire and G(R) → 0 on circles to ∞ ⟹ max principle on big discs ⟹ G ≡ 0 ⟹ F constant. The \"max principle on discs\" + \"entire vanishing on a sequence\" — elementary pieces (MaximumModulus — Mathlib has `Complex.MaximumModulus`? there's `norm_le_of_forall_mem_sphere_norm_le` (used in Zeta23: `Complex.norm_deriv_le_of_forall_mem_sphere_norm_le` appeared in Y.lean) ✓ circle-max exists).\n\nSo the growth needed: |F(s)| ≤ C log|s| on far circles — i.e., |ζ′/ζ(s) − Σ_{near}...| — hmm circular-ish. Let me look at the classical: the proof that the partial-fraction series equals ξ′/ξ minus... uses |ξ′/ξ| or |log ξ| bounds on circles — log ξ(s) = O(|s|^{1+ε})... For ζ′/ζ on far-from-zero circles: the Davenport disc bound we JUST proved (!!) gives |ζ| polynomial on discs, and the disc argument gives |ζ′/ζ(s) − Σ_near 1/(s−ρ)| ≤ A log|s| — THE R-BOUND ITSELF on the circle. Wait — that's circular (the R-bound is what we're proving). BUT — for the identity-principle purpose, ANY polynomial bound on far circles suffices: |F(s)| ≤ |s|^ε-ish. The circle bound: |ζ′/ζ(s)| ≤ |s|^o(1) on circles staying away from zeros: via... the local Davenport argument gives exactly |ζ′/ζ − Σ_near 1/(s−ρ)| ≤ C·(big constant)·log|s| on such circles — the CONSTANT doesn't matter for the growth argument (any C works)! So the loose Davenport R-bound (A ~ 400) is enough to fuel the growth argument for the partial-fraction IDENTITY, and then the identity + D-056's tight constant analysis gives the TIGHT R-bound (A = 10.5)!! \n\nWAIT. Let me double-check this logic — it's important:\n1. Davenport disc (loose): |ζ′/ζ(s) − Σ_{near} 1/(s−ρ)| ≤ C log|s| for s on the strip, far from zeros. (A ~ 400, B ~ 3000 — constants irrelevant.)\n2. Define F(s) := ζ′/ζ(s) + 1/s + 1/(s−1) − ½logπ + ½ψ(s/2) − Σ_ρ(1/(s−ρ) + 1/ρ)·... (the series converges by Σ1/|ρ|²). F entire (poles cancel by residue matching). On far circles: |F| ≤ |ζ′/ζ − Σ_near 1/(s−ρ)| + |Σ_far 1/(s−ρ) + 1/ρ| + |elementary| ≤ C log|s| + o(1) + O(log|s|) = O(log|s|) ⟹ F constant (growth argument). ⟹ **the partial-fraction identity holds** (with F = some constant B′).\n3. D-056's reference-point analysis of the identity: |R(s)| ≤ 10.5 log(|t|+2) + 48 — the tight constants from the identity + C₀-count + digamma_stirling (all available). The B′ constant cancels in the difference (D-056's differencing kills B and Σ1/ρ).\n\nHmm — step 2's growth: |F| on circles of radius R avoiding zeros: |ζ′/ζ(s) − Σ_{|γ−t|<1}1/(s−ρ)| ≤ C log R from step 1 — but step 1's bound is for s with σ ∈ [−5/2, 7/2] (the disc region) — the circle |s| = R has σ ranging to −R — outside the disc region!! The circles must stay in the region where the loose R-bound holds. Hmm. The classical proof uses circles R_k with Re s ∈ [−1, 2]-ish vertical strips... no — the circles are large. The standard growth input for the ξ-product proof is |ξ(s)| ≤ e^{O(|s| log|s|)} globally (from the FE + Stirling) — GLOBAL polynomial-ish growth — which needs... the left-strip |ζ| bound again (Stirling!). Hmm.\n\nOK here's the thing — I keep coming back to needing global-ish growth control. Let me think about what the MINIMAL growth statement for the identity is. The identity F = const needs F's growth on SOME sequence of contours exhausting ℂ (or just: F entire + bounded-ish on a sequence of circles ⟹ const). F is entire (after cancellation). Its growth on the circle |s| = R (R chosen avoiding zeros near |γ| = R... the circle hits all σ). On the right half (σ ≥ 1/2): disc-R-bound (loose) ✓. On σ ∈ [−5/2, 1/2]: FE-reflected loose bound (the digamma bracket needs |ψ| ≤ C log — digamma_stirling ✓ but the FE-reflection of the LOOSE disc R-bound also needs... the reflection needs R(1−s) which is the right-side bound ✓ and the digamma bracket ✓ — no Stirling!). On σ ∈ [−R, −5/2]: ζ′/ζ there — via FE: ζ′/ζ(s) = −ζ′/ζ(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)]: for σ ≤ −5/2: 1−s has re ≥ 7/2: |ζ′/ζ(1−s)| ≤ C (Dirichlet ✓); ΓR′/ΓR(1−s): re(1−s) ≥ 7/2 ✓ digamma_stirling ✓ ≤ C log; ΓR′/ΓR(s) with re s ≤ −5/2: ψ(s/2) with re(s/2) ≤ −5/4: recurrence shift +2: ψ(s/2+2) with re ∈ [3/4, ...] ✓ but ALSO the cot-free... wait — the ΓR′/ΓR(s) for re s ≤ −5/2 needs ψ(s/2) for re(s/2) ≤ −5/4 — the recurrence shifts by +2 each time: for σ ∈ [−R, −5/2], shift by +⌈R⌉-ish — the recurrence chain length grows with R!! The ψ bound then accumulates R/2 rational terms 1/(s/2+j) each ≤ 2/|t|-ish — for |t| ≥ 1: fine: |ψ(s/2)| ≤ C log|s| + (chain length)·O(1) — chain length ~ |σ|/2 ≤ R/2: total ≤ C log|s| + O(R) — POLYNOMIAL in R — breaks the o(R) growth!! Hmm — no wait: for the growth argument I need |F| ≤ o(R) on circles; if the ψ-chain gives O(R) — borderline (need little-o). Actually the classical fact: ψ(w) = log w + O(1) uniformly on re w ≥ −C away from poles — the recurrence: ψ(w) = ψ(w+N) − Σ_{j<N} 1/(w+j): each term 1/(w+j) with |w+j| ≥ ... on a circle avoiding the poles −2n: |w+j| ≥ 1: so |ψ(w)| ≤ C log|w+N| + N ≤ C log R + R/2 — O(R) — exactly borderline, NOT o(R). The tighter truth: the Σ1/(w+j) telescopes against log: Σ_{j<N}1/(w+j) ≈ log(w+N) − log w: |ψ(w)| = |log(w+N) − Σ 1/(w+j)| — the difference is O(1) not O(N) — via integral comparison: Σ_{j=0}^{N−1} 1/(w+j) vs log(w+N)−log w: the difference is bounded by Σ|1/(w+j) − ∫...| ≤ Σ 1/|w+j|² — hmm — converges-ish... For w on a circle avoiding the negative integers by ≥ δ: Σ_{j<N}|1/(w+j) − log-diff| — the Euler–Maclaurin comparison gives Σ_{j=0}^{N−1}1/(w+j) = log(w+N) − log w + O(1) with the O uniform in N for w away from the poles? I believe |ψ(w) − log w| ≤ C_δ uniformly on |w + j| ≥ δ (the standard uniform estimate) — provable via our digamma series (ii′-3a built it!) or Binet. So |ψ(w)| ≤ C log|w| + C′ uniformly — GOOD (o(R) ✓). But that's ANOTHER uniform-digamma-in-the-left-plane build (the recurrence-telescope comparison) — moderate work (~0.5 session).\n\nHmm OK — so the partial-fraction-identity route needs:\n(P1) The loose Davenport R-bound (for the growth input on the right).\n(P2) The FE-reflection machinery (also for ii′-5d anyway).\n(P3) The uniform left-plane digamma bound |ψ(w) − log w| ≤ C (away from poles).\n(P4) The series Σ_ρ(1/(s−ρ)+1/ρ) convergence (from Σ1/|ρ|² ✓ have).\n(P5) F entire via residue-cancellation at zeros (logDeriv residues = orders — ii′-1b machinery ✓), at 1, at 0, and at trivial zeros −2n (ψ's poles cancel ζ's trivial-zero poles — residue matching: ζ′/ζ at −2n has residue mult(−2n) = 1 (zeroMult(−2) = 1 ✓ ii′-4c; general −2n simplicity: ζ(−2n) simple — hmm — need mult(−2n) = 1 for ALL n — the ii′-4c proof was specific to −2 (used Λ(3) ≠ 0); general: Λ(−2n) = Λ(1+2n) ≠ 0 ✓ same argument works for all n (ΓR pole simple at −2n via Gamma_add_one iterations, Λ(1+2n) = ΓR(1+2n)ζ(1+2n) ≠ 0 ✓). So mult(−2n) = 1 for all n — a generalization of the 4c proof (induction). And −½ψ(s/2) at s = −2n: ψ(w) at w = −n: residue −1: −½·(−1)·2 = 1?? ψ(w) ~ −1/(w+n) at w = −n: −½ψ(s/2) ~ −½·(−1)/(s/2+n) = +½·2/(s+2n) = 1/(s+2n) — residue +1; and ζ′/ζ at −2n: residue +1 (simple zero): so ζ′/ζ(s) − ... − ½ψ(s/2) — hmm the F combination has −½ψ(s/2) MINUS?? F := ζ′/ζ + 1/s + 1/(s−1) − ½logπ + ½ψ(s/2) − Σ...: at s = −2n: ζ′/ζ residue +1, ½ψ(s/2) residue: ψ(s/2) ~ −1/(s/2+n) = −2/(s+2n): ½ψ residue = −1: total +1 − 1 = 0 ✓ cancel.\n(P6) The growth argument: F entire + O(log R) on a circle sequence ⟹ F constant. Circles |s| = R_k must avoid: zeros (|γ − R_k| ≥ 1/2 via the count — gaps exist by the C₀ count: in [R−1, R+1] ≤ C₀ zeros ⟹ a gap... elementary) AND the poles −2n (circle |s| = R with R odd-ish avoids −2n by ≥ 1/2: choose R_k = 2k+1 ✓ odd integers avoid even negatives... |s| = 2k+1: the point −(2k+1) is not a pole (−2n even) ✓ distance from −2k−1 to nearest pole −2k or −2k−2 is 1 ✓).\n(P7) D-056's tight constant analysis (the reference-point six-piece computation) — formalized with C0hat + digamma_stirling + Z₂ = −ζ′/ζ(2) ≤ 0.57 (certified via the LSeries partial sum — E-028's V5 certification: partial sum to 10⁶ + tail — in Lean: −ζ′/ζ(2) = Σ Λ(n)/n² — compute Σ_{n≤10⁶} + tail bound (log N+1)/N — a certified real computation in Lean?! That's heavy — 10⁶ partial sum in Lean — the LiBasePoints session did certified interval bounds of a similar flavor (rational partial sums) — a 10⁶-term rational sum in Lean is... actually feasible via native_decide? Hmm — 10⁶ terms with log-free forms (Λ(n) = log p or 0)... n^2 denominators... native_decide on a 10⁶-term rational sum — plausible but heavy (~minutes?). ALTERNATIVE: −ζ′/ζ(2) ≤ 0.57 — get it from the LSeries: −ζ′/ζ(2) = Σ Λ(n)n^{−2} ≤ ζ(2)-ish bounds — hmm: −ζ′/ζ(2) = 0.5699...: bound ≤ 0.57 needs precision ~ 1e-4 — a partial sum to ~10⁴ suffices (tail (log N)/N ~ 1e-4 at N = 10⁴ — E-028 used 10⁶ + tail 1.5e-5). In Lean: Σ_{n≤10⁴} Λ(n)/n² as a rational+log-primes sum — Λ(n) involves log p — not rational — the certified computation of Σ log p /p² needs interval bounds on log p — LiBasePoints did log-certifications... this is its own chunk of work (call it 0.25–0.5 session with the interval machinery from LiBasePoints).\n\nHmm — wait, actually, for (P7): is Z₂ = −ζ′/ζ(2) ≤ 0.5700 avoidable? The value enters B₀ = 48 (piece 1). A cruder Z₂ bound via... −ζ′/ζ(2) = Σ Λ(n)/n²: compare with ζ(2): Λ(n) ≤ log n: Σ log n/n² = −ζ′(2) = 0.9375 — so Z₂ ≤ 0.94 via Λ(n) ≤ log n and −ζ′(2) = Σ log n/n² = 0.9375... (still needs −ζ′(2) evaluated...). Even cruder: Σ Λ(n)/n² ≤ Σ (log n)/n² ≤ ... integral bounds: log n/n² ≤ ... Σ_{n≥2} log n/n² = log 2/4 + Σ_{n≥3} ≤ log2/4 + ∫₂^∞ log x/x² dx = 0.173 + (log 2 + 1)/2 = 0.173 + 0.847 = 1.02. So Z₂ ≤ 1.02 elementary — the cost to B₀ is +0.45 vs 0.57 — B₀ = 48 has slack? The margin sensitivity: B₀ enters 4T·B₀ ~ 192√n — +0.45 → +86√n·... hmm margiñ(8×10⁴) ≈ 8001 certified — the B₀ slack within margin: each unit of B₀ costs 4T ≈ 4·284 = 1136 margin points at n = 8×10⁴: +0.45 costs 511 — margin 8001 − 511 > 0 ✓ OK within slack. BUT — the baked marginTilde has 48 as a LITERAL — the assembly needs the Lean theorem's B₀′ ≤ 48 EXACTLY. If I prove |R| ≤ 10.5 log + 48.45 — that does NOT ≤ 10.5 log + 48. So the cruder Z₂ pushes B₀′ over 48 ✗. So Z₂ must be ≤ 0.569960... hmm — precisely: D-056's B₀ = 48.0 from assembling 39.8 + 7.97 with Z₂ ≤ 0.5700 folded: the constant budget: B₀ = 47.8 + ... — with Z₂ = 1.02 the fold gives ~48.25 — over. So I need Z₂ ≤ 0.57-ish (within ~0.2). Z₂ ≤ 0.65 would keep B₀′ ≤ 48? B₀ = 47.8 traced + 7.97 → 48.0 hmm the exact assembly: 0.57 + C₀ + 12.73C₀ + 7.06 + 0.09 + 0.29 with C₀'s constant 2.9·13.73 = 39.8: total constant = 0.57 + 39.8 + 7.06 + 0.09 + 0.29 = 47.8. If Z₂ ≤ 0.65: 47.9 ✓ under 48 ✓!! Z₂ ≤ 0.65 suffices for B₀ = 48. And Z₂ ≤ 0.65 via... the crude integral bound gave 1.02. Need better: partial sums: Z₂ = Σ Λ(n)n^{−2}: compute Σ_{n≤100} Λ(n)/n² numerically = 0.4927...? and tail Σ_{n>100} log n/n² ≤ (log 100 + 1)/100·... ∫: ≤ (log 100+1)/100 = 0.056: total ≤ 0.55 ✓. A partial sum to n = 100 with Λ's exact values + elementary tail — that's certifiable in Lean with ~100 log-values... the LiBasePoints machinery certified log 2, log 3 etc.? It certified exp/log rationals via the (1−x/16)⁻¹⁶ trick — logs of small primes via atanh series... n = 100 has 25 primes: 25 log values + von Mangoldt for prime powers — the sum Σ Λ(n)/n² to 100 = Σ_{p^k ≤ 100} (log p)/p^{2k} — 25 primes + powers: ~65 terms, each log p needs an interval bound to ~1e-3 — doable via the existing machinery but it's real work (0.25 sess).\n\nOK so honestly the FULL partial-fraction route (P1–P7) is a LOT — like 3–4 sessions, not 2–3. Versus the Davenport route which delivers A′ ~ 400 incompatible with the baked constants. \n\nHmm hold on, wait. Let me reconsider once more whether the baked constants REALLY force A ≤ 10.5. Let me re-read marginTilde (LiSkeleton:754):\n\nmarginTilde F n = (½n log n + (C₁−γ/2)n − 4) − (2F(T) + 4T((2/3)C0hat T + 10.5·log(T+2) + 48) + 40·1.3352 + 2(e⁴+1)(7·Hhat T + 3.3) + IIMaj n + 1) + 1\n\nwith Hhat T = 3·C0hat T² + 10.5·log(T+2) + 48, T = √n+1.\n\nThe 10.5 and 48 appear as the R-bound's A and B₀. If my proved R-bound is |R(s)| ≤ A′ log(|t|+2) + B₀′ with DIFFERENT constants, then the assembly ii′-6 needs marginTilde built with A′, B₀′. The current marginTilde is FIXED. So either:\n(i) A′ = 10.5, B₀′ = 48 (exact), or\n(ii) A′ ≤ 10.5 ∧ B₀′ ≤ 48 (tighter is fine — the assembly applies the theorem and then relaxes: |R| ≤ A′·log + B₀′ ≤ 10.5·log + 48 ✓ pointwise since log(|t|+2) ≥ log 12 > 0 ✓), or\n(iii) REDEFINE marginTilde with bigger constants and redo marginTilde_convex + base points (freeze violation + ~2 sessions of redo + the N₀ ≤ 5×10⁵ bridge analysis).\n\nSo (i)/(ii) are required. The Davenport route delivers (at honest tightest) maybe A′ ~ 30–400. (ii) needs A′ ≤ 10.5 — the disc route just can't get there (the BC factor alone is 100× the M-coefficient ~2.7).\n\nHence: **the R-bound must go through the partial-fraction identity** (P1–P7). The loose Davenport bound becomes a STEP (P1), not the final product. This is a significant route revision from D-064's R3 note — but wait — D-064's R3 note DID say \"the same bound is provable by the Davenport-Ch.-15 local route\" with estimate 2–3 sessions. The constant-tightness issue (BC 100×) means the local route delivers the WRONG constants. D-056's own proof IS the reference-point partial-fraction proof. So the honest plan: formalize D-056's proof, with the partial-fraction identity built via P1–P6.\n\nHmm, hold on, wait. Let me reconsider the BC constant loss once more, because maybe I'm being too pessimistic. The bound: ‖deriv f z‖ ≤ 16MR²/(R−r)³ for z ∈ closedBall(0, r). What if I apply it with r SMALL (the application region is |s−s₀| ≤ 3/2 but the BC needs r only ≥ application)? And R as large as the EM-levels allow... The factor 16R²/(R−r)³ — with r = 3/2: as R → ∞: 16/R — but M's log-coefficient grows: M ≈ (level + 0.7) log t with level ≈ R − 2 (EM levels): A ≈ 16(R−2+0.7)/R·... = 16(R−1.3)/R ≤ 16?!? wait — level ~ R−2: A ≈ (16R²/(R−1.5)³)·(R−1.3): R = 8: 16·64/42.9·6.7 ≈ 16·1.49·6.7 ≈ 160. R = 20: 16·400/6300·18.7 ≈ 16·0.0635·18.7 ≈ 19. R = 40: 16·1600/57000·38.7 ≈ 0.45·38.7 ≈ 17.4. Hmm — asymptotically 16·(level)/R ~ 16·(R)/R = 16. So the infimum ≈ 16–17 — JUST above 10.5, unreachable but close. With the 4M(R+r)²/(R−r)³ form (DerivativeBound, the r′-optimized version): ~4–5. Hmm — 16R²/(R−r)³ ~ 16/R vs 4(R+r)²/(R−r)³ ~ 4/R: with level-count ≈ (R−1.3)/... the product 16(R−1.3)/R → 16 as R→∞. Can't reach 10.5. Confirmed.\n\nBut WAIT — the EM-level count: the level needed for σ ≥ −(R−2) is ⌈R−2⌉+1 hmm — level ℓ covers σ > −(ℓ−1): for the disc B(2+it, R) need σ ≥ 2−R: level ℓ = ⌈R−2⌉+1 ≈ R−1: and |ζ| ≤ C|s|^ℓ: log|ζ| ≤ ℓ log|t| + C: M-coefficient ≈ ℓ + 0.7 ≈ R − 0.3: A ≈ 16R²/(R−1.5)³·(R−0.3) → 16 as R → ∞, always > 16. So even at the theoretical limit, A ≥ 16 > 10.5. The disc route FUNDAMENTALLY cannot deliver 10.5. Confirmed dead for the exact constants.\n\nSo — the partial-fraction route is FORCED. Let me now rescope ii′-5:\n\n**ii′-5 revised plan (partial-fraction route):**\n- ii′-5b ✓ (done): the |ζ| disc bound (still needed for the growth input P1's disc version... wait — P1 needs the loose R-bound on a region to fuel the growth argument. Hmm — do I still need the full loose Davenport R-bound? For the growth argument I need |F| = o(R) on a circle sequence — |F| ≤ |ζ′/ζ − Σnear 1/(s−ρ)| + |series-tail| + |elementary|. The first piece needs the loose R-bound (disc, A~400 fine) on the circle's right portion σ ∈ [−5/2, 7/2]; FE-reflection for σ ∈ [−R, −5/2] portion... and the reflection needs the LEFT-plane digamma uniform bound (P3). So the growth argument itself needs the full machinery of the loose R-bound + reflection + left-digamma. That's most of the work anyway.\n\nHmm, hold on — actually, let me reconsider. For the GROWTH argument for F entire ⟹ const, maybe there's a shortcut that avoids the loose R-bound: F(s) = ζ′/ζ(s) + 1/s + 1/(s−1) − ½logπ + ½ψ(s/2) − Σ_ρ(1/(s−ρ)+1/ρ). Bound |F| on the circle |s| = R_k (avoiding zeros/poles):\n- |½ψ(s/2)| ≤ C log R (left-plane uniform digamma P3).\n- |Σ_ρ(1/(s−ρ)+1/ρ)|: split |γ| ≤ 2R vs > 2R: near part: |1/(s−ρ)| ≤ 1/δ (circle avoids zeros by δ) + |1/ρ| — Σ_{|γ|≤2R} (1/δ + 1/|ρ|) ≤ count(2R)·(1/δ + 1/14) ≤ C R log R/δ·... = O(R log R) — TOO BIG (need o(R) hmm — count(2R) ~ R log R: ×1/δ = R log R — O(R log R) breaks o(R)). Hmm — the classical handles this via the paired form: 1/(s−ρ)+1/ρ = s/(ρ(s−ρ)): |s/(ρ(s−ρ))| ≤ R/(δ|ρ|) hmm — Σ_{|γ|≤2R} R/(|ρ|·δ): with |ρ| ≥ ... Σ 1/|ρ| over |γ| ≤ 2R ~ (log R)² (since Σ 1/|ρ| over |γ| ∈ [2^j, 2^{j+1}] ≤ count/2^j ~ log): so Σ_{|γ|≤2R} R/(δ|ρ|) ≤ R(log R)²/δ — STILL too big (need o(R) — (log R)² kills it? no: R(log R)² is NOT o(R)).\n\nHmm — so the naive circle bound on the series fails. The classical proof instead bounds |ξ′/ξ(s)| on the circles directly (via log ξ = O(|s|^{1+ε}) from the product...) — circular in a different way. Let me recall how the classical proof of the partial fractions for ξ′/ξ actually goes:\n\nDavenport Ch. 11-12: ξ has order 1 (from |ξ(s)| ≤ e^{C|s|log|s|} — via the FE + Stirling for Γ's LOG — the Stirling estimate log Γ(s) = (s−1/2)log s − s + O(1) in −π+δ < arg < π−δ — THE COMPLEX STIRLING AGAIN!). Then Hadamard factorization (order 1) ⟹ ξ(s) = e^{A+Bs}∏(1−s/ρ)e^{s/ρ} ⟹ log-derivative series. The Hadamard factorization theorem for order-1 entire functions — needs Jensen + the product convergence machinery. NOT in Mathlib per D-066.\n\nHmm — is the ξ Hadamard product maybe in Zeta23? It's a PNT+ repo — PNT via the explicit formula NEEDS the partial fractions (the explicit formula IS the integrated partial fractions). Let me grep Zeta23 for the partial fraction series of ξ′/ξ or the Hadamard product of ξ.\n\nActually — the WeilEF folder had \"Effective.lean\" with xi def... and Zeta23 proves the explicit formula (that's the whole point of the repo — the Anthropic paper's Weil-form infrastructure). The explicit formula in the strong form needs the ξ partial fractions. Let me grep for what they have: \"partial\" / \"logDeriv xi\" / \"Hadamard\" / \"XiPrime\"... The repo has XiPrime/ folders with ExplicitFormula/... Let me check Zeta23/XiPrime/ExplicitFormula/ZeroFree.lean and friends for partial-fraction content.\n\nTime check: this turn is already long. Let me do the grep for Zeta23 partial-fraction content, and then STOP to reconsider the plan properly — this is a genuine route fork (per §8.4a fork rule: the Davenport route to the tight constants is OBSTRUCTED (BC constant); the partial-fraction route needs inventory). The right move: investigate what's available for the identity, then update D-067 with the revised plan, and flag the constant-matching discovery (it's an important design correction: the loose Davenport route CANNOT feed the baked 10.5/48 — worth recording prominently).","signature":""},{"type":"text","text":"Before writing any Lean for 5c, I've hit a **design-critical issue** that changes the plan. Let me verify it numerically first, then check what Zeta23 has for the partial-fraction identity."},{"type":"tool_use","id":"Bash_328","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean && grep -rn \"partial\\|Hadamard\\|hadamard\" Zeta23/XiPrime/ --include=*.lean -r -l | head -5; grep -rn \"logDeriv.*xi\\|xi.*logDeriv\\|ξ′/ξ\\|logDeriv completedRiemann\" Zeta23/ --include=*.lean -r | grep -i \"theorem\\|lemma\" | head -8","description":"Search Zeta23 for partial-fraction/Hadamard content"},"extra_content":null}]