exp_taylor_10_at_048
plain-language theorem explainer
The definition supplies the tenth-order Taylor polynomial for exp evaluated at the rational 0.48. Interval-arithmetic workers tightening alpha inverse bounds in Recognition Science cite this rational when comparing exp(0.48) to phi. It is obtained by direct substitution of x = 48/100 into the truncated series and term-by-term rational evaluation.
Claim. Let $x = 48/100$. Define the partial sum $s_{10}(0.48) := 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 alphaInv via symbolic derivations that invoke the golden ratio phi. The Taylor sum at 0.48 enters proofs that compare exp(0.48) against phi to obtain log(phi) > 0.48, which anchors later alpha seed inequalities such as alpha_seed = 4 pi * 11 < 138.230092. The same rational Taylor polynomial is defined upstream in the Log module to support monotonicity arguments for the logarithm.
proof idea
Direct definition that substitutes the rational x = 48/100 into the truncated exponential series and evaluates the nine power terms with exact rational arithmetic.
why it matters
The value feeds the lemmas exp_048_lt and exp_048_taylor_ceiling that produce strict upper bounds on exp(0.48), which in turn discharge log_phi_gt_048. In the Recognition framework this numerical anchor supports the phi-ladder comparisons required for the eight-tick octave and the derivation of D = 3. It closes a concrete gap in the interval arithmetic pipeline for alpha inverse bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.