exp_07144_upper_q
plain-language theorem explainer
This lemma supplies a rational upper bound on the 10-term Taylor sum plus remainder for exp at 0.7144. It is cited inside the parent bound that converts the rational estimate into a real-number inequality used for the electron-mass necessity argument. The proof is a one-line wrapper that invokes native_decide on the explicit rational expressions.
Claim. Let $x = 7144/10000$. Then the partial sum $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!$ plus the error term $x^{10}·11/(10!·10)$ is strictly less than $2.042961$.
background
The module proves that the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier. The two upstream definitions supply the explicit 10-term Taylor polynomial for exp at the rational point 7144/10000 and the corresponding Lagrange-style remainder bound scaled by 11/10. These rational objects are the only ingredients required to obtain a machine-checkable upper estimate before lifting to the reals.
proof idea
The proof is a one-line wrapper that applies native_decide to the inequality between the two explicitly defined rational numbers.
why it matters
The result is invoked by the lemma that establishes Real.exp(0.7144) < 2.042961, which in turn feeds the necessity argument for the electron mass under T9. It therefore closes one numerical step in the chain that derives particle masses from the phi-ladder and the eight-tick octave without external parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.