LiDogLeg.lean

Declarations

Source

/-
NguyenRH1/LiDogLeg.lean — ii′-6-DL-1 (D-074, session 040): the zero-free
dog-leg deformation of the Lagarias horizontal right tail.

THE CONTENT (D-074 §3.1–3.2): on the dog-leg rectangle [3, X_R]×[T, U]
(T > 0), the Lagarias integrand Jlag n s = (s/(s−1))ⁿ−1 · (−ζ′/ζ(s)) is
holomorphic UNCONDITIONALLY (s ≠ 1 since im > 0; ζ s ≠ 0 for re s ≥ 3 > 1
by Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`
— NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem
(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation
identity
  H(3→X_R, T) = H(3→X_R, U) − V(X_R, T→U) + V(3, T→U)
(the upper right tail = the high horizontal − the right drop + the left
lift), plus the Jlag conjugation identity for the lower-side transfer.

This is the repair of Finding F-D (D-072): the broken low-path envelope
is ABANDONED (not bounded) — the magnitude bound comes later from the
three dog-leg pieces, all in the unconditionally zero-free region.
-/
import Mathlib
import NguyenRH1.LiSides
import NguyenRH1.LiTightR
import NguyenRH1.LiBasePoints

open Zeta23 Complex Filter Topology
open scoped Nat

noncomputable section

namespace NguyenRH1

/-! ## 1. Dog-leg analyticity (D-074 §3.1; no perimeter) -/

/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/
def dogZ (T : ℝ) : ℂ := ((3 : ℝ) : ℂ) + (T : ℝ) * Complex.I
def dogW (XR U : ℝ) : ℂ := ((XR : ℝ) : ℂ) + (U : ℝ) * Complex.I

lemma dogZ_re (T : ℝ) : (dogZ T).re = 3 := by simp [dogZ]
lemma dogZ_im (T : ℝ) : (dogZ T).im = T := by simp [dogZ]
lemma dogW_re (XR U : ℝ) : (dogW XR U).re = XR := by simp [dogW]
lemma dogW_im (XR U : ℝ) : (dogW XR U).im = U := by simp [dogW]

/-- Jlag is differentiable at every point with 3 ≤ re, 0 < im:
ζ is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,
UNCONDITIONAL — the Euler-product region) and s ≠ 1 (im ≠ 0).
NO perimeter hypothesis. -/
theorem Jlag_differentiableAt_dogleg {n : ℕ} {s : ℂ}
    (hre : 3 ≤ s.re) (him : 0 < s.im) :
    DifferentiableAt ℂ (Jlag n) s := by
  apply Jlag_differentiableAt
  · rintro rfl
    simp at him
  · exact riemannZeta_ne_zero_of_one_lt_re (by linarith)

/-- Jlag is holomorphic on the whole dog-leg rectangle
[3, X_R]×[T, U] (T > 0). -/
theorem holomorphicOn_Jlag_dogleg {n : ℕ} {T U XR : ℝ}
    (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :
    HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by
  intro s hs
  rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs
  rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs
  exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt

/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is
unconditionally zero-free — the residue sum is EMPTY, no perimeter). -/
theorem rectangleIntegral_Jlag_dogleg_eq_zero {n : ℕ} {T U XR : ℝ}
    (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :
    RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=
  (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl

/-- The (2πi)⁻¹-normalized form (API symmetry with rectInt'_Jlag). -/
theorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : ℕ} {T U XR : ℝ}
    (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :
    RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by
  rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,
    smul_zero]

/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 §3.2 (★), the
capstone for ii′-6-c): the low right-horizontal equals the high
horizontal minus the right drop plus the left lift. Orientations: all
H-integrals left-to-right, all V-integrals upward (the main contour's
top side is their reversal, handled at the fold site). -/
theorem upper_right_horizontal_eq_dogleg {n : ℕ} {T U XR : ℝ}
    (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :
    HIntegral (Jlag n) 3 XR T =
      HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +
        VIntegral (Jlag n) 3 T U := by
  have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR
  unfold RectangleIntegral at h0
  rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0
  linear_combination h0

/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/

/-- kFun is conjugation-symmetric (real-coefficient rational function). -/
theorem kFun_conj (n : ℕ) (s : ℂ) :
    kFun n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (kFun n s) := by
  unfold kFun
  simp [map_sub, map_pow, map_one]

/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +
`iteratedDeriv_riemannZeta_conj`): Jlag n (s̄) = conj (Jlag n s).
Needed for the lower-horizontal transfer (DL-5). -/
theorem Jlag_conj (n : ℕ) {s : ℂ} (hs : s ≠ 1) :
    Jlag n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Jlag n s) := by
  have h1 : deriv riemannZeta ((starRingEnd ℂ) s) =
      (starRingEnd ℂ) (deriv riemannZeta s) := by
    have h := iteratedDeriv_riemannZeta_conj 1 hs
    rwa [iteratedDeriv_one] at h
  unfold Jlag
  rw [kFun_conj, _root_.riemannZeta_conj, h1]
  simp only [map_mul, map_neg, map_div₀]

/-! ## 3. The left-lift bound (DL-2, D-074 §3.3 V_left) -/

/-- **Kernel on the lift**: ‖kFun n (3+it)‖ ≤ e^{5/2}+1 for n ≤ t²
(D-074 §6: |(3+it)/(2+it)|² = (9+t²)/(4+t²) = 1 + 5/(4+t²), whose n-th
power is ≤ e^{5n/(2(4+t²))} ≤ e^{5/2}). -/
theorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : ℕ} {t : ℝ}
    (hT : (n : ℝ) ≤ t ^ 2) :
    ‖kFun n ((3 : ℝ) + t * Complex.I)‖ ≤ Real.exp (5 / 2) + 1 := by
  rcases Nat.eq_zero_or_pos n with hn | hn
  · subst hn
    simp only [kFun, pow_zero, sub_self, norm_zero]
    positivity
  · have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have ht2 : (0 : ℝ) < 4 + t ^ 2 := by positivity
    have hn4t2 : (n : ℝ) ≤ 4 + t ^ 2 := by linarith [hT]
    have hQpos : (0 : ℝ) ≤ (9 + t ^ 2) / (4 + t ^ 2) := by positivity
    have hQle : (9 + t ^ 2) / (4 + t ^ 2) ≤ Real.exp (5 / (n : ℝ)) := by
      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by
        field_simp [ht2.ne']
        ring
      rw [h1]
      have h2 : 5 / (4 + t ^ 2) ≤ 5 / (n : ℝ) :=
        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2
      have h3 := Real.add_one_le_exp (5 / (n : ℝ))
      linarith
    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ Real.exp 5 := by
      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n ≤ (Real.exp (5 / (n : ℝ))) ^ n :=
            pow_le_pow_left₀ hQpos hQle n
        _ = Real.exp 5 := by
            rw [← Real.exp_nat_mul]
            congr 1
            have hn0 : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne'
            field_simp [hn0]
    have hns3 : Complex.normSq ((3 : ℝ) + t * Complex.I) = 9 + t ^ 2 := by
      simp [Complex.normSq_apply]
      ring
    have hns2 : Complex.normSq ((2 : ℝ) + t * Complex.I) = 4 + t ^ 2 := by
      simp [Complex.normSq_apply]
      ring
    have hnormA : ‖((3 : ℝ) + t * Complex.I)‖ = Real.sqrt (9 + t ^ 2) := by
      have h1 : ‖((3 : ℝ) + t * Complex.I)‖ =
          Real.sqrt (Complex.normSq ((3 : ℝ) + t * Complex.I)) := by
        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]
      rw [h1, hns3]
    have hnormB : ‖((2 : ℝ) + t * Complex.I)‖ = Real.sqrt (4 + t ^ 2) := by
      have h1 : ‖((2 : ℝ) + t * Complex.I)‖ =
          Real.sqrt (Complex.normSq ((2 : ℝ) + t * Complex.I)) := by
        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]
      rw [h1, hns2]
    have hnorm : ‖((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)‖ =
        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by
      rw [norm_div, hnormA, hnormB,
        ← Real.sqrt_div (by positivity : (0 : ℝ) ≤ 9 + t ^ 2)]
    have hs1 : ((3 : ℝ) + t * Complex.I) - 1 = (2 : ℝ) + t * Complex.I := by
      push_cast
      ring
    unfold kFun
    rw [hs1]
    calc ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n - 1‖
        ≤ ‖(((3 : ℝ) + t * Complex.I) / ((2 : ℝ) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ :=
          norm_sub_le _ _
      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by
          rw [norm_pow, hnorm, norm_one]
      _ ≤ Real.exp (5 / 2) + 1 := by
          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n ≤ Real.exp (5 / 2) := by
            have hx0 : (0 : ℝ) ≤ Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=
              Real.sqrt_nonneg _
            have hx : (0 : ℝ) ≤ (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=
              pow_nonneg hx0 n
            have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 ≤ Real.exp 5 := by
              have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =
                  ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by
                rw [← pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]
              rw [e]
              exact hQn
            have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =
                Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by
              rw [Real.sqrt_sq hx]
            rw [h8]
            calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)
                ≤ Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5
              _ = Real.exp (5 / 2) := (Real.exp_half 5).symm
          linarith [h4]

/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/
def dirichletC3 : ℝ :=
  ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖

/-- Termwise 3-vs-2 comparison for the Λ L-series: Λ(n)/n³ ≤ (1/2)·Λ(n)/n². -/
lemma norm_term_vonMangoldt_three_le_half (n : ℕ) :
    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ ≤
      (1 / 2) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ := by
  have h3re : ((3 : ℂ).re) = 3 := rfl
  have h2re : ((2 : ℂ).re) = 2 := rfl
  simp only [LSeries.norm_term_eq, h3re, h2re]
  split
  · norm_num
  · next hn =>
    rcases eq_or_ne n 1 with rfl | hn1
    · simp [ArithmeticFunction.vonMangoldt_apply_one]
    · have hn2 : 2 ≤ n := by omega
      have hΛ : ‖(ArithmeticFunction.vonMangoldt n : ℂ)‖ =
          ArithmeticFunction.vonMangoldt n :=
        Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg
      rw [hΛ]
      have e : ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (3 : ℝ) =
          (1 / (n : ℝ)) * (ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (2 : ℝ)) := by
        rw [show (3 : ℝ) = 2 + 1 by norm_num,
          Real.rpow_add (by positivity : (0 : ℝ) < (n : ℝ)), Real.rpow_one]
        field_simp [show (n : ℝ) ≠ 0 by positivity]
      have h12 : (1 : ℝ) / (n : ℝ) ≤ 1 / 2 :=
        one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 2)
          (by exact_mod_cast hn2 : (2 : ℝ) ≤ (n : ℝ))
      have hpos : (0 : ℝ) ≤ ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (2 : ℝ) :=
        div_nonneg ArithmeticFunction.vonMangoldt_nonneg
          (Real.rpow_nonneg (by positivity : (0 : ℝ) ≤ (n : ℝ)) _)
      calc ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (3 : ℝ)
          = (1 / (n : ℝ)) * (ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (2 : ℝ)) := e
        _ ≤ (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : ℝ) ^ (2 : ℝ)) :=
            mul_le_mul_of_nonneg_right h12 hpos

/-- dirichletC3 ≤ 1/2 (the termwise comparison + dirichletC2 ≤ 1) —
the certified C_zeta3 = 0.5 of D-074 §4. (A tighter 0.17 build is
possible via a 6-prime partial sum + antitone-integral tail; the fold
is indifferent to the constant, so the cheap certified 0.5 is charged.) -/
lemma dirichletC3_le_half : dirichletC3 ≤ 1 / 2 := by
  have hsum3 : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)
  have hsum2 : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)
  calc dirichletC3
      = ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ := rfl
    _ ≤ ∑' n : ℕ, (1 / 2) *
          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ :=
        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3
          (hsum2.mul_left (1 / 2))
    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]
    _ ≤ 1 / 2 := by linarith [dirichletC2_le_one]

/-- ‖ζ′/ζ s‖ ≤ dirichletC3 for re s ≥ 3 (the s = 3 clone of the
Dirichlet-series majorant). -/
lemma norm_logDeriv_zeta_le_dirichletC3 {s : ℂ} (hs : 3 ≤ s.re) :
    ‖logDeriv riemannZeta s‖ ≤ dirichletC3 := by
  have hs1 : (1 : ℝ) < s.re := by linarith
  have h1 : -logDeriv riemannZeta s
      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s := by
    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1
    rw [logDeriv, Pi.div_apply, h2]
    ring
  have hsum3 : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)
  have hsumS : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1
  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖
      ≤ dirichletC3 := by
    show ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ ≤ _
    calc ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖
        ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s n‖ :=
          norm_tsum_le_tsum_norm hsumS
      _ ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (3 : ℂ) n‖ :=
          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by
            simp
            exact hs) n) hsumS hsum3
      _ = dirichletC3 := rfl
  calc ‖logDeriv riemannZeta s‖
      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) s‖ := by
        rw [← h1, norm_neg]
    _ ≤ dirichletC3 := hle

/-- ‖ζ′/ζ s‖ ≤ 1/2 for re s ≥ 3 (the charged C_zeta3 = 0.5). -/
lemma norm_logDeriv_zeta_le_half {s : ℂ} (hs : 3 ≤ s.re) :
    ‖logDeriv riemannZeta s‖ ≤ 1 / 2 :=
  (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half

/-- **The left-lift bound** (D-074 §3.3 V_left): for 0 < T ≤ U and
n ≤ T², ‖VIntegral (Jlag n) 3 T U‖ ≤ (U − T)·(e^{5/2}+1)/2. The kernel
≤ e^{5/2}+1 (the 1+5/(4+t²) computation), the zeta factor ≤ 1/2
(certified, no perimeter). -/
theorem vIntegral_Jlag_three_norm_le {n : ℕ} {T U : ℝ}
    (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :
    ‖VIntegral (Jlag n) 3 T U‖ ≤ (U - T) * (Real.exp (5 / 2) + 1) / 2 := by
  have hnorm : ‖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]
  rw [hnorm]
  have hbound : ∀ t ∈ Set.Ioc T U,
      ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤ (Real.exp (5 / 2) + 1) * (1 / 2) := by
    intro t ht
    have htT : T < t := ht.1
    have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]
    have hre : (3 : ℝ) ≤ ((3 : ℝ) + t * Complex.I).re := by simp
    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2
    have h2 := norm_logDeriv_zeta_le_half (s := (3 : ℝ) + t * Complex.I) hre
    have hnorm3 : ‖Jlag n ((3 : ℝ) + t * Complex.I)‖ =
        ‖kFun n ((3 : ℝ) + t * Complex.I)‖ *
          ‖logDeriv riemannZeta ((3 : ℝ) + t * Complex.I)‖ := by
      show ‖kFun n ((3 : ℝ) + t * Complex.I) *
          (-logDeriv riemannZeta ((3 : ℝ) + t * Complex.I))‖ = _
      rw [norm_mul, norm_neg]
    rw [hnorm3]
    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)
  have hint : ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖ ≤
      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by
    apply intervalIntegral.norm_integral_le_of_norm_le_const
    intro t ht
    rw [Set.uIoc_of_le hTU] at ht
    exact hbound t ht
  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)
  rw [habs] at hint
  calc ‖∫ t in T..U, Jlag n ((3 : ℝ) + t * Complex.I)‖
      ≤ ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint
    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring

/-! ## 4. The high-horizontal stepping (DL-3, D-074 §7 + D-073 §4) -/

/-- Termwise σ-vs-2 comparison for the Λ L-series (the (6.10) halving):
Λ(m)/m^σ ≤ 2^{−(σ−2)}·Λ(m)/m² for σ ≥ 2. -/
lemma norm_term_vonMangoldt_le_two_pow {σ t : ℝ} (hσ : 2 ≤ σ) (m : ℕ) :
    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        ((σ : ℝ) + t * Complex.I) m‖ ≤
      (2 : ℝ) ^ (-(σ - 2)) * ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ := by
  have hσre : ((σ : ℝ) + t * Complex.I).re = σ := by simp
  have h2re : ((2 : ℂ).re) = 2 := rfl
  simp only [LSeries.norm_term_eq, hσre, h2re]
  split
  · norm_num
  · next hm =>
    have hΛ : ‖(ArithmeticFunction.vonMangoldt m : ℂ)‖ =
        ArithmeticFunction.vonMangoldt m :=
      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg
    rw [hΛ]
    rcases eq_or_ne m 1 with rfl | hm1
    · simp [ArithmeticFunction.vonMangoldt_apply_one]
    · have hm2 : 2 ≤ m := by omega
      have e : ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ σ =
          (1 / (m : ℝ) ^ (σ - 2)) * (ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ)) := by
        rw [show (σ : ℝ) = (σ - 2) + 2 by ring,
          Real.rpow_add (by positivity : (0 : ℝ) < (m : ℝ))]
        field_simp [show (m : ℝ) ≠ 0 by positivity]
        ring_nf
      rw [e]
      have hle : (1 : ℝ) / (m : ℝ) ^ (σ - 2) ≤ (2 : ℝ) ^ (-(σ - 2)) := by
        rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 2), ← one_div]
        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2) _)
        exact Real.rpow_le_rpow (by norm_num : (0 : ℝ) ≤ 2)
          (by exact_mod_cast hm2 : (2 : ℝ) ≤ (m : ℝ)) (by linarith : (0 : ℝ) ≤ σ - 2)
      have hpos : (0 : ℝ) ≤ ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ) :=
        div_nonneg ArithmeticFunction.vonMangoldt_nonneg
          (Real.rpow_nonneg (by positivity : (0 : ℝ) ≤ (m : ℝ)) _)
      exact mul_le_mul_of_nonneg_right hle hpos

/-- ‖ζ′/ζ(σ+it)‖ ≤ 2^{−(σ−2)}·dirichletC2 for σ ≥ 2 (the (6.10)
halving in LSeries form; dirichletC2 ≤ 1 makes the tail free). -/
lemma norm_logDeriv_zeta_le_two_pow {σ t : ℝ} (hσ : 2 ≤ σ) :
    ‖logDeriv riemannZeta ((σ : ℝ) + t * Complex.I)‖ ≤
      (2 : ℝ) ^ (-(σ - 2)) * dirichletC2 := by
  have hs1 : (1 : ℝ) < ((σ : ℝ) + t * Complex.I).re := by simp; linarith
  have h1 : -logDeriv riemannZeta ((σ : ℝ) + t * Complex.I)
      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) ((σ : ℝ) + t * Complex.I) := by
    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1
    rw [logDeriv, Pi.div_apply, h2]
    ring
  have hsum2 : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)
  have hsumS : Summable (fun n : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        ((σ : ℝ) + t * Complex.I) n‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1
  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
      ((σ : ℝ) + t * Complex.I)‖ ≤ (2 : ℝ) ^ (-(σ - 2)) * dirichletC2 := by
    show ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
      ((σ : ℝ) + t * Complex.I) n‖ ≤ _
    calc ‖∑' n : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          ((σ : ℝ) + t * Complex.I) n‖
        ≤ ∑' n : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            ((σ : ℝ) + t * Complex.I) n‖ :=
          norm_tsum_le_tsum_norm hsumS
      _ ≤ ∑' n : ℕ, (2 : ℝ) ^ (-(σ - 2)) *
            ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) n‖ :=
          Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow hσ n) hsumS
            (hsum2.mul_left _)
      _ = (2 : ℝ) ^ (-(σ - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]
  calc ‖logDeriv riemannZeta ((σ : ℝ) + t * Complex.I)‖
      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          ((σ : ℝ) + t * Complex.I)‖ := by
        rw [← h1, norm_neg]
    _ ≤ (2 : ℝ) ^ (-(σ - 2)) * dirichletC2 := hle

/-- **Kernel envelope** (D-074 §7, the single-exponential form that
replaces the unit-step geometric series): ‖(1+1/((σ−1)+iU))ⁿ‖ ≤
e^{(4/9)σ} for σ ≥ 3 and n ≤ (4/9)U². From the (6.11) core
‖1+1/s‖ ≤ 1+(re s+1)/normSq s ≤ 1+σ/U². -/
theorem one_add_div_pow_norm_le_exp_four_ninths {n : ℕ} {σ U : ℝ}
    (hσ : 3 ≤ σ) (hU : 0 < U) (hnU : (n : ℝ) ≤ (4 / 9) * U ^ 2) :
    ‖(1 + 1/(((σ : ℝ) - 1) + U * Complex.I))‖ ^ n ≤ Real.exp ((4 / 9) * σ) := by
  have hs0 : (((σ : ℝ) - 1) + U * Complex.I) ≠ 0 := by
    intro h
    have him : (((σ : ℝ) - 1) + U * Complex.I).im = 0 := by rw [h]; simp
    simp at him
    linarith
  have hle := norm_one_add_one_div_le hs0
  have hre : (((σ : ℝ) - 1) + U * Complex.I).re + 1 = σ := by
    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,
      Complex.sub_re, Complex.one_re]
  have hns : Complex.normSq (((σ : ℝ) - 1) + U * Complex.I) = (σ - 1) ^ 2 + U ^ 2 := by
    simp [Complex.normSq_apply]
    ring
  have hstep : ((((σ : ℝ) - 1) + U * Complex.I).re + 1) /
      Complex.normSq (((σ : ℝ) - 1) + U * Complex.I) ≤ σ / U ^ 2 := by
    rw [hre, hns]
    have hU2 : (0 : ℝ) < U ^ 2 := by positivity
    have h1 : (0 : ℝ) ≤ (σ - 1) ^ 2 := sq_nonneg _
    exact (div_le_div_iff_of_pos_left (by linarith : (0 : ℝ) < σ)
      (by positivity) hU2).mpr (by linarith [h1])
  have hstep1 : 1 + ((((σ : ℝ) - 1) + U * Complex.I).re + 1) /
      Complex.normSq (((σ : ℝ) - 1) + U * Complex.I) ≤ 1 + σ / U ^ 2 := by
    linarith [hstep]
  have hpow1 : ‖(1 + 1/(((σ : ℝ) - 1) + U * Complex.I))‖ ^ n ≤ (1 + σ / U ^ 2) ^ n :=
    pow_le_pow_left₀ (norm_nonneg _) (hle.trans hstep1) n
  have hpow2 : (1 + σ / U ^ 2) ^ n ≤ Real.exp ((n : ℝ) * (σ / U ^ 2)) := by
    calc (1 + σ / U ^ 2) ^ n ≤ (Real.exp (σ / U ^ 2)) ^ n := by
          have h := Real.add_one_le_exp (σ / U ^ 2)
          exact pow_le_pow_left₀ (by positivity) (by linarith) n
      _ = Real.exp ((n : ℝ) * (σ / U ^ 2)) := (Real.exp_nat_mul (σ / U ^ 2) n).symm
  have hexp : (n : ℝ) * (σ / U ^ 2) ≤ (4 / 9) * σ := by
    have hU2 : (0 : ℝ) < U ^ 2 := by positivity
    have hσ0 : (0 : ℝ) < σ := by linarith
    have h1 : (n : ℝ) / U ^ 2 ≤ 4 / 9 := by
      have h2 := div_le_div_of_nonneg_right hnU hU2.le
      rwa [mul_div_cancel_right₀ _ hU2.ne'] at h2
    rw [show (n : ℝ) * (σ / U ^ 2) = ((n : ℝ) / U ^ 2) * σ by ring]
    exact mul_le_mul_of_nonneg_right h1 hσ0.le
  calc ‖(1 + 1/(((σ : ℝ) - 1) + U * Complex.I))‖ ^ n
      ≤ Real.exp ((n : ℝ) * (σ / U ^ 2)) := hpow1.trans hpow2
    _ ≤ Real.exp ((4 / 9) * σ) := Real.exp_le_exp.mpr hexp

/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/

/-- **The product envelope** (D-074 §7): for σ ≥ 3, 0 < t, n ≤ (4/9)t²,
‖Jlag n (σ+it)‖ ≤ (4·e^{−cσ} + 4·2^{−σ})·dirichletC2, c = log 2 − 4/9.
The kernel envelope (e^{(4/9)σ}) times the zeta halving (2^{−(σ−2)})
collapses to the single exponential 4·e^{−cσ}: no geometric series. -/
theorem Jlag_dogleg_norm_le_envelope {n : ℕ} {σ t : ℝ}
    (hσ : 3 ≤ σ) (ht : 0 < t) (hnU : (n : ℝ) ≤ (4 / 9) * t ^ 2) :
    ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ ≤
      dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) := by
  have hw1 : ((σ : ℝ) + t * Complex.I) - 1 = ((σ : ℝ) - 1) + t * Complex.I := by
    ring
  have hs1ne : (((σ : ℝ) - 1) + t * Complex.I) ≠ 0 := by
    intro h
    have him : (((σ : ℝ) - 1) + t * Complex.I).im = 0 := by rw [h]; simp
    simp at him
    linarith
  have hwid : ((σ : ℝ) + t * Complex.I) / (((σ : ℝ) + t * Complex.I) - 1) =
      1 + 1 / (((σ : ℝ) - 1) + t * Complex.I) := by
    rw [hw1]
    field_simp [hs1ne]
    ring
  have hker := one_add_div_pow_norm_le_exp_four_ninths hσ ht hnU
  have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : ℝ) ≤ σ by linarith) (t := t)
  have hk : ‖kFun n ((σ : ℝ) + t * Complex.I)‖ ≤ Real.exp ((4 / 9) * σ) + 1 := by
    unfold kFun
    rw [hwid]
    calc ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I)) ^ n - 1‖
        ≤ ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _
      _ = ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I))‖ ^ n + 1 := by rw [norm_pow, norm_one]
      _ ≤ Real.exp ((4 / 9) * σ) + 1 := by linarith [hker]
  have hprod : ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ ≤
      (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2)) * dirichletC2) := by
    have hn3 : ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ =
        ‖kFun n ((σ : ℝ) + t * Complex.I)‖ *
          ‖logDeriv riemannZeta ((σ : ℝ) + t * Complex.I)‖ := by
      show ‖kFun n ((σ : ℝ) + t * Complex.I) *
          (-logDeriv riemannZeta ((σ : ℝ) + t * Complex.I))‖ = _
      rw [norm_mul, norm_neg]
    rw [hn3]
    exact mul_le_mul hk hzeta (norm_nonneg _)
      (add_nonneg (Real.exp_nonneg _) (by norm_num))
  have h2b : (2 : ℝ) ^ (-σ) = Real.exp (-(Real.log 2) * σ) := by
    rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]
    congr 1
    ring
  have h22 : (2 : ℝ) ^ (2 : ℝ) = 4 := by
    rw [Real.rpow_two]
    norm_num
  have h2a : (2 : ℝ) ^ (-(σ - 2)) = 4 * (2 : ℝ) ^ (-σ) := by
    rw [show (-(σ - 2)) = -σ + 2 by ring, Real.rpow_add (by norm_num : (0 : ℝ) < 2), h2b, h22]
    ring
  have hexp_alg : Real.exp ((4 / 9) * σ) * Real.exp (-(Real.log 2) * σ) =
      Real.exp (-(Real.log 2 - 4 / 9) * σ) := by
    rw [← Real.exp_add]
    congr 1
    ring
  have halg : (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2))) =
      4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ) := by
    rw [h2a, h2b]
    calc (Real.exp ((4 / 9) * σ) + 1) * (4 * Real.exp (-(Real.log 2) * σ))
        = 4 * (Real.exp ((4 / 9) * σ) * Real.exp (-(Real.log 2) * σ)) +
          4 * Real.exp (-(Real.log 2) * σ) := by ring
      _ = 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * Real.exp (-(Real.log 2) * σ) := by
        rw [hexp_alg]
  calc ‖Jlag n ((σ : ℝ) + t * Complex.I)‖
      ≤ (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2)) * dirichletC2) := hprod
    _ = dirichletC2 * ((Real.exp ((4 / 9) * σ) + 1) * (2 : ℝ) ^ (-(σ - 2))) := by ring
    _ = dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) := by
        rw [halg]

/-- The FTC-bound ∫₃^XR e^{−cσ}dσ ≤ e^{−3c}/c for c > 0. -/
lemma integral_exp_neg_le {c XR : ℝ} (hc : 0 < c) (_hXR : 3 ≤ XR) :
    ∫ σ in (3 : ℝ)..XR, Real.exp (-c * σ) ≤ Real.exp (-3 * c) / c := by
  have hF : ∀ x ∈ Set.uIcc (3 : ℝ) XR,
      HasDerivAt (fun σ => -Real.exp (-c * σ) / c) (Real.exp (-c * x)) x := by
    intro x hx
    have h2 : HasDerivAt (fun σ => Real.exp (-c * σ)) (Real.exp (-c * x) * (-c)) x := by
      have h := ((hasDerivAt_id' x).const_mul (-c)).exp
      rwa [mul_one] at h
    have h3 := h2.const_mul (-1 / c)
    rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by
      field_simp [hc.ne']] at h3
    have h5 : (fun σ => (-1 / c) * Real.exp (-c * σ)) =
        (fun σ => -Real.exp (-c * σ) / c) := by
      funext σ
      field_simp [hc.ne']
    rw [h5] at h3
    exact h3
  have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) MeasureTheory.volume 3 XR := by
    apply ContinuousOn.intervalIntegrable
    exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn
  have e : Real.exp (-c * 3) = Real.exp (-3 * c) := by
    congr 1
    ring
  rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint, e]
  have h1 : (0 : ℝ) ≤ Real.exp (-c * XR) := (Real.exp_pos _).le
  have h2 : (0 : ℝ) < c := hc
  rw [show -Real.exp (-c * XR) / c - -Real.exp (-3 * c) / c =
      (Real.exp (-3 * c) - Real.exp (-c * XR)) / c by
    field_simp [h2.ne']
    ring]
  rw [show Real.exp (-3 * c) / c = (Real.exp (-3 * c) - (0 : ℝ)) / c by ring]
  exact div_le_div_of_nonneg_right (by linarith [h1]) h2.le

/-- The certified exponent-decay constant c = log 2 − 4/9 ≥ 0.2487. -/
lemma cdog_gt : (0.2487 : ℝ) ≤ Real.log 2 - 4 / 9 := by
  have h := Real.log_two_gt_d9
  norm_num at h
  linarith

/-- The certified e^{4/3} ≤ 3.8073 (the (1−x/16)⁻¹⁶ route + d9 e). -/
lemma exp_four_thirds_le : Real.exp (4 / 3) ≤ (3.8073 : ℝ) := by
  have he13 : Real.exp (1 / 3) ≤ (1.4006 : ℝ) :=
    le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)
  rw [show (4 / 3 : ℝ) = 1 + 1 / 3 by norm_num, Real.exp_add]
  calc Real.exp 1 * Real.exp (1 / 3) ≤ 2.7182818286 * 1.4006 :=
        mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)
    _ ≤ 3.8073 := by norm_num

/-- **THE HIGH-HORIZONTAL BOUND** (D-074 §7 capstone; D-073 Cor 4.2's
R(1.5) in single-exponential-envelope form): for 0 < U, n ≤ (4/9)U²
(i.e. U ≥ (3/2)√n) and 3 ≤ XR, ‖HIntegral (Jlag n) 3 XR U‖ ≤ 8.38
(charged; the true value ≤ 1.2 at n = 10⁵, E-034 V5). Charged with
dirichletC2 ≤ 1 — the tight R(1.5) = 5.94 would need a dirichletC2 ≤
0.57 build (documented as the tightening path; the fold is
indifferent: Δ ≈ +2.4 per side). -/
theorem hIntegral_Jlag_dogleg_norm_le {n : ℕ} {U XR : ℝ}
    (hU : 0 < U) (hnU : (n : ℝ) ≤ (4 / 9) * U ^ 2) (hXR : 3 ≤ XR) :
    ‖HIntegral (Jlag n) 3 XR U‖ ≤ (8.38 : ℝ) := by
  have hc : (0 : ℝ) < Real.log 2 - 4 / 9 := by
    have h := cdog_gt
    linarith
  have hpt : ∀ σ ∈ Set.Ioc 3 XR,
      ‖Jlag n ((σ : ℝ) + U * Complex.I)‖ ≤
        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) :=
    fun σ hσ => Jlag_dogleg_norm_le_envelope (by linarith [hσ.1]) hU hnU
  have hcontA : Continuous (fun σ : ℝ => Real.exp (-(Real.log 2 - 4 / 9) * σ)) :=
    Real.continuous_exp.comp (continuous_const.mul continuous_id)
  have hcontB : Continuous (fun σ : ℝ => (2 : ℝ) ^ (-σ)) := by
    have h1 : Continuous (fun σ : ℝ => Real.exp (-(Real.log 2) * σ)) :=
      Real.continuous_exp.comp (continuous_const.mul continuous_id)
    have h2 : (fun σ : ℝ => (2 : ℝ) ^ (-σ)) =
        (fun σ : ℝ => Real.exp (-(Real.log 2) * σ)) := by
      funext σ
      rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]
      congr 1
      ring
    rw [h2]
    exact h1
  have hIntA : IntervalIntegrable (fun σ : ℝ => 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ))
      MeasureTheory.volume 3 XR := by
    apply ContinuousOn.intervalIntegrable
    exact (hcontA.const_mul 4).continuousOn
  have hIntB : IntervalIntegrable (fun σ : ℝ => 4 * (2 : ℝ) ^ (-σ)) MeasureTheory.volume 3 XR := by
    apply ContinuousOn.intervalIntegrable
    exact (hcontB.const_mul 4).continuousOn
  have hIntG : IntervalIntegrable (fun σ : ℝ =>
      dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)))
      MeasureTheory.volume 3 XR := by
    have h := (hIntA.add hIntB).const_mul dirichletC2
    convert h using 1
  -- step 1: ‖H‖ ≤ ∫ envelope
  have h1 : ‖HIntegral (Jlag n) 3 XR U‖ ≤
      ∫ σ in (3 : ℝ)..XR,
        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) := by
    unfold HIntegral
    apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG
    exact Filter.Eventually.of_forall (fun σ hσ => hpt σ hσ)
  -- step 2: ∫ envelope = dirichletC2·(4∫e^{−cσ} + 4∫2^{−σ})
  have h2 : ∫ σ in (3 : ℝ)..XR,
        dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ))
      = dirichletC2 * ((∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ)) +
          (∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ))) := by
    rw [intervalIntegral.integral_const_mul, intervalIntegral.integral_add hIntA hIntB]
  -- step 3: the two integral bounds
  have h3a : ∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) ≤
      Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by
    rw [intervalIntegral.integral_const_mul]
    have h := integral_exp_neg_le hc hXR
    have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by
      have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by
        have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by
          rw [show ((1 : ℝ) / 8) = (2 ^ 3 : ℝ)⁻¹ by norm_num, Real.log_inv, Real.log_pow,
            Nat.cast_ofNat]
        rw [e1, Real.exp_log (by norm_num : (0 : ℝ) < 1 / 8)]
      calc Real.exp (-3 * (Real.log 2 - 4 / 9))
          = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring
        _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]
        _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring
    rw [he3c] at h
    calc 4 * ∫ σ in (3 : ℝ)..XR, Real.exp (-(Real.log 2 - 4 / 9) * σ)
        ≤ 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) :=
          mul_le_mul_of_nonneg_left h (by norm_num)
      _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by
        field_simp [hc.ne']
        ring
  have h3b : ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ) ≤ 1 / (2 * Real.log 2) := by
    have h2e : (fun σ : ℝ => 4 * (2 : ℝ) ^ (-σ)) =
        (fun σ : ℝ => 4 * Real.exp (-(Real.log 2) * σ)) := by
      funext σ
      rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]
      congr 1
      ring
    rw [h2e, intervalIntegral.integral_const_mul]
    have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : ℝ) < 2)) hXR
    have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by
      have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by
        rw [show ((1 : ℝ) / 8) = (2 ^ 3 : ℝ)⁻¹ by norm_num, Real.log_inv, Real.log_pow,
          Nat.cast_ofNat]
        ring
      rw [e1, Real.exp_log (by norm_num : (0 : ℝ) < 1 / 8)]
    rw [h3l2] at h
    calc 4 * ∫ σ in (3 : ℝ)..XR, Real.exp (-(Real.log 2) * σ)
        ≤ 4 * ((1 / 8) / Real.log 2) := by
          apply mul_le_mul_of_nonneg_left h (by norm_num : (0 : ℝ) ≤ 4)
      _ = 1 / (2 * Real.log 2) := by
        field_simp [(Real.log_pos (by norm_num : (1 : ℝ) < 2)).ne']
        norm_num
  -- step 4: the certified assembly
  have hlog2 : (0.6931471803 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9.le
  have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) ≤ (7.6545 : ℝ) := by
    have hcge := cdog_gt
    have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) ≤ 3.8073 / (2 * 0.2487) :=
      div_le_div₀ (by norm_num : (0 : ℝ) ≤ 3.8073) exp_four_thirds_le
        (by norm_num : (0 : ℝ) < 2 * 0.2487) (by linarith [hcge])
    calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))
        ≤ 3.8073 / (2 * 0.2487) := h1
      _ ≤ 7.6545 := by norm_num
  have h72 : 1 / (2 * Real.log 2) ≤ (0.7214 : ℝ) := by
    have h1 : 1 / (2 * Real.log 2) ≤ 1 / (2 * 0.6931471803) :=
      one_div_le_one_div_of_le (by positivity) (by linarith)
    calc 1 / (2 * Real.log 2) ≤ 1 / (2 * 0.6931471803) := h1
      _ ≤ 0.7214 := by norm_num
  have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one
  have hsum : dirichletC2 * ((∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ)) +
      (∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ))) ≤ (8.38 : ℝ) := by
    have hA0 : (0 : ℝ) ≤ Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity
    have hB0 : (0 : ℝ) ≤ 1 / (2 * Real.log 2) := by positivity
    have hIntAB : (0 : ℝ) ≤ (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ)) +
        (∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) := by
      apply add_nonneg
      · apply intervalIntegral.integral_nonneg hXR
        intro σ hσ
        positivity
      · apply intervalIntegral.integral_nonneg hXR
        intro σ hσ
        positivity
    calc dirichletC2 * ((∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ)) +
          (∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)))
        ≤ 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by
          apply mul_le_mul hC2 (add_le_add h3a h3b) hIntAB (by norm_num)
      _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring
      _ ≤ 7.6545 + 0.7214 := add_le_add h48 h72
      _ ≤ 8.38 := by norm_num
  calc ‖HIntegral (Jlag n) 3 XR U‖
      ≤ ∫ σ in (3 : ℝ)..XR,
          dirichletC2 * (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) := h1
    _ = dirichletC2 * ((∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ)) +
          (∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ))) := h2
    _ ≤ 8.38 := hsum

/-! ## 6. The far-right vertical drop (DL-4, D-074 §8) -/

/-- **Kernel at the far-right vertical** (D-074 §8): for n ≥ 16 and
t² ≥ n, ‖kFun n (2√n+it)‖ ≤ e^{√n/2}+1. (The ii′-4 lemma
`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s ≥ 2√n, i.e.
re w ≥ 2√n+1 — this is the w = 2√n variant: |1+1/(w−1)| ≤
1+(2√n)/((2√n−1)²+t²) ≤ 1+1/(2√n) since 4√n−1 ≤ t².) -/
theorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : ℕ} {t : ℝ}
    (hn : 16 ≤ n) (ht : (n : ℝ) ≤ t ^ 2) :
    ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
      Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by
  have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
  have hsq : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)
  have hw1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 =
      ((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I := by
    push_cast
    ring
  have hs0 : ((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I ≠ 0 := by
    intro h
    have him : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).im = 0 := by
      rw [h]; simp
    simp at him
    have ht0 : t = 0 := by
      have h1 : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).im = t := by simp
      linarith
    rw [ht0] at ht
    nlinarith [hnR]
  have hle := norm_one_add_one_div_le hs0
  have hre : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).re + 1 =
      2 * Real.sqrt (n : ℝ) := by
    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,
      Complex.sub_re, Complex.one_re]
  have hns : Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) =
      (2 * Real.sqrt (n : ℝ) - 1) ^ 2 + t ^ 2 := by
    simp [Complex.normSq_apply]
    ring
  have hkey : (2 * Real.sqrt (n : ℝ)) /
      Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤
      1 / (2 * Real.sqrt (n : ℝ)) := by
    rw [hns]
    have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)
    have h1 : 4 * Real.sqrt (n : ℝ) - 1 ≤ t ^ 2 := by
      have h2 : 4 * Real.sqrt (n : ℝ) ≤ (n : ℝ) + 1 := by
        have h3 : (4 * Real.sqrt (n : ℝ)) ^ 2 ≤ ((n : ℝ) + 1) ^ 2 := by
          rw [show (4 * Real.sqrt (n : ℝ)) ^ 2 = 16 * (Real.sqrt (n : ℝ) ^ 2) by ring, hsqn]
          nlinarith [sq_nonneg ((n : ℝ) - 1), hnR]
        nlinarith [hsq]
      nlinarith [ht, h2]
    rw [show (2 * Real.sqrt (n : ℝ) - 1) ^ 2 + t ^ 2 =
        4 * (Real.sqrt (n : ℝ) ^ 2) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2 by ring, hsqn]
    have h4 : (0 : ℝ) < 4 * (n : ℝ) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2 := by
      nlinarith [ht, sq_nonneg t, hsq]
    rw [div_le_iff₀ h4,
      show (1 / (2 * Real.sqrt (n : ℝ))) * (4 * (n : ℝ) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2) =
        (4 * (n : ℝ) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2) / (2 * Real.sqrt (n : ℝ)) by
        field_simp [hsq.ne'],
      le_div_iff₀ (by linarith [hsq] : (0 : ℝ) < 2 * Real.sqrt (n : ℝ))]
    nlinarith [h1, ht, hsq, hsqn]
  have hstep : 1 + ((((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).re + 1) /
      Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤
      1 + 1 / (2 * Real.sqrt (n : ℝ)) := by
    rw [hre]
    have h1 : (2 * Real.sqrt (n : ℝ)) /
        Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤
        1 / (2 * Real.sqrt (n : ℝ)) := hkey
    linarith [h1]
  have hpow1 : ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I))‖ ^ n ≤
      (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n :=
    pow_le_pow_left₀ (norm_nonneg _) (hle.trans hstep) n
  have hpow2 : (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n ≤
      Real.exp (Real.sqrt (n : ℝ) / 2) := by
    calc (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n
        ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ)))) ^ n := by
          have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : ℝ)))
          exact pow_le_pow_left₀ (by positivity) (by linarith) n
      _ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ)))) :=
          (Real.exp_nat_mul _ n).symm
      _ = Real.exp (Real.sqrt (n : ℝ) / 2) := by
          congr 1
          have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)
          field_simp [hsq.ne']
          nlinarith [hsqn]
  have hwid : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) /
      ((((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1) =
      1 + 1 / (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) := by
    rw [hw1]
    field_simp [hs0]
    push_cast
    ring
  unfold kFun
  rw [hwid]
  calc ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I)) ^ n - 1‖
      ≤ ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ :=
        norm_sub_le _ _
    _ = ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I))‖ ^ n + 1 := by
        rw [norm_pow, norm_one]
    _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by linarith [hpow1.trans hpow2]

