[{"type":"thinking","thinking":"DL-4 committed (4bc3c09). Now DL-5: the total right-horizontal bound + the lower side.\n\nDL-5 components:\n1. **The upper-side assembly**: from `upper_right_horizontal_eq_dogleg` (H(3→XR, T) = H(3→XR, U) − V(XR, T→U) + V(3, T→U)):\n   ‖H(3→XR, T)‖ ≤ ‖H(3→XR, U)‖ + ‖V(XR, T→U)‖ + ‖V(3, T→U)‖ ≤ 8.38 + V_right_bound + V_left_bound.\n\n   With the hypotheses: T ∈ [√n, √n+1] (the T_cut window), U = (3/2)·T:\n   - V_left: ‖V(3, T→U)‖ ≤ (U−T)·(e^{5/2}+1)/2 with U−T = T/2 ≤ (√n+1)/2: ≤ ((√n+1)/2)·(e^{5/2}+1)/2 — need T² ≥ n for the kernel lemma ✓ (T ≥ √n) and 0 < T ✓. vIntegral_Jlag_three_norm_le's hypotheses: hT0 : 0 < T, hTU : T ≤ U, hTn : n ≤ T² ✓.\n   - H_high: ‖H(3→XR, U)‖ ≤ 8.38 — hIntegral_Jlag_dogleg_norm_le's hypotheses: hU : 0 < U, hnU : n ≤ (4/9)·U², hXR : 3 ≤ XR. hnU : n ≤ (4/9)·U² ⟺ U² ≥ (9/4)n: U = (3/2)T ≥ (3/2)√n ⟹ U² ≥ (9/4)n ✓ (T ≥ √n).\n   - V_right: ‖V(XR, T→U)‖ ≤ (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 with XR = 2√n — vIntegral_Jlag_right_norm_le's hypotheses: hn : 16 ≤ n, hT0, hTU, hTn ✓. With U−T ≤ (√n+1)/2 and dirichletC2 ≤ 1: ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} ≤ IIMaj/2.\n\n   The XR instantiation: in the assembly, XR := 2√n (the main rectangle's right edge) ✓ and 3 ≤ XR ⟺ 2√n ≥ 3 ⟺ n ≥ 9/4 ✓ (n ≥ 16 covers).\n\n   So the upper total:\n   ‖H(3→2√n, T)‖ ≤ ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj/2\n   =: DogLegUpper(n).\n\n   Hmm — the V_left's factor (e^{5/2}+1)/2 with the (U−T) ≤ (√n+1)/2: VLeft = (U−T)·(e^{5/2}+1)/2·... wait — vIntegral_Jlag_three_norm_le gives ‖V‖ ≤ (U−T)·(e^{5/2}+1)/2. With U−T = T/2 ∈ [√n/2, (√n+1)/2]: ≤ ((√n+1)/2)·(e^{5/2}+1)/2?? — (U−T)·X ≤ ((√n+1)/2)·X ✓. So VLeftBound_Lean := ((√n+1)/2)·(e^{5/2}+1)/2 = (√n+1)·(e^{5/2}+1)/4 ≈ (√n+1)·3.296.\n\n   Hmm — wait, the E-034's VLeftBound was ((√n+1)/2)·(e^{5/2}+1)·C_zeta3 with C_zeta3 = 0.5 = ((√n+1)/2)·13.19·0.5 = 3.2975·(√n+1). The Lean vIntegral_Jlag_three_norm_le states ‖V‖ ≤ (U−T)·(e^{5/2}+1)/2 — that's (U−T)·13.19/2 = (U−T)·6.5975?! — with the /2 from dirichletC3 ≤ 1/2: (e^{5/2}+1)/2 = 13.19/2 = 6.595. And (U−T) ≤ (√n+1)/2: ≤ ((√n+1)/2)·6.595 = 3.2975·(√n+1) ✓ SAME as E-034's VLeftBound ✓✓ consistent (the /2 in the lemma IS the C_zeta3 = 0.5).\n\n   So DogLegUpper(n) := ((√n+1)/2)·(e^{5/2}+1)/2 + 8.38 + IIMaj(n)/2.\n\n2. **The lower side by conjugation**: the main contour's lower horizontal at im = −T: H(3→XR, −T) (traversed L→R). By conjugation: HIntegral (Jlag n) 3 XR (−T) = conj (HIntegral (Jlag n) 3 XR T)?? — the integrand conj identity: Jlag n (conj s) = conj (Jlag n s) (Jlag_conj). The interval integral: ∫_3^XR Jlag(σ−iT) dσ vs conj(∫_3^XR Jlag(σ+iT) dσ): \n   conj(∫ Jlag(σ+iT) dσ) = ∫ conj(Jlag(σ+iT)) dσ = ∫ Jlag(conj(σ+iT)) dσ = ∫ Jlag(σ−iT) dσ ✓ — via the integral's conjugation symmetry: `Complex.conj_integral` or `intervalIntegral.conj`?? — Mathlib: `integral_conj` : conj (∫ f) = ∫ (conj ∘ f) — for interval: `intervalIntegral.integral_conj`? or use the map-cong + Complex.integral_conj... Let me check the exact name. Then ‖H(3→XR, −T)‖ = ‖conj(H(3→XR, T))‖ = ‖H(3→XR, T)‖ (norm_conj) ≤ same bound ✓.\n\n   But WAIT — the LOWER horizontal's orientation in the main contour: the bottom side is traversed L→R at im = −T (from the audit: bottom +H f z.re w.re z.im with z.im = −T: HIntegral f (−5/2) (2√n) (−T) — L→R ✓). The lower right tail [3, XR] at im = −T is traversed L→R — SAME direction as the upper (R→L)?! NO — the audit says: upper top is R→L (x : 2√n → −5/2), lower bottom is L→R (x : −5/2 → 2√n). So the upper right tail in the contour appears as part of −H(z.re→w.re at +T) (reversed), and the lower right tail as part of +H(z.re→w.re at −T) (forward). For the BOUND, orientation doesn't matter for ‖·‖.\n\n   The lower bound: ‖H(3→XR, −T)‖ = ‖conj(H(3→XR, T))‖ = ‖H(3→XR, T)‖ ≤ DogLegUpper(n) ✓.\n\n   The conj-integral lemma: need `∫ conj(f) = conj(∫ f)` on the interval + the pointwise conj identity Jlag n (σ−iT) = conj(Jlag n (σ+iT))... — hmm: conj(σ+iT) = σ−iT ✓ (σ, T real). Jlag_conj (n) {s} (hs : s ≠ 1) : Jlag n (conj s) = conj (Jlag n s) — at s = σ+iT (≠ 1 since im = T > 0 ✓): Jlag n (σ−iT) = conj(Jlag n (σ+iT)) ✓.\n\n   So: HIntegral (Jlag n) 3 XR (−T) = ∫_3^XR Jlag(σ−iT) dσ = ∫_3^XR conj(Jlag n (σ+iT)) dσ = conj(∫_3^XR Jlag(σ+iT) dσ) = conj(HIntegral (Jlag n) 3 XR T) — the middle step: ∫ conj(f(σ)) dσ = conj(∫ f(σ) dσ) — the integral conj-map. Mathlib: `Complex.conj_integral`?? — for Bochner: `integral_conj` (RCLike): `∫ x, conj (f x) = conj (∫ x, f x)`?? — RCLike.conj_integral or `RCLike.integral_conj`... For the interval version, the integral IS a Bochner integral on the interval measure, so the Bochner conj lemma applies. Let me grep for the name.\n\n3. **The two-side total**: ‖H(3→XR, T)‖ + ‖H(3→XR, −T)‖ ≤ 2·DogLegUpper(n) — as the reusable capstone for ii′-6-c.\n\nAlso needed: the U = (3/2)·T definition at the assembly level (U := (3/2)·T) and the window hypotheses (hTn : √n ≤ T, hTn1 : T ≤ √n+1, hn : 16 ≤ n, hT0 : 0 < T... T ≥ √n ≥ 4 ✓).\n\nLet me structure DL-5:\n\n```lean\n/-- The upper right-tail bound (D-074 §3.4): for n ≥ 16, T ∈ [√n, √n+1],\nU = (3/2)·T, ‖HIntegral (Jlag n) 3 (2√n) T‖ ≤ DogLegUpper n. -/\ntheorem hIntegral_Jlag_low_le_dogLegUpper {n : ℕ} {T : ℝ}\n    (hn : 16 ≤ n) (hTn : Real.sqrt (n : ℝ) ≤ T) (hTn1 : T ≤ Real.sqrt (n : ℝ) + 1) :\n    ‖HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T‖ ≤\n      ((Real.sqrt (n : ℝ) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : ℝ) +\n        IIMaj (n : ℝ) / 2 := by\n  -- U := 1.5·T; the identity + the three pieces\n```\n\nand\n\n```lean\n/-- The lower right-tail bound by conjugation. -/\ntheorem hIntegral_Jlag_low_conj_eq (n : ℕ) (T : ℝ) (hT : 0 < T) :\n    HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) (-T) =\n      (starRingEnd ℂ) (HIntegral (Jlag n) 3 (2 * Real.sqrt (n : ℝ)) T) := ...\ntheorem hIntegral_Jlag_low_neg_norm_le_dogLegUpper ... := ‖·‖ = via norm_conj\n```\n\nThe HIntegral conj: HIntegral f x₁ x₂ y = ∫ x in x₁..x₂, f (x + y·I). With y = −T: f(σ − iT) = Jlag n (σ − iT) = conj(Jlag n (σ + iT)) (Jlag_conj with s = σ+iT ≠ 1 ✓). So:\n∫_3^XR Jlag(σ−iT) = ∫_3^XR conj(Jlag n (σ+iT)) dσ = conj(∫_3^XR Jlag(σ+iT) dσ).\n\nThe integral conj lemma: for interval integrals of ℂ-valued functions: `intervalIntegral.integral_conj`? Let me check — there's `intervalIntegral.integral_comp_conj`?? or for Bochner `integral_conj` (RCLike ℂ): `∫ x, (starRingEnd ℂ) (f x) ∂μ = (starRingEnd ℂ) (∫ x, f x ∂μ)` — Mathlib: `RCLike.integral_conj`?? or `star_integral`... Let me grep.\n\nActually — simpler: the norm equality is all I need (‖H(−T)‖ = ‖H(T)‖): \n‖H(3→XR, −T)‖ = ‖conj(H(3→XR, T))‖ = ‖H(3→XR, T)‖ via norm_conj/starRingEnd.norm_apply... — hmm wait: H(−T) = conj(H(T)) by the integral conj symmetry. Then norms equal.\n\nThe pointwise identity: Jlag n (σ + (−T)·I) = conj(Jlag n (σ + T·I)): conj(σ + T·I) = σ − T·I = σ + (−T)·I ✓ — Jlag_conj (with hs : σ+iT ≠ 1 ✓ im = T > 0): Jlag n (conj(σ+iT)) = conj(Jlag n (σ+iT)) and conj(σ+iT) = σ−iT ✓ — need the point identification: ((σ:ℝ) + (−T)·I) = starRingEnd ℂ ((σ:ℝ) + T·I) — by Complex.ext (re/im simp) ✓.\n\nThen: ∫_3^XR Jlag(σ + (−T)·I) dσ = ∫_3^XR conj(Jlag n (σ + T·I)) dσ = conj(∫_3^XR Jlag(σ+T·I) dσ) — the last step: ∫ conj(f) = conj(∫ f) — the integral conj lemma. Name check needed.\n\nLet me grep for the integral conj lemma name, then write DL-5.","signature":""},{"type":"text","text":"DL-4 committed (`4bc3c09`). Now **DL-5** — the total bound + lower side. Checking the integral-conjugation lemma name first."},{"type":"tool_use","id":"TodoWrite_375","name":"TodoWrite","input":{"todos":[{"content":"DL-5a: upper total bound hIntegral_Jlag_low_le_dogLegUpper (identity + 3 pieces + U=(3/2)T accounting)","status":"in_progress","activeForm":"Assembling the upper total bound"},{"content":"DL-5b: lower side by conjugation (HIntegral conj + Jlag_conj) + two-side capstone + build + audit + commit","status":"pending","activeForm":"Proving the lower side by conjugation"}]},"extra_content":null},{"type":"tool_use","id":"Bash_376","name":"Bash","input":{"command":"cd D:/Python/Quantum/zeta-23-lean && grep -rn \"theorem integral_conj\\|lemma integral_conj\\|conj_integral\" .lake/packages/mathlib/Mathlib/MeasureTheory/Integral/Bochner/*.lean 2>/dev/null | head -4; grep -rn \"starRingEnd.*integral\\|integral.*starRingEnd\" .lake/packages/mathlib/Mathlib/Analysis/RCLike/*.lean 2>/dev/null | head -4","description":"Find the integral conjugation lemma name"},"extra_content":null}]