exp_error_10_at_048
plain-language theorem explainer
The declaration defines the rational error term for the 10-term Taylor truncation of exp at argument 0.48. Numerics researchers bounding alphaInv or verifying phi-ladder inequalities cite it when closing interval enclosures. The definition follows the standard Lagrange remainder estimate, replacing the exp(|x|) factor by the constant 11/10 for x = 0.48.
Claim. The truncation error bound for the Taylor series of $e^{0.48}$ after 10 terms is $0.48^{10} · 11 / (10! · 10)$.
background
The module supplies rigorous interval bounds on alphaInv derived from the Recognition Science symbolic derivation. The definition computes a concrete rational upper bound on the remainder of the exponential Taylor series at x = 0.48. The upstream result in the Log module records the identical expression and uses it to compare exp(0.48) against the golden ratio phi.
proof idea
The definition is a direct encoding of the Lagrange remainder formula specialized to n = 10 and x = 0.48, with the exponential growth factor replaced by the constant 11/10. It is a one-line wrapper that supplies the rational error term consumed by the ceiling and comparison lemmas in the same module.
why it matters
The bound is consumed by exp_048_taylor_ceiling and exp_048_lt, which together establish the comparison exp(0.48) < 1.6161. Those lemmas support log_phi_gt_048, confirming log(phi) > 0.48. This step anchors the phi-ladder numerics used for the predicted alpha^{-1} interval (137.030, 137.039) inside the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.