[{"type":"thinking","thinking":"The conj trick is clean: `intervalIntegral.intervalIntegral_conj` + `integral_congr` + `Jlag_conj` + `Complex.norm_conj`. The neg-side theorem reduces to the pos-side one.\n\nNote: `intervalIntegral.intervalIntegral_conj : ∫ x in a..b, conj (f x) = conj (∫ x in a..b, f x)` — used with `rw [← intervalIntegral.intervalIntegral_conj]`.\n\nNow let me plan 6-c-iv's Lean content. This is a big block. Components:\n\n**A. The per-zero arcsinh-FTC machine.** The most delicate part. Let me define it carefully.\n\nFor ρ : ℂ (a nontrivial zero — β := ρ.re ∈ (0,1), γ := ρ.im) and T with δ := |T − γ| > 0:\n\n∫_{-5/2}^{3} dσ/√((σ−β)²+δ²) = F(3) − F(−5/2), F(σ) := log((σ−β) + √((σ−β)²+δ²)).\n\nLean formalization plan (as a standalone lemma):\n\n```lean\ntheorem integral_one_div_sqrt_sq_add_sq_le {β δ : ℝ} (hδ : 0 < δ) :\n    ∫ σ in (-5/2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n      Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ)\n```\n\nHmm — actually the deliverable per-zero is the bound 2·log(16.5/δ); but it's cleaner to prove the FTC equality + the F(3)/F(−5/2) estimates as separate lemmas:\n\n1. `integral_one_div_sqrt_sq_add_sq_eq`: the FTC evaluation:\n   ∫ σ in a..b, 1/√((σ−β)²+δ²) = F(b) − F(a) with F σ = log((σ−β)+√((σ−β)²+δ²)).\n   \n2. The two endpoint estimates:\n   - F(3) ≤ log(6+δ) [for β < 1: (3−β) + √((3−β)²+δ²) ≤ 2(3−β) + δ ≤ 6+δ; the argument positive; log mono]\n   - −F(−5/2) ≤ log(7+δ) + 2·log(1/δ) [for 0 < β: with u := β+5/2 ∈ (5/2, 7/2): F(−5/2) = log(−u + √(u²+δ²)) and −u+√(u²+δ²) = δ²/(u+√(u²+δ²)) ≥ δ²/(7+δ) > 0; so F(−5/2) ≥ log(δ²/(7+δ)) = 2·log δ − log(7+δ); so −F(−5/2) ≤ log(7+δ) − 2·log δ = log(7+δ) + 2·log(1/δ).]\n\nThen ∫ ≤ log(6+δ) + log(7+δ) + 2·log(1/δ).\n\nWait — 2·log(1/δ) vs −2·log δ: log(1/δ) = −log δ (Real.log_div / log_one) — log(1/δ) = log 1 − log δ = −log δ. In Lean: `Real.log_div (by norm_num) (ne_of_gt hδ)` : log(1/δ) = log 1 − log δ = −log δ. Or `Real.log_inv : log x⁻¹ = −log x` — 1/δ = δ⁻¹ (one_div_eq_inv). I'll keep log(1/δ) throughout to avoid sign juggling — the final target uses log(1/δ) anyway.\n\nThe endpoint algebra:\n\nF(3) ≤ log(6+δ):\n- g3 := (3−β) + √((3−β)²+δ²). Need: g3 ≤ 6+δ and g3 > 0, then Real.log_le_log (g3 > 0) (g3 ≤ 6+δ).\n- √(x²+δ²) ≤ x + δ for x ≥ 0: Real.sqrt_le_iff? `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y^2`? Something like: Real.sqrt_le_iff (hy : 0 ≤ y)? — there's `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2`? Hmm — or `Real.sqrt_le' (hy : 0 < y) : √x ≤ y ↔ x ≤ y^2`. Let me use: √((3−β)²+δ²) ≤ (3−β) + δ ⟺ (3−β)²+δ² ≤ ((3−β)+δ)² = (3−β)² + 2(3−β)δ + δ² ⟺ 0 ≤ 2(3−β)δ ✓ (3−β > 0 since β < 1, δ > 0). Via `Real.sqrt_le_iff`/`sq_le_sq`: I'll find the right form: `Real.sqrt_le_iff {x y : ℝ} : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2`? Hmm. There's `Real.sqrt_le_iff (hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y ^ 2`?? and `Real.sqrt_le_sqrt (h : x ≤ y) : √x ≤ √y`. And `sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ≤ b ↔ a^2 ≤ b^2`? The banked gotcha mentions sq_le_sq₀ exists. Route: apply (sq_le_sq₀ (Real.sqrt_nonneg _) (by positivity : 0 ≤ (3−β)+δ)).mpr-ish... sq_le_sq₀ : 0 ≤ a → 0 ≤ b → (a ≤ b ↔ a ^ 2 ≤ b ^ 2)? Then √h ≤ (3−β)+δ ⟺ (√h)² ≤ ((3−β)+δ)² — with Real.sq_sqrt (h ≥ 0): h = (3−β)²+δ² ≤ ((3−β)+δ)² — nlinarith [δ > 0, β < 1]. OK.\n- Then g3 ≤ (3−β) + ((3−β)+δ) = 2(3−β)+δ ≤ 6+δ ⟺ 2(3−β) ≤ 6 ⟺ β ≥ 0 ✓ (0 < β).\n- g3 > 0: √((3−β)²+δ²) > |3−β| ≥ 0... strictly: √((3−β)²+δ²) > √((3−β)²) = |3−β| (Real.sqrt_lt_sqrt (sq_nonneg) (by nlinarith [hδ]) : (3−β)² < (3−β)²+δ²) — Real.sqrt_lt_sqrt (hx : 0 ≤ x) (h : x < y) : √x < √y ✓. And |3−β| = 3−β ≥ 2 > 0. So √ > 3−β ⟹ g3 = (3−β) + √ > 2(3−β) > 0 ✓.\n\n−F(−5/2) ≤ log(7+δ) + 2·log(1/δ):\n- With u := β + 5/2 (0 < β < 1 ⟹ 5/2 < u < 7/2):\n- g25 := (−5/2−β) + √((5/2+β)²+δ²) = −u + √(u²+δ²).\n- g25 > 0: √(u²+δ²) > |u| = u (u > 0) ⟹ −u + √ > 0 ✓.\n- The rationalization: g25 · (u + √(u²+δ²)) = (√(u²+δ²))² − u² = δ² ⟹ g25 = δ²/(u+√(u²+δ²)).\n- u + √(u²+δ²) ≤ u + (u + δ) = 2u + δ ≤ 7 + δ (u < 7/2): √(u²+δ²) ≤ u+δ ⟺ u²+δ² ≤ (u+δ)² ⟺ 0 ≤ 2uδ ✓.\n- So g25 = δ²/(u+√) ≥ δ²/(7+δ) (denominator positive, ≤) — div_le_div_of_nonneg_left (δ² ≥ 0) (0 < u+√) (u+√ ≤ 7+δ): `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (hc : b ≤ c) : a / c ≤ a / b` — wait direction: a/c ≤ a/b ⟸ b ≤ c ✓ — so δ²/(7+δ) ≤ δ²/(u+√) ✓ — i.e. g25 ≥ δ²/(7+δ).\n- log mono: F(−5/2) = log g25 ≥ log(δ²/(7+δ)) = log(δ²) − log(7+δ) (Real.log_div (δ² ≠ 0) (7+δ ≠ 0)) = 2·log δ − log(7+δ) (Real.log_pow : log(δ^2) = 2·log δ ✓).\n- So −F(−5/2) ≤ log(7+δ) − 2·log δ = log(7+δ) + 2·log(1/δ) (log(1/δ) = −log δ).\n\nThe rationalization identity g25 = δ²/(u+√(u²+δ²)): field_simp + the (√h)² = h identity. In Lean:\n```lean\nhave hg25id : -u + Real.sqrt (u ^ 2 + δ ^ 2) = δ ^ 2 / (u + Real.sqrt (u ^ 2 + δ ^ 2)) := by\n  rw [div_eq_iff (by positivity... : u + √ ≠ 0)]\n  -- (−u + √) * (u + √) = δ²\n  have hs : (Real.sqrt (u ^ 2 + δ ^ 2)) ^ 2 = u ^ 2 + δ ^ 2 := Real.sq_sqrt (by positivity)\n  nlinarith [hs]\n```\n`(−u + √)·(u + √) = √² − u² = δ²` — nlinarith [hs]: the product expands: −u·u + √·u − u·√ + √·√ = −u² + √²... nlinarith handles (√·√ → via hs hint) ✓.\n\nWait — div_eq_iff (hb : b ≠ 0) : a / b = c ↔ a = c * b. I want g = δ²/(u+√): rw [div_eq_iff hne] on goal `g = δ²/(u+√)` — hmm, div_eq_iff rewrites δ²/(u+√) = g-form... the goal is `-u + √ = δ^2 / (u+√)`. rw [div_eq_iff hne] : a / b = c ↔ a = c * b — with a := δ², b := u+√, c := -u+√: goal becomes δ² = (−u+√)·(u+√) ✓ then nlinarith [hs]. ✓\n\n- Also g25 > 0 (for the log to be meaningful): as computed ✓ needed for... actually F(−5/2) = log g25 — log of positive — the estimate −F ≤ ... uses log mono log(δ²/(7+δ)) ≤ log g25 ⟸ δ²/(7+δ) ≤ g25 (with δ²/(7+δ) > 0 for Real.log_le_log's positivity side hyps: Real.log_le_log (hx : 0 < x) (h : x ≤ y) : log x ≤ log y — x := δ²/(7+δ) > 0 ✓ h : δ²/(7+δ) ≤ g25 ✓).\n\nThen: −F(−5/2) = −log g25 ≤ −log(δ²/(7+δ)) = −(2 log δ − log(7+δ)) = log(7+δ) − 2 log δ.\n\nAnd the final target 2·log(1/δ) — relate −2 log δ = 2·log(1/δ): Real.log_div (1≠0) (δ≠0) : log(1/δ) = log 1 − log δ = −log δ (log_one). So 2·log(1/δ) = −2·log δ ✓.\n\nThen the FTC lemma itself:\n\n```lean\ntheorem integral_one_div_sqrt_sq_add_sq (β δ : ℝ) (hδ : 0 < δ) (a b : ℝ) :\n    ∫ σ in a..b, 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) =\n      Real.log ((b - β) + Real.sqrt ((b - β) ^ 2 + δ ^ 2)) -\n        Real.log ((a - β) + Real.sqrt ((a - β) ^ 2 + δ ^ 2)) := by\n  apply intervalIntegral.integral_eq_sub_of_hasDerivAt\n  · intro σ hσ\n    -- HasDerivAt F (1/√h σ) σ\n  · -- integrability of 1/√h\n```\n\nThe HasDerivAt proof — let me structure it carefully:\n\n```lean\n  have hgpos : ∀ σ : ℝ, 0 < (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n    intro σ\n    have h1 : |(σ - β)| < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n      have h2 : (σ - β) ^ 2 < (σ - β) ^ 2 + δ ^ 2 := by nlinarith [hδ]\n      have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n      rwa [Real.sqrt_sq_eq_abs] at h3\n    have h4 : -(σ - β) < Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n      have := neg_abs_le (σ - β)  -- -(σ−β) ≤ |σ−β|\n      linarith\n    linarith\n```\n\nneg_abs_le : -a ≤ |a| ✓ root. So (σ−β) + √h > (σ−β) + (−(σ−β)) = 0 ✓ linarith.\n\n```lean\n  have hgder : ∀ σ : ℝ, HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n      (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n    intro σ\n    have hh : (0:ℝ) < (σ - β) ^ 2 + δ ^ 2 := by positivity?? -- needs δ ≠ 0: nlinarith [hδ, sq_nonneg...]\n```\n\nh(σ) = (σ−β)²+δ² > 0 since δ² > 0: nlinarith [sq_nonneg (σ−β), hδ] or by positivity with hδ? positivity can't do δ² > 0 from hδ (it can: 0 < δ ⟹ 0 < δ^2? positivity proves 0 ≤ δ^2 not strict; the SUM (σ−β)²+δ² > 0 needs δ² > 0 strict — from hδ : 0 < δ: δ^2 > 0 via pow_pos hδ 2 ✓ then add_pos_of_nonneg_of_pos (sq_nonneg) (pow_pos hδ 2). I'll write:\n```lean\n    have hh : (0:ℝ) < (σ - β) ^ 2 + δ ^ 2 :=\n      add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)\n```\n\npow_pos : 0 < a → 0 < a^n (n ≠ 0): `pow_pos (h : 0 < a) (n : ℕ) : 0 < a ^ n` ✓.\n\n    The derivative of g(σ) = (σ−β) + √(h(σ)): g′ = 1 + h′/(2√h) where h′ = 2(σ−β). And 1 + 2(σ−β)/(2√h) = 1 + (σ−β)/√h = (√h + (σ−β))/√h = g/√h ✓.\n    \n```lean\n    have h1 : HasDerivAt (fun σ => σ - β) 1 σ := hasDerivAt_id.sub_const β\n    have h2 : HasDerivAt (fun σ => (σ - β) ^ 2 + δ ^ 2) (2 * (σ - β)) σ := by\n      have := (hasDerivAt_id.sub_const β).pow 2\n      -- this : HasDerivAt (fun σ => (σ - β)^2) (2 * (σ-β)^1 * 1) σ\n      have h3 := this.add_const (δ ^ 2)\n      -- convert derivative: 2*(σ-β)^1*1 = 2*(σ-β)\n      convert h3 using 1\n      ring\n    have h4 : HasDerivAt (fun σ => Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n        (2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n      h2.sqrt hh.ne'\n    have h5 : HasDerivAt (fun σ => (σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))\n        (1 + 2 * (σ - β) / (2 * Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) σ :=\n      h1.add h4\n    -- the derivative simplifies to g/√h\n    convert h5 using 1\n    have hsqrt0 : Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hh)\n    have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'\n    field_simp\n    ring\n```\n\nCheck the derivative algebra: need `g/√h = 1 + 2(σ−β)/(2√h)` ⟺ g/√h = 1 + (σ−β)/√h ⟺ g = √h + (σ−β) ✓ (g = (σ−β) + √h ✓). field_simp [hsqrt0] then ring ✓. field_simp on goal `((σ−β)+√h)/√h = 1 + 2*(σ−β)/(2*√h)`: multiplies out: ((σ−β)+√h)·(2√h) = (2√h + 2(σ−β))·√h/√h?? — field_simp clears denominators: LHS·√h·2√h vs... standard: both sides × 2√h: 2√h((σ−β)+√h) = 2√h + 2(σ−β)·... hmm — let me just trust field_simp + ring (banked: \"field_simp closes goals (trailing ring errors)\"). Actually the identity: ((σ−β)+√h)/√h = 1 + 2(σ−β)/(2√h). Multiply both sides by 2√h: 2((σ−β)+√h) = 2√h + 2(σ−β) ⟺ 2(σ−β) + 2√h = 2√h + 2(σ−β) ✓ ring.\n\n`hasDerivAt_id.sub_const β` — hmm: `hasDerivAt_id (x) : HasDerivAt id 1 x`; `.sub_const (c) : HasDerivAt (fun x => f x - c) (f') x` — HasDerivAt.sub_const (hf : HasDerivAt f f' x) (c) : HasDerivAt (fun x => f x - c) f' x ✓. hasDerivAt_id — signature: `hasDerivAt_id (x : 𝕜) : HasDerivAt id 1 x` ✓. So `(hasDerivAt_id σ).sub_const β : HasDerivAt (fun x => x - β) 1 σ` ✓ — note the function is `fun x => x - β` vs my `fun σ => σ - β` ✓ alpha.\n\n`(hasDerivAt_id.sub_const β).pow 2` — HasDerivAt.pow (hf) (n : ℕ) : HasDerivAt (fun x => (f x)^n) (n * f x ^ (n-1) * f') x ✓ — gives derivative `2 * (σ−β)^1 * 1` — my convert handles ✓. Hmm — actually the .pow form: `HasDerivAt.pow {f : 𝕜 → 𝕜} {f'} (hf : HasDerivAt f f' x) (n : ℕ) : HasDerivAt (fun y => f y ^ n) ((n : 𝕜) * f x ^ (n - 1) * f') x`? — the derivative: `↑n * (f x)^(n-1) * f'`. For n=2: `↑2 * (σ−β)^1 * 1` — my target derivative `2 * (σ−β)` — convert via ring ✓. But the convert needs the FUNCTION to match too: .pow gives `fun y => (y−β)^2` vs my `fun σ => (σ−β)^2 + δ^2` — the .add_const (δ^2) fixes: HasDerivAt.add_const (hf) (c): `fun y => (y−β)^2 + δ^2` ✓ derivative unchanged ✓.\n\nHmm — `HasDerivAt.add_const (hf : HasDerivAt f f' x) (c : 𝕜) : HasDerivAt (fun x => f x + c) f' x` ✓ (banked gotcha session-011: \"HasDerivAt.add_const adds to VALUE (use .comp for precomposition)\" — it appends a constant to the function value ✓ what I want).\n\nThen h5's convert: `convert h5 using 1` — h5 : HasDerivAt g (1 + 2(σ−β)/(2√h)) σ; goal: HasDerivAt g (g σ/√h) σ — convert using 1: function parts match (same g — need defeq: my g-lambda vs h5's — both `fun σ => (σ−β) + √(h σ)` ✓ syntactically equal), leaves derivative equality: g/√h = 1 + 2(σ−β)/(2√h) — field_simp [hsqrt0]; ring ✓.\n\nThen the F derivative:\n```lean\n    have hF : HasDerivAt (fun σ => Real.log ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)))\n        (1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) σ := by\n      have h6 := (hgder σ).log (hgpos σ).ne'\n      -- h6 : HasDerivAt (log ∘ g) ((g σ / √h) / g σ)\n      convert h6 using 1\n      field_simp [(hgpos σ).ne']\n```\n\n(g/√h)/g = 1/√h ⟺ g·√h... field_simp with g ≠ 0, √h ≠ 0: (g/√h)/g = 1/√h ⟺ multiply by g·√h: g·g?? — (g/√h)/g = g/(√h·g) = 1/√h ✓ field_simp + ring... `field_simp` then the goal might become √h·g = √h·g or similar — closed by ring (or rfl). Might need `ring` after field_simp. Write `field_simp [hsqrt0, (hgpos σ).ne']` then `ring` — but field_simp might fully close. Include a trailing ring attempt: the banked pattern is field_simp closes or leaves ring-closable. I'll write:\n```lean\n      convert h6 using 1\n      field_simp [hsqrt0, (hgpos σ).ne']\n```\nIf field_simp leaves a goal, add ring. To be safe: \n```lean\n      convert h6 using 1\n      have hg0 : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) ≠ 0 := (hgpos σ).ne'\n      field_simp [hsqrt0, hg0]\n      ring\n```\nHmm — but if field_simp closes it, ring errors \"no goals\". The banked gotcha says field_simp often closes with trailing ring errors — i.e., `field_simp; ring` is a common pattern where field_simp leaves a ring-goal. If field_simp FULLY closes, the trailing ring fails. Risk either way. Alternative deterministic: \n```lean\n      convert h6 using 1\n      rw [div_div, mul_comm, ← div_div, div_self hg0]  -- messy\n```\nOr: `(g σ / √h) / g σ = 1/√h`: \n```lean\n      rw [show ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) /\n          ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) =\n        (Real.sqrt ((σ - β) ^ 2 + δ ^ 2))⁻¹ * (((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) /\n        ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2))) := by ring, div_self hg0, ...]\n```\nOvercomplicating. Standard approach: `field_simp [*]; ring` and if field_simp closed it, drop the ring on the error. I'll write `field_simp [hsqrt0, hg0]; ring` and adjust on failure.\n\nActually — cleaner: prove the derivative algebra separately as a have before convert:\n```lean\n      have hder : ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) /\n          ((σ - β) + Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) = 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) := by\n        field_simp [hsqrt0, hg0]\n      convert h6 using 1\n      exact hder.symm  -- hmm direction\n```\nconvert h6 using 1 leaves goal: (target deriv) = (h6 deriv) i.e. `1/√h = (g/√h)/g`? or the reverse? convert produces equality goals between differing parts: goal `1 / √h = (g σ / √h) / g σ` — then `exact hder.symm` ✓ where hder : (g/√h)/g = 1/√h ✓. But the direction convert presents could be either. Use `exact?`-free robust: `field_simp [hsqrt0, hg0]` directly on the convert goal (whichever direction, field_simp normalizes both sides then ring/closes). Hmm — field_simp on `1/√h = (g/√h)/g`: clears to `√h * g = √h * g`-ish — closed by field_simp itself or needs ring. The banked pattern `div_add_div + div_eq_div_iff + ring as the always-works fraction pattern` (session-038). Let me use div_eq_div_iff:\n```lean\n      rw [div_eq_div_iff hsqrt0 hg0]  -- hmm\n```\ndiv_eq_div_iff (hb : b ≠ 0) (hd : d ≠ 0) : a / b = c / d ↔ a * d = c * b. For `1/√h = (g/√h)/g`: a := 1, b := √h, c := g/√h, d := g: 1·g = (g/√h)·√h ⟺ g = g ✓ (div_mul_cancel₀ g √h ≠ 0)... ring can't do div_mul_cancel. `field_simp` normalizes divisions into num/den form — g/√h/g... \n\nOK let me stop overthinking: the pattern `field_simp [hsqrt0, hg0]; ring` — if it fails at ring with \"no goals\", I drop ring; if it fails with a leftover goal, the error shows it. ONE iteration will settle it. Same for the earlier h5-convert.\n\nThen the integrability: 1/√h continuous: \n```lean\n  have hint : IntervalIntegrable (fun σ => 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2)) volume a b := by\n    apply Continuous.intervalIntegrable\n    apply Continuous.div continuous_const\n    · -- Continuous (fun σ => √((σ−β)²+δ²))\n      apply Continuous.sqrt\n      exact ((continuous_id.sub continuous_const).pow 2).add continuous_const\n    · intro σ\n      exact ne_of_gt (Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos hδ 2)))\n```\n\nContinuous.sqrt : `Continuous Real.sqrt` — it's `Real.continuous_sqrt` ✓. `.sqrt` method? There might not be Continuous.sqrt method — use `Real.continuous_sqrt.comp`. Let me write: `(Real.continuous_sqrt).comp (...)`. \n\n- continuous_id : Continuous id ✓; .sub continuous_const : Continuous fun σ => σ − β ✓; .pow 2? — `Continuous.pow (hf : Continuous f) (n : ℕ) : Continuous fun x => (f x)^n` ✓; .add continuous_const ✓.\n- Continuous.div (hf) (hg) (h0 : ∀ x, g x ≠ 0) : Continuous fun x => f x / g x ✓.\n\nThen integral_eq_sub_of_hasDerivAt (hderiv) (hint): hderiv : ∀ x ∈ uIcc a b, HasDerivAt F (1/√h x) x — from the per-σ hF ✓ (uIcc membership irrelevant — bound holds everywhere).\n\n**B. The endpoint estimates.** Two lemmas:\n```lean\ntheorem arcsinh_right_endpoint_le {β δ : ℝ} (hβ : β < 1) (hδ : 0 < δ) :\n    Real.log ((3 - β) + Real.sqrt ((3 - β) ^ 2 + δ ^ 2)) ≤ Real.log (6 + δ)\ntheorem arcsinh_left_endpoint_le {β δ : ℝ} (hβ : 0 < β) (hδ : 0 < δ) :\n    -Real.log ((-5/2 - β) + Real.sqrt ((-5/2 - β) ^ 2 + δ ^ 2)) ≤\n      Real.log (7 + δ) + 2 * Real.log (1 / δ)\n```\n\nHmm — wait, for the left endpoint, (−5/2−β)² = (5/2+β)² ✓ (neg_sq). I'll phrase with u := 5/2 + β: (−5/2−β) = −(5/2+β) and (−5/2−β)^2 = (5/2+β)^2 via `neg_sq`? `neg_sq (a) : (-a)^2 = a^2` — hmm — neg_sq : (-a) ^ 2 = a ^ 2 ✓. Or ring_nf. Let me phrase the left endpoint directly with the u-substitution inside the proof.\n\n**C. The per-zero integral bound**: combine FTC (a := −5/2, b := 3) + the two endpoint estimates:\n```lean\ntheorem integral_one_div_sqrt_le {β δ : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) (hδ : 0 < δ) :\n    ∫ σ in (-5/2 : ℝ)..(3 : ℝ), 1 / Real.sqrt ((σ - β) ^ 2 + δ ^ 2) ≤\n      Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ)\n```\nby rw [integral_one_div_sqrt_sq_add_sq]; linarith [endpoints].\n\nHmm wait — F(3) − F(−5/2) ≤ log(6+δ) − F(−5/2) ≤ log(6+δ) + (log(7+δ) + 2 log(1/δ)) ✓ linarith [right_endpoint, left_endpoint].\n\n**D. The log-mono simplification to 2·log(16.5/δ)**:\n```lean\ntheorem per_zero_le_two_log {δ : ℝ} (hδ : 0 < δ) (hδ1 : δ ≤ 1) :\n    Real.log (6 + δ) + Real.log (7 + δ) + 2 * Real.log (1 / δ) ≤ 2 * Real.log (16.5 / δ) := by\n  have h1 : Real.log (6 + δ) + Real.log (7 + δ) = Real.log ((6 + δ) * (7 + δ)) :=\n    (Real.log_mul (by positivity... ≠0) (by positivity... ≠0)).symm\n  have h2 : Real.log ((6 + δ) * (7 + δ)) ≤ Real.log (16.5 * 16.5) :=\n    Real.log_le_log (by positivity) (by nlinarith [hδ, hδ1] : (6+δ)*(7+δ) ≤ 16.5*16.5)\n  have h3 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\n    rw [show (16.5 : ℝ) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\n    ring\n  have h4 : Real.log (16.5 / δ) = Real.log 16.5 + Real.log (1 / δ) :=\n    Real.log_div (by norm_num) (ne_of_gt hδ)  -- log(16.5/δ) = log 16.5 − log δ\n```\nHmm — Real.log_div gives log(16.5/δ) = log 16.5 − log δ. And log(1/δ) = −log δ. So 2·log(16.5/δ) = 2·log16.5 − 2·log δ = 2·log16.5 + 2·log(1/δ). So the goal: log(6+δ)+log(7+δ) + 2·log(1/δ) ≤ 2·log16.5 + 2·log(1/δ) ⟺ log((6+δ)(7+δ)) ≤ 2·log16.5 ✓ via h2 h3. linarith [h1 ▸ h2, h3, h4-rewrites]. \n\nStructure it as: \n```lean\n  have h5 : 2 * Real.log (16.5 / δ) = 2 * Real.log 16.5 + 2 * Real.log (1 / δ) := by\n    have h6 : Real.log (1 / δ) = -Real.log δ := by\n      rw [Real.log_div one_ne_zero (ne_of_gt hδ), Real.log_one, zero_sub]\n    rw [Real.log_div (by norm_num) (ne_of_gt hδ), h6]\n    ring\n  rw [h5]\n  linarith [h2, h3, h1]\n```\nWait — after rw [h5]: goal `log(6+δ) + log(7+δ) + 2·log(1/δ) ≤ 2·log 16.5 + 2·log(1/δ)`. With h1 : LHS-sum = log((6+δ)(7+δ)), h2 : log((6+δ)(7+δ)) ≤ log(16.5·16.5), h3 : log(16.5·16.5) = 2·log 16.5: linarith ✓ (atoms: log(6+δ), log(7+δ), log((6+δ)(7+δ)), log(16.5·16.5), log 16.5, log(1/δ) ✓ linear).\n\nHmm — h1 needs rewrites INSIDE the goal? linarith uses h1 as a linear equation between atoms ✓ (log(6+δ) + log(7+δ) = log((6+δ)(7+δ)) — atom-level equation ✓ linarith handles ✓.\n\nReal.log_mul (ha : a ≠ 0) (hb : b ≠ 0) : log (a * b) = log a + log b ✓. So h1 : log(6+δ) + log(7+δ) = log((6+δ)(7+δ)) := (Real.log_mul ...).symm ✓.\n\nThe positivity side goals: 6+δ ≠ 0 (δ > 0 ⟹ 6+δ > 0 ✓ ne_of_gt, positivity or linarith), 7+δ ≠ 0 ✓, (6+δ)(7+δ) > 0 ✓ (Real.log_le_log's first arg: 0 < (6+δ)(7+δ) — by positivity with hδ in context? positivity: 6+δ > 0 needs hδ — positivity uses hyps ✓ hmm — 6+δ: positivity proves 0 < 6+δ? It needs δ > 0 — from hδ in context ✓ positivity should manage; fallback nlinarith).\n\nh2's inequality: (6+δ)(7+δ) ≤ 16.5·16.5 = 272.25: nlinarith [hδ, hδ1] — (6+δ)(7+δ) = 42 + 13δ + δ² ≤ 42+13+1 = 56 ≤ 272.25 ✓ nlinarith (needs δ² ≤ δ or δ² ≤ 1: from hδ1 : δ ≤ 1 and hδ : 0 < δ: δ² ≤ δ·1 = δ ✓ product hint — nlinarith pairwise ✓).\n\n**E. The final per-zero bound with the clearance**: per ρ ∈ nearZerosSub T: with δ_ρ := |T − γ_ρ|:\n- 0 < δ_ρ: from hTwide (δ ≥ c_clear > 0).\n- δ_ρ ≤ 1: mem_nearZerosSub gives |γ − T| < 1 — hmm |ρ.im − T| < 1 — and δ_ρ = |T − γ| = |γ − T| ✓ (abs_sub_comm) — so δ_ρ < 1 hence ≤ 1 ✓.\n- The integral bound: ∫ dσ/√((σ−β)²+δ²) ≤ 2·log(16.5/δ) [from C+D combined] ≤ 2·log(148.5·C0hat(√n+2)) [from δ ≥ c_clear].\n\nCombine C+D into one: per_zero_integral_le {β δ} (hβ0) (hβ1) (hδ) (hδ1) : ∫ ≤ 2·log(16.5/δ). Then the clearance step per ρ.\n\n**F. The near-sum bound**: \n```lean\n-- per ρ: ‖∫ σ, m/(s σ − ρ)‖ machinery\n∫ σ in -5/2..3, ‖Σ_{ρ ∈ nearZerosSub T} (zeroMult ρ.1 : ℂ)/(s σ − ρ.1)‖ dσ\n  ≤ ∫ σ, Σ_ρ ‖(zeroMult ρ.1:ℂ)/(s σ − ρ.1)‖ := integral_mono (norm_sum_le)\n  = ∫ σ, Σ_ρ (zeroMult ρ.1 : ℝ)/‖s σ − ρ.1‖ \n  ≤ ∫ σ, Σ_ρ (zeroMult ρ.1 : ℝ) * (1/√((σ−β_ρ)²+δ_ρ²))  -- ‖s−ρ‖ = √(...) so m/‖s−ρ‖ = m·(1/√(...))\n  = Σ_ρ (zeroMult ρ.1 : ℝ) * ∫ σ, 1/√(...)  -- integral_finsetSum + integral_const_mul\n  ≤ Σ_ρ (zeroMult ρ.1 : ℝ) * (2·log(148.5·C0hat(√n+2)))\n  = (2·log(148.5·C0hat(√n+2))) · Σ_ρ mult\n  ≤ 2·Z2hat(T)·log(148.5·C0hat(√n+2))\n```\n\nThe identity ‖s σ − ρ.1‖ = √((σ−β)² + (T−γ)²): \n```lean\nhave hnormid : ‖((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1‖ =\n    Real.sqrt ((σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2) := by\n  have h1 : Complex.normSq (((σ : ℝ) + (T : ℝ) * Complex.I) - ρ.1) =\n      (σ - ρ.1.re) ^ 2 + (T - ρ.1.im) ^ 2 := by\n    simp [Complex.normSq_apply, Complex.sub_re, Complex.add_re, Complex.ofReal_re,\n      Complex.mul_re, Complex.I_re, Complex.I_im, Complex.sub_im, Complex.add_im,\n      Complex.ofReal_im, Complex.mul_im, Complex.I_re]\n    ring\n  -- ‖z‖ = √(normSq z)\n  rw [← h1]  -- hmm need ‖z‖ = √(normSq z)\n  exact (Complex.norm_def ...)? \n```\nComplex.norm: `Complex.norm z = Real.sqrt (normSq z)`? — `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? Let me check — `Complex.norm_def (z : ℂ) : ‖z‖ = Real.sqrt (normSq z)`? I believe `Complex.norm` is defined via normSq sqrt — there IS `Complex.norm_def : ‖z‖ = √(normSq z)`? or `Complex.norm_eq_sqrt_normSq`? Let me grep. Actually `Complex.normSq_eq_norm_sq : normSq z = ‖z‖ ^ 2` — so ‖z‖ = √(normSq z) via `Complex.norm_eq_sqrt_normSq`?? — hmm, in Mathlib: `Complex.norm_def : ‖z‖ = Real.sqrt (normSq z)`? Let me just grep for it.\n\nAnd (T − γ)² = δ² with δ := |T − γ|: `sq_abs (T − γ) : |T−γ|² = (T−γ)²`? `sq_abs (a) : |a| ^ 2 = a ^ 2` ✓ exists (sq_abs). So (T−γ)² = |T−γ|² = δ² ✓.\n\nThen 1/‖s−ρ‖ = 1/√((σ−β)²+δ²) and m/‖s−ρ‖ = m·(1/√(...)) (div_eq_mul_one_div or mul_one_div.symm).\n\n**G. The R-part integral**: \n```lean\n∫ σ in -5/2..3, ‖logDeriv ζ (σ+iT) − Σ_near‖ dσ ≤ (3 − -5/2)·(10.5·log(T+2)+48)\n```\npointwise capstone per σ ∈ Icc(−5/2,3): needs ht : 10 ≤ T ✓, hσlo : −5/2 ≤ (σ+iT).re = σ ✓ (σ ≥ −5/2 from Icc), hσhi : σ ≤ 3 ✓, him : im = T, hζ : zeta_ne_zero_horizontal hTwide hn hTn hTn1 σ... wait — zeta_ne_zero_horizontal's statement: riemannZeta ((σ:ℝ) + (T:ℝ)*I) ≠ 0 ✓ EXACTLY the path point ✓ (hTwide) (hn : 1 ≤ n) (hTn) (hTn1).\n\nHmm wait — zeta_ne_zero_horizontal {n T σ} (hTwide ...) (hn : 1 ≤ n) (hTn : √n ≤ T) (hTn1 : T ≤ √n+1) : riemannZeta (↑σ + ↑T * I) ≠ 0 ✓.\n\nThe capstone bound: ‖logDeriv − Σ‖ ≤ 10.5·log(|T|+2)+48 = 10.5·log(T+2)+48 (|T| = T, T ≥ 0). So per σ ≤ K_R := 10.5·log(T+2)+48 — constant in σ ✓ integral_const: (3 − −5/2)·K_R = 5.5·K_R ✓.\n\nIntegrability of ‖logDeriv − Σ‖: continuous (logDeriv continuous on the path via zeta_ne_zero_horizontal; the sum continuous — each term (zeroMult)/(s−ρ) continuous in s (denominator nonzero: s−ρ ≠ 0 since s = σ+iT and ρ has im ≠ T... wait — could s = ρ? ρ = β+iγ with γ = T? — ρ ∈ nearZerosSub T has |γ−T| < 1 — if γ = T then s = ρ would need σ = β — possible?! Hmm — s ranges over σ ∈ [−5/2,3] with im T; ρ with im γ: s − ρ = 0 ⟺ σ = β ∧ T = γ. If γ = T, then at σ = β the difference vanishes!! BUT — zeta_ne_zero_horizontal says ζ(σ+iT) ≠ 0 for all σ — and ρ is a zero — so s ≠ ρ always (since ζ(s) ≠ 0 = ζ(ρ) ⟹ s ≠ ρ ✓). But for the CONTINUITY of 1/(s−ρ) along the path, I need s−ρ ≠ 0 — which follows from: if s − ρ = 0 then s = ρ, then ζ(s) = ζ(ρ) = 0, contradicting zeta_ne_zero_horizontal ✓. So s−ρ ≠ 0 on the path ✓.\n\nActually — hmm, more precisely: the capstone APPLICATION needs hζ : riemannZeta s ≠ 0 (given by zeta_ne_zero_horizontal) ✓. And the sum's continuity per term: (fun σ => (zeroMult ρ.1 : ℂ)/(↑σ + ↑T·I − ρ.1)) — continuous if the denominator never vanishes: (↑σ + ↑T·I) − ρ.1 ≠ 0 — as argued (else ζ zero) ✓.\n\n**H. The full mid-horizontal bound**: \n‖Jlag‖ ≤ (e⁴+1)·‖logDeriv‖ pointwise; ∫‖Jlag‖ ≤ (e⁴+1)·∫‖logDeriv‖ (integral_mono_on with constant factor — actually: ∫(e⁴+1)·‖logDeriv‖ = (e⁴+1)·∫‖logDeriv‖ via intervalIntegral.integral_const_mul; pointwise mul_le_mul (kernel bound) ... (norm_nonneg) (e⁴+1 ≥ 0)).\n\n∫‖logDeriv‖ ≤ ∫(‖R‖ + ‖Σ‖) = ∫‖R‖ + ∫‖Σ‖ — integral_mono_on (pointwise norm_le_insert') + intervalIntegral.integral_add (integrability both).\n\nThen ∫‖R‖ ≤ 5.5·K_R and ∫‖Σ‖ ≤ NI — total: ∫‖logDeriv‖ ≤ NI + 5.5·K_R — wait no: ∫‖logDeriv‖ ≤ ∫‖R‖ + ∫‖Σ‖ ≤ 5.5K_R + NI. Then ‖H(−5/2→3, T)‖ ≤ (e⁴+1)·(5.5·K_R + NI).\n\nAnd the kernel bound per σ: kFun_shift_norm_le_exp_four_add_one with s := ↑(σ−1) + ↑T·I: need kFun n (s+1) where s+1 = ↑σ + ↑T·I — cast: ↑(σ−1)+1 = ↑σ ✓ push_cast; ring. re s = σ−1 ≤ 3 ⟸ σ ≤ 4 ⟸ σ ≤ 3 ✓ (Icc). im s = T: n ≤ T² — from √n ≤ T: n = √n² ≤ T² (sq_le_sq... n = (√n)² ≤ T² via Real.sq_sqrt + sq_le_sq₀ or nlinarith [hTn, Real.sqrt_nonneg, sq_sqrt]). \n\nHmm — kFun_shift_norm_le_exp_four_add_one (hσ : s.re ≤ 3) (hT : (n:ℝ) ≤ s.im ^ 2) : ‖kFun n (s + 1)‖ ≤ exp 4 + 1 — with s := ↑σ + ↑T·I − 1 (so s + 1 = ↑σ + ↑T·I): re s = σ−1, im s = T. Let me set s := (↑σ + ↑T*Complex.I) − 1 — then s + 1 = ↑σ + ↑T·I by ring (sub_add_cancel). re s = σ − 1: simp. im s = T: simp.\n\n**I. The bottom side (−T)**: conj trick cloning DL-5.\n\nNow — the ordering of lemmas in the file. This is a LOT. Let me also double-check the integrability of the per-ρ summand integrands for integral_finsetSum: (fun σ => (zeroMult ρ.1 : ℝ) * (1/√((σ−β)²+δ²))) — continuous (const · continuous) ✓ per-term integrable ✓.\n\nAnd for the ∫‖Σ‖ ≤ ∫Σ‖term‖ step: integral_mono_on needs the pointwise norm_sum_le ✓ and integrability of both sides: ‖Σ·‖ (norm of continuous ✓) and Σ‖·‖ (Finset.sum of continuous ✓).\n\nThe equality chain ∫ Σ m/‖s−ρ‖ = Σ ∫ m/‖s−ρ‖: intervalIntegral.integral_finsetSum with per-term integrability ✓. And ∫ m·(1/√) = m·∫ 1/√: intervalIntegral.integral_const_mul ✓ (signature: integral_const_mul (c : ℝ) (f : ℝ → ℝ) : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x ✓ exists).\n\nHmm — actually, the near-sum's complex terms: the Σ in the capstone is over ℂ-valued terms (zeroMult ρ.1 : ℂ)/(s − ρ.1). The pointwise norm: ‖Σ_ρ term_ρ‖ ≤ Σ_ρ ‖term_ρ‖ = Σ_ρ (zeroMult : ℝ)/‖s−ρ‖ (norm_div + natCast norm — clone the 6-c-ii h2 pattern per term).\n\nThen the integrand split: Σ_ρ m_ρ/‖s σ −ρ‖ = Σ_ρ m_ρ·(1/√((σ−β_ρ)²+δ_ρ²)) — this is a pointwise (in σ) Finset-sum identity — sum_congr with the per-ρ norm identity ✓.\n\nThen ∫σ Σ_ρ m_ρ·(1/√(...)) dσ = Σ_ρ ∫σ m_ρ·(1/√(...)) dσ (integral_finsetSum) = Σ_ρ m_ρ·∫σ 1/√(...) (integral_const_mul per term — need sum_congr) ≤ Σ_ρ m_ρ·(2·log(148.5·C0hat(√n+2))) (sum_le_sum with per-zero bound × m_ρ ≥ 0) = (2·log(148.5·C0hat(√n+2)))·Σ_ρ m_ρ (Finset.mul_sum.symm... — Σ m·B0 = B0·Σm hmm: Σ_ρ m_ρ·B0 = B0·Σ_ρ m_ρ via: each m_ρ·B0 = B0·m_ρ (mul_comm) — or Finset.mul_sum: B0·Σm = Σ B0·m — so Σ m·B0 = Σ B0·m (sum_congr mul_comm) = B0·Σm (Finset.mul_sum.symm)). Then ≤ B0·Z2hat(T) (mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 hT10) (B0 ≥ 0)).\n\nB0 := 2·log(148.5·C0hat(√n+2)) ≥ 0: log(148.5·C0hat(√n+2)) ≥ 0 ⟸ 148.5·C0hat(√n+2) ≥ 1 ⟸ C0hat(√n+2) ≥ 2 ✓ (two_le_C0hat, √n+2 ≥ 1). Real.log_nonneg (1 ≤ x) ✓.\n\nOK. And NI := 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt n + 2)) — hmm — the association: 2·Z2hat·log vs B0·Z2hat = 2·log·Z2hat — same by ring.\n\nThe final per-side statement:\n```lean\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n    (hNLZ : NoLowZeros) {n : ℕ} (hn : 100000 ≤ n) {T : ℝ}\n    (hTwide : ∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im →\n      ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|)\n    (hTn : Real.sqrt n ≤ T) (hTn1 : T ≤ Real.sqrt n + 1) :\n    ‖HIntegral (Jlag n) (-5/2) 3 T‖ ≤\n      (Real.exp 4 + 1) * (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt n + 2)) +\n        (3 - -5/2) * (10.5 * Real.log (T + 2) + 48))\n```\n\nand the neg version hIntegral_Jlag_mid_neg_norm_le (same bound) via the conj trick.\n\nHmm — the hTwide hypothesis: it's the output of exists_zero_avoiding_T_wide — let me check that exact form (it's an ∃-statement at 6-d; the 6-c theorems take it as a hypothesis, like zeta_ne_zero_horizontal does). zeta_ne_zero_horizontal's hTwide: `∀ ρ : ℂ, IsNontrivialZero ρ → Real.sqrt n - 1 < ρ.im → ρ.im < Real.sqrt n + 2 → 1 / (9 * C0hat (Real.sqrt n + 2)) ≤ |ρ.im - T|` ✓ — same form. \n\nFor the per-ρ δ-lower bound: ρ ∈ nearZerosSub T with γ := ρ.1.im: hTwide ρ.1 ρ.2 (γ ∈ (√n−1, √n+2)): |γ − T| ≥ 1/(9·C0hat(√n+2)). The window: γ ∈ (T−1, T+1) from |γ − T| < 1 (mem_nearZerosSub) — and (T−1, T+1) ⊆ (√n−1, √n+2): T−1 ≥ √n−1 ✓ (hTn: √n ≤ T); T+1 ≤ √n+2 ✓ (hTn1: T ≤ √n+1). So √n−1 ≤ T−1 < γ ✓ and γ < T+1 ≤ √n+2 ✓ — hTwide needs STRICT: √n−1 < γ: from √n−1 ≤ T−1 < γ ✓ linarith. ✓.\n\nδ_ρ := |T − γ| — hmm, hTwide gives |γ − T| ≥ c_clear; mem_nearZerosSub gives |γ − T| < 1. So work with δ' := |γ − T| throughout (avoid abs_sub_comm): the norm identity ‖s−ρ‖ = √((σ−β)²+(T−γ)²) needs (T−γ)² = |γ−T|²: (T−γ)² = (γ−T)² (neg_sq) = |γ−T|² (sq_abs) ✓.\n\nSo per-ρ: δ' := |ρ.1.im − T|; 0 < c_clear ≤ δ' (hTwide) and δ' < 1 (mem). The FTC bound applies with δ := δ' > 0 ✓ and δ' ≤ 1 ✓.\n\nPer-zero integral ≤ 2·log(16.5/δ') ≤ 2·log(148.5·C0hat(√n+2)): the last step: 16.5/δ' ≤ 148.5·C0hat(√n+2): 1/δ' ≤ 9·C0hat(√n+2): from δ' ≥ 1/(9·C0hat(√n+2)): `one_div_le_one_div_of_le (one_div_pos.mpr (by positivity)) h` — a := 1/(9C), b := δ': 1/δ' ≤ 1/(1/(9C)) — and 1/(1/(9C)) = 9C (one_div_one_div). ✓. Then 16.5·(1/δ') ≤ 16.5·(9·C0hat) = 148.5·C0hat ✓ (mul_le_mul_of_nonneg_left ... 16.5 ≥ 0). Then Real.log_le_log (16.5/δ' > 0) that ✓.\n\nHmm — 16.5/δ' = 16.5·(1/δ') — div_eq_mul_one_div... write 16.5/δ' as 16.5 * (1/δ')? The per-zero bound's final form: 2·log(16.5/δ'). For the comparison: log(16.5/δ') ≤ log(148.5·C0hat) ⟸ Real.log_le_log (0 < 16.5/δ' := by positivity) (16.5/δ' ≤ 148.5·C0hat). The division forms: 16.5/δ' — positivity ✓ (δ' > 0). The ≤: \n```lean\nhave hcomp : 16.5 / δ' ≤ 148.5 * C0hat (√n + 2) := by\n  rw [div_le_iff₀ hδ'0]  -- 16.5 ≤ 148.5·C0hat·δ'\n  ...\n```\n16.5 ≤ 148.5·C·δ' ⟸ δ' ≥ 1/(9C): 148.5·C·δ' ≥ 148.5·C·(1/(9C)) = 148.5/9 = 16.5 ✓. nlinarith [hδ'_ge, hC0pos]? 148.5·C·δ' ≥ 148.5·C·(1/(9C)) = 16.5·(9C)/(9C) = 16.5 — needs C·(1/(9C)) = 1/9·... — the product C·(1/(9·C)) = 1/9 — needs C ≠ 0 — as a FIELD identity — nlinarith can't do division. Provide explicitly:\n```lean\nhave hC0 : (0:ℝ) < C0hat (√n + 2) := by\n  have h2 := two_le_C0hat (by positivity... : 1 ≤ √n + 2)\n  linarith\nhave h9C : (0:ℝ) < 9 * C0hat (√n + 2) := by positivity\nhave hge : 1 / (9 * C0hat (√n + 2)) ≤ δ' := hTwide-applied\nhave hinv : 1 / δ' ≤ 9 * C0hat (√n + 2) := by\n  have := one_div_le_one_div_of_le (one_div_pos.mpr h9C) hge\n  rwa [one_div_one_div] at this\nhave hcomp : 16.5 / δ' ≤ 148.5 * C0hat (√n + 2) := by\n  rw [div_le_iff₀ hδ'0]\n  -- 16.5 ≤ 148.5·C0hat·δ'\n  have h1 : 16.5 * (1 / δ') ≤ 16.5 * (9 * C0hat (√n + 2)) :=\n    mul_le_mul_of_nonneg_left hinv (by norm_num)\n  rw [mul_comm, ← div_eq_mul_one_div] at h1  -- hmm\n  -- h1 : 16.5/δ' ≤ 148.5·C0hat\n  nlinarith [h1, hδ'0]  -- 16.5 ≤ (16.5/δ')·δ' = ... \n```\nHmm messy. Cleaner: 16.5 ≤ 148.5·C·δ' ⟺ (multiply hinv by 16.5·δ' ≥ 0): 16.5·δ'·(1/δ') ≤ 16.5·δ'·(9C) ⟹ 16.5 ≤ 16.5·(9C)·δ' = 148.5·C·δ' ✓ — 16.5·δ'·(1/δ') = 16.5·(δ'/δ') = 16.5·1 = 16.5 (δ' ≠ 0) — field identity — nlinarith can't; use field_simp or:\n```lean\nhave hcomp : 16.5 / δ' ≤ 148.5 * C0hat (√n + 2) := by\n  have h1 : 16.5 * (1 / δ') ≤ 16.5 * (9 * C0hat (√n + 2)) :=\n    mul_le_mul_of_nonneg_left hinv (by norm_num)\n  rw [show (16.5 : ℝ) * (1 / δ') = 16.5 / δ' by rw [mul_one_div],\n    show (16.5 : ℝ) * (9 * C0hat (√n + 2)) = 148.5 * C0hat (√n + 2) by ring] at h1\n  exact h1\n```\nmul_one_div : a * (1/b) = a/b ✓. And 16.5·9 = 148.5 ✓ ring.\n\nOK — this is going to be a large amount of Lean. Let me also double check `Real.log_div` signature: `Real.log_div (hx : x ≠ 0) (hy : y ≠ 0) : Real.log (x / y) = Real.log x - Real.log y` ✓.\n\n`Real.log_pow (n : ℕ) (x : ℝ) : Real.log (x ^ n) = n * Real.log x` ✓.\n\n`Real.log_one : Real.log 1 = 0` ✓.\n\n`neg_sq (a) : (-a) ^ 2 = a ^ 2` — hmm — it's `neg_sq : (-a) ^ 2 = a ^ 2` ✓ exists (even_pow). Or use `Even.neg_pow`? neg_sq exists for sure.\n\n`sq_abs (a : ℝ) : |a| ^ 2 = a ^ 2` ✓ exists.\n\n`neg_abs_le (a) : -a ≤ |a|` ✓.\n\n`Real.sqrt_sq_eq_abs (x) : √(x^2) = |x|` ✓.\n\n`Real.sqrt_lt_sqrt (hx : 0 ≤ x) (h : x < y) : √x < √y` ✓.\n\n`Real.sqrt_pos.mpr : 0 < x → 0 < √x` ✓.\n\n`Real.sq_sqrt (h : 0 ≤ x) : √x ^ 2 = x` ✓.\n\n`div_le_div_of_nonneg_left` — signature? `div_le_div_of_nonneg_left (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a / c ≤ a / b`? — hmm — from LiTightR line 172: `div_le_div_of_nonneg_left (Nat.cast_nonneg _) (by norm_num : (0:ℝ) < 1) h1` giving `m/‖s−ρ‖ ≤ m/1` — so (ha : 0 ≤ a) (hb : 0 < b) (h : b ≤ c) : a / c ≤ a / b ✓ — with a := δ², b := u+√, c := 7+δ: δ²/(7+δ) ≤ δ²/(u+√) ✓ EXACTLY what I need for the left endpoint.\n\n`Real.sqrt_le_iff`? For √h ≤ x+δ: use sq_le_sq₀ or: `Real.sqrt_le_iff (hy : 0 ≤ y)?` — let me instead use: `Real.sqrt_le' ?`... — safest: \n```lean\nhave hsqrt_le : Real.sqrt (x ^ 2 + δ ^ 2) ≤ x + δ := by\n  have h1 : (Real.sqrt (x ^ 2 + δ ^ 2)) ^ 2 ≤ (x + δ) ^ 2 := by\n    rw [Real.sq_sqrt (by positivity)]\n    nlinarith [hδ, hx0]\n  have h2 : 0 ≤ x + δ := by linarith [hx0, hδ]\n  -- from sq ≤ sq with both nonneg: a ≤ b\n  exact (sq_le_sq₀ (Real.sqrt_nonneg _) h2).mp?...\n```\nHmm — sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b? or the iff the other way — `sq_le_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 ≤ b ^ 2 ↔ a ≤ b`? Banked: \"sq_eq_sq₀\" and \"pow_le_one₀'s implicit n\". Let me check sq_le_sq₀'s exact form via grep later. Alternative robust: `Real.sqrt_le_iff`: grep says? I'll check: there's `Real.sqrt_le_iff {x y : ℝ} (hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y^2`?? Hmm — actually I recall `Real.sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2`. And `Real.sqrt_le' {y} (hy : 0 < y) : √x ≤ y ↔ x ≤ y^2`?? Let me grep both.\n\nLet me also check `one_div_pos.mpr`, `one_div_one_div (a) : 1/(1/a) = a` ✓ exists (one_div_one_div). \n\n`Real.log_le_log (hx : 0 < x) (h : x ≤ y) : log x ≤ log y` ✓ used already.\n\nAlso `integral_mono_on` for the ∫‖Jlag‖ ≤ ∫(e⁴+1)·‖logDeriv‖ step — with the constant factor integrand (fun σ => (e⁴+1)·‖logDeriv ζ (s σ)‖) — continuous ✓.\n\nAnd ∫(e⁴+1)·‖logDeriv‖ = (e⁴+1)·∫‖logDeriv‖: intervalIntegral.integral_const_mul ✓.\n\nThen ∫‖logDeriv‖ ≤ ∫‖R‖ + ∫‖Σ‖: intervalIntegral.integral_add hR_int hΣ_int : ∫(‖R‖ + ‖Σ‖) = ∫‖R‖ + ∫‖Σ‖; pointwise: ‖logDeriv‖ ≤ ‖R‖ + ‖Σ‖ via norm_le_insert' (with R := logDeriv − Σ... wait — norm_le_insert' a b : ‖a‖ ≤ ‖b‖ + ‖a − b‖ — a := logDeriv, b := Σ: ‖logDeriv‖ ≤ ‖Σ‖ + ‖logDeriv − Σ‖ — hmm — I want ‖logDeriv‖ ≤ ‖R‖ + ‖Σ‖ with R = logDeriv − Σ: norm_le_insert' gives ‖logDeriv‖ ≤ ‖Σ‖ + ‖logDeriv−Σ‖ = ‖Σ‖ + ‖R‖ — commuted — fine (linarith/add_comm).\n\nIntegrability of ‖R‖ = ‖logDeriv − Σ‖: logDeriv continuous on path (zeta_ne_zero_horizontal), Σ continuous (sum of continuous divisions) ⟹ sub continuous ⟹ norm continuous ✓.\n\nThe kernel: per σ: ‖kFun n (↑σ+↑T·I)‖ = ‖kFun n ((↑σ+↑T·I−1)+1)‖ — kFun_shift_norm_le_exp_four_add_one (s := ↑σ+↑T·I−1): (hσ : (↑σ+↑T·I−1).re ≤ 3) : re = σ−1: σ ≤ 3 ⟹ σ−1 ≤ 2 ≤ 3 ✓; (hT : (n:ℝ) ≤ (↑σ+↑T·I−1).im^2) : im = T: n ≤ T² — from √n ≤ T: n = √n² ≤ T²: \n```lean\nhave hnT2 : (n : ℝ) ≤ T ^ 2 := by\n  have h1 : (Real.sqrt n) ^ 2 ≤ T ^ 2 := by\n    apply sq_le_sq₀?... -- √n ≤ T, both ≥ 0\n  rwa [Real.sq_sqrt (by positivity : 0 ≤ (n:ℝ))] at h1\n```\nHmm — need √n ≤ T ⟹ √n² ≤ T²: sq_le_sq₀ (√n ≥ 0) (T ≥ 0) — if sq_le_sq₀ is the iff: (sq_le_sq₀ h1 h2).mpr hTn? — wait direction: √n ≤ T with 0 ≤ √n, 0 ≤ T ⟹ √n² ≤ T² — `pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2` : (√n)^2 ≤ T^2 ✓ SIMPLER (pow_le_pow_left₀ (0≤a) (a≤b) n : a^n ≤ b^n ✓). Then rw [Real.sq_sqrt] at that: (↑n) ≤ T^2 — wait Real.sq_sqrt : √x^2 = x — rw at h1 : (↑n) ≤ T^2 ✓.\n\nThen ‖kFun n (s+1)‖ ≤ e⁴+1 with s+1 = ↑σ+↑T·I: `(s+1) = ↑σ + ↑T*I` — s := (↑σ + ↑T*I) − 1 so s+1 = ↑σ+↑T·I via sub_add_cancel ✓ — the lemma gives ‖kFun n ((↑σ+↑T·I−1)+1)‖ — need to rewrite (↑σ+↑T·I−1)+1 = ↑σ+↑T·I: `sub_add_cancel`? — a−1+1 = a: `sub_add_cancel : a - b + b = a`? — sub_add_cancel (a b) : a − b + b = a ✓ — with b := 1 ✓. So:\n```lean\nhave hker : ∀ σ ∈ Set.Icc (-5/2 : ℝ) 3, ‖kFun n ((σ:ℝ) + (T:ℝ)*Complex.I)‖ ≤ Real.exp 4 + 1 := by\n  intro σ hσ\n  obtain ⟨hσ1, hσ2⟩ := hσ\n  have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\n    (s := ((σ:ℝ) + (T:ℝ)*Complex.I - 1)) (by simp...) (by simp...; exact hnT2)\n  rwa [sub_add_cancel] at h1\n```\n\nHmm — kFun_shift's s is implicit {s : ℂ} — pin (s := ...). hσ: s.re ≤ 3 — (↑σ+↑T·I−1).re = σ−1: by simp + linarith [hσ2]. The by-block: `by have hre : (...).re = σ - 1 := by simp [...]; rw [hre]; linarith [hσ2]`. Wait — simp computing (↑σ+↑T*I−1).re: sub_re: (↑σ+↑T·I).re − 1; add_re: σ + 0; → σ − 1 ✓. `by simp` should do it (as before with explicit lemma list or plain simp — plain simp worked for these re computations in zeta_ne_zero_left_vertical ✓).\n\nhT hyp: (↑n:ℝ) ≤ (↑σ+↑T·I−1).im^2 — im = T: by simp gives (↑n) ≤ T^2 ✓ exact hnT2. So `by simp [Complex.sub_im, ...]` — hmm — the goal after simp: (n:ℝ) ≤ T^2 — simp might also simplify... just: `by have him : (...).im = T := by simp [...]; rw [him]; exact hnT2`.\n\nrwa [sub_add_cancel] at h1: h1 : ‖kFun n ((↑σ+↑T·I−1)+1)‖ ≤ e⁴+1 — sub_add_cancel : a − b + b = a — the term (↑σ+↑T·I)−1+1 — rw transforms to ↑σ+↑T·I ✓ — hmm — sub_add_cancel (a b) : a - b + b = a — pattern ?a − ?b + ?b — matches (↑σ+↑T·I) − 1 + 1 with ?a := ↑σ+↑T·I, ?b := 1 ✓.\n\nAlright — this 6-c-iv is genuinely large (~450-550 lines). Let me organize the file §4 as:\n\n1. `integral_one_div_sqrt_sq_add_sq` — the FTC machine (β δ general, a b general).\n2. `arcsinh_right_endpoint_le` (F(3) ≤ log(6+δ)).\n3. `arcsinh_left_endpoint_le` (−F(−5/2) ≤ log(7+δ)+2log(1/δ)).\n4. `per_zero_integral_le_two_log` — combine (≤ 2·log(16.5/δ)) incl. D's log-mono simplification.\n5. `hIntegral_Jlag_mid_norm_le` — the top side.\n6. `hIntegral_Jlag_mid_neg_norm_le` — the bottom via conj.\n\nLet me double check a few more signatures before writing: sq_le_sq₀ (not needed — using pow_le_pow_left₀), Real.sqrt_le_iff (for √h ≤ x+δ), Real.continuous_sqrt, intervalIntegral.integral_const_mul, Continuous.pow, Real.log_div, Real.log_mul, Real.log_pow, neg_sq, sq_abs, one_div_one_div, div_le_div_of_nonneg_left (verified in LiTightR ✓), abs_of_nonneg/abs_of_neg ✓, Real.log_one, Real.log_nonneg, two_le_C0hat ✓ (LiContour line 169).\n\nFor Real.sqrt_le_iff — grep.","signature":""},{"type":"text","text":"All patterns confirmed. Checking the last few signatures before writing §4."},{"type":"tool_use","id":"Bash_92","name":"Bash","input":{"command":"grep -rn \"theorem sqrt_le_iff\\|theorem sqrt_le' \" \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/Analysis/Real/Sqrt.lean\" | head -4; grep -rn \"theorem continuous_sqrt\" \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/Analysis/SpecialFunctions/Sqrt.lean\" | head -2; grep -rn \"theorem integral_const_mul \\|theorem integral_const_mul(\" \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean\" | head -3; grep -rn \"theorem Continuous.pow \\|theorem log_pow \\|theorem log_div \\|theorem log_mul \\|theorem neg_sq \\|theorem sq_abs \\|theorem one_div_one_div \\|theorem sqrt_sq_eq_abs\" \"D:/Python/Quantum/zeta-23-lean/.lake/packages/mathlib/Mathlib/\" 2>/dev/null | head -12","description":"Verify sqrt/log/pow lemma signatures"},"extra_content":null}]