exp_error_10_at_0483
plain-language theorem explainer
This definition supplies the explicit rational error term for the tenth-order Taylor remainder of exp at argument 0.483. Researchers verifying phi < exp(0.483) cite it to obtain the strict inequality log(phi) < 0.483. The definition is a direct arithmetic expression that sets x to 483/1000 and evaluates x^10 * 11 / (10! * 10).
Claim. Let $x = 0.483$. The Taylor remainder bound for the exponential is given by $x^{10} · 11 / (10! · 10)$.
background
The Numerics.Interval.AlphaBounds module supplies rigorous interval bounds on the inverse fine-structure constant via symbolic derivations. This definition provides the explicit error term for the Taylor expansion of exp at 0.483, matching the upstream definition in the Log module whose doc-comment states 'Error bound for Taylor at x = 483/1000'. The bound is constructed to support direct numerical comparison with the golden ratio in the subsequent proof that log(phi) < 0.483.
proof idea
The definition is a one-line wrapper. It binds x to the rational 483/1000 and returns the expression x^10 * 11 / (Nat.factorial 10 * 10). No lemmas or tactics are invoked.
why it matters
The value feeds the lemmas exp_0483_taylor_floor and exp_0483_gt in the same module and the theorem log_phi_lt_0483 in the Log module, which together establish phi < exp(0.483) and therefore log(goldenRatio) < 0.483. This step supports the interval estimates for alpha inverse that rely on the self-similar fixed point phi in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.