exp_048_lt_phi

formal source

 186  x^10 * 11 / (Nat.factorial 10 * 10)
 187
 188/-- exp(0.48) < φ (via Taylor bound + φ lower bound) -/
 189private lemma exp_048_lt_phi : exp_taylor_10_at_048 + exp_error_10_at_048 < 161803395 / 100000000 := by
 190  native_decide
 191
 192/-- Rigorous lower bound: log(φ) > 0.48
 193
 194    Proof using exp monotonicity: log(φ) > 0.48 ↔ φ > exp(0.48).
 195    We have φ > 1.61803395 and exp(0.48) ≈ 1.6160... < 1.61803395. -/
 196theorem log_phi_gt_048 : (0.48 : ℝ) < log Real.goldenRatio := by
 197  -- Equivalent to: exp(0.48) < φ
 198  rw [Real.lt_log_iff_exp_lt Real.goldenRatio_pos]
 199  -- Use Taylor bound for exp(0.48)
 200  have hx_pos : (0 : ℝ) ≤ (0.48 : ℝ) := by norm_num
 201  have hx_le1 : (0.48 : ℝ) ≤ 1 := by norm_num
 202  have h_bound := Real.exp_bound' hx_pos hx_le1 (n := 10) (by norm_num : 0 < 10)
 203  -- exp(0.48) ≤ S_10 + error
 204  have h_taylor_eq : (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) =
 205      (exp_taylor_10_at_048 : ℝ) := by
 206    simp only [exp_taylor_10_at_048, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
 207    norm_num
 208  have h_err_eq : (0.48 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) =
 209      (exp_error_10_at_048 : ℝ) := by
 210    simp only [exp_error_10_at_048, Nat.factorial]
 211    norm_num
 212  have h_lt := exp_048_lt_phi
 213  calc Real.exp (0.48 : ℝ)
 214      ≤ (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) +
 215        (0.48 : ℝ)^10 * (10 + 1) / (Nat.factorial 10 * 10) := h_bound
 216    _ = (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by rw [h_taylor_eq, h_err_eq]
 217    _ < ((161803395 / 100000000 : ℚ) : ℝ) := by exact_mod_cast h_lt
 218    _ = (1.61803395 : ℝ) := by norm_num
 219    _ < Real.goldenRatio := phi_gt_161803395