D-067 — ii′-5 design: the R-bound in Lean (route b″, Stirling-free)

Date: 2026-08-22 | Session: 022 | Task: 5.1 tier ii′-5 (D-064 §4 R3) Status: DESIGN COMPLETE (inventory verified live against the vendored Mathlib + Zeta23). Implementation sub-stages ii′-5a..e below.

0. Target and context

Tier-ii′ goal (D-064 §5 graph [R3]): formalize the R-bound input to the ii′-6 assembly — D-056's Theorem R:

R(s) := ζ′/ζ(s) − Σ_{|γ−t|<1} mult(ρ)/(s−ρ), |R(s)| ≤ A·log(|t|+2) + B₀ (A = 10.5, B₀ = 48; σ ∈ [−5/2, 3], |t| ≥ 10)

D-056's pen-and-paper proof uses the ξ Hadamard partial fractions — RULED OUT for Lean (D-066: no Weierstrass/order theory in Mathlib). D-064's prescription: the Davenport Ch.-15 LOCAL route (disc + Borel–Carathéodory). This design pins the exact route, geometry, and constants, and — critically — ELIMINATES the two feared builds:

• No complex Stirling for Γ. The vertical-decay bound |Γ(a+ib)| ~ |b|^{a−1/2}e^{−π|b|/2} is NOT needed anywhere (see §2/§3).
• No Hadamard product for ξ. The zero-sum in R(s) is handled by the disc Blaschke-removal, and the left-strip half by FE-reflection with EXACT zero-sum cancellation (§3).

1. Geometry and the key obstruction

The disc argument needs |ζ| polynomially bounded on a disc covering both the application region and the near zeros. Zeros ρ = β+iγ with |γ−t| < 1 sit at distance up to √(c²+1) from any center c+it (β → 0⁺), and √(c²+1) > c ALWAYS — so every covering disc dips left of σ = 0, where the Dirichlet series and Zeta23's ZetaUpperBnd (σ ≥ 1−A/log|t| only, FromPNTPlus/ZetaBounds.lean:1402) are useless, and the FE bound would need Γ's vertical decay (§0, avoided). Resolution: keep the dip shallow (σ ≥ −1/2) and bound |ζ| there by ONE extra Euler–Maclaurin level (§2).

Chosen geometry (right region). Center s₀ = 2+it, outer radius R = 5/2 (disc ⊆ {σ ≥ −1/2}), zero-collection radius r_c = 2.3 (all |γ−t|<1 zeros: |ρ−s₀| ≤ √5 ≈ 2.236 < 2.3; clearance on the outer circle ≥ 0.2), application radius r_a = 3/2 (covers σ ∈ [1/2, 7/2] — the range the FE-reflection needs, §3).

