Session 025 — 2026-08-22 — ii′-5d COMPLETE: FE-reflection of the loose R-bound + left-plane digamma bound

Directive

Continue tier ii′-5 per STATE.md: ii′-5d — FE-reflection of the loose Davenport-disc R-bound (ii′-5c) to σ ∈ [−5/2, 1/2], |t| ≥ 10, plus the left-plane uniform digamma bound (ii′-5e input). User: "let's work on ii'-5d".

Outcome: ii′-5d COMPLETE

New file NguyenRH1/LiReflect.lean (~640 lines, 26 declarations, all axiom-audited: 3 standard axioms only, zero sorryAx), root-imported; full build GREEN (8761 jobs).

Capstone logDeriv_riemannZeta_sub_nearZeros_le_left: for s.im = t, re s ∈ [−5/2, 1/2], |t| ≥ 10, ζ s ≠ 0: ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} (zeroMult ρ)/(s−ρ)‖ ≤ 200000·(log|t|)². Constant deliberately loose (D-067 §6: only the ii′-5e identity passes tight constants to ii′-5f).

Second deliverable norm_digamma_sub_log_le_of_two_le_abs_im (the 5e input): ‖ψ(w) − log w‖ ≤ 3 for 2 ≤ |w.im| — UNIFORM in the shift chain length (this is what the γ-gap circles of 5e need).

Build path (all per D-067 §3/§6; zero surprises in the math)

1. §1 ΓR shift: gammaR_shift_four — ΓR(s+4) = π⁻²(s/2)(s/2+1)ΓR(s) off ℝ (Gammaℝ_def + Gamma_add_one twice + cpow arithmetic via cpow_def_of_ne_zero → exp form; exp(−2 log π) = (π²)⁻¹ via Real.log_inv/log_pow/exp_log). Then logDeriv_Gammaℝ_shift: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) via the EventuallyEq on {im ≠ 0} + logDeriv_div/const_mul + the comp deriv.
2. §2 the FE logDeriv identity logDeriv_zeta_fe: logDeriv ζ s = −logDeriv ζ(1−s) − [logDeriv ΓR s + logDeriv ΓR(1−s)] — from Λ =ᶠ ΓR·ζ near good points (completedZeta_eventuallyEq via ContinuousAt.eventually_ne), logDeriv_mul, and the chain-rule negation through Λ(1−z) = Λ(z). ζ(1−s) ≠ 0 from ζ s ≠ 0 via the Λ factorization both ways (riemannZeta_one_sub_ne_zero).
3. §3 the EXACT zero-sum cancellation sum_nearZeros_neg_reflect: nearZeros(−t) = (nearZeros t).image (1 − ·) (both directions by the symmetric ball estimate ‖(1−ρ)−(2∓it)‖² = (1+ρ.re)²+(ρ.im−t)² ≤ 5); zeroMult(1−ρ) = zeroMult ρ by Zeta23 analyticOrderAt_zeta_one_sub; 1−s−(1−ρ) = −(s−ρ). ⟹ the −t sum at 1−s IS minus the t sum at s.
4. §4 the ΓR-bracket bound ≤ 4(log|t|)²: both digamma arguments pushed into re > 0 (the s-side via the +4 shift), StirlingVert digamma_stirling + ‖log w‖ ≤ log‖w‖ + π (norm_log_le_of_one_le) + the rational term ≤ 1; fold via two_le_log_abs_t.
5. §5/§6 the left-plane digamma bound: ψ(w+n) = ψ(w) + Σ(w+j)⁻¹ (digamma_add_natCast, induction on digamma_apply_add_one); the sum vs the log difference compared by first-order Euler–Maclaurin (Zeta23 sum_eq_integral_add_integral_deriv with f x = (w+↑x)⁻¹); ∫₀ⁿ (w+x)⁻¹dx = log(w+n) − log w by FTC (hasDerivAt_log on the slit plane, HasDerivAt.comp_ofReal for the ℝ→ℂ chain); the B̃₁ remainder ≤ ½∫₀ⁿ dx/((x+re w)²+(im w)²) ≤ π/(2|im w|) ≤ π/4 by the ARCTAN FTC (avoids the full-line integral entirely: (1/c)arctan((x+a)/c) antiderivative + |arctan| < π/2); StirlingVert at v = w+n gives ‖ψ v − log v‖ ≤ 1; boundary ≤ 1/2. Total 1 + 1/2 + π/4 ≤ 3.
6. §7 capstone assembly: X(s) = −X(1−s) − bracket exactly (ring after hfe/hrefl) ⟹ ‖X‖ ≤ 100000L² + 4L² ≤ 200000L².

