exp_0481_taylor_ceiling
plain-language theorem explainer
The lemma establishes a strict rational upper bound of 1.6177 on the sum of the degree-9 Taylor polynomial for exp at 0.481 together with its remainder estimate. Workers tightening numerical intervals for the inverse fine-structure constant cite this result when assembling the alpha bounds. The proof consists of a single native_decide invocation that confirms the inequality by exhaustive rational arithmetic.
Claim. Let $x = 481/1000$. Then $1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880 + 11 x^{10}/(10! · 10) < 16177/10000$.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant using the symbolic derivation from Recognition Science. Two supporting definitions supply the ingredients: exp_taylor_10_at_0481 evaluates the partial sum 1 + x + x²/2 + ⋯ + x⁹/9! at x = 481/1000, while exp_error_10_at_0481 supplies the explicit remainder x¹⁰ · 11 / (10! · 10). The same pair of definitions appears in the Log module, where the accompanying remark states that the construction yields exp(0.481) < φ via the Taylor bound combined with a lower bound on φ.
proof idea
The proof is a one-line wrapper that applies native_decide to the rational comparison between the pre-defined Taylor sum plus error term and the target fraction 16177/10000.
why it matters
The lemma is used by exp_0481_lt to obtain the corresponding real-number bound Real.exp(0.481) < 1.6177. This step belongs to the pipeline that produces the reported interval for alpha inverse inside (137.030, 137.039). It thereby supports the Recognition Science claim that the fine-structure constant lies inside the eight-tick octave predicted by the T7 and T8 steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.