/-- **The far-right vertical drop** (D-074 §8 V_right): for n ≥ 16,
0 < T ≤ U, T² ≥ n, ‖VIntegral (Jlag n) (2√n) T U‖ ≤
(U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 — exponentially tiny. -/
theorem vIntegral_Jlag_right_norm_le {n : ℕ} {T U : ℝ}
    (hn : 16 ≤ n) (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :
    ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ ≤
      (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
        ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by
  have hnorm : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ =
      ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by
    unfold VIntegral
    rw [norm_smul, Complex.norm_I, one_mul]
  rw [hnorm]
  have hbound : ∀ t ∈ Set.Ioc T U,
      ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
        (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by
    intro t ht
    have htT : T < t := ht.1
    have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]
    have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2
    have h2 := norm_logDeriv_zeta_le_two_pow
      (show (2 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) by
        have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
        have hsq : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by
          have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=
            Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))
          have h2 : Real.sqrt 16 = 4 := by
            rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num
          rwa [h2] at h1
        linarith) (t := t)
    have hnorm3 : ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ =
        ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ *
          ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by
      show ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) *
          (-logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I))‖ = _
      rw [norm_mul, norm_neg]
    rw [hnorm3]
    exact mul_le_mul h1 h2 (norm_nonneg _)
      (add_nonneg (Real.exp_nonneg _) (by norm_num))
  have hint : ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
      ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
        ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)) * |U - T| := by
    apply intervalIntegral.norm_integral_le_of_norm_le_const
    intro t ht
    rw [Set.uIoc_of_le hTU] at ht
    exact hbound t ht
  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)
  rw [habs] at hint
  calc ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖
      ≤ ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)) * (U - T) := hint
    _ = (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by ring

/-! ## 8. The direct Dirichlet bound at re = 2√n (DL-6) — the I_I /
V_right zeta factor WITHOUT certifying dirichletC2 ≤ 0.57.

The I_I charge in IIMaj is 0.57·2^{−(2√n−2)} = 2.28·2^{−2√n} (the
(6.10)-route constant |ζ′/ζ(2)|). Proving dirichletC2 ≤ 0.57 directly
needs a ~100-prime partial-sum build (the antitone-integral tail is too
fat). AVOIDED here: the DIRECT Dirichlet-series bound at re = 2√n gives
log2-leading + a 3^{−(2√n−2)} tail (dirichletC2 ≤ 1), which is ≤
0.57·2^{−(2√n−2)} for n ≥ 5 — the IIMaj charge exactly. -/

/-- The Dirichlet majorant at s = 2√n (summable since 2√n > 1). -/
def dirichletCX (n : ℕ) : ℝ :=
  ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
    ((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ) m‖

/-- ‖ζ′/ζ(2√n+it)‖ ≤ dirichletCX n for n ≥ 1 (the LSeries majorant). -/
lemma norm_logDeriv_zeta_le_dirichletCX {n : ℕ} (hn : 1 ≤ n) {t : ℝ} :
    ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
      dirichletCX n := by
  have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)
  have hs1 : (1 : ℝ) < (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I).re := by
    simp
    linarith
  have h1' : -logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)
      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) := by
    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1
    rw [logDeriv, Pi.div_apply, h2]
    ring
  have hsumX : Summable (fun m : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) := by
    rw [summable_norm_iff]
    apply ArithmeticFunction.LSeriesSummable_vonMangoldt
    rw [show (((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) from by simp]
    linarith
  have hsumS : Summable (fun m : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1
  have hle : ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
      (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤ dirichletCX n := by
    show ‖∑' m : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
      (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖ ≤ _
    calc ‖∑' m : ℕ, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖
        ≤ ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) m‖ :=
          norm_tsum_le_tsum_norm hsumS
      _ ≤ ∑' m : ℕ, ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖ :=
          Summable.tsum_le_tsum (fun m => LSeries.norm_term_le_of_re_le_re _ (by
            simp) m) hsumS hsumX
      _ = dirichletCX n := rfl
  calc ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖
      = ‖LSeries (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by
        rw [← h1', norm_neg]
    _ ≤ dirichletCX n := hle

/-- Termwise tail comparison: for m ≥ 3, the term at 2√n is ≤
3^{−(2√n−2)}·(the term at 2). -/
lemma norm_term_vonMangoldt_X_le_three_pow {n : ℕ} (hn : 1 ≤ n) {m : ℕ} (hm : 3 ≤ m) :
    ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖ ≤
      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *
        ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ := by
  have hXre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) := by simp
  have h2re : ((2 : ℂ).re) = 2 := rfl
  simp only [LSeries.norm_term_eq, hXre, h2re]
  split
  · norm_num
  · next hm0 =>
    have hΛ : ‖(ArithmeticFunction.vonMangoldt m : ℂ)‖ =
        ArithmeticFunction.vonMangoldt m :=
      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg
    rw [hΛ]
    have hm2 : (0 : ℝ) < (m : ℝ) := by exact_mod_cast (by omega : 0 < m)
    have hsqrt2 : (2 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by
      have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)
      linarith
    have hexp_nn : (0 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) - 2 := by linarith
    have e : ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ)) =
        (1 / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ) - 2)) *
          (ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ)) := by
      rw [show (2 * Real.sqrt (n : ℝ)) = (2 * Real.sqrt (n : ℝ) - 2) + 2 by ring,
        Real.rpow_add hm2]
      field_simp [hm2.ne']
      ring
    rw [e]
    have hle : (1 : ℝ) / (m : ℝ) ^ (2 * Real.sqrt (n : ℝ) - 2) ≤
        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
      rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 3), ← one_div]
      apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 3) _)
      exact Real.rpow_le_rpow (by norm_num : (0 : ℝ) ≤ 3)
        (by exact_mod_cast hm : (3 : ℝ) ≤ (m : ℝ)) hexp_nn
    have hpos : (0 : ℝ) ≤ ArithmeticFunction.vonMangoldt m / (m : ℝ) ^ (2 : ℝ) :=
      div_nonneg ArithmeticFunction.vonMangoldt_nonneg
        (Real.rpow_nonneg (by positivity : (0 : ℝ) ≤ (m : ℝ)) _)
    exact mul_le_mul_of_nonneg_right hle hpos

