exp_taylor_10_at_0483
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!.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not supply the Taylor remainder term or prove that the partial sum lies below exp(x).
- Does not extend to other evaluation points or to higher truncation orders.
- Does not invoke or depend on the Recognition Composition Law or J-cost function.
- Does not address complex logarithms or interval arithmetic operations beyond the single-point evaluation.
formal statement (Lean)
262private def exp_taylor_10_at_0483 : ℚ :=
proof body
Definition body.
263 let x : ℚ := 483 / 1000
264 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
265
266/-- Error bound for Taylor at x = 483/1000 -/