exp_048_lt
The lemma proves exp(0.48) is strictly less than 1.6161. Researchers tightening numerical intervals for the inverse fine-structure constant in Recognition Science cite it to anchor exponential comparisons involving phi. The proof invokes the order-10 Taylor remainder bound, equates the partial sum and error to sibling constants via simplification and norm_num, then chains the resulting upper bound through a native-decided ceiling.
claim$e^{0.48} < 1.6161$
background
The module Numerics.Interval.AlphaBounds supplies rigorous interval bounds on alpha inverse using symbolic derivations. It defines exp_taylor_10_at_048 as the partial sum 1 + x + x^2/2! + ... + x^9/9! evaluated at x = 0.48, and exp_error_10_at_048 as the explicit remainder bound x^{10} * 11 / (10! * 10). These feed into comparisons against the rational 16161/10000. Upstream arithmetic lemmas from ArithmeticFromLogic (add_assoc, add_comm, succ) guarantee the algebraic rewrites in the bound calculations are valid.
proof idea
The tactic proof first applies Real.exp_bound at n=10 to obtain the remainder inequality. It then uses simp and norm_num to match the Taylor sum to exp_taylor_10_at_048 and the error term to exp_error_10_at_048. A calc block rewrites the upper bound to their sum; this is shown strictly below 1.6161 by exp_048_taylor_ceiling. The final step applies lt_of_le_of_lt.
why it matters in Recognition Science
This lemma is invoked by log_phi_gt_048 to establish 0.48 < log phi, which anchors the lower end of the interval (137.030, 137.039) for alpha inverse. It supplies a concrete numerical step in the Recognition Science forcing chain that connects the J-uniqueness fixed point to the eight-tick octave and D=3 spatial dimensions. The bound closes one link in the phi-ladder mass formula verification.
scope and limits
- Does not provide a matching lower bound on exp(0.48).
- Does not extend the Taylor estimate to |x| > 1.
- Does not compute the exact decimal expansion of exp(0.48).
- Does not address truncation orders other than n=10.
formal statement (Lean)
45private lemma exp_048_lt : Real.exp (0.48 : ℝ) < (((16161 / 10000 : ℚ) : ℝ)) := by
proof body
Tactic-mode proof.
46 have hx_abs : |(0.48 : ℝ)| ≤ 1 := by norm_num
47 have h_bound := Real.exp_bound hx_abs (n := 10) (by norm_num : 0 < 10)
48 have h_abs := abs_sub_le_iff.mp h_bound
49 have h_taylor_eq :
50 (∑ m ∈ Finset.range 10, (0.48 : ℝ)^m / m.factorial) =
51 (exp_taylor_10_at_048 : ℝ) := by
52 simp only [exp_taylor_10_at_048, Finset.sum_range_succ, Finset.sum_range_zero, Nat.factorial]
53 norm_num
54 have h_err_eq :
55 |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) =
56 (exp_error_10_at_048 : ℝ) := by
57 simp only [exp_error_10_at_048, Nat.factorial, Nat.succ_eq_add_one]
58 norm_num
59 have h_upper_raw :
60 Real.exp (0.48 : ℝ) ≤
61 |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
62 (exp_taylor_10_at_048 : ℝ) := by
63 simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.1
64 have h_upper :
65 Real.exp (0.48 : ℝ) ≤ (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by
66 calc
67 Real.exp (0.48 : ℝ)
68 ≤ |(0.48 : ℝ)|^10 * ((Nat.succ 10 : ℕ) / ((Nat.factorial 10 : ℕ) * 10)) +
69 (exp_taylor_10_at_048 : ℝ) := h_upper_raw
70 _ = (exp_error_10_at_048 : ℝ) + (exp_taylor_10_at_048 : ℝ) := by rw [h_err_eq]
71 _ = (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) := by ring
72 have h_num :
73 (exp_taylor_10_at_048 : ℝ) + (exp_error_10_at_048 : ℝ) <
74 (((16161 / 10000 : ℚ) : ℝ)) := by
75 exact_mod_cast exp_048_taylor_ceiling
76 exact lt_of_le_of_lt h_upper h_num
77