exp_taylor_10_at_neg_00866
plain-language theorem explainer
The definition computes the exact rational value of the degree-9 Taylor polynomial for exp(x) at x = -0.00866. Interval-bound researchers on the inverse fine-structure constant cite this approximation when closing numerical enclosures around alpha inverse. The definition proceeds by direct substitution of the rational argument into the truncated power series with exact factorial denominators.
Claim. Let $x = -0.00866$. The tenth-order Taylor approximation to the exponential is the rational $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$.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant using symbolic derivation. This definition supplies the truncated Taylor sum needed to bound the real exponential at a specific negative argument that appears in the alpha calculation. The module imports W8Bounds for interval machinery and Alpha for the target constant.
proof idea
The definition is a direct algebraic expansion: it binds the rational x = -866/100000 and adds the ten explicit power-series terms with their factorial denominators, all performed in exact rational arithmetic.
why it matters
The definition is referenced by the lemmas exp_neg_00866_lt and exp_neg_00866_taylor_ceiling that close the enclosure Real.exp(-0.00866) < 495689/500000. It therefore participates in the module's interval bounds on alpha inverse, which the Recognition Science framework requires to lie inside (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.