/-- The split: dirichletCX n = log 2·2^{−2√n} + (the m ≥ 3 tail). -/
lemma dirichletCX_le {n : ℕ} (hn : 1 ≤ n) :
    dirichletCX n ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by
  have hsumX : Summable (fun m : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) := by
    rw [summable_norm_iff]
    apply ArithmeticFunction.LSeriesSummable_vonMangoldt
    rw [show (((2 * Real.sqrt (n : ℝ) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) from by simp]
    have h1 : (1 : ℝ) ≤ Real.sqrt (n : ℝ) := Real.one_le_sqrt.mpr (by exact_mod_cast hn)
    linarith
  have hsplit := tsum_split_finset hsumX {0, 1, 2}
  have hsum2 : Summable (fun m : ℕ =>
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖) := by
    rw [summable_norm_iff]
    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)
  have hfin : ∑ i ∈ ({0, 1, 2} : Finset ℕ),
      ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖ =
      Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
    have hXre : ((((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ).re) = 2 * Real.sqrt (n : ℝ) := by simp
    rw [Finset.sum_insert (by norm_num), Finset.sum_insert (by norm_num),
      Finset.sum_singleton]
    simp only [LSeries.norm_term_eq, hXre]
    rw [if_pos (by norm_num), if_neg (by norm_num : (1 : ℕ) ≠ 0),
      if_neg (by norm_num : (2 : ℕ) ≠ 0)]
    simp [ArithmeticFunction.vonMangoldt_apply_one]
    have hΛ2 : |ArithmeticFunction.vonMangoldt 2| = Real.log 2 := by
      rw [ArithmeticFunction.vonMangoldt_apply_prime Nat.prime_two]
      exact abs_of_nonneg (by linarith [Real.log_two_gt_d9] : (0 : ℝ) ≤ Real.log 2)
    rw [hΛ2]
    have e : (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) = (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) := rfl
    rw [show Real.log 2 / (2 : ℝ) ^ (2 * Real.sqrt (n : ℝ)) =
        Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) by
      rw [Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 2)]
      field_simp [(Real.rpow_pos_of_pos (by norm_num : (0 : ℝ) < 2)
        (2 * Real.sqrt (n : ℝ))).ne']]
  have htail : (∑' i : ℕ, (if i ∈ ({0, 1, 2} : Finset ℕ) then 0
      else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
        (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖)) ≤
      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by
    have hterm : ∀ m : ℕ, (if m ∈ ({0, 1, 2} : Finset ℕ) then 0
        else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖) ≤
        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *
          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ := by
      intro m
      by_cases hm : m ∈ ({0, 1, 2} : Finset ℕ)
      · rw [if_pos hm]
        positivity
      · rw [if_neg hm]
        have hm3 : 3 ≤ m := by
          have h : m ∉ ({0, 1, 2} : Finset ℕ) := hm
          simp at h
          omega
        exact norm_term_vonMangoldt_X_le_three_pow hn hm3
    have hsum_tail : Summable (fun m : ℕ => (if m ∈ ({0, 1, 2} : Finset ℕ) then 0
        else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
          (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖)) := by
      apply Summable.of_norm_bounded hsumX.norm
      intro m
      by_cases hm : m ∈ ({0, 1, 2} : Finset ℕ) <;> simp [hm]
    calc (∑' m : ℕ, (if m ∈ ({0, 1, 2} : Finset ℕ) then 0
          else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) m‖))
        ≤ ∑' m : ℕ, (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) *
            ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ)) (2 : ℂ) m‖ :=
          Summable.tsum_le_tsum hterm hsum_tail (hsum2.mul_left _)
      _ = (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 := by
          rw [dirichletC2, tsum_mul_left]
  calc dirichletCX n
      = ∑ i ∈ ({0, 1, 2} : Finset ℕ),
          ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖ +
        ∑' i : ℕ, (if i ∈ ({0, 1, 2} : Finset ℕ) then 0
          else ‖LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : ℂ))
            (((2 * Real.sqrt (n : ℝ)) : ℝ) : ℂ) i‖) := hsplit
    _ ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
        (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2 :=
        add_le_add (le_of_eq hfin) htail

/-- log(9/4) ≥ 0.8109 (via e^{0.8109} = e/e^{0.1891} ≤ 2.25, the tight
e/e^{small} division-by-partial-sum route). -/
lemma log_nine_quarters_ge : (0.8109 : ℝ) ≤ Real.log (9 / 4) := by
  have h01891 : (1.20816 : ℝ) ≤ Real.exp 0.1891 :=
    le_trans (by norm_num [Finset.sum_range_succ])
      (Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 0.1891) 6)
  have h1 : Real.exp 0.8109 = Real.exp 1 / Real.exp 0.1891 := by
    rw [show (0.8109 : ℝ) = 1 - 0.1891 by norm_num, Real.exp_sub]
  have h2 : Real.exp 0.8109 ≤ 9 / 4 := by
    rw [h1]
    calc Real.exp 1 / Real.exp 0.1891
        ≤ 2.7182818286 / 1.20816 :=
          div_le_div₀ (by norm_num) Real.exp_one_lt_d9.le (by norm_num) h01891
      _ ≤ 9 / 4 := by norm_num
  have h3 := Real.log_le_log (Real.exp_pos _) h2
  rwa [Real.log_exp] at h3

