[{"type":"thinking","thinking":"`intervalIntegral.norm_integral_le_of_norm_le_const (h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C) : ‖∫ x in a..b, f x‖ ≤ C * |b - a|` — takes Ι a b (uIoc) and gives C·|b−a|. For a ≤ b: |b−a| = b−a. So:\n\n```\n  have hint : ‖∫ t in T..U, Jlag n ((3:ℝ) + t * Complex.I)‖ ≤\n      ((Real.exp (5/2) + 1) * (1/2)) * |U - T| :=\n    intervalIntegral.norm_integral_le_of_norm_le_const (fun t ht => hbound t (Set.uIoc_of_le ... ▸ ht))\n```\nhbound takes t ∈ Icc: Ι T U ⊆ Icc T U ✓ (Set.uIoc_subset_Icc_self? uIoc T U = Ioc (min) (max)... for T ≤ U: Ι T U = Ioc T U ⊆ Icc T U ✓ via Set.Ioc_subset_Icc_self). So hbound's hypothesis can be stated for Ι directly or convert.\n\nWrite hbound for t ∈ Ι T U: ht.1 : min T U < t... for T ≤ U: Ι T U = Ioc T U: ht : t ∈ Ioc T U: ht.1 : T < t, ht.2 : t ≤ U. Then t² ≥ T² needs T < t ✓ (nlinarith).\n\nNow write the whole DL-2 block (append to LiDogLeg.lean before `end NguyenRH1`):\n\n```lean\n/-! ## 3. The left-lift bound (DL-2, D-074 §3.3 V_left) -/\n\n/-- **Kernel on the lift**: ‖kFun n (3+it)‖ ≤ e^{5/2}+1 for n ≤ t²\n(the |(3+it)/(2+it)|² = 1+5/(4+t²) computation, D-074 §6). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : ℕ} {t : ℝ}\n    (hT : (n : ℝ) ≤ t ^ 2) :\n    ‖kFun n ((3 : ℝ) + t * Complex.I)‖ ≤ Real.exp (5 / 2) + 1 := by\n  ... (as designed)\n\n/-- The Dirichlet majorant at s = 3. -/\ndef dirichletC3 : ℝ :=\n  ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖\n\n/-- Termwise 3-vs-2 comparison for the Λ L-series: Λ(n)/n³ ≤ (1/2)·Λ(n)/n². -/\nlemma norm_term_vonMangoldt_three_le_half (n : ℕ) : ...\n\n/-- dirichletC3 ≤ 1/2 (the termwise comparison + dirichletC2 ≤ 1). -/\nlemma dirichletC3_le_half : dirichletC3 ≤ 1 / 2 := ...\n\n/-- ‖ζ′/ζ s‖ ≤ dirichletC3 for re s ≥ 3 (the C2 clone). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ dirichletC3 := ...\n\n/-- ‖ζ′/ζ s‖ ≤ 1/2 for re s ≥ 3 (the certified C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ 1 / 2 := ...\n\n/-- **The left-lift bound** (D-074 §3.3 V_left): for 0 < T and T² ≥ n,\n‖VIntegral (Jlag n) 3 T U‖ ≤ (U − T)·(e^{5/2}+1)/2. -/\ntheorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}\n    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := ...\n```\n\nDetails on the norm_term comparison:\n```lean\nlemma norm_term_vonMangoldt_three_le_half (n : ℕ) :\n    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ ≤\n      (1 / 2) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ := by\n  simp only [LSeries.norm_term_eq]\n  split\n  · norm_num\n  · next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    · simp [ArithmeticFunction.vonMangoldt_one]\n    · have hn2 : 2 ≤ n := by omega\n      have hΛ : ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ =\n          ArithmeticFunction.vonMangoldt n :=\n        Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n      rw [hΛ]\n      have e : ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ 3 =\n          (1 / (n : ℝ)) * (ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ 2) := by\n        field_simp [show (n : ℝ) ≠ 0 by positivity]\n        ring\n      rw [e]\n      apply mul_le_mul_of_nonneg_right _ (by positivity)\n      · rw [div_le_div_iff_of_pos_left (by norm_num : (0 : ℝ) < 1)\n          (by norm_num : (0 : ℝ) < 2) (by positivity : (0 : ℝ) < (n : ℝ))]\n        exact_mod_cast hn2\n```\nHmm — wait: `Complex.norm_of_nonneg (hx : 0 ≤ x) : ‖(x : ℂ)‖ = x` — is that the name? There's `Complex.norm_of_nonneg`... or `Complex.norm_ofReal_of_nonneg`? Session-033 banked \"abs_re_le_norm as the robust norm-of-cast-expr route\". Let me use: `by rw [Complex.norm_eq_abs, ← Real.norm_eq_abs, Real.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg]` — safe. Or check vonMangoldt's norm lemma: there might be `ArithmeticFunction.norm_vonMangoldt`? Probably not. Use the Real.norm route.\n\nAlso the (3:ℂ)/(2:ℂ) re: (3:ℂ).re = 3 ✓ norm_term_eq uses n ^ s.re: ((3:ℂ).re) = 3 ✓ — the split's goal after norm_term_eq: `‖(Λ n : ℂ)‖ / n ^ ((3:ℂ).re) ≤ (1/2)·‖(Λ n:ℂ)‖ / n ^ ((2:ℂ).re)` — the ((3:ℂ).re) needs simplifying to 3: norm_term_eq's statement has n ^ s.re — with s = (3:ℂ): s.re = 3 — simp only [norm_term_eq] leaves n ^ (3:ℂ).re — hmm the `split` then the goal shows (3:ℂ).re — need `show` or simp to reduce ((3:ℂ).re) — `Complex.ofReal_re`? (3:ℂ) is OfNat.ofNat — (3:ℂ).re = 3 by `rfl`? or `Complex.ofNat_re`? Let me just include `Complex.ofNat_re`-ish in the simp only: `simp only [LSeries.norm_term_eq, Complex.ofNat_re]`?? Hmm — is there such a lemma? For numerals: ((3 : ℂ).re) = 3 — provable by `rfl` (the re of a numeral is defeq) — probably `Complex.add_re`-style not needed since (3:ℂ) is OfNat.ofNat 3 with .re defeq 3 — norm_num can close it, or the term_eq's s.re might just display as 3 directly... To be safe I'll structure the proof to rw [norm_term_eq] and then handle ((3:ℂ).re) via `show` or norm_num1. Actually the C2 proof's comparison `LSeries.norm_term_le_of_re_le_re _ (by simp; exact hs) n` — the `by simp` proved (2:ℂ).re ≤ s.re — simp handles numeral .re ✓. So in norm_term_eq, n ^ s.re with s = (3:ℂ): the ((3:ℂ).re) — simp [norm_term_eq] would simplify it via whatever — let me write `simp only [LSeries.norm_term_eq]` and if ((3:ℂ).re) appears unreduced, add a `show` with 3 explicitly: actually cleaner to state the lemma as:\n```\n    ‖LSeries.term Λ (3:ℂ) n‖ ≤ (1/2) * ‖LSeries.term Λ (2:ℂ) n‖\n```\nand after simp only [norm_term_eq] and split, the goal is (if n ≠ 0): ‖Λ n‖ / (n:ℝ) ^ ((3:ℂ).re) ≤ (1/2)·(‖Λ n‖/(n:ℝ)^((2:ℂ).re)) — I can add `Complex.ofNat_re`?? Hmm, safest: first `have h3re : ((3 : ℂ).re) = 3 := rfl` and `have h2re : ((2 : ℂ).re) = 2 := rfl` then rw [h3re, h2re]?? — ((3:ℂ).re) = 3 by rfl? (3:ℂ) is `OfNat.ofNat 3` : ℂ — its .re — the instance: OfNat.ofNat 3 on ℂ reduces to ⟨3, 0⟩?? — via `Complex.ofNat` instance: OfNat.ofNat n = ⟨n, 0⟩ — defeq, so ((3:ℂ).re) ≡ 3 by rfl ✓ (probably; if not, `by norm_num`).\n\nThen:\n```lean\nlemma dirichletC3_le_half : dirichletC3 ≤ 1 / 2 := by\n  have hsum3 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  calc dirichletC3 = ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ := rfl\n    _ ≤ ∑' n : ℕ, (1 / 2) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ :=\n        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n          (hsum2.mul_left (1 / 2))\n    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ ≤ 1 / 2 := by linarith [dirichletC2_le_one]\n```\n`Summable.tsum_le_tsum` — the C2 proof used it with (fun n => ...) hf hg ✓.\n`hsum2.mul_left (1/2)` : Summable (fun n => (1/2) * ‖term Λ 2 n‖) ✓ (Summable.mul_left — the session-037 gotcha: method form Summable.mul_left ✓).\n`tsum_mul_left : ∑' a, c * f a = c * ∑' a, f a` ✓ plain (session-037 banked ✓).\n\nThe C3 clone (norm_logDeriv_zeta_le_dirichletC3):\n```lean\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ dirichletC3 := by\n  have hs1 : (1 : ℝ) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum3 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖\n      ≤ dirichletC3 := by\n    show ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ ≤ _\n    calc ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖\n        ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ :=\n          norm_tsum_le_tsum_norm hsumS\n      _ ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum3\n      _ = dirichletC3 := rfl\n  calc ‖logDeriv riemannZeta s‖\n      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖ := by\n        rw [← h1, norm_neg]\n    _ ≤ dirichletC3 := hle\n```\n(near-verbatim clone with 3.)\n\nNow the kernel lemma — full text (careful with the norm computation):\n```lean\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : ℕ} {t : ℝ}\n    (hT : (n : ℝ) ≤ t ^ 2) :\n    ‖kFun n ((3 : ℝ) + t * Complex.I)‖ ≤ Real.exp (5 / 2) + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  · subst hn\n    simp only [kFun, pow_zero, sub_self, norm_zero]\n    positivity\n  · have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n    have ht2 : (0 : ℝ) < 4 + t ^ 2 := by positivity\n    have hn4t2 : (n : ℝ) ≤ 4 + t ^ 2 := by linarith [hT]\n    have hQpos : (0 : ℝ) ≤ (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n    have hQle : (9 + t ^ 2) / (4 + t ^ 2) ≤ Real.exp (5 / (n : ℝ)) := by\n      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n        field_simp [ht2.ne']\n        ring\n      rw [h1]\n      have h2 : 5 / (4 + t ^ 2) ≤ 5 / (n : ℝ) :=\n        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n      have h3 := Real.add_one_le_exp (5 / (n : ℝ))\n      linarith\n    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ Real.exp 5 := by\n      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ (Real.exp (5 / (n : ℝ))) ^ n :=\n            pow_le_pow_left₀ hQpos hQle n\n        _ = Real.exp 5 := by\n            rw [← Real.exp_nat_mul]\n            congr 1\n            have hn0 : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'\n            field_simp [hn0]\n    have hns3 : Complex.normSq ((3 : ℝ) + t * Complex.I) = 9 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hns2 : Complex.normSq ((2 : ℝ) + t * Complex.I) = 4 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hnorm : ‖((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)‖ =\n        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n      rw [norm_div, ← Real.sqrt_div hQpos, ← Complex.normSq_eq_norm_sq,\n        ← Complex.normSq_eq_norm_sq, hns3, hns2]\n    have hs1 : ((3 : ℝ) + t * Complex.I) - 1 = (2 : ℝ) + t * Complex.I := by ring\n    unfold kFun\n    rw [hs1]\n    calc ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n - 1‖\n        ≤ ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ :=\n          norm_sub_le _ _\n      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n          rw [norm_pow, hnorm, norm_one]\n      _ ≤ Real.exp (5 / 2) + 1 := by\n          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n ≤ Real.exp (5 / 2) := by\n            rw [Real.sqrt_pow]\n            calc Real.sqrt (((9 + t ^ 2) / (4 + t ^ 2)) ^ n)\n                ≤ Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt hQn\n              _ = Real.exp (5 / 2) := by rw [Real.sqrt_exp]; congr 1; ring\n          linarith [h4]\n```\nConcerns:\n- `div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)` — the signature: div_le_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b?? Let me recall the C2-clone usage at LiContour:527: `(div_le_div_iff_of_pos_left (by norm_num) hD (by positivity)).mpr hDn` gives `4 / Complex.normSq s ≤ 4 / (n:ℝ)` from `hDn : n ≤ normSq s` — so div_le_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a/b ≤ a/c ↔ c ≤ b ✓ (numerator fixed, bigger denominator smaller). In h2: 5/(4+t²) ≤ 5/n ⟺ n ≤ 4+t² = hn4t2 ✓ with hb := ht2 (b = 4+t²), hc := n-pos: (div_le_div_iff_of_pos_left (by norm_num : (0:ℝ) < 5) ht2 (by positivity : (0:ℝ) < n)).mpr hn4t2 ✓ matches the LiContour pattern ✓.\n- `Real.sqrt_pow`: `(√x) ^ n = √(x ^ n)` — signature: Real.sqrt_pow (n : ℕ) (x : ℝ)? or (x) (n)? In Mathlib: `theorem Real.sqrt_pow (n : ℕ) (x : ℝ) : (√x) ^ n = √(x ^ n)` — hmm I think it's `Real.sqrt_pow (x : ℝ) (n : ℕ)`?? Let me not guess: I'll write `rw [Real.sqrt_pow]` and if direction/args fail, adjust. Actually there are two: `Real.sqrt_sq (hx : 0 ≤ x) : √(x ^ 2) = x` and `Real.sqrt_pow : (√x)^n = √(x^n)`... I'll handle in the build.\n- `Real.sqrt_exp` : √(exp x) = exp (x / 2) ✓ then congr 1; ring for (5:ℝ)/2 = 5/2 — the calc target: √(exp 5) = exp (5/2): rw [Real.sqrt_exp] turns LHS into exp (5/2) where 5/2 is the real division — goal becomes exp (5/2) = exp (5/2)?? the written `congr 1; ring` handles 5/2 = 5/2 (identity — ring closes). Hmm — if both sides are identical after rw, the goal closes by rfl automatically — the congr 1; ring is harmless backup. Actually `rw [Real.sqrt_exp]` on the goal `√(exp 5) = exp (5/2)`: gives `exp (5/2) = exp (5/2)` — wait, the goal's RHS is `Real.exp (5 / 2)` and after rw LHS is `Real.exp (5 / 2)` — identical → closed by rfl automatically (rw closes rfl) ✓ so just `by rw [Real.sqrt_exp]` suffices... but the 5/2 might display differently: Real.sqrt_exp : √(exp x) = exp (x / 2) — with x = 5: exp (5/2) — the goal's exp (5/2): 5/2 vs (5:ℝ)/2 — same term ✓ rfl. Fine: `_ = Real.exp (5 / 2) := by rw [Real.sqrt_exp]`.\n\nNow the V_left assembly. VIntegral f x y₁ y₂ = I • ∫ y in y₁..y₂, f (x + y * I). With f = Jlag n, x = 3, y₁ = T, y₂ = U:\n```lean\ntheorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}\n    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  unfold VIntegral\n  rw [norm_smul, Complex.norm_I, one_mul]\n  have hbound : ∀ t ∈ Set.Ioc T U,\n      ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤ (Real.exp (5 / 2) + 1) * (1 / 2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]\n    have hre : 3 ≤ (((3 : ℝ) + t * Complex.I)).re := by simp\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3 : ℝ) + t * Complex.I) hre\n    have hnorm3 : ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ =\n        ‖kFun n ((3 : ℝ) + t * Complex.I)‖ * ‖logDeriv riemannZeta ((3 : ℝ) + t * Complex.I)‖ := by\n      show ‖kFun n ((3:ℝ) + t * Complex.I) *\n          (-logDeriv riemannZeta ((3:ℝ) + t * Complex.I))‖ = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n  have hint : ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  rwa [abs_of_nonneg (by linarith), mul_div] at hint\n```\nDetails:\n- Jlag's def: Jlag n s = kFun n s * (-(deriv ζ s/ζ s)) — and logDeriv ζ s = deriv ζ s/ζ s (logDeriv is defeq to that: logDeriv f := deriv f / f — the Pi.div_apply — in the C2 proof: `rw [logDeriv, Pi.div_apply, h2]` — so logDeriv riemannZeta s = deriv riemannZeta s/riemannZeta s — defeq). Jlag n s = kFun n s * (-logDeriv riemannZeta s) — defeq ✓ the `show` works by rfl.\n- Set.uIoc_of_le hTU : Ι T U = Ioc T U ✓ (uIoc = Ioc when T ≤ U: Set.uIoc_of_le (h : a ≤ b) : Ι a b = Ioc a b ✓).\n- intervalIntegral.norm_integral_le_of_norm_le_const (h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C) ✓ applied with hbound after the uIoc rewrite.\n- hint's form: ‖∫‖ ≤ C·|U−T| with C = (e^{5/2}+1)·(1/2): abs_of_nonneg: |U−T| = U−T (U−T ≥ 0 ✓ linarith); then the goal: ‖VIntegral‖ ≤ (U−T)·(e^{5/2}+1)/2: after rw [norm_smul, Complex.norm_I, one_mul] the goal is ‖∫‖ ≤ (U−T)·(e^{5/2}+1)/2 — hint gives ‖∫‖ ≤ (e^{5/2}+1)·(1/2)·(U−T) — same up to mul-order: (U−T)·X/2 vs X·(1/2)·(U−T): X·(1/2)·(U−T) = (U−T)·X/2: `mul_div` : a * (b / c) = (a * b) / c: hint after abs: ‖∫‖ ≤ ((e^{5/2}+1)·(1/2))·(U−T): hmm — I want ‖∫‖ ≤ (U−T)·(e^{5/2}+1)/2. (e^{5/2}+1)·(1/2)·(U−T) vs (U−T)·(e^{5/2}+1)/2 — equal by ring (comm). So finish: `rwa [abs_of_nonneg (by linarith : 0 ≤ U − T)] at hint; ... linarith [hint]` or convert hint via ring_nf. Cleanest: after getting hint, do `have : ‖VIntegral (Jlag n) 3 T U‖ = ‖∫ t in T..U, Jlag n ((3:ℝ) + t * Complex.I)‖ := by unfold VIntegral; rw [norm_smul, Complex.norm_I, one_mul]` — hmm I already rewrote the goal at the top. Let me restructure:\n\n```\ntheorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}\n    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  have hnorm : ‖VIntegral (Jlag n) 3 T U‖ =\n      ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : ... (as above)\n  have hint : ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc ‖∫ t in T..U, Jlag n ((3:ℝ) + t * Complex.I)‖\n      ≤ ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n```\n✓.\n\nAlso — the Ι vs the ∫ t in T..U: the norm_integral_le_of_norm_le_const's premise is ∀ x ∈ Ι a b — `apply intervalIntegral.norm_integral_le_of_norm_le_const; intro t ht` ✓ then ht : t ∈ Ι T U → rw [Set.uIoc_of_le hTU] at ht → t ∈ Ioc T U ✓ hbound t ht ✓.\n\nOne more check — `Set.uIoc_of_le` name: `Set.uIoc_of_le (h : a ≤ b) : Ι a b = Ioc a b` ✓ (Mathlib: Set.uIoc_of_le : a ≤ b → Ι a b = Set.Ioc a b ✓).\n\nAnd hbound's ht : t ∈ Ioc T U: ht.1 : T < t ✓ ht2 by nlinarith [hTn, hT0]: t² ≥ T² (t > T > 0) ✓ n ≤ T² ≤ t² ✓.\n\nhre : 3 ≤ ((3:ℝ) + t*I).re: `by simp` — ((3:ℝ) + t*I).re = 3: simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re]... the simp should reduce (the dogZ_re pattern was `simp [dogZ]` ✓ here it's the raw expression — simp with the re/im lemmas should give 3 ≤ 3 ✓).\n\nWrite the whole DL-2 block into LiDogLeg.lean (before `end NguyenRH1`). Also `Complex.norm_I` — name check: `Complex.norm_I : ‖Complex.I‖ = 1` ✓ exists.","signature":""},{"type":"text","text":"All API confirmed. Writing the DL-2 block (kernel lemma + dirichletC3 ≤ 1/2 + the V_left assembly) into LiDogLeg.lean."},{"type":"tool_use","id":"Edit_204","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 3. The left-lift bound (DL-2, D-074 §3.3 V_left) -/\n\n/-- **Kernel on the lift**: ‖kFun n (3+it)‖ ≤ e^{5/2}+1 for n ≤ t²\n(D-074 §6: |(3+it)/(2+it)|² = (9+t²)/(4+t²) = 1 + 5/(4+t²), whose n-th\npower is ≤ e^{5n/(2(4+t²))} ≤ e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : ℕ} {t : ℝ}\n    (hT : (n : ℝ) ≤ t ^ 2) :\n    ‖kFun n ((3 : ℝ) + t * Complex.I)‖ ≤ Real.exp (5 / 2) + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  · subst hn\n    simp only [kFun, pow_zero, sub_self, norm_zero]\n    positivity\n  · have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n    have ht2 : (0 : ℝ) < 4 + t ^ 2 := by positivity\n    have hn4t2 : (n : ℝ) ≤ 4 + t ^ 2 := by linarith [hT]\n    have hQpos : (0 : ℝ) ≤ (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n    have hQle : (9 + t ^ 2) / (4 + t ^ 2) ≤ Real.exp (5 / (n : ℝ)) := by\n      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n        field_simp [ht2.ne']\n        ring\n      rw [h1]\n      have h2 : 5 / (4 + t ^ 2) ≤ 5 / (n : ℝ) :=\n        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n      have h3 := Real.add_one_le_exp (5 / (n : ℝ))\n      linarith\n    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ Real.exp 5 := by\n      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ (Real.exp (5 / (n : ℝ))) ^ n :=\n            pow_le_pow_left₀ hQpos hQle n\n        _ = Real.exp 5 := by\n            rw [← Real.exp_nat_mul]\n            congr 1\n            have hn0 : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'\n            field_simp [hn0]\n    have hns3 : Complex.normSq ((3 : ℝ) + t * Complex.I) = 9 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hns2 : Complex.normSq ((2 : ℝ) + t * Complex.I) = 4 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hnorm : ‖((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)‖ =\n        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n      rw [norm_div, ← Real.sqrt_div hQpos, ← Complex.normSq_eq_norm_sq,\n        ← Complex.normSq_eq_norm_sq, hns3, hns2]\n    have hs1 : ((3 : ℝ) + t * Complex.I) - 1 = (2 : ℝ) + t * Complex.I := by ring\n    unfold kFun\n    rw [hs1]\n    calc ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n - 1‖\n        ≤ ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ :=\n          norm_sub_le _ _\n      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n          rw [norm_pow, hnorm, norm_one]\n      _ ≤ Real.exp (5 / 2) + 1 := by\n          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n ≤ Real.exp (5 / 2) := by\n            rw [Real.sqrt_pow]\n            calc Real.sqrt (((9 + t ^ 2) / (4 + t ^ 2)) ^ n)\n                ≤ Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt hQn\n              _ = Real.exp (5 / 2) := by rw [Real.sqrt_exp]\n          linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : ℝ :=\n  ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖\n\n/-- Termwise 3-vs-2 comparison for the Λ L-series: Λ(n)/n³ ≤ (1/2)·Λ(n)/n². -/\nlemma norm_term_vonMangoldt_three_le_half (n : ℕ) :\n    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ ≤\n      (1 / 2) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ := by\n  have h3re : ((3 : ℂ).re) = 3 := rfl\n  have h2re : ((2 : ℂ).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h3re, h2re]\n  split\n  · norm_num\n  · next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    · simp [ArithmeticFunction.vonMangoldt_one]\n    · have hn2 : 2 ≤ n := by omega\n      have hΛ : ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ =\n          ArithmeticFunction.vonMangoldt n := by\n        rw [Complex.norm_eq_abs, ← Real.norm_eq_abs,\n          Real.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg]\n      rw [hΛ]\n      have e : ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ 3 =\n          (1 / (n : ℝ)) * (ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ 2) := by\n        field_simp [show (n : ℝ) ≠ 0 by positivity]\n        ring\n      rw [e]\n      apply mul_le_mul_of_nonneg_right _ (by positivity)\n      rw [div_le_div_iff_of_pos_left (by norm_num : (0 : ℝ) < 1)\n        (by norm_num : (0 : ℝ) < 2) (by positivity : (0 : ℝ) < (n : ℝ))]\n      exact_mod_cast hn2\n\n/-- dirichletC3 ≤ 1/2 (the termwise comparison + dirichletC2 ≤ 1) —\nthe certified C_zeta3 = 0.5 of D-074 §4. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 ≤ 1 / 2 := by\n  have hsum3 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  calc dirichletC3\n      = ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ := rfl\n    _ ≤ ∑' n : ℕ, (1 / 2) *\n          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ :=\n        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n          (hsum2.mul_left (1 / 2))\n    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ ≤ 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- ‖ζ′/ζ s‖ ≤ dirichletC3 for re s ≥ 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ dirichletC3 := by\n  have hs1 : (1 : ℝ) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum3 : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : ℕ =>\n      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖\n      ≤ dirichletC3 := by\n    show ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ ≤ _\n    calc ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖\n        ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ :=\n          norm_tsum_le_tsum_norm hsumS\n      _ ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum3\n      _ = dirichletC3 := rfl\n  calc ‖logDeriv riemannZeta s‖\n      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖ := by\n        rw [← h1, norm_neg]\n    _ ≤ dirichletC3 := hle\n\n/-- ‖ζ′/ζ s‖ ≤ 1/2 for re s ≥ 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : ℂ} (hs : 3 ≤ s.re) :\n    ‖logDeriv riemannZeta s‖ ≤ 1 / 2 :=\n  (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 §3.3 V_left): for 0 < T ≤ U and\nn ≤ T², ‖VIntegral (Jlag n) 3 T U‖ ≤ (U − T)·(e^{5/2}+1)/2. The kernel\n≤ e^{5/2}+1 (the 1+5/(4+t²) computation), the zeta factor ≤ 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}\n    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  have hnorm : ‖VIntegral (Jlag n) 3 T U‖ =\n      ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : ∀ t ∈ Set.Ioc T U,\n      ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤ (Real.exp (5 / 2) + 1) * (1 / 2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]\n    have hre : (3 : ℝ) ≤ ((3 : ℝ) + t * Complex.I).re := by simp\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3 : ℝ) + t * Complex.I) hre\n    have hnorm3 : ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ =\n        ‖kFun n ((3 : ℝ) + t * Complex.I)‖ *\n          ‖logDeriv riemannZeta ((3 : ℝ) + t * Complex.I)‖ := by\n      show ‖kFun n ((3 : ℝ) + t * Complex.I) *\n          (-logDeriv riemannZeta ((3 : ℝ) + t * Complex.I))‖ = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n  have hint : ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖\n      ≤ ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\nend NguyenRH1\n\nend"},"extra_content":null}]