← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (2950 chars)
The inner `apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)` — the goal is `Real.exp (5/2) + 1 ≤ 13.183` — that's NOT a division goal (X/2 ≤ Y/2)! The goal at that bullet is `(Real.exp (5/2) + 1) / 2 ≤ (13.183 : ℝ) / 2`?? — no — the goal shown is `Real.exp (5 / 2) + 1 ≤ 13.183` — so the bullet's goal IS the non-division form. My mul_le_mul's hcd goal: `(e^{5/2}+1) ≤ 13.183`?? — wait — the mul_le_mul's structure: `((√80000+1)/2)·(e^{5/2}+1) ≤ (284/2)·13.183` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) with c := e^{5/2}+1, d := 13.183: hcd : e^{5/2}+1 ≤ 13.183 — and my `apply div_le_div_of_nonneg_right _ (by norm_num : (0:ℝ) ≤ 2)` tries to prove `(e^{5/2}+1)/2 ≤ 13.183/2` but the goal is `e^{5/2}+1 ≤ 13.183` (no division!) — mismatch ✗.
Hmm — wait, the goal at that bullet is `Real.exp (5 / 2) + 1 ≤ 13.183` — so the mul_le_mul's c-side is e^{5/2}+1 (NOT (e^{5/2}+1)/2)!? — the h1 statement: `((√80000+1)/2)·(e^{5/2}+1)/2 ≤ (284/2)·(13.183)/2` — hmm — my h1 has the form `((√80000+1)/2)·((e^{5/2}+1)/2)` vs `(284/2)·(13.183/2)` — wait no — let me look at DogLegRight's def: `((Real.sqrt n + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + 8.38 + IIMaj n / 4` — so DogLegRight's first term is `((√n+1)/2)·(e^{5/2}+1)/2` — parses as `(((√n+1)/2)·(e^{5/2}+1))/2` ✓ — so h1's goal is `(((√80000+1)/2)·(e^{5/2}+1))/2 ≤ ((284/2)·13.183)/2` — X/2 ≤ Y/2 with X := ((√80000+1)/2)·(e^{5/2}+1), Y := (284/2)·13.183 ✓. Then `apply div_le_div_of_nonneg_right _ (by norm_num : (0:ℝ) ≤ 2)` at the OUTER level: X/2 ≤ Y/2 from X ≤ Y ✓ — the remaining goal is X ≤ Y: `((√80000+1)/2)·(e^{5/2}+1) ≤ (284/2)·13.183` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) with a := (√80000+1)/2, b := 284/2, c := e^{5/2}+1, d := 13.183: the hcd goal is `e^{5/2}+1 ≤ 13.183` ✓ — and my inner `apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)` on that goal — WRONG (it's not a division goal). Fix: `linarith [exp_five_halves_le]` directly for the hcd (e^{5/2}+1 ≤ 12.183+1 = 13.183 ✓):
```
apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)
apply mul_le_mul _ _ (by positivity) (by positivity)
· exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)
· linarith [exp_five_halves_le]
```
Wait — the mul_le_mul's hcd : e^{5/2}+1 ≤ 13.183 — linarith [exp_five_halves_le] (e^{5/2} ≤ 12.183 ⟹ +1 ≤ 13.183 ✓ linarith ✓).
Hmm — but the mul_le_mul's apply left TWO bullet goals (hab and hcd) or one? `apply mul_le_mul _ _ (by positivity) (by positivity)` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) — I passed `_ _ (by positivity) (by positivity)` — the first two `_` are hab and hcd (goals) ✓ then hc/hb by positivity ✓ — so the two `_` become bullet goals: `· exact div_le_div_of_nonneg_right hT2 ...` (hab) and `· linarith [exp_five_halves_le]` (hcd) ✓.
Wait — but does `apply mul_le_mul _ _ A B` leave the bullets in order (hab first, hcd second)? — the bullets come as separate goals in order ✓.
The inner goal is non-division — using `linarith` directly for the e^{5/2}+1 side.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
"old_string": " have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"new_string": " have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 linarith [exp_five_halves_le]\n linarith [h1, hII4]"
}
result 2026-08-26 12:40:42Z → 2026-08-26 12:40:42Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
"oldString": " have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"newString": " have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"originalFile": "/-\nNguyenRH1/LiBasePoints.lean \u2014 [PROVED] tier (ii) step 2 (session 012):\nthe two elementary margin evaluations consumed by\n`lambda_pos_finite_height`, discharged by certified rational interval\nbounds, and the resulting three-hypothesis headline form\n`lambda_pos_finite_height_verified` (perimeter + `SfBoundProp` only).\n\nPlan and validation: D-062 \u00a75 (every link pre-verified at dps 40 and by\nexact Fraction arithmetic; true values margin\u0303(8\u00d710\u2074) = 15 763.79 and\nmargin\u0303(10\u2075) \u2248 9.3\u00d710\u2074 from E-028/E-029-scale computations). All\ncertified targets carry explicit slack; the tightest link\n(e\u00b9\u00b7\u00b9\u2074\u2074\u2078 \u2265 \u03c0 at 0.007%) was replaced by the comfortable e\u00b9\u00b7\u00b9\u2075 \u2265 \u03c0\nat a ~104-unit cost, absorbed by the margin. The certified \u2265 8 001 is\ndeliberately coarser than the D-062 \u00a75 dps-40 plan's > 9 960 (outward\nrounding for norm_num comfort); both suffice \u2014 number-trail note filed\nin D-062 \u00a75.\n\nMachinery: exp upper bounds via exp x = (exp(x/16))\u00b9\u2076 \u2264 (1\u2212x/16)\u207b\u00b9\u2076\n(from 1 \u2212 y \u2264 e^{\u2212y}, Mathlib `Real.add_one_le_exp`); exp lower bounds\nvia partial sums (`Real.sum_le_exp_of_nonneg`) and the d9 rational\nbounds on e (`Real.exp_one_gt_d9/lt_d9`); log comparisons by\nmonotonicity through these; \u03c0 via `Real.pi_gt_d20/lt_d20`; log 2 via\n`Real.log_two_gt_d9/lt_d9`.\n-/\nimport Mathlib\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ### 1. Certified exp/log machinery -/\n\n/-- [PROVED session 012] exp x \u2264 (1 \u2212 x/16)\u207b\u00b9\u00b9\u2076 for 0 \u2264 x < 16:\nexp(x/16) \u2264 (1 \u2212 x/16)\u207b\u00b9 from 1 \u2212 y \u2264 e^{\u2212y}, then the 16th power. -/\ntheorem exp_le_inv_sub_sixteen {x : \u211d} (_hx0 : 0 \u2264 x) (hx1 : x < 16) :\n Real.exp x \u2264 (1 - x / 16)\u207b\u00b9 ^ 16 := by\n have h16 : ((16 : \u2115) : \u211d) \u2260 0 := by norm_num\n have hpos : (0 : \u211d) < 1 - x / 16 := by linarith\n have h1 : 1 - x / 16 \u2264 (Real.exp (x / 16))\u207b\u00b9 := by\n have h := Real.add_one_le_exp (-(x / 16))\n rw [Real.exp_neg] at h\n linarith\n have h2 : Real.exp (x / 16) \u2264 (1 - x / 16)\u207b\u00b9 := by\n have h3 := one_div_le_one_div_of_le hpos h1\n rwa [one_div, one_div, inv_inv] at h3\n have h4 : Real.exp x = (Real.exp (x / 16)) ^ 16 := by\n rw [\u2190 Real.exp_nat_mul (x / 16) 16]\n congr 1\n push_cast\n ring\n rw [h4]\n exact pow_le_pow_left\u2080 (Real.exp_nonneg _) h2 16\n\n/-- [PROVED session 012] Powers of e bounded by powers of the d9\nrationals. -/\ntheorem exp_one_pow_le (n : \u2115) : Real.exp 1 ^ n \u2264 (2.7182818286 : \u211d) ^ n :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le Real.exp_one_lt_d9.le n\n\ntheorem exp_one_pow_ge (n : \u2115) : (2.7182818283 : \u211d) ^ n \u2264 Real.exp 1 ^ n :=\n pow_le_pow_left\u2080 (by norm_num) Real.exp_one_gt_d9.le n\n\n/-- [PROVED session 012] Integer exponentials as powers of e. -/\ntheorem exp_eleven : Real.exp 11 = Real.exp 1 ^ 11 := by\n rw [\u2190 Real.exp_nat_mul 1 11]\n congr 1\n norm_num\n\ntheorem exp_five : Real.exp 5 = Real.exp 1 ^ 5 := by\n rw [\u2190 Real.exp_nat_mul 1 5]\n congr 1\n norm_num\n\ntheorem exp_four : Real.exp 4 = Real.exp 1 ^ 4 := by\n rw [\u2190 Real.exp_nat_mul 1 4]\n congr 1\n norm_num\n\n/-- [PROVED session 040] e^{5/2} \u2264 12.183 (via e\u00b3/e^{0.5} with the tight\ndivision-by-partial-sum route; D-074's V_left kernel constant). -/\ntheorem exp_five_halves_le : Real.exp (5 / 2) \u2264 (12.183 : \u211d) := by\n have h3 : Real.exp 3 \u2264 (20.0856 : \u211d) := by\n have e : Real.exp 3 = Real.exp 1 ^ 3 := by\n rw [\u2190 Real.exp_nat_mul 1 3]\n congr 1\n norm_num\n rw [e]\n exact le_trans (exp_one_pow_le 3) (by norm_num)\n have h05 : (1.6487 : \u211d) \u2264 Real.exp 0.5 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.5) 7)\n have h1 : Real.exp (5 / 2) = Real.exp 3 / Real.exp 0.5 := by\n rw [show (5 / 2 : \u211d) = 3 - 0.5 by norm_num, Real.exp_sub]\n rw [h1]\n calc Real.exp 3 / Real.exp 0.5 \u2264 20.0856 / 1.6487 :=\n div_le_div\u2080 (by norm_num) h3 (by norm_num) h05\n _ \u2264 12.183 := by norm_num\n\n/-! ### 2. Certified log bounds at the margin points -/\n\n/-- [PROVED session 012] log 80000 \u2265 11.263 (e\u00b9\u00b9\u00b7\u00b2\u2076\u00b3 \u2264 78057 < 80000). -/\ntheorem log80000_ge : (11.263 : \u211d) \u2264 Real.log 80000 := by\n have h1 : Real.exp 11 \u2264 (59874.31 : \u211d) := by\n rw [exp_eleven]\n exact le_trans (exp_one_pow_le 11) (by norm_num)\n have h2 : Real.exp 0.263 \u2264 (1.3037 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 11.263 = Real.exp 11 * Real.exp 0.263 := by\n rw [show (11.263 : \u211d) = 11 + 0.263 by norm_num, Real.exp_add]\n have h4 : Real.exp 11 * Real.exp 0.263 \u2264 59874.31 * 1.3037 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 11.263 \u2264 80000 := by\n rw [h3]\n exact le_trans h4 (by norm_num)\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log 80000 \u2264 11.3 (e\u00b9\u00b9\u00b7\u00b3 \u2265 80822 > 80000). -/\ntheorem log80000_le : Real.log 80000 \u2264 (11.3 : \u211d) := by\n have h1 : (59874.13 : \u211d) \u2264 Real.exp 11 := by\n rw [exp_eleven]\n exact le_trans (by norm_num) (exp_one_pow_ge 11)\n have h2 : (1.34985 : \u211d) \u2264 Real.exp 0.3 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.3) 7)\n have h3 : Real.exp 11.3 = Real.exp 11 * Real.exp 0.3 := by\n rw [show (11.3 : \u211d) = 11 + 0.3 by norm_num, Real.exp_add]\n have h4 : (80000 : \u211d) \u2264 Real.exp 11 * Real.exp 0.3 :=\n le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)\n have h5 : (80000 : \u211d) \u2264 Real.exp 11.3 := by\n rw [h3]\n exact h4\n have h6 := Real.log_le_log (by norm_num : (0 : \u211d) < 80000) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log 100000 \u2265 11.5 (e\u00b9\u00b9\u00b7\u2075 \u2264 99661 < 100000). -/\ntheorem log100000_ge : (11.5 : \u211d) \u2264 Real.log 100000 := by\n have h1 : Real.exp 11 \u2264 (59874.31 : \u211d) := by\n rw [exp_eleven]\n exact le_trans (exp_one_pow_le 11) (by norm_num)\n have h2 : Real.exp 0.5 \u2264 (1.6644 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 11.5 = Real.exp 11 * Real.exp 0.5 := by\n rw [show (11.5 : \u211d) = 11 + 0.5 by norm_num, Real.exp_add]\n have h4 : Real.exp 11 * Real.exp 0.5 \u2264 59874.31 * 1.6644 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 11.5 \u2264 100000 := by\n rw [h3]\n exact le_trans h4 (by norm_num)\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log \u03c0 \u2264 1.15 (e\u00b9\u00b7\u00b9\u2075 \u2265 3.1582 > \u03c0). -/\ntheorem logpi_le : Real.log Real.pi \u2264 (1.15 : \u211d) := by\n have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\n have h2 : (1.1618 : \u211d) \u2264 Real.exp 0.15 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.15) 7)\n have h3 : Real.exp 1.15 = Real.exp 1 * Real.exp 0.15 := by\n rw [show (1.15 : \u211d) = 1 + 0.15 by norm_num, Real.exp_add]\n have h4 : (3.1415926536 : \u211d) \u2264 Real.exp 1 * Real.exp 0.15 :=\n le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)\n have h5 : Real.pi \u2264 Real.exp 1.15 := by\n have hpi := Real.pi_lt_d20.le\n rw [h3]\n linarith\n have h6 := Real.log_le_log Real.pi_pos h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log \u03c0 \u2265 1.14 (e\u00b9\u00b7\u00b9\u2074 \u2264 3.1287 < \u03c0). -/\ntheorem logpi_ge : (1.14 : \u211d) \u2264 Real.log Real.pi := by\n have h1 : Real.exp 1 \u2264 (2.7182818286 : \u211d) := Real.exp_one_lt_d9.le\n have h2 : Real.exp 0.14 \u2264 (1.151 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 1.14 = Real.exp 1 * Real.exp 0.14 := by\n rw [show (1.14 : \u211d) = 1 + 0.14 by norm_num, Real.exp_add]\n have h4 : Real.exp 1 * Real.exp 0.14 \u2264 2.7182818286 * 1.151 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 1.14 \u2264 Real.pi := by\n have hpi := Real.pi_gt_d20.le\n rw [h3]\n linarith\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] \u221a80000 \u2264 283 (283\u00b2 = 80089). -/\ntheorem sqrt80000_le : Real.sqrt 80000 \u2264 283 :=\n (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a80000 \u2265 282 (282\u00b2 = 79524). -/\ntheorem sqrt80000_ge : (282 : \u211d) \u2264 Real.sqrt 80000 :=\n (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a100000 \u2264 317 (317\u00b2 = 100489). -/\ntheorem sqrt100000_le : Real.sqrt 100000 \u2264 317 :=\n (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a100000 \u2265 316 (316\u00b2 = 99856). -/\ntheorem sqrt100000_ge : (316 : \u211d) \u2264 Real.sqrt 100000 :=\n (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)\n\n/-! ### 3. The archimedean lower bound evaluated -/\n\n/-- [PROVED session 012] Normal form of sInftyLower: the \u03b3 cancels\nexactly (D-037 parity algebra at the point level). -/\ntheorem sInftyLower_eq' (n : \u211d) :\n sInftyLower n = (1 / 2) * n * Real.log n -\n ((1 + Real.log 2 + Real.log Real.pi) / 2) * n - 4 := by\n unfold sInftyLower lagariasC1\n rw [Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) Real.pi_ne_zero]\n ring\n\n/-- [PROVED session 012] sInftyLower(8\u00d710\u2074) \u2265 336000 (certified\n336 790; true 338 072). -/\ntheorem sInftyLower_80000_lo : (336000 : \u211d) \u2264 sInftyLower 80000 := by\n rw [sInftyLower_eq']\n have h1 := log80000_ge\n have h2 := Real.log_two_lt_d9.le\n have h3 := logpi_le\n have g1 : (1 / 2 : \u211d) * 80000 * 11.263 \u2264 (1 / 2) * 80000 * Real.log 80000 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 \u2264\n (2.8431472 / 2 : \u211d) * 80000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 80000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(8\u00d710\u2074) \u2264 339000 (certified\n338 671; true 338 072). -/\ntheorem sInftyLower_80000_up : sInftyLower 80000 \u2264 (339000 : \u211d) := by\n rw [sInftyLower_eq']\n have h1 := log80000_le\n have h2 := Real.log_two_gt_d9.le\n have h3 := logpi_ge\n have g1 : (1 / 2 : \u211d) * 80000 * Real.log 80000 \u2264 (1 / 2) * 80000 * 11.3 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((2.8331471 : \u211d) / 2) * 80000 \u2264\n ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 80000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(10\u2075) \u2265 432500 (certified\n432 839; true \u2248 433 747). -/\ntheorem sInftyLower_100000_lo : (432500 : \u211d) \u2264 sInftyLower 100000 := by\n rw [sInftyLower_eq']\n have h1 := log100000_ge\n have h2 := Real.log_two_lt_d9.le\n have h3 := logpi_le\n have g1 : (1 / 2 : \u211d) * 100000 * 11.5 \u2264 (1 / 2) * 100000 * Real.log 100000 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 100000 \u2264\n (2.8431472 / 2 : \u211d) * 100000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 100000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-! ### 4. The finite-part bound evaluated -/\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(8\u00d710\u2074) \u2264 332000 (certified \u2248 331 005; true\n\u2248 325 122 with the dog-leg Bn, E-034's exact Bn_DL = 324 913). -/\ntheorem Bn_FAlt_80000_le : Bn FAlt 80000 \u2264 (332000 : \u211d) := by\n have hT : Real.sqrt 80000 + 1 \u2264 284 := by\n have h := sqrt80000_le\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by\n have h := Real.sqrt_nonneg 80000\n linarith\n -- log T \u2264 5.7 (T \u2264 284 \u2264 e\u2075\u00b7\u2077 = e\u2075\u00b7e\u2070\u00b7\u2077, 148.328\u00b72.0136 = 298.674)\n have h5 : (148.328 : \u211d) \u2264 Real.exp 5 := by\n rw [exp_five]\n exact le_trans (by norm_num) (exp_one_pow_ge 5)\n have h07 : (2.0136 : \u211d) \u2264 Real.exp 0.7 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.7) 7)\n have h57 : Real.exp 5.7 = Real.exp 5 * Real.exp 0.7 := by\n rw [show (5.7 : \u211d) = 5 + 0.7 by norm_num, Real.exp_add]\n have h57big : (284 : \u211d) \u2264 Real.exp 5.7 := by\n rw [h57]\n exact le_trans (by norm_num : (284 : \u211d) \u2264 148.328 * 2.0136)\n (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)\n have hlogT : Real.log (Real.sqrt 80000 + 1) \u2264 (5.7 : \u211d) := by\n have h := Real.log_le_log hTpos (le_trans hT h57big)\n rwa [Real.log_exp] at h\n have h57big2 : (286 : \u211d) \u2264 Real.exp 5.7 := by\n rw [h57]\n exact le_trans (by norm_num : (286 : \u211d) \u2264 148.328 * 2.0136)\n (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)\n have hlogT2 : Real.log (Real.sqrt 80000 + 1 + 2) \u2264 (5.7 : \u211d) := by\n have hbig : Real.sqrt 80000 + 1 + 2 \u2264 Real.exp 5.7 := by\n have h : Real.sqrt 80000 + 1 + 2 \u2264 (286 : \u211d) := by linarith\n exact le_trans h h57big2\n have hT2pos : (0 : \u211d) < Real.sqrt 80000 + 1 + 2 := by linarith\n have h := Real.log_le_log hT2pos hbig\n rwa [Real.log_exp] at h\n -- log log T \u2264 1.75 (log T \u2264 5.7 \u2264 e\u00b9\u00b7\u2077\u2075 = e\u00b7e\u2070\u00b7\u2077\u2075, 2.7183\u00b72.1169)\n have h175 : Real.exp 1.75 = Real.exp 1 * Real.exp 0.75 := by\n rw [show (1.75 : \u211d) = 1 + 0.75 by norm_num, Real.exp_add]\n have h075 : (2.1169 : \u211d) \u2264 Real.exp 0.75 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.75) 7)\n have h175big : (5.7 : \u211d) \u2264 Real.exp 1.75 := by\n rw [h175]\n exact le_trans (by norm_num : (5.7 : \u211d) \u2264 2.7182818283 * 2.1169)\n (mul_le_mul Real.exp_one_gt_d9.le h075 (by norm_num) (Real.exp_pos _).le)\n have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) :=\n Real.log_pos (by linarith [sqrt80000_ge])\n have h := Real.log_le_log hlogTpos (le_trans hlogT h175big)\n rwa [Real.log_exp] at h\n have hloglogT2 : Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) \u2264 (1.75 : \u211d) := by\n have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1 + 2) :=\n Real.log_pos (by linarith [sqrt80000_ge])\n have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h175big)\n rwa [Real.log_exp] at h\n -- e\u2074 \u2264 54.6015\n have he4 : Real.exp 4 \u2264 (54.6015 : \u211d) := by\n rw [exp_four]\n exact le_trans (exp_one_pow_le 4) (by norm_num)\n -- 1/(2\u03c0) \u2264 1/6\n have h2pi : (1 : \u211d) / (2 * Real.pi) \u2264 1 / 6 := by\n apply one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6)\n have hpi := Real.pi_gt_d20.le\n linarith\n -- log T \u2265 0, log log T \u2265 0, log(T+2) \u2265 0, log log(T+2) \u2265 0\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])\n have hlogT2nn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n Real.log_nonneg hlogTge1\n have hlogT2ge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 + 2 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=\n Real.log_nonneg hlogT2ge1\n -- FAlt T \u2264 273.82\n have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n unfold FAlt\n have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264\n 284 * 5.7 :=\n mul_le_mul hT hlogT hlogTnn (by norm_num)\n have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n Real.log (Real.sqrt 80000 + 1)) \u2264 (1 / 6 : \u211d) * (284 * 5.7) :=\n mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)\n linarith [ha, hlogT, hloglogT]\n -- \u0108\u2080 T \u2264 6.9186 and \u2265 0\n have hC0 : C0hat (Real.sqrt 80000 + 1) \u2264 (6.9186 : \u211d) := by\n unfold C0hat\n linarith [hlogT2, hloglogT2]\n have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n unfold C0hat\n linarith [hlogT2nn, hloglogT2nn]\n -- H\u0302 T \u2264 251.46 and \u2265 0\n have hH : Hhat (Real.sqrt 80000 + 1) \u2264 (251.46 : \u211d) := by\n unfold Hhat\n have hsq : C0hat (Real.sqrt 80000 + 1) ^ 2 \u2264 6.9186 ^ 2 :=\n pow_le_pow_left\u2080 hC0pos hC0 2\n linarith [hsq, hlogT2]\n have hHnn : (0 : \u211d) \u2264 Hhat (Real.sqrt 80000 + 1) := by\n unfold Hhat\n have hsq : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 := pow_nonneg hC0pos 2\n linarith [hsq, hlogT2nn]\n -- Z\u2082 T \u2264 7.6705 and \u2265 0 (the corrected I_III count, D-071)\n have hZ2 : Z2hat (Real.sqrt 80000 + 1) \u2264 (7.6705 : \u211d) := by\n unfold Z2hat\n linarith [hlogT2, hloglogT2]\n have hZ2nn : (0 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n unfold Z2hat\n linarith [hlogT2nn, hloglogT2nn]\n -- the big bracket: 0 \u2264 \u00b7 \u2264 112.9637\n have hbr : (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 \u2264 112.9637 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hbrnn : (0 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n linarith [hZ2nn, hlogT2nn]\n -- IIMaj \u2264 2590.08\n have hII : IIMaj 80000 \u2264 (2590.08 : \u211d) := by\n refine le_trans (IIMaj_le_two_mul 80000 (by norm_num)) ?_\n have h3 : (4.56 : \u211d) * (Real.sqrt 80000 + 1) \u2264 4.56 * 284 :=\n mul_le_mul_of_nonneg_left (by linarith [sqrt80000_le]) (by norm_num)\n linarith [h3]\n -- the dog-leg share (D-074): 2\u00b7DogLegRight(8\u00d710\u2074) \u2264 3184 (certified)\n have hDL : 2 * DogLegRight 80000 \u2264 (3184 : \u211d) := by\n unfold DogLegRight\n have hT2 : Real.sqrt 80000 + 1 \u2264 284 := hT\n have hII4 : IIMaj 80000 / 4 \u2264 (2590.08 : \u211d) / 4 := by linarith [hII]\n have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]\n -- assemble\n simp only [Bn]\n have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) \u2264 4 * 284 * 112.9637 := by\n apply mul_le_mul _ hbr hbrnn (by norm_num)\n exact mul_le_mul_of_nonneg_left hT (by norm_num)\n have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) \u2264\n 2 * (54.6015 + 1) * (7 * 251.46) := by\n apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hH]\n linarith [hFAlt, hterm2, hterm4, hDL, hII]\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(8\u00d710\u2074) \u2265 273000 (the lower side only needs\nthe two big terms; the dog-leg share is nonneg). -/\ntheorem Bn_FAlt_80000_ge : (273000 : \u211d) \u2264 Bn FAlt 80000 := by\n have hTge : (283 : \u211d) \u2264 Real.sqrt 80000 + 1 := by\n have h := sqrt80000_ge\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by linarith\n -- log (T+2) \u2265 5.6 (T+2 \u2265 285 \u2265 e\u2075\u00b7\u2076 = e\u2075\u00b7e\u2070\u00b7\u2076, 148.414\u00b71.8433 = 273.571)\n have h5up : Real.exp 5 \u2264 (148.414 : \u211d) := by\n rw [exp_five]\n exact le_trans (exp_one_pow_le 5) (by norm_num)\n have h06up : Real.exp 0.6 \u2264 (1.8433 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h56 : Real.exp 5.6 = Real.exp 5 * Real.exp 0.6 := by\n rw [show (5.6 : \u211d) = 5 + 0.6 by norm_num, Real.exp_add]\n have h56small : Real.exp 5.6 \u2264 (285 : \u211d) := by\n rw [h56]\n exact le_trans (mul_le_mul h5up h06up (Real.exp_pos _).le (by norm_num))\n (by norm_num)\n have hlogT2ge : (5.6 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) := by\n have hbig : (285 : \u211d) \u2264 Real.sqrt 80000 + 1 + 2 := by linarith\n have h1 : (5.6 : \u211d) \u2264 Real.log 285 := by\n have h := Real.log_le_log (Real.exp_pos _) h56small\n rwa [Real.log_exp] at h\n exact le_trans h1 (Real.log_le_log (by norm_num : (0 : \u211d) < 285) hbig)\n -- log log (T+2) \u2265 0 (log (T+2) \u2265 5.6 \u2265 1)\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=\n Real.log_nonneg (by linarith)\n -- log T \u2265 0 and log log T \u2265 0 (T \u2265 283 \u2265 e)\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n Real.log_nonneg (by linarith)\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith)\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n Real.log_nonneg hlogTge1\n -- FAlt T \u2265 0 (every term nonneg)\n have hFAlt0 : (0 : \u211d) \u2264 FAlt (Real.sqrt 80000 + 1) := by\n unfold FAlt\n have hpi : (0 : \u211d) < Real.pi := Real.pi_pos\n have hp1 : (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n Real.log (Real.sqrt 80000 + 1)) :=\n mul_nonneg (by positivity) (mul_nonneg hTpos.le hlogTnn)\n have hp2 : (0 : \u211d) \u2264 0.137 * Real.log (Real.sqrt 80000 + 1) :=\n mul_nonneg (by norm_num) hlogTnn\n have hp3 : (0 : \u211d) \u2264 0.443 * Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n mul_nonneg (by norm_num) hloglogTnn\n linarith [hp1, hp2, hp3]\n -- \u0108\u2080 T \u2265 5.3248\n have hC0lo : (5.3248 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n unfold C0hat\n linarith [hlogT2ge, hloglogT2nn]\n -- H\u0302 T \u2265 191.85\n have hHlo : (191.85 : \u211d) \u2264 Hhat (Real.sqrt 80000 + 1) := by\n unfold Hhat\n have hsq : (5.3248 : \u211d) ^ 2 \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 :=\n pow_le_pow_left\u2080 (by norm_num) hC0lo 2\n linarith [hsq, hlogT2ge]\n -- e\u2074 \u2265 54.5978\n have he4 : (54.5978 : \u211d) \u2264 Real.exp 4 := by\n rw [exp_four]\n exact le_trans (by norm_num) (exp_one_pow_ge 4)\n -- assemble\n simp only [Bn]\n -- Z\u2082 T \u2265 6.06 (0.6\u00b75.6 + 0 + 2.7; log log \u2265 0; the corrected count, D-071)\n have hZ2lo : (6.06 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n unfold Z2hat\n linarith [hlogT2ge, hloglogT2nn]\n have hbrlo : (110.84 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2lo (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2ge (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hterm2 : (4 * 283 * 110.84 : \u211d) \u2264 4 * (Real.sqrt 80000 + 1) *\n ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) := by\n apply mul_le_mul _ hbrlo (by norm_num) (by positivity)\n exact mul_le_mul_of_nonneg_left hTge (by norm_num)\n have hterm4 : (2 * (54.5978 + 1) * (7 * 191.85) : \u211d) \u2264\n 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) := by\n apply mul_le_mul _ _ (by norm_num) (by positivity)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hHlo]\n have hII : (0 : \u211d) \u2264 IIMaj 80000 := IIMaj_nonneg 80000\n have hDLnn : (0 : \u211d) \u2264 2 * DogLegRight 80000 := by\n unfold DogLegRight\n have hIIMnn := hII\n positivity\n linarith [hFAlt0, hterm2, hterm4, hII, hDLnn]\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(10\u2075) \u2264 352000 (certified \u2248 351 367; true\n\u2248 333 700 with the dog-leg Bn, E-034's exact Bn_DL = 344 838). -/\ntheorem Bn_FAlt_100000_le : Bn FAlt 100000 \u2264 (352000 : \u211d) := by\n have hT : Real.sqrt 100000 + 1 \u2264 318 := by\n have h := sqrt100000_le\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 100000 + 1 := by\n have h := Real.sqrt_nonneg 100000\n linarith\n -- log T \u2264 5.8 (T \u2264 318 \u2264 e\u2075\u00b7\u2078 = e\u2075\u00b7e\u2070\u00b7\u2078, 148.328\u00b72.2254 = 330.087)\n have h5 : (148.328 : \u211d) \u2264 Real.exp 5 := by\n rw [exp_five]\n exact le_trans (by norm_num) (exp_one_pow_ge 5)\n have h08 : (2.2254 : \u211d) \u2264 Real.exp 0.8 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.8) 7)\n have h58 : Real.exp 5.8 = Real.exp 5 * Real.exp 0.8 := by\n rw [show (5.8 : \u211d) = 5 + 0.8 by norm_num, Real.exp_add]\n have h58big : (320 : \u211d) \u2264 Real.exp 5.8 := by\n rw [h58]\n exact le_trans (by norm_num : (320 : \u211d) \u2264 148.328 * 2.2254)\n (mul_le_mul h5 h08 (by norm_num) (Real.exp_pos _).le)\n have hlogT : Real.log (Real.sqrt 100000 + 1) \u2264 (5.8 : \u211d) := by\n have h := Real.log_le_log hTpos (le_trans hT (le_trans (by norm_num :\n (318 : \u211d) \u2264 320) h58big))\n rwa [Real.log_exp] at h\n have hlogT2 : Real.log (Real.sqrt 100000 + 1 + 2) \u2264 (5.8 : \u211d) := by\n have hbig : Real.sqrt 100000 + 1 + 2 \u2264 Real.exp 5.8 := by\n have h : Real.sqrt 100000 + 1 + 2 \u2264 (320 : \u211d) := by linarith\n exact le_trans h h58big\n have hT2pos : (0 : \u211d) < Real.sqrt 100000 + 1 + 2 := by linarith\n have h := Real.log_le_log hT2pos hbig\n rwa [Real.log_exp] at h\n -- log log \u2264 1.77 (log \u2264 5.8 \u2264 e\u00b9\u00b7\u2077\u2077 = e\u00b7e\u2070\u00b7\u2077\u2077, 2.7183\u00b72.1597 = 5.8707)\n have h177 : Real.exp 1.77 = Real.exp 1 * Real.exp 0.77 := by\n rw [show (1.77 : \u211d) = 1 + 0.77 by norm_num, Real.exp_add]\n have h077 : (2.1597 : \u211d) \u2264 Real.exp 0.77 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.77) 7)\n have h177big : (5.8 : \u211d) \u2264 Real.exp 1.77 := by\n rw [h177]\n exact le_trans (by norm_num : (5.8 : \u211d) \u2264 2.7182818283 * 2.1597)\n (mul_le_mul Real.exp_one_gt_d9.le h077 (by norm_num) (Real.exp_pos _).le)\n have hloglogT : Real.log (Real.log (Real.sqrt 100000 + 1)) \u2264 (1.77 : \u211d) := by\n have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 100000 + 1) :=\n Real.log_pos (by linarith [sqrt100000_ge])\n have h := Real.log_le_log hlogTpos (le_trans hlogT h177big)\n rwa [Real.log_exp] at h\n have hloglogT2 : Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) \u2264 (1.77 : \u211d) := by\n have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 100000 + 1 + 2) :=\n Real.log_pos (by linarith [sqrt100000_ge])\n have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h177big)\n rwa [Real.log_exp] at h\n -- e\u2074 \u2264 54.6015\n have he4 : Real.exp 4 \u2264 (54.6015 : \u211d) := by\n rw [exp_four]\n exact le_trans (exp_one_pow_le 4) (by norm_num)\n -- 1/(2\u03c0) \u2264 1/6\n have h2pi : (1 : \u211d) / (2 * Real.pi) \u2264 1 / 6 := by\n apply one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6)\n have hpi := Real.pi_gt_d20.le\n linarith\n -- nonnegativity pieces\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])\n have hlogT2nn : (0 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1 + 2) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 100000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 100000 + 1)) :=\n Real.log_nonneg hlogTge1\n have hlogT2ge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1 + 2) := by\n have he : Real.exp 1 \u2264 Real.sqrt 100000 + 1 + 2 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) :=\n Real.log_nonneg hlogT2ge1\n -- FAlt T \u2264 311.45\n have hFAlt : FAlt (Real.sqrt 100000 + 1) \u2264 (311.45 : \u211d) := by\n unfold FAlt\n have hTl : (Real.sqrt 100000 + 1) * Real.log (Real.sqrt 100000 + 1) \u2264\n 318 * 5.8 :=\n mul_le_mul hT hlogT hlogTnn (by norm_num)\n have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 100000 + 1) *\n Real.log (Real.sqrt 100000 + 1)) \u2264 (1 / 6 : \u211d) * (318 * 5.8) :=\n mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)\n linarith [ha, hlogT, hloglogT]\n -- \u0108\u2080 T \u2264 6.9797 and \u2265 0\n have hC0 : C0hat (Real.sqrt 100000 + 1) \u2264 (6.9797 : \u211d) := by\n unfold C0hat\n linarith [hlogT2, hloglogT2]\n have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 100000 + 1) := by\n unfold C0hat\n linarith [hlogT2nn, hloglogT2nn]\n -- H\u0302 T \u2264 255.05 and \u2265 0\n have hH : Hhat (Real.sqrt 100000 + 1) \u2264 (255.05 : \u211d) := by\n unfold Hhat\n have hsq : C0hat (Real.sqrt 100000 + 1) ^ 2 \u2264 6.9797 ^ 2 :=\n pow_le_pow_left\u2080 hC0pos hC0 2\n linarith [hsq, hlogT2]\n have hHnn : (0 : \u211d) \u2264 Hhat (Real.sqrt 100000 + 1) := by\n unfold Hhat\n have hsq : (0 : \u211d) \u2264 C0hat (Real.sqrt 100000 + 1) ^ 2 := pow_nonneg hC0pos 2\n linarith [hsq, hlogT2nn]\n -- Z\u2082 T \u2264 7.7483 and \u2265 0 (the corrected I_III count, D-071)\n have hZ2 : Z2hat (Real.sqrt 100000 + 1) \u2264 (7.7483 : \u211d) := by\n unfold Z2hat\n linarith [hlogT2, hloglogT2]\n have hZ2nn : (0 : \u211d) \u2264 Z2hat (Real.sqrt 100000 + 1) := by\n unfold Z2hat\n linarith [hlogT2nn, hloglogT2nn]\n -- the big bracket: 0 \u2264 \u00b7 \u2264 114.0655\n have hbr : (2 / 3 : \u211d) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 \u2264 114.0656 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hbrnn : (0 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 := by\n linarith [hZ2nn, hlogT2nn]\n -- IIMaj \u2264 2900.16\n have hII : IIMaj 100000 \u2264 (2900.16 : \u211d) := by\n refine le_trans (IIMaj_le_two_mul 100000 (by norm_num)) ?_\n have h3 : (4.56 : \u211d) * (Real.sqrt 100000 + 1) \u2264 4.56 * 318 :=\n mul_le_mul_of_nonneg_left (by linarith [sqrt100000_le]) (by norm_num)\n linarith [h3]\n -- the dog-leg share (D-074): 2\u00b7DogLegRight(10\u2075) \u2264 3564 (certified)\n have hDL : 2 * DogLegRight 100000 \u2264 (3564 : \u211d) := by\n unfold DogLegRight\n have hT2 : Real.sqrt 100000 + 1 \u2264 318 := hT\n have hII4 : IIMaj 100000 / 4 \u2264 (2900.16 : \u211d) / 4 := by linarith [hII]\n have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]\n -- assemble\n simp only [Bn]\n have hterm2 : 4 * (Real.sqrt 100000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48) \u2264 4 * 318 * 114.0656 := by\n apply mul_le_mul _ hbr hbrnn (by norm_num)\n exact mul_le_mul_of_nonneg_left hT (by norm_num)\n have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 100000 + 1)) \u2264\n 2 * (54.6015 + 1) * (7 * 255.05) := by\n apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hH]\n linarith [hFAlt, hterm2, hterm4, hDL, hII]\n\n/-! ### 5. The two base points and the final three-hypothesis form -/\n\n/-- [PROVED session 012; values updated session 038 for the D-071\ncorrection] hbase: margin\u0303(8\u00d710\u2074) > 0. Certified: sInftyLower \u2265 336 000,\nBn \u2264 329 000 \u27f9 margin \u2265 7 001 (true 14 682 with the corrected Bn). -/\ntheorem marginTilde_FAlt_80000_pos : 0 < marginTilde FAlt 80000 := by\n rw [marginTilde_eq_sub]\n have hS := sInftyLower_80000_lo\n have hB := Bn_FAlt_80000_le\n linarith\n\n/-- [PROVED session 012; values updated session 038 for the D-071\ncorrection] hbase2: margin\u0303(8\u00d710\u2074) < margin\u0303(10\u2075).\nCertified: margin\u0303(8\u00d710\u2074) \u2264 339 000 \u2212 274 000 + 1 = 65 001 and\nmargin\u0303(10\u2075) \u2265 432 500 \u2212 350 000 + 1 = 82 501. -/\ntheorem marginTilde_FAlt_80000_lt_100000 :\n marginTilde FAlt 80000 < marginTilde FAlt 100000 := by\n rw [marginTilde_eq_sub, marginTilde_eq_sub]\n have h1 := sInftyLower_80000_up\n have h2 := Bn_FAlt_80000_ge\n have h3 := sInftyLower_100000_lo\n have h4 := Bn_FAlt_100000_le\n linarith\n\n/-- [PROVED session 012 \u2014 TIER (ii) STEP 2] R-004, the finite-height Li\ntheorem, in its final assembly form: machine-verified modulo ONE named\nanalytic hypothesis (`SfBoundProp`, the traced contour bound) plus the\ndeclared computational perimeter (Platt\u2013Trudgian `RHUpTo`; the finite Li\nverification `LiVerifiedUpTo`). The two elementary margin evaluations\nare discharged in this file. -/\ntheorem lambda_pos_finite_height_verified\n (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hSf : SfBoundProp) :\n \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n 0 < (liCoeff n).re :=\n fun n hn1 hnN => lambda_pos_finite_height hRH hfinite\n marginTilde_FAlt_80000_pos marginTilde_FAlt_80000_lt_100000 hSf n hn1 hnN\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 406,
"oldLines": 8,
"newStart": 406,
"newLines": 7,
"lines": [
" apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)",
" apply mul_le_mul _ _ (by positivity) (by positivity)",
" \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)",
"- \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)",
"- linarith [exp_five_halves_le]",
"+ \u00b7 linarith [exp_five_halves_le]",
" linarith [h1, hII4]",
" -- assemble",
" simp only [Bn]"
]
}
],
"userModified": false,
"replaceAll": false
}
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
"old_string": " have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"new_string": " have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 linarith [exp_five_halves_le]\n linarith [h1, hII4]"
}
result 2026-08-26 12:40:42Z → 2026-08-26 12:40:42Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
"oldString": " have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"newString": " have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 linarith [exp_five_halves_le]\n linarith [h1, hII4]",
"originalFile": "/-\nNguyenRH1/LiBasePoints.lean \u2014 [PROVED] tier (ii) step 2 (session 012):\nthe two elementary margin evaluations consumed by\n`lambda_pos_finite_height`, discharged by certified rational interval\nbounds, and the resulting three-hypothesis headline form\n`lambda_pos_finite_height_verified` (perimeter + `SfBoundProp` only).\n\nPlan and validation: D-062 \u00a75 (every link pre-verified at dps 40 and by\nexact Fraction arithmetic; true values margin\u0303(8\u00d710\u2074) = 15 763.79 and\nmargin\u0303(10\u2075) \u2248 9.3\u00d710\u2074 from E-028/E-029-scale computations). All\ncertified targets carry explicit slack; the tightest link\n(e\u00b9\u00b7\u00b9\u2074\u2074\u2078 \u2265 \u03c0 at 0.007%) was replaced by the comfortable e\u00b9\u00b7\u00b9\u2075 \u2265 \u03c0\nat a ~104-unit cost, absorbed by the margin. The certified \u2265 8 001 is\ndeliberately coarser than the D-062 \u00a75 dps-40 plan's > 9 960 (outward\nrounding for norm_num comfort); both suffice \u2014 number-trail note filed\nin D-062 \u00a75.\n\nMachinery: exp upper bounds via exp x = (exp(x/16))\u00b9\u2076 \u2264 (1\u2212x/16)\u207b\u00b9\u2076\n(from 1 \u2212 y \u2264 e^{\u2212y}, Mathlib `Real.add_one_le_exp`); exp lower bounds\nvia partial sums (`Real.sum_le_exp_of_nonneg`) and the d9 rational\nbounds on e (`Real.exp_one_gt_d9/lt_d9`); log comparisons by\nmonotonicity through these; \u03c0 via `Real.pi_gt_d20/lt_d20`; log 2 via\n`Real.log_two_gt_d9/lt_d9`.\n-/\nimport Mathlib\nimport NguyenRH1.LiSkeleton\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ### 1. Certified exp/log machinery -/\n\n/-- [PROVED session 012] exp x \u2264 (1 \u2212 x/16)\u207b\u00b9\u00b9\u2076 for 0 \u2264 x < 16:\nexp(x/16) \u2264 (1 \u2212 x/16)\u207b\u00b9 from 1 \u2212 y \u2264 e^{\u2212y}, then the 16th power. -/\ntheorem exp_le_inv_sub_sixteen {x : \u211d} (_hx0 : 0 \u2264 x) (hx1 : x < 16) :\n Real.exp x \u2264 (1 - x / 16)\u207b\u00b9 ^ 16 := by\n have h16 : ((16 : \u2115) : \u211d) \u2260 0 := by norm_num\n have hpos : (0 : \u211d) < 1 - x / 16 := by linarith\n have h1 : 1 - x / 16 \u2264 (Real.exp (x / 16))\u207b\u00b9 := by\n have h := Real.add_one_le_exp (-(x / 16))\n rw [Real.exp_neg] at h\n linarith\n have h2 : Real.exp (x / 16) \u2264 (1 - x / 16)\u207b\u00b9 := by\n have h3 := one_div_le_one_div_of_le hpos h1\n rwa [one_div, one_div, inv_inv] at h3\n have h4 : Real.exp x = (Real.exp (x / 16)) ^ 16 := by\n rw [\u2190 Real.exp_nat_mul (x / 16) 16]\n congr 1\n push_cast\n ring\n rw [h4]\n exact pow_le_pow_left\u2080 (Real.exp_nonneg _) h2 16\n\n/-- [PROVED session 012] Powers of e bounded by powers of the d9\nrationals. -/\ntheorem exp_one_pow_le (n : \u2115) : Real.exp 1 ^ n \u2264 (2.7182818286 : \u211d) ^ n :=\n pow_le_pow_left\u2080 (Real.exp_pos 1).le Real.exp_one_lt_d9.le n\n\ntheorem exp_one_pow_ge (n : \u2115) : (2.7182818283 : \u211d) ^ n \u2264 Real.exp 1 ^ n :=\n pow_le_pow_left\u2080 (by norm_num) Real.exp_one_gt_d9.le n\n\n/-- [PROVED session 012] Integer exponentials as powers of e. -/\ntheorem exp_eleven : Real.exp 11 = Real.exp 1 ^ 11 := by\n rw [\u2190 Real.exp_nat_mul 1 11]\n congr 1\n norm_num\n\ntheorem exp_five : Real.exp 5 = Real.exp 1 ^ 5 := by\n rw [\u2190 Real.exp_nat_mul 1 5]\n congr 1\n norm_num\n\ntheorem exp_four : Real.exp 4 = Real.exp 1 ^ 4 := by\n rw [\u2190 Real.exp_nat_mul 1 4]\n congr 1\n norm_num\n\n/-- [PROVED session 040] e^{5/2} \u2264 12.183 (via e\u00b3/e^{0.5} with the tight\ndivision-by-partial-sum route; D-074's V_left kernel constant). -/\ntheorem exp_five_halves_le : Real.exp (5 / 2) \u2264 (12.183 : \u211d) := by\n have h3 : Real.exp 3 \u2264 (20.0856 : \u211d) := by\n have e : Real.exp 3 = Real.exp 1 ^ 3 := by\n rw [\u2190 Real.exp_nat_mul 1 3]\n congr 1\n norm_num\n rw [e]\n exact le_trans (exp_one_pow_le 3) (by norm_num)\n have h05 : (1.6487 : \u211d) \u2264 Real.exp 0.5 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.5) 7)\n have h1 : Real.exp (5 / 2) = Real.exp 3 / Real.exp 0.5 := by\n rw [show (5 / 2 : \u211d) = 3 - 0.5 by norm_num, Real.exp_sub]\n rw [h1]\n calc Real.exp 3 / Real.exp 0.5 \u2264 20.0856 / 1.6487 :=\n div_le_div\u2080 (by norm_num) h3 (by norm_num) h05\n _ \u2264 12.183 := by norm_num\n\n/-! ### 2. Certified log bounds at the margin points -/\n\n/-- [PROVED session 012] log 80000 \u2265 11.263 (e\u00b9\u00b9\u00b7\u00b2\u2076\u00b3 \u2264 78057 < 80000). -/\ntheorem log80000_ge : (11.263 : \u211d) \u2264 Real.log 80000 := by\n have h1 : Real.exp 11 \u2264 (59874.31 : \u211d) := by\n rw [exp_eleven]\n exact le_trans (exp_one_pow_le 11) (by norm_num)\n have h2 : Real.exp 0.263 \u2264 (1.3037 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 11.263 = Real.exp 11 * Real.exp 0.263 := by\n rw [show (11.263 : \u211d) = 11 + 0.263 by norm_num, Real.exp_add]\n have h4 : Real.exp 11 * Real.exp 0.263 \u2264 59874.31 * 1.3037 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 11.263 \u2264 80000 := by\n rw [h3]\n exact le_trans h4 (by norm_num)\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log 80000 \u2264 11.3 (e\u00b9\u00b9\u00b7\u00b3 \u2265 80822 > 80000). -/\ntheorem log80000_le : Real.log 80000 \u2264 (11.3 : \u211d) := by\n have h1 : (59874.13 : \u211d) \u2264 Real.exp 11 := by\n rw [exp_eleven]\n exact le_trans (by norm_num) (exp_one_pow_ge 11)\n have h2 : (1.34985 : \u211d) \u2264 Real.exp 0.3 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.3) 7)\n have h3 : Real.exp 11.3 = Real.exp 11 * Real.exp 0.3 := by\n rw [show (11.3 : \u211d) = 11 + 0.3 by norm_num, Real.exp_add]\n have h4 : (80000 : \u211d) \u2264 Real.exp 11 * Real.exp 0.3 :=\n le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)\n have h5 : (80000 : \u211d) \u2264 Real.exp 11.3 := by\n rw [h3]\n exact h4\n have h6 := Real.log_le_log (by norm_num : (0 : \u211d) < 80000) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log 100000 \u2265 11.5 (e\u00b9\u00b9\u00b7\u2075 \u2264 99661 < 100000). -/\ntheorem log100000_ge : (11.5 : \u211d) \u2264 Real.log 100000 := by\n have h1 : Real.exp 11 \u2264 (59874.31 : \u211d) := by\n rw [exp_eleven]\n exact le_trans (exp_one_pow_le 11) (by norm_num)\n have h2 : Real.exp 0.5 \u2264 (1.6644 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 11.5 = Real.exp 11 * Real.exp 0.5 := by\n rw [show (11.5 : \u211d) = 11 + 0.5 by norm_num, Real.exp_add]\n have h4 : Real.exp 11 * Real.exp 0.5 \u2264 59874.31 * 1.6644 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 11.5 \u2264 100000 := by\n rw [h3]\n exact le_trans h4 (by norm_num)\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log \u03c0 \u2264 1.15 (e\u00b9\u00b7\u00b9\u2075 \u2265 3.1582 > \u03c0). -/\ntheorem logpi_le : Real.log Real.pi \u2264 (1.15 : \u211d) := by\n have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\n have h2 : (1.1618 : \u211d) \u2264 Real.exp 0.15 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.15) 7)\n have h3 : Real.exp 1.15 = Real.exp 1 * Real.exp 0.15 := by\n rw [show (1.15 : \u211d) = 1 + 0.15 by norm_num, Real.exp_add]\n have h4 : (3.1415926536 : \u211d) \u2264 Real.exp 1 * Real.exp 0.15 :=\n le_trans (by norm_num) (mul_le_mul h1 h2 (by norm_num) (Real.exp_pos _).le)\n have h5 : Real.pi \u2264 Real.exp 1.15 := by\n have hpi := Real.pi_lt_d20.le\n rw [h3]\n linarith\n have h6 := Real.log_le_log Real.pi_pos h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] log \u03c0 \u2265 1.14 (e\u00b9\u00b7\u00b9\u2074 \u2264 3.1287 < \u03c0). -/\ntheorem logpi_ge : (1.14 : \u211d) \u2264 Real.log Real.pi := by\n have h1 : Real.exp 1 \u2264 (2.7182818286 : \u211d) := Real.exp_one_lt_d9.le\n have h2 : Real.exp 0.14 \u2264 (1.151 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h3 : Real.exp 1.14 = Real.exp 1 * Real.exp 0.14 := by\n rw [show (1.14 : \u211d) = 1 + 0.14 by norm_num, Real.exp_add]\n have h4 : Real.exp 1 * Real.exp 0.14 \u2264 2.7182818286 * 1.151 :=\n mul_le_mul h1 h2 (Real.exp_pos _).le (by norm_num)\n have h5 : Real.exp 1.14 \u2264 Real.pi := by\n have hpi := Real.pi_gt_d20.le\n rw [h3]\n linarith\n have h6 := Real.log_le_log (Real.exp_pos _) h5\n rwa [Real.log_exp] at h6\n\n/-- [PROVED session 012] \u221a80000 \u2264 283 (283\u00b2 = 80089). -/\ntheorem sqrt80000_le : Real.sqrt 80000 \u2264 283 :=\n (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a80000 \u2265 282 (282\u00b2 = 79524). -/\ntheorem sqrt80000_ge : (282 : \u211d) \u2264 Real.sqrt 80000 :=\n (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a100000 \u2264 317 (317\u00b2 = 100489). -/\ntheorem sqrt100000_le : Real.sqrt 100000 \u2264 317 :=\n (Real.sqrt_le_left (by norm_num)).mpr (by norm_num)\n\n/-- [PROVED session 012] \u221a100000 \u2265 316 (316\u00b2 = 99856). -/\ntheorem sqrt100000_ge : (316 : \u211d) \u2264 Real.sqrt 100000 :=\n (Real.le_sqrt (by norm_num) (by norm_num)).mpr (by norm_num)\n\n/-! ### 3. The archimedean lower bound evaluated -/\n\n/-- [PROVED session 012] Normal form of sInftyLower: the \u03b3 cancels\nexactly (D-037 parity algebra at the point level). -/\ntheorem sInftyLower_eq' (n : \u211d) :\n sInftyLower n = (1 / 2) * n * Real.log n -\n ((1 + Real.log 2 + Real.log Real.pi) / 2) * n - 4 := by\n unfold sInftyLower lagariasC1\n rw [Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) Real.pi_ne_zero]\n ring\n\n/-- [PROVED session 012] sInftyLower(8\u00d710\u2074) \u2265 336000 (certified\n336 790; true 338 072). -/\ntheorem sInftyLower_80000_lo : (336000 : \u211d) \u2264 sInftyLower 80000 := by\n rw [sInftyLower_eq']\n have h1 := log80000_ge\n have h2 := Real.log_two_lt_d9.le\n have h3 := logpi_le\n have g1 : (1 / 2 : \u211d) * 80000 * 11.263 \u2264 (1 / 2) * 80000 * Real.log 80000 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 \u2264\n (2.8431472 / 2 : \u211d) * 80000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 80000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(8\u00d710\u2074) \u2264 339000 (certified\n338 671; true 338 072). -/\ntheorem sInftyLower_80000_up : sInftyLower 80000 \u2264 (339000 : \u211d) := by\n rw [sInftyLower_eq']\n have h1 := log80000_le\n have h2 := Real.log_two_gt_d9.le\n have h3 := logpi_ge\n have g1 : (1 / 2 : \u211d) * 80000 * Real.log 80000 \u2264 (1 / 2) * 80000 * 11.3 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((2.8331471 : \u211d) / 2) * 80000 \u2264\n ((1 + Real.log 2 + Real.log Real.pi) / 2) * 80000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 80000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(10\u2075) \u2265 432500 (certified\n432 839; true \u2248 433 747). -/\ntheorem sInftyLower_100000_lo : (432500 : \u211d) \u2264 sInftyLower 100000 := by\n rw [sInftyLower_eq']\n have h1 := log100000_ge\n have h2 := Real.log_two_lt_d9.le\n have h3 := logpi_le\n have g1 : (1 / 2 : \u211d) * 100000 * 11.5 \u2264 (1 / 2) * 100000 * Real.log 100000 :=\n mul_le_mul_of_nonneg_left h1 (by norm_num)\n have g2 : ((1 + Real.log 2 + Real.log Real.pi) / 2) * 100000 \u2264\n (2.8431472 / 2 : \u211d) * 100000 := by\n apply mul_le_mul_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 100000)\n rw [div_le_div_iff_of_pos_right (by norm_num : (0 : \u211d) < 2)]\n linarith\n linarith [g1, g2]\n\n/-! ### 4. The finite-part bound evaluated -/\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(8\u00d710\u2074) \u2264 332000 (certified \u2248 331 005; true\n\u2248 325 122 with the dog-leg Bn, E-034's exact Bn_DL = 324 913). -/\ntheorem Bn_FAlt_80000_le : Bn FAlt 80000 \u2264 (332000 : \u211d) := by\n have hT : Real.sqrt 80000 + 1 \u2264 284 := by\n have h := sqrt80000_le\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by\n have h := Real.sqrt_nonneg 80000\n linarith\n -- log T \u2264 5.7 (T \u2264 284 \u2264 e\u2075\u00b7\u2077 = e\u2075\u00b7e\u2070\u00b7\u2077, 148.328\u00b72.0136 = 298.674)\n have h5 : (148.328 : \u211d) \u2264 Real.exp 5 := by\n rw [exp_five]\n exact le_trans (by norm_num) (exp_one_pow_ge 5)\n have h07 : (2.0136 : \u211d) \u2264 Real.exp 0.7 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.7) 7)\n have h57 : Real.exp 5.7 = Real.exp 5 * Real.exp 0.7 := by\n rw [show (5.7 : \u211d) = 5 + 0.7 by norm_num, Real.exp_add]\n have h57big : (284 : \u211d) \u2264 Real.exp 5.7 := by\n rw [h57]\n exact le_trans (by norm_num : (284 : \u211d) \u2264 148.328 * 2.0136)\n (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)\n have hlogT : Real.log (Real.sqrt 80000 + 1) \u2264 (5.7 : \u211d) := by\n have h := Real.log_le_log hTpos (le_trans hT h57big)\n rwa [Real.log_exp] at h\n have h57big2 : (286 : \u211d) \u2264 Real.exp 5.7 := by\n rw [h57]\n exact le_trans (by norm_num : (286 : \u211d) \u2264 148.328 * 2.0136)\n (mul_le_mul h5 h07 (by norm_num) (Real.exp_pos _).le)\n have hlogT2 : Real.log (Real.sqrt 80000 + 1 + 2) \u2264 (5.7 : \u211d) := by\n have hbig : Real.sqrt 80000 + 1 + 2 \u2264 Real.exp 5.7 := by\n have h : Real.sqrt 80000 + 1 + 2 \u2264 (286 : \u211d) := by linarith\n exact le_trans h h57big2\n have hT2pos : (0 : \u211d) < Real.sqrt 80000 + 1 + 2 := by linarith\n have h := Real.log_le_log hT2pos hbig\n rwa [Real.log_exp] at h\n -- log log T \u2264 1.75 (log T \u2264 5.7 \u2264 e\u00b9\u00b7\u2077\u2075 = e\u00b7e\u2070\u00b7\u2077\u2075, 2.7183\u00b72.1169)\n have h175 : Real.exp 1.75 = Real.exp 1 * Real.exp 0.75 := by\n rw [show (1.75 : \u211d) = 1 + 0.75 by norm_num, Real.exp_add]\n have h075 : (2.1169 : \u211d) \u2264 Real.exp 0.75 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.75) 7)\n have h175big : (5.7 : \u211d) \u2264 Real.exp 1.75 := by\n rw [h175]\n exact le_trans (by norm_num : (5.7 : \u211d) \u2264 2.7182818283 * 2.1169)\n (mul_le_mul Real.exp_one_gt_d9.le h075 (by norm_num) (Real.exp_pos _).le)\n have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) :=\n Real.log_pos (by linarith [sqrt80000_ge])\n have h := Real.log_le_log hlogTpos (le_trans hlogT h175big)\n rwa [Real.log_exp] at h\n have hloglogT2 : Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) \u2264 (1.75 : \u211d) := by\n have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1 + 2) :=\n Real.log_pos (by linarith [sqrt80000_ge])\n have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h175big)\n rwa [Real.log_exp] at h\n -- e\u2074 \u2264 54.6015\n have he4 : Real.exp 4 \u2264 (54.6015 : \u211d) := by\n rw [exp_four]\n exact le_trans (exp_one_pow_le 4) (by norm_num)\n -- 1/(2\u03c0) \u2264 1/6\n have h2pi : (1 : \u211d) / (2 * Real.pi) \u2264 1 / 6 := by\n apply one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6)\n have hpi := Real.pi_gt_d20.le\n linarith\n -- log T \u2265 0, log log T \u2265 0, log(T+2) \u2265 0, log log(T+2) \u2265 0\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])\n have hlogT2nn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 80000])\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n Real.log_nonneg hlogTge1\n have hlogT2ge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 + 2 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt80000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=\n Real.log_nonneg hlogT2ge1\n -- FAlt T \u2264 273.82\n have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n unfold FAlt\n have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264\n 284 * 5.7 :=\n mul_le_mul hT hlogT hlogTnn (by norm_num)\n have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n Real.log (Real.sqrt 80000 + 1)) \u2264 (1 / 6 : \u211d) * (284 * 5.7) :=\n mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)\n linarith [ha, hlogT, hloglogT]\n -- \u0108\u2080 T \u2264 6.9186 and \u2265 0\n have hC0 : C0hat (Real.sqrt 80000 + 1) \u2264 (6.9186 : \u211d) := by\n unfold C0hat\n linarith [hlogT2, hloglogT2]\n have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n unfold C0hat\n linarith [hlogT2nn, hloglogT2nn]\n -- H\u0302 T \u2264 251.46 and \u2265 0\n have hH : Hhat (Real.sqrt 80000 + 1) \u2264 (251.46 : \u211d) := by\n unfold Hhat\n have hsq : C0hat (Real.sqrt 80000 + 1) ^ 2 \u2264 6.9186 ^ 2 :=\n pow_le_pow_left\u2080 hC0pos hC0 2\n linarith [hsq, hlogT2]\n have hHnn : (0 : \u211d) \u2264 Hhat (Real.sqrt 80000 + 1) := by\n unfold Hhat\n have hsq : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 := pow_nonneg hC0pos 2\n linarith [hsq, hlogT2nn]\n -- Z\u2082 T \u2264 7.6705 and \u2265 0 (the corrected I_III count, D-071)\n have hZ2 : Z2hat (Real.sqrt 80000 + 1) \u2264 (7.6705 : \u211d) := by\n unfold Z2hat\n linarith [hlogT2, hloglogT2]\n have hZ2nn : (0 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n unfold Z2hat\n linarith [hlogT2nn, hloglogT2nn]\n -- the big bracket: 0 \u2264 \u00b7 \u2264 112.9637\n have hbr : (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 \u2264 112.9637 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hbrnn : (0 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n linarith [hZ2nn, hlogT2nn]\n -- IIMaj \u2264 2590.08\n have hII : IIMaj 80000 \u2264 (2590.08 : \u211d) := by\n refine le_trans (IIMaj_le_two_mul 80000 (by norm_num)) ?_\n have h3 : (4.56 : \u211d) * (Real.sqrt 80000 + 1) \u2264 4.56 * 284 :=\n mul_le_mul_of_nonneg_left (by linarith [sqrt80000_le]) (by norm_num)\n linarith [h3]\n -- the dog-leg share (D-074): 2\u00b7DogLegRight(8\u00d710\u2074) \u2264 3184 (certified)\n have hDL : 2 * DogLegRight 80000 \u2264 (3184 : \u211d) := by\n unfold DogLegRight\n have hT2 : Real.sqrt 80000 + 1 \u2264 284 := hT\n have hII4 : IIMaj 80000 / 4 \u2264 (2590.08 : \u211d) / 4 := by linarith [hII]\n have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (284 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 linarith [exp_five_halves_le]\n linarith [h1, hII4]\n -- assemble\n simp only [Bn]\n have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) \u2264 4 * 284 * 112.9637 := by\n apply mul_le_mul _ hbr hbrnn (by norm_num)\n exact mul_le_mul_of_nonneg_left hT (by norm_num)\n have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) \u2264\n 2 * (54.6015 + 1) * (7 * 251.46) := by\n apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hH]\n linarith [hFAlt, hterm2, hterm4, hDL, hII]\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(8\u00d710\u2074) \u2265 273000 (the lower side only needs\nthe two big terms; the dog-leg share is nonneg). -/\ntheorem Bn_FAlt_80000_ge : (273000 : \u211d) \u2264 Bn FAlt 80000 := by\n have hTge : (283 : \u211d) \u2264 Real.sqrt 80000 + 1 := by\n have h := sqrt80000_ge\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by linarith\n -- log (T+2) \u2265 5.6 (T+2 \u2265 285 \u2265 e\u2075\u00b7\u2076 = e\u2075\u00b7e\u2070\u00b7\u2076, 148.414\u00b71.8433 = 273.571)\n have h5up : Real.exp 5 \u2264 (148.414 : \u211d) := by\n rw [exp_five]\n exact le_trans (exp_one_pow_le 5) (by norm_num)\n have h06up : Real.exp 0.6 \u2264 (1.8433 : \u211d) :=\n le_trans (exp_le_inv_sub_sixteen (by norm_num) (by norm_num)) (by norm_num)\n have h56 : Real.exp 5.6 = Real.exp 5 * Real.exp 0.6 := by\n rw [show (5.6 : \u211d) = 5 + 0.6 by norm_num, Real.exp_add]\n have h56small : Real.exp 5.6 \u2264 (285 : \u211d) := by\n rw [h56]\n exact le_trans (mul_le_mul h5up h06up (Real.exp_pos _).le (by norm_num))\n (by norm_num)\n have hlogT2ge : (5.6 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) := by\n have hbig : (285 : \u211d) \u2264 Real.sqrt 80000 + 1 + 2 := by linarith\n have h1 : (5.6 : \u211d) \u2264 Real.log 285 := by\n have h := Real.log_le_log (Real.exp_pos _) h56small\n rwa [Real.log_exp] at h\n exact le_trans h1 (Real.log_le_log (by norm_num : (0 : \u211d) < 285) hbig)\n -- log log (T+2) \u2265 0 (log (T+2) \u2265 5.6 \u2265 1)\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) :=\n Real.log_nonneg (by linarith)\n -- log T \u2265 0 and log log T \u2265 0 (T \u2265 283 \u2265 e)\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n Real.log_nonneg (by linarith)\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith)\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n Real.log_nonneg hlogTge1\n -- FAlt T \u2265 0 (every term nonneg)\n have hFAlt0 : (0 : \u211d) \u2264 FAlt (Real.sqrt 80000 + 1) := by\n unfold FAlt\n have hpi : (0 : \u211d) < Real.pi := Real.pi_pos\n have hp1 : (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n Real.log (Real.sqrt 80000 + 1)) :=\n mul_nonneg (by positivity) (mul_nonneg hTpos.le hlogTnn)\n have hp2 : (0 : \u211d) \u2264 0.137 * Real.log (Real.sqrt 80000 + 1) :=\n mul_nonneg (by norm_num) hlogTnn\n have hp3 : (0 : \u211d) \u2264 0.443 * Real.log (Real.log (Real.sqrt 80000 + 1)) :=\n mul_nonneg (by norm_num) hloglogTnn\n linarith [hp1, hp2, hp3]\n -- \u0108\u2080 T \u2265 5.3248\n have hC0lo : (5.3248 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n unfold C0hat\n linarith [hlogT2ge, hloglogT2nn]\n -- H\u0302 T \u2265 191.85\n have hHlo : (191.85 : \u211d) \u2264 Hhat (Real.sqrt 80000 + 1) := by\n unfold Hhat\n have hsq : (5.3248 : \u211d) ^ 2 \u2264 C0hat (Real.sqrt 80000 + 1) ^ 2 :=\n pow_le_pow_left\u2080 (by norm_num) hC0lo 2\n linarith [hsq, hlogT2ge]\n -- e\u2074 \u2265 54.5978\n have he4 : (54.5978 : \u211d) \u2264 Real.exp 4 := by\n rw [exp_four]\n exact le_trans (by norm_num) (exp_one_pow_ge 4)\n -- assemble\n simp only [Bn]\n -- Z\u2082 T \u2265 6.06 (0.6\u00b75.6 + 0 + 2.7; log log \u2265 0; the corrected count, D-071)\n have hZ2lo : (6.06 : \u211d) \u2264 Z2hat (Real.sqrt 80000 + 1) := by\n unfold Z2hat\n linarith [hlogT2ge, hloglogT2nn]\n have hbrlo : (110.84 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2lo (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2ge (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hterm2 : (4 * 283 * 110.84 : \u211d) \u2264 4 * (Real.sqrt 80000 + 1) *\n ((2 / 3) * Z2hat (Real.sqrt 80000 + 1) +\n 10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) := by\n apply mul_le_mul _ hbrlo (by norm_num) (by positivity)\n exact mul_le_mul_of_nonneg_left hTge (by norm_num)\n have hterm4 : (2 * (54.5978 + 1) * (7 * 191.85) : \u211d) \u2264\n 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 80000 + 1)) := by\n apply mul_le_mul _ _ (by norm_num) (by positivity)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hHlo]\n have hII : (0 : \u211d) \u2264 IIMaj 80000 := IIMaj_nonneg 80000\n have hDLnn : (0 : \u211d) \u2264 2 * DogLegRight 80000 := by\n unfold DogLegRight\n have hIIMnn := hII\n positivity\n linarith [hFAlt0, hterm2, hterm4, hII, hDLnn]\n\n/-- [PROVED session 012; target updated session 040 for the D-074\ndog-leg repair] Bn FAlt(10\u2075) \u2264 352000 (certified \u2248 351 367; true\n\u2248 333 700 with the dog-leg Bn, E-034's exact Bn_DL = 344 838). -/\ntheorem Bn_FAlt_100000_le : Bn FAlt 100000 \u2264 (352000 : \u211d) := by\n have hT : Real.sqrt 100000 + 1 \u2264 318 := by\n have h := sqrt100000_le\n linarith\n have hTpos : (0 : \u211d) < Real.sqrt 100000 + 1 := by\n have h := Real.sqrt_nonneg 100000\n linarith\n -- log T \u2264 5.8 (T \u2264 318 \u2264 e\u2075\u00b7\u2078 = e\u2075\u00b7e\u2070\u00b7\u2078, 148.328\u00b72.2254 = 330.087)\n have h5 : (148.328 : \u211d) \u2264 Real.exp 5 := by\n rw [exp_five]\n exact le_trans (by norm_num) (exp_one_pow_ge 5)\n have h08 : (2.2254 : \u211d) \u2264 Real.exp 0.8 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.8) 7)\n have h58 : Real.exp 5.8 = Real.exp 5 * Real.exp 0.8 := by\n rw [show (5.8 : \u211d) = 5 + 0.8 by norm_num, Real.exp_add]\n have h58big : (320 : \u211d) \u2264 Real.exp 5.8 := by\n rw [h58]\n exact le_trans (by norm_num : (320 : \u211d) \u2264 148.328 * 2.2254)\n (mul_le_mul h5 h08 (by norm_num) (Real.exp_pos _).le)\n have hlogT : Real.log (Real.sqrt 100000 + 1) \u2264 (5.8 : \u211d) := by\n have h := Real.log_le_log hTpos (le_trans hT (le_trans (by norm_num :\n (318 : \u211d) \u2264 320) h58big))\n rwa [Real.log_exp] at h\n have hlogT2 : Real.log (Real.sqrt 100000 + 1 + 2) \u2264 (5.8 : \u211d) := by\n have hbig : Real.sqrt 100000 + 1 + 2 \u2264 Real.exp 5.8 := by\n have h : Real.sqrt 100000 + 1 + 2 \u2264 (320 : \u211d) := by linarith\n exact le_trans h h58big\n have hT2pos : (0 : \u211d) < Real.sqrt 100000 + 1 + 2 := by linarith\n have h := Real.log_le_log hT2pos hbig\n rwa [Real.log_exp] at h\n -- log log \u2264 1.77 (log \u2264 5.8 \u2264 e\u00b9\u00b7\u2077\u2077 = e\u00b7e\u2070\u00b7\u2077\u2077, 2.7183\u00b72.1597 = 5.8707)\n have h177 : Real.exp 1.77 = Real.exp 1 * Real.exp 0.77 := by\n rw [show (1.77 : \u211d) = 1 + 0.77 by norm_num, Real.exp_add]\n have h077 : (2.1597 : \u211d) \u2264 Real.exp 0.77 :=\n le_trans (by norm_num [Finset.sum_range_succ])\n (Real.sum_le_exp_of_nonneg (by norm_num : (0 : \u211d) \u2264 0.77) 7)\n have h177big : (5.8 : \u211d) \u2264 Real.exp 1.77 := by\n rw [h177]\n exact le_trans (by norm_num : (5.8 : \u211d) \u2264 2.7182818283 * 2.1597)\n (mul_le_mul Real.exp_one_gt_d9.le h077 (by norm_num) (Real.exp_pos _).le)\n have hloglogT : Real.log (Real.log (Real.sqrt 100000 + 1)) \u2264 (1.77 : \u211d) := by\n have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 100000 + 1) :=\n Real.log_pos (by linarith [sqrt100000_ge])\n have h := Real.log_le_log hlogTpos (le_trans hlogT h177big)\n rwa [Real.log_exp] at h\n have hloglogT2 : Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) \u2264 (1.77 : \u211d) := by\n have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 100000 + 1 + 2) :=\n Real.log_pos (by linarith [sqrt100000_ge])\n have h := Real.log_le_log hlogT2pos (le_trans hlogT2 h177big)\n rwa [Real.log_exp] at h\n -- e\u2074 \u2264 54.6015\n have he4 : Real.exp 4 \u2264 (54.6015 : \u211d) := by\n rw [exp_four]\n exact le_trans (exp_one_pow_le 4) (by norm_num)\n -- 1/(2\u03c0) \u2264 1/6\n have h2pi : (1 : \u211d) / (2 * Real.pi) \u2264 1 / 6 := by\n apply one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 6)\n have hpi := Real.pi_gt_d20.le\n linarith\n -- nonnegativity pieces\n have hlogTnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])\n have hlogT2nn : (0 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1 + 2) :=\n Real.log_nonneg (by linarith [Real.sqrt_nonneg 100000])\n have hlogTge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1) := by\n have he : Real.exp 1 \u2264 Real.sqrt 100000 + 1 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogTnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 100000 + 1)) :=\n Real.log_nonneg hlogTge1\n have hlogT2ge1 : (1 : \u211d) \u2264 Real.log (Real.sqrt 100000 + 1 + 2) := by\n have he : Real.exp 1 \u2264 Real.sqrt 100000 + 1 + 2 :=\n le_trans Real.exp_one_lt_d9.le (by linarith [sqrt100000_ge])\n have h := Real.log_le_log (Real.exp_pos 1) he\n rwa [Real.log_exp] at h\n have hloglogT2nn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 100000 + 1 + 2)) :=\n Real.log_nonneg hlogT2ge1\n -- FAlt T \u2264 311.45\n have hFAlt : FAlt (Real.sqrt 100000 + 1) \u2264 (311.45 : \u211d) := by\n unfold FAlt\n have hTl : (Real.sqrt 100000 + 1) * Real.log (Real.sqrt 100000 + 1) \u2264\n 318 * 5.8 :=\n mul_le_mul hT hlogT hlogTnn (by norm_num)\n have ha : (1 / (2 * Real.pi)) * ((Real.sqrt 100000 + 1) *\n Real.log (Real.sqrt 100000 + 1)) \u2264 (1 / 6 : \u211d) * (318 * 5.8) :=\n mul_le_mul h2pi hTl (mul_nonneg hTpos.le hlogTnn) (by norm_num)\n linarith [ha, hlogT, hloglogT]\n -- \u0108\u2080 T \u2264 6.9797 and \u2265 0\n have hC0 : C0hat (Real.sqrt 100000 + 1) \u2264 (6.9797 : \u211d) := by\n unfold C0hat\n linarith [hlogT2, hloglogT2]\n have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 100000 + 1) := by\n unfold C0hat\n linarith [hlogT2nn, hloglogT2nn]\n -- H\u0302 T \u2264 255.05 and \u2265 0\n have hH : Hhat (Real.sqrt 100000 + 1) \u2264 (255.05 : \u211d) := by\n unfold Hhat\n have hsq : C0hat (Real.sqrt 100000 + 1) ^ 2 \u2264 6.9797 ^ 2 :=\n pow_le_pow_left\u2080 hC0pos hC0 2\n linarith [hsq, hlogT2]\n have hHnn : (0 : \u211d) \u2264 Hhat (Real.sqrt 100000 + 1) := by\n unfold Hhat\n have hsq : (0 : \u211d) \u2264 C0hat (Real.sqrt 100000 + 1) ^ 2 := pow_nonneg hC0pos 2\n linarith [hsq, hlogT2nn]\n -- Z\u2082 T \u2264 7.7483 and \u2265 0 (the corrected I_III count, D-071)\n have hZ2 : Z2hat (Real.sqrt 100000 + 1) \u2264 (7.7483 : \u211d) := by\n unfold Z2hat\n linarith [hlogT2, hloglogT2]\n have hZ2nn : (0 : \u211d) \u2264 Z2hat (Real.sqrt 100000 + 1) := by\n unfold Z2hat\n linarith [hlogT2nn, hloglogT2nn]\n -- the big bracket: 0 \u2264 \u00b7 \u2264 114.0655\n have hbr : (2 / 3 : \u211d) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 \u2264 114.0656 := by\n have h1 := mul_le_mul_of_nonneg_left hZ2 (by norm_num : (0 : \u211d) \u2264 2 / 3)\n have h2 := mul_le_mul_of_nonneg_left hlogT2 (by norm_num : (0 : \u211d) \u2264 10.5)\n linarith [h1, h2]\n have hbrnn : (0 : \u211d) \u2264 (2 / 3 : \u211d) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48 := by\n linarith [hZ2nn, hlogT2nn]\n -- IIMaj \u2264 2900.16\n have hII : IIMaj 100000 \u2264 (2900.16 : \u211d) := by\n refine le_trans (IIMaj_le_two_mul 100000 (by norm_num)) ?_\n have h3 : (4.56 : \u211d) * (Real.sqrt 100000 + 1) \u2264 4.56 * 318 :=\n mul_le_mul_of_nonneg_left (by linarith [sqrt100000_le]) (by norm_num)\n linarith [h3]\n -- the dog-leg share (D-074): 2\u00b7DogLegRight(10\u2075) \u2264 3564 (certified)\n have hDL : 2 * DogLegRight 100000 \u2264 (3564 : \u211d) := by\n unfold DogLegRight\n have hT2 : Real.sqrt 100000 + 1 \u2264 318 := hT\n have hII4 : IIMaj 100000 / 4 \u2264 (2900.16 : \u211d) / 4 := by linarith [hII]\n have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 \u2264\n (318 / 2) * (13.183 : \u211d) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)\n \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]\n -- assemble\n simp only [Bn]\n have hterm2 : 4 * (Real.sqrt 100000 + 1) * ((2 / 3) * Z2hat (Real.sqrt 100000 + 1) +\n 10.5 * Real.log (Real.sqrt 100000 + 1 + 2) + 48) \u2264 4 * 318 * 114.0656 := by\n apply mul_le_mul _ hbr hbrnn (by norm_num)\n exact mul_le_mul_of_nonneg_left hT (by norm_num)\n have hterm4 : 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt 100000 + 1)) \u2264\n 2 * (54.6015 + 1) * (7 * 255.05) := by\n apply mul_le_mul _ _ (by linarith [hHnn]) (by norm_num)\n \u00b7 apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 2)\n linarith [he4]\n \u00b7 linarith [hH]\n linarith [hFAlt, hterm2, hterm4, hDL, hII]\n\n/-! ### 5. The two base points and the final three-hypothesis form -/\n\n/-- [PROVED session 012; values updated session 038 for the D-071\ncorrection] hbase: margin\u0303(8\u00d710\u2074) > 0. Certified: sInftyLower \u2265 336 000,\nBn \u2264 329 000 \u27f9 margin \u2265 7 001 (true 14 682 with the corrected Bn). -/\ntheorem marginTilde_FAlt_80000_pos : 0 < marginTilde FAlt 80000 := by\n rw [marginTilde_eq_sub]\n have hS := sInftyLower_80000_lo\n have hB := Bn_FAlt_80000_le\n linarith\n\n/-- [PROVED session 012; values updated session 038 for the D-071\ncorrection] hbase2: margin\u0303(8\u00d710\u2074) < margin\u0303(10\u2075).\nCertified: margin\u0303(8\u00d710\u2074) \u2264 339 000 \u2212 274 000 + 1 = 65 001 and\nmargin\u0303(10\u2075) \u2265 432 500 \u2212 350 000 + 1 = 82 501. -/\ntheorem marginTilde_FAlt_80000_lt_100000 :\n marginTilde FAlt 80000 < marginTilde FAlt 100000 := by\n rw [marginTilde_eq_sub, marginTilde_eq_sub]\n have h1 := sInftyLower_80000_up\n have h2 := Bn_FAlt_80000_ge\n have h3 := sInftyLower_100000_lo\n have h4 := Bn_FAlt_100000_le\n linarith\n\n/-- [PROVED session 012 \u2014 TIER (ii) STEP 2] R-004, the finite-height Li\ntheorem, in its final assembly form: machine-verified modulo ONE named\nanalytic hypothesis (`SfBoundProp`, the traced contour bound) plus the\ndeclared computational perimeter (Platt\u2013Trudgian `RHUpTo`; the finite Li\nverification `LiVerifiedUpTo`). The two elementary margin evaluations\nare discharged in this file. -/\ntheorem lambda_pos_finite_height_verified\n (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hSf : SfBoundProp) :\n \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n 0 < (liCoeff n).re :=\n fun n hn1 hnN => lambda_pos_finite_height hRH hfinite\n marginTilde_FAlt_80000_pos marginTilde_FAlt_80000_lt_100000 hSf n hn1 hnN\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 657,
"oldLines": 8,
"newStart": 657,
"newLines": 7,
"lines": [
" apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)",
" apply mul_le_mul _ _ (by positivity) (by positivity)",
" \u00b7 exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : \u211d) \u2264 2)",
"- \u00b7 apply div_le_div_of_nonneg_right _ (by norm_num : (0 : \u211d) \u2264 2)",
"- linarith [exp_five_halves_le]",
"+ \u00b7 linarith [exp_five_halves_le]",
" linarith [h1, hII4]",
" -- assemble",
" simp only [Bn]"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"The inner `apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)` — the goal is `Real.exp (5/2) + 1 ≤ 13.183` — that's NOT a division goal (X/2 ≤ Y/2)! The goal at that bullet is `(Real.exp (5/2) + 1) / 2 ≤ (13.183 : ℝ) / 2`?? — no — the goal shown is `Real.exp (5 / 2) + 1 ≤ 13.183` — so the bullet's goal IS the non-division form. My mul_le_mul's hcd goal: `(e^{5/2}+1) ≤ 13.183`?? — wait — the mul_le_mul's structure: `((√80000+1)/2)·(e^{5/2}+1) ≤ (284/2)·13.183` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) with c := e^{5/2}+1, d := 13.183: hcd : e^{5/2}+1 ≤ 13.183 — and my `apply div_le_div_of_nonneg_right _ (by norm_num : (0:ℝ) ≤ 2)` tries to prove `(e^{5/2}+1)/2 ≤ 13.183/2` but the goal is `e^{5/2}+1 ≤ 13.183` (no division!) — mismatch ✗.\n\nHmm — wait, the goal at that bullet is `Real.exp (5 / 2) + 1 ≤ 13.183` — so the mul_le_mul's c-side is e^{5/2}+1 (NOT (e^{5/2}+1)/2)!? — the h1 statement: `((√80000+1)/2)·(e^{5/2}+1)/2 ≤ (284/2)·(13.183)/2` — hmm — my h1 has the form `((√80000+1)/2)·((e^{5/2}+1)/2)` vs `(284/2)·(13.183/2)` — wait no — let me look at DogLegRight's def: `((Real.sqrt n + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + 8.38 + IIMaj n / 4` — so DogLegRight's first term is `((√n+1)/2)·(e^{5/2}+1)/2` — parses as `(((√n+1)/2)·(e^{5/2}+1))/2` ✓ — so h1's goal is `(((√80000+1)/2)·(e^{5/2}+1))/2 ≤ ((284/2)·13.183)/2` — X/2 ≤ Y/2 with X := ((√80000+1)/2)·(e^{5/2}+1), Y := (284/2)·13.183 ✓. Then `apply div_le_div_of_nonneg_right _ (by norm_num : (0:ℝ) ≤ 2)` at the OUTER level: X/2 ≤ Y/2 from X ≤ Y ✓ — the remaining goal is X ≤ Y: `((√80000+1)/2)·(e^{5/2}+1) ≤ (284/2)·13.183` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) with a := (√80000+1)/2, b := 284/2, c := e^{5/2}+1, d := 13.183: the hcd goal is `e^{5/2}+1 ≤ 13.183` ✓ — and my inner `apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)` on that goal — WRONG (it's not a division goal). Fix: `linarith [exp_five_halves_le]` directly for the hcd (e^{5/2}+1 ≤ 12.183+1 = 13.183 ✓):\n```\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)\n · linarith [exp_five_halves_le]\n```\nWait — the mul_le_mul's hcd : e^{5/2}+1 ≤ 13.183 — linarith [exp_five_halves_le] (e^{5/2} ≤ 12.183 ⟹ +1 ≤ 13.183 ✓ linarith ✓).\n\nHmm — but the mul_le_mul's apply left TWO bullet goals (hab and hcd) or one? `apply mul_le_mul _ _ (by positivity) (by positivity)` — mul_le_mul (hab : a ≤ b) (hcd : c ≤ d) (hc : 0 ≤ c) (hb : 0 ≤ b) — I passed `_ _ (by positivity) (by positivity)` — the first two `_` are hab and hcd (goals) ✓ then hc/hb by positivity ✓ — so the two `_` become bullet goals: `· exact div_le_div_of_nonneg_right hT2 ...` (hab) and `· linarith [exp_five_halves_le]` (hcd) ✓.\n\nWait — but does `apply mul_le_mul _ _ A B` leave the bullets in order (hab first, hcd second)? — the bullets come as separate goals in order ✓.","signature":""},{"type":"text","text":"The inner goal is non-division — using `linarith` directly for the e^{5/2}+1 side."},{"type":"tool_use","id":"Edit_644","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean","old_string":" have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤\n (284 / 2) * (13.183 : ℝ) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)\n · apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]","new_string":" have h1 : ((Real.sqrt 80000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤\n (284 / 2) * (13.183 : ℝ) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)\n · linarith [exp_five_halves_le]\n linarith [h1, hII4]"},"extra_content":null},{"type":"tool_use","id":"Edit_645","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean","old_string":" have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤\n (318 / 2) * (13.183 : ℝ) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)\n · apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n linarith [exp_five_halves_le]\n linarith [h1, hII4]","new_string":" have h1 : ((Real.sqrt 100000 + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 ≤\n (318 / 2) * (13.183 : ℝ) / 2 := by\n apply div_le_div_of_nonneg_right _ (by norm_num : (0 : ℝ) ≤ 2)\n apply mul_le_mul _ _ (by positivity) (by positivity)\n · exact div_le_div_of_nonneg_right hT2 (by norm_num : (0 : ℝ) ≤ 2)\n · linarith [exp_five_halves_le]\n linarith [h1, hII4]"},"extra_content":null}]