/-- log(4/9) ≤ −0.8109 (the negation). -/
lemma log_four_ninths_le : Real.log (4 / 9) ≤ (-0.8109 : ℝ) := by
  have h1 := log_nine_quarters_ge
  have h2 : Real.log (4 / 9) = -Real.log (9 / 4) := by
    rw [show ((4 : ℝ) / 9) = (9 / 4)⁻¹ by norm_num, Real.log_inv]
  rw [h2]
  linarith [h1]

/-- The certified (4/9)^{√n} ≤ 0.164 for √n ≥ 2.236. -/
lemma four_ninths_rpow_sqrt_le {x : ℝ} (hx : (2.236 : ℝ) ≤ x) :
    (4 / 9 : ℝ) ^ x ≤ (0.164 : ℝ) := by
  have hlog49 := log_four_ninths_le
  have hlogneg : Real.log (4 / 9) < 0 :=
    Real.log_neg (by norm_num : (0 : ℝ) < 4 / 9) (by norm_num : (4 / 9 : ℝ) < 1)
  have h1 : (4 / 9 : ℝ) ^ x = Real.exp (Real.log (4 / 9) * x) :=
    Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) x
  rw [h1]
  have h2 : Real.log (4 / 9) * x ≤ (-1.81316 : ℝ) := by
    have h2a : Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 :=
      mul_le_mul_of_nonpos_left hx hlogneg.le
    have h2b : Real.log (4 / 9) * 2.236 ≤ (-0.8109) * 2.236 :=
      mul_le_mul_of_nonneg_right hlog49 (by norm_num)
    calc Real.log (4 / 9) * x ≤ Real.log (4 / 9) * 2.236 := h2a
      _ ≤ (-0.8109) * 2.236 := h2b
      _ ≤ -1.81316 := by norm_num
  have h3 : Real.exp (-1.81316) ≤ (0.164 : ℝ) := by
    have hsum : (6.113 : ℝ) ≤ Real.exp 1.81316 := by
      calc (6.113 : ℝ) ≤ ∑ i ∈ Finset.range 7, (1.81316 : ℝ) ^ i / (Nat.factorial i : ℝ) := by
            norm_num [Finset.sum_range_succ]
        _ ≤ Real.exp 1.81316 :=
            Real.sum_le_exp_of_nonneg (by norm_num : (0 : ℝ) ≤ 1.81316) 7
    rw [show Real.exp (-1.81316) = 1 / Real.exp 1.81316 by
      rw [Real.exp_neg, one_div]]
    calc 1 / Real.exp 1.81316 ≤ 1 / 6.113 :=
        one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 6.113) hsum
      _ ≤ 0.164 := by norm_num
  calc Real.exp (Real.log (4 / 9) * x) ≤ Real.exp (-1.81316) :=
        Real.exp_le_exp.mpr h2
    _ ≤ 0.164 := h3

