exp_0481_lt
plain-language theorem explainer
The lemma establishes that exp(0.481) is strictly less than 1.6177. It is cited when deriving logarithmic comparisons to the golden ratio in Recognition Science bounds on the inverse fine-structure constant. The argument invokes the order-10 Taylor remainder for the exponential, equates the polynomial and error terms to precomputed rationals via simp and norm_num, then chains the resulting upper bound through a ceiling lemma.
Claim. $ e^{0.481} < 1.6177 $
background
The Numerics.Interval.AlphaBounds module supplies rigorous rational enclosures for alpha inverse by Taylor expansion of the exponential. The sibling definitions exp_taylor_10_at_0481 and exp_error_10_at_0481 compute the degree-9 partial sum and the explicit Lagrange remainder bound at argument 0.481, respectively. These are combined with the standard-library bound Real.exp_bound to obtain machine-verifiable inequalities without floating-point rounding.
proof idea
The tactic proof first confirms |0.481| <= 1. It applies Real.exp_bound (n:=10) to produce an inequality between exp(x) and the Taylor sum plus remainder. Simp and norm_num identify the sum with exp_taylor_10_at_0481 and the remainder with exp_error_10_at_0481. A short calc rewrites the upper bound as their sum, after which exp_0481_taylor_ceiling supplies the final strict comparison to 1.6177 and lt_of_le_of_lt closes the goal.
why it matters
The result is used by log_phi_gt_0481 to show 0.481 < log phi. In the Recognition Science framework this comparison anchors the placement of alpha inverse inside (137.030, 137.039) once phi is identified with the self-similar fixed point forced by J-uniqueness and the eight-tick octave. It therefore supplies a concrete numerical step in the derivation of the fine-structure constant from the forcing chain T5-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.