exp_taylor_10_at_0481
plain-language theorem explainer
A rational partial sum for the exponential Taylor series at 481/1000 up to the ninth power term. Numerics code in the Recognition Science interval layer cites it to obtain a concrete upper bound on exp(0.481) that is compared against a rational lower bound for the golden ratio. The definition is an explicit finite sum of rational monomials with no lemmas or tactics invoked.
Claim. Let $x = 481/1000$. Define the rational $s = 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 Log module supplies interval arithmetic for the natural logarithm to obtain rigorous comparisons involving the golden ratio. It relies on monotonicity of log together with Taylor error estimates for log(1+x) when |x|<1, but invokes the exponential series in the opposite direction to bound log(φ) from below. The upstream definition in AlphaBounds supplies an identical rational expression for the same partial sum at the same point.
proof idea
The definition is a direct term-mode construction: fix the rational x = 481/1000 and add the nine successive Taylor monomials with their factorial denominators expressed as rationals. No lemmas are applied and no tactics are used.
why it matters
The partial sum is added to an error term in AlphaBounds to produce the strict inequality exp(0.481) < 1.6177, which is then used by log_phi_gt_0481 to prove log(φ) > 0.481. That theorem supplies a concrete numerical anchor for the phi-ladder and the self-similar fixed point (T6) inside the eight-tick octave (T7). It closes one step in the chain that ultimately forces D = 3 and places alpha inverse inside (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.