[{"type":"thinking","thinking":"The proof is generic except the type is ℝ. `Summable.of_norm_bounded` — works for any NormedAddCommGroup? The proof uses `hf.norm` (Summable of norms). For ℂ the same proof works verbatim if Summable.of_norm_bounded is general. Actually — simpler: rather than duplicating, I can make the ℂ version by the same 20 lines. Let me check `Summable.of_norm_bounded`: hmm — the standard is `Summable.of_norm_bounded (hf : Summable g) (h : ∀ i, ‖f i‖ ≤ g i) : Summable f`. So `Summable.of_norm_bounded hf.norm (fun i => ...)` where the bound is ‖f i‖ ≤ ‖f i‖ ✓. Fine for ℂ.\n\nNow writing LiTightR.lean. Let me draft the whole 5f-i file carefully.\n\n```lean\n/-\nNguyenRH1/LiTightR.lean — tier ii′ sub-stage ii′-5f (D-069): the tight\nR-bound from the partial-fraction identity (reference-point method,\nD-056 §2 with the D-069 honest piece-2 count).\n\n§1: the ℂ tsum split (variant of LiCircleBound's tsum_split_finset).\n§2: the near-zero subtype finset `nearZerosSub` + membership.\n§3: the seriesFun difference identity.\n§4: the six-piece reference-point decomposition `Rexpr_decomp`.\n§5: piece 1 — `dirichletC2_le` (≤ 0.995).\n§6: piece 2 — the near sum at s₀ ≤ the ZeroCountProp2 count.\n§7: pieces 4/5 — the reciprocal differences.\n(pieces 3, 6: 5f-ii; the assembly + pinch lemma: 5f-iii.)\n-/\nimport Mathlib\nimport NguyenRH1.LiSqueeze\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n```\n\n§1:\n```lean\n/-! ## 1. The ℂ tsum split -/\n\n/-- Splitting a summable complex tsum over a finset (the ℂ variant of\nLiCircleBound's `tsum_split_finset`). -/\nlemma tsum_split_finset_complex {ι : Type*} [DecidableEq ι] {f : ι → ℂ} (hf : Summable f)\n    (s : Finset ι) :\n    ∑' i, f i = ∑ i ∈ s, f i + ∑' i, (if i ∈ s then 0 else f i) := by\n  classical\n  have h1 : Summable (fun i => if i ∈ s then f i else 0) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i ∈ s <;> simp [hi]\n  have h2 : Summable (fun i => if i ∈ s then 0 else f i) := by\n    apply Summable.of_norm_bounded hf.norm\n    intro i\n    by_cases hi : i ∈ s <;> simp [hi]\n  have h3 : ∑' i, f i\n      = ∑' i, ((if i ∈ s then f i else 0) + (if i ∈ s then 0 else f i)) := by\n    apply tsum_congr\n    intro i\n    by_cases hi : i ∈ s <;> simp [hi]\n  rw [h3, Summable.tsum_add h1 h2]\n  congr 1\n  rw [tsum_eq_sum (s := s) (fun b hb => if_neg hb)]\n  exact Finset.sum_congr rfl (fun b hb => if_pos hb)\n```\nHmm — `Summable.of_norm_bounded hf.norm` — the exact name/signature: from the LiCircleBound usage it works for ℝ. For ℂ: `Summable.of_norm_bounded (hf : Summable g) (h : ∀ i, ‖f i‖ ≤ g i)`? The LiCircleBound call: `Summable.of_norm_bounded hf.norm` then `intro i` — so of_norm_bounded takes the dominator's Summable and returns a goal ∀ i, ‖f i‖ ≤ ‖f' i‖... For ℂ, hf.norm : Summable (fun i => ‖f i‖) ✓ same. OK — but wait: is `Summable.of_norm_bounded` the right name? The LiCircleBound code compiled with it ✓ (it's in the same Mathlib). For ℂ the lemma might need the CompleteSpace — ℂ is complete ✓. Fine — actually, might as well try to just USE the ℝ version via... no, ℂ needed. Alternatively state it for a general NormedField? Just do ℂ.\n\nHmm wait — actually even simpler: can I state it for `{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]`? Overkill. ℂ only.\n\n§2: nearZerosSub.\n```lean\n/-! ## 2. The near-zero subtype finset -/\n\n/-- The near-zero subtype finset: nontrivial zeros with |γ − t| < 1,\nas a finset of the zero subtype (the seriesFun index type). -/\ndef nearZerosSub (t : ℝ) : Finset {ρ : ℂ // IsNontrivialZero ρ} :=\n  (finite_subtype_norm_lt (|t| + 3)).toFinset.filter fun ρ => |ρ.1.im - t| < 1\n```\nCheck `finite_subtype_norm_lt`'s exact name/form: from lowZeros def: `(finite_subtype_norm_lt 4)` : {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ:ℂ)‖ < 4}.Finite. So `finite_subtype_norm_lt (X : ℝ) : {ρ : subtype | ‖ρ.1‖ < X}.Finite` — hmm wait, the lowZeros def: `(show {ρ : {ρ // IsNontrivialZero ρ} | ‖(ρ : ℂ)‖ ≤ 3}.Finite from (finite_subtype_norm_lt 4).subset (fun ρ hρ => lt_of_le_of_lt (show ‖(ρ : ℂ)‖ ≤ 3 from hρ) (by norm_num)))`. So finite_subtype_norm_lt X : {ρ | ‖ρ.1‖ < X}.Finite where the subtype coercion ρ.1 or (ρ : ℂ) — both appear. OK.\n\n```lean\nlemma mem_nearZerosSub {t : ℝ} {ρ : {ρ : ℂ // IsNontrivialZero ρ}} :\n    ρ ∈ nearZerosSub t ↔ |ρ.1.im - t| < 1 := by\n  rw [nearZerosSub, Finset.mem_filter]\n  refine ⟨fun h => h.2, fun h => ⟨?_, h⟩⟩\n  rw [Set.Finite.mem_toFinset]\n  -- goal: ρ ∈ {ρ | ‖ρ.1‖ < |t| + 3}\n  show ‖ρ.1‖ < |t| + 3\n  have hre : |ρ.1.re| ≤ 1 := by\n    have h1 := ρ.2.2.1  -- 0 < re\n    have h2 := ρ.2.2.2  -- re < 1\n    rw [abs_le]\n    constructor <;> linarith\n  have him : |ρ.1.im| ≤ |t| + 1 := by\n    have := abs_sub_abs_le_abs_sub ρ.1.im t  -- hmm want |im| ≤ |im − t| + |t|\n    ...\n```\n|im| ≤ |im − t| + |t|: `abs_sub_abs_le_abs_sub : |a| − |b| ≤ |a − b|`... I want |im| ≤ |im−t| + |t| = abs_sub_le_abs_add_abs_sub? The triangle: |im| = |(im−t) + t| ≤ |im−t| + |t| (abs_add_le) ✓. So |im| ≤ |im−t| + |t| < 1 + |t|. And ‖ρ.1‖ ≤ |re| + |im| (Complex.norm_le_abs_re_add_abs_im — check name; there's `Complex.norm_le_abs_re_add_abs_im : ‖z‖ ≤ |z.re| + |z.im|` ✓ I believe). So ‖ρ‖ < 1 + (1 + |t|) = |t| + 2 < |t| + 3 ✓.\n\nSet.Finite.mem_toFinset — signature: (hs : s.Finite)? Earlier usage: `Set.Finite.mem_toFinset hfin` (one arg) at LiContour:175. So `Set.Finite.mem_toFinset (finite_subtype_norm_lt _) : a ∈ ....toFinset ↔ a ∈ {ρ | ‖ρ.1‖ < X}` — membership in the set-builder = the predicate ✓ `show ‖ρ.1‖ < |t| + 3` should be defeq ✓.\n\n§3: the difference identity.\n```lean\n/-! ## 3. The seriesFun difference identity -/\n\n/-- seriesFun s − seriesFun s₀ as the termwise difference series. -/\ntheorem seriesFun_sub_seriesFun (s s₀ : ℂ) :\n    seriesFun s - seriesFun s₀ = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1)) := by\n  rw [seriesFun, seriesFun, ← tsum_sub seriesSummable seriesSummable]\n  refine tsum_congr fun ρ => ?_\n  rw [seriesTerm, seriesTerm]\n  ring\n```\nCheck seriesSummable's signature: from LiSeries — \"seriesSummable at EVERY s\" — presumably `theorem seriesSummable (s : ℂ) : Summable (seriesTerm s)` or `Summable (fun ρ => seriesTerm s ρ)`. tsum_sub (hf : Summable f) (hg : Summable g) : ∑' (f − g) = ∑' f − ∑' g — so ← tsum_sub: ∑' f − ∑' g = ∑' (f − g) where f − g is the pointwise Pi.sub — ∑' ρ, (seriesTerm s − seriesTerm s₀) ρ = ∑' ρ, seriesTerm s ρ − seriesTerm s₀ ρ. Then tsum_congr with the pointwise identity: seriesTerm s ρ − seriesTerm s₀ ρ = (zeroMult ρ.1 : ℂ)·(1/(s−ρ.1) − 1/(s₀−ρ.1)) — via rw [seriesTerm, seriesTerm]: the def seriesTerm s ρ := (zeroMult ρ : ℂ)·(1/(s−(ρ:ℂ)) + 1/(ρ:ℂ)) — from LiSeries line 55-56: `def seriesTerm (s : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ := (zeroMult ρ : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))`. Hmm — (zeroMult ρ : ℂ) — ρ here is the subtype; zeroMult takes ℂ — so it's zeroMult ρ.1 with the coe. rw [seriesTerm] unfolds? For a def, `rw [seriesTerm]` uses the equation lemma — used in LiCircleBound (`rw [Fexpr]`). Hmm — actually `rw [seriesTerm]` might not work directly on defs... they used `rw [Fexpr]` in Fexpr_circle_le ✓ and `rw [Fexpr] at hG` in my capstone ✓ worked. For seriesTerm similar. But safer: `show` + ring, or `unfold seriesTerm`. Let me use `simp only [seriesTerm]`? hmm — I'll write `rw [seriesTerm, seriesTerm]` and if it fails, `unfold`. Actually there's a subtlety: after ← tsum_sub, the goal is ∑' ρ, seriesTerm s ρ − seriesTerm s₀ ρ = ∑' ρ, m·(1/(s−ρ.1) − 1/(s₀−ρ.1)). tsum_congr needs pointwise: seriesTerm s ρ − seriesTerm s₀ ρ = m·(...). rw [seriesTerm] rewrites the LHS occurrences: seriesTerm s ρ → (zeroMult ↑ρ : ℂ)·(1/(s − ↑ρ) + 1/↑ρ)... wait — does rw with a def name generate the equation? For `def f x := body`, rw [f] uses f.eq_def or the auto-generated equational lemma f : f x = body? In Lean4/Mathlib, `rw [f]` for a non-recursive def uses `f.eq_def`? There's the auto-generated `f.eq_def`? Hmm — the pattern used in the codebase: `rw [Fexpr]` at LiCircleBound:3846 and it worked. Also `rw [Gammaℝ_def]`-style. So `rw [seriesTerm, seriesTerm]` should unfold both applications — hmm, one rw [seriesTerm] unfolds ALL instances? Each rw [seriesTerm] unfolds every `seriesTerm ?s ?ρ` occurrence... it rewrites with the equation lemma `seriesTerm = fun s ρ => ...`? That would rewrite the FUNCTION, not the application — producing (fun s ρ => ...) s ρ redexes. Hmm — the codebase banked gotcha (session 027): \"sum_add_tsum_nat_add's shifted terms are beta-redexes (state goals in redex form)\". So rw [defname] produces beta-redexes which need beta reduction — `ring` after should still work (ring normalizes through beta-redexes? maybe not). The pattern that worked in Fexpr_circle_le: `rw [Fexpr]` then `exact norm_add_le _ _` — the goal after rw had the unfolded form ✓ worked there.\n\nAlternatively avoid rw: prove the pointwise identity by `show`:\n```lean\n  refine tsum_congr fun ρ => ?_\n  show (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) + 1 / ρ.1) - (zeroMult ρ.1 : ℂ) * (1 / (s₀ - ρ.1) + 1 / ρ.1) = _\n  ring\n```\nThe `show` needs the defeq form — seriesTerm s ρ is DEFEQ to its body (a plain def) ✓ `show` works. But I need to write the exact body form. The body: (zeroMult (ρ:ℂ) : ℂ) * (1 / (s - (ρ:ℂ)) + 1 / ((ρ:ℂ))). With ρ : subtype, (ρ : ℂ) = ρ.1 ✓. Let me write:\n```lean\n  refine tsum_congr fun ρ => ?_\n  show (zeroMult (ρ : ℂ) : ℂ) * (1 / (s - (ρ : ℂ)) + 1 / (ρ : ℂ))\n      - (zeroMult (ρ : ℂ) : ℂ) * (1 / (s₀ - (ρ : ℂ)) + 1 / (ρ : ℂ))\n      = (zeroMult (ρ : ℂ) : ℂ) * (1 / (s - (ρ : ℂ)) - 1 / (s₀ - (ρ : ℂ)))\n  ring\n```\nAnd the goal's RHS has (zeroMult ρ.1 : ℂ) — ρ.1 vs (ρ : ℂ) — defeq, and the `show` target's defeq to the goal ✓ (Subtype coe is ρ.1 — syntactically ↑ρ; the goal written with ρ.1 vs ↑ρ — hmm, my §3 statement writes `zeroMult ρ.1` and `s - ρ.1` but the def body uses `(ρ : ℂ)`. These are the SAME (ρ.1 = ↑ρ syntactically? In Lean4, Subtype's coe is `Subtype.val` = ρ.1 — `(ρ : ℂ)` elaborates to `Subtype.val ρ` i.e. `ρ.1` ✓ same term). OK.\n\n§4: the six-piece decomposition. Statement:\n\n```lean\n/-! ## 4. The reference-point decomposition -/\n\n/-- The R-expression decomposed at the reference point s₀ (both s and s₀\ngood, so the partial-fraction identity applies at both): the near sums\nover `nearZerosSub t`, the far difference series, the elementary terms,\nand the digamma difference. -/\ntheorem Rexpr_decomp (hZC : ZeroCountProp) {s s₀ : ℂ}\n    (hs : riemannZeta s ≠ 0) (hs0 : s ≠ 0) (hs1 : s ≠ 1)\n    (hst : ∀ n : ℕ, 1 ≤ n → s ≠ -2 * (n : ℂ))\n    (hs₀ : riemannZeta s₀ ≠ 0) (hs₀0 : s₀ ≠ 0) (hs₀1 : s₀ ≠ 1)\n    (hs₀t : ∀ n : ℕ, 1 ≤ n → s₀ ≠ -2 * (n : ℂ)) (t : ℝ) :\n    logDeriv riemannZeta s\n        - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)\n      = logDeriv riemannZeta s₀\n        - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s₀ - ρ.1)\n        + (∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n            if ρ ∈ nearZerosSub t then (0 : ℂ)\n            else (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1)))\n        - (1 / s - 1 / s₀) - (1 / (s - 1) - 1 / (s₀ - 1))\n        - (Complex.digamma (s / 2) - Complex.digamma (s₀ / 2)) / 2 := by\n  obtain ⟨B, hB⟩ := partialFraction_identity hZC\n  have hsid := hB s hs hs0 hs1 hst\n  have hs₀id := hB s₀ hs₀ hs₀0 hs₀1 hs₀t\n  -- the series difference\n  have hdiff := seriesFun_sub_seriesFun s s₀\n  -- the split of the difference series over nearZerosSub\n  have hsplit := tsum_split_finset_complex (f := fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>\n      (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1)))\n    (by ...) (nearZerosSub t)\n  ...\n```\nThe summability of the diff-term: from hdiff's RHS — `hsplit`'s hf : Summable (fun ρ => m·(1/(s−ρ.1) − 1/(s₀−ρ.1))): from seriesFun_sub_seriesFun: the RHS tsum equals seriesFun s − seriesFun s₀ — summable because it's the difference: `Summable.sub seriesSummable seriesSummable` — hmm the term form: seriesTerm s ρ − seriesTerm s₀ ρ vs m·(1/(s−ρ)−1/(s₀−ρ)) — pointwise equal (the §3 congr) so the summability transfers via Summable.congr: (Summable.sub seriesSummable seriesSummable).congr (fun ρ => (the pointwise identity)). Let me package: in §3, ALSO prove `diffTerm_summable : Summable (fun ρ => m·(1/(s−ρ.1) − 1/(s₀−ρ.1)))`.\n\nThen the algebra: Rexpr = logDeriv s − near(s). From hsid: logDeriv s = B + seriesFun s − 1/s − 1/(s−1) + c − ψ(s/2)/2. So:\nRexpr = B + seriesFun s − 1/s − 1/(s−1) + c − ψ(s/2)/2 − near(s)\nand logDeriv s₀ similarly. seriesFun s = seriesFun s₀ + Σ'all-diff (hdiff) = seriesFun s₀ + Σ_near diff + Σ'_far diff (hsplit). And Σ_near diff = Σ_near m·(1/(s−ρ) − 1/(s₀−ρ)) = near(s) − near(s₀) — the finset algebra: Σ ρ∈S, m·(1/(s−ρ) − 1/(s₀−ρ)) = Σ m/(s−ρ) − Σ m/(s₀−ρ) via Finset.sum_sub_distrib + mul_sub ✓.\n\nAssemble: Rexpr = logDeriv s₀ − near(s₀) + Σ'_far diff − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψ(s/2)−ψ(s₀/2))/2. All linear algebra in ℂ — after the substitutions, `linear_combination` with the haves or a calc. The ψ piece: hsid has − Complex.digamma (s/2)/2 — wait the identity: logDeriv ζ s = B + seriesFun s − 1/s − 1/(s−1) + (log π)/2 − digamma(s/2)/2. So the ψ terms: −ψ(s/2)/2 + ψ(s₀/2)/2 = −(ψ(s/2) − ψ(s₀/2))/2 ✓.\n\nProof sketch:\n```lean\n  have hnear : ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1))\n      = ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)\n        - ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s₀ - ρ.1) := by\n    rw [← Finset.sum_sub_distrib]\n    refine Finset.sum_congr rfl fun ρ _ => ?_\n    rw [mul_sub, div_eq_mul_one_div, div_eq_mul_one_div]  -- hmm m/(s−ρ) = m·(1/(s−ρ))\n    ring? \n```\nm·(1/(s−ρ) − 1/(s₀−ρ)) = m/(s−ρ) − m/(s₀−ρ): field_simp-free: div_eq_mul_one_div both sides then ring: m·(1/(s−ρ)) − m·(1/(s₀−ρ)) ✓ = m·(1/(s−ρ) − 1/(s₀−ρ)) ✓ ring. But rw div_eq_mul_one_div rewrites ALL divisions — including in the tsum... in this local have it's fine. Actually simpler: `rw [div_eq_mul_one_div, div_eq_mul_one_div, mul_sub]`? The goal: m·(1/(s−ρ) − 1/(s₀−ρ)) = m/(s−ρ) − m/(s₀−ρ): rw div_eq_mul_one_div twice turns RHS into m·(s−ρ)⁻¹ − m·(s₀−ρ)⁻¹; LHS has 1/(s−ρ) = (s−ρ)⁻¹ — one_div: 1/x = x⁻¹. So: rw [div_eq_mul_one_div (zeroMult ... : ℂ), div_eq_mul_one_div] — hmm the two divs are m/(s−ρ) and m/(s₀−ρ) — rw [div_eq_mul_one_div] rewrites ALL `_ / _` instances — including 1/(s−ρ) inside. Then LHS: m·((s−ρ)⁻¹·... no: 1/(s−ρ) = 1·(s−ρ)⁻¹ → (s−ρ)⁻¹ after one_mul? rw gives 1/(s−ρ) → 1 * (s−ρ)⁻¹. Messy. Cleanest: `field_simp`? No — pure commutive-ring identity with divisions as atoms: `linear_combination`? no haves. Just: have h : ∀ a b : ℂ, m·(a − b) = m·a − m·b := fun a b => mul_sub ..; the terms m/(s−ρ) = m·(1/(s−ρ)) via div_eq_mul_one_div... Actually simplest robust: prove with `rw [mul_sub]` after showing the div-forms match: m/(s−ρ) IS definitionally m·(s−ρ)⁻¹ and 1/(s−ρ) is 1·(s−ρ)⁻¹... The identity m·((s−ρ)⁻¹ − (s₀−ρ)⁻¹) = m·(s−ρ)⁻¹ − m·(s₀−ρ)⁻¹ is mul_sub ✓ and m/(s−ρ) = m·(s−ρ)⁻¹ = m·(1/(s−ρ)) since 1/(s−ρ) = (s−ρ)⁻¹ (one_div) and ·1... `one_mul`. So:\n```lean\n    refine Finset.sum_congr rfl fun ρ _ => ?_\n    rw [div_eq_mul_one_div, div_eq_mul_one_div, one_div, one_div]\n    ring\n```\ndiv_eq_mul_one_div : a / b = a * (1 / b). So m/(s−ρ) → m·(1/(s−ρ)) ✓ then one_div: 1/(s−ρ) → (s−ρ)⁻¹ — the LHS term m·(1/(s−ρ) − 1/(s₀−ρ)) → m·((s−ρ)⁻¹ − (s₀−ρ)⁻¹) — wait one_div rewrites 1/(s−ρ) too — after div_eq_mul_one_div turned m/(s−ρ) into m·(1/(s−ρ)), there are MORE 1/· instances — the two one_div rewrites handle 1/(s−ρ) and 1/(s₀−ρ) — but div_eq_mul_one_div also rewrites the 1/(s−ρ) inside?? div_eq_mul_one_div matches a/b with a = 1: 1/(s−ρ) → 1·(s−ρ)⁻¹ — hmm it rewrites ALL _/_ occurrences: the goal m·(1/(s−ρ) − 1/(s₀−ρ)) = m/(s−ρ) − m/(s₀−ρ): after rw [div_eq_mul_one_div]: LHS: m·((1·(s−ρ)⁻¹) − (1·(s₀−ρ)⁻¹)); RHS: m·(1·(s−ρ)⁻¹) − m·(1·(s₀−ρ)⁻¹). Then ring closes (the 1·x are fine for ring) ✓. So just `rw [div_eq_mul_one_div]; ring`? rw once rewrites all div instances ✓. Let me use that.\n\nThen the full assembly by linear_combination with hsid, hs₀id, hdiff, hsplit, hnear:\nGoal: logDeriv s − near(s) = logDeriv s₀ − near(s₀) + far − (1/s−1/s₀) − (1/(s−1)−1/(s₀−1)) − (ψs−ψs₀)/2.\nlinear_combination needs the goal minus a linear combination of haves to be a ring identity. Atoms: logDeriv s, logDeriv s₀, seriesFun s, seriesFun s₀, near(s), near(s₀), far-tsum-if, the all-diff-tsum, the if-near tsum, elems, ψs, ψs₀, B, c. Relations:\n- hsid: logDeriv s = B + seriesFun s − 1/s − 1/(s−1) + c − ψs/2\n- hs₀id: logDeriv s₀ = B + seriesFun s₀ − 1/s₀ − 1/(s₀−1) + c − ψs₀/2\n- hdiff: seriesFun s − seriesFun s₀ = alldiff\n- hsplit: alldiff = near-diff + far (tsum_split: ∑' = ∑ + ∑'if — the form: alldiff = Σ_near diff + far-tsum ✓)\n- hnear: near-diff-sum = near(s) − near(s₀)\nGoal: logDeriv s − near(s) = logDeriv s₀ − near(s₀) + far − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψs−ψs₀)/2.\nlinear_combination hsid − hs₀id + hdiff + hsplit + hnear: check: goal-LHS − goal-RHS = (logDeriv s − near(s)) − (logDeriv s₀ − near(s₀) + far − (1/s−1/s₀) − ...). Substitute: logDeriv s − logDeriv s₀ = (seriesFun s − seriesFun s₀) − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψs−ψs₀)/2 [hsid − hs₀id]. Then goal becomes: (seriesFun s − seriesFun s₀) − near(s) + near(s₀) − far = 0-ish ⟸ alldiff = near-diff + far, near-diff = near(s) − near(s₀) ✓. So linear_combination hsid - hs₀id + hdiff + hsplit + hnear — need to get the signs right; linear_combination checks goal_lhs − goal_rhs − (combination of (have_lhs − have_rhs)) = 0 by ring. Let me just try `linear_combination hsid - hs₀id + hdiff + hsplit + hnear` and adjust signs at compile.\n\nWait — but the statements: hsid : logDeriv riemannZeta s = B + seriesFun s − 1/s − 1/(s−1) + (↑(Real.log π))/2 − Complex.digamma (s/2)/2. The goal's far tsum: ∑' ρ, if ρ ∈ nearZerosSub t then 0 else m·(...) — and hsplit's form: tsum_split_finset_complex gives ∑' i, f i = ∑ i ∈ nearZerosSub t, f i + ∑' i, if i ∈ nearZerosSub t then 0 else f i ✓.\n\nOne subtlety: the goal and haves must have SYNTACTICALLY matching atoms for ring: e.g. the goal's `∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / (s - ρ.1)` vs hnear's RHS terms — written identically ✓. The `1 / s` forms ✓. The B from obtain ⟨B, hB⟩ — hsid/hs₀id both mention B ✓ cancels.\n\n§5: piece 1 — dirichletC2 ≤ 0.995. \n\ndirichletC2 := ∑' n, ‖LSeries.term (Λ) (2:ℂ) n‖. The term: LSeries.term f a n = f n / n^a for n ≥ 1, 0 for n = 0? LSeries.term: `LSeries.term f s n = if n = 0 then 0 else f n / n^s`. So ‖term‖ = if n=0 then 0 else Λ(n)/‖n^2‖ = Λ(n)/n² (for n ≥ 1; Λ(n) ≥ 0 real; ‖(n:ℂ)²‖ = n²). So dirichletC2 = Σ'_{n≥1} Λ(n)/n². Bound: Λ(n) ≤ log n (real): Mathlib `ArithmeticFunction.vonMangoldt_le_log : Λ n ≤ log n`? Let me check — there's `ArithmeticFunction.vonMangoldt_le_log : ∀ (n : ℕ), Λ n ≤ Real.log n`? I believe it exists (vonMangoldt_le_log). Check at build.\n\nThen the tail: Σ'_{n≥4} log n/n² ≤ ∫₃^∞ log x/x² dx = (log 3 + 1)/3. The integral: ∫ log x/x² dx = −(log x + 1)/x. Mathlib: is there `Real.integral_log_div_pow_two`? Unlikely. Prove via FTC: the antiderivative F(x) = −(log x + 1)/x has F'(x) = log x/x² for x > 0. Then ∫_{3}^{N} = F(N) − F(3) → −F(3) = (log 3+1)/3 as N → ∞ (F(N) → 0). The improper integral value + the comparison via AntitoneOn.tsum_comp_add_le_integral — its needs: AntitoneOn f (Ici N), IntegrableOn f (Ioi N), nonneg. IntegrableOn of log x/x² on Ioi 3 — from the explicit antiderivative + `intervalIntegral_tendsto_integral_Ioi`? There's machinery: `integrableOn_Ioi_of_intervalIntegral_norm_tendsto`... This is getting heavy. ALTERNATIVE cheaper bound for the tail avoiding integrals: for n ≥ 4: log n ≤ n^{0.34}·c? Hmm. log n/n² ≤ 1/n^{1.66}·(log n/n^{0.34}) — max of log n/n^{0.34} at n = e^{1/0.34} = e^{2.94} ≈ 18.9: value 2.94/18.9^{0.34}·... = (1/0.34)/e ≈ 1.0816/... hmm: max log n/n^ε = 1/(εe) at n = e^{1/ε}. ε = 0.34: 1/(0.34·e) = 1.0817. So log n/n² ≤ 1.0817/n^{1.66} — Σ_{n≥4} n^{−1.66} ≤ ∫₃^∞ x^{−1.66} = 3^{−0.66}/0.66 ≈ 0.484/0.66 = 0.733. Total tail ≤ 1.0817·0.733 = 0.793 > 0.6996 budget. Worse. ε = 0.5: max log n/√n = 2/e = 0.736; Σ n^{−1.5} from 4: ∫₃^∞ x^{−1.5} = 2/√3 = 1.155; 0.736·1.155 = 0.85 — worse. The integral route is needed for the sharp tail.\n\nHmm — OR: take more exact head terms. Head n=2..7 exact-ish, tail Σ_{n≥8} log n/n² ≤ ∫₇^∞ log x/x² = (log 7 + 1)/7 = 0.4216. Head: log2/4 = 0.17329, log3/9 = 0.12207, log4/16 = 0.08664, log5/25 = 0.06438, log6/36 = 0.04977, log7/49 = 0.03971. Head sum = 0.53586. Total: 0.53586 + 0.4216 = 0.9575 ≤ 1.01 ✓ more room (0.05). But still needs the integral. OK the integral is unavoidable — let me look for the cleanest integral evaluation. Actually — Mathlib DOES have some: `Real.integral_...`? Search for `log.*div.*pow` in Integrals.lean at build time. Alternatively compute ∫₃^N log x/x² dx via `intervalIntegral.integral_deriv_eq_sub` with F = fun x => −(log x + 1)/x: F' = log x/x² (by deriv rules: deriv of −(log x+1)/x = −[(1/x)·x − (log x+1)]/x² = −[1 − log x − 1]/x² = log x/x² ✓). Then ∫_{Ioi 3} = lim F(N) − F(3) = 0 − (−(log 3+1)/3) = (log 3+1)/3. The Ioi integral from the interval integrals: `intervalIntegral_tendsto_integral_Ioi` (h : Tendsto F atTop (𝓝 L))-style. This is standard-but-fiddly ~80 lines.\n\nHmm — actually, let me reconsider: is there an even cheaper majorant for dirichletC2 avoiding the tsum tail entirely? dirichletC2 = Σ Λ(n)/n² = −ζ′(2)/ζ(2). Closed form: −ζ′(2)/ζ(2) — Mathlib has ζ(2) = π²/6 (hasSum_zeta_two) but not ζ′(2). What about bounding the tsum by a geometric-ish comparison: for n ≥ 2, Λ(n) ≤ log n ≤ log 2·log₂ n... no.\n\nAlternative: use the PRIME-POWER structure: Σ_n Λ(n)/n² = Σ_p log p/(p²−1)·... = Σ_p log p·(1/p² + 1/p⁴ + ...) = Σ_p log p/(p²−1). Not easier in Lean.\n\nOR — completely different: skip the dirichletC2 numeric bound; note piece 1's budget is 1.01 and dirichletC2 = ∑' ‖term‖... can I bound dirichletC2 ≤ ζ(2)·something? Λ(n) ≤ log n ≤ (n^ε)/ε... \n\nActually you know what — simplest robust: head to n = 2, 3 exact + the integral tail, with the integral via the explicit antiderivative. It's ~80-100 lines. That's the honest cost. Actually wait — maybe use `AntitoneOn.tsum_le_integral` with the integrable proof from... the integrability of log x/x² on Ioi 3 — Mathlib might have `integrableOn_Ioi_...`? Hmm. There IS `integrableOn_Ioi_of_intervalIntegral...`. Let me look for a slicker path: `Real.integrableOn_log_div_pow`? Unlikely to exist.\n\nOK — time/context management: the file is getting big in planning. Let me structure 5f-i to include pieces 1,2,4,5 with piece 1 possibly via the integral route, and see how far the compile gets. Actually — for THIS session's remaining budget, maybe I should scope 5f-i to §1–§4 (the identity + split + decomposition) + pieces 2, 4, 5 (pure algebra/count) and defer piece 1's integral to 5f-ii (grouping it with the other analytic pieces). That gives a clean commit tonight.\n\nLet me write LiTightR.lean with §1–§4 + §6(piece 2) + §7(pieces 4/5), and leave piece 1 (dirichletC2 bound) + pieces 3, 6 for 5f-ii. The capstone in 5f-iii.\n\nPiece 2 detail (near sum at s₀ ≤ P1-count):\n```lean\n/-- Piece 2: the near sum at the reference point s₀ = 2 + it is bounded\nby the two-unit count (ZeroCountProp2), since |s₀ − ρ| ≥ 1 for every\nnontrivial zero. -/\ntheorem near_sum_refPoint_le (hZC2 : ZeroCountProp2) {t : ℝ} (ht : 10 ≤ t) :\n    ‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖\n      ≤ 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7 := by\n  -- per-term bound\n  have hterm : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub t →\n      ‖(zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖ ≤ (zeroMult ρ.1 : ℝ) := by\n    intro ρ hρ\n    -- |s₀ − ρ| ≥ 1\n    have h1 : (1 : ℝ) ≤ ‖(2 + t * Complex.I) - ρ.1‖ := by\n      have hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp [sub_re]\n      have h := abs_re_le_norm (((2 + t * Complex.I) - ρ.1))\n      rw [hre] at h\n      -- |2 − re ρ| ≥ 1 since re ρ ≤ 1 (strictly < 1)\n      have hρre : ρ.1.re < 1 := ρ.2.2.2\n      have : (1 : ℝ) ≤ |2 - ρ.1.re| := by\n        rw [abs_of_nonneg (by linarith)]; linarith\n      exact this.trans h\n    rw [norm_div]\n    have h2 : ‖(zeroMult ρ.1 : ℂ)‖ = (zeroMult ρ.1 : ℝ) := by\n      rw [show (zeroMult ρ.1 : ℂ) = ((zeroMult ρ.1 : ℝ) : ℂ) by push_cast; ring,\n        Complex.norm_real]\n      exact abs_of_nonneg (Nat.cast_nonneg _)  -- hmm norm_real gives |x| = x for x ≥ 0\n    rw [h2]\n    exact (div_le_one (by linarith : (0:ℝ) < ‖(2 + t*I) − ρ.1‖)).mpr ... \n```\nhmm: ‖a/b‖ = ‖a‖/‖b‖ ≤ ‖a‖ iff ‖b‖ ≥ 1 (‖a‖ ≥ 0): div_le_iff₀: ‖a‖/‖b‖ ≤ ‖a‖ ⟺ ‖a‖ ≤ ‖a‖·‖b‖ ⟸ 1 ≤ ‖b‖ (mul_le_mul_of_nonneg_left). So:\n```lean\n    rw [norm_div, h2]\n    calc (zeroMult ρ.1 : ℝ) / ‖(2 + t * Complex.I) - ρ.1‖\n        ≤ (zeroMult ρ.1 : ℝ) / 1 := div_le_div_of_nonneg_left (Nat.cast_nonneg _)\n            (by linarith) h1\n      _ = (zeroMult ρ.1 : ℝ) := div_one _\n```\n`div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a / c ≤ a / b` — signature check: div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (hbc : b ≤ c) : a / c ≤ a / b. So `div_le_div_of_nonneg_left (Nat.cast_nonneg _) (by linarith [h1] : (0:ℝ) < 1) h1 : (zeroMult:ℝ)/‖..‖ ≤ (zeroMult:ℝ)/1` — wait direction: a/c ≤ a/b with b = 1 ≤ c = ‖..‖ ✓ gives (zeroMult)/‖..‖ ≤ (zeroMult)/1 ✓.\n\nThen:\n```lean\n  calc ‖∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖\n      ≤ ∑ ρ ∈ nearZerosSub t, ‖(zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖ :=\n        norm_sum_le _ _\n    _ ≤ ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ) := Finset.sum_le_sum hterm\n    _ ≤ ((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ : ℝ) := by\n        -- nearZerosSub t (as a ℂ-finset) ⊆ zeroAbsWindow finset\n        ...\n    _ ≤ 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7 := hZC2 t ht\n```\nThe inclusion step: the nearZerosSub sum is over the SUBTYPE; the ZeroCountProp2 sum is over the ℂ-finset (zeroAbsWindow_finite t).toFinset. Bridge: Σ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ) = Σ ρ ∈ (nearZerosSub t).image Subtype.val, (zeroMult ρ : ℝ) via Finset.sum_image (Subtype.val injective) — and the image ⊆ (zeroAbsWindow_finite t).toFinset: elements are nontrivial zeros with |im − t| < 1 ⊂ ≤ 1 ✓. Then Finset.sum_le_sum_of_subset_of_nonneg (terms ≥ 0). So:\n```lean\n    have hbridge : ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)\n        = ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n      rw [Finset.sum_image]\n      · exact fun x _ y _ h => Subtype.ext h\n    have hsub : (nearZerosSub t).image (fun ρ => ρ.1) ⊆ (zeroAbsWindow_finite t).toFinset := by\n      intro ρ hρ\n      rw [Finset.mem_image] at hρ\n      obtain ⟨ρ', hρ'mem, hρ'eq⟩ := hρ\n      rw [Set.Finite.mem_toFinset]\n      -- ρ = ρ'.1, ρ' ∈ nearZerosSub t ⟹ |ρ.im − t| < 1 ⟹ ≤ 1\n      have hnear := (mem_nearZerosSub.mp hρ'mem)  -- |ρ'.1.im − t| < 1\n      rw [← hρ'eq]  -- ρ'.1 = ρ? hρ'eq : ρ'.1 = ρ\n      refine ⟨ρ'.2, ?_⟩\n      · exact hnear.le  -- |ρ'.1.im − t| ≤ 1\n    calc ...\n```\nHmm — hρ'eq : (fun ρ => ρ.1) ρ' = ρ i.e. ρ'.1 = ρ. And zeroAbsWindow t = {ρ | IsNontrivialZero ρ ∧ |ρ.im − t| ≤ 1} — membership: ⟨ρ'.2, hnear.le⟩ with ρ'.1 = ρ — the rewriting: goal IsNontrivialZero ρ ∧ |ρ.im − t| ≤ 1; rw [← hρ'eq] changes ρ to ρ'.1 ✓ then exact ⟨ρ'.2, hnear.le⟩ ✓.\n\nWait — `Set.Finite.mem_toFinset` for the membership in (zeroAbsWindow_finite t).toFinset: `Set.Finite.mem_toFinset (hs : s.Finite) : a ∈ hs.toFinset ↔ a ∈ s` ✓.\n\nThen `Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ _ => Nat.cast_nonneg _)` : Σ image ≤ Σ window ✓.\n\nHmm — the sum in ZeroCountProp2 is `(zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ` — a ℕ sum cast to ℝ: `(((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ)`. My hbridge produces an ℝ-sum Σ (zeroMult ρ : ℝ). The cast bridge: ((Σ_{ℕ} zeroMult) : ℝ) = Σ_ℝ (zeroMult : ℝ) via Nat.cast_sum ✓ (push_cast handles). So:\n```lean\n    have hcast : (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ)\n        = ∑ ρ ∈ (zeroAbsWindow_finite t).toFinset, (zeroMult ρ : ℝ) := by\n      push_cast\n      rfl  -- hmm Nat.cast_sum: ↑(∑ f) = ∑ ↑f — push_cast normalizes the LHS to the RHS form\n    rw [hcast] at hZC2t  -- where hZC2t := hZC2 t ht\n```\nThen chain. OK.\n\nPiece 4/5:\n```lean\n/-- Pieces 4/5: the reciprocal differences at s vs s₀ = 2 + it. -/\ntheorem one_div_sub_one_div_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ} (hσ : -5/2 ≤ s.re ∧ s.re ≤ 3)\n    (him : s.im = t) :\n    ‖1 / s - 1 / (2 + t * Complex.I)‖ ≤ 0.045 ∧\n    ‖1 / (s - 1) - 1 / ((2 + t * Complex.I) - 1)‖ ≤ 0.045 := by\n  ...\n```\nDetails: 1/s − 1/s₀ = (s₀ − s)/(s·s₀): norm = |s₀−s|/(‖s‖‖s₀‖). |s₀ − s| = |2 − σ| (same t): (s₀ − s) = (2 − σ) + (t − t)i = 2 − σ: ‖s₀ − s‖ = |2 − σ| ≤ 4.5 (σ ∈ [−2.5, 3] ⟹ 2−σ ∈ [−1, 4.5] ⟹ |2−σ| ≤ 4.5). ‖s‖ ≥ |im s| = t ≥ 10 (im s = t; |im s| ≤ ‖s‖ via abs_im_le_norm... wait ‖s‖ ≥ |im s|: `Complex.abs_im_le_norm`? there's abs_re_le_norm (used in session 033) — abs_im_le_norm should exist too). ‖s₀‖ = ‖2 + tI‖ ≥ |im| = t. So norm ≤ 4.5/(t·t) ≤ 4.5/100 = 0.045. \n\nFor the s−1 version: ‖s−1‖ ≥ |im(s−1)| = t (im(s−1) = im s = t); ‖s₀−1‖ = ‖1 + tI‖ ≥ t. Same bound ✓.\n\nThe division identity: 1/s − 1/s₀ = (s₀ − s)/(s·s₀) — `one_div_sub_one_div` : 1/a − 1/b = (b − a)/(a·b)? There's `one_div_sub_one_div'`. Or field_simp with s ≠ 0, s₀ ≠ 0. The norms: ‖(s₀−s)/(s s₀)‖ = ‖s₀−s‖/(‖s‖‖s₀‖) (norm_div, norm_mul).\n\nFine. Now — the assemble order. Let me also decide the exact final form of pieces to make the 5f-iii assembly smooth. But that's for later. Let me now WRITE the file with §1–§4 + piece 2 + pieces 4/5. Check `Complex.abs_im_le_norm` name... I'll use `Complex.abs_im_le_norm` — if not, `abs_im_le_norm` or via normSq. Risky names to verify: `abs_re_le_norm` (banked session-033 ✓ exists), `abs_im_le_norm` (probably exists), `Complex.norm_le_abs_re_add_abs_im` (check), `norm_sum_le` ✓ standard, `Finset.sum_image` ✓ (used before with f-pin — banked gotcha: \"sum_image's f is auto-bound (pin (f := ...))\" — hmm, from session 032: \"sum_image's f is auto-bound (pin (f := ...))\" — I'll write Finset.sum_image with the inj proof and pin if needed).\n\n`Complex.norm_le_abs_re_add_abs_im` — hmm not sure. Alternative for §2's membership: ‖ρ‖² = re² + im² (normSq) ≤ (|re|+|im|)²: ‖ρ‖ = √(re²+im²) ≤ |re|+|im| since re²+im² ≤ (|re|+|im|)² (cross term 2|re||im| ≥ 0) and sqrt monotone: `Real.sqrt_le_sqrt` + `Real.sqrt_le_left`?... Simpler: Complex.norm_le_abs_re_add_abs_im — grep at build; fallback: nlinarith with normSq: ‖ρ‖² = re²+im² ≤ (1 + (|t|+1))²: have ‖ρ‖^2 = re^2 + im^2 (Complex.norm_sq_eq... `Complex.normSq_eq_norm_sq : normSq z = ‖z‖²` ✓ banked) then (|re| + |im|)² ≥ re²+im² ⟹ ‖ρ‖ ≤ |re|+|im| via pow_le_pow_left₀-reverse (sq_le_sq₀)... `sq_le_sq₀ (norm_nonneg _) (h)`... Let me just use: ‖ρ‖ ≤ ‖ρ‖... you know what, simplest: ‖ρ‖ ≤ |re ρ| + |im ρ| — I'm fairly confident `Complex.norm_le_abs_re_add_abs_im` exists in Mathlib (Analysis/Complex/Basic.lean or .../Abs). If not: prove via nlinarith on squares.\n\nLet me check quickly before writing.","signature":""},{"type":"text","text":"Continuing with 5f-i. Verifying the last few lemma names for the file."},{"type":"tool_use","id":"Bash_140","name":"Bash","input":{"command":"M=D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib; grep -rn \"norm_le_abs_re_add_abs_im\\|abs_im_le_norm\" $M/Analysis/Complex/Basic.lean $M/Analysis/Complex/Abs.lean $M/Data/Complex/*.lean 2>/dev/null | head -5; grep -rn \"theorem finite_subtype_norm_lt\\|lemma finite_subtype_norm_lt\" D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/*.lean | head -2; grep -rn \"theorem seriesSummable\" D:/Python/Quantum/research/lean/NguyenRH1/NguyenRH1/LiSeries.lean | head -2","description":"Verify norm lemmas and seriesSummable signature"},"extra_content":null}]