exp_048_lt
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.