Banked gotchas (session 025 additions)

• lake -d <dir> env lean <abs path> compiles a single file from anywhere (no cd needed) — the reliable foreground form.
• add_le_add_left/right are SWAPPED vs the classic convention in this Mathlib: add_le_add_left (h : b ≤ c) (a) : b + a ≤ c + a; add_le_add_right (h : b ≤ c) (a) : a + b ≤ a + c.
• sub_left_inj here : a − c = b − c ↔ a = b (the VARYING side is "left"); for 1 − a = 1 − b use sub_right_inj.
• Finset.sum_image takes the map as the implicit g (to_additive of prod_image: (g := ...) or let the InjOn proof's type drive it); Finset.sum_neg_distrib : ∑ −f = −∑ f (use ← for the RHS form).
• Finset.sum_image's InjOn proof: beta-redex hypotheses break sub_left_inj.mp — ascribe have h1 : 1 - a = 1 - b := hab first.
• Real.pi_lt_d2 : π < 3.15 (NOT pi_lt_315); Real.log_two_lt_d9, Real.exp_one_gt_d9 as banked.
• HasDerivAt.inv produces the Pi.inv function form (c⁻¹) — instance paths don't match pointwise goals; use (hasDerivAt_inv hne).comp _ (...).const_add instead (pointwise fun y => y⁻¹ form) + simpa [Function.comp_def].
• HasDerivAt.comp_ofReal (RealDeriv.lean) : HasDerivAt e e' ↑z → HasDerivAt (fun y : ℝ => e ↑y) e' z — the clean ℝ→ℂ chain rule for complex antiderivatives on real intervals (FTC input).
• RCLike-coe cast atoms (↑(−1/2 : ℝ) inside EM conclusions) do NOT normalize under linear_combination's ring_nf — push_cast at hEM first; and ((↑(0:ℕ):ℝ):ℂ) vs ((0:ℝ):ℂ) vs (↑(0:ℕ):ℂ) are DIFFERENT atoms — keep every sum family in the single-cast (ℕ→ℂ) form from the start (digamma_add_natCast's family) and normalize hEM by push_cast + simp only [add_zero].
• intervalIntegral.integral_const_mul (const LEFT); the mul_const variant is f·r. intervalIntegral.integral_mono_on (hab) (hf) (hg) (h : ∀ x ∈ Icc ...).
• IntervalIntegrable.continuousOn_mul (hf : IntervalIntegrable f) (hg : ContinuousOn g) : IntervalIntegrable (g · * f ·) (continuous factor FIRST) — mirror Zeta23 EulerMaclaurin's usage; B1's integrability via intervalIntegrable_iff' + integrableOn_of_bounded with aestronglyMeasurable_B1.norm + abs_B1_le_half.
• div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (hbc : b ≤ c) : a / c ≤ a / b (the ordered-field form; div_le_div_iff_left is the ordered-GROUP one — wrong typeclass for ℝ).
• Complex.div_ofNat_im/re (simp): (z/2).im = z.im/2 — no manual div_im arithmetic needed.
• Complex.zero_im/zero_re exist but are NOT simp — simp at h on IsNontrivialZero 0 fails ("no progress"); use .ne' projections.

Status / next

ii′-5d COMPLETE. Next per D-067 §6: ii′-5e — the partial-fraction identity ζ′/ζ(s) = B + Σ_ρ m(1/(s−ρ) + 1/ρ) − 1/s − 1/(s−1) + ½log π − ½ψ(s/2) (series convergence via mult-weighted zero_sum_inv_sq; F entire by residue cancellation; |F| = o(R) on γ-gap circles using 5c + 5d + the left-plane digamma bound ⟹ F const). FIRST ITEM of session 026: zeroMult(−2n) = 1 for ALL n (generalize ii′-4c's zeroMult_neg_two via the product-form Γ recurrence Γ(z) = Γ(z+n+1)/∏_{j≤n}(z+j) — needed for F's entirety at the trivial zeros; ~0.25 sess, deferred from 5d per the sub-stage rule). Then ii′-5f (tight analysis → 10.5/48), ii′-3b, ii′-3c, ii′-6, ii′-7.