Current task: —

Updated 08-24-2026

D-069 — ii′-5f design: the tight R-bound in Lean (D-056's Theorem R)

Date: 2026-08-23 | Session: 035 | Task: 5.1 tier ii′-5f Status: DESIGN COMPLETE; two perimeter additions (P1, P2) APPROVED by the user 2026-08-23 and declared (LiContour.lean, session-035 commit).

0. Target

D-056's Theorem R, in the LiDisc-capstone shape: ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} m_ρ/(s−ρ)‖ ≤ 10.5·log(|t|+2) + 48 for s = σ + it, σ ∈ [−5/2, 3], |t| ≥ 10, s off the excluded set — from partialFraction_identity (5e-v-d) at s vs the reference point s₀ = 2 + it (B cancels; no evaluation of B needed).

1. Finding 1 (session 035): D-056's piece 2 undercounts the near window

D-056's assembly charges the near sum Σ_{|γ−t|<1} 1/|s₀−ρ| ONE unit-window count C₀(t), but |γ−t| < 1 spans TWO unit windows. Two honest routes:

Conclusion: the 10.5/48 constants survive, but ONLY via the two-unit form, which is NOT derivable from the per-unit perimeter ⟹ new declared specialization (P1) ZeroCountProp2 (approved; LiContour.lean).

This is a D-054-class assembly slip (paper-side; the BOUND is true — E-028 measured 26× slack; the traced constants needed the sharper count form). Erratum to D-056 §2 piece 2 recorded here.

2. The two perimeter additions (approved 2026-08-23)

Paper-ii′-7 duty: the appendix's perimeter list gains these two items (same trust classes as the existing entries).

3. The honest assembly (the fold)

With L = log(t+2), LL = log L, C₀ := Ĉ₀(t+1) = 0.433·L′ + 0.886·LL′ + 2.9 (L′ = log(t+3) ≤ L + 1/12):

  1. ‖ζ′/ζ(s₀)‖ ≤ dirichletC2 ≤ 0.995 (Λ(n) ≤ log n ⟹ ≤ Σ_{n≥2} log n/n² ≤ (log 2)/4 + (log 3)/9 + ∫₃^∞ log x/x² dx = (log 2)/4 + (log 3)/9 + (log 3 + 1)/3 ≈ 0.1733 + 0.1221 + 0.6995 = 0.9949; budget 1.01).
  2. near ≤ P1-count ≤ 0.6·L + 0.886·LL + 2.7 (|s₀−ρ| ≥ 1 since re ρ ≤ 1).

  3. far ≤ 4.5√2·[C₀ + (C₀ + 0.55) + 0.55] = 12.7279·C₀ + 7.00 (per-interval |s₀−s| ≤ 4.5, |s−ρ| ≥ x, |s₀−ρ| ≥ (1+x)/√2 with x = |t−γ|; Σ_{k≥1} 1/(k(k+1)) = 1; C₀(2t+1) ≤ C₀ + 0.55; the k > t tail ≤ 0.55 via Σ_{k≥11} log k/k² ≤ (log 10 + 1)/10 ≤ 0.331 and Σ 1/(k(k+1)) ≤ 1/11; the height-< 14 intervals empty by P2; the negative-γ side via conjugation). 4./5. ‖1/s − 1/s₀‖, ‖1/(s−1) − 1/(s₀−1)‖ ≤ 4.5/|t|² ≤ 0.045 each.

  4. ½‖ψ(s/2) − ψ(s₀/2)‖ ≤ 0.30 (sharp digamma remainder |r(w)| ≤ 1.2/|w|² via the level-2 EM (LiRBound b2Fun machinery) — the Lean Lemma D; |log(w/w₀)| ≤ 0.45·(1+ε) via the arg/modulus split). Total: 6.111·L + 12.163·LL + 47.6 ≤ 10.5·L + 48 ⟺ 12.163·LL − 4.389·L ≤ 0.4, and max over L ≥ log 12 is at L* = 12.163/4.389 = 2.772 with value 12.163·log(2.772) − 4.389·2.772 ≈ 0.234 ≤ 0.4 ✓ (the pinch lemma: one-variable calculus + certified endpoint/point evaluation, LiBasePoints pattern).

4. Finding 2 (session 035; ii′-6 repair map — NOT 5f scope)

D-036 §2's H(T) = 3·Ĉ₀² + A·log + B₀ charges the horizontal-contour near sum (i) one unit-window count (Finding-1 issue again — the two-unit form fixes this part cheaply) and (ii) L3's clearance 1/(3·Ĉ₀), which covers only zeros INSIDE the pigeonhole window: with T ∈ [a, a+1], zeros just outside [a, a+1] can sit at distance < 1/(3Ĉ₀) from T. Honest repair: extend the pigeonhole to the 3-unit window (a−1, a+2) (count ≤ 3·Ĉ₀, clearance ≥ 1/(7·Ĉ₀)-ish) and split the near sum at |γ−T| = 1/4: Σ ≤ Ĉ₀·7Ĉ₀ + 2Ĉ₀·4 = 7·Ĉ₀² + 8·Ĉ₀. Impact: marginTilde's baked 3·Ĉ₀² coefficient moves to ≈ 7 + o(1); the margin at the certified base points drops by ≈ 2(e⁴+1)·7·4·Ĉ₀² (≈ 1.5×10⁵ at n = 8×10⁴) — the crossover N₀ moves up (estimate: within [10⁵, 5×10⁵], still under the finite-verification cap); the convexity proof is structural and re-verifies. TO BE FACED at ii′-6 (D-037's I_III (2/3)·Ĉ₀ coefficient gets the analogous two-unit correction to (4/3)-ish). File under the 4.5-class repair map. E-028's 26× slack says the theorem survives; the certified crossover artifacts move.

5. Lean build plan (sub-stages)

Capstone statement (5f-iii; t ≥ 10 first, the t ≤ −10 corollary via conjugation if ii′-6's bottom horizontal needs it — TBD there): theorem logDeriv_riemannZeta_sub_nearZeros_le_tight (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hNLZ : NoLowZeros) {t : ℝ} (ht : 10 ≤ t) {s : ℂ} (hσ : -5/2 ≤ s.re ∧ s.re ≤ 3) (him : s.im = t) (hζ : riemannZeta s ≠ 0) : ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZeros t, (zeroMult ρ : ℂ) / (s - ρ)‖ ≤ 10.5 * Real.log (|t| + 2) + 48

6. Risks