/-- The 3^{−(2√n−2)} = 9·(4/9)^{√n}·2^{−2√n} identity. -/
lemma three_pow_neg_two_sqrt_sub_two_eq {n : ℕ} :
    (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) =
      9 * ((4 / 9 : ℝ) ^ Real.sqrt (n : ℝ)) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
  have h9 : Real.log 9 = 2 * Real.log 3 := by
    rw [show (9 : ℝ) = 3 ^ 2 by norm_num, Real.log_pow]
    push_cast
    ring
  have h2 : (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) =
      Real.exp (-(Real.log 2) * (2 * Real.sqrt (n : ℝ))) := by
    rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]
    congr 1
    ring
  have h3 : (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) =
      Real.exp (-(Real.log 3) * (2 * Real.sqrt (n : ℝ) - 2)) := by
    rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 3)]
    congr 1
    ring
  have h49 : (4 / 9 : ℝ) ^ Real.sqrt (n : ℝ) =
      Real.exp (Real.log (4 / 9) * Real.sqrt (n : ℝ)) :=
    Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 4 / 9) _
  rw [h2, h3, h49]
  have hlog49 : Real.log (4 / 9) = Real.log 2 - Real.log 9 + Real.log 2 := by
    rw [Real.log_div (by norm_num : (4 : ℝ) ≠ 0) (by norm_num : (9 : ℝ) ≠ 0),
      show Real.log 4 = 2 * Real.log 2 by
        rw [show ((4 : ℝ)) = 2 ^ 2 by norm_num, Real.log_pow]
        push_cast
        ring]
    ring
  rw [hlog49, h9, mul_assoc, ← Real.exp_add]
  rw [show (9 : ℝ) = Real.exp (Real.log 9) from (Real.exp_log (by norm_num : (0 : ℝ) < 9)).symm]
  rw [← Real.exp_add, h9]
  congr 1
  ring

