← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (7951 chars)
DL-3 committed (6eaf531). Now DL-4: the far-right vertical drop. Components:
‖VIntegral (Jlag n) XR T U‖ ≤ (U−T)·(e^{√n/2}+1)·2^{−(XR−2)}·dirichletC2 for XR = 2√n, 0 < T ≤ U.
Pieces:
1. Kernel at w = XR+it: kFun n w = (w/(w−1))ⁿ − 1 with w−1 = (XR−1)+it, re(w−1) = XR−1 = 2√n−1... — the ii′-4 lemma `kFun_shift_norm_le_exp_sqrt_half_add_one (hn : 0 < n) (hσ : 2√n ≤ s.re)` : ‖kFun n (s+1)‖ ≤ e^{√n/2}+1 — with s+1 = w, s = w−1, s.re = XR−1: need 2√n ≤ XR−1 = 2√n−1?? — that's 2√n ≤ 2√n−1 — FALSE!! Hmm — the ii′-4 lemma bounds kFun n (s+1) for 2√n ≤ s.re — the right vertical of the MAIN rectangle is at re w = 2√n, so s = w−1 has re = 2√n−1 < 2√n — the lemma does NOT apply!! Let me check how the I_I bound was planned (D-071 §4.4: "I_I (right vertical σ₁ = 2√n): |ζ′/ζ| ≤ 2^{−(σ₁−2)}·dirichletC2; kernel ≤ e^{√n/2}+1 (kFun_shift_norm_le_exp_sqrt_half_add_one ✓)"). So D-071 intended that lemma for I_I — with s+1 = w where s.re = 2√n−1... — hmm, the lemma's hypothesis is hσ : 2√n ≤ s.re and conclusion ‖kFun n (s+1)‖ ≤ e^{√n/2}+1. For I_I at w = 2√n+it: s+1 = w ⟹ s = w−1 = (2√n−1)+it: s.re = 2√n−1 — does 2√n ≤ 2√n−1? NO. So the ii′-4 lemma does NOT cover I_I at re w = 2√n!?
Let me look at the lemma's proof to understand its actual content: kFun_shift_norm_le_exp_sqrt_half_add_one {n s} (hn : 0 < n) (hσ : 2√n ≤ s.re) : ‖kFun n (s + 1)‖ ≤ Real.exp (√n/2) + 1. The proof: |1+1/s| ≤ 1 + 1/(2√n) (since re s ≥ 2√n: (re s+1)/normSq s ≤ ... (σ+1)/(σ²+t²) ≤ 1/(2√n) for σ ≥ 2√n) — the exponent n/(2√n) = √n/2 ✓. For the application s+1 = w at re w = 2√n: s = w−1, s.re = 2√n−1 — the bound |1+1/s| ≤ 1+1/(2√n) needs re s ≥ 2√n... — at s.re = 2√n−1: (σ+1)/(σ²+t²) = 2√n/((2√n−1)²+t²) — is that ≤ 1/(2√n)?? — 2√n/((2√n−1)²+t²) ≤ 1/(2√n) ⟺ (2√n)² ≤ (2√n−1)²+t² ⟺ 4n ≤ 4n−4√n+1+t² ⟺ 4√n ≤ 1+t² ✓ for t ≥ 1 (t = T ≥ √n ≥ 316 ✓✓). So the |1+1/s| ≤ 1+1/(2√n) bound HOLDS at s = w−1 with t ≥ ~2√n^{1/2}·... — via a slightly different computation than the lemma's hypothesis.
So for DL-4 I need a small variant lemma: ‖kFun n ((2√n)+it)‖ ≤ e^{√n/2}+1 for t² ≥ 4√n−1-ish... — cleaner: prove the V_right kernel bound directly with the norm_one_add_one_div_le core:
‖1+1/((XR−1)+it)‖ ≤ 1 + (XR)/((XR−1)²+t²) ≤ 1 + 1/(2√n) — the last step needs (XR)/((XR−1)²+t²) ≤ 1/(2√n) ⟺ 2√n·2√n ≤ (2√n−1)²+t² ⟺ 4n ≤ 4n−4√n+1+t² ⟺ 4√n−1 ≤ t². With t ≥ T ≥ √n: t² ≥ n ≥ 4√n−1 ⟺ n ≥ 4√n−1 ⟺ √n·(√n−4) ≥ −1 ✓ for √n ≥ 4 (n ≥ 16; our n ≥ 10⁵ ✓). So:
‖kFun n w‖ ≤ ‖(1+1/(w−1))ⁿ‖+1 = ‖1+1/(w−1)‖ⁿ+1 ≤ (1+1/(2√n))ⁿ+1 ≤ e^{n/(2√n)}+1 = e^{√n/2}+1 ✓.
2. Zeta: ‖ζ′/ζ(XR+it)‖ ≤ 2^{−(XR−2)}·dirichletC2 (DL-3a's lemma with σ := XR ≥ 2 ✓ — wait, norm_logDeriv_zeta_le_two_pow takes {σ t : ℝ} (hσ : 2 ≤ σ) — at σ = XR = 2√n ≥ 632 ✓).
3. The product: ‖Jlag n (XR+it)‖ ≤ (e^{√n/2}+1)·2^{−(XR−2)}·dirichletC2 — then the interval integral: ‖VIntegral‖ ≤ (U−T)·that.
So DL-4's structure:
- `kFun_right_vertical_norm_le_exp_sqrt_half_add_one` {n t} (hn : 0 < n) (ht : 4 * Real.sqrt n - 1 ≤ t ^ 2)... — hmm — let me state it with the condition 2 ≤ √n (or n ≥ 16): for n ≥ 16 and any t with t² ≥ n: ‖kFun n ((2√n:ℝ)+t·I)‖ ≤ e^{√n/2}+1. Hmm — the t-condition: (XR)/((XR−1)²+t²) ≤ 1/(2√n) needs t² ≥ 4√n−1. With t ≥ T (T ≥ √n... in DL-5's application t ranges over [T, U] with T ≥ √n): t² ≥ n. So the hypothesis (hn : 16 ≤ n) + (ht : (n:ℝ) ≤ t²) suffices: t² ≥ n ≥ 4√n−1 ⟺ n+1 ≥ 4√n ⟺ (√n−2)² ≥ 3 ✓ for √n ≥ 4 ⟺ n ≥ 16 ✓ (16: (4−2)² = 4 ≥ 3 ✓; n = 16: 4·4−1 = 15 ≤ 16 ✓).
Let me write:
```
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
-- w−1 = (2√n−1)+it; ‖1+1/(w−1)‖ ≤ 1+(2√n)/((2√n−1)²+t²) ≤ 1+1/(2√n)
```
The norm computation: ‖1+1/(w−1)‖ ≤ 1+(re(w−1)+1)/normSq(w−1) = 1+(2√n)/((2√n−1)²+t²) via norm_one_add_one_div_le (needs w−1 ≠ 0 ✓ im = t, t² ≥ n ≥ 16 → t ≠ 0 ✓).
(2√n)/((2√n−1)²+t²) ≤ 1/(2√n) ⟺ (2√n)·(2√n) ≤ (2√n−1)²+t² ⟺ 4n ≤ (2√n−1)²+t²: (2√n−1)² = 4n−4√n+1: 4n ≤ 4n−4√n+1+t² ⟺ 4√n−1 ≤ t² ✓ (from ht + hn: t² ≥ n ≥ 4√n−1 ⟺ n ≥ 4√n−1: n+1 ≥ 4√n ⟺ (n+1)² ≥ 16n ⟺ n²−14n+1 ≥ 0 ⟺ (n−7)² ≥ 48 ✓ for n ≥ 16: (16−7)² = 81 ≥ 48 ✓ — need to show n ≥ 4√n−1 from 16 ≤ n: 4√n ≤ n+1 ⟺ 16n ≤ (n+1)² ⟺ 0 ≤ n²−14n+1 — for n ≥ 14+... n²−14n+1 = (n−7)²−48: n ≥ 16 ⟹ (n−7)² ≥ 81 > 48 ✓ — the Lean proof: nlinarith with √-bounds (Real.sqrt_le_sqrt, Real.sq_sqrt).
Then: ‖(1+1/(w−1))ⁿ‖ ≤ (1+1/(2√n))ⁿ ≤ e^{n·(1/(2√n))} = e^{√n/2} ✓ (the exp chain like the other kernel lemmas).
Then the V_right assembly:
```
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
```
same structure as vIntegral_Jlag_three_norm_le (the norm_smul + norm_integral_le_of_norm_le_const + pointwise product bound).
And finally the VRightBound ≤ IIMaj/4 accounting? — the IIMaj def: IIMaj n = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}. My V_right bound: (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 with U−T ≤ (√n+1)/2 (DL-5's T ∈ [√n, √n+1], U = 1.5T): ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (dirichletC2 ≤ 1) vs IIMaj/4 = (1/4)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = ((√n+1)/2)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — so V_right ≤ (1/0.57)·IIMaj/4·... = IIMaj/4·(1/0.57)?? — wait: my bound has dirichletC2 ≤ 1 vs IIMaj/4's 0.57 — mine is (1/0.57)× FATTER: V_right ≤ IIMaj/(4·0.57)·... hmm: V_right ≤ ((√n+1)/2)(e+1)2^{−X}·1 and IIMaj/4 = ((√n+1)/2)(e+1)2^{−X}·0.57 — so V_right ≤ IIMaj/4 · (1/0.57)?? NO: my bound (with 1) is LARGER than IIMaj/4 (with 0.57): V_right ≤ B where B = ((√n+1)/2)(e^{√n/2}+1)2^{−(2√n−2)} and IIMaj/4 = 0.57·B: so B = IIMaj/(4·0.57) > IIMaj/4. To charge V_right ≤ IIMaj/4 I'd need dirichletC2 ≤ 0.57 — the same infeasibility! So charge VRightBound := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} (= IIMaj/(4·0.57) = IIMaj/2.28) — or just charge it as its own explicit form; it's negligible either way. For the fold, VRightBound(n) := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} — which is (1/4)·IIMaj(n)/0.57 ≈ 0.438·IIMaj(n) — tiny. In the E-034 fold, DogLegRight = VLeftBound + HHIGH + IIMaj/4 — the IIMaj/4 slot stays (it's bigger than my Lean VRightBound by 1.75× ✓ so the Lean bound V_right ≤ ((√n+1)/2)(e+1)2^{−X} ≤ IIMaj/4 is FALSE... wait: ((√n+1)/2)(e+1)2^{−X}·1 vs IIMaj/4 = 0.57·((√n+1)/2)(e+1)2^{−X}: the Lean bound (with dirichletC2 ≤ 1) is 1/0.57 ≈ 1.75× IIMaj/4. So charging V_right ≤ IIMaj/4 is NOT provable with dirichletC2 ≤ 1!! Need to charge VRightBound = ((√n+1)/2)(e^{√n/2}+1)2^{−(2√n−2)} = IIMaj(n)/(4·0.57) — i.e., charge VRightBound := IIMaj(n)/2 (which is bigger: IIMaj/2 = 0.5·B·... — IIMaj/2 = ((√n+1)·1)·(e+1)·0.57·2^{−X} vs my B = ((√n+1)/2)(e+1)·1·2^{−X}: IIMaj/2 / B = 2·0.57 = 1.14 > 1 ✓ so V_right ≤ IIMaj/2 provable ✓). So charge VRightBound := IIMaj(n)/2 — still negligible (IIMaj ~1e-105 at 8e4) ✓ fold indifferent ✓.
Hmm wait — let me recompute cleanly:
B := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (the Lean-provable bound with dirichletC2 ≤ 1).
IIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.
B/IIMaj = (1/2)/(2·0.57) = (1/2)/(1.14) = 0.4386. So B = 0.4386·IIMaj < IIMaj/2 = 0.5·IIMaj ✓. And B > IIMaj/4 = 0.25·IIMaj ✗. So charge VRightBound := IIMaj/2 ✓ (provable: B ≤ IIMaj/2 ⟺ 0.4386 ≤ 0.5 ✓ — the Lean proof: B = ((√n+1)/2)(e+1)2^{−X}·dirichletC2 ≤ ((√n+1)/2)(e+1)2^{−X}·1 ≤ (1/2)·IIMaj = ((√n+1))(e+1)·0.57·2^{−X} ⟺ 1/2 ≤ 2·0.57 = 1.14 ✓ trivial).
So DL-4 deliverables:
1. kFun_right_vertical_norm_le_exp_sqrt_half_add_one (kernel e^{√n/2}+1 at re = 2√n).
2. vIntegral_Jlag_right_norm_le : ‖VIntegral (Jlag n) (2√n) T U‖ ≤ (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2.
3. (the IIMaj/2 accounting goes in DL-5's total assembly.)
Let me write DL-4. It's essentially the DL-2 pattern with the new kernel lemma. ~150 lines.
DL-3 committed (`6eaf531`). Now **DL-4** — the far-right drop. The kernel lemma needs a small variant at re = 2√n (the ii′-4 lemma's hypothesis is at re ≥ 2√n for s, i.e. re w ≥ 2√n+1 — so I prove the w-form directly). Writing it.
tool: TodoWrite ok
input
{
"todos": [
{
"content": "DL-4a: kernel lemma \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1 for n \u2265 16, t\u00b2 \u2265 n",
"status": "in_progress",
"activeForm": "Proving the right-vertical kernel bound"
},
{
"content": "DL-4b: vIntegral_Jlag_right_norm_le \u2264 (U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 + build + audit + commit",
"status": "pending",
"activeForm": "Proving the V_right assembly"
}
]
}
result 2026-08-26 07:28:03Z → 2026-08-26 07:28:03Z
{
"oldTodos": [
"content='DL-3a: zeta halving bound \u2016\u03b6\u2032/\u03b6(\u03c3+iU)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 (termwise LSeries comparison)' status='in_progress' active_form='Proving the zeta halving bound'",
"content='DL-3b: kernel envelope \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264 e^{(4/9)\u03c3} for \u03c3 \u2265 3, U\u00b2 \u2265 (9/4)n' status='pending' active_form='Proving the kernel envelope'",
"content='DL-3c: product envelope \u2016Jlag\u2016 \u2264 (4e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3})\u00b7dirichletC2 + certified constants (c \u2265 0.2487, e^{4/3} \u2264 3.8073)' status='pending' active_form='Building the product envelope'",
"content='DL-3d: integrals (FTC for e^{\u2212c\u03c3} and 2^{\u2212\u03c3}) + capstone \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 8.38 + build + audit + commit' status='pending' active_form='Assembling the H_high capstone'"
],
"newTodos": [
"content='DL-4a: kernel lemma \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1 for n \u2265 16, t\u00b2 \u2265 n' status='in_progress' active_form='Proving the right-vertical kernel bound'",
"content='DL-4b: vIntegral_Jlag_right_norm_le \u2264 (U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 + build + audit + commit' status='pending' active_form='Proving the V_right assembly'"
],
"cleared": false
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 6. The far-right vertical drop (DL-4, D-074 \u00a78) -/\n\n/-- **Kernel at the far-right vertical** (D-074 \u00a78): for n \u2265 16 and\nt\u00b2 \u2265 n, \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2}+1. (The ii\u2032-4 lemma\n`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s \u2265 2\u221an, i.e.\nre w \u2265 2\u221an+1 \u2014 this is the w = 2\u221an variant: |1+1/(w\u22121)| \u2264\n1+(2\u221an)/((2\u221an\u22121)\u00b2+t\u00b2) \u2264 1+1/(2\u221an) since 4\u221an\u22121 \u2264 t\u00b2.) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : \u2115} {t : \u211d}\n (hn : 16 \u2264 n) (ht : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n have hw1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 =\n ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I := by\n push_cast\n ring\n have hs0 : ((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I \u2260 0 := by\n intro h\n have him : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = 0 := by\n rw [h]; simp\n simp at him\n have ht0 : t = 0 := by\n have h1 : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).im = t := by simp\n linarith\n rw [ht0] at ht\n nlinarith [hnR]\n have hle := norm_one_add_one_div_le hs0\n have hre : (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1 =\n 2 * Real.sqrt (n : \u211d) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n ring\n have hns : Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) =\n (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hkey : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hns]\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n have h1 : 4 * Real.sqrt (n : \u211d) - 1 \u2264 t ^ 2 := by\n have h2 : 4 * Real.sqrt (n : \u211d) \u2264 (n : \u211d) + 1 := by\n have h3 : (4 * Real.sqrt (n : \u211d)) ^ 2 \u2264 ((n : \u211d) + 1) ^ 2 := by\n rw [show (4 * Real.sqrt (n : \u211d)) ^ 2 = 16 * (Real.sqrt (n : \u211d) ^ 2) by ring, hsqn]\n nlinarith [sq_nonneg ((n : \u211d) - 1), hnR]\n nlinarith [hsq]\n nlinarith [ht, h2]\n rw [show (2 * Real.sqrt (n : \u211d) - 1) ^ 2 + t ^ 2 =\n 4 * (Real.sqrt (n : \u211d) ^ 2) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 by ring, hsqn]\n have h4 : (0 : \u211d) < 4 * (n : \u211d) - 4 * Real.sqrt (n : \u211d) + 1 + t ^ 2 := by\n nlinarith [ht, sq_nonneg t, hsq]\n rw [div_le_div_iff_of_pos_left hsq h4 (by positivity)]\n nlinarith [h1, ht, hsq]\n have hstep : 1 + ((((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I).re + 1) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 + 1 / (2 * Real.sqrt (n : \u211d)) := by\n rw [hre]\n have h1 : (2 * Real.sqrt (n : \u211d)) /\n Complex.normSq (((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I) \u2264\n 1 / (2 * Real.sqrt (n : \u211d)) := hkey\n linarith [h1]\n have hpow1 : \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n \u2264\n (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n have hpow2 : (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2) := by\n calc (1 + 1 / (2 * Real.sqrt (n : \u211d))) ^ n\n \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d)))) ^ n := by\n have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d)))\n exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d)))) :=\n (Real.exp_nat_mul _ n).symm\n _ = Real.exp (Real.sqrt (n : \u211d) / 2) := by\n congr 1\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n field_simp [hsq.ne']\n nlinarith [hsqn]\n unfold kFun\n rw [hw1]\n calc \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = \u2016(1 + 1/(((2 * Real.sqrt (n : \u211d) - 1) : \u211d) + t * Complex.I))\u2016 ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2) + 1 := by linarith [hpow1.trans hpow2]\n\n/-- **The far-right vertical drop** (D-074 \u00a78 V_right): for n \u2265 16,\n0 < T \u2264 U, T\u00b2 \u2265 n, \u2016VIntegral (Jlag n) (2\u221an) T U\u2016 \u2264\n(U\u2212T)\u00b7(e^{\u221an/2}+1)\u00b72^{\u2212(2\u221an\u22122)}\u00b7dirichletC2 \u2014 exponentially tiny. -/\ntheorem vIntegral_Jlag_right_norm_le {n : \u2115} {T U : \u211d}\n (hn : 16 \u2264 n) (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 \u2264\n (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n have hnorm : \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) T U\u2016 =\n \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2\n have h2 := norm_logDeriv_zeta_le_two_pow\n (show (2 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) by\n have hnR : (16 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq : (4 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by linarith)]; norm_num\n linarith) (t := t)\n have hnorm3 : \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have hint : \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) *\n ((2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) * dirichletC2) := by ring\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"DL-3 committed (6eaf531). Now DL-4: the far-right vertical drop. Components:\n\n‖VIntegral (Jlag n) XR T U‖ ≤ (U−T)·(e^{√n/2}+1)·2^{−(XR−2)}·dirichletC2 for XR = 2√n, 0 < T ≤ U.\n\nPieces:\n1. Kernel at w = XR+it: kFun n w = (w/(w−1))ⁿ − 1 with w−1 = (XR−1)+it, re(w−1) = XR−1 = 2√n−1... — the ii′-4 lemma `kFun_shift_norm_le_exp_sqrt_half_add_one (hn : 0 < n) (hσ : 2√n ≤ s.re)` : ‖kFun n (s+1)‖ ≤ e^{√n/2}+1 — with s+1 = w, s = w−1, s.re = XR−1: need 2√n ≤ XR−1 = 2√n−1?? — that's 2√n ≤ 2√n−1 — FALSE!! Hmm — the ii′-4 lemma bounds kFun n (s+1) for 2√n ≤ s.re — the right vertical of the MAIN rectangle is at re w = 2√n, so s = w−1 has re = 2√n−1 < 2√n — the lemma does NOT apply!! Let me check how the I_I bound was planned (D-071 §4.4: \"I_I (right vertical σ₁ = 2√n): |ζ′/ζ| ≤ 2^{−(σ₁−2)}·dirichletC2; kernel ≤ e^{√n/2}+1 (kFun_shift_norm_le_exp_sqrt_half_add_one ✓)\"). So D-071 intended that lemma for I_I — with s+1 = w where s.re = 2√n−1... — hmm, the lemma's hypothesis is hσ : 2√n ≤ s.re and conclusion ‖kFun n (s+1)‖ ≤ e^{√n/2}+1. For I_I at w = 2√n+it: s+1 = w ⟹ s = w−1 = (2√n−1)+it: s.re = 2√n−1 — does 2√n ≤ 2√n−1? NO. So the ii′-4 lemma does NOT cover I_I at re w = 2√n!?\n\nLet me look at the lemma's proof to understand its actual content: kFun_shift_norm_le_exp_sqrt_half_add_one {n s} (hn : 0 < n) (hσ : 2√n ≤ s.re) : ‖kFun n (s + 1)‖ ≤ Real.exp (√n/2) + 1. The proof: |1+1/s| ≤ 1 + 1/(2√n) (since re s ≥ 2√n: (re s+1)/normSq s ≤ ... (σ+1)/(σ²+t²) ≤ 1/(2√n) for σ ≥ 2√n) — the exponent n/(2√n) = √n/2 ✓. For the application s+1 = w at re w = 2√n: s = w−1, s.re = 2√n−1 — the bound |1+1/s| ≤ 1+1/(2√n) needs re s ≥ 2√n... — at s.re = 2√n−1: (σ+1)/(σ²+t²) = 2√n/((2√n−1)²+t²) — is that ≤ 1/(2√n)?? — 2√n/((2√n−1)²+t²) ≤ 1/(2√n) ⟺ (2√n)² ≤ (2√n−1)²+t² ⟺ 4n ≤ 4n−4√n+1+t² ⟺ 4√n ≤ 1+t² ✓ for t ≥ 1 (t = T ≥ √n ≥ 316 ✓✓). So the |1+1/s| ≤ 1+1/(2√n) bound HOLDS at s = w−1 with t ≥ ~2√n^{1/2}·... — via a slightly different computation than the lemma's hypothesis. \n\nSo for DL-4 I need a small variant lemma: ‖kFun n ((2√n)+it)‖ ≤ e^{√n/2}+1 for t² ≥ 4√n−1-ish... — cleaner: prove the V_right kernel bound directly with the norm_one_add_one_div_le core:\n‖1+1/((XR−1)+it)‖ ≤ 1 + (XR)/((XR−1)²+t²) ≤ 1 + 1/(2√n) — the last step needs (XR)/((XR−1)²+t²) ≤ 1/(2√n) ⟺ 2√n·2√n ≤ (2√n−1)²+t² ⟺ 4n ≤ 4n−4√n+1+t² ⟺ 4√n−1 ≤ t². With t ≥ T ≥ √n: t² ≥ n ≥ 4√n−1 ⟺ n ≥ 4√n−1 ⟺ √n·(√n−4) ≥ −1 ✓ for √n ≥ 4 (n ≥ 16; our n ≥ 10⁵ ✓). So:\n\n‖kFun n w‖ ≤ ‖(1+1/(w−1))ⁿ‖+1 = ‖1+1/(w−1)‖ⁿ+1 ≤ (1+1/(2√n))ⁿ+1 ≤ e^{n/(2√n)}+1 = e^{√n/2}+1 ✓.\n\n2. Zeta: ‖ζ′/ζ(XR+it)‖ ≤ 2^{−(XR−2)}·dirichletC2 (DL-3a's lemma with σ := XR ≥ 2 ✓ — wait, norm_logDeriv_zeta_le_two_pow takes {σ t : ℝ} (hσ : 2 ≤ σ) — at σ = XR = 2√n ≥ 632 ✓).\n\n3. The product: ‖Jlag n (XR+it)‖ ≤ (e^{√n/2}+1)·2^{−(XR−2)}·dirichletC2 — then the interval integral: ‖VIntegral‖ ≤ (U−T)·that.\n\nSo DL-4's structure:\n- `kFun_right_vertical_norm_le_exp_sqrt_half_add_one` {n t} (hn : 0 < n) (ht : 4 * Real.sqrt n - 1 ≤ t ^ 2)... — hmm — let me state it with the condition 2 ≤ √n (or n ≥ 16): for n ≥ 16 and any t with t² ≥ n: ‖kFun n ((2√n:ℝ)+t·I)‖ ≤ e^{√n/2}+1. Hmm — the t-condition: (XR)/((XR−1)²+t²) ≤ 1/(2√n) needs t² ≥ 4√n−1. With t ≥ T (T ≥ √n... in DL-5's application t ranges over [T, U] with T ≥ √n): t² ≥ n. So the hypothesis (hn : 16 ≤ n) + (ht : (n:ℝ) ≤ t²) suffices: t² ≥ n ≥ 4√n−1 ⟺ n+1 ≥ 4√n ⟺ (√n−2)² ≥ 3 ✓ for √n ≥ 4 ⟺ n ≥ 16 ✓ (16: (4−2)² = 4 ≥ 3 ✓; n = 16: 4·4−1 = 15 ≤ 16 ✓).\n\nLet me write:\n```\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : ℕ} {t : ℝ}\n (hn : 16 ≤ n) (ht : (n : ℝ) ≤ t ^ 2) :\n ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by\n -- w−1 = (2√n−1)+it; ‖1+1/(w−1)‖ ≤ 1+(2√n)/((2√n−1)²+t²) ≤ 1+1/(2√n)\n```\nThe norm computation: ‖1+1/(w−1)‖ ≤ 1+(re(w−1)+1)/normSq(w−1) = 1+(2√n)/((2√n−1)²+t²) via norm_one_add_one_div_le (needs w−1 ≠ 0 ✓ im = t, t² ≥ n ≥ 16 → t ≠ 0 ✓).\n(2√n)/((2√n−1)²+t²) ≤ 1/(2√n) ⟺ (2√n)·(2√n) ≤ (2√n−1)²+t² ⟺ 4n ≤ (2√n−1)²+t²: (2√n−1)² = 4n−4√n+1: 4n ≤ 4n−4√n+1+t² ⟺ 4√n−1 ≤ t² ✓ (from ht + hn: t² ≥ n ≥ 4√n−1 ⟺ n ≥ 4√n−1: n+1 ≥ 4√n ⟺ (n+1)² ≥ 16n ⟺ n²−14n+1 ≥ 0 ⟺ (n−7)² ≥ 48 ✓ for n ≥ 16: (16−7)² = 81 ≥ 48 ✓ — need to show n ≥ 4√n−1 from 16 ≤ n: 4√n ≤ n+1 ⟺ 16n ≤ (n+1)² ⟺ 0 ≤ n²−14n+1 — for n ≥ 14+... n²−14n+1 = (n−7)²−48: n ≥ 16 ⟹ (n−7)² ≥ 81 > 48 ✓ — the Lean proof: nlinarith with √-bounds (Real.sqrt_le_sqrt, Real.sq_sqrt).\n\nThen: ‖(1+1/(w−1))ⁿ‖ ≤ (1+1/(2√n))ⁿ ≤ e^{n·(1/(2√n))} = e^{√n/2} ✓ (the exp chain like the other kernel lemmas).\n\nThen the V_right assembly:\n```\ntheorem vIntegral_Jlag_right_norm_le {n : ℕ} {T U : ℝ}\n (hn : 16 ≤ n) (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ ≤\n (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by\n```\nsame structure as vIntegral_Jlag_three_norm_le (the norm_smul + norm_integral_le_of_norm_le_const + pointwise product bound).\n\nAnd finally the VRightBound ≤ IIMaj/4 accounting? — the IIMaj def: IIMaj n = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}. My V_right bound: (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 with U−T ≤ (√n+1)/2 (DL-5's T ∈ [√n, √n+1], U = 1.5T): ≤ ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (dirichletC2 ≤ 1) vs IIMaj/4 = (1/4)·2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)} = ((√n+1)/2)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)} — so V_right ≤ (1/0.57)·IIMaj/4·... = IIMaj/4·(1/0.57)?? — wait: my bound has dirichletC2 ≤ 1 vs IIMaj/4's 0.57 — mine is (1/0.57)× FATTER: V_right ≤ IIMaj/(4·0.57)·... hmm: V_right ≤ ((√n+1)/2)(e+1)2^{−X}·1 and IIMaj/4 = ((√n+1)/2)(e+1)2^{−X}·0.57 — so V_right ≤ IIMaj/4 · (1/0.57)?? NO: my bound (with 1) is LARGER than IIMaj/4 (with 0.57): V_right ≤ B where B = ((√n+1)/2)(e^{√n/2}+1)2^{−(2√n−2)} and IIMaj/4 = 0.57·B: so B = IIMaj/(4·0.57) > IIMaj/4. To charge V_right ≤ IIMaj/4 I'd need dirichletC2 ≤ 0.57 — the same infeasibility! So charge VRightBound := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} (= IIMaj/(4·0.57) = IIMaj/2.28) — or just charge it as its own explicit form; it's negligible either way. For the fold, VRightBound(n) := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)} — which is (1/4)·IIMaj(n)/0.57 ≈ 0.438·IIMaj(n) — tiny. In the E-034 fold, DogLegRight = VLeftBound + HHIGH + IIMaj/4 — the IIMaj/4 slot stays (it's bigger than my Lean VRightBound by 1.75× ✓ so the Lean bound V_right ≤ ((√n+1)/2)(e+1)2^{−X} ≤ IIMaj/4 is FALSE... wait: ((√n+1)/2)(e+1)2^{−X}·1 vs IIMaj/4 = 0.57·((√n+1)/2)(e+1)2^{−X}: the Lean bound (with dirichletC2 ≤ 1) is 1/0.57 ≈ 1.75× IIMaj/4. So charging V_right ≤ IIMaj/4 is NOT provable with dirichletC2 ≤ 1!! Need to charge VRightBound = ((√n+1)/2)(e^{√n/2}+1)2^{−(2√n−2)} = IIMaj(n)/(4·0.57) — i.e., charge VRightBound := IIMaj(n)/2 (which is bigger: IIMaj/2 = 0.5·B·... — IIMaj/2 = ((√n+1)·1)·(e+1)·0.57·2^{−X} vs my B = ((√n+1)/2)(e+1)·1·2^{−X}: IIMaj/2 / B = 2·0.57 = 1.14 > 1 ✓ so V_right ≤ IIMaj/2 provable ✓). So charge VRightBound := IIMaj(n)/2 — still negligible (IIMaj ~1e-105 at 8e4) ✓ fold indifferent ✓.\n\nHmm wait — let me recompute cleanly: \nB := ((√n+1)/2)·(e^{√n/2}+1)·2^{−(2√n−2)}·1 (the Lean-provable bound with dirichletC2 ≤ 1).\nIIMaj(n) = 2(√n+1)(e^{√n/2}+1)·0.57·2^{−(2√n−2)}.\nB/IIMaj = (1/2)/(2·0.57) = (1/2)/(1.14) = 0.4386. So B = 0.4386·IIMaj < IIMaj/2 = 0.5·IIMaj ✓. And B > IIMaj/4 = 0.25·IIMaj ✗. So charge VRightBound := IIMaj/2 ✓ (provable: B ≤ IIMaj/2 ⟺ 0.4386 ≤ 0.5 ✓ — the Lean proof: B = ((√n+1)/2)(e+1)2^{−X}·dirichletC2 ≤ ((√n+1)/2)(e+1)2^{−X}·1 ≤ (1/2)·IIMaj = ((√n+1))(e+1)·0.57·2^{−X} ⟺ 1/2 ≤ 2·0.57 = 1.14 ✓ trivial).\n\nSo DL-4 deliverables:\n1. kFun_right_vertical_norm_le_exp_sqrt_half_add_one (kernel e^{√n/2}+1 at re = 2√n).\n2. vIntegral_Jlag_right_norm_le : ‖VIntegral (Jlag n) (2√n) T U‖ ≤ (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2.\n3. (the IIMaj/2 accounting goes in DL-5's total assembly.)\n\nLet me write DL-4. It's essentially the DL-2 pattern with the new kernel lemma. ~150 lines.","signature":""},{"type":"text","text":"DL-3 committed (`6eaf531`). Now **DL-4** — the far-right drop. The kernel lemma needs a small variant at re = 2√n (the ii′-4 lemma's hypothesis is at re ≥ 2√n for s, i.e. re w ≥ 2√n+1 — so I prove the w-form directly). Writing it."},{"type":"tool_use","id":"TodoWrite_340","name":"TodoWrite","input":{"todos":[{"content":"DL-4a: kernel lemma ‖kFun n (2√n+it)‖ ≤ e^{√n/2}+1 for n ≥ 16, t² ≥ n","status":"in_progress","activeForm":"Proving the right-vertical kernel bound"},{"content":"DL-4b: vIntegral_Jlag_right_norm_le ≤ (U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 + build + audit + commit","status":"pending","activeForm":"Proving the V_right assembly"}]},"extra_content":null},{"type":"tool_use","id":"Edit_341","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 6. The far-right vertical drop (DL-4, D-074 §8) -/\n\n/-- **Kernel at the far-right vertical** (D-074 §8): for n ≥ 16 and\nt² ≥ n, ‖kFun n (2√n+it)‖ ≤ e^{√n/2}+1. (The ii′-4 lemma\n`kFun_shift_norm_le_exp_sqrt_half_add_one` takes re s ≥ 2√n, i.e.\nre w ≥ 2√n+1 — this is the w = 2√n variant: |1+1/(w−1)| ≤\n1+(2√n)/((2√n−1)²+t²) ≤ 1+1/(2√n) since 4√n−1 ≤ t².) -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_half_add_one {n : ℕ} {t : ℝ}\n (hn : 16 ≤ n) (ht : (n : ℝ) ≤ t ^ 2) :\n ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by\n have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsq : (0 : ℝ) < Real.sqrt (n : ℝ) := Real.sqrt_pos.mpr (by linarith)\n have hw1 : (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) - 1 =\n ((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I := by\n push_cast\n ring\n have hs0 : ((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I ≠ 0 := by\n intro h\n have him : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).im = 0 := by\n rw [h]; simp\n simp at him\n have ht0 : t = 0 := by\n have h1 : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).im = t := by simp\n linarith\n rw [ht0] at ht\n nlinarith [hnR]\n have hle := norm_one_add_one_div_le hs0\n have hre : (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).re + 1 =\n 2 * Real.sqrt (n : ℝ) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n Complex.sub_re, Complex.one_re]\n ring\n have hns : Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) =\n (2 * Real.sqrt (n : ℝ) - 1) ^ 2 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hkey : (2 * Real.sqrt (n : ℝ)) /\n Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤\n 1 / (2 * Real.sqrt (n : ℝ)) := by\n rw [hns]\n have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)\n have h1 : 4 * Real.sqrt (n : ℝ) - 1 ≤ t ^ 2 := by\n have h2 : 4 * Real.sqrt (n : ℝ) ≤ (n : ℝ) + 1 := by\n have h3 : (4 * Real.sqrt (n : ℝ)) ^ 2 ≤ ((n : ℝ) + 1) ^ 2 := by\n rw [show (4 * Real.sqrt (n : ℝ)) ^ 2 = 16 * (Real.sqrt (n : ℝ) ^ 2) by ring, hsqn]\n nlinarith [sq_nonneg ((n : ℝ) - 1), hnR]\n nlinarith [hsq]\n nlinarith [ht, h2]\n rw [show (2 * Real.sqrt (n : ℝ) - 1) ^ 2 + t ^ 2 =\n 4 * (Real.sqrt (n : ℝ) ^ 2) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2 by ring, hsqn]\n have h4 : (0 : ℝ) < 4 * (n : ℝ) - 4 * Real.sqrt (n : ℝ) + 1 + t ^ 2 := by\n nlinarith [ht, sq_nonneg t, hsq]\n rw [div_le_div_iff_of_pos_left hsq h4 (by positivity)]\n nlinarith [h1, ht, hsq]\n have hstep : 1 + ((((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I).re + 1) /\n Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤\n 1 + 1 / (2 * Real.sqrt (n : ℝ)) := by\n rw [hre]\n have h1 : (2 * Real.sqrt (n : ℝ)) /\n Complex.normSq (((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I) ≤\n 1 / (2 * Real.sqrt (n : ℝ)) := hkey\n linarith [h1]\n have hpow1 : ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I))‖ ^ n ≤\n (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n :=\n pow_le_pow_left₀ (norm_nonneg _) (hle.trans hstep) n\n have hpow2 : (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n ≤\n Real.exp (Real.sqrt (n : ℝ) / 2) := by\n calc (1 + 1 / (2 * Real.sqrt (n : ℝ))) ^ n\n ≤ (Real.exp (1 / (2 * Real.sqrt (n : ℝ)))) ^ n := by\n have h := Real.add_one_le_exp (1 / (2 * Real.sqrt (n : ℝ)))\n exact pow_le_pow_left₀ (by positivity) (by linarith) n\n _ = Real.exp ((n : ℝ) * (1 / (2 * Real.sqrt (n : ℝ)))) :=\n (Real.exp_nat_mul _ n).symm\n _ = Real.exp (Real.sqrt (n : ℝ) / 2) := by\n congr 1\n have hsqn : Real.sqrt (n : ℝ) ^ 2 = (n : ℝ) := Real.sq_sqrt (by linarith)\n field_simp [hsq.ne']\n nlinarith [hsqn]\n unfold kFun\n rw [hw1]\n calc ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I)) ^ n - 1‖\n ≤ ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ :=\n norm_sub_le _ _\n _ = ‖(1 + 1/(((2 * Real.sqrt (n : ℝ) - 1) : ℝ) + t * Complex.I))‖ ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ ≤ Real.exp (Real.sqrt (n : ℝ) / 2) + 1 := by linarith [hpow1.trans hpow2]\n\n/-- **The far-right vertical drop** (D-074 §8 V_right): for n ≥ 16,\n0 < T ≤ U, T² ≥ n, ‖VIntegral (Jlag n) (2√n) T U‖ ≤\n(U−T)·(e^{√n/2}+1)·2^{−(2√n−2)}·dirichletC2 — exponentially tiny. -/\ntheorem vIntegral_Jlag_right_norm_le {n : ℕ} {T U : ℝ}\n (hn : 16 ≤ n) (hT0 : (0 : ℝ) < T) (hTU : T ≤ U) (hTn : (n : ℝ) ≤ T ^ 2) :\n ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ ≤\n (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by\n have hnorm : ‖VIntegral (Jlag n) (2 * Real.sqrt (n : ℝ)) T U‖ =\n ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : ∀ t ∈ Set.Ioc T U,\n ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : ℝ) ≤ t ^ 2 := by nlinarith [hTn, hT0]\n have h1 := kFun_right_vertical_norm_le_exp_sqrt_half_add_one hn ht2\n have h2 := norm_logDeriv_zeta_le_two_pow\n (show (2 : ℝ) ≤ 2 * Real.sqrt (n : ℝ) by\n have hnR : (16 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn\n have hsq : (4 : ℝ) ≤ Real.sqrt (n : ℝ) := by\n rw [Real.le_sqrt (by norm_num) (by linarith)]; norm_num\n linarith) (t := t)\n have hnorm3 : ‖Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ =\n ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ *\n ‖logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ := by\n show ‖kFun n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I) *\n (-logDeriv riemannZeta (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I))‖ = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have hint : ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖ ≤\n ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc ‖∫ t in T..U, Jlag n (((2 * Real.sqrt (n : ℝ)) : ℝ) + t * Complex.I)‖\n ≤ ((Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (Real.sqrt (n : ℝ) / 2) + 1) *\n ((2 : ℝ) ^ (-(2 * Real.sqrt (n : ℝ) - 2)) * dirichletC2) := by ring\n\nend NguyenRH1\n\nend"},"extra_content":null}]