Lean statement shape (target): for s = σ+it, σ ∈ [−5/2, 3], |t| ≥ 10, riemannZeta s ≠ 0: ‖logDeriv riemannZeta s − Σ_{ρ ∈ nearZeros t} (zeroMult ρ)/(s−ρ)‖ ≤ 10.5 * Real.log (|t|+2) + 48 with nearZeros t the finset of nontrivial zeros in the open window (finiteness: ii′-4's zerosIn_finite pattern; the mult-weighted count bound via the perimeter or ZerosBound — pinned at implementation).

2. The |ζ| polynomial bound on σ ≥ −1/2 (NEW BUILD, ~1 session)

One extra Euler–Maclaurin level over Zeta23's existing B₁ machinery:

ζ(s) = 1/2 + 1/(s−1) + s(s+1)·∫₁^∞ B̃₂(x)·x^{−s−2} dx (re s > −1, s ≠ 1)

with B̃₂(x) = ∫₀ˣ B̃₁, periodic, B̃₂(0) = 0, |B̃₂| ≤ 1/8 (B̃₂(x) = ((x−⌊x⌋)²−(x−⌊x⌋))/2 on each period). Derivation: Zeta23 has riemannZeta0 N s = riemannZeta s (re s > 0, Zeta0EqZeta) with the B₁-integral; IBP once (per unit interval + telescope; B̃₂ continuous so the boundary terms at integers vanish; tail converges for re s > −1); extend to −1 < re s ≤ 0 by the identity principle (both sides analytic there; agree on re s > 0). Then on the disc B(2+it, 5/2):

|ζ(s)| ≤ 1/2 + 1/|s−1| + |s||s+1|/(8(σ+1)) ≤ C(1+|t|)² (σ ≥ −1/2).

Pieces in Zeta23/FromPNTPlus: EulerMaclaurin.lean (B1, abs_B1_le_half, integral_deriv_mul_add_const IBP helper), ZetaBounds.lean (Zeta0EqZeta, integrability lemmas). New: B̃₂ def + properties + the IBP step + the identity-principle extension.

3. The two-half plan

Right half: σ ∈ [1/2, 7/2], |t| ≥ 10 (the Davenport disc, ~1–1.5 sess)

On B(2+it, 5/2):

1. |ζ| ≤ C(1+|t|)² (§2).
2. Collect the zeros {ρₖ} of ζ in B(s₀, 2.3) with multiplicities mₖ = analyticOrderNatAt ζ ρₖ (= zeroMult); count-with-multiplicity ≤ 3·C0hat(t+3)-style bound (three unit windows of ii′-4's ZeroCountProp; mult ≤ count via the window bound applied to multiplicities — or ZerosBound/Jensen; pin at implementation). g(s) := ζ(s)/∏ₖ(s−ρₖ)^{mₖ} — analytic, NONVANISHING on B(s₀, 2.3+); the removal analyticity via Zeta23 ZeroFactorization (StrongPNTPrefix.lean:214) or direct order arguments.
3. Outer circle: |g| ≤ C(1+|t|)²/(0.2)^m ⟹ log|g| ≤ A′log|t| + B′.
4. Center: |ζ(2+it)| ≥ 1/ζ(2) (via 1/ζ = Σμ(n)n^{−s}, ‖1/ζ‖ ≤ ζ(2) — Mathlib LSeries moebius; name check at build time) and ∏|s₀−ρₖ| ≤ 2.3^m ⟹ −log|g(s₀)| ≤ C′log|t|.
5. LogOfAnalyticFunction (StrongPNTPrefix:124): J_g analytic, J_g(s₀) = 0 (after the 0-centered translation), deriv J_g = g′/g, and Re J_g = log|g| − log|g(s₀)| ≤ M := (A′+C′)log|t| + B″.
6. BorelCaratheodoryDeriv (StrongPNTPrefix:108): ‖deriv J_g‖ ≤ 16M R²/(R−r_a)³ = 100M on B(s₀, 3/2).
7. deriv J_g = ζ′/ζ − Σₖ mₖ/(s−ρₖ) (logDeriv quotient/product rules). R(s) = (log g)′(s) + Σ_{collected, |γ−t|≥1} mₖ/(s−ρₖ); extras: each |s−ρₖ| ≥ |t−γₖ| ≥ 1 ⟹ |extras| ≤ count ≤ C₀-bound.

Left half: σ ∈ [−5/2, 1/2], |t| ≥ 10 (FE-reflection, ~0.5 sess)

Via Λ = ΓR·ζ (Zeta23 RvM.completedRiemannZeta_eq_Gammaℝ_mul, valid since ΓR(s) ≠ 0 off {−2n} and s ≠ 0) and Λ(1−s) = Λ(s) (completedRiemannZeta_one_sub):

ζ′/ζ(s) = −ζ′/ζ(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)].

Under riemannZeta s ≠ 0 also ζ(1−s) ≠ 0 (Λ-vanishing ⟺ IsNontrivialZero, completedRiemannZeta_eq_zero_iff, + the FE). Substituting R(1−s):

R(s) = −R(1−s) − [ΓR′/ΓR(1−s) + ΓR′/ΓR(s)] + [Σ_{|γ−t|<1} m/(s−ρ)] − [Σ_{|γ′+t|<1} m′/(1−s−ρ′)]

and the two sums CANCEL EXACTLY: zeros with γ′ near −t are ρ′ = 1−ρ with γ near t (FE symmetry), multiplicities match (mult_reflect — Zeta23 seam), and 1/(1−s−(1−ρ)) = −1/(s−ρ).

The ΓR-bracket: ΓR′/ΓR(w) = −(log π)/2 + ½ψ(w/2) (Zeta23 RvM.logDeriv_Gammaℝ — exists, used in XiPrime/ZeroCount/Y.lean). Both digamma arguments have positive real part:

• (1−s)/2: re ∈ [1/4, 7/4], |im| = |t|/2 ≥ 5 — direct.
• s/2: re ∈ [−5/4, 1/4] — shift by +2 via the digamma recurrence (Mathlib digamma_apply_add_one twice; two rational terms O(1/|t|)), landing in re ∈ [3/4, 9/4]. Bound: Zeta23.StirlingVert.digamma_stirling (0 < re, 1/2 ≤ |im|): ‖ψ(w) − log w + 1/(2w)‖ ≤ 3/w.im² — already proved in Zeta23. ⟹ |ΓR-bracket| ≤ log π + C·log|t| + O(1).

So |R(s)| ≤ |R(1−s)| + C·log|t| + O(1), and the right-half bound closes it. NOTE: this also SUBSUMES D-056's Lemma D (the digamma remainder) — never needed separately; digamma_stirling is strictly stronger.

Constants fold (~0.25 sess, with E-support if wanted)

Trace the constants through §2–§3 to the A = 10.5, B₀ = 48 form (the paper's values; the Lean proof can carry its own traced constants — they only need to fit under Bn FAlt in ii′-6, which has huge slack — D-056 §3 sensitivity: 26×). Decision at build time: match D-056's numbers or take the natural traced ones (must stay ≤ paper claims).

4. Inventory of existing machinery (all verified live, session 022)

Mathlib: Complex.borelCaratheodory (unused — Zeta23's derivative version is the one), completedRiemannZeta_one_sub, riemannZeta_ne_zero_of_one_lt_re, digamma_apply_add_one, riemannZeta_neg_two_mul_nat_add_one, LSeries vonMangoldt/moebius. Zeta23: FromPNTPlus/StrongPNTPrefix.lean — BorelCaratheodoryDeriv (‖deriv f‖ ≤ 16MR²/(R−r)³), LogOfAnalyticFunction (J_B with Re J_B = log‖B‖−log‖B(0)‖, deriv J_B = B′/B), ZeroFactorization, ZerosBound; FromPNTPlus/ZetaBounds.lean — Zeta0EqZeta (B₁-level ζ rep, re > 0), ZetaUpperBnd; GammaFacts/StirlingVert.lean — digamma_stirling; GammaFacts/Series.lean — digamma series + Weierstrass for 1/Γ (unused); RvM/CountByIntegral.lean — completedRiemannZeta_eq_Gammaℝ_mul, completedRiemannZeta_eq_zero_iff; XiPrime/ZeroCount/Y.lean — norm_digamma_le (‖ψ(w)‖ ≤ ‖w‖+8), RvM.logDeriv_Gammaℝ. ii′-4 (this project): ZeroCountProp, zeroWindow_finite, zeroMult_neg_two, two_le_C0hat.

5. Sub-stage plan (SUPERSEDED by §6 — see the route revision)

Risks: (a) the B̃₂ IBP is fiddly but elementary (mitigation: per-interval work is exactly EulerMaclaurin.lean's pattern); (b) the mult-weighted zero count may want a Jensen detour (ZerosBound exists); (c) logDeriv product-rule glue for the quotient g — standard.

6. ROUTE REVISION (session 022/023, constant accounting)

Discovery: the direct disc bound CANNOT deliver the target constants. The assembly's marginTilde/Hhat (LiSkeleton) have A = 10.5, B₀ = 48 as LITERALS inside already-proved, freeze-protected lemmas (marginTilde_convex, the LiBasePoints certifications, sessions 011–012). So the Lean R-bound theorem must land at A ≤ 10.5, B₀ ≤ 48 pointwise. But the disc route's final log-coefficient is (M's log-coefficient) × (the Borel–Carathéodory derivative factor): M ≈ 2.7·log|t| (log|g| ≤ 2log|t| + (log 5)·Σmₖ with the tight mult-weighted C₀-count) and StrongPNTPrefix's BorelCaratheodoryDeriv gives ‖(log g)′‖ ≤ 16MR²/(R−r)³ = 100·M at R = 5/2, r = 3/2 ⟹ A ≈ 270. Even the classically sharp form 2R/(R−r)² = 5 gives A ≈ 13.5, and minimizing 16R²/(R−1.5)³ over R (paying extra EM levels for the deeper left dip, M-coeff ~ R−1.3) has infimum 16. Every disc-only variant overshoots 10.5. (The disc route remains correct as a bound, just with unusable constants.)

Revised plan (two stages). The loose disc bound is the GROWTH INPUT for the partial-fraction identity; the tight R-bound is D-056's analysis of the identity:

• ii′-5c (revised): the LOOSE disc R-bound (any A < ∞), σ ∈ [1/2, 7/2], |t| ≥ 10 — the g/log-g/BC machinery of §3.
• ii′-5d: FE-reflection (loose bound to σ ∈ [−5/2, 1/2]) + the left-plane uniform digamma bound |ψ(w) − log w| ≤ C away from poles (recurrence + series-vs-log comparison, O(1) in the chain length).
• ii′-5e (NEW): the partial-fraction identity ζ′/ζ(s) = B + Σ_ρ m_ρ(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2) via: (i) the series converges (mult-weighted Σm_ρ/|ρ|² — Zeta23 zero_sum_inv_sq, the ii′-1a dominator); (ii) F := LHS − RHS is entire (residue cancellation at nontrivial zeros via the ii′-1b logDeriv machinery; at 1; at 0; at trivial zeros −2n — needs zeroMult(−2n) = 1 for ALL n, generalizing ii′-4c, ~0.25 sess); (iii) |F| = o(R) on a γ-gap circle sequence (R_k in gaps of the zero-ordinate set from the perimeter count; the series on the circle is O((log R)²) by the dyadic split; |ζ′/ζ| ≤ C log R on the circle by 5c on the right + 5d reflection on the left; elementary terms O(log R)) ⟹ F constant (divide by z after subtracting F(0), then maximum principle + Liouville — Mathlib has the bounded-entire Liouville + circle-max lemmas).
• ii′-5f (NEW): D-056's tight reference-point analysis ON the identity: the six-piece computation (Z₂ ≤ 0.65 certified in Lean suffices — B₀-budget 47.8 + slack; the near sum ≤ C₀(t); the far difference ≤ 12.73C₀ + 7.06 via Σ 1/(k(k+1)) = 1; the ψ-difference via digamma_stirling) ⟹ |R(s)| ≤ 13.73·C₀(t) + 7.97 ≤ 10.5 log(|t|+2)
• 48 EXACTLY. ~1 sess.

Total revised estimate for ii′-5: ~4 sessions (was 2–3). The loose disc constants never propagate — only the identity passes to 5f.

What 5f needs that 5c already provides: NOTHING of its constants — 5c's role is purely existential growth. This is the sense in which the user-flagged concern ("constants must survive the whole chain") is resolved: they do, because the chain is re-routed through the identity where the tight constants live.