exp_error_10_at_0481
plain-language theorem explainer
exp_error_10_at_0481 defines the explicit Lagrange remainder for the 10-term Taylor expansion of exp at x = 0.481. Interval proofs establishing log(phi) > 0.481 cite this value to bound truncation error before comparing to the golden-ratio lower bound. The definition is obtained by direct substitution of x = 481/1000 into the standard remainder formula x^n * (n+1) / (n! * n) with n = 10.
Claim. Let $x = 0.481$. The truncation error bound after ten terms of the Taylor series for exp is given by $x^{10} * 11 / (10! * 10)$.
background
The Numerics.Interval.AlphaBounds module supplies rigorous interval bounds on alpha inverse via symbolic derivations that invoke the golden ratio. The definition supplies the explicit remainder term needed to control the Taylor truncation when proving exp(0.481) < phi. The upstream Log module records the identical expression to support the monotonicity argument that log(phi) > 0.481.
proof idea
One-line definition that instantiates the Lagrange remainder formula at the concrete point x = 481/1000 with n = 10. It evaluates the expression x^10 * 11 / (Nat.factorial 10 * 10) directly in rational arithmetic.
why it matters
The definition is invoked by exp_0481_taylor_ceiling and exp_0481_lt_phi to close the comparison exp(0.481) < phi, which yields the theorem log_phi_gt_0481. That lower bound on log(phi) enters the alpha-inverse interval calculations and aligns with the Recognition Science constants where phi appears in the mass ladder and the alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.