exp_taylor_10_at_048
plain-language theorem explainer
Definition of the tenth-order Taylor sum for the exponential at the rational 0.48. Interval proofs for the golden-ratio lower bound on log(phi) cite this value to close the comparison exp(0.48) < phi. The body is a direct substitution of x = 48/100 into the explicit sum of the first ten power terms.
Claim. Let $x = 48/100$. The tenth partial sum of the Taylor series for exp at $x$ 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 Numerics.Interval.Log module supplies rigorous interval bounds for the natural logarithm by monotonicity on (0, ∞) together with Taylor expansions of log(1 + x) for |x| < 1, with remainder controlled by |x|^{n+1}/((n+1)(1 - |x|)). This definition supplies the truncated exponential series at 0.48 that converts an upper bound on the partial sum into an upper bound on exp(0.48) via monotonicity. An identical definition appears in the sibling AlphaBounds module, where the same rational seed supports bounds on the fine-structure constant.
proof idea
Direct definition that sets the rational x equal to 48/100 and assembles the sum of the first ten terms of the exponential Taylor series using the explicit factorial denominators.
why it matters
Supplies the concrete rational needed to prove log(phi) > 0.48 via the equivalence log(phi) > 0.48 iff phi > exp(0.48). This inequality anchors the phi-ladder mass formula and confirms the self-similar fixed point required by the forcing chain T5-T6. It is invoked by log_phi_gt_048 and by the ceiling lemma exp_048_taylor_ceiling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.