← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (10567 chars)
LiTightR imports LiSqueeze; the chain LiSqueeze → LiCircleBound → ... does it reach LiBasePoints or LiSkeleton? LiSqueeze imports LiCircleBound + Zeta23 presumably; LiCircleBound imports LiFEntire → LiSeries → LiDigammaLeft → LiGapCircles → LiTrivialZeros → LiReflect → LiDisc → LiRBound → LiContour → ... → LiSwaps → LiResidue/LiPrincipal → LiSides... and LiSkeleton? LiContour imports LiSkeleton probably (C0hat, ZeroCountProp). And LiBasePoints imports LiSkeleton (not vice versa). So exp_le_inv_sub_sixteen (in LiBasePoints) is NOT in LiDogLeg's transitive closure (LiDogLeg ← LiSides + LiTightR; nothing imports LiBasePoints except the root).
Options: (a) import NguyenRH1.LiBasePoints in LiDogLeg (adds it to the closure — fine, no cycles since LiBasePoints only imports LiSkeleton); (b) reprove the exp upper bound inline. Take (a) — clean.
Now write the DL-3c/d block. Let me carefully draft it all (~280 lines). I'll write it as one big edit, then iterate on compile errors.
Key lemma signatures:
```lean
/-- 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 h1 : HasDerivAt (fun σ => -c * σ) (-c) x := (hasDerivAt_id' x).const_mul (-c)
have h2 := h1.exp
have h3 := h2.const_mul (-1 / c)
convert h3 using 1
· ext σ
field_simp [hc.ne']
ring
· field_simp [hc.ne']
ring
have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) volume 3 XR :=
(Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn.intervalIntegrable
rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint]
have h1 : -Real.exp (-c * XR) / c ≤ 0 := by
apply div_nonpos_of_nonpos_of_nonneg _ hc.le
linarith [Real.exp_pos (-c * XR)]
have e : -Real.exp (-c * 3) / c = Real.exp (-3 * c) / c := by
congr 1
congr 1
ring
rw [e]
-- F(XR) − F(3) = −e^{−cXR}/c + e^{−3c}/c ≤ e^{−3c}/c
linarith [h1]
```
Hmm — convert h3 using 1 produces two goals (function-eq + derivative-value) — with `ext σ` for the funext. Actually `convert h3 using 1` on a HasDerivAt goal: HasDerivAt F' D x vs HasDerivAt F D' x: convert using 1 gives goals F' = F (funext) and D = D' — hmm, convert on HasDerivAt: using 1 might give the function equality via congrFun. The cleaner pattern used in the project (from LiBasePoints hasDerivAt work): state the derivative form so h3's type matches directly. Alternative avoid convert:
```
have h2 : HasDerivAt (fun σ => Real.exp (-c * σ)) (Real.exp (-c * x) * (-c)) x :=
((hasDerivAt_id' x).const_mul (-c)).exp
have h3 : HasDerivAt (fun σ => -Real.exp (-c * σ) / c) (Real.exp (-c * x)) x := by
have h4 := h2.const_mul (-1 / c)
rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by
field_simp [hc.ne']
ring] at h4
have h5 : (fun σ => (-1 / c) * Real.exp (-c * σ)) = (fun σ => -Real.exp (-c * σ) / c) := by
funext σ
field_simp [hc.ne']
ring
rw [h5] at h4
exact h4
```
(-1/c)·(exp(-cx)·(-c)) = exp(-cx)·(c/c)·... = exp(-cx)·((−1)·(−c)/c) = exp(-cx)·(c/c) = exp(-cx)·1 = exp(-cx) ✓ field_simp + ring — wait field_simp then ring — trailing ring issue again... The identity (−1/c)·(E·(−c)) = E: (−1)·E·(−c)/c = E·(c/c) = E — field_simp clears /c: goal becomes (−1)·(E·(−c)) = E·c ⟺ E·c = E·c ✓ ring closes; field_simp might close directly (it ends with ring1) — if so the ring errors. Use just `field_simp [hc.ne']` and if it leaves something, adjust. Let me write `by field_simp [hc.ne']` alone — field_simp's internal finish usually handles.
Actually — simplest possible antiderivative choice: F(σ) = −(1/c)·exp(−cσ) — derivative: −(1/c)·(−c)·exp = exp ✓. HasDerivAt (fun σ => -(1/c)*exp(-cσ)) ... with h2.const_mul (-(1/c))... same thing. Fine.
The integrability: `Real.continuous_exp.comp (continuous_const.mul continuous_id)` — continuous function −c·σ: continuous_const.mul continuous_id : Continuous (fun σ => -c * σ)?? continuous_const.mul continuous_id : Continuous (fun x => -c * x) — hmm continuous_const.mul : Continuous (fun x => c * f x) given Continuous f — with f = id ✓ gives Continuous (fun x => -c * x) ✓. Then .continuousOn.intervalIntegrable — the method: ContinuousOn.intervalIntegrable (h : ContinuousOn f (uIcc a b)) : IntervalIntegrable f μ a b ✓ (needs uIcc form — it infers). Let me write:
```
have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) volume 3 XR := by
apply ContinuousOn.intervalIntegrable
exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn
```
ContinuousOn.intervalIntegrable : ContinuousOn f (Set.uIcc a b) → IntervalIntegrable f μ a b — the apply unifies ✓.
Then the capstone pieces. Let me also pre-decide the two integral bounds' exact forms:
Bound A: ∫_3^XR 4·exp(−cσ) ≤ e^{4/3}/(2c):
∫ 4·exp = 4·∫ exp ≤ 4·e^{−3c}/c (integral_exp_neg_le) = 4·(e^{4/3}/8)/c = e^{4/3}/(2c) ✓.
e^{−3c} = e^{4/3}/8: exp(−3c) = exp(−3(log2−4/9)) = exp(4/3 − 3 log2) = exp(4/3)·exp(−3 log2); exp(−3 log2) = (exp(log2))⁻³ = 2⁻³ = 1/8: exp(−3·log 2) = exp(log(2^{-3}))? — via Real.exp_log: exp(log (1/8)) = 1/8 with log(1/8) = −3 log 2 (log_div/log_pow: log(1/8) = −log 8 = −3 log 2 ✓ Real.log_pow : log (x^n) = n log x; log 8 = log (2^3) = 3 log 2 ✓). So exp(−3 log 2) = 1/8 ✓.
Bound B: ∫_3^XR 4·2^{−σ} ≤ 1/(2 log 2):
2^{−σ} = exp(−(log 2)·σ) (rpow_def_of_pos): ∫ 4·2^{−σ} = 4·∫ exp(−(log 2)σ) ≤ 4·exp(−3 log 2)/log 2 = 4·(1/8)/log 2 = 1/(2 log 2) ✓ (integral_exp_neg_le with c := log 2, hc : 0 < log 2 via log_pos (by norm_num : (1:ℝ) < 2)).
The capstone:
```
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
-- pointwise envelope
have hpt : ∀ σ ∈ Set.Ioc 3 XR,
‖Jlag n ((σ : ℝ) + U * Complex.I)‖ ≤
(4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 :=
fun σ hσ => Jlag_dogleg_norm_le_envelope (by linarith [hσ.1]) hU hnU
-- the norm-of-integral bound
have hInt_g : IntervalIntegrable (fun σ : ℝ =>
(4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2) volume 3 XR := ...
have h1 : ‖HIntegral (Jlag n) 3 XR U‖ ≤
∫ σ in (3 : ℝ)..XR, (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := by
unfold HIntegral
apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hInt_g
-- the a.e. premise: ∀ᵐ t, t ∈ Ioc 3 XR → ‖Jlag‖ ≤ g
exact Filter.Eventually.of_forall (fun σ hσ => hpt σ hσ)
-- ∫ g = dirichletC2·[4∫e^{−cσ} + 4∫2^{−σ}] ≤ dirichletC2·[e^{4/3}/(2c) + 1/(2 log 2)] ≤ 8.38
...
```
norm_integral_le_of_norm_le (hab : a ≤ b) (h : ∀ᵐ t ∂μ, t ∈ Set.Ioc a b → ‖f t‖ ≤ g t) (hbound : IntervalIntegrable g μ a b) : ‖∫ f‖ ≤ ∫ g ✓ — the signature from Basic.lean:755. The μ is volume by default ✓.
Then:
```
have h2 : ∫ σ in (3 : ℝ)..XR, (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2
= dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +
∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) := by
rw [integral_const_mul, intervalIntegral.integral_add hIntA hIntB]
ring
-- hIntA/hIntB integrability
```
integral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x ✓ (intervalIntegral.integral_const_mul — exists? `intervalIntegral.integral_const_mul (c : ℝ) (f : ℝ → ℝ)`? — or `MeasureTheory.integral_const_mul` for the interval form: `intervalIntegral.integral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x` — I believe exists ✓).
intervalIntegral.integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : ∫ f + g = ∫ f + ∫ g ✓ (the [simp] lemma seen earlier ✓).
Then the two bounds + assembly + certified constants. Full block below. For the certified constants:
- hc_gt : (0.2487 : ℝ) ≤ Real.log 2 - 4 / 9 — via log_two_gt_d9: 0.6931471803 ≤ log 2: c ≥ 0.6931471803−(4/9): 4/9 ≤ 0.4444444445: c ≥ 0.2487027358 ≥ 0.2487 ✓.
- he43 : Real.exp (4/3) ≤ 3.8073 — via exp_le_inv_sub_sixteen at 1/3 + exp_add + exp_one_lt_d9 (needs LiBasePoints import).
- hlog2 : 0.6931471803 ≤ Real.log 2 (d9).
The final assembly: ‖H‖ ≤ dirichletC2·[e^{4/3}/(2c) + 1/(2 log 2)] ≤ 1·[3.8073/(2·0.2487) + 1/(2·0.6931471803)] ≤ [7.6544+0.72134] ≤ 8.38:
3.8073/(2·0.2487) = 3.8073/0.4974: division bound: a/b ≤ a'/b' with a ≤ a', b ≥ b' > 0: (div_le_div he43 (hc_lower...) — div_le_div (hac : a ≤ c) (hdb : d ≤ b) (hd : 0 < d) (hb : 0 ≤ b)... the Mathlib div_le_div (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 < c) (hd : 0 ≤ d)?? — direction: a/b ≤ c/d ⟸ a ≤ c, d ≤ b, 0 < d, 0 ≤ b: `div_le_div (h₁ : a ≤ c) (h₂ : d ≤ b) (h₃ : 0 < d) (h₄ : 0 ≤ b) : a / b ≤ c / d` — hmm signature uncertain; the session-033 notes mention div_le_div_of_nonneg_right exists. For a/b ≤ c/d with a ≤ c and 0 < d ≤ b: `div_le_div (hac : a ≤ c) (hdb : d ≤ b) (hd : 0 < d) (hb : 0 ≤ b) : a / b ≤ c / d` — I'm fairly sure this exists with that exact arg order (used in the project?). I'll write it and fix if the elaborator objects.
1/(2 log 2) ≤ 0.7214: 1/(2·0.6931471803) = 0.72134 — div bound: 1/(2 log 2) ≤ 1/(2·0.6931471803) via one_div_le_one_div_of_le (pos) (2·d9 ≤ 2 log 2) ✓ then 1/(2·0.6931471803) ≤ 0.7214 by norm_num (1/1.38629... = 0.72134 ≤ 0.7214 ✓ norm_num with division — needs the field form: 1/(2·0.6931471803) ≤ 0.7214 ⟺ 1 ≤ 0.7214·(2·0.6931471803) = 0.999... — hmm: 0.7214·1.3862943606 = 1.00006... ≥ 1 ✓ norm_num can verify via div_le_iff₀ or by norm_num directly on the rational inequality (no log involved — it's a pure rational computation after substituting the d9 bound ✓).
The e^{4/3}/(2c) ≤ 3.8073/(2·0.2487) bound: div_le_div he43 (2·0.2487 ≤ 2c) (0 < 2·0.2487) (0 ≤ 2c)... then 3.8073/0.4974 ≤ 7.6545 by norm_num (3.8073/0.4974 = 7.65440 ≤ 7.6545 ✓ rational ✓).
Total: 7.6545+0.7214 = 8.3759 ≤ 8.38 ✓ charge 8.38.
Also — dirichletC2·[X] ≤ 1·X: mul_le_mul_of_nonneg_right dirichletC2_le_one (X ≥ 0).
Now, the certified-constant e^{4/3} ≤ 3.8073 needs exp_le_inv_sub_sixteen from LiBasePoints — add `import NguyenRH1.LiBasePoints` to LiDogLeg. Hmm wait — will that create an import cycle? LiBasePoints imports LiSkeleton only; LiDogLeg imports LiSides + LiTightR + LiBasePoints — no cycle ✓ (LiSkeleton is upstream of everything).
Let me write the full DL-3c/d block.
`LiBasePoints` isn't in LiDogLeg's closure — adding the import (no cycle), then writing the DL-3c/d block.
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "import Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR",
"new_string": "import Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiBasePoints"
}
tool: Edit
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"old_string": "end NguyenRH1\n\nend",
"new_string": "/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/\n\n/-- **The product envelope** (D-074 \u00a77): for \u03c3 \u2265 3, 0 < t, n \u2264 (4/9)t\u00b2,\n\u2016Jlag n (\u03c3+it)\u2016 \u2264 (4\u00b7e^{\u2212c\u03c3} + 4\u00b72^{\u2212\u03c3})\u00b7dirichletC2, c = log 2 \u2212 4/9.\nThe kernel envelope (e^{(4/9)\u03c3}) times the zeta halving (2^{\u2212(\u03c3\u22122)})\ncollapses to the single exponential 4\u00b7e^{\u2212c\u03c3}: no geometric series. -/\ntheorem Jlag_dogleg_norm_le_envelope {n : \u2115} {\u03c3 t : \u211d}\n (h\u03c3 : 3 \u2264 \u03c3) (ht : 0 < t) (hnU : (n : \u211d) \u2264 (4 / 9) * t ^ 2) :\n \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2 := by\n have hw1 : ((\u03c3 : \u211d) + t * Complex.I) - 1 = ((\u03c3 : \u211d) - 1) + t * Complex.I := by\n push_cast\n ring\n have hs1ne : (((\u03c3 : \u211d) - 1) + t * Complex.I) \u2260 0 := by\n intro h\n have him : (((\u03c3 : \u211d) - 1) + t * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hwid : ((\u03c3 : \u211d) + t * Complex.I) / (((\u03c3 : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs1ne]\n ring\n have hker := one_add_div_pow_norm_le_exp_four_ninths h\u03c3 ht hnU\n have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : \u211d) \u2264 \u03c3 by linarith) (t := t)\n have hk : \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u2016(1 + 1 / (((\u03c3 : \u211d) - 1) + t * Complex.I))\u2016 ^ n + 1 := by rw [norm_pow, norm_one]\n _ \u2264 Real.exp ((4 / 9) * \u03c3) + 1 := by linarith [hker]\n have hprod : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := by\n have hn3 : \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((\u03c3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hn3]\n exact mul_le_mul hk hzeta (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have h2b : (2 : \u211d) ^ (-\u03c3) = Real.exp (-(Real.log 2) * \u03c3) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n have h22 : (2 : \u211d) ^ (2 : \u211d) = 4 := by\n rw [Real.rpow_two]\n norm_num\n have h2a : (2 : \u211d) ^ (-(\u03c3 - 2)) = 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [show (-(\u03c3 - 2)) = -\u03c3 + 2 by ring, Real.rpow_add (by norm_num : (0 : \u211d) < 2), h2b, h22]\n ring\n have hexp_alg : Real.exp ((4 / 9) * \u03c3) * Real.exp (-(Real.log 2) * \u03c3) =\n Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) := by\n rw [\u2190 Real.exp_add]\n congr 1\n ring\n have halg : (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2))) =\n 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3) := by\n rw [h2a, h2b, hexp_alg]\n ring\n calc \u2016Jlag n ((\u03c3 : \u211d) + t * Complex.I)\u2016\n \u2264 (Real.exp ((4 / 9) * \u03c3) + 1) * ((2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2) := hprod\n _ = ((Real.exp ((4 / 9) * \u03c3) + 1) * (2 : \u211d) ^ (-(\u03c3 - 2))) * dirichletC2 := by ring\n _ = (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2 := by\n rw [halg]\n\n/-- The FTC-bound \u222b\u2083^XR e^{\u2212c\u03c3}d\u03c3 \u2264 e^{\u22123c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : \u211d} (hc : 0 < c) (_hXR : 3 \u2264 XR) :\n \u222b \u03c3 in (3 : \u211d)..XR, Real.exp (-c * \u03c3) \u2264 Real.exp (-3 * c) / c := by\n have hF : \u2200 x \u2208 Set.uIcc (3 : \u211d) XR,\n HasDerivAt (fun \u03c3 => -Real.exp (-c * \u03c3) / c) (Real.exp (-c * x)) x := by\n intro x hx\n have h2 : HasDerivAt (fun \u03c3 => Real.exp (-c * \u03c3)) (Real.exp (-c * x) * (-c)) x :=\n ((hasDerivAt_id' x).const_mul (-c)).exp\n have h3 := h2.const_mul (-1 / c)\n rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n field_simp [hc.ne']] at h3\n have h5 : (fun \u03c3 => (-1 / c) * Real.exp (-c * \u03c3)) =\n (fun \u03c3 => -Real.exp (-c * \u03c3) / c) := by\n funext \u03c3\n field_simp [hc.ne']\n ring\n rw [h5] at h3\n exact h3\n have hint : IntervalIntegrable (fun \u03c3 => Real.exp (-c * \u03c3)) volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint]\n have h1 : -Real.exp (-c * XR) / c \u2264 0 := by\n apply div_nonpos_of_nonpos_of_nonneg _ hc.le\n linarith [Real.exp_pos (-c * XR)]\n have e : -Real.exp (-c * 3) / c = Real.exp (-3 * c) / c := by\n congr 1\n congr 1\n ring\n rw [e]\n linarith [h1]\n\n/-- The certified exponent-decay constant c = log 2 \u2212 4/9 \u2265 0.2487. -/\nlemma cdog_gt : (0.2487 : \u211d) \u2264 Real.log 2 - 4 / 9 := by\n have h := Real.log_two_gt_d9\n norm_num at h\n linarith\n\n/-- The certified e^{4/3} \u2264 3.8073 (the (1\u2212x/16)\u207b\u00b9\u2076 route + d9 e). -/\nlemma exp_four_thirds_le : Real.exp (4 / 3) \u2264 (3.8073 : \u211d) := by\n have he13 : Real.exp (1 / 3) \u2264 (1.4006 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n rw [show (4 / 3 : \u211d) = 1 + 1 / 3 by norm_num, Real.exp_add]\n calc Real.exp 1 * Real.exp (1 / 3) \u2264 2.7182818286 * 1.4006 :=\n mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)\n _ \u2264 3.8073 := by norm_num\n\n/-- **THE HIGH-HORIZONTAL BOUND** (D-074 \u00a77 capstone; D-073 Cor 4.2's\nR(1.5) in single-exponential-envelope form): for 0 < U, n \u2264 (4/9)U\u00b2\n(i.e. U \u2265 (3/2)\u221an) and 3 \u2264 XR, \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 8.38\n(charged; the true value \u2264 1.2 at n = 10\u2075, E-034 V5). Charged with\ndirichletC2 \u2264 1 \u2014 the tight R(1.5) = 5.94 would need a dirichletC2 \u2264\n0.57 build (documented as the tightening path; the fold is\nindifferent: \u0394 \u2248 +2.4 per side). -/\ntheorem hIntegral_Jlag_dogleg_norm_le {n : \u2115} {U XR : \u211d}\n (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) (hXR : 3 \u2264 XR) :\n \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264 (8.38 : \u211d) := by\n have hc : (0 : \u211d) < Real.log 2 - 4 / 9 := by\n have h := cdog_gt\n linarith\n have hpt : \u2200 \u03c3 \u2208 Set.Ioc 3 XR,\n \u2016Jlag n ((\u03c3 : \u211d) + U * Complex.I)\u2016 \u2264\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2 :=\n fun \u03c3 h\u03c3 => Jlag_dogleg_norm_le_envelope (by linarith [h\u03c3.1]) hU hnU\n have hcontA : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2 - 4 / 9) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have hcontB : Continuous (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) := by\n have h1 : Continuous (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have h2 : (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2]\n exact h1\n have hIntA : IntervalIntegrable (fun \u03c3 : \u211d => 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3))\n volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontA.const_mul 4).continuousOn\n have hIntB : IntervalIntegrable (fun \u03c3 : \u211d => 4 * (2 : \u211d) ^ (-\u03c3)) volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontB.const_mul 4).continuousOn\n have hIntG : IntervalIntegrable (fun \u03c3 : \u211d =>\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2)\n volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact ((hcontA.add hcontB).const_mul dirichletC2).continuousOn\n -- step 1: \u2016H\u2016 \u2264 \u222b envelope\n have h1 : \u2016HIntegral (Jlag n) 3 XR U\u2016 \u2264\n \u222b \u03c3 in (3 : \u211d)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2 := by\n unfold HIntegral\n apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG\n exact Filter.Eventually.of_forall (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n -- step 2: \u222b envelope = dirichletC2\u00b7(4\u222be^{\u2212c\u03c3} + 4\u222b2^{\u2212\u03c3})\n have h2 : \u222b \u03c3 in (3 : \u211d)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2\n = dirichletC2 * (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) +\n \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) := by\n rw [integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n ring\n -- step 3: the two integral bounds\n have h3a : \u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) \u2264\n Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n rw [intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le hc hXR\n have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by\n have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by\n have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by\n rw [Real.log_div (by norm_num : (1 : \u211d) \u2260 0) (by norm_num : (8 : \u211d) \u2260 0),\n Real.log_one, Real.log_pow]\n push_cast\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n calc Real.exp (-3 * (Real.log 2 - 4 / 9))\n = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring\n _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]\n _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring\n rw [he3c] at h\n calc 4 * (Real.exp (-3 * (Real.log 2 - 4 / 9)) / (Real.log 2 - 4 / 9))\n = 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) := by rw [he3c]\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n field_simp [hc.ne']\n ring\n have h3b : \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3) \u2264 1 / (2 * Real.log 2) := by\n have h2e : (fun \u03c3 : \u211d => (2 : \u211d) ^ (-\u03c3)) =\n (fun \u03c3 : \u211d => Real.exp (-(Real.log 2) * \u03c3)) := by\n funext \u03c3\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n rw [h2e, intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : \u211d) < 2)) hXR\n have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by\n have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by\n rw [Real.log_div (by norm_num : (1 : \u211d) \u2260 0) (by norm_num : (8 : \u211d) \u2260 0),\n Real.log_one, Real.log_pow]\n push_cast\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : \u211d) < 1 / 8)]\n rw [h3l2] at h\n calc 4 * ((1 / 8) / Real.log 2) = 1 / (2 * Real.log 2) := by\n field_simp [Real.log_pos (by norm_num : (1 : \u211d) < 2)].ne'\n ring\n exact h.trans (by rw [h3l2])\n -- hmm, h's RHS after rw [h3l2] at h: (1/8)/log2; the calc shows 4\u00b7((1/8)/log2) = 1/(2 log2)\n -- step 4: the certified assembly\n have hlog2 : (0.6931471803 : \u211d) \u2264 Real.log 2 := Real.log_two_gt_d9\n have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 (7.6545 : \u211d) := by\n have hcge := cdog_gt\n have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) \u2264 3.8073 / (2 * 0.2487) :=\n div_le_div exp_four_thirds_le (by linarith) (by norm_num) (by positivity)\n calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))\n \u2264 3.8073 / (2 * 0.2487) := h1\n _ \u2264 7.6545 := by norm_num\n have h72 : 1 / (2 * Real.log 2) \u2264 (0.7214 : \u211d) := by\n have h1 : 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) :=\n one_div_le_one_div_of_le (by positivity) (by linarith)\n calc 1 / (2 * Real.log 2) \u2264 1 / (2 * 0.6931471803) := h1\n _ \u2264 0.7214 := by norm_num\n have hC2 : dirichletC2 \u2264 1 := dirichletC2_le_one\n have hsum : dirichletC2 * (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) +\n \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) \u2264 (8.38 : \u211d) := by\n have hA0 : (0 : \u211d) \u2264 Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity\n have hB0 : (0 : \u211d) \u2264 1 / (2 * Real.log 2) := by positivity\n calc dirichletC2 * (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) +\n \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3))\n \u2264 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by\n apply mul_le_mul hC2 (add_le_add h3a h3b) (by positivity) (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring\n _ \u2264 7.6545 + 0.7214 := add_le_add h48 h72\n _ \u2264 8.38 := by norm_num\n calc \u2016HIntegral (Jlag n) 3 XR U\u2016\n \u2264 \u222b \u03c3 in (3 : \u211d)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) + 4 * (2 : \u211d) ^ (-\u03c3)) * dirichletC2 := h1\n _ = dirichletC2 * (\u222b \u03c3 in (3 : \u211d)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * \u03c3) +\n \u222b \u03c3 in (3 : \u211d)..XR, 4 * (2 : \u211d) ^ (-\u03c3)) := h2\n _ \u2264 8.38 := hsum\n\nend NguyenRH1\n\nend"
}
raw content_json (database row)
[{"type":"thinking","thinking":"LiTightR imports LiSqueeze; the chain LiSqueeze → LiCircleBound → ... does it reach LiBasePoints or LiSkeleton? LiSqueeze imports LiCircleBound + Zeta23 presumably; LiCircleBound imports LiFEntire → LiSeries → LiDigammaLeft → LiGapCircles → LiTrivialZeros → LiReflect → LiDisc → LiRBound → LiContour → ... → LiSwaps → LiResidue/LiPrincipal → LiSides... and LiSkeleton? LiContour imports LiSkeleton probably (C0hat, ZeroCountProp). And LiBasePoints imports LiSkeleton (not vice versa). So exp_le_inv_sub_sixteen (in LiBasePoints) is NOT in LiDogLeg's transitive closure (LiDogLeg ← LiSides + LiTightR; nothing imports LiBasePoints except the root).\n\nOptions: (a) import NguyenRH1.LiBasePoints in LiDogLeg (adds it to the closure — fine, no cycles since LiBasePoints only imports LiSkeleton); (b) reprove the exp upper bound inline. Take (a) — clean.\n\nNow write the DL-3c/d block. Let me carefully draft it all (~280 lines). I'll write it as one big edit, then iterate on compile errors.\n\nKey lemma signatures:\n\n```lean\n/-- The FTC-bound ∫₃^XR e^{−cσ}dσ ≤ e^{−3c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : ℝ} (hc : 0 < c) (hXR : 3 ≤ XR) :\n ∫ σ in (3 : ℝ)..XR, Real.exp (-c * σ) ≤ Real.exp (-3 * c) / c := by\n have hF : ∀ x ∈ Set.uIcc (3 : ℝ) XR,\n HasDerivAt (fun σ => -Real.exp (-c * σ) / c) (Real.exp (-c * x)) x := by\n intro x hx\n have h1 : HasDerivAt (fun σ => -c * σ) (-c) x := (hasDerivAt_id' x).const_mul (-c)\n have h2 := h1.exp\n have h3 := h2.const_mul (-1 / c)\n convert h3 using 1\n · ext σ\n field_simp [hc.ne']\n ring\n · field_simp [hc.ne']\n ring\n have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) volume 3 XR :=\n (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn.intervalIntegrable\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint]\n have h1 : -Real.exp (-c * XR) / c ≤ 0 := by\n apply div_nonpos_of_nonpos_of_nonneg _ hc.le\n linarith [Real.exp_pos (-c * XR)]\n have e : -Real.exp (-c * 3) / c = Real.exp (-3 * c) / c := by\n congr 1\n congr 1\n ring\n rw [e]\n -- F(XR) − F(3) = −e^{−cXR}/c + e^{−3c}/c ≤ e^{−3c}/c\n linarith [h1]\n```\nHmm — convert h3 using 1 produces two goals (function-eq + derivative-value) — with `ext σ` for the funext. Actually `convert h3 using 1` on a HasDerivAt goal: HasDerivAt F' D x vs HasDerivAt F D' x: convert using 1 gives goals F' = F (funext) and D = D' — hmm, convert on HasDerivAt: using 1 might give the function equality via congrFun. The cleaner pattern used in the project (from LiBasePoints hasDerivAt work): state the derivative form so h3's type matches directly. Alternative avoid convert: \n\n```\n have h2 : HasDerivAt (fun σ => Real.exp (-c * σ)) (Real.exp (-c * x) * (-c)) x :=\n ((hasDerivAt_id' x).const_mul (-c)).exp\n have h3 : HasDerivAt (fun σ => -Real.exp (-c * σ) / c) (Real.exp (-c * x)) x := by\n have h4 := h2.const_mul (-1 / c)\n rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n field_simp [hc.ne']\n ring] at h4\n have h5 : (fun σ => (-1 / c) * Real.exp (-c * σ)) = (fun σ => -Real.exp (-c * σ) / c) := by\n funext σ\n field_simp [hc.ne']\n ring\n rw [h5] at h4\n exact h4\n```\n(-1/c)·(exp(-cx)·(-c)) = exp(-cx)·(c/c)·... = exp(-cx)·((−1)·(−c)/c) = exp(-cx)·(c/c) = exp(-cx)·1 = exp(-cx) ✓ field_simp + ring — wait field_simp then ring — trailing ring issue again... The identity (−1/c)·(E·(−c)) = E: (−1)·E·(−c)/c = E·(c/c) = E — field_simp clears /c: goal becomes (−1)·(E·(−c)) = E·c ⟺ E·c = E·c ✓ ring closes; field_simp might close directly (it ends with ring1) — if so the ring errors. Use just `field_simp [hc.ne']` and if it leaves something, adjust. Let me write `by field_simp [hc.ne']` alone — field_simp's internal finish usually handles.\n\nActually — simplest possible antiderivative choice: F(σ) = −(1/c)·exp(−cσ) — derivative: −(1/c)·(−c)·exp = exp ✓. HasDerivAt (fun σ => -(1/c)*exp(-cσ)) ... with h2.const_mul (-(1/c))... same thing. Fine.\n\nThe integrability: `Real.continuous_exp.comp (continuous_const.mul continuous_id)` — continuous function −c·σ: continuous_const.mul continuous_id : Continuous (fun σ => -c * σ)?? continuous_const.mul continuous_id : Continuous (fun x => -c * x) — hmm continuous_const.mul : Continuous (fun x => c * f x) given Continuous f — with f = id ✓ gives Continuous (fun x => -c * x) ✓. Then .continuousOn.intervalIntegrable — the method: ContinuousOn.intervalIntegrable (h : ContinuousOn f (uIcc a b)) : IntervalIntegrable f μ a b ✓ (needs uIcc form — it infers). Let me write:\n```\n have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n```\nContinuousOn.intervalIntegrable : ContinuousOn f (Set.uIcc a b) → IntervalIntegrable f μ a b — the apply unifies ✓.\n\nThen the capstone pieces. Let me also pre-decide the two integral bounds' exact forms:\n\nBound A: ∫_3^XR 4·exp(−cσ) ≤ e^{4/3}/(2c):\n∫ 4·exp = 4·∫ exp ≤ 4·e^{−3c}/c (integral_exp_neg_le) = 4·(e^{4/3}/8)/c = e^{4/3}/(2c) ✓.\ne^{−3c} = e^{4/3}/8: exp(−3c) = exp(−3(log2−4/9)) = exp(4/3 − 3 log2) = exp(4/3)·exp(−3 log2); exp(−3 log2) = (exp(log2))⁻³ = 2⁻³ = 1/8: exp(−3·log 2) = exp(log(2^{-3}))? — via Real.exp_log: exp(log (1/8)) = 1/8 with log(1/8) = −3 log 2 (log_div/log_pow: log(1/8) = −log 8 = −3 log 2 ✓ Real.log_pow : log (x^n) = n log x; log 8 = log (2^3) = 3 log 2 ✓). So exp(−3 log 2) = 1/8 ✓.\n\nBound B: ∫_3^XR 4·2^{−σ} ≤ 1/(2 log 2):\n2^{−σ} = exp(−(log 2)·σ) (rpow_def_of_pos): ∫ 4·2^{−σ} = 4·∫ exp(−(log 2)σ) ≤ 4·exp(−3 log 2)/log 2 = 4·(1/8)/log 2 = 1/(2 log 2) ✓ (integral_exp_neg_le with c := log 2, hc : 0 < log 2 via log_pos (by norm_num : (1:ℝ) < 2)).\n\nThe capstone:\n```\ntheorem hIntegral_Jlag_dogleg_norm_le {n : ℕ} {U XR : ℝ}\n (hU : 0 < U) (hnU : (n : ℝ) ≤ (4 / 9) * U ^ 2) (hXR : 3 ≤ XR) :\n ‖HIntegral (Jlag n) 3 XR U‖ ≤ (8.38 : ℝ) := by\n -- pointwise envelope\n have hpt : ∀ σ ∈ Set.Ioc 3 XR,\n ‖Jlag n ((σ : ℝ) + U * Complex.I)‖ ≤\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 :=\n fun σ hσ => Jlag_dogleg_norm_le_envelope (by linarith [hσ.1]) hU hnU\n -- the norm-of-integral bound\n have hInt_g : IntervalIntegrable (fun σ : ℝ =>\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2) volume 3 XR := ...\n have h1 : ‖HIntegral (Jlag n) 3 XR U‖ ≤\n ∫ σ in (3 : ℝ)..XR, (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := by\n unfold HIntegral\n apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hInt_g\n -- the a.e. premise: ∀ᵐ t, t ∈ Ioc 3 XR → ‖Jlag‖ ≤ g\n exact Filter.Eventually.of_forall (fun σ hσ => hpt σ hσ)\n -- ∫ g = dirichletC2·[4∫e^{−cσ} + 4∫2^{−σ}] ≤ dirichletC2·[e^{4/3}/(2c) + 1/(2 log 2)] ≤ 8.38\n ...\n```\nnorm_integral_le_of_norm_le (hab : a ≤ b) (h : ∀ᵐ t ∂μ, t ∈ Set.Ioc a b → ‖f t‖ ≤ g t) (hbound : IntervalIntegrable g μ a b) : ‖∫ f‖ ≤ ∫ g ✓ — the signature from Basic.lean:755. The μ is volume by default ✓.\n\nThen:\n```\n have h2 : ∫ σ in (3 : ℝ)..XR, (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2\n = dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +\n ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) := by\n rw [integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n ring\n -- hIntA/hIntB integrability\n```\nintegral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x ✓ (intervalIntegral.integral_const_mul — exists? `intervalIntegral.integral_const_mul (c : ℝ) (f : ℝ → ℝ)`? — or `MeasureTheory.integral_const_mul` for the interval form: `intervalIntegral.integral_const_mul : ∫ x in a..b, c * f x = c * ∫ x in a..b, f x` — I believe exists ✓).\nintervalIntegral.integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) : ∫ f + g = ∫ f + ∫ g ✓ (the [simp] lemma seen earlier ✓).\n\nThen the two bounds + assembly + certified constants. Full block below. For the certified constants:\n- hc_gt : (0.2487 : ℝ) ≤ Real.log 2 - 4 / 9 — via log_two_gt_d9: 0.6931471803 ≤ log 2: c ≥ 0.6931471803−(4/9): 4/9 ≤ 0.4444444445: c ≥ 0.2487027358 ≥ 0.2487 ✓.\n- he43 : Real.exp (4/3) ≤ 3.8073 — via exp_le_inv_sub_sixteen at 1/3 + exp_add + exp_one_lt_d9 (needs LiBasePoints import).\n- hlog2 : 0.6931471803 ≤ Real.log 2 (d9).\n\nThe final assembly: ‖H‖ ≤ dirichletC2·[e^{4/3}/(2c) + 1/(2 log 2)] ≤ 1·[3.8073/(2·0.2487) + 1/(2·0.6931471803)] ≤ [7.6544+0.72134] ≤ 8.38:\n3.8073/(2·0.2487) = 3.8073/0.4974: division bound: a/b ≤ a'/b' with a ≤ a', b ≥ b' > 0: (div_le_div he43 (hc_lower...) — div_le_div (hac : a ≤ c) (hdb : d ≤ b) (hd : 0 < d) (hb : 0 ≤ b)... the Mathlib div_le_div (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 < c) (hd : 0 ≤ d)?? — direction: a/b ≤ c/d ⟸ a ≤ c, d ≤ b, 0 < d, 0 ≤ b: `div_le_div (h₁ : a ≤ c) (h₂ : d ≤ b) (h₃ : 0 < d) (h₄ : 0 ≤ b) : a / b ≤ c / d` — hmm signature uncertain; the session-033 notes mention div_le_div_of_nonneg_right exists. For a/b ≤ c/d with a ≤ c and 0 < d ≤ b: `div_le_div (hac : a ≤ c) (hdb : d ≤ b) (hd : 0 < d) (hb : 0 ≤ b) : a / b ≤ c / d` — I'm fairly sure this exists with that exact arg order (used in the project?). I'll write it and fix if the elaborator objects.\n\n1/(2 log 2) ≤ 0.7214: 1/(2·0.6931471803) = 0.72134 — div bound: 1/(2 log 2) ≤ 1/(2·0.6931471803) via one_div_le_one_div_of_le (pos) (2·d9 ≤ 2 log 2) ✓ then 1/(2·0.6931471803) ≤ 0.7214 by norm_num (1/1.38629... = 0.72134 ≤ 0.7214 ✓ norm_num with division — needs the field form: 1/(2·0.6931471803) ≤ 0.7214 ⟺ 1 ≤ 0.7214·(2·0.6931471803) = 0.999... — hmm: 0.7214·1.3862943606 = 1.00006... ≥ 1 ✓ norm_num can verify via div_le_iff₀ or by norm_num directly on the rational inequality (no log involved — it's a pure rational computation after substituting the d9 bound ✓).\n\nThe e^{4/3}/(2c) ≤ 3.8073/(2·0.2487) bound: div_le_div he43 (2·0.2487 ≤ 2c) (0 < 2·0.2487) (0 ≤ 2c)... then 3.8073/0.4974 ≤ 7.6545 by norm_num (3.8073/0.4974 = 7.65440 ≤ 7.6545 ✓ rational ✓).\n\nTotal: 7.6545+0.7214 = 8.3759 ≤ 8.38 ✓ charge 8.38.\n\nAlso — dirichletC2·[X] ≤ 1·X: mul_le_mul_of_nonneg_right dirichletC2_le_one (X ≥ 0).\n\nNow, the certified-constant e^{4/3} ≤ 3.8073 needs exp_le_inv_sub_sixteen from LiBasePoints — add `import NguyenRH1.LiBasePoints` to LiDogLeg. Hmm wait — will that create an import cycle? LiBasePoints imports LiSkeleton only; LiDogLeg imports LiSides + LiTightR + LiBasePoints — no cycle ✓ (LiSkeleton is upstream of everything).\n\nLet me write the full DL-3c/d block.","signature":""},{"type":"text","text":"`LiBasePoints` isn't in LiDogLeg's closure — adding the import (no cycle), then writing the DL-3c/d block."},{"type":"tool_use","id":"Edit_256","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"import Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR","new_string":"import Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiBasePoints"},"extra_content":null},{"type":"tool_use","id":"Edit_257","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean","old_string":"end NguyenRH1\n\nend","new_string":"/-! ## 5. The product envelope and the integral assembly (DL-3c/d) -/\n\n/-- **The product envelope** (D-074 §7): for σ ≥ 3, 0 < t, n ≤ (4/9)t²,\n‖Jlag n (σ+it)‖ ≤ (4·e^{−cσ} + 4·2^{−σ})·dirichletC2, c = log 2 − 4/9.\nThe kernel envelope (e^{(4/9)σ}) times the zeta halving (2^{−(σ−2)})\ncollapses to the single exponential 4·e^{−cσ}: no geometric series. -/\ntheorem Jlag_dogleg_norm_le_envelope {n : ℕ} {σ t : ℝ}\n (hσ : 3 ≤ σ) (ht : 0 < t) (hnU : (n : ℝ) ≤ (4 / 9) * t ^ 2) :\n ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ ≤\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := by\n have hw1 : ((σ : ℝ) + t * Complex.I) - 1 = ((σ : ℝ) - 1) + t * Complex.I := by\n push_cast\n ring\n have hs1ne : (((σ : ℝ) - 1) + t * Complex.I) ≠ 0 := by\n intro h\n have him : (((σ : ℝ) - 1) + t * Complex.I).im = 0 := by rw [h]; simp\n simp at him\n linarith\n have hwid : ((σ : ℝ) + t * Complex.I) / (((σ : ℝ) + t * Complex.I) - 1) =\n 1 + 1 / (((σ : ℝ) - 1) + t * Complex.I) := by\n rw [hw1]\n field_simp [hs1ne]\n ring\n have hker := one_add_div_pow_norm_le_exp_four_ninths hσ ht hnU\n have hzeta := norm_logDeriv_zeta_le_two_pow (show (2 : ℝ) ≤ σ by linarith) (t := t)\n have hk : ‖kFun n ((σ : ℝ) + t * Complex.I)‖ ≤ Real.exp ((4 / 9) * σ) + 1 := by\n unfold kFun\n rw [hwid]\n calc ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I)) ^ n - 1‖\n ≤ ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I)) ^ n‖ + ‖(1 : ℂ)‖ := norm_sub_le _ _\n _ = ‖(1 + 1 / (((σ : ℝ) - 1) + t * Complex.I))‖ ^ n + 1 := by rw [norm_pow, norm_one]\n _ ≤ Real.exp ((4 / 9) * σ) + 1 := by linarith [hker]\n have hprod : ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ ≤\n (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2)) * dirichletC2) := by\n have hn3 : ‖Jlag n ((σ : ℝ) + t * Complex.I)‖ =\n ‖kFun n ((σ : ℝ) + t * Complex.I)‖ *\n ‖logDeriv riemannZeta ((σ : ℝ) + t * Complex.I)‖ := by\n show ‖kFun n ((σ : ℝ) + t * Complex.I) *\n (-logDeriv riemannZeta ((σ : ℝ) + t * Complex.I))‖ = _\n rw [norm_mul, norm_neg]\n rw [hn3]\n exact mul_le_mul hk hzeta (norm_nonneg _)\n (add_nonneg (Real.exp_nonneg _) (by norm_num))\n have h2b : (2 : ℝ) ^ (-σ) = Real.exp (-(Real.log 2) * σ) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]\n congr 1\n ring\n have h22 : (2 : ℝ) ^ (2 : ℝ) = 4 := by\n rw [Real.rpow_two]\n norm_num\n have h2a : (2 : ℝ) ^ (-(σ - 2)) = 4 * (2 : ℝ) ^ (-σ) := by\n rw [show (-(σ - 2)) = -σ + 2 by ring, Real.rpow_add (by norm_num : (0 : ℝ) < 2), h2b, h22]\n ring\n have hexp_alg : Real.exp ((4 / 9) * σ) * Real.exp (-(Real.log 2) * σ) =\n Real.exp (-(Real.log 2 - 4 / 9) * σ) := by\n rw [← Real.exp_add]\n congr 1\n ring\n have halg : (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2))) =\n 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ) := by\n rw [h2a, h2b, hexp_alg]\n ring\n calc ‖Jlag n ((σ : ℝ) + t * Complex.I)‖\n ≤ (Real.exp ((4 / 9) * σ) + 1) * ((2 : ℝ) ^ (-(σ - 2)) * dirichletC2) := hprod\n _ = ((Real.exp ((4 / 9) * σ) + 1) * (2 : ℝ) ^ (-(σ - 2))) * dirichletC2 := by ring\n _ = (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := by\n rw [halg]\n\n/-- The FTC-bound ∫₃^XR e^{−cσ}dσ ≤ e^{−3c}/c for c > 0. -/\nlemma integral_exp_neg_le {c XR : ℝ} (hc : 0 < c) (_hXR : 3 ≤ XR) :\n ∫ σ in (3 : ℝ)..XR, Real.exp (-c * σ) ≤ Real.exp (-3 * c) / c := by\n have hF : ∀ x ∈ Set.uIcc (3 : ℝ) XR,\n HasDerivAt (fun σ => -Real.exp (-c * σ) / c) (Real.exp (-c * x)) x := by\n intro x hx\n have h2 : HasDerivAt (fun σ => Real.exp (-c * σ)) (Real.exp (-c * x) * (-c)) x :=\n ((hasDerivAt_id' x).const_mul (-c)).exp\n have h3 := h2.const_mul (-1 / c)\n rw [show (-1 / c) * (Real.exp (-c * x) * (-c)) = Real.exp (-c * x) by\n field_simp [hc.ne']] at h3\n have h5 : (fun σ => (-1 / c) * Real.exp (-c * σ)) =\n (fun σ => -Real.exp (-c * σ) / c) := by\n funext σ\n field_simp [hc.ne']\n ring\n rw [h5] at h3\n exact h3\n have hint : IntervalIntegrable (fun σ => Real.exp (-c * σ)) volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (Real.continuous_exp.comp (continuous_const.mul continuous_id)).continuousOn\n rw [intervalIntegral.integral_eq_sub_of_hasDerivAt hF hint]\n have h1 : -Real.exp (-c * XR) / c ≤ 0 := by\n apply div_nonpos_of_nonpos_of_nonneg _ hc.le\n linarith [Real.exp_pos (-c * XR)]\n have e : -Real.exp (-c * 3) / c = Real.exp (-3 * c) / c := by\n congr 1\n congr 1\n ring\n rw [e]\n linarith [h1]\n\n/-- The certified exponent-decay constant c = log 2 − 4/9 ≥ 0.2487. -/\nlemma cdog_gt : (0.2487 : ℝ) ≤ Real.log 2 - 4 / 9 := by\n have h := Real.log_two_gt_d9\n norm_num at h\n linarith\n\n/-- The certified e^{4/3} ≤ 3.8073 (the (1−x/16)⁻¹⁶ route + d9 e). -/\nlemma exp_four_thirds_le : Real.exp (4 / 3) ≤ (3.8073 : ℝ) := by\n have he13 : Real.exp (1 / 3) ≤ (1.4006 : ℝ) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n rw [show (4 / 3 : ℝ) = 1 + 1 / 3 by norm_num, Real.exp_add]\n calc Real.exp 1 * Real.exp (1 / 3) ≤ 2.7182818286 * 1.4006 :=\n mul_le_mul Real.exp_one_lt_d9.le he13 (Real.exp_pos _).le (by norm_num)\n _ ≤ 3.8073 := by norm_num\n\n/-- **THE HIGH-HORIZONTAL BOUND** (D-074 §7 capstone; D-073 Cor 4.2's\nR(1.5) in single-exponential-envelope form): for 0 < U, n ≤ (4/9)U²\n(i.e. U ≥ (3/2)√n) and 3 ≤ XR, ‖HIntegral (Jlag n) 3 XR U‖ ≤ 8.38\n(charged; the true value ≤ 1.2 at n = 10⁵, E-034 V5). Charged with\ndirichletC2 ≤ 1 — the tight R(1.5) = 5.94 would need a dirichletC2 ≤\n0.57 build (documented as the tightening path; the fold is\nindifferent: Δ ≈ +2.4 per side). -/\ntheorem hIntegral_Jlag_dogleg_norm_le {n : ℕ} {U XR : ℝ}\n (hU : 0 < U) (hnU : (n : ℝ) ≤ (4 / 9) * U ^ 2) (hXR : 3 ≤ XR) :\n ‖HIntegral (Jlag n) 3 XR U‖ ≤ (8.38 : ℝ) := by\n have hc : (0 : ℝ) < Real.log 2 - 4 / 9 := by\n have h := cdog_gt\n linarith\n have hpt : ∀ σ ∈ Set.Ioc 3 XR,\n ‖Jlag n ((σ : ℝ) + U * Complex.I)‖ ≤\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 :=\n fun σ hσ => Jlag_dogleg_norm_le_envelope (by linarith [hσ.1]) hU hnU\n have hcontA : Continuous (fun σ : ℝ => Real.exp (-(Real.log 2 - 4 / 9) * σ)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have hcontB : Continuous (fun σ : ℝ => (2 : ℝ) ^ (-σ)) := by\n have h1 : Continuous (fun σ : ℝ => Real.exp (-(Real.log 2) * σ)) :=\n Real.continuous_exp.comp (continuous_const.mul continuous_id)\n have h2 : (fun σ : ℝ => (2 : ℝ) ^ (-σ)) =\n (fun σ : ℝ => Real.exp (-(Real.log 2) * σ)) := by\n funext σ\n rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]\n congr 1\n ring\n rw [h2]\n exact h1\n have hIntA : IntervalIntegrable (fun σ : ℝ => 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ))\n volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontA.const_mul 4).continuousOn\n have hIntB : IntervalIntegrable (fun σ : ℝ => 4 * (2 : ℝ) ^ (-σ)) volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact (hcontB.const_mul 4).continuousOn\n have hIntG : IntervalIntegrable (fun σ : ℝ =>\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2)\n volume 3 XR := by\n apply ContinuousOn.intervalIntegrable\n exact ((hcontA.add hcontB).const_mul dirichletC2).continuousOn\n -- step 1: ‖H‖ ≤ ∫ envelope\n have h1 : ‖HIntegral (Jlag n) 3 XR U‖ ≤\n ∫ σ in (3 : ℝ)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := by\n unfold HIntegral\n apply intervalIntegral.norm_integral_le_of_norm_le hXR _ hIntG\n exact Filter.Eventually.of_forall (fun σ hσ => hpt σ hσ)\n -- step 2: ∫ envelope = dirichletC2·(4∫e^{−cσ} + 4∫2^{−σ})\n have h2 : ∫ σ in (3 : ℝ)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2\n = dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +\n ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) := by\n rw [integral_const_mul, intervalIntegral.integral_add hIntA hIntB]\n ring\n -- step 3: the two integral bounds\n have h3a : ∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) ≤\n Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n rw [intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le hc hXR\n have he3c : Real.exp (-3 * (Real.log 2 - 4 / 9)) = Real.exp (4 / 3) / 8 := by\n have h3l2 : Real.exp (-(3 * Real.log 2)) = 1 / 8 := by\n have e1 : -(3 * Real.log 2) = Real.log (1 / 8) := by\n rw [Real.log_div (by norm_num : (1 : ℝ) ≠ 0) (by norm_num : (8 : ℝ) ≠ 0),\n Real.log_one, Real.log_pow]\n push_cast\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : ℝ) < 1 / 8)]\n calc Real.exp (-3 * (Real.log 2 - 4 / 9))\n = Real.exp ((4 / 3) + -(3 * Real.log 2)) := by congr 1; ring\n _ = Real.exp (4 / 3) * Real.exp (-(3 * Real.log 2)) := by rw [Real.exp_add]\n _ = Real.exp (4 / 3) / 8 := by rw [h3l2]; ring\n rw [he3c] at h\n calc 4 * (Real.exp (-3 * (Real.log 2 - 4 / 9)) / (Real.log 2 - 4 / 9))\n = 4 * ((Real.exp (4 / 3) / 8) / (Real.log 2 - 4 / 9)) := by rw [he3c]\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by\n field_simp [hc.ne']\n ring\n have h3b : ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ) ≤ 1 / (2 * Real.log 2) := by\n have h2e : (fun σ : ℝ => (2 : ℝ) ^ (-σ)) =\n (fun σ : ℝ => Real.exp (-(Real.log 2) * σ)) := by\n funext σ\n rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]\n congr 1\n ring\n rw [h2e, intervalIntegral.integral_const_mul]\n have h := integral_exp_neg_le (Real.log_pos (by norm_num : (1 : ℝ) < 2)) hXR\n have h3l2 : Real.exp (-3 * Real.log 2) = 1 / 8 := by\n have e1 : (-3 * Real.log 2) = Real.log (1 / 8) := by\n rw [Real.log_div (by norm_num : (1 : ℝ) ≠ 0) (by norm_num : (8 : ℝ) ≠ 0),\n Real.log_one, Real.log_pow]\n push_cast\n ring\n rw [e1, Real.exp_log (by norm_num : (0 : ℝ) < 1 / 8)]\n rw [h3l2] at h\n calc 4 * ((1 / 8) / Real.log 2) = 1 / (2 * Real.log 2) := by\n field_simp [Real.log_pos (by norm_num : (1 : ℝ) < 2)].ne'\n ring\n exact h.trans (by rw [h3l2])\n -- hmm, h's RHS after rw [h3l2] at h: (1/8)/log2; the calc shows 4·((1/8)/log2) = 1/(2 log2)\n -- step 4: the certified assembly\n have hlog2 : (0.6931471803 : ℝ) ≤ Real.log 2 := Real.log_two_gt_d9\n have h48 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) ≤ (7.6545 : ℝ) := by\n have hcge := cdog_gt\n have h1 : Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) ≤ 3.8073 / (2 * 0.2487) :=\n div_le_div exp_four_thirds_le (by linarith) (by norm_num) (by positivity)\n calc Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9))\n ≤ 3.8073 / (2 * 0.2487) := h1\n _ ≤ 7.6545 := by norm_num\n have h72 : 1 / (2 * Real.log 2) ≤ (0.7214 : ℝ) := by\n have h1 : 1 / (2 * Real.log 2) ≤ 1 / (2 * 0.6931471803) :=\n one_div_le_one_div_of_le (by positivity) (by linarith)\n calc 1 / (2 * Real.log 2) ≤ 1 / (2 * 0.6931471803) := h1\n _ ≤ 0.7214 := by norm_num\n have hC2 : dirichletC2 ≤ 1 := dirichletC2_le_one\n have hsum : dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +\n ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) ≤ (8.38 : ℝ) := by\n have hA0 : (0 : ℝ) ≤ Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) := by positivity\n have hB0 : (0 : ℝ) ≤ 1 / (2 * Real.log 2) := by positivity\n calc dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +\n ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ))\n ≤ 1 * (Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2)) := by\n apply mul_le_mul hC2 (add_le_add h3a h3b) (by positivity) (by norm_num)\n _ = Real.exp (4 / 3) / (2 * (Real.log 2 - 4 / 9)) + 1 / (2 * Real.log 2) := by ring\n _ ≤ 7.6545 + 0.7214 := add_le_add h48 h72\n _ ≤ 8.38 := by norm_num\n calc ‖HIntegral (Jlag n) 3 XR U‖\n ≤ ∫ σ in (3 : ℝ)..XR,\n (4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) + 4 * (2 : ℝ) ^ (-σ)) * dirichletC2 := h1\n _ = dirichletC2 * (∫ σ in (3 : ℝ)..XR, 4 * Real.exp (-(Real.log 2 - 4 / 9) * σ) +\n ∫ σ in (3 : ℝ)..XR, 4 * (2 : ℝ) ^ (-σ)) := h2\n _ ≤ 8.38 := hsum\n\nend NguyenRH1\n\nend"},"extra_content":null}]