← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (3753 chars)
`Rectangle z w := [[z.re, w.re]] ×ℂ [[z.im, w.im]]` where [[a,b]] is uIcc. Membership: `Complex.mem_reProdIm : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t` ✓.
For the rewrite in holomorphicOn_Jlag_dogleg:
```
intro s hs
rw [Rectangle, Complex.mem_reProdIm] at hs
```
rw [Rectangle] — Rectangle is a def; rw with the def name works if it has equation lemmas (simple def → `Rectangle.eq_def` or unfold). Safer: `rw [Rectangle, Complex.mem_reProdIm] at hs` — Mathlib defs by pattern-matching usually generate usable equation lemmas for rw; if not, use `simp only [Rectangle, Complex.mem_reProdIm] at hs`. Hmm — LiAssembly did `rw [RectangleBorder] at hb` — RectangleBorder is a def in Zeta23 and rw worked ✓. Rectangle is a plain def too — rw [Rectangle] should unfold it via its equation lemma ✓. But [[a,b]] is uIcc notation — after rw, hs : s.re ∈ [[(dogZ T).re, (dogW XR U).re]] ∧ ... — then rewrite the corner re/ims. `[[a,b]]` is `Set.uIcc a b` (notation in Mathlib: [[a, b]] = uIcc a b with open scoped Interval). Then `rw [Set.uIcc_of_le hXR]` etc.
Actually cleaner:
```
intro s hs
have hs' := 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
```
Wait — hs'.1.1 : 3 ≤ s.re ✓; hs'.2.1 : T ≤ s.im, need 0 < s.im: linarith [hT, hs'.2.1] ✓.
But does `rw [dogZ_re, ...]` work inside hs'? dogZ_re (T) : (dogZ T).re = 3 — rewriting (dogZ T).re → 3 ✓. But after `rw [Rectangle]`, the term is [[(dogZ T).re, (dogW XR U).re]] ×ℂ ... — rw [Complex.mem_reProdIm] turns membership into the ∧ ✓ then rw [dogZ_re] rewrites (dogZ T).re ✓ ✓.
OK. Now also the `unfold RectangleIntegral at h0` step in upper_right_horizontal_eq_dogleg: RectangleIntegral is a def in Zeta23 — unfold works, or rw [RectangleIntegral]. LiPrincipal used `rw [RectangleIntegral', RectangleIntegral', ...]` — those are abbrevs (reducible). For the def RectangleIntegral, `unfold RectangleIntegral at h0` should work (LiSides or others used `unfold` for defs? kFun was unfolded via `unfold kFun` in LiContour? It used `simp [kFun]`? Whatever — `unfold RectangleIntegral at h0` is standard).
Then h0 : HIntegral (Jlag n) (dogZ T).re (dogW XR U).re (dogZ T).im − HIntegral (Jlag n) (dogZ T).re (dogW XR U).re (dogW XR U).im + VIntegral (Jlag n) (dogW XR U).re (dogZ T).im (dogW XR U).im − VIntegral (Jlag n) (dogZ T).re (dogZ T).im (dogW XR U).im = 0. rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0 normalizes all corners ✓ then linear_combination h0.
Wait — the VIntegral args: VIntegral f x y₁ y₂ with the rectangle's V f w.re z.im w.im: x = (dogW).re = XR, y₁ = (dogZ).im = T, y₂ = (dogW).im = U ✓ → VIntegral (Jlag n) XR T U ✓; and −V f z.re z.im w.im: −VIntegral (Jlag n) 3 T U ✓. The goal: H 3 XR T = H 3 XR U − V XR T U + V 3 T U. From h0: H_low − H_high + V_right − V_left = 0. linear_combination h0: goal − h0 = 0: (H_low − (H_high − V_right + V_left)) − (H_low − H_high + V_right − V_left) = 0 ✓.
One risk: the dogZ/dogW def form ((3:ℝ):ℂ) + (T:ℝ)*I vs rectW's ((2√n:ℝ):ℂ) + T*I — same pattern ✓ simp [dogZ] should prove dogZ_re like simp [rectW] proved rectW_re ✓.
Now write the file and build. Also need to check `riemannZeta_ne_zero_of_one_lt_re` visibility: it's Mathlib's root lemma (in Dirichlet.lean, probably root namespace). LiDogLeg imports Mathlib + LiSides + LiTightR ✓.
Also `rintro rfl; simp at him` for s ≠ 1: him : 0 < s.im becomes 0 < (1:ℂ).im — simp: Complex.one_im : (1:ℂ).im = 0 — simp at him derives 0 < 0 → closes by lt_irrefl? simp should close it (simp at him turns it into False and closes the goal if him reduces to False ✓ standard pattern).
Write LiDogLeg.lean now.
All API confirmed. Writing `LiDogLeg.lean` (DL-1).
tool: Write ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"content": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_div, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one, iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1, map_mul, map_neg, map_div]\n\nend NguyenRH1\n\nend\n"
}
result 2026-08-26 04:59:28Z → 2026-08-26 04:59:28Z
{
"type": "create",
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"content": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_div, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one, iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1, map_mul, map_neg, map_div]\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [],
"originalFile": null
}
raw content_json (database row)
[{"type":"thinking","thinking":"`Rectangle z w := [[z.re, w.re]] ×ℂ [[z.im, w.im]]` where [[a,b]] is uIcc. Membership: `Complex.mem_reProdIm : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t` ✓.\n\nFor the rewrite in holomorphicOn_Jlag_dogleg:\n```\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm] at hs\n```\nrw [Rectangle] — Rectangle is a def; rw with the def name works if it has equation lemmas (simple def → `Rectangle.eq_def` or unfold). Safer: `rw [Rectangle, Complex.mem_reProdIm] at hs` — Mathlib defs by pattern-matching usually generate usable equation lemmas for rw; if not, use `simp only [Rectangle, Complex.mem_reProdIm] at hs`. Hmm — LiAssembly did `rw [RectangleBorder] at hb` — RectangleBorder is a def in Zeta23 and rw worked ✓. Rectangle is a plain def too — rw [Rectangle] should unfold it via its equation lemma ✓. But [[a,b]] is uIcc notation — after rw, hs : s.re ∈ [[(dogZ T).re, (dogW XR U).re]] ∧ ... — then rewrite the corner re/ims. `[[a,b]]` is `Set.uIcc a b` (notation in Mathlib: [[a, b]] = uIcc a b with open scoped Interval). Then `rw [Set.uIcc_of_le hXR]` etc.\n\nActually cleaner: \n```\n intro s hs\n have hs' := hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs'\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs'\n exact (Jlag_differentiableAt_dogleg hs'.1.1 (by linarith [hs'.2.1])).differentiableWithinAt\n```\nWait — hs'.1.1 : 3 ≤ s.re ✓; hs'.2.1 : T ≤ s.im, need 0 < s.im: linarith [hT, hs'.2.1] ✓.\n\nBut does `rw [dogZ_re, ...]` work inside hs'? dogZ_re (T) : (dogZ T).re = 3 — rewriting (dogZ T).re → 3 ✓. But after `rw [Rectangle]`, the term is [[(dogZ T).re, (dogW XR U).re]] ×ℂ ... — rw [Complex.mem_reProdIm] turns membership into the ∧ ✓ then rw [dogZ_re] rewrites (dogZ T).re ✓ ✓.\n\nOK. Now also the `unfold RectangleIntegral at h0` step in upper_right_horizontal_eq_dogleg: RectangleIntegral is a def in Zeta23 — unfold works, or rw [RectangleIntegral]. LiPrincipal used `rw [RectangleIntegral', RectangleIntegral', ...]` — those are abbrevs (reducible). For the def RectangleIntegral, `unfold RectangleIntegral at h0` should work (LiSides or others used `unfold` for defs? kFun was unfolded via `unfold kFun` in LiContour? It used `simp [kFun]`? Whatever — `unfold RectangleIntegral at h0` is standard).\n\nThen h0 : HIntegral (Jlag n) (dogZ T).re (dogW XR U).re (dogZ T).im − HIntegral (Jlag n) (dogZ T).re (dogW XR U).re (dogW XR U).im + VIntegral (Jlag n) (dogW XR U).re (dogZ T).im (dogW XR U).im − VIntegral (Jlag n) (dogZ T).re (dogZ T).im (dogW XR U).im = 0. rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0 normalizes all corners ✓ then linear_combination h0.\n\nWait — the VIntegral args: VIntegral f x y₁ y₂ with the rectangle's V f w.re z.im w.im: x = (dogW).re = XR, y₁ = (dogZ).im = T, y₂ = (dogW).im = U ✓ → VIntegral (Jlag n) XR T U ✓; and −V f z.re z.im w.im: −VIntegral (Jlag n) 3 T U ✓. The goal: H 3 XR T = H 3 XR U − V XR T U + V 3 T U. From h0: H_low − H_high + V_right − V_left = 0. linear_combination h0: goal − h0 = 0: (H_low − (H_high − V_right + V_left)) − (H_low − H_high + V_right − V_left) = 0 ✓.\n\nOne risk: the dogZ/dogW def form ((3:ℝ):ℂ) + (T:ℝ)*I vs rectW's ((2√n:ℝ):ℂ) + T*I — same pattern ✓ simp [dogZ] should prove dogZ_re like simp [rectW] proved rectW_re ✓.\n\nNow write the file and build. Also need to check `riemannZeta_ne_zero_of_one_lt_re` visibility: it's Mathlib's root lemma (in Dirichlet.lean, probably root namespace). LiDogLeg imports Mathlib + LiSides + LiTightR ✓.\n\nAlso `rintro rfl; simp at him` for s ≠ 1: him : 0 < s.im becomes 0 < (1:ℂ).im — simp: Complex.one_im : (1:ℂ).im = 0 — simp at him derives 0 < 0 → closes by lt_irrefl? simp should close it (simp at him turns it into False and closes the goal if him reduces to False ✓ standard pattern).\n\nWrite LiDogLeg.lean now.","signature":""},{"type":"text","text":"All API confirmed. Writing `LiDogLeg.lean` (DL-1)."},{"type":"tool_use","id":"Write_175","name":"Write","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","content":"/-\nNguyenRH1/LiDogLeg.lean — ii′-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 §3.1–3.2): on the dog-leg rectangle [3, X_R]×[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s−1))ⁿ−1 · (−ζ′/ζ(s)) is\nholomorphic UNCONDITIONALLY (s ≠ 1 since im > 0; ζ s ≠ 0 for re s ≥ 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n— NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3→X_R, T) = H(3→X_R, U) − V(X_R, T→U) + V(3, T→U)\n(the upper right tail = the high horizontal − the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) — the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 §3.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : ℝ) : ℂ := ((3 : ℝ) : ℂ) + (T : ℝ) * Complex.I\ndef dogW (XR U : ℝ) : ℂ := ((XR : ℝ) : ℂ) + (U : ℝ) * Complex.I\n\nlemma dogZ_re (T : ℝ) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : ℝ) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : ℝ) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : ℝ) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 ≤ re, 0 < im:\nζ is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL — the Euler-product region) and s ≠ 1 (im ≠ 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : ℕ} {s : ℂ}\n (hre : 3 ≤ s.re) (him : 0 < s.im) :\n DifferentiableAt ℂ (Jlag n) s := by\n apply Jlag_differentiableAt\n · rintro rfl\n simp at him\n · exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]×[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : ℕ} {T U XR : ℝ}\n (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free — the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : ℕ} {T U XR : ℝ}\n (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2πi)⁻¹-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : ℕ} {T U XR : ℝ}\n (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 §3.2 (★), the\ncapstone for ii′-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : ℕ} {T U XR : ℝ}\n (hT : 0 < T) (hTU : T ≤ U) (hXR : 3 ≤ XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : ℕ) (s : ℂ) :\n kFun n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_div, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s̄) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : ℕ) {s : ℂ} (hs : s ≠ 1) :\n Jlag n ((starRingEnd ℂ) s) = (starRingEnd ℂ) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd ℂ) s) =\n (starRingEnd ℂ) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one, iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1, map_mul, map_neg, map_div]\n\nend NguyenRH1\n\nend\n"},"extra_content":null}]