exp_taylor_10_at_0483
plain-language theorem explainer
The definition supplies the explicit 10-term Taylor polynomial for the exponential at the rational 483/1000. Interval-arithmetic proofs that compare the golden ratio to exp(0.483) cite this partial sum to obtain a concrete lower bound. It arises by direct substitution of x = 483/1000 into the truncated series sum_{k=0 to 9} x^k / k!.
Claim. Let $x = 483/1000$. Define the partial sum $s_{10}(x) = 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 for the natural logarithm on (0, ∞) by monotonicity together with Taylor remainders for log(1+x) when |x|<1. For the golden-ratio comparison the strategy inverts the inequality: an explicit lower bound on exp(0.483) yields log(φ) < 0.483 once φ is known to lie below that value. The upstream AlphaBounds module contains an identical definition of the same partial sum, confirming that the numeric anchor is shared across the interval-arithmetic layer.
proof idea
The definition is a direct literal expansion: bind x to the rational 483/1000 and write out the ten explicit terms of the exponential series up to degree 9. No external lemmas or tactics are invoked; the body is the closed-form polynomial itself.
why it matters
The partial sum is invoked by log_phi_lt_0483 and phi_lt_exp_0483 to close the comparison φ < exp(0.483), which anchors the phi-ladder numerics required by the self-similar fixed-point step (T6) of the forcing chain. It thereby supports the eight-tick octave (T7) and the alpha-inverse interval (137.030, 137.039) by furnishing a machine-checked rational lower bound that downstream mass and coupling formulas can reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.