[{"type":"thinking","thinking":"`Complex.continuous_conj : Continuous (conj : ℂ → ℂ)` ✓. And (starRingEnd ℂ) x = conj x — `starRingEnd_apply` simp lemma. To avoid mixing, I'll state everything with (starRingEnd ℂ) and bridge to conj via starRingEnd_apply, or just use `(starRingEnd ℂ)` and its continuity: (starRingEnd ℂ) as a function ℂ → ℂ equals conj (they're definitionally equal? starRingEnd ℂ = { conj } as a RingEquiv — applying it: (starRingEnd ℂ) x = conj x by rfl? Probably `starRingEnd_apply : (starRingEnd R) x = conj x` simp lemma ✓). For continuity: `starRingEnd_continuous`?? not found — use: `show Continuous ((starRingEnd ℂ) : ℂ → ℂ)` — it's defeq to conj? The ZetaReflect usage: `(Complex.continuous_conj).tendsto (conj w)` and starRingEnd elsewhere — there might be coercion friction. Simplest: convert with `starRingEnd_apply` rewrites and use Complex.continuous_conj:\n```\nhave hconjcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) := by\n  simp only [starRingEnd_apply]\n  exact Complex.continuous_conj\n```\nHmm — (starRingEnd ℂ) as a function: `⇑(starRingEnd ℂ)` — simp only [starRingEnd_apply] should turn the goal Continuous ⇑(starRingEnd ℂ) into Continuous conj... Actually `starRingEnd_apply : (starRingEnd R) x = conj x` — for the function-level: funext or `show Continuous (conj : ℂ → ℂ)` then exact. Let me use: \n```\nhave hconjcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) :=\n  Complex.continuous_conj\n```\n— is ⇑(starRingEnd ℂ) DEFEQ to conj? The starRingEnd is a structure with toFun = conj — the coercion ⇑(starRingEnd ℂ) should be defeq to conj ✓ try it.\n\nNow write §13 (C0hat bridges) and §14 (conj machinery). Let me draft the C0hat bridges concretely.\n\nFor C0hat_two_mul_add_one_le (k ≥ 11):\n```\nlemma C0hat_two_mul_add_one_le {k : ℕ} (hk : 11 ≤ k) :\n    C0hat (2 * (k : ℝ) + 1)\n      ≤ 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n  have hkR : (11 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n  have hk0 : (0 : ℝ) < (k : ℝ) := by linarith\n  have hlogk : (2.3978 : ℝ) ≤ Real.log k := by\n    have h2a := log_eleven_ge\n    have h2b : Real.log 11 ≤ Real.log k := Real.log_le_log (by norm_num : (0:ℝ) < 11) hkR\n    linarith [h2a, h2b]\n  have hlogpos : (0 : ℝ) < Real.log k := by linarith [hlogk]\n  -- the log increment\n  have hinc1 : Real.log (2 * (k : ℝ) + 3) ≤ Real.log k + 0.833 := by\n    have h2 : (2 : ℝ) * (k : ℝ) + 3 ≤ 2.3 * (k : ℝ) := by linarith [hkR]\n    have h3 : Real.log (2 * (k : ℝ) + 3) ≤ Real.log (2.3 * (k : ℝ)) :=\n      Real.log_le_log (by positivity : (0:ℝ) < 2 * (k:ℝ) + 3) h2\n    have h4 : Real.log (2.3 * (k : ℝ)) = Real.log 2.3 + Real.log k :=\n      Real.log_mul (by norm_num : (2.3 : ℝ) ≠ 0) hk0.ne'\n    have h5 := log_two_point_three_le\n    linarith [h3, h4 ▸ h3, h5]  -- careful: h4 ▸ h3 rewrites; simpler: rw [h4] at h3; linarith\n  -- the loglog increment\n  have hinc2 : Real.log (Real.log (2 * (k : ℝ) + 3))\n      ≤ Real.log (Real.log k) + 0.3475 := by\n    have h6 : Real.log (Real.log (2 * (k : ℝ) + 3)) ≤ Real.log (Real.log k + 0.833) := by\n      apply Real.log_le_log (by positivity : (0:ℝ) < Real.log (2*(k:ℝ)+3)) hinc1\n    have h7 : Real.log (Real.log k + 0.833)\n        ≤ Real.log (Real.log k) + 0.833 / Real.log k := by\n      have h8 : Real.log k + 0.833 = Real.log k * (1 + 0.833 / Real.log k) := by\n        field_simp [hlogpos.ne']\n        ring\n      rw [h8, Real.log_mul hlogpos.ne' (by positivity : (1:ℝ) + 0.833/Real.log k ≠ 0)]\n      have h9 : Real.log (1 + 0.833 / Real.log k) ≤ 0.833 / Real.log k :=\n        Real.log_le_sub_one_of_pos (by positivity : (0:ℝ) < 1 + 0.833/Real.log k)\n      linarith [h9]\n    have h10 : (0.833 : ℝ) / Real.log k ≤ 0.3475 := by\n      rw [div_le_iff₀ hlogpos]\n      have h11 : (0.3475 : ℝ) * 2.3978 ≤ 0.3475 * Real.log k :=\n        mul_le_mul_of_nonneg_left hlogk (by norm_num)\n      have h12 : (0.833 : ℝ) ≤ 0.3475 * 2.3978 := by norm_num\n      exact h12.trans h11\n    linarith [h6, h7, h10]\n  -- assemble\n  rw [C0hat]\n  have harg : (2 : ℝ) * (k : ℝ) + 1 + 2 = 2 * (k : ℝ) + 3 := by ring\n  rw [harg]\n  linarith [hinc1, hinc2]\n```\nCheck the final: C0hat(2k+1) = 0.433·log(2k+1+2) + 0.886·loglog(2k+1+2) + 2.9 = 0.433·log(2k+3)+0.886·loglog(2k+3)+2.9 ≤ 0.433·(log k+0.833)+0.886·(loglog k+0.3475)+2.9 ⟸ 0.433·hinc1 + 0.886·hinc2 (coeffs nonneg) — linarith with the coefficient nonnegativity: linarith can't multiply hinc1 by 0.433 (nonlinear: 0.433·(log k + 0.833) — the term log k·0.433 is nonlinear in the atom view? linarith treats 0.433·log(2k+3) ≤ 0.433·(log k+0.833) as linear in the atoms log(2k+3), log k, 0.833-constants ✓ linarith CAN multiply hypotheses by positive rational constants internally (it's linear arithmetic) ✓.\n\nFor C0hat_add_one_le_of_fourteen_le (j ≥ 14): same skeleton with 0.1942/0.0736 and log_17_14_le/log_fourteen_ge:\n```\nlemma C0hat_add_one_le_of_fourteen_le {j : ℕ} (hj : 14 ≤ j) :\n    C0hat ((j : ℝ) + 1)\n      ≤ 0.433 * (Real.log j + 0.1942) + 0.886 * (Real.log (Real.log j) + 0.0736) + 2.9\n```\n- hinc1: log(j+3) ≤ log j + 0.1942: j+3 ≤ (17/14)j ⟺ 3 ≤ (3/14)j ⟺ j ≥ 14 ✓: log(j+3) ≤ log((17/14)j) = log(17/14)+log j ≤ 0.1942+log j ✓.\n  ((j:ℝ)+1)+2 = (j:ℝ)+3 ✓ harg.\n- hinc2: loglog(j+3) ≤ loglog j + 0.1942/log j ≤ loglog j + 0.0736: log j ≥ log 14 ≥ 2.6388: 0.1942/2.6388 = 0.073594 ≤ 0.0736: via div_le_iff₀: 0.1942 ≤ 0.0736·log j: 0.0736·2.6388 = 0.19422 ≥ 0.1942 ✓ norm_num: 0.0736·2.6388 = 0.19421568 ≥ 0.1942 ✓.\n\nFor C0hat_two_t_add_one_le (t ≥ 10):\n```\nlemma C0hat_two_t_add_one_le {t : ℝ} (ht : 10 ≤ t) :\n    C0hat (2 * t + 1) ≤ C0hat (t + 1) + 0.55 := by\n  have ht3 : (0 : ℝ) < t + 3 := by linarith\n  have hlog13 : (2.5 : ℝ) ≤ Real.log (t + 3) := by\n    have h1 : Real.log 13 ≤ Real.log (t + 3) :=\n      Real.log_le_log (by norm_num : (0:ℝ) < 13) (by linarith : (13:ℝ) ≤ t + 3)\n    have h2 := log_thirteen_ge_five  -- the new lemma log 13 ≥ 2.5\n    linarith [h1, h2]\n  -- log increment: log(2t+3) ≤ log 2 + log(t+3)\n  have hinc1 : Real.log (2 * t + 3) ≤ Real.log 2 + Real.log (t + 3) := by\n    have h1 : (2 : ℝ) * t + 3 ≤ 2 * (t + 3) := by linarith\n    have h2 : Real.log (2 * t + 3) ≤ Real.log (2 * (t + 3)) :=\n      Real.log_le_log (by positivity) h1\n    have h3 : Real.log (2 * (t + 3)) = Real.log 2 + Real.log (t + 3) :=\n      Real.log_mul (by norm_num : (2:ℝ) ≠ 0) ht3.ne'\n    linarith [h2, h3 ▸ h2]  -- rw [h3] at h2 instead\n  -- loglog increment: loglog(2t+3) ≤ loglog(t+3) + 0.6932/2.5\n  ...\n```\nlog_thirteen_ge_five : (2.5 : ℝ) ≤ Real.log 13: via 13 ≥ e^2.5:\n```\nlemma exp_two_point_five_le_thirteen : Real.exp 2.5 ≤ 13 := by\n  have h1 : Real.exp 2.5 = Real.exp 1 * Real.exp 1 * Real.exp 0.5 := by\n    rw [← Real.exp_add, ← Real.exp_add]\n    congr 1\n    norm_num\n  have he1 : (2.7182818 : ℝ) ≤ Real.exp 1 := ...\n  have he2 : Real.exp 1 ≤ (2.7182819 : ℝ) := ...\n  have he5 : Real.exp 0.5 ≤ (1.6488 : ℝ) := by\n    have h2 : Real.exp 0.5 * Real.exp 0.5 = Real.exp 1 := by\n      rw [← Real.exp_add]\n      congr 1\n      norm_num\n    have h3 : Real.exp 0.5 * Real.exp 0.5 ≤ 1.6488 * 1.6488 := by\n      rw [h2]\n      calc Real.exp 1 ≤ 2.7182819 := he2\n        _ ≤ 1.6488 * 1.6488 := by norm_num\n    have h4 : (0 : ℝ) ≤ Real.exp 0.5 := (Real.exp_pos 0.5).le\n    nlinarith [h3, h4, Real.exp_pos 0.5]\n  rw [h1]\n  have h5 : Real.exp 1 * Real.exp 1 * Real.exp 0.5 ≤ 2.7182819 * 2.7182819 * 1.6488 := by\n    apply mul_le_mul\n    · exact mul_le_mul he2 he2 (Real.exp_pos 1).le (by norm_num)\n    · exact he5\n    · exact (Real.exp_pos 0.5).le\n    · positivity\n  have h6 : (2.7182819 : ℝ) * 2.7182819 * 1.6488 ≤ 13 := by norm_num\n  exact h5.trans h6\nlemma log_thirteen_ge_five : (2.5 : ℝ) ≤ Real.log 13 := by\n  rw [Real.le_log_iff_exp_le (by norm_num : (0:ℝ) < 13)]\n  exact exp_two_point_five_le_thirteen\n```\nnlinarith for he5: (exp 0.5)² ≤ 1.6488² with exp 0.5 ≥ 0, 1.6488 ≥ 0 ⟹ exp 0.5 ≤ 1.6488 — nlinarith [h3, h4]: from (e05)² ≤ (1.6488)² and e05 ≥ 0 ⟹ e05 ≤ 1.6488: nlinarith needs: (1.6488−e05)(1.6488+e05) ≥ 0 ⟹ ... give nlinarith the product hint: nlinarith [h3, h4, mul_nonneg (by linarith : (0:ℝ) ≤ 1.6488 - Real.exp 0.5 + 2*Real.exp 0.5)...] — simpler: use sq_le_sq: |e05| ≤ |1.6488| ⟸ e05² ≤ 1.6488²: `abs_le_abs_of_nonneg`?? there's `sq_le_sq'`? or `pow_le_pow_left₀`-inverse: `le_of_pow_le_pow_left₀ (n ≠ 0) (hb : 0 ≤ b) (h : a^n ≤ b^n) : a ≤ b` — `le_of_pow_le_pow_left₀ (by norm_num : (2:ℕ) ≠ 0) (by norm_num : (0:ℝ) ≤ 1.6488) h3'` — where h3' : (Real.exp 0.5)^2 ≤ (1.6488)^2. Let me use that: \n```\n    have h3' : Real.exp 0.5 ^ 2 ≤ (1.6488 : ℝ) ^ 2 := by\n      have h2 : Real.exp 0.5 ^ 2 = Real.exp 1 := by\n        rw [sq, ← Real.exp_add]\n        congr 1\n        norm_num\n      rw [h2]\n      calc Real.exp 1 ≤ 2.7182819 := he2\n        _ ≤ (1.6488 : ℝ) ^ 2 := by norm_num\n    exact le_of_pow_le_pow_left₀ (by norm_num : (2:ℕ) ≠ 0) (by norm_num : (0:ℝ) ≤ 1.6488) h3'\n```\n`le_of_pow_le_pow_left₀ : n ≠ 0 → 0 ≤ b → a ^ n ≤ b ^ n → a ≤ b` ✓ exists (root-namespace or _root_). \n\nThe hloglog increment for C0hat_two_t_add_one_le: loglog(2t+3) ≤ loglog(t+3) + 0.6932/2.5:\n```\n  have hinc2 : Real.log (Real.log (2 * t + 3))\n      ≤ Real.log (Real.log (t + 3)) + 0.6932 / 2.5 := by\n    have h6 : Real.log (Real.log (2 * t + 3)) ≤ Real.log (Real.log (t + 3) + Real.log 2) := by\n      apply Real.log_le_log (by positivity : (0:ℝ) < Real.log (2*t+3)) \n      linarith [hinc1]  -- log(2t+3) ≤ log(t+3) + log 2 ✓\n    have h7 : Real.log (Real.log (t + 3) + Real.log 2)\n        ≤ Real.log (Real.log (t + 3)) + Real.log 2 / Real.log (t + 3) := by\n      <same log(a+c) machine with a = log(t+3) ≥ 2.5, c = log 2 ≤ 0.6932>\n    have h10 : Real.log 2 / Real.log (t + 3) ≤ 0.6932 / 2.5 := by\n      <log 2 ≤ 0.6932 (log_two_lt_d9) and log(t+3) ≥ 2.5: div_le_div: 0.6932/2.5 form>\n    linarith [h6, h7, h10]\n```\nThe div: log 2/log(t+3) ≤ 0.6932/2.5 ⟺ via div_le_div (log 2 ≤ 0.6932) (2.5 ≤ log(t+3)) (pos) (pos): `div_le_div h2a h2b (by positivity) (by positivity)`? div_le_div (hab : a ≤ b) (hbc : c ≤ d)?? — the four-arg: div_le_div (h₁ : a ≤ b) (h₂ : c ≤ d) (hc : 0 ≤ c) (hd : 0 < d)?? hmm — `div_le_div (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 < b) : a / d ≤ b / c`?? Signature guess: div_le_div (h₁ : a ≤ b) (h₂ : c ≤ d) (hc : 0 ≤ c) (hd : 0 < d) : a / d ≤ b / c. For log 2/log(t+3) ≤ 0.6932/2.5: a = log 2, b = 0.6932, c = 2.5, d = log(t+3): a/d ≤ b/c ⟺ log 2/log(t+3) ≤ 0.6932/2.5 ✓ with h₁ : log 2 ≤ 0.6932 (log_two_lt_d9.le.trans norm_num), h₂ : 2.5 ≤ log(t+3) (hlog13), hc : 0 ≤ 2.5 (norm_num), hd : 0 < log(t+3) (linarith). If the signature differs, adjust at compile.\n\nFinal assembly C0hat_two_t_add_one_le:\n```\n  rw [C0hat, C0hat]\n  have harg1 : (2 : ℝ) * t + 1 + 2 = 2 * t + 3 := by ring\n  have harg2 : (t : ℝ) + 1 + 2 = t + 3 := by ring\n  rw [harg1, harg2]\n  -- 0.433·log(2t+3) + 0.886·loglog(2t+3) + 2.9 ≤ 0.433·log(t+3)+0.886·loglog(t+3)+2.9+0.55\n  have hlog2le := Real.log_two_lt_d9.le.trans (by norm_num : (0.6931471809:ℝ) ≤ 0.6932)\n  linarith [hinc1, hinc2, hlog2le]\n```\nCheck the arithmetic: LHS ≤ 0.433·(log 2 + log(t+3)) + 0.886·(loglog(t+3)+0.6932/2.5) + 2.9 = 0.433·log(t+3)+0.886·loglog(t+3)+2.9 + [0.433·log 2 + 0.886·0.27728] = RHS + [0.433·0.69315+0.24567] = RHS + 0.54583 ≤ RHS + 0.55 ✓ (linarith with log 2 ≤ 0.6932: 0.433·0.6932+0.886·(0.6932/2.5) = 0.30015+0.24583·... compute: 0.886·0.6932/2.5 = 0.245666; 0.433·0.6932 = 0.300156; sum = 0.545822 ≤ 0.55 ✓ linarith verifies via the atoms).\n\nAlso needed: `log_le_log_add` machine used twice — factor it as a lemma:\n```\nlemma log_add_le (a c : ℝ) (ha : 0 < a) (hc : 0 ≤ c) :\n    Real.log (a + c) ≤ Real.log a + c / a := by\n  have h1 : a + c = a * (1 + c / a) := by field_simp [ha.ne']; ring\n  rw [h1, Real.log_mul ha.ne' (by positivity : (1 : ℝ) + c / a ≠ 0)]\n  have h2 : Real.log (1 + c / a) ≤ c / a :=\n    Real.log_le_sub_one_of_pos (by positivity : (0 : ℝ) < 1 + c / a)\n  linarith [h2]\n```\n✓ nice and reusable.\n\nNow — before writing, also double-check `Real.log_two_lt_d9` (used in dirichletC2_le_one as `Real.log_two_lt_d9.le.trans (by norm_num)` : log 2 ≤ 0.6932 ✓).\n\nLet me now write §13 (C0hat bridges) + §14 (conj machinery) as one edit. §14's hasDerivAt_conj_of_conj_eq is the delicate one — let me write it very carefully:\n\n```\n/-- The conjugate-derivative lemma: if f commutes with conjugation near\nconj z and is differentiable at z, then f has derivative conj(deriv f z)\nat conj z. -/\nlemma hasDerivAt_conj_of_conj_eq {f : ℂ → ℂ} {z : ℂ}\n    (hconj : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z),\n      f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f s))\n    (hdiff : DifferentiableAt ℂ f z) :\n    HasDerivAt f ((starRingEnd ℂ) (deriv f z)) ((starRingEnd ℂ) z) := by\n  have h1 : Filter.Tendsto (fun x : ℂ => (f x - f z) / (x - z)) (𝓝[≠] z)\n      (𝓝 (deriv f z)) :=\n    hasDerivAt_iff_tendsto.mp hdiff.hasDerivAt\n  have hmap : Filter.Tendsto (starRingEnd ℂ) (𝓝[≠] ((starRingEnd ℂ) z)) (𝓝[≠] z) := by\n    have hcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) := Complex.continuous_conj\n    have hT := hcont.tendsto ((starRingEnd ℂ) z)\n    rw [Filter.tendsto_nhdsWithin_iff]\n    refine ⟨hT.mono_left Filter.nhdsWithin_le_nhds, ?_⟩\n    rw [Filter.eventually_nhdsWithin_iff]\n    exact Filter.Eventually.of_forall (fun x hx => by\n      show (starRingEnd ℂ) x ∈ {z}ᶜ\n      rw [Set.mem_compl_singleton_iff]\n      intro hbad\n      apply hx\n      have h3 := congrArg (starRingEnd ℂ) hbad\n      rwa [starRingEnd_self_apply, map_one?] at h3)\n  ...\n```\nHmm wait — hx : x ∈ {conj z}ᶜ i.e. x ≠ conj z; want conj x ≠ z: conj x = z ⟹ conj(conj x) = conj z ⟹ x = conj z ✓ contradiction. The congrArg route: hbad : (starRingEnd ℂ) x = z — apply conj: (starRingEnd ℂ)((starRingEnd ℂ) x) = (starRingEnd ℂ) z — LHS = x (starRingEnd_self_apply) — so x = (starRingEnd ℂ) z ✓ contradicts hx. The `map_one?` is wrong — I need: from hbad, congrArg (starRingEnd ℂ) hbad : conj(conj x) = conj z, then starRingEnd_self_apply at LHS: x = conj z ✓: rwa [starRingEnd_self_apply] at h3 — then h3 : x = (starRingEnd ℂ) z, and hx : x ≠ (starRingEnd ℂ) z — exact hx h3 ✓. But careful: nhdsWithin's eventual: x ∈ {conj z}ᶜ — the mem form: eventually x in 𝓝[≠] (conj z): x ≠ conj z ✓ hx : x ∈ {(starRingEnd ℂ) z}ᶜ or x ≠ ... Let me write:\n```\n    exact Filter.Eventually.of_forall (fun x (hx : x ≠ (starRingEnd ℂ) z) => by\n      show (starRingEnd ℂ) x ≠ z\n      intro hbad\n      apply hx\n      have h3 := congrArg (starRingEnd ℂ) hbad\n      rwa [starRingEnd_self_apply] at h3)\n```\n— the eventually_nhdsWithin_iff's second component: ∀ᶠ x in 𝓝 (conj z), x ∈ s → x ∈ conj ⁻¹' s — with s = {conj z}ᶜ: x ≠ conj z → conj x ≠ z ✓ the form `x ∈ {z}ᶜ` — mem_compl_singleton_iff: x ∈ {z}ᶜ ↔ x ≠ z ✓. Let me write it with the set-membership forms and let simp bridge.\n\nThen the composition:\n```\n  have h2 : Filter.Tendsto (fun x : ℂ =>\n      (starRingEnd ℂ) ((f ((starRingEnd ℂ) x) - f z) / (((starRingEnd ℂ) x) - z)))\n      (𝓝[≠] ((starRingEnd ℂ) z)) (𝓝 ((starRingEnd ℂ) (deriv f z))) := by\n    have hcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) := Complex.continuous_conj\n    exact (hcont.tendsto _).comp (h1.comp hmap)\n```\nThen the EventuallyEq of h2's function and the standard slope:\n```\n  have h3 : (fun x : ℂ => (f x - f ((starRingEnd ℂ) z)) / (x - (starRingEnd ℂ) z))\n      =ᶠ[𝓝[≠] ((starRingEnd ℂ) z)] fun x : ℂ =>\n      (starRingEnd ℂ) ((f ((starRingEnd ℂ) x) - f z) / (((starRingEnd ℂ) x) - z)) := by\n    have hcz : ((starRingEnd ℂ) z) ≠ z → True := fun _ => trivial  -- unused\n    apply Filter.EventuallyEq.filter_mono ?_ Filter.nhdsWithin_le_nhds\n    -- work in 𝓝 (conj z): eventually hconj\n    exact hconj.mono (fun s hs => by\n      rw [hs]\n      simp only [map_sub, map_div₀, starRingEnd_self_apply])\n  exact hasDerivAt_iff_tendsto.mpr (Filter.Tendsto.congr' h3 h2)\n```\nCheck the pointwise step: at s with hconj : f (conj s) = conj (f s): goal: (f s − f(conj z))/(s − conj z) = conj((f(conj s) − f z)/((conj s) − z)): rw [hs]: RHS = conj((conj(f s) − f z)/((conj s) − z)): simp [map_sub, map_div₀, starRingEnd_self_apply]: conj(a−b) = conj a − conj b ✓; conj(a/b) = conj a/conj b ✓; conj(conj u) = u ✓; also need conj(f z) = f(conj z) — NOT from simp! The hconj hypothesis at s gives f(conj s) = conj(f s) — I need the identity at z too: f(conj z) = conj(f z). But hconj is only eventually near conj z — does it include z?? hconj : ∀ᶠ s in 𝓝 (conj z) — the point z is NOT necessarily near conj z!! (z vs conj z could be far apart — e.g. z = 1+i.) Hmm — wait: hconj is around conj z; I need the identity at points s near conj z (for the slope evaluation) AND at z (for the f z term). At z: z is the CENTER of... no — hconj is centered at conj z, so it covers s near conj z, not z. The identity at z (f(conj z) = conj(f z)) is NOT covered unless z is near conj z. PROBLEM!\n\nHmm — wait, actually: in the EventuallyEq, the term f z appears — I need conj(f z) = f(conj z), which is hconj AT THE POINT z. In the inductive application, the identity itD n ζ (conj s) = conj(itD n ζ s) holds for ALL s ≠ 1 — including s = z (z ≠ 1 ✓). So hconj eventually + the z-point separately. Simplest: strengthen the hypothesis to: hconj holds at z AND eventually near conj z. Or make hconj : ∀ s, ... in a SET containing z ∪ nhd(conj z). Cleanest: two hypotheses (hzc : f (conj z) = conj (f z)) (hconj : ∀ᶠ s in 𝓝 (conj z), ...). For the ζ-induction: hzc from ih z hz ✓; hconj eventually ✓.\n\nHmm — actually simpler: note that the slope function at x needs f(conj x) = conj(f x) (hconj at x near conj z ✓) and the IDENTITY at z only enters via conj(f z) = f(conj z) — since this is a FIXED value (not varying with x), I can rewrite it as a standalone hypothesis. Let me restructure with both. Actually — cleanest: make hconj : ∀ s ∈ (nhd of conj z ∪ {z})... overkill. Two hypotheses:\n\n(hzid : f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (f z))\n(hconj : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z), f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f s))\n\nThen the pointwise step: rw [hs] (hconj at s) and rw [hzid]?? — hzid : f(conj z) = conj(f z): the goal has f(conj z) on the LHS and conj(f z) inside the RHS-conj: rw [hzid] rewrites f(conj z) → conj(f z) — then LHS = (f s − conj(f z))/(s − conj z); RHS = conj((conj(f s) − f z)/(conj s − z)) → simp [map_sub, map_div₀, starRingEnd_self_apply] → (f s − conj(f z))/(s − conj z) ✓ equal ✓.\n\nOK — and in the induction: hzid := ih hz (the identity at z ✓); hconj := eventually near conj z: conj z ≠ 1 ⟹ eventually s ≠ 1 ⟹ ih s hs ✓.\n\nThe eventually-ne: `eventually_ne_nhds (h : conj z ≠ 1) : ∀ᶠ s in 𝓝 (conj z), s ≠ 1` — name check: `eventually_ne_nhds : x ≠ a → ∀ᶠ y in 𝓝 x, y ≠ a`? — I believe `eventually_ne_nhds (h : x ≠ a) : ∀ᶠ (y) in 𝓝 x, y ≠ a` exists. If not: `isOpen_compl_singleton.eventually_nhds`? There's `IsOpen.eventually_nhds`: isOpen_compl_singleton : IsOpen {a}ᶜ: (isOpen_compl_singleton.eventually_nhds ?). Let me use: `(isOpen_compl_singleton.eventually_nhds h)`?? hmm — `IsOpen.eventually_nhds : IsOpen s → x ∈ s → ∀ᶠ y in 𝓝 y, y ∈ s`: (isOpen_compl_singleton (𝕜 := ℂ)).eventually_nhds (show conj z ∈ {1}ᶜ from ...) — then ∀ᶠ s, s ∈ {1}ᶜ = s ≠ 1 ✓. I'll write it and adjust.\n\nAlso hdiff.hasDerivAt: DifferentiableAt.hasDerivAt ✓.\n\nNow the iteratedDeriv_riemannZeta_conj:\n```\nlemma iteratedDeriv_riemannZeta_conj (n : ℕ) {z : ℂ} (hz : z ≠ 1) :\n    iteratedDeriv n riemannZeta ((starRingEnd ℂ) z)\n      = (starRingEnd ℂ) (iteratedDeriv n riemannZeta z) := by\n  induction n generalizing z with\n  | zero =>\n    rw [iteratedDeriv_zero, iteratedDeriv_zero]\n    exact riemannZeta_conj z\n  | succ n ih =>\n    rw [iteratedDeriv_succ, iteratedDeriv_succ]\n    have hzid : iteratedDeriv n riemannZeta ((starRingEnd ℂ) z)\n        = (starRingEnd ℂ) (iteratedDeriv n riemannZeta z) := ih hz\n    have hconj : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z),\n        iteratedDeriv n riemannZeta ((starRingEnd ℂ) s)\n          = (starRingEnd ℂ) (iteratedDeriv n riemannZeta s) := by\n      have hne : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z), s ≠ 1 := by\n        apply (isOpen_compl_singleton.eventually_nhds ?_) \n        ...\n      exact hne.mono (fun s hs => ih hs)\n    have hd : DifferentiableAt ℂ (iteratedDeriv n riemannZeta) z := by\n      have han : AnalyticAt ℂ (iteratedDeriv n riemannZeta) z := by\n        induction n with\n        | zero => exact analyticAt_riemannZeta hz\n        | succ m ihm =>\n          rw [iteratedDeriv_succ]\n          exact ihm.deriv\n      exact han.differentiableAt\n    exact (hasDerivAt_conj_of_conj_eq hzid hconj hd).deriv\n```\nWait — the inner induction for han shadows n — the `induction n with` inside a proof about fixed n: better as a separate have-proved-by-induction claim: \n```\nlemma analyticAt_iteratedDeriv_riemannZeta (n : ℕ) {z : ℂ} (hz : z ≠ 1) :\n    AnalyticAt ℂ (iteratedDeriv n riemannZeta) z := by\n  induction n with\n  | zero => exact analyticAt_riemannZeta hz\n  | succ m ihm =>\n    rw [iteratedDeriv_succ]\n    exact ihm.deriv\n```\nHmm — in the succ case, ihm : AnalyticAt (iteratedDeriv m riemannZeta) z, and goal after rw [iteratedDeriv_succ]: AnalyticAt (deriv (iteratedDeriv m riemannZeta)) z = ihm.deriv ✓.\n\nThe `riemannZeta_conj` form: from isNontrivialZero_conj: `rw [_root_.riemannZeta_conj, hρ.1, map_zero]` — so riemannZeta_conj (s) : riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s) — _root_ namespace. In my namespace use `_root_.riemannZeta_conj`.\n\nAlso `analyticAt_riemannZeta` — root? In one_le_zeroMult: `analyticAt_riemannZeta hρ1` plain ✓ (Mathlib's).\n\nOK — and the analyticOrderAt lemma + zeroMult_conj as sketched. Let me now also double check `map_div₀` exists for starRingEnd: map_div (starRingEnd ℂ) : f (a/b) = f a/f b — for field ring homs: `map_div₀`? or `map_div`? For DivisionRing homs: `map_div₀ (f : α →+* β) (a b) : f (a / b) = f a / f b` — or `map_div`. starRingEnd is ≃+* (stronger) — map_div₀ should apply via the →+* coercion... the simp set [map_sub, map_div₀, starRingEnd_self_apply] — if map_div₀ doesn't fire, try map_div. I'll include both.\n\nLet me write §13+§14 now.","signature":""},{"type":"text","text":"All API confirmed. Writing §13 (C0hat bridges) + §14 (conj machinery)."},{"type":"tool_use","id":"Edit_133","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiTightR.lean","old_string":"  linarith [hle, h4, h3]\n\nend NguyenRH1\n\nend","new_string":"  linarith [hle, h4, h3]\n\n/-! ## 13. Piece 3e: the C0hat interval-count bridges -/\n\n/-- log(a + c) ≤ log a + c/a (the log-increment machine). -/\nlemma log_add_le (a c : ℝ) (ha : 0 < a) (hc : 0 ≤ c) :\n    Real.log (a + c) ≤ Real.log a + c / a := by\n  have h1 : a + c = a * (1 + c / a) := by field_simp [ha.ne']; ring\n  rw [h1, Real.log_mul ha.ne' (by positivity : (1 : ℝ) + c / a ≠ 0)]\n  have h2 : Real.log (1 + c / a) ≤ c / a :=\n    Real.log_le_sub_one_of_pos (by positivity : (0 : ℝ) < 1 + c / a)\n  linarith [h2]\n\n/-- e^2.5 ≤ 13 (via e² ≤ 7.3890566 and e^0.5 ≤ 1.6488). -/\nlemma exp_two_point_five_le_thirteen : Real.exp 2.5 ≤ 13 := by\n  have he2 : Real.exp 1 ≤ (2.7182819 : ℝ) := Real.exp_one_lt_d9.le.trans (by norm_num)\n  have he5 : Real.exp 0.5 ≤ (1.6488 : ℝ) := by\n    have h3' : Real.exp 0.5 ^ 2 ≤ (1.6488 : ℝ) ^ 2 := by\n      have h2 : Real.exp 0.5 ^ 2 = Real.exp 1 := by\n        rw [sq, ← Real.exp_add]\n        congr 1\n        norm_num\n      rw [h2]\n      calc Real.exp 1 ≤ 2.7182819 := he2\n        _ ≤ (1.6488 : ℝ) ^ 2 := by norm_num\n    exact le_of_pow_le_pow_left₀ (by norm_num : (2 : ℕ) ≠ 0)\n      (by norm_num : (0 : ℝ) ≤ 1.6488) h3'\n  have h1 : Real.exp 2.5 = Real.exp 1 * Real.exp 1 * Real.exp 0.5 := by\n    rw [← Real.exp_add, ← Real.exp_add]\n    congr 1\n    norm_num\n  rw [h1]\n  have h5 : Real.exp 1 * Real.exp 1 * Real.exp 0.5 ≤ 2.7182819 * 2.7182819 * 1.6488 := by\n    apply mul_le_mul\n    · exact mul_le_mul he2 he2 (Real.exp_pos 1).le (by norm_num)\n    · exact he5\n    · exact (Real.exp_pos 0.5).le\n    · positivity\n  have h6 : (2.7182819 : ℝ) * 2.7182819 * 1.6488 ≤ 13 := by norm_num\n  exact h5.trans h6\n\n/-- log 13 ≥ 2.5. -/\nlemma log_thirteen_ge_five : (2.5 : ℝ) ≤ Real.log 13 := by\n  rw [Real.le_log_iff_exp_le (by norm_num : (0 : ℝ) < 13)]\n  exact exp_two_point_five_le_thirteen\n\n/-- **The 2k+1 bridge** (k ≥ 11): C0hat(2k+1) ≤\n0.433·(log k + 0.833) + 0.886·(log log k + 0.3475) + 2.9. -/\nlemma C0hat_two_mul_add_one_le {k : ℕ} (hk : 11 ≤ k) :\n    C0hat (2 * (k : ℝ) + 1)\n      ≤ 0.433 * (Real.log k + 0.833) + 0.886 * (Real.log (Real.log k) + 0.3475) + 2.9 := by\n  have hkR : (11 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk\n  have hk0 : (0 : ℝ) < (k : ℝ) := by linarith\n  have hlogk : (2.3978 : ℝ) ≤ Real.log k := by\n    have h2a := log_eleven_ge\n    have h2b : Real.log 11 ≤ Real.log k := Real.log_le_log (by norm_num : (0 : ℝ) < 11) hkR\n    linarith [h2a, h2b]\n  have hlogpos : (0 : ℝ) < Real.log k := by linarith [hlogk]\n  have hinc1 : Real.log (2 * (k : ℝ) + 3) ≤ Real.log k + 0.833 := by\n    have h2 : (2 : ℝ) * (k : ℝ) + 3 ≤ 2.3 * (k : ℝ) := by linarith [hkR]\n    have h3 : Real.log (2 * (k : ℝ) + 3) ≤ Real.log (2.3 * (k : ℝ)) :=\n      Real.log_le_log (by positivity : (0 : ℝ) < 2 * (k : ℝ) + 3) h2\n    have h4 : Real.log (2.3 * (k : ℝ)) = Real.log 2.3 + Real.log k :=\n      Real.log_mul (by norm_num : (2.3 : ℝ) ≠ 0) hk0.ne'\n    rw [h4] at h3\n    have h5 := log_two_point_three_le\n    linarith [h3, h5]\n  have hinc2 : Real.log (Real.log (2 * (k : ℝ) + 3))\n      ≤ Real.log (Real.log k) + 0.3475 := by\n    have h6 : Real.log (Real.log (2 * (k : ℝ) + 3)) ≤ Real.log (Real.log k + 0.833) :=\n      Real.log_le_log (by positivity : (0 : ℝ) < Real.log (2 * (k : ℝ) + 3)) hinc1\n    have h7 : Real.log (Real.log k + 0.833)\n        ≤ Real.log (Real.log k) + 0.833 / Real.log k :=\n      log_add_le (Real.log k) 0.833 hlogpos (by norm_num)\n    have h10 : (0.833 : ℝ) / Real.log k ≤ 0.3475 := by\n      rw [div_le_iff₀ hlogpos]\n      have h11 : (0.3475 : ℝ) * 2.3978 ≤ 0.3475 * Real.log k :=\n        mul_le_mul_of_nonneg_left hlogk (by norm_num)\n      have h12 : (0.833 : ℝ) ≤ 0.3475 * 2.3978 := by norm_num\n      exact h12.trans h11\n    linarith [h6, h7, h10]\n  rw [C0hat]\n  have harg : (2 : ℝ) * (k : ℝ) + 1 + 2 = 2 * (k : ℝ) + 3 := by ring\n  rw [harg]\n  linarith [hinc1, hinc2]\n\n/-- **The j+1 bridge** (j ≥ 14): C0hat(j+1) ≤\n0.433·(log j + 0.1942) + 0.886·(log log j + 0.0736) + 2.9. -/\nlemma C0hat_add_one_le_of_fourteen_le {j : ℕ} (hj : 14 ≤ j) :\n    C0hat ((j : ℝ) + 1)\n      ≤ 0.433 * (Real.log j + 0.1942) + 0.886 * (Real.log (Real.log j) + 0.0736) + 2.9 := by\n  have hjR : (14 : ℝ) ≤ (j : ℝ) := by exact_mod_cast hj\n  have hj0 : (0 : ℝ) < (j : ℝ) := by linarith\n  have hlogj : (2.6388 : ℝ) ≤ Real.log j := by\n    have h2a := log_fourteen_ge\n    have h2b : Real.log 14 ≤ Real.log j := Real.log_le_log (by norm_num : (0 : ℝ) < 14) hjR\n    linarith [h2a, h2b]\n  have hlogpos : (0 : ℝ) < Real.log j := by linarith [hlogj]\n  have hinc1 : Real.log ((j : ℝ) + 3) ≤ Real.log j + 0.1942 := by\n    have h2 : (j : ℝ) + 3 ≤ (17 / 14 : ℝ) * (j : ℝ) := by linarith [hjR]\n    have h3 : Real.log ((j : ℝ) + 3) ≤ Real.log ((17 / 14 : ℝ) * (j : ℝ)) :=\n      Real.log_le_log (by positivity : (0 : ℝ) < (j : ℝ) + 3) h2\n    have h4 : Real.log ((17 / 14 : ℝ) * (j : ℝ))\n        = Real.log (17 / 14) + Real.log j :=\n      Real.log_mul (by norm_num : (17 / 14 : ℝ) ≠ 0) hj0.ne'\n    rw [h4] at h3\n    have h5 := log_17_14_le\n    linarith [h3, h5]\n  have hinc2 : Real.log (Real.log ((j : ℝ) + 3))\n      ≤ Real.log (Real.log j) + 0.0736 := by\n    have h6 : Real.log (Real.log ((j : ℝ) + 3)) ≤ Real.log (Real.log j + 0.1942) :=\n      Real.log_le_log (by positivity : (0 : ℝ) < Real.log ((j : ℝ) + 3)) hinc1\n    have h7 : Real.log (Real.log j + 0.1942)\n        ≤ Real.log (Real.log j) + 0.1942 / Real.log j :=\n      log_add_le (Real.log j) 0.1942 hlogpos (by norm_num)\n    have h10 : (0.1942 : ℝ) / Real.log j ≤ 0.0736 := by\n      rw [div_le_iff₀ hlogpos]\n      have h11 : (0.0736 : ℝ) * 2.6388 ≤ 0.0736 * Real.log j :=\n        mul_le_mul_of_nonneg_left hlogj (by norm_num)\n      have h12 : (0.1942 : ℝ) ≤ 0.0736 * 2.6388 := by norm_num\n      exact h12.trans h11\n    linarith [h6, h7, h10]\n  rw [C0hat]\n  have harg : (j : ℝ) + 1 + 2 = (j : ℝ) + 3 := by ring\n  rw [harg]\n  linarith [hinc1, hinc2]\n\n/-- **The 2t+1 increment** (t ≥ 10): C0hat(2t+1) ≤ C0hat(t+1) + 0.55. -/\nlemma C0hat_two_t_add_one_le {t : ℝ} (ht : 10 ≤ t) :\n    C0hat (2 * t + 1) ≤ C0hat (t + 1) + 0.55 := by\n  have ht3 : (0 : ℝ) < t + 3 := by linarith\n  have hlog13 : (2.5 : ℝ) ≤ Real.log (t + 3) := by\n    have h1 : Real.log 13 ≤ Real.log (t + 3) :=\n      Real.log_le_log (by norm_num : (0 : ℝ) < 13) (by linarith : (13 : ℝ) ≤ t + 3)\n    have h2 := log_thirteen_ge_five\n    linarith [h1, h2]\n  have hlogpos : (0 : ℝ) < Real.log (t + 3) := by linarith [hlog13]\n  have hinc1 : Real.log (2 * t + 3) ≤ Real.log 2 + Real.log (t + 3) := by\n    have h1 : (2 : ℝ) * t + 3 ≤ 2 * (t + 3) := by linarith\n    have h2 : Real.log (2 * t + 3) ≤ Real.log (2 * (t + 3)) :=\n      Real.log_le_log (by positivity : (0 : ℝ) < 2 * t + 3) h1\n    have h3 : Real.log (2 * (t + 3)) = Real.log 2 + Real.log (t + 3) :=\n      Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) ht3.ne'\n    rw [h3] at h2\n    exact h2\n  have hinc2 : Real.log (Real.log (2 * t + 3))\n      ≤ Real.log (Real.log (t + 3)) + 0.6932 / 2.5 := by\n    have h6 : Real.log (Real.log (2 * t + 3))\n        ≤ Real.log (Real.log (t + 3) + Real.log 2) := by\n      apply Real.log_le_log (by positivity : (0 : ℝ) < Real.log (2 * t + 3))\n      linarith [hinc1]\n    have h7 : Real.log (Real.log (t + 3) + Real.log 2)\n        ≤ Real.log (Real.log (t + 3)) + Real.log 2 / Real.log (t + 3) :=\n      log_add_le (Real.log (t + 3)) (Real.log 2) hlogpos (Real.log_nonneg (by norm_num))\n    have hlog2le : Real.log 2 ≤ 0.6932 := Real.log_two_lt_d9.le.trans (by norm_num)\n    have h10 : Real.log 2 / Real.log (t + 3) ≤ 0.6932 / 2.5 := by\n      apply div_le_div hlog2le hlog13 (by norm_num : (0 : ℝ) ≤ 2.5) hlogpos\n    linarith [h6, h7, h10]\n  have hlog2le : Real.log 2 ≤ 0.6932 := Real.log_two_lt_d9.le.trans (by norm_num)\n  rw [C0hat, C0hat]\n  have harg1 : (2 : ℝ) * t + 1 + 2 = 2 * t + 3 := by ring\n  have harg2 : (t : ℝ) + 1 + 2 = t + 3 := by ring\n  rw [harg1, harg2]\n  linarith [hinc1, hinc2, hlog2le]\n\n/-! ## 14. Piece 3f: the conjugation machinery (zeroMult_conj) -/\n\n/-- ζ is analytic at iterated-derivatives level (off the pole). -/\nlemma analyticAt_iteratedDeriv_riemannZeta (n : ℕ) {z : ℂ} (hz : z ≠ 1) :\n    AnalyticAt ℂ (iteratedDeriv n riemannZeta) z := by\n  induction n with\n  | zero => exact analyticAt_riemannZeta hz\n  | succ m ihm =>\n    rw [iteratedDeriv_succ]\n    exact ihm.deriv\n\n/-- **The conjugate-derivative lemma**: if f commutes with conjugation at\nz and near conj z, and is differentiable at z, then f has derivative\nconj(deriv f z) at conj z. -/\nlemma hasDerivAt_conj_of_conj_eq {f : ℂ → ℂ} {z : ℂ}\n    (hzid : f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (f z))\n    (hconj : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z),\n      f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f s))\n    (hdiff : DifferentiableAt ℂ f z) :\n    HasDerivAt f ((starRingEnd ℂ) (deriv f z)) ((starRingEnd ℂ) z) := by\n  have h1 : Filter.Tendsto (fun x : ℂ => (f x - f z) / (x - z)) (𝓝[≠] z)\n      (𝓝 (deriv f z)) :=\n    hasDerivAt_iff_tendsto.mp hdiff.hasDerivAt\n  have hmap : Filter.Tendsto (starRingEnd ℂ) (𝓝[≠] ((starRingEnd ℂ) z)) (𝓝[≠] z) := by\n    have hcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) := Complex.continuous_conj\n    have hT := hcont.tendsto ((starRingEnd ℂ) z)\n    rw [Filter.tendsto_nhdsWithin_iff]\n    refine ⟨hT.mono_left Filter.nhdsWithin_le_nhds, ?_⟩\n    rw [Filter.eventually_nhdsWithin_iff]\n    exact Filter.Eventually.of_forall (fun x (hx : x ≠ (starRingEnd ℂ) z) => by\n      show (starRingEnd ℂ) x ≠ z\n      intro hbad\n      apply hx\n      have h3 := congrArg (starRingEnd ℂ) hbad\n      rwa [starRingEnd_self_apply] at h3)\n  have h2 : Filter.Tendsto (fun x : ℂ =>\n      (starRingEnd ℂ) ((f ((starRingEnd ℂ) x) - f z) / (((starRingEnd ℂ) x) - z)))\n      (𝓝[≠] ((starRingEnd ℂ) z)) (𝓝 ((starRingEnd ℂ) (deriv f z))) := by\n    have hcont : Continuous ((starRingEnd ℂ) : ℂ → ℂ) := Complex.continuous_conj\n    exact (hcont.tendsto _).comp (h1.comp hmap)\n  have h3 : (fun x : ℂ => (f x - f ((starRingEnd ℂ) z)) / (x - (starRingEnd ℂ) z))\n      =ᶠ[𝓝[≠] ((starRingEnd ℂ) z)] fun x : ℂ =>\n      (starRingEnd ℂ) ((f ((starRingEnd ℂ) x) - f z) / (((starRingEnd ℂ) x) - z)) := by\n    apply Filter.EventuallyEq.filter_mono ?_ Filter.nhdsWithin_le_nhds\n    exact hconj.mono (fun s hs => by\n      rw [hs, hzid]\n      simp only [map_sub, map_div₀, starRingEnd_self_apply])\n  exact hasDerivAt_iff_tendsto.mpr (Filter.Tendsto.congr' h3 h2)\n\n/-- The iterated derivatives of ζ commute with conjugation (off the pole). -/\nlemma iteratedDeriv_riemannZeta_conj (n : ℕ) {z : ℂ} (hz : z ≠ 1) :\n    iteratedDeriv n riemannZeta ((starRingEnd ℂ) z)\n      = (starRingEnd ℂ) (iteratedDeriv n riemannZeta z) := by\n  induction n generalizing z with\n  | zero =>\n    rw [iteratedDeriv_zero, iteratedDeriv_zero]\n    exact _root_.riemannZeta_conj z\n  | succ m ihm =>\n    rw [iteratedDeriv_succ, iteratedDeriv_succ]\n    have hzid := ihm hz\n    have hconj : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z),\n        iteratedDeriv m riemannZeta ((starRingEnd ℂ) s)\n          = (starRingEnd ℂ) (iteratedDeriv m riemannZeta s) := by\n      have hne : ∀ᶠ s in 𝓝 ((starRingEnd ℂ) z), s ≠ 1 := by\n        have h1 : ((starRingEnd ℂ) z) ≠ 1 := by\n          intro h\n          apply hz\n          have h2 := congrArg (starRingEnd ℂ) h\n          rwa [starRingEnd_self_apply, map_one] at h2\n        exact isOpen_compl_singleton.eventually_nhds h1\n      exact hne.mono (fun s hs => ihm hs)\n    have hd : DifferentiableAt ℂ (iteratedDeriv m riemannZeta) z :=\n      (analyticAt_iteratedDeriv_riemannZeta m hz).differentiableAt\n    exact (hasDerivAt_conj_of_conj_eq hzid hconj hd).deriv\n\n/-- The analytic order of ζ is conjugation-invariant (off the pole). -/\nlemma analyticOrderAt_riemannZeta_conj {z : ℂ} (hz : z ≠ 1) :\n    analyticOrderAt riemannZeta ((starRingEnd ℂ) z) = analyticOrderAt riemannZeta z := by\n  have hzconj : ((starRingEnd ℂ) z) ≠ 1 := by\n    intro h\n    apply hz\n    have h2 := congrArg (starRingEnd ℂ) h\n    rwa [starRingEnd_self_apply, map_one] at h2\n  have htop : analyticOrderAt riemannZeta z ≠ ⊤ := zeta_order_ne_top_of_ne hz\n  set n := analyticOrderNatAt riemannZeta z with hn\n  have hzn : analyticOrderAt riemannZeta z = (n : ℕ∞) :=\n    (Nat.cast_analyticOrderNatAt htop).symm\n  obtain ⟨hz1, hz2⟩ :=\n    (analyticAt_riemannZeta hz).analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero.mp hzn\n  have hkey : analyticOrderAt riemannZeta ((starRingEnd ℂ) z) = (n : ℕ∞) :=\n    (analyticAt_riemannZeta hzconj).analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero.mpr\n      ⟨fun k hk => by\n        rw [iteratedDeriv_riemannZeta_conj k hz, hz1 k hk, map_zero],\n       by\n        rw [iteratedDeriv_riemannZeta_conj n hz]\n        intro hbad\n        apply hz2\n        have h3 := congrArg (starRingEnd ℂ) hbad\n        rwa [starRingEnd_self_apply, map_zero] at h3⟩\n  rw [hzn, hkey]\n\n/-- **zeroMult is conjugation-invariant** (the left-tail count bridge). -/\nlemma zeroMult_conj {ρ : ℂ} (hρ : IsNontrivialZero ρ) :\n    zeroMult ((starRingEnd ℂ) ρ) = zeroMult ρ := by\n  have hρ1 : ρ ≠ 1 := by\n    rintro rfl\n    have h := hρ.2.2\n    rw [Complex.one_re] at h\n    exact (lt_irrefl (1 : ℝ)) h\n  show (analyticOrderAt riemannZeta ((starRingEnd ℂ) ρ)).toNat\n      = (analyticOrderAt riemannZeta ρ).toNat\n  rw [analyticOrderAt_riemannZeta_conj hρ1]\n\nend NguyenRH1\n\nend"},"extra_content":null}]