[{"type":"thinking","thinking":"All verified:\n- `Complex.abs_im_le_norm` (in Complex namespace at Norm.lean:185 — with `open Complex` it's abs_im_le_norm; but abs_re_le_norm was used unqualified in LiCircleBound — they're in the Complex namespace? Line 185 is `theorem abs_im_le_norm (z : ℂ)` inside `namespace Complex` presumably; the project used `abs_re_le_norm` unqualified with open Complex ✓ so abs_im_le_norm works the same).\n- `Complex.norm_le_abs_re_add_abs_im` ✓.\n- `finite_subtype_norm_lt (R : ℝ) : {ρ : subtype | ‖(ρ:ℂ)‖ < R}.Finite` ✓.\n- `seriesSummable (s : ℂ) : Summable (fun ρ : subtype => seriesTerm s ρ)` ✓.\n\nNow write the file. Pieces for 5f-i:\n§1 tsum_split_finset_complex\n§2 nearZerosSub + mem_nearZerosSub\n§3 diffTerm summable + seriesFun_sub_seriesFun\n§4 Rexpr_decomp\n§5 piece 2 (near_sum_refPoint_le)\n§6 pieces 4/5 (one_div bounds)\n\nPiece 1 (dirichletC2) deferred to 5f-ii (integral work), pieces 3, 6 likewise, assembly 5f-iii.\n\nLet me be careful with the Rexpr_decomp statement — matching atom forms exactly. I'll write the goal with the same term forms used in the proof haves.\n\nOne concern in §4: the partialFraction_identity instance gives logDeriv ζ s = B + seriesFun s − 1/s − 1/(s−1) + ↑(Real.log π)/2 − ψ(s/2)/2. The hB form: hB s hs hs0 hs1 hst where the hypothesis order: (hζ : riemannZeta s ≠ 0) (hs0 : s ≠ 0) (hs1 : s ≠ 1) (hsn : ∀ n, 1 ≤ n → s ≠ −2n) ✓ matches my §4 hypotheses.\n\nThe final algebra: goal:\nlogDeriv ζ s − N(s) = logDeriv ζ s₀ − N(s₀) + FAR − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψs − ψs₀)/2\nwhere N(s) := ∑ ρ ∈ nearZerosSub t, m/(s−ρ), FAR := ∑' ρ, if ρ ∈ nearZerosSub t then 0 else m·(1/(s−ρ)−1/(s₀−ρ)).\n\nlinear_combination hsid − hs₀id + hdiff + hsplit + hnear with:\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 (the Σ' of m·(1/(s−ρ)−1/(s₀−ρ)))\n- hsplit : ALLDIFF = NEARDIFF + FAR where NEARDIFF := ∑ ρ ∈ nearZerosSub t, m·(1/(s−ρ)−1/(s₀−ρ)) — from tsum_split_finset_complex hfsum (nearZerosSub t) : ∑' = ∑ + ∑'if ✓ (f := the diff term).\n- hnear : NEARDIFF = N(s) − N(s₀).\n\nGoal − (hsid − hs₀id + hdiff + hsplit + hnear):\nLHS−RHS of goal: (logDeriv s − N s) − (logDeriv s₀ − N s₀ + FAR − (1/s − 1/s₀) − (1/(s−1) − 1/(s₀−1)) − (ψs−ψs₀)/2).\nMinus hsid: −(B + seriesFun s − 1/s − 1/(s−1) + c − ψs/2) + logDeriv s — wait linear_combination h: goal_lhs − goal_rhs = coefficient·(h_lhs − h_rhs) must be ring-zero. Let me expand goal−[hsid − hs₀id + hdiff + hsplit + hnear]:\n\ngoal(L−R) = Ls − Ns − Ls₀ + Ns₀ − FAR + (1/s − 1/s₀) + (1/(s−1) − 1/(s₀−1)) + (ψs−ψs₀)/2.\nhsid(L−R) = Ls − (B + Ss − 1/s − 1/(s−1) + c − ψs/2).\nhs₀id(L−R) = Ls₀ − (B + Ss₀ − 1/s₀ − 1/(s₀−1) + c − ψs₀/2).\nhdiff(L−R) = (Ss − Ss₀) − ALLDIFF.\nhsplit(L−R) = ALLDIFF − NEARDIFF − FAR.\nhnear(L−R) = NEARDIFF − (Ns − Ns₀).\n\ngoal − hsid + hs₀id − hdiff − hsplit − hnear:\n= [Ls − Ns − Ls₀ + Ns₀ − FAR + Δ1 + Δ2 + Δψ/2] − [Ls − B − Ss + 1/s + 1/(s−1) − c + ψs/2] + [Ls₀ − B − Ss₀ + 1/s₀ + 1/(s₀−1) − c + ψs₀/2] − [Ss − Ss₀ − ALLDIFF] − [ALLDIFF − NEARDIFF − FAR] − [NEARDIFF − Ns + Ns₀]\nwhere Δ1 = (1/s − 1/s₀), Δ2 = (1/(s−1) − 1/(s₀−1)), Δψ = ψs − ψs₀.\n\nCollect Ls: 1 − 1 = 0 ✓. Ls₀: −1 + 1 = 0 ✓. Ns: −1 + 1 = 0 ✓ (last term +Ns). Ns₀: +1 − 1 = 0 ✓. FAR: −1 + 1 = 0 ✓. B: +1 − 1 = 0 ✓. Ss: +1 − 1 = 0 ✓. Ss₀: −1 + 1 = 0 ✓. ALLDIFF: +1 − 1 = 0 ✓. NEARDIFF: +1 − 1 = 0 ✓. c: +1 − 1 = 0 ✓. Constants: 1/s: from goal +1/s; from −hsid: +1/s... wait: goal has +Δ1 = +1/s − 1/s₀; −hsid contributes +1/s (since −(−1/s)... let me redo: −hsid(L−R) = −Ls + B + Ss − 1/s − 1/(s−1) + c − ψs/2. Hmm I need to be careful. Let me just trust linear_combination's ring to sort out: the remaining atoms: 1/s: goal +1, −hsid: −(−1/s)=+1/s·(−1)... \n\nLet me redo cleanly. linear_combination e computes (goal_lhs − goal_rhs) − e_expanded and checks = 0 by ring, where e = Σ cᵢ·(hᵢ_lhs − hᵢ_rhs).\n\ngoal_lhs − goal_rhs = Ls − Ns − Ls₀ + Ns₀ − FAR + Δ₁ + Δ₂ + Δψ/2.\nhsid diff: hsid_l − hsid_r = Ls − B − Ss + (1/s) + (1/(s−1)) − c + ψs/2.\nhs₀id diff: Ls₀ − B − Ss₀ + (1/s₀) + (1/(s₀−1)) − c + ψs₀/2.\nhdiff diff: Ss − Ss₀ − ALLDIFF.\nhsplit diff: ALLDIFF − NEARDIFF − FAR.\nhnear diff: NEARDIFF − Ns + Ns₀.\n\nTry combination: goal − hsid + hs₀id − hdiff − hsplit − hnear:\nLs: 1 − 1 = 0 ✓\nNs: −1 − (−1)·... hnear coeff is −1: −(− Ns) = +Ns: −1 + 1 = 0 ✓\nLs₀: −1 + 1 = 0 ✓\nNs₀: +1 + (−1)(+Ns₀) = 1 − 1 = 0 ✓\nFAR: −1 + (−1)(−FAR) = −1 + 1 = 0 ✓ (hsplit coeff −1, its diff has −FAR: −(−FAR) = +FAR: −1 + 1 ✓)\nB: 0 − (−B) + (−B) = +B − B = 0 ✓\nSs: 0 − (−Ss) + (−1)(Ss) = Ss − Ss = 0 ✓\nSs₀: 0 + (−Ss₀) + (−1)(−Ss₀) = −Ss₀ + Ss₀ = 0 ✓\n1/s: +1 (from Δ₁) + (−1)(+1/s) = 1 − 1 = 0 ✓\n1/s₀: −1 (from Δ₁) + (+1)(+1/s₀) = −1 + 1 = 0 ✓\n1/(s−1): +1 + (−1)(+1/(s−1)) = 0 ✓\n1/(s₀−1): −1 + 1·(+1/(s₀−1)) = 0 ✓\nc: 0 − (−c) + (+1)(−c) = c − c = 0 ✓\nψs: +1/2 + (−1)(ψs/2) = 0 ✓\nψs₀: −1/2 + (1)(ψs₀/2) = 0 ✓\nALLDIFF: 0 + (−1)(−ALLDIFF) + (−1)(ALLDIFF) = ALLDIFF − ALLDIFF = 0 ✓\nNEARDIFF: 0 + (−1)(−NEARDIFF) + (−1)(NEARDIFF) = 0 ✓\n\nSo `linear_combination hsid - hs₀id ... ` wait my coeffs: goal − hsid + hs₀id − hdiff − hsplit − hnear — I.e., e := hsid − hs₀id + hdiff + hsplit + hnear, and linear_combination checks (goal_diff) = e_expanded... whatever the convention, `linear_combination hsid - hs₀id + hdiff + hsplit + hnear`? Hmm — I computed goal − hsid + hs₀id − hdiff − hsplit − hnear = 0, so e := hsid − hs₀id + hdiff + hsplit + hnear gives goal_diff − e_diff = 0 ✓ wait no: I computed goal − (hsid − hs₀id + hdiff + hsplit + hnear) = goal − hsid + hs₀id − hdiff − hsplit − hnear = 0 ✓. So `linear_combination hsid - hs₀id + hdiff + hsplit + hnear` — linear_combination e checks goal_diff − e = ring-zero, with e = hsid − hs₀id + hdiff + hsplit + hnear ✓.\n\nBUT — the atom matching for ring: the FAR term in the goal is `∑' ρ, if ρ ∈ nearZerosSub t then 0 else ...` and hsplit's is `∑' i, (if i ∈ nearZerosSub t then 0 else f i)` — same if the f and set match syntactically. tsum_split_finset_complex's statement: ∑' i, f i = ∑ i ∈ s, f i + ∑' i, (if i ∈ s then 0 else f i) — the if-term: `if i ∈ s then 0 else f i` with my f := fun ρ => (zeroMult ρ.1 : ℂ)·(1/(s−ρ.1) − 1/(s₀−ρ.1)). The goal's FAR must be written in EXACTLY this form for the ring atom match. I'll write the goal's FAR as `∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, if ρ ∈ nearZerosSub t then (0 : ℂ) else (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1))`. The hsplit instance: tsum_split_finset_complex (f := fun ρ => (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1))) hfsum (nearZerosSub t) — its if-term: `if ρ ∈ nearZerosSub t then 0 else (fun ρ => ...) ρ` — BETA REDEX! (fun ρ => ...) ρ vs the direct application — defeq but not syntactic; ring treats them as different atoms?? ring's atom matching is up to reducible defeq — a beta-redex (fun ρ => f ρ) x reduces to f x at whnf — ring should see through it (ring normalizes terms up to atomic instances... hmm, ring's atom recognition uses `ring_nf` which does reduce beta-redexes? To be safe, state hsplit via a `show` to normalize, or use `only`. The banked gotcha (session 027): \"sum_add_tsum_nat_add's shifted terms are beta-redexes (state goals in redex form)\" — i.e., BANKED: state the goal in the redex form to match. So in MY goal, write the FAR as the redex form? Ugly. Alternative: after obtaining hsplit, `simp only []` at it to beta-reduce? `beta_reduce`? There's `simp only []` does beta. Or `change` at hsplit. I'll handle with a `have hsplit := ... ; simp only [] at hsplit`? Hmm — cleaner: `rw` nothing; state the goal's FAR in the redex form... Actually simplest: make the diff term a DEF:\n```lean\ndef farDiffTerm (s s₀ : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  if ρ ∈ nearZerosSub t then 0 else ...\n```\nno — the membership depends on t. Let me just make the diff term a plain def WITHOUT the if, and the if applied to it:\n```lean\n/-- The seriesFun difference term. -/\ndef seriesDiffTerm (s s₀ : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1))\n```\nThen hdiff : seriesFun s − seriesFun s₀ = ∑' ρ, seriesDiffTerm s s₀ ρ; hsplit : ∑' ρ, seriesDiffTerm s s₀ ρ = ∑ ρ ∈ nearZerosSub t, seriesDiffTerm s s₀ ρ + ∑' ρ, if ρ ∈ nearZerosSub t then 0 else seriesDiffTerm s s₀ ρ — the if-else applies to the def-application (no redex: f is (seriesDiffTerm s s₀), a partial application, and (fun...) ρ = seriesDiffTerm s s₀ ρ ✓ syntactic). And the goal's FAR: ∑' ρ, if ρ ∈ nearZerosSub t then (0:ℂ) else seriesDiffTerm s s₀ ρ ✓ matches. hnear : ∑ ρ ∈ nearZerosSub t, seriesDiffTerm s s₀ ρ = N(s) − N(s₀) via sum_congr (each term: seriesDiffTerm s s₀ ρ = m/(s−ρ) − m/(s₀−ρ) by [unfold/rw seriesDiffTerm + div algebra]) + Finset.sum_sub_distrib.\n\nThis def-form is robust. Let me use it. seriesFun_sub_seriesFun's congr then: seriesTerm s ρ − seriesTerm s₀ ρ = seriesDiffTerm s s₀ ρ via show+ring.\n\nAlso for hsplit's Summable input: need Summable (seriesDiffTerm s s₀): from the congr with (seriesTerm s − seriesTerm s₀): Summable.congr (Summable.sub seriesSummable seriesSummable) (fun ρ => (pointwise)).symm — Summable.congr (hf : Summable f) (h : ∀ i, f i = g i) : Summable g ✓.\n\nOK. Also piece 2 and 4/5 as planned. One more check for piece 2: `norm_sum_le : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖` ✓ standard (`norm_sum_le (s : Finset ι) (f : ι → E)`).\n\nAnd the `Set.Finite.mem_toFinset` signature — from LiContour:175: `Set.Finite.mem_toFinset hfin : ρ ∈ hfin.toFinset ↔ ρ ∈ zeroWindow a` — one explicit arg ✓.\n\nFor nearZerosSub mem (§2): \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  show ‖ρ.1‖ < |t| + 3\n  have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n  have hre : |ρ.1.re| ≤ 1 := by\n    have h1 : 0 < ρ.1.re := ρ.2.2.1\n    have h2 : ρ.1.re < 1 := ρ.2.2.2\n    rw [abs_le]\n    constructor <;> linarith\n  have him : |ρ.1.im| ≤ |t| + 1 := by\n    calc |ρ.1.im| = |ρ.1.im - t + t| := by rw [sub_add_cancel]\n      _ ≤ |ρ.1.im - t| + |t| := abs_add_le _ _\n      _ ≤ 1 + |t| := by linarith [h]\n      _ = |t| + 1 := by ring\n  linarith [hle, hre, him]\n```\nHmm — the membership in the set-builder {ρ | ‖ρ.1‖ < |t|+3}: `Set.Finite.mem_toFinset` gives ρ ∈ toFinset ↔ ρ ∈ {ρ | ‖ρ.1‖ < |t|+3}; ρ ∈ {set-builder} is defeq to ‖ρ.1‖ < |t|+3 but needs a `show` — `show ‖(ρ : ℂ)‖ < |t| + 3` — careful: the set-builder predicate is ‖(ρ : ℂ)‖ < R where (ρ : ℂ) vs ρ.1 — same. `show ‖(ρ:ℂ)‖ < |t| + 3` should work (defeq via Set.mem_setOf_eq — deprecated in this Mathlib per warnings! \"Set.mem_setOf_eq deprecated: use Set.mem_ofPred_eq\" — the set-builder {ρ | p ρ} membership: `show p ρ`? The deprecation warnings suggest mem_setOf_eq exists but deprecated — usable (warnings only). For `show`: ρ ∈ {ρ : subtype | ‖ρ.1‖ < R} — the membership unfolds to the predicate by defeq? Set membership a ∈ {x | p x} is `p a` by definition (Set.mem_setOf is defeq — `rfl`-level? In Lean4 Mathlib, `a ∈ {x | p x}` is defeq to `p a` ✓ so `show ‖ρ.1‖ < |t| + 3` typechecks ✓ modulo the ρ.1 vs ↑ρ form).\n\nAlso `abs_le` constructor: |x| ≤ 1 ↔ −1 ≤ x ∧ x ≤ 1: `abs_le.mpr ⟨h1, h2⟩`. My hre: from 0 < re < 1: |re| ≤ 1: abs_le: −1 ≤ re ∧ re ≤ 1 ✓ linarith both.\n\nOK — also for piece 2's hterm: ‖(zeroMult ρ.1 : ℂ) / w‖ where w = (2 + t·I) − ρ.1: need ‖w‖ ≥ 1: |re w| = |2 − re ρ| = 2 − re ρ (re ρ < 1 ⟹ 2 − re ρ > 1 > 0): |re w| = 2 − re ρ ≥ 1... abs_re_le_norm : |w.re| ≤ ‖w‖ ✓ (banked session-033: abs_re_le_norm exists). w.re: ((2 + t·I) − ρ.1).re = 2 − ρ.1.re: `sub_re` + the re of 2 + t·I: (2 : ℂ).re = 2 (Complex.ofReal_re? (2:ℂ) = ((2:ℝ):ℂ) by push_cast; or `Complex.add_re`: (2 + tI).re = 2 + 0... Let me compute: (2 + t * Complex.I).re: add_re: (2:ℂ).re + (t*I).re; (2:ℂ).re: `Complex.two_re`? hmm — (2:ℂ) is OfNat — `Complex.ofNat_re`? In practice: `simp [Complex.add_re, Complex.mul_re]` or push_cast. The robust route: `by simp [sub_re]` might not fully evaluate. Let me write: have hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp [Complex.sub_re, Complex.add_re] — with (t*I).re = 0 (Complex.mul_re: (t·I).re = t·I.re − 0·I.im... = t·0 − 0·1 = 0; simp knows Complex.I_re : I.re = 0 ✓ and ofReal_re: (↑t).re = t ✓). simp [Complex.sub_re, Complex.add_re, Complex.mul_re] should give 2·1 − 0·... hmm the real part of t*I: t*I = (t:ℂ)·I: mul_re: (t:ℂ).re·I.re − (t:ℂ).im·I.im = t·0 − 0·1 = 0 ✓ simp with I_re, I_im, ofReal_re, ofReal_im. I'll write `by simp [Complex.sub_re, Complex.add_re]` and adjust if needed — actually simpler: `by simp` might just do it with the default simp set for re/im (Complex.ext_iff simp lemmas). Let me just compute: simp can evaluate (2 + t*I − ρ).re fully if given sub_re/add_re/mul_re/ofReal_re/ofReal_im/I_re/I_im — these are all simp lemmas ✓ plain `simp` should work. I'll use `by simp`.\n\nPiece 4/5 statement:\n```lean\ntheorem one_div_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5/2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) (hs0 : s ≠ 0) :\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```\nProof: \n- s₀ := 2 + t·I. ‖s₀ − s‖ = |2 − s.re| (since ims equal): s₀ − s = (2 − s.re) + (t − s.im)·I = (2 − s.re) + 0·I (him): so s₀ − s = ((2 − s.re : ℝ) : ℂ): norm = |2 − s.re| ≤ 4.5 (from −2.5 ≤ re ≤ 3: 2−re ∈ [−1, 4.5]). \n  The cast: s₀ − s = ((2 − s.re : ℝ):ℂ): via Complex.ext_iff: re: 2 − re ✓; im: t − t = 0 ✓. Then norm of a real cast: Complex.norm_real : ‖(x:ℂ)‖ = |x| ✓.\n- ‖s‖ ≥ t: |im s| = |t| = t (ht ≥ 10 > 0): abs_im_le_norm: ‖s‖ ≥ |s.im| = |t| = t ✓ (rw [him]).\n- ‖s₀‖ ≥ t: |s₀.im| = t similarly (s₀.im = t by simp).\n- 1/s − 1/s₀ = (s₀ − s)/(s·s₀): `one_div_sub_one_div`? hmm — there's `one_div_sub_one_div' : 1/a − 1/b = (b − a)/(a·b)`? or field_simp. With hs0 : s ≠ 0 and hs₀0 : s₀ ≠ 0: field_simp [hs0, hs₀0] then ring: field_simp rewrites the goal 1/s − 1/s₀ = X to (s₀ − s)·... hmm field_simp on an equation with divisions: produces (s₀ − s) = X·(s·s₀)... messy. Better: `one_div_sub_one_div (ha : a ≠ 0) (hb : b ≠ 0) : 1/a − 1/b = (b − a)/(a*b)` — does this exist? I don't recall exactly; there IS `one_div_sub_one_div'`? Let me just prove via field: rw [div_sub_div _ _ hs0 hs₀0]? `div_sub_div (a b) (hc : c ≠ 0) (hd : d ≠ 0) : a/c − b/d = (a·d − c·b)/(c·d)` ✓ that's standard. So 1/s − 1/s₀ = (1·s₀ − s·1)/(s·s₀) = (s₀ − s)/(s·s₀) via div_sub_div + ring-ish (1·s₀ − s·1 = s₀ − s: by ring? as a rewrite the numerator form must match — after div_sub_div, norm: ‖(1·s₀ − s·1)/(s·s₀)‖; have : 1·s₀ − s·1 = s₀ − s := by ring; rw [this].) ✓.\n- Then ‖(s₀−s)/(s·s₀)‖ = ‖s₀−s‖/‖s·s₀‖ = ‖s₀−s‖/(‖s‖·‖s₀‖) ≤ 4.5/(t·t) ≤ 4.5/100 = 0.045: via div_le_div: numerator ≤ 4.5, denominator ≥ t·t ≥ 100: div_le_div (hnum : a ≤ b) (hden : c ≤ d)... the right lemma: a/c ≤ b/d... forms: div_le_div (hc : 0 ≤ c) (hab : a ≤ b) (hd : 0 < d) (hcd : c ≤ d)? hmm signature variants. `div_le_div (hc : 0 ≤ c) (hab : a ≤ b) (hd : 0 < d) (hcd : c ≤ d) : a / d ≤ b / c`? I recall `div_le_div (hac : a ≤ b) (hcd : c ≤ d) (c nonneg) (d pos)`... There are several forms; the safe one: `div_le_div_of_nonneg_left`/`div_le_div_iff`... Let me use: ‖s₀−s‖/(‖s‖‖s₀‖) ≤ 4.5/(‖s‖‖s₀‖) [div_le_div_of_nonneg_right? wait that's a/c ≤ b/c] — `div_le_div_right (hc : 0 < c) : a/c ≤ b/c ↔ a ≤ b` — hmm session-032 gotcha said \"div_le_div_right does NOT exist\". Use div_le_div_of_nonneg_right (h : a ≤ b) (hc : 0 ≤ c) : a/c ≤ b/c ✓ (banked exists). Then 4.5/(‖s‖‖s₀‖) ≤ 4.5/100: needs ‖s‖‖s₀‖ ≥ 100 and div_le_div_of_nonneg_left (0 ≤ 4.5) (0 < 100) (100 ≤ ‖s‖‖s₀‖) : 4.5/‖s‖‖s₀‖ ≤ 4.5/100 ✓. Then 4.5/100 = 0.045 by norm_num.\n  ‖s‖·‖s₀‖ ≥ 100: from ‖s‖ ≥ t ≥ 10, ‖s₀‖ ≥ t: mul_le_mul (both ≥ 0): mul_le_mul (h1 : t ≤ ‖s‖)... need t ≥ 0: t ≥ 10 ✓.\n- For s−1: ‖s−1‖ ≥ |im(s−1)| = |s.im| = t; ‖s₀−1‖ = ‖1 + tI‖ ≥ |im| = t. Same.\n\n0.045 — as a decimal literal in Lean ℝ: (0.045 : ℝ) — OfNat scientific — fine (they used 0.433 etc. in C0hat ✓).\n\nOK. Time to write the file. Also the far sum's eventual form for piece 3 (5f-ii): the far tsum with term (s₀−s)/((s−ρ)(s₀−ρ)) — from m·(1/(s−ρ) − 1/(s₀−ρ)) = m·(s₀−s)/((s−ρ)(s₀−ρ)): one_div_sub_one_div: 1/(s−ρ) − 1/(s₀−ρ) = (s₀−ρ − (s−ρ))/((s−ρ)(s₀−ρ)) = (s₀−s)/((s−ρ)(s₀−ρ)) ✓ (div_sub_div). For 5f-ii.\n\nLet me write the file now. I'll write §1–§6 (identity + piece 2 + pieces 4/5), defer piece 1 (dirichletC2 ≤ ...) to 5f-ii as noted in the header.","signature":""},{"type":"text","text":"All verified. Writing LiTightR.lean with the identity + pieces 2/4/5 (piece 1's integral bound groups with the 5f-ii analytic pieces)."},{"type":"tool_use","id":"Write_142","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","content":"/-\nNguyenRH1/LiTightR.lean — tier ii′ sub-stage ii′-5f (D-069): the tight\nR-bound from the partial-fraction identity (the reference-point method,\nD-056 §2, with the D-069 honest piece-2 two-unit 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 term + identity.\n§4: the six-piece reference-point decomposition `Rexpr_decomp`.\n§5: piece 2 — the near sum at s₀ = 2+it bounded by ZeroCountProp2.\n§6: pieces 4/5 — the reciprocal differences ≤ 0.045.\n\nRemaining (5f-ii): piece 1 (dirichletC2 ≤ 0.995), piece 6 (the sharp\ndigamma remainder via the level-2 EM), piece 3 (the far-sum interval\nmachine). (5f-iii): the assembly + the pinch lemma + the capstone\n`logDeriv_riemannZeta_sub_nearZeros_le_tight`.\n\nArchive references: D-069 (design + Findings 1/2), D-056 §2, journal-035.\n-/\nimport Mathlib\nimport NguyenRH1.LiSqueeze\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\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\n/-! ## 2. The near-zero subtype finset -/\n\n/-- The near-zero subtype finset: the nontrivial zeros with |γ − t| < 1,\nas a finset of the zero subtype (the `seriesFun` index type). The\ncontaining ball: |γ−t| < 1 and 0 < re < 1 give ‖ρ‖ ≤ |re| + |im| <\n|t| + 3. -/\ndef nearZerosSub (t : ℝ) : Finset {ρ : ℂ // IsNontrivialZero ρ} :=\n  (finite_subtype_norm_lt (|t| + 3)).toFinset.filter fun ρ => |ρ.1.im - t| < 1\n\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  show ‖ρ.1‖ < |t| + 3\n  have hle : ‖ρ.1‖ ≤ |ρ.1.re| + |ρ.1.im| := Complex.norm_le_abs_re_add_abs_im _\n  have hre : |ρ.1.re| ≤ 1 := by\n    have h1 : 0 < ρ.1.re := ρ.2.2.1\n    have h2 : ρ.1.re < 1 := ρ.2.2.2\n    rw [abs_le]\n    constructor <;> linarith\n  have him : |ρ.1.im| ≤ |t| + 1 := by\n    calc |ρ.1.im| = |ρ.1.im - t + t| := by rw [sub_add_cancel]\n      _ ≤ |ρ.1.im - t| + |t| := abs_add_le _ _\n      _ ≤ 1 + |t| := by linarith [h]\n      _ = |t| + 1 := by ring\n  linarith [hle, hre, him]\n\n/-! ## 3. The seriesFun difference identity -/\n\n/-- The seriesFun difference term (a def so the tsum split matches\nsyntactically — no beta-redexes). -/\ndef seriesDiffTerm (s s₀ : ℂ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=\n  (zeroMult ρ.1 : ℂ) * (1 / (s - ρ.1) - 1 / (s₀ - ρ.1))\n\n/-- The difference series is summable (the two seriesFun summabilities). -/\ntheorem seriesDiffTerm_summable (s s₀ : ℂ) :\n    Summable (seriesDiffTerm s s₀) := by\n  apply Summable.congr (Summable.sub seriesSummable seriesSummable)\n  intro ρ\n  show seriesTerm s ρ - seriesTerm s₀ ρ = seriesDiffTerm s s₀ ρ\n  rw [seriesDiffTerm, seriesTerm, seriesTerm]\n  ring\n\n/-- seriesFun s − seriesFun s₀ as the termwise difference series. -/\ntheorem seriesFun_sub_seriesFun (s s₀ : ℂ) :\n    seriesFun s - seriesFun s₀ = ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ},\n      seriesDiffTerm s s₀ ρ := by\n  rw [seriesFun, seriesFun, ← tsum_sub seriesSummable seriesSummable]\n  refine tsum_congr fun ρ => ?_\n  show seriesTerm s ρ - seriesTerm s₀ ρ = seriesDiffTerm s s₀ ρ\n  rw [seriesDiffTerm, seriesTerm, seriesTerm]\n  ring\n\n/-! ## 4. The reference-point decomposition -/\n\n/-- **The six-piece reference-point decomposition** (D-056 §2, D-069 §3):\nwith both s and s₀ good (so `partialFraction_identity` applies at both —\nB cancels), the R-expression at s equals: the reference value, minus the\nnear sum at s₀, plus the far difference series, minus the elementary\ndifferences, minus 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 : ℂ) else seriesDiffTerm s s₀ ρ)\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  have hdiff := seriesFun_sub_seriesFun s s₀\n  have hsplit := tsum_split_finset_complex (seriesDiffTerm_summable s s₀) (nearZerosSub t)\n  have hnear : ∑ ρ ∈ nearZerosSub t, seriesDiffTerm s s₀ ρ\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 [seriesDiffTerm, div_eq_mul_one_div, div_eq_mul_one_div]\n    ring\n  linear_combination hsid - hs₀id + hdiff + hsplit + hnear\n\n/-! ## 5. Piece 2: the near sum at the reference point -/\n\n/-- **Piece 2** (D-069 §3, honest two-unit form): the near sum at\ns₀ = 2 + it is bounded by the ZeroCountProp2 count, since\n|s₀ − ρ| ≥ 2 − re ρ ≥ 1 for every nontrivial 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  classical\n  have hterm : ∀ ρ : {ρ : ℂ // IsNontrivialZero ρ}, ρ ∈ nearZerosSub t →\n      ‖(zeroMult ρ.1 : ℂ) / ((2 + t * Complex.I) - ρ.1)‖ ≤ (zeroMult ρ.1 : ℝ) := by\n    intro ρ _\n    have hρre : ρ.1.re < 1 := ρ.2.2.2\n    have h1 : (1 : ℝ) ≤ ‖(2 + t * Complex.I) - ρ.1‖ := by\n      have hre : ((2 + t * Complex.I) - ρ.1).re = 2 - ρ.1.re := by simp\n      have h := abs_re_le_norm ((2 + t * Complex.I) - ρ.1)\n      rw [hre] at h\n      have h2 : (1 : ℝ) ≤ |2 - ρ.1.re| := by\n        rw [abs_of_nonneg (by linarith)]\n        linarith\n      exact h2.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 _)\n    rw [h2]\n    calc (zeroMult ρ.1 : ℝ) / ‖(2 + t * Complex.I) - ρ.1‖\n        ≤ (zeroMult ρ.1 : ℝ) / 1 :=\n          div_le_div_of_nonneg_left (Nat.cast_nonneg _)\n            (by norm_num : (0 : ℝ) < 1) h1\n      _ = (zeroMult ρ.1 : ℝ) := div_one _\n  have hbridge : ∑ ρ ∈ nearZerosSub t, (zeroMult ρ.1 : ℝ)\n      = ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := by\n    rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n  have hsub : (nearZerosSub t).image (fun ρ => ρ.1)\n      ⊆ (zeroAbsWindow_finite t).toFinset := by\n    intro ρ hρ\n    rw [Finset.mem_image] at hρ\n    obtain ⟨ρ', hρ'mem, hρ'eq⟩ := hρ\n    have hnear := mem_nearZerosSub.mp hρ'mem\n    rw [Set.Finite.mem_toFinset]\n    show IsNontrivialZero ρ ∧ |ρ.im - t| ≤ 1\n    rw [← hρ'eq]\n    exact ⟨ρ'.2, hnear.le⟩\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    _ = ∑ ρ ∈ (nearZerosSub t).image (fun ρ => ρ.1), (zeroMult ρ : ℝ) := hbridge\n    _ ≤ ∑ ρ ∈ (zeroAbsWindow_finite t).toFinset, (zeroMult ρ : ℝ) :=\n        Finset.sum_le_sum_of_subset_of_nonneg hsub (fun ρ _ _ => Nat.cast_nonneg _)\n    _ = (((zeroAbsWindow_finite t).toFinset.sum fun ρ => zeroMult ρ) : ℝ) := by\n        push_cast\n        rfl\n    _ ≤ 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7 :=\n        hZC2 t ht\n\n/-! ## 6. Pieces 4/5: the reciprocal differences -/\n\n/-- **Pieces 4/5** (D-056 §2): the elementary reciprocal differences,\neach ≤ 4.5/|t|² ≤ 0.045 (|s₀ − s| = |2 − σ| ≤ 4.5; ‖s‖, ‖s₀‖ ≥ t). -/\ntheorem one_div_diff_le {t : ℝ} (ht : 10 ≤ t) {s : ℂ}\n    (hσlo : -5 / 2 ≤ s.re) (hσhi : s.re ≤ 3) (him : s.im = t) (hs0 : s ≠ 0) :\n    ‖1 / s - 1 / (2 + t * Complex.I)‖ ≤ 0.045 ∧\n      ‖1 / (s - 1) - 1 / ((2 + t * Complex.I) - 1)‖ ≤ 0.045 := by\n  have ht0 : (0 : ℝ) < t := by linarith\n  -- the difference s₀ − s is the real (2 − s.re)\n  have hdiff : (2 + t * Complex.I) - s = ((2 - s.re : ℝ) : ℂ) := by\n    rw [← Complex.ext_iff]\n    constructor\n    · simp\n    · simp [him]\n  have hsdiff : ‖(2 + t * Complex.I) - s‖ = |2 - s.re| := by\n    rw [hdiff]\n    exact Complex.norm_real _\n  have hsdiffle : ‖(2 + t * Complex.I) - s‖ ≤ 4.5 := by\n    rw [hsdiff, abs_le]\n    constructor <;> linarith\n  have hs_norm : (t : ℝ) ≤ ‖s‖ := by\n    have h := abs_im_le_norm s\n    rw [him, abs_of_nonneg ht0.le] at h\n    exact h\n  have hs0_norm : (t : ℝ) ≤ ‖2 + t * Complex.I‖ := by\n    have h := abs_im_le_norm (2 + t * Complex.I)\n    rw [show (2 + t * Complex.I).im = t by simp, abs_of_nonneg ht0.le] at h\n    exact h\n  have hsm1_norm : (t : ℝ) ≤ ‖s - 1‖ := by\n    have h := abs_im_le_norm (s - 1)\n    rw [show (s - 1).im = t by simp [him], abs_of_nonneg ht0.le] at h\n    exact h\n  have hs0m1_norm : (t : ℝ) ≤ ‖(2 + t * Complex.I) - 1‖ := by\n    have h := abs_im_le_norm ((2 + t * Complex.I) - 1)\n    rw [show ((2 + t * Complex.I) - 1).im = t by simp, abs_of_nonneg ht0.le] at h\n    exact h\n  have hprods : (100 : ℝ) ≤ ‖s‖ * ‖2 + t * Complex.I‖ := by\n    have h1 := mul_le_mul hs_norm hs0_norm ht0.le (by positivity : (0 : ℝ) ≤ ‖s‖)\n    nlinarith [h1, ht]\n  have hprods1 : (100 : ℝ) ≤ ‖s - 1‖ * ‖(2 + t * Complex.I) - 1‖ := by\n    have h1 := mul_le_mul hsm1_norm hs0m1_norm ht0.le (by positivity : (0 : ℝ) ≤ ‖s - 1‖)\n    nlinarith [h1, ht]\n  constructor\n  · -- 1/s − 1/s₀\n    have hs₀0 : (2 + t * Complex.I) ≠ 0 := by\n      intro h\n      have : (2 + t * Complex.I).re = 0 := by rw [h]; simp\n      simp at this\n    rw [div_sub_div _ _ hs0 hs₀0]\n    have hnum : 1 * (2 + t * Complex.I) - s * 1 = (2 + t * Complex.I) - s := by ring\n    rw [hnum, norm_div, norm_mul]\n    calc ‖(2 + t * Complex.I) - s‖ / (‖s‖ * ‖2 + t * Complex.I‖)\n        ≤ 4.5 / (‖s‖ * ‖2 + t * Complex.I‖) :=\n          div_le_div_of_nonneg_right hsdiffle (by positivity)\n      _ ≤ 4.5 / 100 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) hprods\n      _ = 0.045 := by norm_num\n  · -- 1/(s−1) − 1/(s₀−1)\n    have hs1 : s - 1 ≠ 0 := by\n      intro h\n      have : (s - 1).im = 0 := by rw [h]; simp\n      rw [show (s - 1).im = t by simp [him]] at this\n      linarith\n    have hs₀1 : (2 + t * Complex.I) - 1 ≠ 0 := by\n      intro h\n      have : ((2 + t * Complex.I) - 1).re = 0 := by rw [h]; simp\n      simp at this\n    rw [div_sub_div _ _ hs1 hs₀1]\n    have hnum : 1 * ((2 + t * Complex.I) - 1) - (s - 1) * 1\n        = (2 + t * Complex.I) - s := by ring\n    rw [hnum, norm_div, norm_mul]\n    calc ‖(2 + t * Complex.I) - s‖ / (‖s - 1‖ * ‖(2 + t * Complex.I) - 1‖)\n        ≤ 4.5 / (‖s - 1‖ * ‖(2 + t * Complex.I) - 1‖) :=\n          div_le_div_of_nonneg_right hsdiffle (by positivity)\n      _ ≤ 4.5 / 100 := div_le_div_of_nonneg_left (by norm_num) (by norm_num) hprods1\n      _ = 0.045 := by norm_num\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]