{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
  "content": "/-\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 slack \u2265 300 except the flagged tight links\n(e\u00b9\u00b7\u00b9\u2074\u2074\u2078 \u2265 \u03c0 was replaced by the comfortable e\u00b9\u00b7\u00b9\u2075 \u2265 \u03c0 at a 104-unit\ncost, absorbed).\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    field_simp\n  rw [h4]\n  exact pow_le_pow_left (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 (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 (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/-! ### 2. Certified log bounds at the margin points -/\n\n/-- [PROVED session 012] log 80000 \u2265 11.263 (via e\u00b9\u00b9\u00b7\u00b2\u2076\u00b3 \u2264 78063 <\n80000). -/\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 (via e\u00b9\u00b9\u00b7\u00b3 \u2265 80821 > 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 (via e\u00b9\u00b9\u00b7\u2075 \u2264 99661 <\n100000). -/\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 (via 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 (via 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/-! ### 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 value\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_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 value\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_right (by norm_num : (0 : \u211d) < 2)]\n    linarith\n  linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(10\u2075) \u2265 432500 (certified value\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_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] Bn FAlt(8\u00d710\u2074) \u2264 328000 (certified value\n327 053; true 322 309). -/\ntheorem Bn_FAlt_80000_le : Bn FAlt 80000 \u2264 (328000 : \u211d) := by\n  have hT : Real.sqrt 80000 + 1 \u2264 284 := by\n    have := sqrt80000_le\n    linarith\n  have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by\n    have := Real.sqrt_nonneg 80000\n    linarith\n  have hTge : (283 : \u211d) \u2264 Real.sqrt 80000 + 1 := by\n    have := sqrt80000_ge\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 hlogT : Real.log (Real.sqrt 80000 + 1) \u2264 (5.7 : \u211d) := by\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 hbig : Real.sqrt 80000 + 1 \u2264 Real.exp 5.7 := by\n      rw [h57]\n      exact le_trans (by norm_num : Real.sqrt 80000 + 1 \u2264 (284 : \u211d))\n        (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 h := Real.log_le_log hTpos hbig\n    rwa [Real.log_exp] at h\n  -- log (T+2) \u2264 5.7 (T+2 \u2264 286 \u2264 e\u2075\u00b7\u2077)\n  have hlogT2 : Real.log (Real.sqrt 80000 + 1 + 2) \u2264 (5.7 : \u211d) := by\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 hbig : Real.sqrt 80000 + 1 + 2 \u2264 Real.exp 5.7 := by\n      rw [h57]\n      exact le_trans (by norm_num : Real.sqrt 80000 + 1 + 2 \u2264 (286 : \u211d))\n        (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 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 = 5.7544)\n  have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\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 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 hbig : (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 h1 h075 (by norm_num) (Real.exp_pos _).le)\n    have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogTpos (le_trans hlogT hbig)\n    have h57 : Real.log (5.7 : \u211d) \u2264 1.75 := by\n      have h' := Real.log_le_log (by norm_num : (0 : \u211d) < 5.7) hbig\n      rwa [Real.log_exp] at h'\n    linarith [h, h57]\n  -- log log (T+2) \u2264 1.75\n  have hloglogT2 : Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\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 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 hbig : (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 h1 h075 (by norm_num) (Real.exp_pos _).le)\n    have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1 + 2) :=\n      Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogT2pos (le_trans hlogT2 hbig)\n    have h57 : Real.log (5.7 : \u211d) \u2264 1.75 := by\n      have h' := Real.log_le_log (by norm_num : (0 : \u211d) < 5.7) hbig\n      rwa [Real.log_exp] at h'\n    linarith [h, h57]\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  -- FAlt T \u2264 273.82\n  have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n    unfold FAlt\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    have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264 284 * 5.7 := by\n      apply mul_le_mul hT hlogT (Real.log_nonneg (by linarith)) (by norm_num)\n    have h1 : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_nonneg (by linarith)\n    have h2 : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 283)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\n    linarith [mul_le_mul_of_nonneg_left hTl (by norm_num : (0 : \u211d) \u2264 1 / 6) |>.trans\n      (by norm_num : (1 / 6 : \u211d) * (284 * 5.7) \u2264 269.8)]\n  -- \u0108\u2080 T \u2264 6.9186\n  have hC0 : C0hat (Real.sqrt 80000 + 1) \u2264 (6.9186 : \u211d) := by\n    unfold C0hat\n    linarith [hlogT2, hloglogT2]\n  -- \u0108\u2080 T \u2265 0 (for the product chains)\n  have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n    unfold C0hat\n    have h1 : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) :=\n      Real.log_nonneg (by linarith)\n    have h2 : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 + 2 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 285)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\n    linarith\n  -- H\u0302 T \u2264 251.45\n  have hH : Hhat (Real.sqrt 80000 + 1) \u2264 (251.45 : \u211d) := by\n    unfold Hhat\n    have hsq : C0hat (Real.sqrt 80000 + 1) ^ 2 \u2264 6.9186 ^ 2 :=\n      pow_le_pow_left hC0pos hC0 2\n    linarith [hsq, hlogT2]\n  -- the big bracket \u2264 112.4624\n  have hbr : (2 / 3 : \u211d) * C0hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 \u2264 112.4624 := by\n    have h1 := mul_le_mul_of_nonneg_left hC0 (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  -- 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 := sqrt80000_le\n    norm_num [this]\n  -- assemble\n  simp only [Bn]\n  have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * C0hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) \u2264 4 * 284 * 112.4624 := by\n    apply mul_le_mul _ hbr (by linarith [hC0pos]) (by norm_num)\n    have h4 : (0 : \u211d) \u2264 4 * (Real.sqrt 80000 + 1) := by positivity\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) + 3.3) \u2264\n      2 * (54.6015 + 1) * (7 * 251.45 + 3.3) := by\n    apply mul_le_mul _ _ (by positivity) (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 [mul_le_mul_of_nonneg_left hH (by norm_num : (0 : \u211d) \u2264 7)]\n  linarith [hFAlt, hterm2, hterm4, hII]\n```\n\nHmm wait \u2014 issues with the above draft:\n1. `norm_num [this]` in hII: 4.56\u00b7(\u221a80000+1)\u00b72 \u2264 2590.08: from \u221a80000 \u2264 283: 4.56\u00b7284\u00b72 = 2590.08. norm_num can't do this with sqrt in it. Need: mul_le_mul chains: 4.56*(\u221a+1)*2 \u2264 4.56*284*2 = 2590.08: \n```\n  have hII : IIMaj 80000 \u2264 (2590.08 : \u211d) := by\n    have h1 := IIMaj_le_two_mul 80000 (by norm_num)\n    have h2 : (4.56 : \u211d) * (Real.sqrt 80000 + 1) * 2 \u2264 2590.08 := by\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      norm_num [show (4.56:\u211d)*284*2 = 2590.08 by norm_num]  -- hmm\n    exact le_trans h1 h2\n```\nh2: 4.56*(\u221a80000+1)*2 \u2264 2590.08: from h3: 4.56*(\u221a80000+1) \u2264 4.56*284 = 1295.04; \u00b72 = 2590.08: linarith [h3] after norm_num computing 4.56*284: linarith handles linear arithmetic with numerals \u2014 4.56*284 is a numeral multiplication linarith can evaluate? linarith's preprocessing does ring_nf, so 4.56*284*2 \u2192 2590.08 \u2713 should work: h2 := by have h3 := ...; linarith [h3]. But h3 has \u221a80000 in it: 4.56*(\u221a80000+1) \u2264 4.56*284 \u2014 linarith treats (\u221a80000) as atom: h3 : 4.56*(\u221a80000+1) \u2264 1295.04 after norm_num-eval... linarith will expand 4.56*(\u221a80000+1) = 4.56*\u221a80000 + 4.56 (ring_nf) and h3 gives 4.56*\u221a80000 \u2264 1290.48; goal 4.56*(\u221a80000+1)*2 \u2264 2590.08 \u27fa 9.12\u00b7\u221a80000 + 9.12 \u2264 2590.08 \u27f8 9.12\u00b7283 = 2580.96 + 9.12 = 2590.08 \u2713 \u2014 need \u221a80000 \u2264 283 directly: linarith [sqrt80000_le] should close after ring_nf normalizes. So:\n```\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```\nlinarith: goal 4.56*(\u221a80000+1)*2 \u2264 2590.08; h3: 4.56*(\u221a80000+1) \u2264 4.56*284. ring_nf both: 4.56\u00b7s + 4.56 \u2264 1295.04; goal: 9.12\u00b7s + 9.12 \u2264 2590.08 \u27f8 2\u00b7(4.56s+4.56) \u2264 2\u00b71295.04 = 2590.08 \u2713 linarith closes.\n\n2. In hFAlt: the `linarith [mul_le_mul_of_nonneg_left hTl ... |>.trans ...]` \u2014 the |>.trans inside linarith list: the bracket has pieces:\n   (1/(2\u03c0))\u00b7(T\u00b7log T) \u2264 (1/6)\u00b7(284\u00b75.7) \u2264 269.8: h2pi gives 1/(2\u03c0) \u2264 1/6; then (1/(2\u03c0))\u00b7(T\u00b7logT) \u2264 (1/6)\u00b7(T\u00b7logT) \u2264 (1/6)\u00b7(284\u00b75.7): mul_le_mul_of_nonneg_right h2pi (T\u00b7logT \u2265 0) then mul_le_mul_of_nonneg_left hTl (0 \u2264 1/6)... chain:\n   ha : (1/(2*\u03c0)) * (T8 * log T8) \u2264 (1/6) * (284 * 5.7):\n     mul_le_mul (h2pi) (hTl) (0 \u2264 T8*logT8) (0 \u2264 1/6) \u2014 mul_le_mul : a\u2264b \u2192 c\u2264d \u2192 0\u2264c \u2192 0\u2264b \u2192 a\u00b7c \u2264 b\u00b7d: a = 1/(2\u03c0), b = 1/6, c = T8\u00b7logT8, d = 284\u00b75.7: need 0 \u2264 T8\u00b7logT8 \u2713 (mul_nonneg hTpos.le (log_nonneg)) and 0 \u2264 1/6 \u2713. Gives (1/(2\u03c0))\u00b7(T8\u00b7logT8) \u2264 (1/6)\u00b7(284\u00b75.7) \u2713.\n   Then FAlt T8 = (1/(2\u03c0))\u00b7(T8\u00b7logT8) + 0.137\u00b7logT8 + 0.443\u00b7loglogT8 + (7/8+1.588) \u2264 269.8 + 0.137\u00b75.7 + 0.443\u00b71.75 + 2.463 = 269.8 + 0.7809 + 0.77525 + 2.463 = 273.82. \u2014 wait: (1/6)\u00b7(284\u00b75.7) = 1618.8/6 = 269.8 \u2713. Sum: 269.8+0.7809+0.77525+2.463 = 273.81915 \u2264 273.82 \u2713.\n   linarith [ha, hlogT, hloglogT] \u2014 linarith must multiply 0.137\u00b7logT8 \u2264 0.137\u00b75.7 itself (product of hypotheses \u2014 linarith CAN multiply a hypothesis by a positive constant \u2713 but logT8 is an atom \u00d7 constant \u2014 yes linarith handles).\n   The `(7/8 + 1.588 : \u211d)` \u2014 norm_num-evaluated by linarith's ring_nf \u2713 2.463.\n\n   So hFAlt:\n```\n  have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n    unfold FAlt\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    have hTlnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_nonneg (by linarith)\n    have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264 284 * 5.7 :=\n      mul_le_mul hT hlogT hTlnn (by norm_num)\n    have hllnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 283)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\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 hTlnn) (by norm_num)\n    linarith [ha, hlogT, hloglogT]\n```\n   linarith closing: goal (after unfold FAlt): (1/(2\u03c0))\u00b7(T8\u00b7logT8) + 0.137\u00b7logT8 + 0.443\u00b7loglogT8 + (7/8+1.588) \u2264 273.82. From ha: first \u2264 269.8; 0.137\u00b7logT8 \u2264 0.137\u00b75.7 = 0.7809 (linarith multiplies hlogT by 0.137 \u2713); 0.443\u00b7loglogT8 \u2264 0.443\u00b71.75 = 0.77525 \u2713; 7/8+1.588 = 2.463. Total \u2264 269.8+0.7809+0.77525+2.463 = 273.81915 \u2264 273.82 \u2713 linarith closes (needs hlogT, hloglogT in context \u2014 they're haves \u2713 but linarith [ha, hlogT, hloglogT] \u2014 hlogT/hloglogT already in context; passing them again harmless).\n   \n   Wait \u2014 subtlety: 0.137\u00b7logT8 \u2264 0.137\u00b75.7 requires logT8 atom with coefficient \u2014 linarith multiplies hypotheses by POSITIVE constants only when needed; hlogT : log T8 \u2264 5.7 \u2014 linarith can use 0.137\u00b7(hlogT) \u2713 standard.\n\n3. hC0: unfold C0hat: 0.433\u00b7log(T8+2) + 0.886\u00b7log log(T8+2) + 2.9 \u2264 0.433\u00b75.7 + 0.886\u00b71.75 + 2.9 = 6.9186: linarith [hlogT2, hloglogT2] \u2713 (0.433\u00b75.7 = 2.4681, 0.886\u00b71.75 = 1.5505, +2.9 = 6.9186 exact \u2014 linarith handles \u2713).\n\n4. hC0pos: C0hat \u2265 0: pieces nonneg: 0.433\u00b7log(T8+2) \u2265 0 (h1), 0.886\u00b7loglog(T8+2) \u2265 0 (h2), 2.9 \u2265 0: linarith [h1, h2] \u2014 the goal after unfold: 0 \u2264 0.433*log(...) + 0.886*log(...)... + 2.9 \u2014 linarith with h1 : 0 \u2264 log(T8+2), h2 : 0 \u2264 log log(T8+2) \u2713.\n\n5. hH: Hhat = 3\u00b7C0hat\u00b2 + 10.5\u00b7log(T8+2) + 48 \u2264 3\u00b76.9186\u00b2 + 10.5\u00b75.7 + 48: 3\u00b747.867011 = 143.601 + 59.85 + 48 = 251.451 \u2264 251.45?? 3\u00b76.9186\u00b2 = 3\u00b747.8670059... compute: 6.9186\u00b2 = 47.86700...; 6.9186\u00b2 = 47.8670 (6.9186\u00b2 = 47.86700596); \u00d73 = 143.601018; +59.85+48 = 251.451018 > 251.45 \u2717!! TOO TIGHT \u2014 251.451 > 251.45. Adjust: hH \u2264 251.46. Then term4: 7\u00b7251.46+3.3 = 1763.52; 111.203\u00b71763.52 = 196116.4 (+12.8). Total: 327053+12.8 = 327065.8 \u2264 328000 \u2713 fine. Use 251.46.\n\n6. hbr: \u2264 (2/3)\u00b76.9186 + 10.5\u00b75.7 + 48 = 4.6124+59.85+48 = 112.4624 \u2713 exact.\n\n7. hterm2: mul_le_mul _ hbr (by linarith [hC0pos]) (by norm_num): mul_le_mul (a := 4T8) (b := 4\u00b7284) (c := bracket) (d := 112.4624): first arg a \u2264 b: 4\u00b7T8 \u2264 4\u00b7284: mul_le_mul_of_nonneg_left hT (by norm_num : (0:\u211d) \u2264 4) \u2014 my draft had the args wrong order: mul_le_mul h1 h2 h3 h4 where h1 : a \u2264 b = the 4T8 \u2264 4\u00b7284; h2 : c \u2264 d = hbr; h3 : 0 \u2264 c = bracket \u2265 0 \u2014 bracket = (2/3)C0hat + 10.5 log + 48 \u2265 0+0+48: linarith [hC0pos, hlogT2nn] \u2014 need log(T8+2) \u2265 0 (Real.log_nonneg (T8+2 \u2265 1)) \u2014 add have. h4 : 0 \u2264 b = 4\u00b7284 \u2265 0 \u2713 norm_num.\n   Then 4\u00b7284\u00b7112.4624 = 1136\u00b7112.4624 = 127757.29 \u2014 the final linarith [hFAlt, hterm2, hterm4, hII] evaluates numerals \u2713.\n\n8. hterm4: mul_le_mul h41 h42 h43 h44: a = 2(e\u2074+1), b = 2\u00b755.6015, c = 7H\u0302+3.3, d = 7\u00b7251.46+3.3: h41 : 2(e\u2074+1) \u2264 2\u00b755.6015: mul_le_mul_of_nonneg_left (by linarith [he4]) (by norm_num) \u2014 wait 2\u00b7(e\u2074+1) \u2264 2\u00b7(54.6015+1) \u27f8 e\u2074+1 \u2264 54.6015+1 \u27f8 e\u2074 \u2264 54.6015 \u2713 linarith [he4]. h42 : 7H\u0302+3.3 \u2264 7\u00b7251.46+3.3: linarith [mul_le_mul_of_nonneg_left hH (0 \u2264 7)] or just linarith [hH] (linarith can scale hH by 7 \u2713). h43 : 0 \u2264 7H\u0302+3.3: Hhat \u2265 0? Hhat = 3C0\u00b2+10.5 log+48 \u2265 0: 3\u00b7C0\u00b2 \u2265 0 (pow_nonneg/sq), 10.5\u00b7log(T8+2) \u2265 0 \u2713, 48 > 0: need a have hHnn : 0 \u2264 Hhat T8: unfold Hhat; positivity-ish: 3*C0hat^2 \u2265 0 (pow_nonneg hC0pos 2... pow_nonneg needs 0 \u2264 C0hat \u2713), 10.5\u00b7log \u2265 0 (hlogT2nn), 48: linarith [pow_nonneg hC0pos 2, hlogT2nn]. h44 : 0 \u2264 2\u00b755.6015 \u2713 norm_num.\n\n9. Final linarith [hFAlt, hterm2, hterm4, hII]: goal (after simp only [Bn]): 2\u00b7FAlt T8 + 4\u00b7T8\u00b7(bracket) + 40\u00b71.3352 + 2(e\u2074+1)(7H\u0302+3.3) + IIMaj 80000 + 1 \u2264 328000. From: 2\u00b7FAlt \u2264 547.64; term2 \u2264 127757.29; 40\u00b71.3352 = 53.408; term4 \u2264 196116.4; IIMaj \u2264 2590.08; +1. Sum: 547.64+127757.29+53.408+196116.4+2590.08+1 = 327065.8 \u2264 328000 \u2713 slack 934.\n\nBut WAIT \u2014 after `simp only [Bn]`, does the goal keep `C0hat`, `Hhat`, `FAlt` folded? simp only [Bn] unfolds only Bn \u2014 the goal has FAlt (\u221a80000+1), C0hat (\u221a80000+1), Hhat (\u221a80000+1), Real.log (\u221a80000+1+2), IIMaj 80000, Real.exp 4 \u2014 matches my haves \u2713 (assuming the let zeta-reduces, giving Real.sqrt 80000 + 1 for T everywhere, and T + 2 becomes Real.sqrt 80000 + 1 + 2 \u2713).\n\nPotential mismatch: `10.5 * Real.log (T + 2)` with T = \u221a80000+1 gives Real.log (\u221a80000 + 1 + 2) \u2713 my haves use exactly that form \u2713. And C0hat/Hhat unfolded inside Bn? NO \u2014 Bn references C0hat T and Hhat T by name; simp only [Bn] leaves them folded \u2713. hC0/hH unfold them locally \u2713. But the FINAL goal has C0hat (\u221a80000+1) etc. \u2014 my hterm2's statement I wrote with explicit ((2/3)*C0hat(...) + ...) \u2014 matches \u2713.\n\nOne more: hloglogT's inner proof uses hlogT \u2014 fine (local). And hloglogT uses le_trans hlogT hbig: log T8 \u2264 5.7 \u2264 exp 1.75 \u2192 log T8 \u2264 exp 1.75; then Real.log_le_log hlogTpos (le_trans hlogT hbig) : log (log T8) \u2264 log (exp 1.75)?? NO \u2014 Real.log_le_log (hx : 0 < x) (h : x \u2264 y) : log x \u2264 log y. With x = log T8, y = exp 1.75: log(log T8) \u2264 log(exp 1.75) = 1.75 \u2014 I did an extra step via log 5.7: `h := Real.log_le_log hlogTpos (le_trans hlogT hbig) : Real.log (Real.log T8) \u2264 Real.log (Real.exp 1.75)`; then Real.log_exp: log(exp 1.75) = 1.75 \u2014 my draft wrote h then h57 separately then linarith [h, h57] \u2014 h57 : log 5.7 \u2264 1.75 \u2014 that's the WRONG piece; the clean way: h : log(log T8) \u2264 log(exp 1.75); rwa [Real.log_exp] at h. My draft's h57 dance was unnecessary and the linarith [h, h57] where h : log(log T8) \u2264 log(exp 1.75) \u2014 linarith can't simplify log(exp 1.75) (atom). FIX: rwa [Real.log_exp] at h \u2014 direct. Let me restructure hloglogT:\n```\n  have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\n    have h075 : (2.1169 : \u211d) \u2264 Real.exp 0.75 := ...\n    have h175 : Real.exp 1.75 = Real.exp 1 * Real.exp 0.75 := ...\n    have hbig : (5.7 : \u211d) \u2264 Real.exp 1.75 := ...\n    have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) := Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogTpos (le_trans hlogT hbig)\n    rwa [Real.log_exp] at h\n```\nle_trans hlogT hbig : log T8 \u2264 exp 1.75 \u2713 (hlogT : log T8 \u2264 5.7; hbig : 5.7 \u2264 exp 1.75). Real.log_le_log hlogTpos (that) : log (log T8) \u2264 log (exp 1.75); rw log_exp: = 1.75 \u2713 DONE. \u2713 cleaner.\n\nReal.log_pos (1 < x): T8 > 1: from hTge : 283 \u2264 T8: linarith \u2713 \u2014 hlogTpos uses Real.log_pos (by linarith) \u2014 needs 1 < \u221a80000+1 in context-solvable form: hTge present? I define hlogTpos inside hloglogT where hTge is in scope (declared before) \u2713 but linarith needs hTge explicitly? linarith uses context \u2713 hTge is a have in the proof \u2713.\n\nOK. Given the scale, let me write the file with all these corrections baked in, compile, iterate. For Bn_FAlt_80000_ge and Bn_FAlt_100000_le similar structure. To keep the response manageable I'll write the complete file now.\n\nFor Bn_FAlt_80000_ge (lower bound):\n- hFAlt0 : 0 \u2264 FAlt T8: unfold FAlt; pieces \u2265 0: (1/(2\u03c0))\u00b7(T8\u00b7log T8): positivity with hTlnn (log T8 \u2265 0) and pi_pos: (1/(2\u03c0)) \u2265 0: positivity knows \u03c0 > 0? positivity has an extension for Real.pi \u2713 (Real.pi_pos via positivity? I think positivity proves 0 < \u03c0 \u2014 there's a positivity extension for pi). mul_nonneg chains + linarith. Write:\n```\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 hTlnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := Real.log_nonneg (by linarith)\n    have hllnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := ... (as before)\n    have hp1 : (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n        Real.log (Real.sqrt 80000 + 1)) := by positivity  -- needs log T8 \u2265 0 in context: positivity uses hypotheses? positivity does NOT use hypotheses. Use mul_nonneg: mul_nonneg (by positivity) (mul_nonneg hTpos.le hTlnn)\n    linarith [hp1, mul_nonneg (by norm_num : (0:\u211d) \u2264 0.137) hTlnn, mul_nonneg (by norm_num : (0:\u211d) \u2264 0.443) hllnn]\n```\n  positivity for 1/(2\u03c0) \u2265 0: positivity should handle (pi_pos extension exists \u2713).\n\n- term2 lower: 4\u00b7T8\u00b7bracket \u2265 4\u00b7283\u00b7110.34987: hbrlo : bracket \u2265 (2/3)\u00b75.3248 + 10.5\u00b75.6 + 48 = 110.34987: needs C0hat \u2265 5.3248 (hC0lo : 0.433\u00b7log(T8+2) \u2265 0.433\u00b75.6 from logT82_ge; 0.886\u00b7loglog \u2265 0; +2.9: linarith) and 10.5\u00b7log \u2265 10.5\u00b75.6 \u2713 linarith.\n  logT82_ge : 5.6 \u2264 log (T8+2): T8+2 \u2265 285 \u2265 exp 5.6: exp 5.6 = exp 5\u00b7exp 0.6 \u2264 148.414\u00b71.8433 = 273.571: \n  h5up : exp 5 \u2264 148.414 (exp_five + exp_one_pow_le 5 + norm_num)\n  h06up : exp 0.6 \u2264 1.8433 (exp_le_inv_sub_sixteen + norm_num)\n  h56 : exp 5.6 = exp 5\u00b7exp 0.6\n  T8+2 \u2265 285 (hTge: T8 \u2265 283); 285 \u2265 273.571 \u2265 exp 5.6: Real.log_le_log (exp_pos) (285 \u2265 exp 5.6 via le_trans) : 5.6 = log(exp 5.6) \u2264 log 285 \u2264 log(T8+2) \u2014 chain: log 285 \u2265 5.6 then log(T8+2) \u2265 log 285 (T8+2 \u2265 285): two log_le_log steps.\n  hC0lo : C0hat T8 \u2265 5.3248: unfold C0hat: 0.433\u00b7log(T8+2) \u2265 0.433\u00b75.6 = 2.4248; 0.886\u00b7loglog(T8+2) \u2265 0; +2.9: linarith [logT82_ge, hllT2nn].\n  hHlo : Hhat T8 \u2265 191.86: 3\u00b7C0hat\u00b2 \u2265 3\u00b75.3248\u00b2 (pow_le_pow_left (5.3248 \u2265 0) hC0lo 2): 3\u00b728.35352 = 85.0606; 10.5\u00b7log(T8+2) \u2265 10.5\u00b75.6 = 58.8; +48: 85.0606+58.8+48 = 191.8606 \u2265 191.86 \u2713 (0.0006 margin \u2014 exact rational, OK but tight; use 191.85: 191.8606 \u2265 191.85 \u2713 safer).\n  5.3248\u00b2 = 28.35352...; compute exactly: 5.3248\u00b2 = 28.35351504; \u00d73 = 85.06054512; +58.8+48 = 191.86054512 \u2265 191.85 \u2713.\n  term4 lower: 2(e\u2074+1)(7H\u0302+3.3) \u2265 2\u00b755.5978\u00b7(7\u00b7191.85+3.3) = 111.1956\u00b71346.25 = 149713.7: mul_le_mul (2\u00b755.5978 \u2264 2(e\u2074+1): from e4lo : 54.5978 \u2264 exp 4) (1346.25 \u2264 7H\u0302+3.3: linarith [hHlo]) (0 \u2264 1346.25 norm_num) (0 \u2264 2(e\u2074+1): positivity exp_pos... linarith [Real.exp_pos 4]).\n  e4lo : 54.5978 \u2264 exp 4: rw [exp_four]; le_trans (by norm_num : 54.5978 \u2264 2.7182818283^4) (exp_one_pow_ge 4).\n  Assemble: Bn = 2F + term2 + 53.408 + term4 + IIMaj + 1 \u2265 0 + 124916.25 + 53.408 + 149713.7 + 0 + 1 = 274684.4 \u2265 274000 \u2713.\n  term2 lower number: 4\u00b7283\u00b7110.34987 = 1132\u00b7110.34987 = 124916.25. \u2713\n\nBn_FAlt_100000_le:\n- hT10 : \u221a100000+1 \u2264 318 (sqrt100000_le)\n- log T10 \u2264 5.8: T10 \u2264 318 \u2264 exp 5.8 (exp 5\u00b7exp 0.8 \u2265 148.328\u00b72.2254 = 330.087 \u2265 318 \u2713)\n- log(T10+2) \u2264 5.8 (T10+2 \u2264 320 \u2264 330.087 \u2713)\n- log log T10 \u2264 1.77: log T10 \u2264 5.8 \u2264 exp 1.77 (exp 1\u00b7exp 0.77 \u2265 2.7182818283\u00b72.1597 = 5.87068 \u2713)\n- log log(T10+2) \u2264 1.77 \u2713\n- FAlt T10 \u2264 (1/6)\u00b7(318\u00b75.8) + 0.137\u00b75.8 + 0.443\u00b71.77 + 2.463 = 307.4 + 0.7946 + 0.78411 + 2.463 = 311.44\n- C0hat \u2264 0.433\u00b75.8 + 0.886\u00b71.77 + 2.9 = 2.5114+1.56822+2.9 = 6.97962 \u2192 \u2264 6.9797\n- Hhat \u2264 3\u00b76.9797\u00b2 + 10.5\u00b75.8 + 48 = 3\u00b748.7162 + 60.9 + 48 = 146.149+108.9 = 255.049 \u2192 \u2264 255.05\n- bracket \u2264 (2/3)\u00b76.9797 + 10.5\u00b75.8 + 48 = 4.65313+60.9+48 = 113.55313 \u2192 113.5532\n- term2 \u2264 4\u00b7318\u00b7113.5532 = 1272\u00b7113.5532 = 144439.7\n- term4 \u2264 2\u00b755.6015\u00b7(7\u00b7255.05+3.3) = 111.203\u00b71788.65 = 198893.9\n- IIMaj \u2264 4.56\u00b7318\u00b72 = 2900.16\n- Sum: 2\u00b7311.44 + 144439.7 + 53.408 + 198893.9 + 2900.16 + 1 = 622.88+144439.7+53.408+198893.9+2900.16+1 = 346911.0 \u2264 347000 \u2713 slack 89.\n\nTight but OK (exact arithmetic). Hmm 89 slack on 347000 is 0.026% \u2014 all links are exact rational computations, and every sub-bound was verified with slack; the 89 is just accumulation tightness. Acceptable \u2014 but let me loosen: FAlt \u2264 311.45 (311.44271 exact: 307.4+0.7946+0.78411+2.463 = 311.44271): use 311.45. term2: 1272\u00b7113.5532 = 144439.67. term4: 111.203\u00b71788.65 = 198894.4? compute precisely: 1788.65\u00b7111.203 = 1788.65\u00b7111 = 198540.15 + 1788.65\u00b70.203 = 363.1 \u2192 198903.2? Let me recompute: 7\u00b7255.05 = 1785.35; +3.3 = 1788.65. 111.203\u00b71788.65: 111\u00b71788.65 = 198540.15; 0.203\u00b71788.65 = 363.10; total 198903.25. Hmm I had 198893.9 before \u2014 recompute: 111.203\u00b71788.65 = 1788.65\u00b7111.203. 1788.65\u00b7100 = 178865; \u00b711.203 = 1788.65\u00b711 = 19675.15 + 1788.65\u00b70.203 = 363.10 \u2192 20038.25. Sum: 178865+20038.25 = 198903.25. So term4 \u2264 198903.25. Then total: 622.9 + 144439.67 + 53.408 + 198903.25 + 2900.16 + 1 = 346920.4 \u2264 347000 \u2713 slack 80. Fine (exact).\n\nLet me also recompute Bn80000 term4 exactly: 7\u00b7251.46 = 1760.22; +3.3 = 1763.52; 111.203\u00b71763.52 = 1763.52\u00b7100 = 176352 + 1763.52\u00b711.203 = 1763.52\u00b711 = 19398.72 + 1763.52\u00b70.203 = 358.0 \u2192 19756.7; total 196108.7. Total Bn80000: 547.64 + 127757.29 + 53.408 + 196108.7 + 2590.08 + 1 = 327058.1 \u2264 328000 \u2713 slack 942.\n\nAnd Bn80000_ge term4: 7\u00b7191.85 = 1342.95; +3.3 = 1346.25; 111.1956\u00b71346.25 = 111.1956\u00b71000 = 111195.6 + 111.1956\u00b7346.25 = 38501.4 \u2192 149697.0? compute: 111.1956\u00b7346.25: 111.1956\u00b7300 = 33358.68; \u00b746.25 = 5142.8; total 38501.5. Sum: 111195.6+38501.5 = 149697.1. Total lower: 124916.25 + 53.408 + 149697.1 + 1 = 274667.8 \u2265 274000 \u2713 slack 668.\n\nWait \u2014 I previously had 149715.4 with H\u0302 \u2265 191.86; with 191.85: 7\u00b7191.85+3.3 = 1346.25 \u2713 recomputed 149697.1. Fine.\n\nThese decimal products \u2014 linarith/norm_num compute them exactly \u2713.\n\nOne thing to double check: mul_le_mul argument order convention. mul_le_mul : a \u2264 b \u2192 c \u2264 d \u2192 0 \u2264 c \u2192 0 \u2264 b \u2192 a * c \u2264 b * d. \u2713 (used throughout).\n\npow_le_pow_left : 0 \u2264 a \u2192 a \u2264 b \u2192 \u2200 n, a^n \u2264 b^n? Signature: pow_le_pow_left (ha : 0 \u2264 a) (hab : a \u2264 b) (n : \u2115) : a ^ n \u2264 b ^ n \u2713 (used in file for exp_one_pow etc. \u2014 wait I defined exp_one_pow_le using pow_le_pow_left (exp_pos 1).le (lt_d9.le) n : exp1^n \u2264 2.7182818286^n \u2713).\n\nAlso \u2014 `Real.log_le_log`: signature (hx : 0 < x) (h : x \u2264 y) : log x \u2264 log y? The file used: `Real.log_le_log (Real.exp_pos 2) he2` \u2014 where he2 : exp 2 \u2264 T+2: gives log (exp 2) \u2264 log (T+2) \u2713 so signature (0 < x) \u2192 x \u2264 y \u2192 log x \u2264 log y \u2713.\n\nFinset.sum_range_succ evaluation via norm_num: in iimaj they had h3 : (47 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7, (3.9635:\u211d)^i/(Nat.factorial i : \u211d) := by norm_num [Finset.sum_range_succ] \u2014 note the summand there is x^i/(Nat.factorial i : \u211d) \u2014 the sum_le_exp_of_nonneg summand is x^i / i! where i! is \u2115 cast. Should be the same after push_cast; norm_num [Finset.sum_range_succ] handled it there \u2713. My h2 : (1.34985 : \u211d) \u2264 Real.exp 0.3 := le_trans (by norm_num [Finset.sum_range_succ]) (Real.sum_le_exp_of_nonneg (by norm_num) 7) \u2014 the middle term: le_trans (h : 1.34985 \u2264 ?mid) (sum_le_exp : \u2211 \u2264 exp 0.3) \u2014 ?mid is the \u2211 expression; le_trans needs the first inequality's RHS to match sum_le_exp's LHS syntactically: \u2211 i \u2208 Finset.range 7, (0.3:\u211d)^i/i!. The norm_num proof's goal: 1.34985 \u2264 \u2211 i \u2208 Finset.range 7, 0.3^i/i! \u2014 elaborated from le_trans's type inference: le_trans (_ : 1.34985 \u2264 ?m) (Real.sum_le_exp_of_nonneg ... 7 : \u2211 i \u2208 range 7, 0.3^i / \u2191(i)! \u2264 exp 0.3) \u2014 unifies ?m with the sum \u2713 then norm_num [Finset.sum_range_succ] proves 1.34985 \u2264 sum \u2713. The i! casting: Real.sum_le_exp_of_nonneg statement uses (i : \u2115)! as \u2115 cast to \u211d? From source: `\u2211 i \u2208 range n, x ^ i / i ! \u2264 exp x` \u2014 i! is Nat.factorial cast. In iimaj they matched with (Nat.factorial i : \u211d) explicitly. My version leaves i! \u2014 the elaboration should unify. Risk: cast forms differ; fix at compile if needed by writing the summand explicitly.\n\nLet me now write the complete file. Also add NguyenRH1.lean import + PrintAxioms entries. Given length, write the file in one go, then compile and fix."
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiBasePoints.lean",
  "content": "/-\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 slack \u2265 300 except the flagged tight links\n(e\u00b9\u00b7\u00b9\u2074\u2074\u2078 \u2265 \u03c0 was replaced by the comfortable e\u00b9\u00b7\u00b9\u2075 \u2265 \u03c0 at a 104-unit\ncost, absorbed).\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    field_simp\n  rw [h4]\n  exact pow_le_pow_left (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 (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 (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/-! ### 2. Certified log bounds at the margin points -/\n\n/-- [PROVED session 012] log 80000 \u2265 11.263 (via e\u00b9\u00b9\u00b7\u00b2\u2076\u00b3 \u2264 78063 <\n80000). -/\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 (via e\u00b9\u00b9\u00b7\u00b3 \u2265 80821 > 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 (via e\u00b9\u00b9\u00b7\u2075 \u2264 99661 <\n100000). -/\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 (via 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 (via 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/-! ### 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 value\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_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 value\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_right (by norm_num : (0 : \u211d) < 2)]\n    linarith\n  linarith [g1, g2]\n\n/-- [PROVED session 012] sInftyLower(10\u2075) \u2265 432500 (certified value\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_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] Bn FAlt(8\u00d710\u2074) \u2264 328000 (certified value\n327 053; true 322 309). -/\ntheorem Bn_FAlt_80000_le : Bn FAlt 80000 \u2264 (328000 : \u211d) := by\n  have hT : Real.sqrt 80000 + 1 \u2264 284 := by\n    have := sqrt80000_le\n    linarith\n  have hTpos : (0 : \u211d) < Real.sqrt 80000 + 1 := by\n    have := Real.sqrt_nonneg 80000\n    linarith\n  have hTge : (283 : \u211d) \u2264 Real.sqrt 80000 + 1 := by\n    have := sqrt80000_ge\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 hlogT : Real.log (Real.sqrt 80000 + 1) \u2264 (5.7 : \u211d) := by\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 hbig : Real.sqrt 80000 + 1 \u2264 Real.exp 5.7 := by\n      rw [h57]\n      exact le_trans (by norm_num : Real.sqrt 80000 + 1 \u2264 (284 : \u211d))\n        (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 h := Real.log_le_log hTpos hbig\n    rwa [Real.log_exp] at h\n  -- log (T+2) \u2264 5.7 (T+2 \u2264 286 \u2264 e\u2075\u00b7\u2077)\n  have hlogT2 : Real.log (Real.sqrt 80000 + 1 + 2) \u2264 (5.7 : \u211d) := by\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 hbig : Real.sqrt 80000 + 1 + 2 \u2264 Real.exp 5.7 := by\n      rw [h57]\n      exact le_trans (by norm_num : Real.sqrt 80000 + 1 + 2 \u2264 (286 : \u211d))\n        (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 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 = 5.7544)\n  have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\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 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 hbig : (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 h1 h075 (by norm_num) (Real.exp_pos _).le)\n    have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogTpos (le_trans hlogT hbig)\n    have h57 : Real.log (5.7 : \u211d) \u2264 1.75 := by\n      have h' := Real.log_le_log (by norm_num : (0 : \u211d) < 5.7) hbig\n      rwa [Real.log_exp] at h'\n    linarith [h, h57]\n  -- log log (T+2) \u2264 1.75\n  have hloglogT2 : Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\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 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 hbig : (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 h1 h075 (by norm_num) (Real.exp_pos _).le)\n    have hlogT2pos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1 + 2) :=\n      Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogT2pos (le_trans hlogT2 hbig)\n    have h57 : Real.log (5.7 : \u211d) \u2264 1.75 := by\n      have h' := Real.log_le_log (by norm_num : (0 : \u211d) < 5.7) hbig\n      rwa [Real.log_exp] at h'\n    linarith [h, h57]\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  -- FAlt T \u2264 273.82\n  have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n    unfold FAlt\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    have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264 284 * 5.7 := by\n      apply mul_le_mul hT hlogT (Real.log_nonneg (by linarith)) (by norm_num)\n    have h1 : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_nonneg (by linarith)\n    have h2 : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 283)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\n    linarith [mul_le_mul_of_nonneg_left hTl (by norm_num : (0 : \u211d) \u2264 1 / 6) |>.trans\n      (by norm_num : (1 / 6 : \u211d) * (284 * 5.7) \u2264 269.8)]\n  -- \u0108\u2080 T \u2264 6.9186\n  have hC0 : C0hat (Real.sqrt 80000 + 1) \u2264 (6.9186 : \u211d) := by\n    unfold C0hat\n    linarith [hlogT2, hloglogT2]\n  -- \u0108\u2080 T \u2265 0 (for the product chains)\n  have hC0pos : (0 : \u211d) \u2264 C0hat (Real.sqrt 80000 + 1) := by\n    unfold C0hat\n    have h1 : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1 + 2) :=\n      Real.log_nonneg (by linarith)\n    have h2 : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1 + 2)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 + 2 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 285)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\n    linarith\n  -- H\u0302 T \u2264 251.45\n  have hH : Hhat (Real.sqrt 80000 + 1) \u2264 (251.45 : \u211d) := by\n    unfold Hhat\n    have hsq : C0hat (Real.sqrt 80000 + 1) ^ 2 \u2264 6.9186 ^ 2 :=\n      pow_le_pow_left hC0pos hC0 2\n    linarith [hsq, hlogT2]\n  -- the big bracket \u2264 112.4624\n  have hbr : (2 / 3 : \u211d) * C0hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48 \u2264 112.4624 := by\n    have h1 := mul_le_mul_of_nonneg_left hC0 (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  -- 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 := sqrt80000_le\n    norm_num [this]\n  -- assemble\n  simp only [Bn]\n  have hterm2 : 4 * (Real.sqrt 80000 + 1) * ((2 / 3) * C0hat (Real.sqrt 80000 + 1) +\n      10.5 * Real.log (Real.sqrt 80000 + 1 + 2) + 48) \u2264 4 * 284 * 112.4624 := by\n    apply mul_le_mul _ hbr (by linarith [hC0pos]) (by norm_num)\n    have h4 : (0 : \u211d) \u2264 4 * (Real.sqrt 80000 + 1) := by positivity\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) + 3.3) \u2264\n      2 * (54.6015 + 1) * (7 * 251.45 + 3.3) := by\n    apply mul_le_mul _ _ (by positivity) (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 [mul_le_mul_of_nonneg_left hH (by norm_num : (0 : \u211d) \u2264 7)]\n  linarith [hFAlt, hterm2, hterm4, hII]\n```\n\nHmm wait \u2014 issues with the above draft:\n1. `norm_num [this]` in hII: 4.56\u00b7(\u221a80000+1)\u00b72 \u2264 2590.08: from \u221a80000 \u2264 283: 4.56\u00b7284\u00b72 = 2590.08. norm_num can't do this with sqrt in it. Need: mul_le_mul chains: 4.56*(\u221a+1)*2 \u2264 4.56*284*2 = 2590.08: \n```\n  have hII : IIMaj 80000 \u2264 (2590.08 : \u211d) := by\n    have h1 := IIMaj_le_two_mul 80000 (by norm_num)\n    have h2 : (4.56 : \u211d) * (Real.sqrt 80000 + 1) * 2 \u2264 2590.08 := by\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      norm_num [show (4.56:\u211d)*284*2 = 2590.08 by norm_num]  -- hmm\n    exact le_trans h1 h2\n```\nh2: 4.56*(\u221a80000+1)*2 \u2264 2590.08: from h3: 4.56*(\u221a80000+1) \u2264 4.56*284 = 1295.04; \u00b72 = 2590.08: linarith [h3] after norm_num computing 4.56*284: linarith handles linear arithmetic with numerals \u2014 4.56*284 is a numeral multiplication linarith can evaluate? linarith's preprocessing does ring_nf, so 4.56*284*2 \u2192 2590.08 \u2713 should work: h2 := by have h3 := ...; linarith [h3]. But h3 has \u221a80000 in it: 4.56*(\u221a80000+1) \u2264 4.56*284 \u2014 linarith treats (\u221a80000) as atom: h3 : 4.56*(\u221a80000+1) \u2264 1295.04 after norm_num-eval... linarith will expand 4.56*(\u221a80000+1) = 4.56*\u221a80000 + 4.56 (ring_nf) and h3 gives 4.56*\u221a80000 \u2264 1290.48; goal 4.56*(\u221a80000+1)*2 \u2264 2590.08 \u27fa 9.12\u00b7\u221a80000 + 9.12 \u2264 2590.08 \u27f8 9.12\u00b7283 = 2580.96 + 9.12 = 2590.08 \u2713 \u2014 need \u221a80000 \u2264 283 directly: linarith [sqrt80000_le] should close after ring_nf normalizes. So:\n```\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```\nlinarith: goal 4.56*(\u221a80000+1)*2 \u2264 2590.08; h3: 4.56*(\u221a80000+1) \u2264 4.56*284. ring_nf both: 4.56\u00b7s + 4.56 \u2264 1295.04; goal: 9.12\u00b7s + 9.12 \u2264 2590.08 \u27f8 2\u00b7(4.56s+4.56) \u2264 2\u00b71295.04 = 2590.08 \u2713 linarith closes.\n\n2. In hFAlt: the `linarith [mul_le_mul_of_nonneg_left hTl ... |>.trans ...]` \u2014 the |>.trans inside linarith list: the bracket has pieces:\n   (1/(2\u03c0))\u00b7(T\u00b7log T) \u2264 (1/6)\u00b7(284\u00b75.7) \u2264 269.8: h2pi gives 1/(2\u03c0) \u2264 1/6; then (1/(2\u03c0))\u00b7(T\u00b7logT) \u2264 (1/6)\u00b7(T\u00b7logT) \u2264 (1/6)\u00b7(284\u00b75.7): mul_le_mul_of_nonneg_right h2pi (T\u00b7logT \u2265 0) then mul_le_mul_of_nonneg_left hTl (0 \u2264 1/6)... chain:\n   ha : (1/(2*\u03c0)) * (T8 * log T8) \u2264 (1/6) * (284 * 5.7):\n     mul_le_mul (h2pi) (hTl) (0 \u2264 T8*logT8) (0 \u2264 1/6) \u2014 mul_le_mul : a\u2264b \u2192 c\u2264d \u2192 0\u2264c \u2192 0\u2264b \u2192 a\u00b7c \u2264 b\u00b7d: a = 1/(2\u03c0), b = 1/6, c = T8\u00b7logT8, d = 284\u00b75.7: need 0 \u2264 T8\u00b7logT8 \u2713 (mul_nonneg hTpos.le (log_nonneg)) and 0 \u2264 1/6 \u2713. Gives (1/(2\u03c0))\u00b7(T8\u00b7logT8) \u2264 (1/6)\u00b7(284\u00b75.7) \u2713.\n   Then FAlt T8 = (1/(2\u03c0))\u00b7(T8\u00b7logT8) + 0.137\u00b7logT8 + 0.443\u00b7loglogT8 + (7/8+1.588) \u2264 269.8 + 0.137\u00b75.7 + 0.443\u00b71.75 + 2.463 = 269.8 + 0.7809 + 0.77525 + 2.463 = 273.82. \u2014 wait: (1/6)\u00b7(284\u00b75.7) = 1618.8/6 = 269.8 \u2713. Sum: 269.8+0.7809+0.77525+2.463 = 273.81915 \u2264 273.82 \u2713.\n   linarith [ha, hlogT, hloglogT] \u2014 linarith must multiply 0.137\u00b7logT8 \u2264 0.137\u00b75.7 itself (product of hypotheses \u2014 linarith CAN multiply a hypothesis by a positive constant \u2713 but logT8 is an atom \u00d7 constant \u2014 yes linarith handles).\n   The `(7/8 + 1.588 : \u211d)` \u2014 norm_num-evaluated by linarith's ring_nf \u2713 2.463.\n\n   So hFAlt:\n```\n  have hFAlt : FAlt (Real.sqrt 80000 + 1) \u2264 (273.82 : \u211d) := by\n    unfold FAlt\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    have hTlnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) :=\n      Real.log_nonneg (by linarith)\n    have hTl : (Real.sqrt 80000 + 1) * Real.log (Real.sqrt 80000 + 1) \u2264 284 * 5.7 :=\n      mul_le_mul hT hlogT hTlnn (by norm_num)\n    have hllnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := by\n      apply Real.log_nonneg\n      have he : Real.exp 1 \u2264 Real.sqrt 80000 + 1 :=\n        le_trans Real.exp_one_lt_d9.le (by norm_num : (2.7182818286 : \u211d) \u2264 283)\n      have h := Real.log_le_log (Real.exp_pos 1) he\n      rwa [Real.log_exp] at h\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 hTlnn) (by norm_num)\n    linarith [ha, hlogT, hloglogT]\n```\n   linarith closing: goal (after unfold FAlt): (1/(2\u03c0))\u00b7(T8\u00b7logT8) + 0.137\u00b7logT8 + 0.443\u00b7loglogT8 + (7/8+1.588) \u2264 273.82. From ha: first \u2264 269.8; 0.137\u00b7logT8 \u2264 0.137\u00b75.7 = 0.7809 (linarith multiplies hlogT by 0.137 \u2713); 0.443\u00b7loglogT8 \u2264 0.443\u00b71.75 = 0.77525 \u2713; 7/8+1.588 = 2.463. Total \u2264 269.8+0.7809+0.77525+2.463 = 273.81915 \u2264 273.82 \u2713 linarith closes (needs hlogT, hloglogT in context \u2014 they're haves \u2713 but linarith [ha, hlogT, hloglogT] \u2014 hlogT/hloglogT already in context; passing them again harmless).\n   \n   Wait \u2014 subtlety: 0.137\u00b7logT8 \u2264 0.137\u00b75.7 requires logT8 atom with coefficient \u2014 linarith multiplies hypotheses by POSITIVE constants only when needed; hlogT : log T8 \u2264 5.7 \u2014 linarith can use 0.137\u00b7(hlogT) \u2713 standard.\n\n3. hC0: unfold C0hat: 0.433\u00b7log(T8+2) + 0.886\u00b7log log(T8+2) + 2.9 \u2264 0.433\u00b75.7 + 0.886\u00b71.75 + 2.9 = 6.9186: linarith [hlogT2, hloglogT2] \u2713 (0.433\u00b75.7 = 2.4681, 0.886\u00b71.75 = 1.5505, +2.9 = 6.9186 exact \u2014 linarith handles \u2713).\n\n4. hC0pos: C0hat \u2265 0: pieces nonneg: 0.433\u00b7log(T8+2) \u2265 0 (h1), 0.886\u00b7loglog(T8+2) \u2265 0 (h2), 2.9 \u2265 0: linarith [h1, h2] \u2014 the goal after unfold: 0 \u2264 0.433*log(...) + 0.886*log(...)... + 2.9 \u2014 linarith with h1 : 0 \u2264 log(T8+2), h2 : 0 \u2264 log log(T8+2) \u2713.\n\n5. hH: Hhat = 3\u00b7C0hat\u00b2 + 10.5\u00b7log(T8+2) + 48 \u2264 3\u00b76.9186\u00b2 + 10.5\u00b75.7 + 48: 3\u00b747.867011 = 143.601 + 59.85 + 48 = 251.451 \u2264 251.45?? 3\u00b76.9186\u00b2 = 3\u00b747.8670059... compute: 6.9186\u00b2 = 47.86700...; 6.9186\u00b2 = 47.8670 (6.9186\u00b2 = 47.86700596); \u00d73 = 143.601018; +59.85+48 = 251.451018 > 251.45 \u2717!! TOO TIGHT \u2014 251.451 > 251.45. Adjust: hH \u2264 251.46. Then term4: 7\u00b7251.46+3.3 = 1763.52; 111.203\u00b71763.52 = 196116.4 (+12.8). Total: 327053+12.8 = 327065.8 \u2264 328000 \u2713 fine. Use 251.46.\n\n6. hbr: \u2264 (2/3)\u00b76.9186 + 10.5\u00b75.7 + 48 = 4.6124+59.85+48 = 112.4624 \u2713 exact.\n\n7. hterm2: mul_le_mul _ hbr (by linarith [hC0pos]) (by norm_num): mul_le_mul (a := 4T8) (b := 4\u00b7284) (c := bracket) (d := 112.4624): first arg a \u2264 b: 4\u00b7T8 \u2264 4\u00b7284: mul_le_mul_of_nonneg_left hT (by norm_num : (0:\u211d) \u2264 4) \u2014 my draft had the args wrong order: mul_le_mul h1 h2 h3 h4 where h1 : a \u2264 b = the 4T8 \u2264 4\u00b7284; h2 : c \u2264 d = hbr; h3 : 0 \u2264 c = bracket \u2265 0 \u2014 bracket = (2/3)C0hat + 10.5 log + 48 \u2265 0+0+48: linarith [hC0pos, hlogT2nn] \u2014 need log(T8+2) \u2265 0 (Real.log_nonneg (T8+2 \u2265 1)) \u2014 add have. h4 : 0 \u2264 b = 4\u00b7284 \u2265 0 \u2713 norm_num.\n   Then 4\u00b7284\u00b7112.4624 = 1136\u00b7112.4624 = 127757.29 \u2014 the final linarith [hFAlt, hterm2, hterm4, hII] evaluates numerals \u2713.\n\n8. hterm4: mul_le_mul h41 h42 h43 h44: a = 2(e\u2074+1), b = 2\u00b755.6015, c = 7H\u0302+3.3, d = 7\u00b7251.46+3.3: h41 : 2(e\u2074+1) \u2264 2\u00b755.6015: mul_le_mul_of_nonneg_left (by linarith [he4]) (by norm_num) \u2014 wait 2\u00b7(e\u2074+1) \u2264 2\u00b7(54.6015+1) \u27f8 e\u2074+1 \u2264 54.6015+1 \u27f8 e\u2074 \u2264 54.6015 \u2713 linarith [he4]. h42 : 7H\u0302+3.3 \u2264 7\u00b7251.46+3.3: linarith [mul_le_mul_of_nonneg_left hH (0 \u2264 7)] or just linarith [hH] (linarith can scale hH by 7 \u2713). h43 : 0 \u2264 7H\u0302+3.3: Hhat \u2265 0? Hhat = 3C0\u00b2+10.5 log+48 \u2265 0: 3\u00b7C0\u00b2 \u2265 0 (pow_nonneg/sq), 10.5\u00b7log(T8+2) \u2265 0 \u2713, 48 > 0: need a have hHnn : 0 \u2264 Hhat T8: unfold Hhat; positivity-ish: 3*C0hat^2 \u2265 0 (pow_nonneg hC0pos 2... pow_nonneg needs 0 \u2264 C0hat \u2713), 10.5\u00b7log \u2265 0 (hlogT2nn), 48: linarith [pow_nonneg hC0pos 2, hlogT2nn]. h44 : 0 \u2264 2\u00b755.6015 \u2713 norm_num.\n\n9. Final linarith [hFAlt, hterm2, hterm4, hII]: goal (after simp only [Bn]): 2\u00b7FAlt T8 + 4\u00b7T8\u00b7(bracket) + 40\u00b71.3352 + 2(e\u2074+1)(7H\u0302+3.3) + IIMaj 80000 + 1 \u2264 328000. From: 2\u00b7FAlt \u2264 547.64; term2 \u2264 127757.29; 40\u00b71.3352 = 53.408; term4 \u2264 196116.4; IIMaj \u2264 2590.08; +1. Sum: 547.64+127757.29+53.408+196116.4+2590.08+1 = 327065.8 \u2264 328000 \u2713 slack 934.\n\nBut WAIT \u2014 after `simp only [Bn]`, does the goal keep `C0hat`, `Hhat`, `FAlt` folded? simp only [Bn] unfolds only Bn \u2014 the goal has FAlt (\u221a80000+1), C0hat (\u221a80000+1), Hhat (\u221a80000+1), Real.log (\u221a80000+1+2), IIMaj 80000, Real.exp 4 \u2014 matches my haves \u2713 (assuming the let zeta-reduces, giving Real.sqrt 80000 + 1 for T everywhere, and T + 2 becomes Real.sqrt 80000 + 1 + 2 \u2713).\n\nPotential mismatch: `10.5 * Real.log (T + 2)` with T = \u221a80000+1 gives Real.log (\u221a80000 + 1 + 2) \u2713 my haves use exactly that form \u2713. And C0hat/Hhat unfolded inside Bn? NO \u2014 Bn references C0hat T and Hhat T by name; simp only [Bn] leaves them folded \u2713. hC0/hH unfold them locally \u2713. But the FINAL goal has C0hat (\u221a80000+1) etc. \u2014 my hterm2's statement I wrote with explicit ((2/3)*C0hat(...) + ...) \u2014 matches \u2713.\n\nOne more: hloglogT's inner proof uses hlogT \u2014 fine (local). And hloglogT uses le_trans hlogT hbig: log T8 \u2264 5.7 \u2264 exp 1.75 \u2192 log T8 \u2264 exp 1.75; then Real.log_le_log hlogTpos (le_trans hlogT hbig) : log (log T8) \u2264 log (exp 1.75)?? NO \u2014 Real.log_le_log (hx : 0 < x) (h : x \u2264 y) : log x \u2264 log y. With x = log T8, y = exp 1.75: log(log T8) \u2264 log(exp 1.75) = 1.75 \u2014 I did an extra step via log 5.7: `h := Real.log_le_log hlogTpos (le_trans hlogT hbig) : Real.log (Real.log T8) \u2264 Real.log (Real.exp 1.75)`; then Real.log_exp: log(exp 1.75) = 1.75 \u2014 my draft wrote h then h57 separately then linarith [h, h57] \u2014 h57 : log 5.7 \u2264 1.75 \u2014 that's the WRONG piece; the clean way: h : log(log T8) \u2264 log(exp 1.75); rwa [Real.log_exp] at h. My draft's h57 dance was unnecessary and the linarith [h, h57] where h : log(log T8) \u2264 log(exp 1.75) \u2014 linarith can't simplify log(exp 1.75) (atom). FIX: rwa [Real.log_exp] at h \u2014 direct. Let me restructure hloglogT:\n```\n  have hloglogT : Real.log (Real.log (Real.sqrt 80000 + 1)) \u2264 (1.75 : \u211d) := by\n    have h1 : (2.7182818283 : \u211d) \u2264 Real.exp 1 := Real.exp_one_gt_d9.le\n    have h075 : (2.1169 : \u211d) \u2264 Real.exp 0.75 := ...\n    have h175 : Real.exp 1.75 = Real.exp 1 * Real.exp 0.75 := ...\n    have hbig : (5.7 : \u211d) \u2264 Real.exp 1.75 := ...\n    have hlogTpos : (0 : \u211d) < Real.log (Real.sqrt 80000 + 1) := Real.log_pos (by linarith)\n    have h := Real.log_le_log hlogTpos (le_trans hlogT hbig)\n    rwa [Real.log_exp] at h\n```\nle_trans hlogT hbig : log T8 \u2264 exp 1.75 \u2713 (hlogT : log T8 \u2264 5.7; hbig : 5.7 \u2264 exp 1.75). Real.log_le_log hlogTpos (that) : log (log T8) \u2264 log (exp 1.75); rw log_exp: = 1.75 \u2713 DONE. \u2713 cleaner.\n\nReal.log_pos (1 < x): T8 > 1: from hTge : 283 \u2264 T8: linarith \u2713 \u2014 hlogTpos uses Real.log_pos (by linarith) \u2014 needs 1 < \u221a80000+1 in context-solvable form: hTge present? I define hlogTpos inside hloglogT where hTge is in scope (declared before) \u2713 but linarith needs hTge explicitly? linarith uses context \u2713 hTge is a have in the proof \u2713.\n\nOK. Given the scale, let me write the file with all these corrections baked in, compile, iterate. For Bn_FAlt_80000_ge and Bn_FAlt_100000_le similar structure. To keep the response manageable I'll write the complete file now.\n\nFor Bn_FAlt_80000_ge (lower bound):\n- hFAlt0 : 0 \u2264 FAlt T8: unfold FAlt; pieces \u2265 0: (1/(2\u03c0))\u00b7(T8\u00b7log T8): positivity with hTlnn (log T8 \u2265 0) and pi_pos: (1/(2\u03c0)) \u2265 0: positivity knows \u03c0 > 0? positivity has an extension for Real.pi \u2713 (Real.pi_pos via positivity? I think positivity proves 0 < \u03c0 \u2014 there's a positivity extension for pi). mul_nonneg chains + linarith. Write:\n```\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 hTlnn : (0 : \u211d) \u2264 Real.log (Real.sqrt 80000 + 1) := Real.log_nonneg (by linarith)\n    have hllnn : (0 : \u211d) \u2264 Real.log (Real.log (Real.sqrt 80000 + 1)) := ... (as before)\n    have hp1 : (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * ((Real.sqrt 80000 + 1) *\n        Real.log (Real.sqrt 80000 + 1)) := by positivity  -- needs log T8 \u2265 0 in context: positivity uses hypotheses? positivity does NOT use hypotheses. Use mul_nonneg: mul_nonneg (by positivity) (mul_nonneg hTpos.le hTlnn)\n    linarith [hp1, mul_nonneg (by norm_num : (0:\u211d) \u2264 0.137) hTlnn, mul_nonneg (by norm_num : (0:\u211d) \u2264 0.443) hllnn]\n```\n  positivity for 1/(2\u03c0) \u2265 0: positivity should handle (pi_pos extension exists \u2713).\n\n- term2 lower: 4\u00b7T8\u00b7bracket \u2265 4\u00b7283\u00b7110.34987: hbrlo : bracket \u2265 (2/3)\u00b75.3248 + 10.5\u00b75.6 + 48 = 110.34987: needs C0hat \u2265 5.3248 (hC0lo : 0.433\u00b7log(T8+2) \u2265 0.433\u00b75.6 from logT82_ge; 0.886\u00b7loglog \u2265 0; +2.9: linarith) and 10.5\u00b7log \u2265 10.5\u00b75.6 \u2713 linarith.\n  logT82_ge : 5.6 \u2264 log (T8+2): T8+2 \u2265 285 \u2265 exp 5.6: exp 5.6 = exp 5\u00b7exp 0.6 \u2264 148.414\u00b71.8433 = 273.571: \n  h5up : exp 5 \u2264 148.414 (exp_five + exp_one_pow_le 5 + norm_num)\n  h06up : exp 0.6 \u2264 1.8433 (exp_le_inv_sub_sixteen + norm_num)\n  h56 : exp 5.6 = exp 5\u00b7exp 0.6\n  T8+2 \u2265 285 (hTge: T8 \u2265 283); 285 \u2265 273.571 \u2265 exp 5.6: Real.log_le_log (exp_pos) (285 \u2265 exp 5.6 via le_trans) : 5.6 = log(exp 5.6) \u2264 log 285 \u2264 log(T8+2) \u2014 chain: log 285 \u2265 5.6 then log(T8+2) \u2265 log 285 (T8+2 \u2265 285): two log_le_log steps.\n  hC0lo : C0hat T8 \u2265 5.3248: unfold C0hat: 0.433\u00b7log(T8+2) \u2265 0.433\u00b75.6 = 2.4248; 0.886\u00b7loglog(T8+2) \u2265 0; +2.9: linarith [logT82_ge, hllT2nn].\n  hHlo : Hhat T8 \u2265 191.86: 3\u00b7C0hat\u00b2 \u2265 3\u00b75.3248\u00b2 (pow_le_pow_left (5.3248 \u2265 0) hC0lo 2): 3\u00b728.35352 = 85.0606; 10.5\u00b7log(T8+2) \u2265 10.5\u00b75.6 = 58.8; +48: 85.0606+58.8+48 = 191.8606 \u2265 191.86 \u2713 (0.0006 margin \u2014 exact rational, OK but tight; use 191.85: 191.8606 \u2265 191.85 \u2713 safer).\n  5.3248\u00b2 = 28.35352...; compute exactly: 5.3248\u00b2 = 28.35351504; \u00d73 = 85.06054512; +58.8+48 = 191.86054512 \u2265 191.85 \u2713.\n  term4 lower: 2(e\u2074+1)(7H\u0302+3.3) \u2265 2\u00b755.5978\u00b7(7\u00b7191.85+3.3) = 111.1956\u00b71346.25 = 149713.7: mul_le_mul (2\u00b755.5978 \u2264 2(e\u2074+1): from e4lo : 54.5978 \u2264 exp 4) (1346.25 \u2264 7H\u0302+3.3: linarith [hHlo]) (0 \u2264 1346.25 norm_num) (0 \u2264 2(e\u2074+1): positivity exp_pos... linarith [Real.exp_pos 4]).\n  e4lo : 54.5978 \u2264 exp 4: rw [exp_four]; le_trans (by norm_num : 54.5978 \u2264 2.7182818283^4) (exp_one_pow_ge 4).\n  Assemble: Bn = 2F + term2 + 53.408 + term4 + IIMaj + 1 \u2265 0 + 124916.25 + 53.408 + 149713.7 + 0 + 1 = 274684.4 \u2265 274000 \u2713.\n  term2 lower number: 4\u00b7283\u00b7110.34987 = 1132\u00b7110.34987 = 124916.25. \u2713\n\nBn_FAlt_100000_le:\n- hT10 : \u221a100000+1 \u2264 318 (sqrt100000_le)\n- log T10 \u2264 5.8: T10 \u2264 318 \u2264 exp 5.8 (exp 5\u00b7exp 0.8 \u2265 148.328\u00b72.2254 = 330.087 \u2265 318 \u2713)\n- log(T10+2) \u2264 5.8 (T10+2 \u2264 320 \u2264 330.087 \u2713)\n- log log T10 \u2264 1.77: log T10 \u2264 5.8 \u2264 exp 1.77 (exp 1\u00b7exp 0.77 \u2265 2.7182818283\u00b72.1597 = 5.87068 \u2713)\n- log log(T10+2) \u2264 1.77 \u2713\n- FAlt T10 \u2264 (1/6)\u00b7(318\u00b75.8) + 0.137\u00b75.8 + 0.443\u00b71.77 + 2.463 = 307.4 + 0.7946 + 0.78411 + 2.463 = 311.44\n- C0hat \u2264 0.433\u00b75.8 + 0.886\u00b71.77 + 2.9 = 2.5114+1.56822+2.9 = 6.97962 \u2192 \u2264 6.9797\n- Hhat \u2264 3\u00b76.9797\u00b2 + 10.5\u00b75.8 + 48 = 3\u00b748.7162 + 60.9 + 48 = 146.149+108.9 = 255.049 \u2192 \u2264 255.05\n- bracket \u2264 (2/3)\u00b76.9797 + 10.5\u00b75.8 + 48 = 4.65313+60.9+48 = 113.55313 \u2192 113.5532\n- term2 \u2264 4\u00b7318\u00b7113.5532 = 1272\u00b7113.5532 = 144439.7\n- term4 \u2264 2\u00b755.6015\u00b7(7\u00b7255.05+3.3) = 111.203\u00b71788.65 = 198893.9\n- IIMaj \u2264 4.56\u00b7318\u00b72 = 2900.16\n- Sum: 2\u00b7311.44 + 144439.7 + 53.408 + 198893.9 + 2900.16 + 1 = 622.88+144439.7+53.408+198893.9+2900.16+1 = 346911.0 \u2264 347000 \u2713 slack 89.\n\nTight but OK (exact arithmetic). Hmm 89 slack on 347000 is 0.026% \u2014 all links are exact rational computations, and every sub-bound was verified with slack; the 89 is just accumulation tightness. Acceptable \u2014 but let me loosen: FAlt \u2264 311.45 (311.44271 exact: 307.4+0.7946+0.78411+2.463 = 311.44271): use 311.45. term2: 1272\u00b7113.5532 = 144439.67. term4: 111.203\u00b71788.65 = 198894.4? compute precisely: 1788.65\u00b7111.203 = 1788.65\u00b7111 = 198540.15 + 1788.65\u00b70.203 = 363.1 \u2192 198903.2? Let me recompute: 7\u00b7255.05 = 1785.35; +3.3 = 1788.65. 111.203\u00b71788.65: 111\u00b71788.65 = 198540.15; 0.203\u00b71788.65 = 363.10; total 198903.25. Hmm I had 198893.9 before \u2014 recompute: 111.203\u00b71788.65 = 1788.65\u00b7111.203. 1788.65\u00b7100 = 178865; \u00b711.203 = 1788.65\u00b711 = 19675.15 + 1788.65\u00b70.203 = 363.10 \u2192 20038.25. Sum: 178865+20038.25 = 198903.25. So term4 \u2264 198903.25. Then total: 622.9 + 144439.67 + 53.408 + 198903.25 + 2900.16 + 1 = 346920.4 \u2264 347000 \u2713 slack 80. Fine (exact).\n\nLet me also recompute Bn80000 term4 exactly: 7\u00b7251.46 = 1760.22; +3.3 = 1763.52; 111.203\u00b71763.52 = 1763.52\u00b7100 = 176352 + 1763.52\u00b711.203 = 1763.52\u00b711 = 19398.72 + 1763.52\u00b70.203 = 358.0 \u2192 19756.7; total 196108.7. Total Bn80000: 547.64 + 127757.29 + 53.408 + 196108.7 + 2590.08 + 1 = 327058.1 \u2264 328000 \u2713 slack 942.\n\nAnd Bn80000_ge term4: 7\u00b7191.85 = 1342.95; +3.3 = 1346.25; 111.1956\u00b71346.25 = 111.1956\u00b71000 = 111195.6 + 111.1956\u00b7346.25 = 38501.4 \u2192 149697.0? compute: 111.1956\u00b7346.25: 111.1956\u00b7300 = 33358.68; \u00b746.25 = 5142.8; total 38501.5. Sum: 111195.6+38501.5 = 149697.1. Total lower: 124916.25 + 53.408 + 149697.1 + 1 = 274667.8 \u2265 274000 \u2713 slack 668.\n\nWait \u2014 I previously had 149715.4 with H\u0302 \u2265 191.86; with 191.85: 7\u00b7191.85+3.3 = 1346.25 \u2713 recomputed 149697.1. Fine.\n\nThese decimal products \u2014 linarith/norm_num compute them exactly \u2713.\n\nOne thing to double check: mul_le_mul argument order convention. mul_le_mul : a \u2264 b \u2192 c \u2264 d \u2192 0 \u2264 c \u2192 0 \u2264 b \u2192 a * c \u2264 b * d. \u2713 (used throughout).\n\npow_le_pow_left : 0 \u2264 a \u2192 a \u2264 b \u2192 \u2200 n, a^n \u2264 b^n? Signature: pow_le_pow_left (ha : 0 \u2264 a) (hab : a \u2264 b) (n : \u2115) : a ^ n \u2264 b ^ n \u2713 (used in file for exp_one_pow etc. \u2014 wait I defined exp_one_pow_le using pow_le_pow_left (exp_pos 1).le (lt_d9.le) n : exp1^n \u2264 2.7182818286^n \u2713).\n\nAlso \u2014 `Real.log_le_log`: signature (hx : 0 < x) (h : x \u2264 y) : log x \u2264 log y? The file used: `Real.log_le_log (Real.exp_pos 2) he2` \u2014 where he2 : exp 2 \u2264 T+2: gives log (exp 2) \u2264 log (T+2) \u2713 so signature (0 < x) \u2192 x \u2264 y \u2192 log x \u2264 log y \u2713.\n\nFinset.sum_range_succ evaluation via norm_num: in iimaj they had h3 : (47 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7, (3.9635:\u211d)^i/(Nat.factorial i : \u211d) := by norm_num [Finset.sum_range_succ] \u2014 note the summand there is x^i/(Nat.factorial i : \u211d) \u2014 the sum_le_exp_of_nonneg summand is x^i / i! where i! is \u2115 cast. Should be the same after push_cast; norm_num [Finset.sum_range_succ] handled it there \u2713. My h2 : (1.34985 : \u211d) \u2264 Real.exp 0.3 := le_trans (by norm_num [Finset.sum_range_succ]) (Real.sum_le_exp_of_nonneg (by norm_num) 7) \u2014 the middle term: le_trans (h : 1.34985 \u2264 ?mid) (sum_le_exp : \u2211 \u2264 exp 0.3) \u2014 ?mid is the \u2211 expression; le_trans needs the first inequality's RHS to match sum_le_exp's LHS syntactically: \u2211 i \u2208 Finset.range 7, (0.3:\u211d)^i/i!. The norm_num proof's goal: 1.34985 \u2264 \u2211 i \u2208 Finset.range 7, 0.3^i/i! \u2014 elaborated from le_trans's type inference: le_trans (_ : 1.34985 \u2264 ?m) (Real.sum_le_exp_of_nonneg ... 7 : \u2211 i \u2208 range 7, 0.3^i / \u2191(i)! \u2264 exp 0.3) \u2014 unifies ?m with the sum \u2713 then norm_num [Finset.sum_range_succ] proves 1.34985 \u2264 sum \u2713. The i! casting: Real.sum_le_exp_of_nonneg statement uses (i : \u2115)! as \u2115 cast to \u211d? From source: `\u2211 i \u2208 range n, x ^ i / i ! \u2264 exp x` \u2014 i! is Nat.factorial cast. In iimaj they matched with (Nat.factorial i : \u211d) explicitly. My version leaves i! \u2014 the elaboration should unify. Risk: cast forms differ; fix at compile if needed by writing the summand explicitly.\n\nLet me now write the complete file. Also add NguyenRH1.lean import + PrintAxioms entries. Given length, write the file in one go, then compile and fix.",
  "structuredPatch": [],
  "originalFile": null
}