/-- **The I_I zeta charge WITHOUT dirichletC2 ≤ 0.57** (DL-6 capstone):
for n ≥ 5, ‖ζ′/ζ(2√n+it)‖ ≤ 0.57·2^{−(2√n−2)} — the IIMaj zeta form,
via the direct log2-leading + 3^{−(2√n−2)} tail (dirichletC2 ≤ 1) with
the certified (4/9)^{√n} ≤ 0.17631 bound at √n ≥ √5. -/
theorem norm_logDeriv_zeta_le_iimZeta {n : ℕ} (hn : 5 ≤ n) {t : ℝ} :
    ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
      (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
  have hn1 : 1 ≤ n := by omega
  have h1 := norm_logDeriv_zeta_le_dirichletCX hn1 (t := t)
  have h2 := dirichletCX_le hn1
  have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one
  have hC2nn : (0 : ℝ) ≤ dirichletC2 := dirichletC2_nonneg
  have hsqrt5 : (2.236 : ℝ) ≤ Real.sqrt (n : ℝ) := by
    have hnR : (5 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have h1 : Real.sqrt 5 ≤ Real.sqrt (n : ℝ) := Real.sqrt_le_sqrt hnR
    have h2 : (2.236 : ℝ) ≤ Real.sqrt 5 := by
      rw [Real.le_sqrt (by norm_num) (by norm_num)]
      norm_num
    linarith
  have h49 := four_ninths_rpow_sqrt_le hsqrt5
  have h3 : dirichletCX n ≤ Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
    have hnn : (0 : ℝ) ≤ (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by positivity
    refine h2.trans ?_
    simpa using add_le_add_right (mul_le_mul_of_nonneg_left hC2 hnn)
      (Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))))
  have h4 : (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) ≤
      (1.476 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
    rw [three_pow_neg_two_sqrt_sub_two_eq]
    calc 9 * ((4 / 9 : ℝ) ^ Real.sqrt (n : ℝ)) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ)))
        ≤ 9 * (0.164 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
          apply mul_le_mul_of_nonneg_right _ (Real.rpow_nonneg (by norm_num) _)
          apply mul_le_mul_of_nonneg_left h49 (by norm_num)
      _ = (1.476 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by ring
  have h5 : Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
      (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) ≤
      (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) := by
    have hlog2 : Real.log 2 ≤ (0.6931471808 : ℝ) := Real.log_two_lt_d9.le
    have hpos2 : (0 : ℝ) < (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by positivity
    have e : (0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) =
        (2.28 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
      rw [show (-(2 * Real.sqrt (n : ℝ) - 2)) = -2 * Real.sqrt (n : ℝ) + 2 by ring,
        Real.rpow_add (by norm_num : (0 : ℝ) < 2), Real.rpow_two]
      ring
    rw [e]
    calc Real.log 2 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
          (3 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))
        ≤ 0.6931471808 * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) +
          (1.476 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
          apply add_le_add _ h4
          exact mul_le_mul_of_nonneg_right hlog2 hpos2.le
      _ = (0.6931471808 + 1.476 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by ring
      _ ≤ (2.28 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ))) := by
          apply mul_le_mul_of_nonneg_right _ hpos2.le
          norm_num
  exact h1.trans (h3.trans h5)

/-! ## 9. The far-right vertical drop, quarter charge (DL-6-ii) -/

/-- **The far-right vertical drop, quarter charge** (DL-6-ii): for
n ≥ 16, 0 < T ≤ U, T² ≥ n, ‖VIntegral (Jlag n) (2√n) T U‖ ≤
(U−T)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — the IIMaj/4 per-length form,
via the DIRECT dirichlet bound (norm_logDeriv_zeta_le_iimZeta, NO
dirichletC2 ≤ 0.57 needed). -/
theorem vIntegral_Jlag_right_norm_le_quarter {n : ℕ} {T U : ℝ}
    (hn : 16 ≤ n) (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :
    ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ ≤
      (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
        ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
  have hnorm : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ =
      ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by
    unfold VIntegral
    rw [norm_smul, Complex.norm_I, one_mul]
  rw [hnorm]
  have hbound : ∀ t ∈ Set.Ioc T U,
      ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
        (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
    intro t ht
    have htT : T < t := ht.1
    have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]
    have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2
    have h2 := norm_logDeriv_zeta_le_iimZeta (by omega : 5 ≤ n) (t := t)
    have hnorm3 : ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ =
        ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ *
          ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by
      show ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) *
          (-logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I))‖ = _
      rw [norm_mul, norm_neg]
    rw [hnorm3]
    exact mul_le_mul h1 h2 (norm_nonneg _)
      (add_nonneg (Real.exp_nonneg _) (by norm_num))
  have hint : ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤
      ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
        ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) * |U - T| := by
    apply intervalIntegral.norm_integral_le_of_norm_le_const
    intro t ht
    rw [Set.uIoc_of_le hTU] at ht
    exact hbound t ht
  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)
  rw [habs] at hint
  calc ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖
      ≤ ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)))) * (U - T) := hint
    _ = (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
          ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by ring

/-- **V_right ≤ IIMaj/4** (DL-6-ii accounting): for n ≥ 16 and
T ∈ [√n, √n+1], U = (3/2)·T, the far-right drop is ≤ IIMaj(n)/4
(exactly: IIMaj/4 = ((√n+1)/2)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)}). -/
theorem vIntegral_Jlag_right_le_IIMaj_quarter {n : ℕ} {T : ℝ}
    (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
    ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤ IIMaj (n : ℝ) / 4 := by
  have hT0 : (0 : ℝ) < T := by
    have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have hsqrt4 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by
      have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=
        Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))
      have h2 : Real.sqrt 16 = 4 := by
        rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num
      rwa [h2] at h1
    linarith
  have hTn2 : (n : ℝ) ≤ T ^ 2 := by
    have h1 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 :=
      pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2
    rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : ℝ)])] at h1
  have hTU : T ≤ (3 / 2) * T := by linarith [hT0]
  have hVr' := vIntegral_Jlag_right_norm_le_quarter hn hT0 hTU hTn2 (n := n)
  have hlen : (3 / 2) * T - T ≤ (Real.sqrt (n : ℝ) + 1) / 2 := by linarith [hTn1, hTn]
  have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]
  have e4 : IIMaj (n : ℝ) / 4 =
      ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *
        ((0.57 : ℝ) * (2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2))) := by
    unfold IIMaj
    ring
  rw [e4]
  refine hVr'.trans ?_
  apply mul_le_mul _ (le_refl _) (by positivity) (by positivity)
  exact mul_le_mul hlen (le_refl _) (by positivity) (by positivity)
