← Session 25 — ii′-5 R-bound: design + level-2 EM disc bound
**ii′-5c COMPLETE** — the loose Davenport-disc R-bound is proved in Lean.
## What was built (LiDisc.lean, +~1000 lines, 32 new decls)
**Capstone** `logDeriv_riemannZeta_sub_nearZeros_le`: for `s.im = t`, `re s ∈ [1/2, 7/2]`, `|t| ≥ 10`, `ζ s ≠ 0`:
$$\bigl\|\zeta'/\zeta(s) - \textstyle\sum_{|\gamma-t|<1} m_\rho/(s-\rho)\bigr\| \le 100000\cdot(\log|t|)^2$$
- **R-gap**: the ×10-rescale trick — applied ii′-4's unit-window pigeonhole at a = 23 to the ×10-image of the zero-norm finset, ÷10 → R_c ∈ [2.3, 2.4] with clearance `gapD = 1/(50(k+1))`. Zero new pigeonhole code.
- **g = Cf r_c F**: built entirely on Zeta23's `Cf` API (`CfAnalytic`, `ZeroFactorization`); nonvanishing on closedBall(0, r_c) — the gap makes the boundary sphere zero-free, which is what lets the else-branch norm computation run.
- **Bounds**: `|g| ≤ (9/4)|t|²·gapD^{−M_c}` (max-modulus over the sphere), `log|g(0)| ≥ 0` (free since collected ‖ρ‖ < 1).
- **BC**: `LogOfAnalyticFunction` + `BorelCaratheodoryDeriv` with the factor folded to 450·M; logDeriv chain (`logDeriv_div/prod/pow/comp`) through the affine push-forward; extras bounded by the Jensen count (each ‖s−ρ‖ ≥ |t−γ| ≥ 1).
- **Constant fold**: `log(33/32) ≥ 1/33`, `log 4150 ≤ 9` (via e > 2.71), `M_bound ≤ 420L²`, final 75642L² ≤ 100000L².
- Notably: **no perimeter hypothesis** — the count input is the session-023 Jensen bound, not `ZeroCountProp`.
Build GREEN (8753 jobs, LiDisc now root-imported); all 32 declarations audited: **3 standard axioms only, no sorryAx**. Commits c7cbae5 (build) + 0755db5 (closure: journal-024, STATE, NGUYEN, db).
## Next (Session 025): ii′-5d
FE-reflection of the loose bound to σ ∈ [−5/2, 1/2]: the zero-sums cancel exactly by FE symmetry (ρ′ = 1−ρ, `mult_reflect`), the ΓR-bracket is bounded by `digamma_stirling` after a +2 recurrence shift — plus the left-plane uniform digamma bound needed again in 5e. Also queued: `zeroMult(−2n) = 1` for all n (generalizing ii′-4c).
raw content_json (database row)
[{"type":"text","text":"**ii′-5c COMPLETE** — the loose Davenport-disc R-bound is proved in Lean.\n\n## What was built (LiDisc.lean, +~1000 lines, 32 new decls)\n\n**Capstone** `logDeriv_riemannZeta_sub_nearZeros_le`: for `s.im = t`, `re s ∈ [1/2, 7/2]`, `|t| ≥ 10`, `ζ s ≠ 0`:\n$$\\bigl\\|\\zeta'/\\zeta(s) - \\textstyle\\sum_{|\\gamma-t|<1} m_\\rho/(s-\\rho)\\bigr\\| \\le 100000\\cdot(\\log|t|)^2$$\n\n- **R-gap**: the ×10-rescale trick — applied ii′-4's unit-window pigeonhole at a = 23 to the ×10-image of the zero-norm finset, ÷10 → R_c ∈ [2.3, 2.4] with clearance `gapD = 1/(50(k+1))`. Zero new pigeonhole code.\n- **g = Cf r_c F**: built entirely on Zeta23's `Cf` API (`CfAnalytic`, `ZeroFactorization`); nonvanishing on closedBall(0, r_c) — the gap makes the boundary sphere zero-free, which is what lets the else-branch norm computation run.\n- **Bounds**: `|g| ≤ (9/4)|t|²·gapD^{−M_c}` (max-modulus over the sphere), `log|g(0)| ≥ 0` (free since collected ‖ρ‖ < 1).\n- **BC**: `LogOfAnalyticFunction` + `BorelCaratheodoryDeriv` with the factor folded to 450·M; logDeriv chain (`logDeriv_div/prod/pow/comp`) through the affine push-forward; extras bounded by the Jensen count (each ‖s−ρ‖ ≥ |t−γ| ≥ 1).\n- **Constant fold**: `log(33/32) ≥ 1/33`, `log 4150 ≤ 9` (via e > 2.71), `M_bound ≤ 420L²`, final 75642L² ≤ 100000L².\n- Notably: **no perimeter hypothesis** — the count input is the session-023 Jensen bound, not `ZeroCountProp`.\n\nBuild GREEN (8753 jobs, LiDisc now root-imported); all 32 declarations audited: **3 standard axioms only, no sorryAx**. Commits c7cbae5 (build) + 0755db5 (closure: journal-024, STATE, NGUYEN, db).\n\n## Next (Session 025): ii′-5d\nFE-reflection of the loose bound to σ ∈ [−5/2, 1/2]: the zero-sums cancel exactly by FE symmetry (ρ′ = 1−ρ, `mult_reflect`), the ΓR-bracket is bounded by `digamma_stirling` after a +2 recurrence shift — plus the left-plane uniform digamma bound needed again in 5e. Also queued: `zeroMult(−2n) = 1` for all n (generalizing ii′-4c)."}]