exp_error_10_at_7144
plain-language theorem explainer
This definition supplies the rational error bound for the 10-term Taylor expansion of exp at x = 0.7144. It is referenced by the upper bound lemmas that close numerical gaps in the electron mass necessity proof. The definition is a direct algebraic expression that encodes the standard remainder estimate as an exact rational for native_decide comparison.
Claim. Let $x = 7144/10000$. The error bound is given by $x^{10} · 11 / (10! · 10)$.
background
The module proves that the electron mass formula is forced from T8 ledger quantization and the geometric constants derived in earlier theorems. This definition provides a precise rational error term for bounding the real exponential at the specific point 0.7144 that arises in the alpha and gap calculations. The local setting requires exact rational comparisons to verify inequalities without floating-point error in the necessity argument.
proof idea
The definition is a direct algebraic expression: set x to 7144/10000, raise to the 10th power, multiply by 11, and divide by the product of 10 factorial and 10. No lemmas or tactics are invoked; the body is a pure rational formula implementing the Lagrange remainder estimate for the exponential series.
why it matters
It supplies the error term that feeds into the lemmas exp_07144_upper and exp_07144_upper_q, which establish exp(0.7144) < 2.042961. These bounds are required to confirm the electron mass formula under T9. The definition closes a numerical verification step in the forcing chain from T8 to the mass formula, using constants from AlphaDerivation and PhiBounds modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.