exp_taylor_10_at_0481
plain-language theorem explainer
The definition supplies the explicit 10-term Taylor partial sum for exp at the rational point 481/1000. Numerics workers tightening interval bounds on the inverse fine-structure constant reference this value to control the approximation error for exp(0.481). The body is a direct abbreviation that assembles the sum in rational arithmetic.
Claim. Let $x = 481/1000$. Define the partial sum $s_{10}(x) := 1 + x + x^2/2! + x^3/3! + x^4/4! + x^5/5! + x^6/6! + x^7/7! + x^8/8! + x^9/9!$.
background
The module develops rigorous interval bounds on the inverse fine-structure constant α⁻¹ using symbolic derivation. It imports interval tools from W8Bounds and constants from Alpha. The upstream definition in the Log module supplies the identical rational Taylor sum at x = 481/1000, which is reused here to anchor exponential bounds.
proof idea
The definition is a one-line abbreviation that substitutes x = 481/1000 into the truncated exponential series and evaluates the resulting rational expression.
why it matters
This rational value feeds the lemmas exp_0481_lt and exp_0481_taylor_ceiling, which in turn support log_phi_gt_0481 establishing log(φ) > 0.481. The bound enters Recognition Science via the phi-ladder and the self-similar fixed point T6, tightening the numerical window around α⁻¹.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.