exp_error_10_at_0483
plain-language theorem explainer
This definition supplies the explicit rational Lagrange remainder for the 10-term Taylor series of exp at argument 0.483. Numerics routines in the logarithm interval module cite it to certify that the golden ratio lies below exp(0.483). The body is a direct one-line formula x^10 * 11 / (10! * 10) with x = 483/1000.
Claim. Let $x = 0.483$. The Lagrange remainder bound after ten terms for the Taylor series of the exponential is $x^{10} · 11 / (10! · 10)$.
background
The Numerics.Interval.Log module develops rigorous interval enclosures for the natural logarithm by combining monotonicity with Taylor expansions of log(1+x) for |x|<1. For the golden ratio the argument x = φ - 1 ≈ 0.618 is used, but the present definition supplies the companion exponential error term needed to invert the inequality via exp monotonicity. Upstream, the MassToLight.via structure encodes recognition-weighted stellar assembly while the sibling definition in AlphaBounds provides an identical numerical expression for the same bound.
proof idea
This is a one-line definition that directly encodes the standard Lagrange remainder estimate for the exponential Taylor series truncated after ten terms at x = 0.483. It evaluates the rational expression without invoking any further lemmas.
why it matters
The bound is invoked by log_phi_lt_0483 to certify log(φ) < 0.483, which closes the numerical verification that the self-similar fixed point phi satisfies the required inequality for the eight-tick octave in the forcing chain. It supports the phi-ladder mass formula by furnishing a concrete numerical anchor inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.