[{"type":"thinking","thinking":"- `Zeta23.differentiableAt_Gammaℝ_of_im_ne_zero` — cheap proof via Gammaℝ_def + differentiableAt_Gamma. It lives in XiPrime/Hardy/Basic.lean which imports a big subtree. Rather than importing that heavy module, I can copy the 8-line proof into my file (it's a trivial composition). Also `isOpen_im_ne_zero` — one line. And `half_ne_neg_nat`: `s/2 ≠ -m` from im ≠ 0 — check where that lives (same file presumably): `half_ne_neg_nat (hs : s.im ≠ 0) : ∀ m : ℕ, s / 2 ≠ -m`? Let me not bother; inline: if s/2 = −m then im(s/2) = 0 but im(s/2) = (im s)/2 ≠ 0. Fine.\n\n- `Real.arctan_lt_pi_div_two (x) : arctan x < π/2` ✓; presumably `Real.neg_pi_div_two_lt_arctan` also exists — the grep didn't show it but let me assume `Real.neg_pi_div_two_lt_arctan (x) : -(π/2) < arctan x` — check at build; else derive from arctan neg: arctan (−x) = −arctan x (Real.arctan_neg).\n\n- sum_Ioc_eq_sum_range didn't appear. Alternatives: `Finset.sum_Ioc_eq_sum_range` might not exist in this Mathlib. I can reindex differently: Ioc 0 n = range(n+1) \\ {0}... or `Finset.sum_range_succ_comm`? Simplest robust approach: Σ_{k ∈ Ioc 0 n} f k = Σ_{j ∈ range n} f (j+1): via Finset.sum_bij with i : k ↦ k − 1... Or: Ioc 0 n = (range (n+1)).erase 0? There's `Finset.Icc_eq_range'`... `Finset.Ioc 0 n = (Finset.range (n+1)).erase 0`: `Finset.Ioc_zero_eq_range'`? hmm. There IS `Finset.sum_range_succ_sub_sum`? Let me think of the cleanest: I want Σ_{j=0}^{n−1} f j in terms of Σ_{k ∈ Ioc 0 n} f k = Σ_{k=1}^{n} f k. Σ_{j ∈ range n} f j = Σ_{j ∈ range (n+1)} f j + f 0 − f n − ... hmm: range (n+1) = {0,...,n} = insert 0 (Ioc 0 n) for n ≥ 0: `Finset.range_succ` : range (n+1) = insert n (range n). And Ioc 0 n = range(n+1) \\ {0}: `Finset.Ioc_zero_eq_range'`? I recall `Finset.range_eq_Ico : range n = Ico 0 n` ✓ exists. Ico 0 (n+1) = insert 0 (Ioc 0 n): `Finset.Ico_zero_eq_range`... and `Finset.Ico_succ_left_eq_insert_Ioc`? Something like Ico_insert_succ_left... There is `Finset.Ico_insert_succ_left (h : a ≤ b) : insert a (Ico (a+1) b) = Ico a b`? hmm names: `Finset.Ico_insert_succ_left : insert a (Ico (a + 1) b) = Ico a b` for a < b? Roughly. With Ico 0 (n+1) and 0 < n+1: insert 0 (Ico 1 (n+1)) = Ico 0 (n+1); Ico 1 (n+1) = Ioc 0 n: `Finset.Ioc_eq_Ico`? Ioc a b = Ico (a+1) (b+1): `Finset.Ioc_eq_Ico_succ_succ`? hmm. Honestly the most robust: prove Σ_{j ∈ range n} f j = Σ_{k ∈ Ioc 0 n} f k + f 0 − f n via:\n  range n = Ico 0 n (range_eq_Ico); Ico 0 n = insert 0 (Ico 1 n) [Finset.Ico_insert_succ_left? for 0 < n... wait Ico_insert_succ_left : a ≤ b → insert a (Ico (a+1) b) = Ico a b? check direction]; Ico 1 n = Ioc 0 n [Finset.Ioc 0 n: Ioc a b = {x | a < x ≤ b}; Ico 1 n = {1 ≤ x < n+1}... for naturals 1 ≤ x ↔ 0 < x and x < n+1 ↔ x ≤ n ✓ so equal: ext + omega, or existing lemma `Finset.Ico_succ_right`? Ico 1 n vs Ioc 0 n: `Finset.Ico_eq_Ioc`? I recall `Finset.Ico_succ_left_eq_Ioc : Ico (a+1) b = Ioc a b`? something. There IS `Finset.Ico_succ_right : Ico a (b+1) = Ioc (a−1)...` hmm I don't remember exactly. The fallback: prove set equality by `ext x; simp [Finset.mem_Ico, Finset.mem_Ioc]; omega` — totally robust. Then sum over insert.\n  \n  Alternatively skip Ioc entirely: apply the EM lemma with a = 0, b = n and then convert. OR use a = 1, b = n+1?? Same issue.\n  \n  OK: `Ioc 0 n = (range (n+1)).erase 0`: ext x: mem_Ioc: 0 < x ∧ x ≤ n; mem (range (n+1)).erase 0: x ≠ 0 ∧ x < n+1 — omega ✓. Then Σ over erase: sum_erase (needs 0 ∈ range (n+1), i.e., 0 < n+1 ✓): Σ_{range(n+1)} f − f 0. And Σ_{range (n+1)} f = Σ_{range n} f + f n (sum_range_succ). So Σ_{Ioc 0 n} f k = Σ_{range n} f j + f n − f 0 ⟹ Σ_{range n} f j = Σ_{Ioc} − f n + f 0. Combine with EM — all elementary algebra.\n\nFine. Now — one more thing to verify: `Complex.Gammaℝ_ne_zero_of_re_pos` exact name and `Gammaℝ_ne_zero_of_im_ne_zero` (the first lemma in the snippet above line 55 shows a proof of Gammaℝ_ne_zero from im ≠ 0 — the lemma right before differentiableAt_Gammaℝ_of_im_ne_zero; its name is cut off — probably `Gammaℝ_ne_zero_of_im_ne_zero` in the same file). Since I want to avoid importing XiPrime.Hardy.Basic, I'll write my own one-liner: Gammaℝ s ≠ 0 from Gammaℝ_eq_zero_iff: if = 0 then s = −2n real ⟹ im = 0 contra.\n\nAlso check `Complex.Gammaℝ_eq_zero_iff` exact form — from zeroDisc_isNontrivial: `rw [Complex.Gammaℝ_eq_zero_iff] at hG; obtain ⟨n, hn⟩ := hG` then `rw [hn]` and `simp [neg_re, mul_re]` gave ρ.re = −2n — so hn : ρ = −2 * ↑n ✓.\n\nNow the Λ = ΓR * ζ EventuallyEq needs ΓR ≠ 0 in a nbhd of s: ContinuousAt ΓR s (from differentiableAt) .eventually_ne? Hmm — is there `ContinuousAt.eventually_ne`? I recall `ContinuousAt.eventually_ne (hf : ContinuousAt f x) (h : f x ≠ 0) : ∀ᶠ y in 𝓝 x, f y ≠ 0`? Hmm, might be `ContinuousAt.eventually_ne` in Mathlib.Topology.Basic or Algebra/Group: there's `ContinuousAt.eventually_ne` — yes I'm fairly confident (used for inverses). Alternatively: {z | Gammaℝ z ≠ 0} ∈ 𝓝 s via (isOpen_ne.preimage continuous).mem_nhds — continuous ΓR: need `Continuous Gammaℝ`? ΓR is not continuous at poles... continuousAt at s suffices: `ContinuousAt.preimage_mem_nhds`? For Eventually: (h.continuousAt...). Let me just: have hc : ContinuousAt Gammaℝ s := (differentiableAt_...).continuousAt; have : ∀ᶠ z in 𝓝 s, Gammaℝ z ≠ 0 := hc.eventually_ne hΓ — if eventually_ne doesn't exist: `hc.eventually (isOpen_compl_singleton.preimage ...).mem_nhds`... I'll figure at build; fallback: tendsto: hc : Tendsto ΓR (𝓝 s) (𝓝 (ΓR s)); (𝓝 (ΓR s)) contains {0}ᶜ since ΓR s ≠ 0: `tendsto_nhds.mp hc _ (isOpen_compl_singleton)...` or `hc (isOpen_compl_singleton.mem_nhds hΓ)` : {z | ΓR z ∈ {0}ᶜ} ∈ 𝓝 s — that IS ∀ᶠ z, ΓR z ≠ 0 (mem_compl_iff). Robust: `Filter.Tendsto.eventually`? `(hc.tendsto...)`. Fine, multiple routes.\n\nAlso the s ≠ 0 nbhd: isOpen_compl_singleton.mem_nhds hs0 : {0}ᶜ ∈ 𝓝 s; i.e. ∀ᶠ z, z ≠ 0 ✓.\n\nNow B3's deriv of (1 − ·): `HasDerivAt.const_sub (c : ℂ) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c - f x) (-f') x` ✓ exists I'm confident.\n\nLogDeriv congr lemma: `Filter.EventuallyEq.deriv_eq (h : f =ᶠ[𝓝 x] g) : deriv f x = deriv g x` ✓ (journal-024 banked). And `Filter.EventuallyEq.eq_of_nhds (h : f =ᶠ[𝓝 x] g) : f x = g x` ✓ (journal-024 banked). So:\n```\ntheorem logDeriv_congr {f g : ℂ → ℂ} {x : ℂ} (h : f =ᶠ[𝓝 x] g) : logDeriv f x = logDeriv g x := by\n  simp only [logDeriv_apply, h.deriv_eq, h.eq_of_nhds]\n```\nWait — `logDeriv_apply : logDeriv f x = deriv f x / f x` ✓ (used in logDeriv_mul's proof: simp [logDeriv_apply]). \n\nNow let me also double-check `completedRiemannZeta_one_sub` exact name in Mathlib: `completedRiemannZeta_one_sub (s : ℂ) : completedRiemannZeta (1 - s) = completedRiemannZeta s` — grep to confirm.\n\nAlso `differentiableAt_completedZeta`: from CountByIntegral: `differentiableAt_completedZeta hz.1 hz.2` with hz.1 : z ≠ 0, hz.2 : z ≠ 1 — so `differentiableAt_completedZeta (h0 : s ≠ 0) (h1 : s ≠ 1) : DifferentiableAt ℂ completedRiemannZeta s` ✓.\n\nAlso `differentiableAt_riemannZeta (hs : s ≠ 1)` ✓ (used in ZetaReflect).\n\nOne more: for the 5c application I need `logDeriv_riemannZeta_sub_nearZeros_le` with t := −t: hypothesis 10 ≤ |−t| = |t| ✓ abs_neg.\n\nLet me also confirm `Complex.norm_le_abs_re_add_abs_im` exists (used it in LiDisc? journal says normSq chains used; let me grep quickly) — `Complex.norm_le_abs_re_add_abs_im (z : ℂ) : ‖z‖ ≤ |z.re| + |z.im|` ✓ I'm confident it exists.\n\n`Complex.abs_im_le_norm (z) : |z.im| ≤ ‖z‖` ✓ (used in StirlingVert: Complex.abs_im_le_norm w).\n\nOK — also the assembly needs: log|−t| = log|t| (abs_neg inside Real.log: Real.log |−t| — rw [abs_neg] — the 5c conclusion at −t gives 100000 * (Real.log |−t|)^2; rw abs_neg to match).\n\nNow write the file. Plan the sections and decl names:\n\n```\nNguyenRH1/LiReflect.lean — ii′-5d\n\nimport Mathlib\nimport Zeta23.FromPNTPlus.StrongPNTPrefix  (via LiDisc anyway)\nimport Zeta23.RvM.GammaSide          -- logDeriv_Gammaℝ\nimport Zeta23.GammaFacts.StirlingVert -- digamma_stirling\nimport Zeta23.ZetaReflect            -- analyticOrderAt_zeta_one_sub\nimport NguyenRH1.LiDisc\n\nopen Zeta23 Complex Filter Topology MeasureTheory\nopen scoped Nat\nnoncomputable section\nnamespace NguyenRH1\n\n§1 helpers:\n- Gammaℝ_ne_zero_of_im_ne_zero {s} (hs : s.im ≠ 0) : Gammaℝ s ≠ 0\n- differentiableAt_Gammaℝ_of_im_ne_zero' — copy (or just import XiPrime.Hardy.Basic? it's heavy; copy the 8 lines, renaming to avoid clash if LiDigamma or something already imports Hardy.Basic transitively — CHECK: does LiDisc import anything importing XiPrime.Hardy.Basic? LiContour imports? LiSides? Probably not. But Zeta23.ZetaReflect imports only Statement + Mathlib. RvM.GammaSide imports? Let me be careful with name clashes: if I define `differentiableAt_Gammaℝ_of_im_ne_zero` in namespace NguyenRH1, no clash with Zeta23's (different namespace). ✓ But if some import chain pulls in Hardy.Basic, my local def in NguyenRH1 namespace shadows nothing. Fine.)\n  Actually simpler: just prove differentiableAt at the specific points I need inline via Gammaℝ_def composition — no wait, I need it at s (arbitrary with im ≠ 0) in B2. So one local lemma it is.\n\n§1 A: \n- gammaR_shift (s : ℂ) (hs : s.im ≠ 0) : Gammaℝ s = (Real.pi : ℂ)^2 * Gammaℝ (s+4) / ((s/2)*(s/2+1))\n   proof: field_simp-ish via the recurrence; or prove the ratio form:\n   Gammaℝ (s+4) = (Real.pi:ℂ)^(-2:ℝ) * ((s/2)*(s/2+1)) * Gammaℝ s, then divide.\n   Steps: Gammaℝ (s+4) = π^{−(s+4)/2} Γ((s+4)/2) [Gammaℝ_def]\n   (s+4)/2 = s/2 + 2 [ring]\n   Γ(s/2+2) = (s/2+1)*Γ(s/2+1) [Complex.Gamma_add_one (s/2+1 ≠ 0)]; s/2+1 ≠ 0: if = 0 then im = 0: (s/2+1).im = s.im/2 ≠ 0 ✓\n   Γ(s/2+1) = (s/2)*Γ(s/2) [Gamma_add_one (s/2 ≠ 0: s ≠ 0 from im ≠ 0)]\n   π^{−(s+4)/2} = π^{−s/2} * π^{−2}: cpow: write (π:ℂ)^(w) = exp (↑(Real.log π) * w) [Complex.cpow_def_of_ne_zero? check name: `Complex.cpow_def_of_ne_zero (x : ℂ) (hx : x ≠ 0) (y : ℂ) : x ^ y = exp (log x * y)`? I believe signature is cpow_def_of_ne_zero (hx : x ≠ 0) (y) : x^y = exp (log x * y). Hmm or (x y : ℂ) (hx : x ≠ 0)... check.] and Complex.log π-ofReal: `Complex.ofReal_log (hx : 0 ≤ x) : log ↑x = ↑(Real.log x)` ✓ I'm fairly sure.\n   Then exp(↑logπ * (−(s+4)/2)) = exp(↑logπ * (−s/2) + ↑(−2·logπ))... exp_add: exp(a + b) = exp a * exp b; exp(↑(−2 log π)) = ↑(Real.exp(−2 log π)) [Complex.ofReal_exp] = ↑(π^{−2}) [Real.exp_neg, Real.exp_nat_mul, Real.exp_log pi_pos]... then π^{−2} = (π^2)⁻¹ real rpow vs zpow vs pow: work with ((Real.pi^2 : ℝ) : ℂ)⁻¹: Real.exp (−2 * log π) = (π²)⁻¹: Real.exp (−2 * log π) = (Real.exp (log π))^(−2:ℤ)? Use: −2 * log π = log ((π²)⁻¹): Real.log_inv? log (π^{−2}) hmm: Real.log_inv : log x⁻¹ = −log x; Real.log_pow : log (x^n) = n log x. So log ((π^2)⁻¹) = −(2 log π) = −2 * log π ✓. Then Real.exp (−2 * log π) = Real.exp (log ((π²)⁻¹)) = (π²)⁻¹ [Real.exp_log (inv_pos.mpr (pow_pos pi_pos 2))] ✓ clean.\n   \n   So the π^{−(s+4)/2} = π^{−s/2}·(π²)⁻¹ identity:\n   (π:ℂ)^(−(s+4)/2) = exp (↑log π * (−(s+4)/2))\n   = exp (↑log π * (−s/2) + ↑(−2*log π))   [ring inside: ↑logπ * (−(s+4)/2) = ↑logπ*(−s/2) + ↑(−2*logπ): need ↑(−2*logπ) = ↑logπ * (−2): push_cast ring ✓]\n   = exp (↑log π * (−s/2)) * exp (↑(−2*log π)) [exp_add]\n   = (π:ℂ)^(−s/2) * ↑(π²)⁻¹ [← cpow_def_of_ne_zero backwards, ofReal_exp, the real identity]\n   \n   Then assemble Gammaℝ (s+4) = ↑((π²)⁻¹) * (s/2) * (s/2+1) * Gammaℝ s [mul comm/assoc + Gammaℝ_def].\n   And conclude Gammaℝ s = (π:ℂ)² * Gammaℝ (s+4) / ((s/2)*(s/2+1)): field_simp with (s/2) ≠ 0, (s/2+1) ≠ 0, π² ≠ 0; or: multiply both sides... Use: Gammaℝ s = Gammaℝ (s+4) / (↑(π²)⁻¹ * (s/2) * (s/2+1)) [eq_div_iff / div_eq_iff with the product ≠ 0] then simplify ↑((π²)⁻¹)⁻¹ = (π:ℂ)². Hmm — cleaner: from h : Gammaℝ (s+4) = C * P * Gammaℝ s with C = ↑(π²)⁻¹, P = (s/2)(s/2+1): Gammaℝ s = (C*P)⁻¹ * Gammaℝ (s+4) [by field_simp or: Gammaℝ s = (C*P)⁻¹ * (C*P) * Gammaℝ s = (C*P)⁻¹ * Gammaℝ(s+4) — via eq_of_mul_eq... let me just: have hC : C ≠ 0, hP : P ≠ 0; field_simp [h] ... Actually simplest robust: \n   calc Gammaℝ s = (C * P)⁻¹ * (C * P * Gammaℝ s) := by field_simp; ring\n     _ = (C*P)⁻¹ * Gammaℝ (s+4) := by rw [h]\n     _ = (π:ℂ)² * Gammaℝ (s+4) / P := by field_simp [hC, hP] — (↑(π²)⁻¹)⁻¹ = ↑(π²): inv_inv; and push_cast (π² : ℝ → ℂ) ✓.\n   Manageable.\n\n- logDeriv_Gammaℝ_shift {s : ℂ} (hs : s.im ≠ 0) :\n    logDeriv Gammaℝ s = logDeriv Gammaℝ (s + 4) - 2*(s+1)/(s*(s+2))\n  proof:\n  U := {z : ℂ | z.im ≠ 0} open (isOpen_ne_fun continuous_im continuous_const — from the Zeta23 snippet: isOpen_ne_fun Complex.continuous_im continuous_const ✓).\n  hEv : Gammaℝ =ᶠ[𝓝 s] fun z => (π:ℂ)² * Gammaℝ (z+4) / ((z/2)*(z/2+1)):\n    filter_upwards [U.mem_nhds hs... wait (hU.mem_nhds hs) : ∀ᶠ z in 𝓝 s, z ∈ U i.e. z.im ≠ 0] with z hz; exact gammaR_shift z hz.\n  logDeriv ΓR s = logDeriv (that) s [logDeriv_congr hEv]\n  = logDeriv (fun z => (π:ℂ)² * Gammaℝ (z+4)) s − logDeriv (fun z => (z/2)*(z/2+1)) s [logDeriv_div s hnum hden hdnum hdden]\n    hnum : (π:ℂ)² * Gammaℝ (s+4) ≠ 0: pi² ≠ 0 (cast; pow_ne_zero 2 (cast_ne_zero pi_ne_zero)), Gammaℝ (s+4) ≠ 0: re(s+4) — hmm! I need re(s+4) > 0 OR im(s+4) = im s ≠ 0 ⟹ Gammaℝ_ne_zero_of_im_ne_zero ✓ (don't need re). ✓\n    hden : (s/2)*(s/2+1) ≠ 0 ✓ both factors ≠ 0 (im arguments).\n    hdnum : DifferentiableAt ℂ (fun z => (π:ℂ)² * Gammaℝ (z+4)) s: const mul + (differentiableAt_Gammaℝ_of_im_ne_zero (im(s+4) = im s ≠ 0)).comp s (differentiableAt_id.add_const 4 → (fun z => z + 4): differentiableAt_id'.add_const? `DifferentiableAt.add_const (hf : DifferentiableAt 𝕜 f x) (c) : DifferentiableAt 𝕜 (fun x => f x + c) x` ✓).\n    hdden : poly differentiable ✓ (differentiableAt_id.div_const... (fun z => z/2): differentiableAt_id.div_const 2? hmm div_const exists for DifferentiableAt? `DifferentiableAt.div_const (hf) (c)` ✓; (fun z => z/2 + 1): .add_const ✓; .mul ✓).\n  logDeriv (fun z => (π:ℂ)² * Gammaℝ (z+4)) s = logDeriv (fun z => Gammaℝ (z+4)) s [logDeriv_const_mul s _ hpi2] \n  = deriv (fun z => Gammaℝ (z+4)) s / Gammaℝ (s+4) [logDeriv_apply]\n  deriv (fun z => Gammaℝ (z+4)) s = deriv Gammaℝ (s+4): HasDerivAt: (differentiableAt_Gammaℝ_of_im_ne_zero' ...).hasDerivAt.comp s ((hasDerivAt_id' s).add_const 4) : HasDerivAt (Gammaℝ ∘ fun z => z+4) (deriv Gammaℝ (s+4) * 1) s; .deriv gives deriv (Gammaℝ ∘ ·) s = deriv ΓR (s+4) * 1; mul_one; and (Gammaℝ ∘ fun z => z+4) = (fun z => Gammaℝ (z+4)) defeq via show or rfl.\n  So logDeriv (fun z => Gammaℝ (z+4)) s = deriv Gammaℝ (s+4) / Gammaℝ (s+4) = logDeriv Gammaℝ (s+4) [logDeriv_apply symm].\n  logDeriv (fun z => (z/2)*(z/2+1)) s = deriv (...) s / ((s/2)*(s/2+1)):\n    deriv: HasDerivAt: (hasDerivAt_id' s).div_const 2 → HasDerivAt (·/2) (1/2) s? `HasDerivAt.div_const (hf : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x / c) (f' / c) x` ✓. .add_const 1: (·/2+1) (1/2). .mul: HasDerivAt ((·/2)*(·/2+1)) ((1/2)*(s/2+1) + (s/2)*(1/2)) s [HasDerivAt.mul : (f*g)' = f'*g + f*g']. (1/2)*(s/2+1) + (s/2)*(1/2) = s/2 + 1/2 [ring].\n    Then (s/2 + 1/2) / ((s/2)*(s/2+1)) = 2*(s+1)/(s*(s+2)): field_simp with s ≠ 0 (im), s + 2 ≠ 0 (im(s+2) = im s ≠ 0): ring_nf to verify: LHS = (s/2+1/2)/((s/2)(s/2+1)); multiply num/den: (s+1)/2 / ((s/2)(s+2)/2)... (s/2+1) = (s+2)/2 so den = (s/2)((s+2)/2) = s(s+2)/4; num = (s+1)/2; ratio = (s+1)/2 * 4/(s(s+2)) = 2(s+1)/(s(s+2)) ✓. In Lean: field_simp [hs0, hs2]; ring.\n```\n\n§2 B:\n- completedZeta_eq_gammaR_mul_zeta_eventually {s} (hs0 : s ≠ 0) (hG : Gammaℝ s ≠ 0) (hcont : ContinuousAt Gammaℝ s): completedRiemannZeta =ᶠ[𝓝 s] fun z => Gammaℝ z * riemannZeta z\n- logDeriv_completedZeta_eq {s} (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hG : Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0) (hdG : DifferentiableAt ℂ Gammaℝ s):\n    logDeriv completedRiemannZeta s = logDeriv Gammaℝ s + logDeriv riemannZeta s\n  [logDeriv_congr + logDeriv_mul s hG hζ hdG (differentiableAt_riemannZeta hs1)]\n- logDeriv_completedZeta_one_sub {s} (hs0 : s ≠ 0) (hs1 : s ≠ 1) (h1s0 : 1 - s ≠ 0) (h1s1 : 1 - s ≠ 1):\n    logDeriv completedRiemannZeta s = - logDeriv completedRiemannZeta (1 - s)\n  [funext: (fun z => Λ (1 − z)) = Λ via funext fun z => completedRiemannZeta_one_sub z ✓;\n   deriv (fun z => Λ (1−z)) s = deriv Λ (1−s) * (−1): ((differentiableAt_completedZeta h1s0 h1s1).hasDerivAt.comp s ((hasDerivAt_const s 1).sub (hasDerivAt_id' s)))... HasDerivAt.const_sub (c) (hf : HasDerivAt f f' x) : HasDerivAt (fun x => c - f x) (-f') x ✓. So ((diff.hasDerivAt).comp s ((hasDerivAt_id' s).const_sub 1)) : HasDerivAt (Λ ∘ fun z => 1 − z) (deriv Λ (1−s) * −1) s; .deriv.\n   logDeriv Λ s = deriv Λ s / Λ s; rw the funext backwards: logDeriv Λ s = logDeriv (fun z => Λ (1−z)) s = deriv(...)/Λ(1−s) = deriv Λ (1−s) * −1 / Λ (1−s) = −(deriv Λ (1−s)/Λ (1−s)) = −logDeriv Λ (1−s) ✓.]\n- riemannZeta_one_sub_ne_zero_of {s} (hs0 : s ≠ 0) (hG : Gammaℝ s ≠ 0) (hζ : riemannZeta s ≠ 0) (h1s0 : 1 - s ≠ 0) (hG1 : Gammaℝ (1-s) ≠ 0): riemannZeta (1 - s) ≠ 0\n  [Λ(1−s) = Λ(s) = ΓR s * ζ s ≠ 0; Λ(1−s) = ΓR(1−s)*ζ(1−s); if ζ(1−s) = 0 then Λ(1−s) = 0 contra.]\n- logDeriv_zeta_one_sub_fe {s} (hs0, hs1, hG, hG1, hζ, hdG s, hdG (1−s)):\n    logDeriv riemannZeta s = -logDeriv riemannZeta (1-s) - (logDeriv Gammaℝ s + logDeriv Gammaℝ (1-s))\n  [from the three equations via linear_combination.]\n\n§3 C: (as planned)\n- riemannZeta_one_sub_eq_zero_of_nontrivial {ρ} (hρ : IsNontrivialZero ρ) : riemannZeta (1 - ρ) = 0\n- one_sub_mem_nearZeros_neg {t} {ρ} (hρ : ρ ∈ nearZeros t) : 1 - ρ ∈ nearZeros (-t)\n- nearZeros_neg_eq_image {t} : nearZeros (-t) = (nearZeros t).image (fun ρ => 1 - ρ)\n- zeroMult_one_sub {ρ} (h0 : 0 < ρ.re) (h1 : ρ.re < 1) : zeroMult (1 - ρ) = zeroMult ρ\n- sum_nearZeros_neg_reflect {t} {s : ℂ} : Σ ρ' ∈ nearZeros (-t), (zeroMult ρ' : ℂ)/(1 - s - ρ') = - Σ ρ ∈ nearZeros t, (zeroMult ρ : ℂ)/(s - ρ)\n\n§4 D:\n- Complex norm_log bound: norm_log_le {w : ℂ} (hw : w ≠ 0)... actually ‖log w‖ ≤ |Real.log ‖w‖| + π: no hw needed? log 0 = 0 junk: |log ‖0‖| = |log 0| = 0... Real.log 0 = 0, arg 0 = π? junk arg 0 = π? hmm — Complex.arg 0 = π by junk? arg 0 = π? Actually Complex.arg 0 = π I think (or 0). Doesn't matter; I'll take hw : 1 ≤ ‖w‖ so |Real.log ‖w‖| = Real.log ‖w‖ (log ≥ 0) — cleaner:\n  norm_log_le_of_one_le {w : ℂ} (hw : 1 ≤ ‖w‖) : ‖Complex.log w‖ ≤ Real.log ‖w‖ + Real.pi\n  [log w = ↑(Real.log ‖w‖) + ↑(arg w) * I? Complex.log_def: log z = ↑(Real.log ‖z‖) + ↑(arg z) * I? something: `Complex.log_def : log z = ↑(Real.log ‖z‖) + ↑(arg z) * I`? hmm — there's `Complex.log_re : (log z).re = Real.log ‖z‖` and `Complex.log_im : (log z).im = arg z`. Use: ‖log w‖ ≤ |(log w).re| + |(log w).im| [Complex.norm_le_abs_re_add_abs_im] = |Real.log ‖w‖| + |arg w| [congr] = Real.log ‖w‖ + |arg w| [abs_of_nonneg: Real.log ‖w‖ ≥ 0 from Real.log_nonneg hw] ≤ Real.log ‖w‖ + π [Complex.abs_arg_le_pi] ✓.]\n- norm_digamma_le {t} {w} (ht : 10 ≤ |t|) (hwre : 0 < w.re) (hwim : w.im = t/2 ∨ ... ) hmm — parametrize: (hwre : 0 < w.re) (hwim : |w.im| = |t|/2) (hwnorm : ‖w‖ ≤ 2*|t|): ‖digamma w‖ ≤ Real.log |t| + 5.\n  proof: ‖ψ w‖ = ‖(ψ w − log w + 1/(2w)) + log w − 1/(2w)‖ ≤ 3/(w.im)² + ‖log w‖ + 1/(2‖w‖):\n  |w.im| = |t|/2 ≥ 5: 3/(w.im)² = 3/(|t|/2)² = 12/|t|² ≤ 12/100 ≤ 1/8? Just bound ≤ 1 (12/100 < 1).\n  ‖w‖ ≥ |w.im| ≥ 5 ≥ 1: norm_log_le gives ‖log w‖ ≤ log ‖w‖ + π ≤ log (2|t|) + π = log 2 + log|t| + π [Real.log_mul (two_ne_zero) (abs pos... |t| ≠ 0)] ≤ log|t| + 4 (log 2 ≤ 1 via Real.log_two_lt_d9? there's `Real.log_two_lt_d9 : Real.log 2 < 0.6931471803`? and pi ≤ 3.15 via Real.pi_lt_315. So log 2 + π ≤ 0.7 + 3.15 = 3.85 ≤ 4 ✓ nlinarith with those two facts).\n  1/(2‖w‖) ≤ 1/10 ≤ 1.\n  Total: ≤ 1 + log|t| + 4 + 1 = log|t| + 6. State + 6 (avoid tightness). Actually let me recount: 3/(im)² ≤ 3/25 (im ≥ 5) = 0.12; 1/(2‖w‖) ≤ 1/10 = 0.1; log ≤ log|t| + 4; total ≤ log|t| + 4.22 ≤ log|t| + 5 ✓ state ≤ Real.log |t| + 5.\n- gammaR_bracket_norm_le {t} (ht : 10 ≤ |t|) {s} (hsim : s.im = t) (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 1/2):\n    ‖logDeriv Gammaℝ (1-s) + logDeriv Gammaℝ s‖ ≤ 4 * (Real.log |t|)^2\n  proof: \n  logDeriv ΓR (1−s) = −(logπ)/2 + ½ ψ((1−s)/2) [RvM.logDeriv_Gammaℝ — wait, namespace: Zeta23/RvM/GammaSide.lean line 65 theorem logDeriv_Gammaℝ {s} (hs : 0 < s.re) — namespace inside? The file: does it sit in namespace Zeta23.RvM? From the grep earlier \"RvM.logDeriv_Gammaℝ\" in D-067/STATE — STATE says \"RvM.logDeriv_Gammaℝ\". And LiDisc used RvM.completedRiemannZeta_eq_Gammaℝ_mul. So namespace Zeta23.RvM. With open Zeta23: RvM.logDeriv_Gammaℝ ✓. re(1−s) = 1 − s.re ≥ 1/2 > 0 ✓.]\n  logDeriv ΓR s = logDeriv ΓR (s+4) − 2(s+1)/(s(s+2)) [logDeriv_Gammaℝ_shift, im ≠ 0] = −(logπ)/2 + ½ψ((s+4)/2) − 2(s+1)/(s(s+2)) [logDeriv_Gammaℝ at s+4: re(s+4) = s.re + 4 ≥ 3/2 > 0 ✓].\n  Sum: = −log π + ½[ψ((1−s)/2) + ψ((s+4)/2)] − 2(s+1)/(s(s+2)).\n  norm ≤ log π + ½‖ψ w₁‖ + ½‖ψ w₂‖ + ‖2(s+1)/(s(s+2))‖:\n    w₁ = (1−s)/2: re ∈ [1/4, 7/4] > 0 ✓; im w₁ = −t/2, |im| = |t|/2 ✓; ‖w₁‖ ≤ (1 + ‖s‖)/2 ≤ (1 + 5/2 + |t|)/2 ≤ 2|t|/2·... need ‖w₁‖ ≤ 2|t|: ‖s‖ ≤ |s.re| + |s.im| ≤ 5/2 + |t| (norm_le_abs_re_add_abs_im; |s.re| ≤ 5/2: −5/2 ≤ re ≤ 1/2 ⟹ |re| ≤ 5/2 ✓; |s.im| = |t| ✓) ⟹ ‖w₁‖ ≤ (1 + 5/2 + |t|)/2 = 7/4 + |t|/2 ≤ |t| (7/4 ≤ |t|/2 ⟺ 3.5 ≤ |t| ✓) ≤ 2|t| ✓.\n    w₂ = (s+4)/2: re = (s.re+4)/2 ∈ [3/4, 9/4] > 0 ✓; im = t/2 ✓; ‖w₂‖ ≤ (‖s‖+4)/2 ≤ (5/2 + |t| + 4)/2 = 13/4 + |t|/2 ≤ |t| (13/4 = 3.25 ≤ 5 = |t|/2 ✓) ≤ 2|t| ✓.\n    Each ‖ψ‖ ≤ log|t| + 5 ✓ (D-norm_digamma_le).\n    rational ≤ 1 (as computed: ≤ 2.8/|t| ≤ 0.28 — implement: ‖2*(s+1)/(s*(s+2))‖ = 2‖s+1‖/(‖s‖‖s+2‖): ‖s‖ ≥ |im s| = |t| (abs_im_le_norm) ✓, ‖s+2‖ ≥ |im(s+2)| = |t| ✓, ‖s+1‖ ≤ ‖s‖+1 ≤ 5/2+|t|+1 = 7/2+|t| ≤ 1.35|t| (3.5 ≤ 0.35·10 ✓): 2·1.35|t|/(|t|²) = 2.7/|t| ≤ 0.27 ≤ 1 ✓. In Lean: div_le: 2‖s+1‖ ≤ ‖s‖‖s+2‖·1? 2·(7/2+|t|) ≤ |t|·|t| ⟺ 7 + 2|t| ≤ |t|² ✓ (|t| ≥ 10: |t|² ≥ 10|t| ≥ 7 + 2|t| ⟺ 8|t| ≥ 7 ✓). nlinarith.)\n    log π ≤ 2 (Real.log_pi_lt_d9? `Real.log_pi_lt_d9 : log π < 1.1447298859`? there is Real.log_pi... just: π ≤ e² ⟹ log π ≤ 2: Real.log_le_iff_le_exp banked journal-024: Real.log_le_iff_le_exp (h : 0 < x) : log x ≤ y ↔ x ≤ exp y; π ≤ exp 2? exp 2 > 7.38 > π ✓ via Real.exp_one_gt_d9: e > 2.7182818283 ⟹ e² > 7.38 ✓ nlinarith or: journal-024's two_le_log_abs_t used e² ≤ 2.7183² < 10 — I need π < e²: 2.7183² = 7.389 > 3.1416 ✓. So log π ≤ 2 ✓.)\n  Total: ≤ 2 + (log|t| + 5)/2 + (log|t| + 5)/2 + 1 = log|t| + 8 ≤ 4·(log|t|)² [L ≥ 2: 4L² ≥ 8L ≥ L + 14 > L + 8 ⟹ 4L² − L − 8 ≥ 7L − 8 ≥ 6 > 0 — via nlinarith [hL : 2 ≤ L, sq_nonneg (L − 2)]... 4L² − L − 8 ≥ 0 at L ≥ 2: 4L² = 4L·L ≥ 8L (L ≥ 2) ⟹ ≥ 8L − L − 8 = 7L − 8 ≥ 6 ✓ nlinarith [mul_le_mul_of_nonneg...]. Simplest: nlinarith [hL, sq_nonneg (L - 2)]: 4(L−2)² ≥ 0 ⟹ 4L² ≥ 16L − 16 ⟹ 4L² − L − 8 ≥ 15L − 24 ≥ 6 ✓ nlinarith should close with hL and sq_nonneg.]\n  where 2 ≤ log|t| from LiDisc's two_le_log_abs_t (check the name/form: journal-024 §6 \"two_le_log_abs_t (e² ≤ 2.7183² < 10)\" — it's in LiDisc.lean, namespace NguyenRH1 ✓ same namespace here).\n\n§5 capstone:\n- logDeriv_riemannZeta_sub_nearZeros_le_left {t} (ht : 10 ≤ |t|) {s} (hsim : s.im = t) (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 1/2) (hs0 : riemannZeta s ≠ 0):\n    ‖logDeriv riemannZeta s − Σ ρ ∈ nearZeros t, (zeroMult ρ : ℂ)/(s − ρ)‖ ≤ 200000 * (Real.log |t|)^2\n  proof:\n  set s' := 1 - s. Facts: s'.im = −t [simp: sub_im, one_im, hsim: (1−s).im = 1.im − s.im = −t]; |−t| = |t|; s'.re = 1 − s.re ∈ [1/2, 7/2]; ζ s' ≠ 0 [riemannZeta_one_sub_ne_zero_of: needs s ≠ 0 (im), Gammaℝ s ≠ 0 (im), 1−s ≠ 0 (re(1−s) ≥ 1/2 > 0 ⟹ ≠ 0), Gammaℝ (1−s) ≠ 0 (re > 0)].\n  h5c := logDeriv_riemannZeta_sub_nearZeros_le (t := −t) (abs_neg ▸ ht) (s := s') (s'.im = −t rfl-ish) hre'lo hre'hi hζ'\n    → ‖logDeriv ζ s' − Σ_{nearZeros (−t)} m/(s' − ρ')‖ ≤ 100000 * (log |−t|)²; rw abs_neg.\n  hfe := the FE identity (§2 B4 instantiated: s ≠ 0, s ≠ 1 (im), ΓR s ≠ 0, ΓR (1−s) ≠ 0, ζ s ≠ 0, diffs).\n  hrefl := sum_nearZeros_neg_reflect (s := s): Σ_{−t} m/(1−s−ρ') = −Σ_t m/(s−ρ).\n  hbr := gammaR_bracket_norm_le.\n  Algebra: X := logDeriv ζ s − Σ_t = [by hfe] −logDeriv ζ s' − (bracket) − Σ_t = −(logDeriv ζ s' − Σ_{−t}) − bracket [by hrefl: −Σ_t = Σ_{−t}... check: hrefl : Σ_{−t} (s'−form) = −Σ_t. logDeriv ζ s = −logDeriv ζ s' − bracket. So X = −logDeriv ζ s' − bracket − Σ_t = −logDeriv ζ s' − bracket + Σ_{−t} = −(logDeriv ζ s' − Σ_{−t}) − bracket ✓.]\n  ‖X‖ ≤ ‖logDeriv ζ s' − Σ_{−t}‖ + ‖bracket‖ [norm_neg + norm_add_le] ≤ 100000 L² + 4 L² = 100004 L² ≤ 200000 L² ✓ nlinarith [nonneg].\n\n§6 E (left-plane digamma): as planned; decls:\n- digamma_add_natCast {w : ℂ} (hw : w.im ≠ 0) (n : ℕ) : digamma (w + ↑n) = digamma w + Σ j ∈ Finset.range n, (w + ↑j)⁻¹ [induction; digamma_apply_add_one with (∀ m, w + ↑j ≠ −↑m): w + j = −m ⟹ im = 0 contra.]\n  Hmm wait — actually for E I only need the SHIFT with specific n. The induction: \n  n = 0: digamma (w + 0) = digamma w + 0 ✓ simp.\n  n+1: digamma (w + ↑(n+1)) = digamma ((w + ↑n) + 1) [push_cast ring] = digamma (w+↑n) + (w+↑n)⁻¹ [digamma_apply_add_one (w+↑n) (its hyp)] = (digamma w + Σ_{range n}) + (w+↑n)⁻¹ = digamma w + Σ_{range (n+1)} [sum_range_succ] ✓.\n- Then E2–E6 as planned. Constants: final ‖digamma w − log w‖ ≤ 3 for 2 ≤ |w.im|.\n\nHmm — for E3's FTC: the antiderivative F(x) = Complex.log (w + ↑x). HasDerivAt F ((w + ↑x)⁻¹) x? hasDerivAt_log (h : z ∈ slitPlane) : HasDerivAt log z⁻¹ z. comp with (w + ·): HasDerivAt (fun x => w + ↑x) 1 x: `HasDerivAt.const_add w (hasDerivAt_id' x)`? hasDerivAt_id' : HasDerivAt (fun x => x) 1 x? for ℝ → ℝ: hasDerivAt_id' (x : ℝ) : HasDerivAt (fun y => y) 1 x — hmm but here I need ℝ → ℂ: w + ↑x: the function is (fun x : ℝ => w + (x : ℂ)) = fun x => w + Complex.ofReal x. deriv of ofReal: ofRealCLM: `Complex.hasDerivAt_ofReal`? There's `Complex.hasDerivAt_ofReal : HasDerivAt ofReal 1 x`? I recall `Complex.hasDerivAt_ofReal (x : ℝ) : HasDerivAt Complex.ofReal 1 x`? or ofRealCLM.hasDerivAt. The Zeta23 EM helper used `ContinuousLinearMap.hasDerivAt (RCLike.ofRealCLM (K := 𝕜))` — so: (RCLike.ofRealCLM (K := ℂ)).hasDerivAt : HasDerivAt ofRealCLM 1... gives HasDerivAt (fun x => ofRealCLM x) ofRealCLM x — the derivative is a ContinuousLinearMap, not a ℂ scalar! Then comp with log (which is ℂ → ℂ): HasDerivAt.comp needs matching scalar types: log : ℂ → ℂ derivative ℂ-scalar; the inner ℝ → ℂ has CLM derivative. HasDerivAt.comp requires f : 𝕜 → 𝕜' and h : 𝕜' → 𝕜'' same field — here ℝ vs ℂ mismatch! So chain rule doesn't apply directly. Need: HasDerivAt (fun x : ℝ => log (w + ↑x)) — this is a function ℝ → ℂ; use `HasDerivAt.hasDerivAt_ofReal_comp`? Hmm. Alternative: define everything with f : ℝ → ℂ directly via `HasDerivAt.comp_ofReal`? There IS: `HasDerivAt.comp_ofReal (hf : HasDerivAt f f' (ofReal x)) : HasDerivAt (fun x => f (ofReal x)) (ofRealCLM... hmm. I recall Mathlib has `HasDerivAt.comp_ofReal : HasDerivAt f f' ↑x → HasDerivAt (fun r : ℝ => f ↑r) (f' • ofRealCLM...)`? There's `HasDerivAt.comp_ofReal (h : HasDerivAt f₁ f' (ofReal x)) : HasDerivAt (fun x : ℝ => f₁ (ofReal x)) (f' * 1 ...)`? Hmm. Let me think differently: the function g : ℝ → ℂ, g x = (w + ↑x)⁻¹ for FTC; the ANTIDERIVATIVE candidates: F : ℝ → ℂ with HasDerivAt F ((w+↑x)⁻¹) x. Take F x = log (w + ↑x): HasDerivAt: log differentiable at (w+↑x) as ℂ-function; the map x ↦ w + ↑x is ℝ → ℂ. Combined derivative: the CLM route: HasDerivAt (fun x : ℝ => log (w + ↑x)) (ofRealCLM?)... \n\n  The clean way in Mathlib: `HasDerivAt.comp_ofReal`:\n  `theorem HasDerivAt.comp_ofReal {f : ℂ → ℂ} {f' : ℂ} {x : ℝ} (h : HasDerivAt f f' ↑x) : HasDerivAt (fun y : ℝ => f ↑y) (f' • (1 : ℝ →L[ℝ] ℂ)?...` — I genuinely remember there being `HasDerivAt.comp_ofReal` and `HasDerivAt.ofReal_comp` in Mathlib.Analysis.SpecialFunctions... hmm, actually I recall `HasDerivAt.ofReal_comp (hf : HasDerivAt f f' x) : HasDerivAt (fun x => ofReal (f x)) ...` (the other direction) and `HasDerivAt.comp_ofReal (hf : HasDerivAt f f' (ofReal x)) : HasDerivAt (f ∘ ofReal) (ofRealCLM.comp...` — the resulting derivative is f' • ofRealCLM? something. The FTC lemma `intervalIntegral.integral_eq_sub_of_hasDerivAt` needs HasDerivAt F (F' x) x with F' : ℝ → ℂ — a FUNCTION, so the derivative must be expressed as a vector (not CLM). There's `HasDerivAt.hasDerivAt_of_hasDerivAt_ofReal`?... \n\n  Alternative much simpler route: avoid log-antiderivative FTC entirely! Compute ∫₀ⁿ (w+↑x)⁻¹ dx differently? Hmm no — the log difference is ESSENTIAL (that's the whole point).\n  \n  OK let me look for the right lemma: `HasDerivAt.comp_ofReal` — grep. Actually there's a cleaner approach used in PNT/Zeta23 for exactly this (integrals of complex functions along real intervals with log): check how Zeta23 handles similar FTCs. In LiRBound's intervalIntegral_b1_cpow they integrated x^{−s−2} — antiderivative x^{−s−1}/(−s−1) — they must have used ofReal-cpow derivs. Let me look at how LiRBound proved `intervalIntegral_b1_cpow` — there must be a HasDerivAt for (fun x : ℝ => (↑x)^(s : ℂ)) pattern I can mimic for log (w + ↑x). Let me grep LiRBound for hasDerivAt patterns.\n\nLet me check these details now. Also for §6 E4 the arctan FTC: pure real: HasDerivAt (fun x => (1/c) * Real.arctan ((x + a)/c)) (1/((x+a)²+c²)) x — standard real chain rule ✓ no ofReal issues.\n\nActually — hold on. For E3, maybe simpler: use `Complex.log` antiderivative via `HasDerivAt.comp_ofReal`. Let me grep Mathlib for comp_ofReal.","signature":""},{"type":"text","text":"Let me check the ofReal-chain-rule pattern (needed for the complex FTC) and how LiRBound handles it."},{"type":"tool_use","id":"Bash_31","name":"Bash","input":{"command":"cd /d/Python/Quantum/zeta-23-lean/.lake/packages/mathlib && grep -rn \"comp_ofReal\\|ofReal_comp\" Mathlib/Analysis/Calculus/Deriv/Comp.lean Mathlib/Analysis/SpecialFunctions/Complex/*.lean 2>/dev/null | grep -i \"theorem\\|lemma\" | head -6 && echo === && grep -rn \"hasDerivAt\\|HasDerivAt\" /d/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiRBound.lean | head -10","description":"Find ofReal chain rule and LiRBound HasDerivAt patterns"},"extra_content":null}]