← Session 27 — ii′-5c/5d: Davenport disc + FE-reflection bounds
thinking (52 chars)
All done. Let me give the final summary to the user.
**ii′-5d COMPLETE** — committed as `422505e` + closure `807c3b9`.
## What was built (LiReflect.lean, ~640 lines, 26 decls)
**Capstone** `logDeriv_riemannZeta_sub_nearZeros_le_left`: the loose R-bound
‖ζ′/ζ(s) − Σ_{|γ−t|<1} m/(s−ρ)‖ ≤ 200000·(log|t|)² now holds on the **left** half-strip σ ∈ [−5/2, 1/2], |t| ≥ 10 — the FE-reflection of 5c's disc bound. The three ingredients, exactly per D-067 §3:
1. **`logDeriv_zeta_fe`** — the pointwise log-derivative functional equation, via Λ =ᶠ ΓR·ζ near good points + the Λ(1−z) = Λ(z) chain-rule negation.
2. **`sum_nearZeros_neg_reflect`** — the zero-sums at t and −t cancel *exactly*: `nearZeros(−t) = (nearZeros t).image (1−·)` (symmetric ball estimate (1+ρ.re)²+(ρ.im−t)² ≤ 5), `zeroMult(1−ρ) = zeroMult ρ` via Zeta23's `analyticOrderAt_zeta_one_sub`, and 1−s−(1−ρ) = −(s−ρ).
3. **ΓR-bracket ≤ 4(log|t|)²** — the s-side needed the new `logDeriv_Gammaℝ_shift` (ΓR recurrence shifted by +4, exp-form cpow arithmetic) to put both digamma arguments in re > 0, then `digamma_stirling`.
**Bonus deliverable** (the 5e input): `norm_digamma_sub_log_le_of_two_le_abs_im` — ‖ψ(w) − log w‖ ≤ 3 for 2 ≤ |im w|, *uniform in the shift chain length* (digamma recurrence + first-order Euler–Maclaurin + an arctan-FTC bound that avoids the full-line integral entirely).
## Verification
- Full build GREEN: 8761 jobs, LiReflect root-imported.
- Axiom audit (`audit-session025-axioms.txt`): all 26 decls depend on **propext, Classical.choice, Quot.sound** only — zero sorryAx.
## Next (session 026)
ii′-5e — the partial-fraction identity. First item: `zeroMult(−2n) = 1` for all n (generalizing ii′-4c's `zeroMult_neg_two` via the product-form Γ recurrence; ~0.25 session, deferred from 5d per the sub-stage rule). STATE.md has the full 5e breakdown.
Banked gotchas worth noting: this Mathlib has `add_le_add_left/right` **swapped** vs the classic convention, and `Finset.sum_image`'s map is the implicit argument `g` — both cost a few compile cycles and are now in the journal.
raw content_json (database row)
[{"type":"thinking","thinking":"All done. Let me give the final summary to the user.","signature":""},{"type":"text","text":"**ii′-5d COMPLETE** — committed as `422505e` + closure `807c3b9`.\n\n## What was built (LiReflect.lean, ~640 lines, 26 decls)\n\n**Capstone** `logDeriv_riemannZeta_sub_nearZeros_le_left`: the loose R-bound\n‖ζ′/ζ(s) − Σ_{|γ−t|<1} m/(s−ρ)‖ ≤ 200000·(log|t|)² now holds on the **left** half-strip σ ∈ [−5/2, 1/2], |t| ≥ 10 — the FE-reflection of 5c's disc bound. The three ingredients, exactly per D-067 §3:\n\n1. **`logDeriv_zeta_fe`** — the pointwise log-derivative functional equation, via Λ =ᶠ ΓR·ζ near good points + the Λ(1−z) = Λ(z) chain-rule negation.\n2. **`sum_nearZeros_neg_reflect`** — the zero-sums at t and −t cancel *exactly*: `nearZeros(−t) = (nearZeros t).image (1−·)` (symmetric ball estimate (1+ρ.re)²+(ρ.im−t)² ≤ 5), `zeroMult(1−ρ) = zeroMult ρ` via Zeta23's `analyticOrderAt_zeta_one_sub`, and 1−s−(1−ρ) = −(s−ρ).\n3. **ΓR-bracket ≤ 4(log|t|)²** — the s-side needed the new `logDeriv_Gammaℝ_shift` (ΓR recurrence shifted by +4, exp-form cpow arithmetic) to put both digamma arguments in re > 0, then `digamma_stirling`.\n\n**Bonus deliverable** (the 5e input): `norm_digamma_sub_log_le_of_two_le_abs_im` — ‖ψ(w) − log w‖ ≤ 3 for 2 ≤ |im w|, *uniform in the shift chain length* (digamma recurrence + first-order Euler–Maclaurin + an arctan-FTC bound that avoids the full-line integral entirely).\n\n## Verification\n- Full build GREEN: 8761 jobs, LiReflect root-imported.\n- Axiom audit (`audit-session025-axioms.txt`): all 26 decls depend on **propext, Classical.choice, Quot.sound** only — zero sorryAx.\n\n## Next (session 026)\nii′-5e — the partial-fraction identity. First item: `zeroMult(−2n) = 1` for all n (generalizing ii′-4c's `zeroMult_neg_two` via the product-form Γ recurrence; ~0.25 session, deferred from 5d per the sub-stage rule). STATE.md has the full 5e breakdown.\n\nBanked gotchas worth noting: this Mathlib has `add_le_add_left/right` **swapped** vs the classic convention, and `Finset.sum_image`'s map is the implicit argument `g` — both cost a few compile cycles and are now in the journal."}]