exp_neg_00866_taylor_ceiling
plain-language theorem explainer
This lemma verifies that the 10-term Taylor sum for exp(-0.00866) plus its explicit remainder bound is strictly less than the rational 495689/500000. It is invoked by the proof that the real exponential at this argument lies below the same threshold. The verification is a direct exact rational computation.
Claim. $1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880 + |x|^{10}·11/(10!·10) < 495689/500000$ where $x = -0.00866$.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant using symbolic derivations and Taylor expansions with controlled remainders. Upstream definitions compute the explicit 10-term Taylor polynomial for exp at argument -0.00866 together with the Lagrange-style remainder estimate $x^{10}·11/(10!·10)$ for |x| = 0.00866.
proof idea
One-line wrapper that applies native_decide to confirm the rational inequality by exact arithmetic on the supplied Taylor sum and error term.
why it matters
The lemma feeds exp_neg_00866_lt, which supplies the real-valued exponential bound required for the alpha inverse interval. It forms part of the numerical scaffolding that places alpha inverse inside (137.030, 137.039), consistent with the Recognition Science prediction for the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.