/-! ## 7. The total right-horizontal bound (DL-5, D-074 §3.4) -/

/-- **The upper right-tail bound** (D-074 §3.4): for n ≥ 16 and
T ∈ [√n, √n+1] (the T_cut window), U = (3/2)·T,
‖HIntegral (Jlag n) 3 (2√n) T‖ ≤ ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 +
IIMaj(n)/4 — the exact deformation identity +
V_left/H_high/V_right piece bounds, all in the zero-free region. -/
theorem hIntegral_Jlag_low_le_dogLegUpper {n : ℕ} {T : ℝ}
    (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
    ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ ≤
      ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
        IIMaj (n : ℝ) / 4 := by
  have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
  have hsqrt4 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by
    have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=
      Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))
    have h2 : Real.sqrt 16 = 4 := by
      rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num
    rwa [h2] at h1
  have hT0 : (0 : ℝ) < T := by linarith
  have hTn2 : (n : ℝ) ≤ T ^ 2 := by
    have h1 : (Real.sqrt (n : ℝ)) ^ 2 ≤ T ^ 2 :=
      pow_le_pow_left₀ (Real.sqrt_nonneg _) hTn 2
    rwa [Real.sq_sqrt (by linarith [Real.sqrt_nonneg (n : ℝ)])] at h1
  have hU0 : (0 : ℝ) < (3 / 2) * T := by linarith [hT0]
  have hTU : T ≤ (3 / 2) * T := by linarith [hT0]
  have hnU : (n : ℝ) ≤ (4 / 9) * ((3 / 2) * T) ^ 2 := by
    have h1 : (4 / 9) * ((3 / 2) * T) ^ 2 = T ^ 2 := by
      field_simp
      ring
    rw [h1]
    exact hTn2
  have hXR : (3 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) := by linarith
  have hid := upper_right_horizontal_eq_dogleg hT0 hTU hXR (n := n)
  have hH := hIntegral_Jlag_dogleg_norm_le hU0 hnU hXR (n := n)
  have hVr := vIntegral_Jlag_right_norm_le hn hT0 hTU hTn2 (n := n)
  have hVl := vIntegral_Jlag_three_norm_le hT0 hTU hTn2 (n := n)
  have hlen : (3 / 2) * T - T ≤ (Real.sqrt (n : ℝ) + 1) / 2 := by linarith [hTn1, hTn]
  have hlen0 : (0 : ℝ) ≤ (3 / 2) * T - T := by linarith [hT0]
  -- V_left ≤ ((√n+1)/2)·(e^{5/2}+1)/2
  have hVl2 : ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ ≤
      ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 := by
    refine hVl.trans ?_
    exact div_le_div_of_nonneg_right
      (mul_le_mul hlen (le_refl _) (by positivity) (by positivity)) (by norm_num)
  -- V_right ≤ IIMaj/4 (DL-6-ii's quarter charge)
  have hVr2 : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ ≤
      IIMaj (n : ℝ) / 4 :=
    vIntegral_Jlag_right_le_IIMaj_quarter hn hTn hTn1 (n := n)
  -- assemble via the exact identity
  rw [hid]
  calc ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -
        VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T) +
        VIntegral (Jlag n) 3 T ((3 / 2) * T)‖
      ≤ ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T)‖ +
        ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T)‖ +
        ‖VIntegral (Jlag n) 3 T ((3 / 2) * T)‖ := by
        have h1 := norm_add_le
          (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T) -
            VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T))
          (VIntegral (Jlag n) 3 T ((3 / 2) * T))
        have h2 := norm_sub_le
          (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) ((3 / 2) * T))
          (VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T ((3 / 2) * T))
        linarith [h1, h2]
    _ ≤ (8.38 : ℝ) + IIMaj (n : ℝ) / 4 +
        ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 :=
        add_le_add (add_le_add hH hVr2) hVl2
    _ = ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
        IIMaj (n : ℝ) / 4 := by ring

