exp_neg_00866_lt
plain-language theorem explainer
This lemma proves that exp(-0.00866) is strictly less than the rational 495689/500000. Numerics work on the inverse fine-structure constant in Recognition Science cites it to close the upper end of the alphaInv interval. The proof applies the order-10 Taylor remainder bound for the exponential, equates the partial sum and error to precomputed rationals, then chains the resulting inequality through a native-decided ceiling lemma.
Claim. $e^{-0.00866} < 495689/500000$
background
The lemma lives in the module that supplies rigorous interval bounds on alphaInv, the dimensionless inverse fine-structure constant defined by alpha_seed * exp(-(f_gap / alpha_seed)). The local setting fixes the evaluation point -0.00866 that appears when the gap ratio is inserted into the exponential factor, then controls the value via a degree-10 Taylor expansion whose remainder is bounded by the standard Lagrange form. Upstream results include the definition of alphaInv itself, which states that the constant is obtained from the structural seed and gap with zero adjustable parameters, together with the auxiliary definitions exp_taylor_10_at_neg_00866 and exp_error_10_at_neg_00866 that precompute the partial sum and the explicit error term at this point.
proof idea
The tactic proof first records that the absolute value of the argument is at most 1, then calls Real.exp_bound with n=10 to obtain the remainder estimate. It rewrites the Taylor sum and the error term to the sibling definitions exp_taylor_10_at_neg_00866 and exp_error_10_at_neg_00866 by simp and norm_num. The upper bound is formed by adding these two rationals; the final strict inequality follows by applying the companion lemma exp_neg_00866_taylor_ceiling and using lt_of_le_of_lt.
why it matters
The lemma supplies the concrete numerical step needed for the downstream theorem alphaInv_lt that asserts alphaInv < 137.039. It therefore completes one side of the interval (137.030, 137.039) that the Recognition Science framework predicts for the fine-structure constant from the phi-ladder and the eight-tick octave. The result is part of the chain that derives alpha from the forcing steps T5 through T8 without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.