exp_error_10_at_7145
plain-language theorem explainer
This definition supplies the rational error bound for the 10-term Taylor expansion of exp at 0.7145. Researchers proving the forced electron mass under T9 cite it to close numerical gaps in lower bounds for exp(0.7145). The definition directly encodes the remainder estimate with x set to 7145/10000 and the factor 11/(10! * 10).
Claim. Let $x = 7145/10000$. The error bound is the rational $x^{10} * 11 / (10! * 10)$.
background
The module proves T9 necessity: the electron mass formula is forced from T8 ledger quantization and geometric constants. This definition belongs to a family of numerical Taylor bounds (alongside similar ones at 481211 and 481212) that support interval arithmetic for exp and log. It relies on the general exp_bound lemma imported from Mathlib to convert the rational error into a concrete lower bound on Real.exp(0.7145).
proof idea
One-line definition. It binds x to the rational 7145/10000 then returns the explicit remainder expression x^10 * 11 / (Nat.factorial 10 * 10).
why it matters
It is used directly by the lemmas exp_07145_lower and exp_07145_lower_q that establish 2.0431648 < Real.exp(0.7145). These bounds feed the electron-mass necessity argument in T9, closing the numerical step between the phi-ladder mass formula and the observed electron mass. The definition therefore anchors the final link from T8 quantization to the concrete mass value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.