/-- **The lower right-tail bound by conjugation** (D-074 §3.4): the
same bound holds at im = −T (the integrand is conjugation-symmetric,
Jlag_conj; the interval integral maps conj through). -/
theorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper {n : ℕ} {T : ℝ}
    (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
    ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤
      ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
        IIMaj (n : ℝ) / 4 := by
  have hT0 : (0 : ℝ) < T := by
    have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
    have hsqrt4 : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by
      have h1 : Real.sqrt 16 ≤ Real.sqrt (n : ℝ) :=
        Real.sqrt_le_sqrt (by exact_mod_cast hn : (16 : ℝ) ≤ (n : ℝ))
      have h2 : Real.sqrt 16 = 4 := by
        rw [Real.sqrt_eq_iff_eq_sq (by norm_num) (by norm_num)]; norm_num
      rwa [h2] at h1
    linarith
  have hconj : HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T) =
      (starRingEnd ℂ) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T) := by
    unfold HIntegral
    rw [← intervalIntegral.intervalIntegral_conj]
    apply intervalIntegral.integral_congr
    intro σ hσ
    show Jlag n ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
      (starRingEnd ℂ) (Jlag n ((σ : ℝ) + T * Complex.I))
    have hid2 : ((σ : ℝ) + (((-T : ℝ)) : ℂ) * Complex.I) =
        (starRingEnd ℂ) ((σ : ℝ) + T * Complex.I) := by
      simp
    rw [hid2]
    exact Jlag_conj n (by
      intro h
      have him : (((σ : ℝ) + T * Complex.I)).im = T := by simp
      rw [h] at him
      simp at him
      linarith [hT0])
  rw [hconj, Complex.norm_conj]
  exact hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1

/-- **THE TWO-SIDE RIGHT-HORIZONTAL BOUND** (the DL capstone for
ii′-6-c): both horizontal right tails bounded by the dog-leg charge. -/
theorem dogLegUpper_two_sides {n : ℕ} {T : ℝ}
    (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :
    ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ +
      ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T)‖ ≤
    2 * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
      IIMaj (n : ℝ) / 4) := by
  rw [show (2 : ℝ) * (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 +
      (8.38 : ℝ) + IIMaj (n : ℝ) / 4) =
      (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
        IIMaj (n : ℝ) / 4) +
      (((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +
        IIMaj (n : ℝ) / 4) by ring]
  exact add_le_add (hIntegral_Jlag_low_le_dogLegUpper hn hTn hTn1)
    (hIntegral_Jlag_low_neg_norm_le_dogLegUpper hn hTn hTn1)


end NguyenRH1

end