exp_048_taylor_ceiling
plain-language theorem explainer
The lemma certifies that the 10-term Taylor sum for exp at 0.48 plus its remainder bound stays strictly below 1.6161 over the rationals. Interval-arithmetic workers tightening bounds on the inverse fine-structure constant would cite this step to close the gap between polynomial and exponential. The proof is a one-line wrapper that invokes native_decide on the explicit rational comparison.
Claim. $T_9(0.48) + R_{10}(0.48) < 1.6161$, where $T_9(x) = 1 + x + x^2/2! + x^3/3! + x^4/4! + x^5/5! + x^6/6! + x^7/7! + x^8/8! + x^9/9!$ and $R_{10}(x) = x^{10}·11/(10!·10)$ at $x = 0.48$.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant using symbolic derivations from the Recognition framework. The two supporting definitions are the partial Taylor sum exp_taylor_10_at_048, which evaluates the sum up to the $x^9/9!$ term at $x = 0.48$, and the error term exp_error_10_at_048 given explicitly by $x^{10}·11/(10!·10)$ at the same point. Parallel definitions appear in the Log module to furnish the same rational expressions for exponential bounds.
proof idea
This is a one-line wrapper that applies native_decide to the rational inequality between the sum of the Taylor polynomial and error bound and the target fraction 16161/10000.
why it matters
It supplies the rational ceiling used by the downstream lemma exp_048_lt to obtain Real.exp(0.48) < 1.6161, which tightens the interval for alpha_seed = 4π·11. The step contributes to the module's verification of α^{-1} bounds inside the Recognition Science derivation of constants from the J-function and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.