exp_error_10_at_048
plain-language theorem explainer
exp_error_10_at_048 supplies the explicit rational upper bound on the truncation error for the degree-9 Taylor polynomial of exp at 0.48. Numerics routines in AlphaBounds and Log cite it to certify exp(0.48) < 1.6161 and thereby obtain log(φ) > 0.48. The definition is a direct arithmetic expression that transcribes the standard Lagrange remainder estimate scaled by 11/10.
Claim. Let $x = 48/100$. The Taylor remainder bound after nine terms for $e^{0.48}$ is given by $x^{10} · 11 / (10! · 10)$.
background
The module develops interval arithmetic for the natural logarithm by exploiting monotonicity on (0, ∞) together with Taylor series for log(1 + x) when |x| < 1; the error after n terms is bounded by |x|^{n+1} / ((n+1)(1 - |x|)). The present definition supplies the companion rational error term for the exponential, which is required when inverting the inequality to bound φ from below. Upstream, the identical expression appears in AlphaBounds.exp_error_10_at_048; the structure via from MassToLight frames these constants inside recognition-weighted stellar assembly.
proof idea
The definition is a one-line arithmetic expression. It sets x := 48/100 and returns x^10 * 11 / (Nat.factorial 10 * 10). No external lemmas are applied; the expression directly implements the remainder estimate used by the downstream Taylor-ceiling lemmas.
why it matters
This definition is invoked by exp_048_lt_phi and log_phi_gt_048 to establish the rigorous inequality log(φ) > 0.48. That inequality tightens the phi-ladder constants appearing in the mass formula and supports the alpha inverse band inside (137.030, 137.039). It closes a numerical verification step inside the eight-tick octave derivations of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.