[{"type":"thinking","thinking":"The Zeta23 `sum_eq_integral_add_integral_deriv` is the EM formula, for real-valued f? Let me check: `∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f k = f a * B1 a - f b * B1 b + ∫ f + ∫ deriv f * B1`. It's stated for `f : ℝ → 𝕜` with 𝕜 presumably ℂ or general RCLike. With a = 0, b = n (natural): B1 0 = ... B1 x = fract x − 1/2 for x ≥ 0; B1 0 = −1/2, B1 n = −1/2. Sum over k ∈ Ioc 0 n = {1..n}: f k. So Σ_{k=1}^{n} f k = −f 0·(−1/2)... wait: f a * B1 a = f 0 * (−1/2) = −f(0)/2; −f b * B1 b = +f(n)/2. So Σ_{k=1}^n f k = ∫₀ⁿ f + (f(n) − f(0))/2 + ∫₀ⁿ f′·B1. Then Σ_{j=0}^{n−1} f(j) = Σ_{k=1}^n f(k) + f(0) − f(n) = ∫₀ⁿ f + (f(0) − f(n))/2 + ∫ B̃₁ f′ ✓ matches my formula. \n\nFor the digamma bound, f(x) = (w + ↑x)⁻¹ : ℝ → ℂ. Conditions: differentiableAt ℝ f t for t ∈ Icc 0 n: f is smooth since w + t ≠ 0 (im ≠ 0) ✓; deriv f t = −(w+t)⁻² ✓; ContinuousOn deriv ✓. All fine.\n\nSo §5 (left-plane digamma) plan is fully supported:\n1. ψ(w + n) = ψ(w) + Σ_{j ∈ range n} (w + j)⁻¹ — induction with digamma_apply_add_one. Wait: hypothesis ∀ m : ℕ, s ≠ −m: with s = w + j, need w + j ≠ −m for all m; since im(w + j) = im w ≠ 0, w + j is never a real (≠ −m means complex not equal to real cast: if w + j = −m then im = 0 contradiction) ✓.\n2. EM: Σ_{j=0}^{n−1} f j = ∫₀ⁿ f + (f 0 − f n)/2 + ∫₀ⁿ f′·B1 with f = (w + ·)⁻¹.\n3. ∫₀ⁿ (w+x)⁻¹ dx = log(w+n) − log w via FTC (hasDerivAt_log, slit plane: im ≠ 0 ✓).\n4. Remainder: ‖∫₀ⁿ (−(w+x)⁻²) B1 x dx‖ ≤ (1/2) ∫₀ⁿ ‖w+x‖⁻² dx ≤ (1/2) ∫₀ⁿ ((x + re w)² + (im w)²)⁻¹ dx ≤ (1/2)(π/|im w|) ≤ π/4.\n   The integral evaluation ∫₀ⁿ ((x+a)² + c²)⁻¹ dx ≤ ∫_ℝ ... = π/c: need to build this. Check Mathlib for `integral_one_div_one_add_sq` or similar.\n\nLet me check what exists for ∫ 1/(1+x²) and whether intervalIntegral ≤ full integral lemmas exist.\n\nAlso I realize I should double-check how 5e will actually use the left-plane digamma bound, to get the hypothesis right. But per STATE.md the formulation \"|ψ(w) − log w| ≤ C away from poles\" with our |im w| ≥ 2 condition is the deliverable. Fine.\n\nNow — think about the main R-bound reflection theorem more carefully, since that's the core deliverable of 5d.\n\n**Theorem (ii′-5d capstone):** for t with 10 ≤ |t|, s with s.im = t, −5/2 ≤ s.re, s.re ≤ 1/2, ζ s ≠ 0:\n  ‖logDeriv ζ s − Σ_{ρ ∈ nearZeros t} (zeroMult ρ)/(s−ρ)‖ ≤ 200000·(log|t|)².\n\nProof:\n1. s' := 1 − s: s'.im = −t, |−t| ≥ 10 ✓; s'.re = 1 − s.re ∈ [1/2, 7/2] ✓; ζ s' ≠ 0 (via Λ) ✓. Apply 5c at (−t, s'): \n   ‖logDeriv ζ s' − Σ_{ρ' ∈ nearZeros (−t)} m(ρ')/(s'−ρ')‖ ≤ 100000·(log|−t|)² = 100000·(log|t|)² ✓ (abs_neg).\n\n2. FE identity: logDeriv ζ s = −logDeriv ζ s' − [logDeriv ΓR s + logDeriv ΓR s'].\n\n3. Sum cancellation: Σ_{ρ' ∈ nearZeros (−t)} m(ρ')/(s'−ρ') = −Σ_{ρ ∈ nearZeros t} m(ρ)/(s−ρ). (s' − ρ' = 1 − s − ρ'; with ρ' = 1 − ρ: 1−s−(1−ρ) = −(s−ρ) ✓.)\n\n4. Compute:\n   logDeriv ζ s − Σ_t m/(s−ρ) = −logDeriv ζ s' − bracket − Σ_t = −[logDeriv ζ s' + Σ_t ... ]... let me redo:\n   logDeriv ζ s = −logDeriv ζ s' − bracket\n   ⟹ logDeriv ζ s − Σ_t m/(s−ρ) = −logDeriv ζ s' − bracket − Σ_t m/(s−ρ)\n   = −[logDeriv ζ s' + Σ_t m/(s−ρ)] − bracket\n   and Σ_t m/(s−ρ) = −Σ_{−t} m/(s'−ρ') so:\n   = −[logDeriv ζ s' − Σ_{−t} m/(s'−ρ')] − bracket.\n   ⟹ ‖·‖ ≤ 100000 L² + ‖bracket‖ ✓.\n\n5. bracket bound ≤ 4·(log|t|)²-ish → final ≤ 100004·(log|t|)² ≤ 200000·(log|t|)². I'll fold loosely.\n\nNow the pieces to build, in dependency order:\n\n**Piece A: ΓR identities.**\n- A1: `Complex.Gammaℝ_ne_zero_of_im_ne_zero`? For s with im ≠ 0: ΓR s ≠ 0 since ΓR s = 0 ↔ s = −2n (real!). Gammaℝ_eq_zero_iff : Gammaℝ s = 0 ↔ ∃ n : ℕ, s = −2 * ↑n. If im s ≠ 0, s can't equal −2n (real) ✓. Check the exact Mathlib name: used in zeroDisc_isNontrivial as `Complex.Gammaℝ_eq_zero_iff`. ✓\n- A2: `differentiableAt_Gammaℝ_of_im_ne_zero` (Zeta23 XiPrime/Hardy/Basic.lean) ✓ exists.\n- A3: The shift identity: `logDeriv_Gammaℝ_of_im_ne_zero`-ish: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) for im s ≠ 0. OR the direct digamma form. Let me structure it as:\n  `logDeriv_Gammaℝ_eq_digamma_of_im_ne_zero {s : ℂ} (hs : s.im ≠ 0) : logDeriv Gammaℝ s = −(log π)/2 + (1/2)·digamma (s/2)`.\n  Proof: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) [shift lemma] = [−(logπ)/2 + ½ψ((s+4)/2)] − 2(s+1)/(s(s+2)) [logDeriv_Gammaℝ at s+4, re > 0 ✓] = −(logπ)/2 + ½[ψ(s/2) + (s/2)⁻¹ + (s/2+1)⁻¹] − 2(s+1)/(s(s+2)) [digamma_apply_add_one twice: ψ(v+2) = ψ(v+1) + (v+1)⁻¹ = ψ(v) + v⁻¹ + (v+1)⁻¹ with v = s/2; hypotheses ∀ m, v ≠ −m and ∀ m, v+1 ≠ −m — from im v = t/2 ≠ 0 ✓] = −(logπ)/2 + ½ψ(s/2) [field: ½·(2/s + 2/(s+2)) = 2(s+1)/(s(s+2)) ✓].\n  \n  So sub-lemma: `logDeriv_Gammaℝ_add_four_sub {s : ℂ} (hs : s.im ≠ 0) : logDeriv Gammaℝ s = logDeriv Gammaℝ (s + 4) − 2*(s+1)/(s*(s+2))`.\n  Proof via EventuallyEq: on U = {z | z.im ≠ 0} (open: isOpen_ne... {z : z.im ≠ 0} is open: continuous_im, isOpen_compl_singleton preimage... `isOpen_ne.preimage Complex.continuous_im`? hmm: {z | z.im ≠ 0} = Complex.im ⁻¹' {0}ᶜ — isOpen: isOpen_compl_singleton.preimage continuous_im ✓. Or use IsOpen from {z | z.im < 0} ∪ {0 < z.im}.)\n  On U: ΓR(z+4) = π^{−2}·(z/2)(z/2+1)·ΓR(z).\n    ΓR(z+4) = π^{−(z+4)/2} Γ((z+4)/2) [Gammaℝ_def]\n    (z+4)/2 = z/2 + 2 [ring]\n    Γ(z/2+2) = (z/2+1)·Γ(z/2+1) [Complex.Gamma_add_one (z/2+1 ≠ 0)] = (z/2+1)(z/2)Γ(z/2) [Gamma_add_one (z/2 ≠ 0)]\n    π^{−(z+4)/2} = π^{−z/2}·π^{−2}: cpow arithmetic. Via exp form: (π:ℂ)^w = exp (log π · w): `Complex.cpow_def_of_ne_zero`? Let me check the exact form: I think it's `Complex.cpow_def_of_ne_zero (hx : x ≠ 0) : x ^ y = exp (log x * y)`. Hmm, or use `Complex.ofReal_cpow`... Actually there's a cleaner simp path: for r > 0 real: ((r:ℝ):ℂ) ^ (z:ℂ) = Complex.exp (↑(Real.log r) * z)? There's `Complex.ofReal_cpow`? Let me check: `Complex.ofReal_cpow (hx : 0 ≤ x) (y : ℂ) : (↑x) ^ y = ↑(x ^ y.re) * ...`? no. Hmm, what about `Complex.ofReal_cpow_of_pos`? I don't remember. The safest: use cpow_def_of_ne_zero + Complex.log_ofReal (ofReal_log : log ↑r = ↑(Real.log r) for 0 ≤ r? `Complex.ofReal_log (hx : 0 ≤ x) : log ↑x = ↑(Real.log x)` ✓ exists I believe). Then:\n    π^{−(z+4)/2} = exp(log π · (−(z+4)/2)) = exp(log π·(−z/2) − 2 log π) = exp(log π·(−z/2))·exp(−2 log π) [exp_sub] = π^{−z/2} · (π:ℝ)^{(−2:ℝ)} [exp_ofReal... exp(↑(−2 log π)) = ↑(Real.exp (−2 log π)) = ↑(π^{−2}) via Real.exp_log? Real.exp(−2·log π) = (exp(log π))^{−2} = π^{−2}: Real.exp_log (π > 0) + Real.exp_mul? −2·log π = log of π^{−2}... `Real.exp_log (h : 0 < x) : exp (log x) = x`; write −2 log π = log (π^(−2:ℝ))? Real.log_rpow... simpler: Real.exp (−2 * Real.log π) = (Real.exp (Real.log π)) ^ (−2 : ℤ)? via `Real.exp_nat_mul`-ish... journal-024 banked `Real.exp_nat_mul : exp (n*x) = (exp x)^n`. For −2: Real.exp (−(2·log π)) = (exp (2 log π))⁻¹ = ((exp log π)²)⁻¹ = (π²)⁻¹ = π^{−2} ✓ elementary via Real.exp_neg + Real.exp_nat_mul/np ow.\n    So: ΓR(z+4) = π^{−2}·(z/2)(z/2+1)·ΓR(z) ⟹ ΓR(z) = π²·ΓR(z+4)/((z/2)(z/2+1)) on U [field_simp: π ≠ 0, z/2 ≠ 0 (im z ≠ 0 ⟹ z ≠ 0), z/2+1 ≠ 0 (im(z/2+1) = im z /2 ≠ 0... wait z/2 + 1 has im = (im z)/2 ≠ 0 ✓ so z/2+1 ≠ 0 ✓).]\n  Then logDeriv ΓR s = logDeriv (fun z => (π:ℂ)² * ΓR (z+4) / ((z/2)*(z/2+1))) s [EventuallyEq.deriv_eq + eq_of_nhds — via a small lemma logDeriv_congr: f =ᶠ[𝓝 x] g → logDeriv f x = logDeriv g x: simp [logDeriv_apply, h.deriv_eq, h.eq_of_nhds]]\n  = logDeriv (fun z => (π:ℂ)² * ΓR (z+4)) s − logDeriv (fun z => (z/2)*(z/2+1)) s [logDeriv_div: numer ≠ 0 at s (π² ≠ 0, ΓR(s+4) ≠ 0 since re(s+4) = re s + 4 ≥ 3/2 > 0 — Gammaℝ_ne_zero_of_re_pos ✓), denom ≠ 0 at s (factors ≠ 0 ✓), differentiability: ΓR(·+4) at s from differentiableAt_Gammaℝ (re(s+4) > 0) .comp (s+4 differentiable); polynomials ✓]\n  = logDeriv (ΓR ∘ (·+4)) s [logDeriv_const_mul: (π:ℂ)² ≠ 0] \n  = [deriv (ΓR ∘ (·+4)) s] / ΓR (s+4): deriv comp: deriv (fun z => ΓR (z+4)) s = deriv ΓR (s+4) * deriv (·+4) s = deriv ΓR (s+4) · 1. Via `deriv_comp`? hmm — journal gotchas: deriv_add_const etc. Actually there's `Deriv.comp`... simplest: (differentiableAt_Gammaℝ ...).hasDerivAt.comp s (hasDerivAt_id s |>.add_const 4)?? Then .deriv gives deriv (ΓR ∘ (·+4)) s = deriv ΓR (s+4) * 1... HasDerivAt.comp: (h₁ : HasDerivAt h h' (f x)) (h₂ : HasDerivAt f f' x) : HasDerivAt (h ∘ f) (h' * f') x. With f = (·+4), f' = 1: (hasDerivAt_id' s).add_const 4 : HasDerivAt (·+4) 1 s? `HasDerivAt.add_const (c) : HasDerivAt f f' x → HasDerivAt (fun x => f x + c) f' x` ✓. Then .deriv : deriv (ΓR ∘ (·+4)) s = deriv ΓR (s+4) * 1. But note the function is (fun z => ΓR (z+4)) vs (ΓR ∘ (·+4)) — defeq, `show` bridges.\n  Then logDeriv (fun z => ΓR (z+4)) s = deriv ΓR (s+4)/ΓR(s+4) = logDeriv ΓR (s+4) [logDeriv_apply def].\n  − logDeriv P s where P z = (z/2)*(z/2+1): logDeriv P s = deriv P s / P s; deriv P s: deriv_mul (both linear) = (1/2)(s/2+1) + (s/2)(1/2) = s/2 + 1/2. So logDeriv P s = (s/2 + 1/2)/((s/2)(s/2+1)) = 2(s+1)/(s(s+2)) [field_simp: s ≠ 0, s + 2 ≠ 0; note s+2 has im ≠ 0 ✓].\n  ✓ Piece A3 done. Then A4: the digamma form via logDeriv_Gammaℝ (re(s+4) > 0 ✓) + digamma recurrence twice.\n\n**Piece B: Λ logDeriv split.**\n- B1: EventuallyEq Λ (ΓR * ζ) at s: need s ≠ 0 and ΓR s ≠ 0 in a neighborhood. U = {z | z ≠ 0 ∧ Gammaℝ z ≠ 0} — open? ΓR continuous at s (differentiableAt_Gammaℝ_of_im_ne_zero ⟹ continuousAt) ⟹ {ΓR ≠ 0} ∩ ... is a nbhd: Filter.Eventually: (continuousAt_ΓR s).eventually_ne? `ContinuousAt.eventually_ne (h : f x ≠ 0) : ∀ᶠ y in 𝓝 x, f y ≠ 0`? hmm: ContinuousAt.eventually_ne exists? There's `ContinuousAt.eventually_ne (hf : ContinuousAt f x) (h : f x ≠ 0) : ∀ᶠ y in 𝓝 x, f y ≠ 0`? I believe yes. And s ≠ 0: isOpen_compl_singleton.mem_nhds. Combine: ∀ᶠ z in 𝓝 s, (z ≠ 0 ∧ ΓR z ≠ 0) — then on that set Λ z = ΓR z * ζ z (completedRiemannZeta_eq_Gammaℝ_mul) ⟹ EventuallyEq (Filter.eventuallyEq_of_mem? use Filter.EventuallyEq: `Filter.Eventually.mono` with eventuallyEq_iff... `Filter.EventuallyEq.of...` — construct: ⟨the Eventually of pairwise, mapped⟩ — `Filter.Eventually.eventuallyEq`? hmm: (h : ∀ᶠ x in l, f x = g x) : f =ᶠ[l] g IS the definition (EventuallyEq f g l := ∀ᶠ x in l, f x = g x). So just prove the ∀ᶠ of equality directly: filter_upwards [hU] with z hz; exact completedRiemannZeta_eq_Gammaℝ_mul hz.1 hz.2 ✓.\n- B2: logDeriv Λ s = logDeriv ΓR s + logDeriv ζ s: via B1 logDeriv_congr + logDeriv_mul (ΓR s ≠ 0, ζ s ≠ 0, differentiableAt ΓR (im ≠ 0), differentiableAt ζ (s ≠ 1: im ≠ 0)). \n- B3: logDeriv Λ s = −logDeriv Λ (1−s): as planned (funext of completedRiemannZeta_one_sub + deriv comp + deriv of (1−·) = −1).\n  Hmm wait: Λ (1−s) = Λ s pointwise (Mathlib completedRiemannZeta_one_sub : completedRiemannZeta (1 − s) = completedRiemannZeta s). So the FUNCTION (fun s => Λ (1−s)) = Λ (funext). Then logDeriv Λ s = logDeriv (fun s => Λ (1−s)) s [congr by the funext equality — rw] = deriv (fun s => Λ (1−s)) s / Λ (1−s). deriv: comp with (1−·): HasDerivAt (1−·) (−1): (hasDerivAt_const ..).sub? `HasDerivAt.const_sub (c) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c − f x) (−f') x` ✓. With f = id: hasDerivAt_id'... So HasDerivAt (fun s => Λ (1−s)) (deriv Λ (1−s) * (−1)) s via (differentiableAt_completedZeta h1s0 h1s1).hasDerivAt.comp s (hasDerivAt_const_sub...)... wait order: h.comp: (hh : HasDerivAt h h' (f x)) → (hf : HasDerivAt f f' x) → HasDerivAt (h ∘ f) (h' * f') x. Then .deriv: deriv (Λ ∘ (1−·)) s = deriv Λ (1−s) * (−1). logDeriv: /Λ(1−s) = −logDeriv Λ (1−s) [neg_div]. ✓\n  Needs: differentiableAt_completedZeta at 1−s: (1−s ≠ 0: im(1−s) = −t ≠ 0 ✓; 1−s ≠ 1 ⟺ s ≠ 0 ✓).\n- B4: combine B2(at s) + B2(at 1−s) + B3: logDeriv ζ s = −logDeriv ζ (1−s) − (logDeriv ΓR s + logDeriv ΓR (1−s)) — pure linear algebra from the three equations (linear_combination or ring_nf after treating as atoms: use `linear_combination` on ℂ? The equations are complex equalities; linear_combination works in commutative rings ✓).\n  Needs at 1−s: ΓR (1−s) ≠ 0 (re(1−s) = 1 − re s ≥ 1/2 > 0: Gammaℝ_ne_zero_of_re_pos ✓), ζ (1−s) ≠ 0 (via Λ argument), differentiableAt ΓR (1−s) (differentiableAt_Gammaℝ re > 0), differentiableAt ζ (1−s) ✓.\n- B5: ζ (1−s) ≠ 0: Λ(1−s) = Λ(s) [one_sub] = ΓR(s)ζ(s) [B1 pointwise at s] ≠ 0 [mul_ne_zero ΓR-ne (im≠0), hs0]. And Λ(1−s) = ΓR(1−s)ζ(1−s) [completedRiemannZeta_eq_Gammaℝ_mul at 1−s: 1−s ≠ 0 ✓, ΓR(1−s) ≠ 0 ✓]. So ζ(1−s) ≠ 0 [by contradiction: if = 0 then Λ(1−s) = 0 contra]. ✓\n\n**Piece C: reflection of the sum.**\n- C1: `zeta_one_sub_eq_zero_of` : ρ nontrivial zero ⟹ riemannZeta (1 − ρ) = 0. Via Λ: Λ(1−ρ) = Λ(ρ) = ΓR(ρ)·ζ(ρ) = 0 [completedRiemannZeta_eq_Gammaℝ_mul: ρ ≠ 0 (0 < re ρ), ΓR ρ ≠ 0 (re ρ > 0)]; Λ(1−ρ) = ΓR(1−ρ)ζ(1−ρ) [1−ρ ≠ 0 (re(1−ρ) = 1−re ρ > 0 ⟹ ≠ 0), ΓR(1−ρ) ≠ 0 (re > 0)] ⟹ ζ(1−ρ) = 0 ✓.\n- C2: `one_sub_mem_nearZeros_neg`: ρ ∈ nearZeros t ⟹ 1−ρ ∈ nearZeros (−t): \n  mem_nearZeros.mpr ⟨mem_zeroDiscFinset.mpr ⟨ball, C1⟩, im-window⟩.\n  ball: ‖1−ρ − discCenter (−t)‖ ≤ 5/2: 1−ρ − (2 + (−t)I) = −1 − ρ + tI... compute ‖·‖² = (1 + ρ.re)² + (ρ.im − t)² ≤ 4 + 1 = 5 ≤ 25/4 ✓ — need (ρ−discCenter t) decomposition: ρ ∈ zeroDiscFinset t gives nontrivial (0 < re < 1) and the im window |ρ.im − t| < 1.\n  Write 1 − ρ − discCenter (−t) = −(ρ − discCenter t) − ... hmm: 1 − ρ − (2 − it) = −1 − ρ + it = −(1 + ρ − it). And ρ − discCenter t = (ρ.re − 2) + (ρ.im − t)i. 1 + ρ − it = (1 + ρ.re) + (ρ.im − t)i. So ‖1−ρ − discCenter(−t)‖² = (1+ρ.re)² + (ρ.im−t)². With 0 < ρ.re < 1: (1+ρ.re)² < 4; |ρ.im − t| < 1: (ρ.im−t)² < 1. Total < 5 ≤ 6.25 ✓. In Lean: mirror the hnorm1 computation in nearZeros_subset_image (lines 1004–1033) — clone that pattern with (1 + ρ.re) instead of (ρ.re − 2): (1+ρ.re)² ≤ 4 via |1+ρ.re| ≤ 2... 1 + ρ.re ∈ (1, 2) so |1+ρ.re| ≤ 2 ✓, (1+ρ.re)² ≤ 4 ✓.\n  im-window: |(1−ρ).im − (−t)| = |−ρ.im + t| = |ρ.im − t| < 1 ✓.\n- C3: `nearZeros_neg_eq_image`: nearZeros (−t) = (nearZeros t).image (fun ρ => 1 − ρ):\n  ext ρ'; constructor:\n  - ρ' ∈ nearZeros (−t) ⟹ ρ' = 1 − (1 − ρ') and 1 − ρ' ∈ nearZeros t (C2 applied with roles swapped: 1−ρ' ∈ nearZeros t needs: ball ‖(1−ρ') − discCenter t‖ ≤ 5/2: (1−ρ') − (2+it) = −1 − ρ' − it = −(1 + ρ' + it); ‖1 + ρ' + it‖² = (1 + ρ'.re)² + (ρ'.im + t)²; ρ' nontrivial: 0 < re < 1 ✓; |ρ'.im + t| < 1 ✓ (from ρ' ∈ nearZeros(−t): |ρ'.im − (−t)| = |ρ'.im + t| < 1). im-window: |(1−ρ').im − t| = |−ρ'.im − t| = |ρ'.im + t| < 1 ✓. So C2 actually needs to be stated symmetric: I'll make one lemma `one_sub_mem_nearZeros_neg` and a second `mem_nearZeros_of_one_sub_mem` or just prove both directions inline with a shared computation. Cleanest: prove the bidirectional: ρ ∈ nearZeros t ↔ 1 − ρ ∈ nearZeros (−t), then C3 by ext + mem_image (∃ ρ ∈ nearZeros t, 1 − ρ = ρ' — take ρ = 1 − ρ').\n- C4: `zeroMult_one_sub (hρ : 0 < ρ.re) (hρ1 : ρ.re < 1) : zeroMult (1 − ρ) = zeroMult ρ`: unfold zeroMult; rw [analyticOrderAt_zeta_one_sub hρ hρ1]. ✓ (zeroMult is Zeta23.zeroMult — in our files we've been using `zeroMult` directly since `open Zeta23`.)\n- C5: `sum_nearZeros_neg_reflect`: Σ_{ρ' ∈ nearZeros (−t)} (zeroMult ρ' : ℂ)/(s' − ρ') = −Σ_{ρ ∈ nearZeros t} (zeroMult ρ : ℂ)/(s − ρ) where s' = 1 − s:\n  rw [C3, Finset.sum_image (injOn)]; then sum_congr: for ρ ∈ nearZeros t: zeroMult (1−ρ)/( (1−s) − (1−ρ) ) = zeroMult ρ/(−(s−ρ)) = −(zeroMult ρ/(s−ρ)); then sum_neg_distrib... `Finset.sum_neg_distrib`? or map: Σ (−f) = −Σ f: `Finset.sum_neg_distrib` exists? There's `Finset.sum_neg_distrib : ∑ i in s, -f i = -∑ i in s, f i` ✓ (I think it exists; else neg_sum or map_neg). \n  injOn: Set.InjOn (fun ρ => 1 − ρ) s: fun a _ b _ h => sub_left_inj.mp h ✓.\n\n**Piece D: the ΓR-bracket bound.**\n- D1: log bound: `Complex.norm_log_le_of...`: for w ≠ 0: ‖log w‖ ≤ |Real.log ‖w‖| + π. Build: log w re/im: `(Complex.log w).re = Real.log ‖w‖` (Complex.log_re), im = arg (Complex.log_im); ‖z‖ ≤ |z.re| + |z.im| (Complex.norm_le_abs_re_add_abs_im); |arg w| ≤ π (Complex.abs_arg_le_pi). ✓\n- D2: for our two specific w's ((1−s)/2 and (s+4)/2): 5 ≤ ‖w‖, ‖w‖ ≤ |t| + c ⟹ |Real.log ‖w‖| = Real.log ‖w‖ (‖w‖ ≥ 1 ⟹ log ≥ 0) ≤ Real.log |t| + const: Real.log ‖w‖ ≤ Real.log (2|t|) = log 2 + log|t|... ‖w‖ ≤ 2|t| for |t| ≥ 10: Real.log_le_log (0 < 5 → 0 < ‖w‖) (‖w‖ ≤ 2|t|) hmm Real.log_le_log (hx : 0 < x) (h : x ≤ y) : log x ≤ log y ✓ banked journal-024. Then log (2|t|) = log 2 + log |t| (Real.log_mul (2 ≠ 0) (|t| ≠ 0)) ✓. So ‖log w‖ ≤ log|t| + (log 2 + π) ≤ log|t| + 4 (log 2 < 0.7, π < 3.15).\n- D3: `norm_digamma_le_of` : 0 < re w, 1/2 ≤ |im w|, 5 ≤ ‖w‖, ‖w‖ ≤ 2|t|, 10 ≤ |t| ⟹ ‖digamma w‖ ≤ Real.log |t| + 5: ‖ψ‖ ≤ ‖ψ − log + 1/(2w)‖ + ‖log w‖ + ‖1/(2w)‖ ≤ 3/(im w)² + (log|t| + 4) + 1/(2·5) with |im w| = |t|/2 ≥ 5: 3/25 ≤ 0.12; total ≤ log|t| + 4 + 0.12 + 0.1 ≤ log|t| + 5. ✓\n- D4: rational term: ‖2(s+1)/(s(s+2))‖ ≤ 1 (say): ‖2(s+1)‖ ≤ 2(‖s‖ + 1) ≤ 2(|t| + 5/2 + 1) ≤ 2·2|t|... hmm |re s| ≤ 5/2 so ‖s‖ ≤ |re| + |im| ≤ 5/2 + |t| (norm_le_abs_re_add_abs_im) — need ‖s + 1‖ ≤ ‖s‖ + 1 ≤ |t| + 7/2 ≤ 1.4|t| (|t| ≥ 10: 7/2 ≤ 0.35·10 ✓ hmm 3.5/10 = 0.35 so ‖s+1‖ ≤ 1.35|t| ≤ 1.4|t|). ‖s‖ ≥ |im s| = |t| (abs_im_le_norm) ✓; ‖s+2‖ ≥ |t| ✓. So ‖2(s+1)/(s(s+2))‖ = 2‖s+1‖/(‖s‖‖s+2‖) ≤ 2·1.4|t|/(|t|·|t|) = 2.8/|t| ≤ 0.28 ≤ 1. ✓\n- D5: bracket assembly: bracket = logDeriv ΓR (1−s) + logDeriv ΓR s = [−(logπ)/2 + ½ψ((1−s)/2)] + [−(logπ)/2 + ½ψ(s/2)] — wait, for the s-side I need the digamma form at s/2 directly (A4 gives logDeriv ΓR s = −(logπ)/2 + ½ψ(s/2) for im s ≠ 0). But then bounding ψ(s/2) with re(s/2) possibly negative needs the LEFT-plane bound (§5)! Hmm. That's why the design shifts s/2 by +2: ψ(s/2) = ψ(s/2+2) − (s/2)⁻¹ − (s/2+1)⁻¹ and bound ψ(s/2+2) via StirlingVert (re(s/2+2) ∈ [3/4, 9/4] > 0 ✓, im = t/2 ✓). So in the bracket, keep the ψ((s+4)/2) form (avoid §5 dependency):\n  bracket = −log π + ½ψ((1−s)/2) + ½ψ((s+4)/2) − 2(s+1)/(s(s+2)).\n  [from: logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) (A3) and logDeriv ΓR (s+4) = −(logπ)/2 + ½ψ((s+4)/2) (logDeriv_Gammaℝ, re > 0).]\n  ‖bracket‖ ≤ log π + ½(log|t| + 5) + ½(log|t| + 5) + 1 = log π + log|t| + 6 ≤ log|t| + 8 (log π ≤ 1.2 < 2). \n  Fold: log|t| + 8 ≤ 2 log|t| + ... whatever; final: ≤ (log|t|)² + ... Let me just do: log|t| + 8 ≤ 4·(log|t|)²? (log|t|)² ≥ (log 10)² ≥ 5.3 > 5.29; log|t| ≤ (log|t|)²/2·... For x ≥ log 10 = 2.302: x + 8 ≤ 4x²? 4·5.3 = 21.2 ≥ 10.3 ✓ and 4x² − x − 8 increasing for x ≥ 2.3 ✓ (derivative 8x−1 > 0). So bracket ≤ 4·(log|t|)² for |t| ≥ 10 ✓. In Lean: nlinarith with hL : Real.log 10 ≤ Real.log |t| and Real.log 10 ≥ 23/10 (or some rational bound: log 10 > 2.3: Real.log 10 — is there a Mathlib bound? `Real.log_two_lt_d9`? For log 10: log 10 = log 2 + log 5... or from journal-024: two_le_log_abs_t (e² ≤ 2.7183² < 10 ⟹ 2 ≤ log 10 ≤ log|t|) — LiDisc HAS `two_le_log_abs_t`! (journal-024 §6: \"two_le_log_abs_t (e² ≤ 2.7183² < 10)\"). So with L := log|t| ≥ 2: L + 8 ≤ 4L² ⟺ 4L² − L − 8 ≥ 0 at L = 2: 16 − 2 − 8 = 6 ≥ 0 ✓; nlinarith with L ≥ 2: 4L² − L − 8 = L(4L − 1) − 8 ≥ 2·7 − 8 = 6 > 0 ✓ nlinarith [sq_nonneg ...] should handle: 4L² ≥ 4·2·L = 8L (from L ≥ 2: L² ≥ 2L) ⟹ 4L² − L − 8 ≥ 7L − 8 ≥ 6 > 0 ✓ nlinarith [hL, mul_le_mul ...]. Fine.\n  \n  Then final: ‖R(s)‖ ≤ 100000 L² + 4 L² = 100004 L² ≤ 200000 L² ✓. I'll state the final theorem with 100004 or 200000 — 200000 is cleaner and obviously safe; but hmm, actually let me reconsider: maybe better to keep it tight-ish as 100004·(log|t|)²? Nah — \"constants don't propagate\" (D-067 §6). 200000 it is. Actually wait — for elegance, state as ‖·‖ ≤ 100000·(log|t|)² + 4·(log|t|)² then conclude ≤ 200000·(log|t|)²? Just do the calc to 100004 then nlinarith to 200000 in one go. Or simply state the theorem with bound 100000·(log|t|)² + 4·(log|t|)²? No — cleaner single constant: 200000.\n\n**Piece E: left-plane digamma uniform bound** (for 5e; standalone):\n`norm_digamma_sub_log_le {w : ℂ} (hw : 2 ≤ |w.im|) : ‖digamma w − Complex.log w‖ ≤ 4` (constant TBD from the assembly: 1 + 1/2 + π/4 ≈ 2.3; use 3 or 4 for slack).\nSteps (as analyzed):\n- E1: shift: digamma (w + n) = digamma w + Σ_{j ∈ range n} (w + j)⁻¹ for n : ℕ, all w + j ≠ 0 — induction. With n := ⌈|w.re|⌉₊ + 2? hmm: need 0 < re(w + n): re(w+n) = w.re + n ≥ w.re + |w.re| + 2 ≥ 2 ✓ wait n = ⌈|re|⌉ + 2 ≥ |re| + 1 (Nat.ceil ≥ x, actually ⌈x⌉₊ ≥ x for x ≥ 0: `Nat.le_ceil`). So re(w+n) ≥ w.re + |w.re| + 1 ≥ 1 > 0 — for digamma_stirling need 0 < re ✓ and |im(w+n)| = |im w| ≥ 2 ≥ 1/2 ✓.\n- E2: EM (sum_eq_integral_add_integral_deriv) with a = 0, b = n, f x = (w + ↑x)⁻¹:\n  Σ_{k ∈ Ioc 0 n} f k = f 0 · B1 0 − f n · B1 n + ∫₀ⁿ f + ∫₀ⁿ f′·B1.\n  B1 0 = B1 n = −1/2 (b1_eq_fract_sub_half: B1 x = fract x − 1/2 for x ≥ 0; fract 0 = 0, fract n = 0 (Int.fract_natCast? `Int.fract_natCast_eq_zero`? or fract_ofNat... check: Int.fract_natCast : Int.fract n = 0? something like that)). Ioc 0 n as finset: {1,...,n} = range n shifted: Σ_{k ∈ Ioc 0 n} f k = Σ_{j ∈ range n} f (j+1) — reindex (Finset.sum_Ioc_eq_sum_range? there's `Finset.sum_Ioc_eq_sum_range : ∑ k ∈ Ioc m n, f k = ∑ k ∈ range (n − m), f (m + 1 + k)` ✓ I believe).\n  Hmm — but E1's sum is over j ∈ range n of (w + j)⁻¹ = f j. So Σ_{j ∈ range n} f j = f 0 + Σ_{k=1}^{n−1}... = f 0 + [Σ_{k=1}^{n} f k] − f n. Combine: Σ_{j=0}^{n−1} f j = ∫₀ⁿ f + (f 0 − f n)/2 + ∫ f′B1 ✓.\n  Wait — actually need n ≥ 1 for the manipulations; if n = 0 the sum is empty; but n = ⌈|re|⌉ + 2 ≥ 2 ✓ always.\n- E3: ∫₀ⁿ f = log(w + n) − log w: intervalIntegral.integral_eq_sub_of_hasDerivAt (hasDerivAt_log at each w + x ∈ slitPlane) — needs the derivative continuous/integrable: f continuous ✓. HasDerivAt (fun x => Complex.log (w + ↑x)) ((w + ↑x)⁻¹ · 1)? chain: hasDerivAt_log (slit) comp... HasDerivAt.comp with (w + ·): ((w+x)⁻¹ * 1). Hmm: HasDerivAt (log ∘ (w + ·)) ((w+x)⁻¹ * 1) x: (hasDerivAt_log hslit).comp x ((hasDerivAt_id x).const_add w)? const_add: HasDerivAt (fun x => w + x) 1 x: (hasDerivAt_id' x).const_add w — forms: HasDerivAt.const_add (c) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c + f x) f' x ✓. comp: HasDerivAt (log ∘ fun x => w + x) ((w+x)⁻¹ * 1) x; (w+x)⁻¹ * 1 = (w+x)⁻¹ ✓ simp. Then integral_eq_sub_of_hasDerivAt needs: ∀ x ∈ uIcc 0 n, HasDerivAt ... AND IntervalIntegrable of the derivative: continuous (w+x)⁻¹ on the interval (im ≠ 0) ⟹ ContinuousOn.intervalIntegrable ✓.\n  Slit plane membership: w + ↑x ∈ slitPlane ⟺ ¬(im = 0 ∧ re ≤ 0): im(w + x) = im w ≠ 0 ✓. `Complex.mem_slitPlane_iff`? or slitPlane_def — there are lemmas `Complex.mem_slitPlane_iff : z ∈ slitPlane ↔ 0 < z.re ∨ z.im ≠ 0` ✓ I think.\n- E4: remainder bound: ‖∫₀ⁿ deriv f · B1‖ ≤ ∫₀ⁿ ‖deriv f x‖·(1/2) dx ≤ (1/2)∫₀ⁿ ((x + w.re)² + (im w)²)⁻¹ dx ≤ (1/2)(π/|im w|) ≤ π/4.\n  - deriv f x = −(w + ↑x)⁻²: deriv (fun x => (w + ↑x)⁻¹) x = −(w+↑x)⁻² · deriv(w + ↑x) = −(w+x)⁻² · 1: via HasDerivAt: hasDerivAt_inverse? `HasDerivAt.inv (hf : HasDerivAt f f' x) (hx : f x ≠ 0) : HasDerivAt (fun x => (f x)⁻¹) (−f' / (f x)^2) x` ✓ hmm: HasDerivAt.inv : HasDerivAt (f⁻¹) (−(f x)^2)⁻¹ * f'... exact form: `HasDerivAt.inv (hf : HasDerivAt f f' x) (hnz : f x ≠ 0) : HasDerivAt f⁻¹ (-(f x ^ 2)⁻¹ * f') x`? roughly. Or use `hasDerivAt_inv`? Hmm. There's `HasDerivAt.inv`. The derivative value: −(w+x)⁻². Fine — I only need deriv f x = −(w+x)⁻² for the norm bound; ‖deriv f x‖ = ‖w+x‖⁻² ✓.\n  - ‖B1 x‖ ≤ 1/2 (abs_B1_le_half, needs 0 ≤ x ✓ on [0, n]).\n  - norm integral ≤ integral of norm: `intervalIntegral.norm_integral_le_integral_norm (h : a ≤ b)` ✓.\n  - ((x + w.re)² + (im w)²)⁻¹ = ‖w + ↑x‖⁻²: ‖w + x‖² = (w.re + x)² + (w.im)² via normSq: Complex.normSq (w + ↑x) = (w.re + x)² + w.im² (normSq_apply, add_re, ofReal_re...). And ‖z‖⁻² = (normSq z)⁻¹: `Complex.normSq_eq_norm_sq : normSq z = ‖z‖^2` ✓ (used in LiDisc). So ‖w+x‖⁻² = ((w.re+x)² + w.im²)⁻¹ ✓.\n  - ∫₀ⁿ ((x + a)² + c²)⁻¹ dx ≤ π/c where c = |im w| > 0:\n    First: ∫ (x:ℝ), ((x+a)² + c²)⁻¹ dx = π/c:\n    - translation: ∫ f(x+a) = ∫ f: `MeasureTheory.integral_comp_add_right (f : ℝ → E) (a : ℝ) : ∫ x, f (x + a) ∂μ = ∫ x, f ∂μ`? I believe `MeasureTheory.integral_comp_add_right` exists for Haar measure on ℝ. \n    - then ∫ (x² + c²)⁻¹ dx = (1/c) ∫ ((x/c)² + 1)⁻¹ dx = (1/c)·c·∫ (y²+1)⁻¹ dy = π/c hmm: 1/(x²+c²) = (1/c²)/((x/c)² + 1): sub y = x/c: dx = c dy: ∫ (1/c²)/(y²+1) · c dy = (1/c)·π.\n    In Lean: `MeasureTheory.integral_comp_div (f : ℝ → E) (c : ℝ) : ∫ x, f (x / c) = |c| * ∫ x, f x`? hmm there's `integral_comp_div` in Mathlib (Haar measure scaling): `MeasureTheory.integral_comp_div (f : ℝ → E) (d : ℝ) : ∫ x, f (x / d) = |d|⁻¹... ` no wait: ∫ f(x/d) dx = |d| ∫ f(y) dy. I recall `MeasureTheory.integral_comp_div : ∫ x, f (x / d) = |d| * ∫ x, f x`? Need to check names. And the base: `integral_one_div_one_add_sq : ∫ x : ℝ, (1 + x^2)⁻¹ = Real.pi`? or `∫ x, 1/(1 + x^2) = π`: grep.\n    Alternatively — AVOID the exact π evaluation: I just need an absolute constant! ∫₀ⁿ ((x+a)²+c²)⁻¹ dx ≤ ∫_ℝ ((x+a)²+c²)⁻¹ dx = π/c. Any bound like ≤ 4/c would do (constant folds into C). Even simpler: bound by arctan FTC? The antiderivative of 1/(x²+c²) is (1/c)arctan(x/c): ∫₀ⁿ = (1/c)(arctan((n+a)/c) − arctan(a/c)) ≤ (1/c)(π/2 + π/2) = π/c — using |arctan| ≤ π/2 (Real.abs_arctan_le_pi_div_two? `Real.arctan_le_pi_div_two`/`neg_pi_div_two_le_arctan` — exist). FTC for real functions is easier than the full-line integral! `intervalIntegral.integral_deriv_eq_sub`? or integral_eq_sub_of_hasDerivAt with HasDerivAt (fun x => (1/c) arctan((x+a)/c)) (1/((x+a)²+c²))... deriv arctan: `Real.hasDerivAt_arctan : HasDerivAt arctan (1/(1+x²)) x` ✓ exists. Chain: (1/c)·1/(1+((x+a)/c)²)·(1/c) = 1/(c²(1 + (x+a)²/c²)) = 1/(c² + (x+a)²) ✓. This avoids translation/scaling integral lemmas entirely — just real FTC + arctan range. \n    So: ∫₀ⁿ ((x+a)²+c²)⁻¹ dx = (1/c)(arctan((n+a)/c) − arctan(a/c)) ≤ (1/c)·π (arctan difference ≤ π: each |arctan| < π/2: `Real.arctan_lt_pi_div_two`, `Real.neg_pi_div_two_lt_arctan` — check names; abs_arctan_lt_pi_div_two? there's `Real.abs_arctan_lt_pi_div_two`? hmm — I'll find them). Then ≤ π/c ≤ π/2 (c ≥ 2).\n    Wait — even better: this gives the remainder ≤ (1/2)·(π/c) ≤ π/4 with c ≥ 2 ✓.\n  - So the EM-remainder ≤ (1/2)·(π/2) = π/4.\n  Boundary terms: ‖(f 0 − f n)/2‖ ≤ (1/2)(‖w‖⁻¹ + ‖w+n‖⁻¹) ≤ (1/2)(1/2 + 1/2) = 1/2 (‖w‖ ≥ |im w| ≥ 2, ‖w+n‖ ≥ |im| ≥ 2).\n- E5: StirlingVert at v = w + n: ‖ψ(v) − log v + 1/(2v)‖ ≤ 3/(im v)² ≤ 3/4 (|im v| ≥ 2); ‖ψ(v) − log v‖ ≤ 3/4 + ‖1/(2v)‖ ≤ 3/4 + 1/4 = 1.\n- E6: assemble: ψ(w) − log w = [ψ(v) − log v] + [log v − log w − Σ_j f j] where v = w + n:\n  = [ψ(v) − log v] − [Σ_j f j − (log v − log w)]\n  and Σ_j f j − (log v − log w) = (f 0 − f n)/2 + ∫ f′B1 (from E2/E3) with norm ≤ 1/2 + π/4.\n  Total: ‖ψ(w) − log w‖ ≤ 1 + 1/2 + π/4 ≤ 3 (π/4 ≤ 1: Real.pi_lt_315 or π < 4; 1 + 1/2 + 1 = 2.5 ≤ 3 ✓). State constant 3. Hmm — wait, but there's a subtlety: log v − log w = log(w + n) − log w as COMPLEX logs — from the FTC integral equality, exact ✓ (no branch issue since it's the FTC value directly).\n\nAlso need: w ≠ 0 and w + j ≠ 0 for the inverses — all from |im| ≥ 2 ⟹ im ≠ 0 ✓. And w+n ≠ 0 ✓.\n\nFor E1's digamma shift: hypothesis of digamma_apply_add_one: ∀ m : ℕ, (w + j) ≠ −↑m: since im(w + j) = im w ≠ 0 and −↑m is real (im = 0) ✓.\n\nPiece E is self-contained modulo the EM lemma and FTC — no dependence on A–D. Estimated 300–400 lines.\n\nHmm wait — one more consideration for E: the EM lemma `sum_eq_integral_add_integral_deriv` signature: f : ℝ → 𝕜 with 𝕜 : Type [RCLike 𝕜]? Let me check the context variables of EulerMaclaurin.lean (the `variable` line). It said `integral_deriv_mul_add_const (c : 𝕜) ...` with RCLike.ofRealCLM — so 𝕜 is RCLike. f : ℝ → ℂ with 𝕜 = ℂ ✓.\n\nB1 x for x ≥ 0: `b1_eq_fract_sub_half` is in OUR LiRBound (line 95) — and B1 0: fract 0 = 0 ⟹ B1 0 = −1/2 ✓; B1 ↑n: fract ↑n = 0 (`Int.fract_natCast` : Int.fract (↑n) = 0? name check; there's `Int.fract_natCast_eq_zero`? or via Int.fract_eq_iff... I'll find it).\n\nNow, where to put the code: new file `NguyenRH1/LiReflect.lean`, imported by the root after LiDisc. Wait — freeze protocol: \"no edits to existing Lean proofs except the liCoeff correctness fix\" — adding a new file + root import is the established pattern (LiDisc was added the same way in session 024). ✓\n\nImports for LiReflect: `import NguyenRH1.LiDisc` (gets Mathlib, StrongPNTPrefix, LiRBound, LiContour transitively) + `import Zeta23.GammaFacts.StirlingVert`? LiContour probably imports some GammaFacts — LiDisc gets digamma stuff? The digamma_stirling is Zeta23.StirlingVert.digamma_stirling — need the import. Check what LiContour/LiDigamma import: LiDigamma surely imports GammaFacts stuff. Simplest: `import NguyenRH1.LiDisc` + `import Zeta23.GammaFacts.StirlingVert` + `import Zeta23.RvM.GammaSide` (logDeriv_Gammaℝ) + `import Zeta23.WeilEF.XiLogDeriv`? Hmm — LiSides or LiContour may already import GammaSide/XiLogDeriv. Actually since everything is built, extra imports are free (already-compiled deps). I'll add what I need.\n\nAlso need `Zeta23.ZetaReflect` for analyticOrderAt_zeta_one_sub — check it's importable (it imports Statement etc. ✓).\n\nAnd differentiableAt_Gammaℝ_of_im_ne_zero is in Zeta23/XiPrime/Hardy/Basic.lean — that's a heavy import? It's in the XiPrime subtree; importing Zeta23.XiPrime.Hardy.Basic might pull a lot. Alternatively use differentiableAt_Gammaℝ (WeilEF/XiLogDeriv, needs re > 0) for the (s+4)/(1−s) points and for the POINT s itself: s with im ≠ 0. Where do I need ΓR differentiability at s exactly? In B2 (logDeriv_mul at s: ΓR * ζ). Hmm. Options: (a) import XiPrime.Hardy.Basic (heavy but already built — check its imports; it's part of the 9010-job build so no rebuild cost, just import time); (b) prove a local copy: ΓR = π^{−s/2}Γ(s/2), differentiable at s with s/2 ∉ {0,−1,−2,...}: Complex.differentiableAt_Gamma? Does Mathlib have `Complex.differentiableAt_Gamma (s : ℂ) (hs : ∀ m : ℕ, s ≠ -m)`? Let me check — in Mathlib/Analysis/SpecialFunctions/Gamma/Basic or Analytic: `Complex.differentiableAt_Gamma`? I saw in the digamma file: `hasDerivAt_Gamma_one_half`, `deriv_Gamma_add_one`, `Gamma_ne_zero hs`... The differentiability of Complex.Gamma: search \"differentiableAt_Gamma\\b\".\n\nLet me check both: Mathlib differentiableAt_Gamma and what XiPrime.Hardy.Basic's differentiableAt_Gammaℝ_of_im_ne_zero proof uses (maybe it's cheap to inline).\n\nAlso check `Complex.Gammaℝ_def : Gammaℝ s = π ^ (-s/2) * Gamma (s/2)` — used in logDeriv_Gammaℝ proof ✓ (from the grep snippet: `Complex.Gammaℝ_def`).\n\nAnd `Complex.Gamma_add_one (s : ℂ) (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s` — exact name `Complex.Gamma_add_one`. From digamma_apply_add_one's proof: `Gamma_add_one s hs0` ✓ (inside namespace Complex).\n\nLet me also double check `completedRiemannZeta_one_sub` in Mathlib: `completedRiemannZeta_one_sub (s : ℂ) : completedRiemannZeta (1 - s) = completedRiemannZeta s` ✓ (D-067 verified).\n\n`differentiableAt_completedZeta (hs₀ : s ≠ 0) (hs₁ : s ≠ 1)` — from CountByIntegral usage ✓.\n\nOK. Remaining greps: differentiableAt_Gamma in Mathlib; Complex.Gammaℝ_ne_zero_of_re_pos exact namespace (used as Complex.Gammaℝ_ne_zero_of_re_pos in Zeta23 — so `Complex.Gammaℝ_ne_zero_of_re_pos`); Gammaℝ_eq_zero_iff namespace (Complex.); Nat.ceil APIs (Nat.le_ceil : x ≤ ⌈x⌉₊? `Nat.le_ceil (a : α) : a ≤ ⌈a⌉₊` for linear ordered semiring... for ℝ: Nat.le_ceil ✓); Finset.sum_Ioc_eq_sum_range; Real.arctan bounds; interval integral norm lemma names.\n\nLet me also reconsider E4's per-term FTC: ∫₀ⁿ deriv-with-B1: I need IntervalIntegrable of (deriv f · B1) on 0..n — provided by Zeta23's `intervalIntegrable_deriv_mul_B1` (needs ContinuousOn deriv f [[0,n]]) ✓ and sum_eq_integral_add_integral_deriv needs hf_diff on Icc + h_cont ContinuousOn deriv f [[a,b]] — for f x = (w + ↑x)⁻¹: deriv f x = −(w+↑x)⁻² continuous on any set since w + ↑x ≠ 0 (im ≠ 0) ✓: ContinuousOn (fun x => −(w+↑x)⁻²): continuous_inv₀? Complex: ContinuousAt (fun x => (w + ↑x)⁻¹) via ContinuousAt.inv₀ (continuousAt_const.add continuousAt_ofReal...) hmm ofReal: `Complex.continuous_ofReal.continuousAt`. Fine, standard.\n\nOne subtle thing: in E2, sum_eq_integral_add_integral_deriv sums over Ioc ⌊0⌋ ⌊n⌋ = Ioc 0 n — the summand is f ↑k = (w + ↑k)⁻¹ ✓ matches E1's Σ_{j ∈ range n} (w + ↑j)⁻¹ after the shift reindex.\n\nAlso for E1 induction: digamma (w + ↑(j+1)) = digamma (w + ↑j + 1) = digamma (w + ↑j) + (w + ↑j)⁻¹ — need w + ↑j + 1 = w + ↑(j+1) (push_cast, ring) ✓.\n\nNow, let me also confirm what `B1` is called (Zeta23.FromPNTPlus namespace? In EulerMaclaurin.lean, inside namespace — check: the file has `namespace`? It used `B1` unqualified in LiRBound (`b1_eq_fract_sub_half : B1 x = ...`), and LiRBound imports what? LiRBound line 95 uses B1 directly with `open Zeta23`? Let me check LiRBound's header imports and opens. And the EulerMaclaurin namespace.\n\nAlso for §5 E3's FTC: `intervalIntegral.integral_eq_sub_of_hasDerivAt (hf : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x) (hi : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b - f a` ✓ exists in Mathlib (intervalIntegral.integral_eq_sub_of_hasDerivAt).\n\nAlright — also Piece A1: Gammaℝ_eq_zero_iff: `Complex.Gammaℝ_eq_zero_iff : Gammaℝ s = 0 ↔ ∃ n : ℕ, s = -2 * n` — from zeroDisc_isNontrivial usage: `rw [Complex.Gammaℝ_eq_zero_iff] at hG; obtain ⟨n, hn⟩ := hG` with hn : s = −2*↑n presumably ✓.\n\nLet me do the final round of API checks, then start writing the file. Actually — one more important check: the exact statement of `logDeriv_Gammaℝ` requires 0 < s.re; at (1−s) we have re ∈ [1/2, 7/2] ✓; at (s+4): re ∈ [3/2, 9/2] ✓. Good.\n\nAnd check: `Complex.Gammaℝ_ne_zero_of_re_pos (hs : 0 < s.re) : Gammaℝ s ≠ 0` ✓ (used in ZetaReflect/CountByIntegral).\n\nLet me also plan the file structure:\n\n```\nNguyenRH1/LiReflect.lean — ii′-5d\n§0 setup/imports\n§1 ΓR shift machinery (Piece A)\n  - gammaR_shift_four (pointwise identity on im ≠ 0)  \n  - logDeriv_gammaR_sub_shift (A3)\n  - logDeriv_gammaR_eq_digamma (A4, im ≠ 0 version)  [maybe not needed if bracket keeps (s+4)/2 form — skip? The bracket uses A3 + logDeriv_Gammaℝ directly. A4 = combining with digamma recurrence: not needed for the main theorem! SKIP A4 unless cheap. Actually wait — do I need the digamma recurrence at all for the MAIN theorem? No! The bracket bound uses ψ((s+4)/2) directly. The recurrence is only needed if I wanted the ψ(s/2) form. So digamma_apply_add_one is only needed in Piece E (the left-plane bound).]\n§2 Λ logDeriv split + FE identity (Piece B)\n  - completedZeta_eventuallyEq (B1)\n  - logDeriv_completedZeta (B2)\n  - logDeriv_completedZeta_one_sub_neg (B3)\n  - riemannZeta_one_sub_ne_zero (B5)\n  - logDeriv_zeta_fe (B4): the FE logDeriv identity\n§3 Sum reflection (Piece C): C1–C5\n§4 Bracket bound (Piece D): D1–D5\n§5 Left-half R-bound capstone\n§6 Left-plane digamma bound (Piece E)\n```\n\nOrder note: E is independent; could do first to warm up or last. I'll write §1–§5 first (the capstone), get it green, then §6.\n\nLet me now check the remaining API names in one grep round, then write §1.\n\nChecks:\n1. EulerMaclaurin namespace/B1 qualification.\n2. LiRBound header (imports, opens).\n3. Mathlib differentiableAt_Gamma.\n4. Finset.sum_Ioc_eq_sum_range.\n5. Real arctan bound names.\n6. intervalIntegral.integral_eq_sub_of_hasDerivAt exact name.\n7. Nat.le_ceil.\n8. Int.fract of nat = 0 name.\n9. Complex.mem_slitPlane_iff.\n10. Complex.log_re / log_im / abs_arg_le_pi / norm_le_abs_re_add_abs_im.","signature":""},{"type":"text","text":"All key APIs exist. Final round of signature checks, then I'll write the file."},{"type":"tool_use","id":"Bash_25","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean && sed -n '1,30p' Zeta23/FromPNTPlus/EulerMaclaurin.lean && echo === && sed -n '1,37p' ../lean/NguyenRH1/NguyenRH1/LiRBound.lean","description":"Check EulerMaclaurin namespace and LiRBound header"},"extra_content":null},{"type":"tool_use","id":"Bash_26","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"theorem differentiableAt_Gamma\\b\\|lemma differentiableAt_Gamma\\b\" Mathlib/ | head -2; grep -rn \"sum_Ioc_eq_sum_range\" Mathlib/Algebra/BigOperators/ | head -2; grep -rn \"integral_eq_sub_of_hasDerivAt\\b\" Mathlib/MeasureTheory/Integral/IntervalIntegral.lean Mathlib/Analysis/Calculus/FTC*.lean 2>/dev/null | head -3; grep -rn \"arctan_le_pi_div_two\\|neg_pi_div_two_le_arctan\\|abs_arctan\" Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan*.lean Mathlib/Analysis/SpecialFunctions/Trigonometric/*.lean 2>/dev/null | head -5","description":"Check Mathlib differentiableAt_Gamma, sum reindex, FTC, arctan bounds"},"extra_content":null}]