exp_error_10_at_062924882
plain-language theorem explainer
This definition supplies the rational truncation error for the degree-10 Taylor series of exp at the point 0.62924882, scaled by the factor 11/(10! * 10). It is cited by the two bounding lemmas that convert the series into strict real inequalities used for lepton mass predictions. The definition is a direct arithmetic expression with no lemmas or tactics.
Claim. Let $x = 62924882/100000000$. Define the error term $e_{10}(x) := x^{10} · 11 / (10! · 10)$.
background
The module establishes that the muon and tau masses are forced once the electron mass (T9) and the geometric constants from cube geometry are fixed. The exponential arises in the mass-ladder formula that combines the golden-ratio step with the passive-edge count E_passive = 11. This definition supplies a concrete rational upper bound on the remainder after ten terms of the Taylor series for exp(0.62924882), allowing the subsequent lemmas to replace floating-point checks with exact rational comparisons.
proof idea
Direct definition: substitute the rational x := 62924882/100000000 into the scaled monomial x^10 * 11 / (Nat.factorial 10 * 10). No upstream lemmas are invoked; the expression is evaluated entirely inside the rationals.
why it matters
The definition is invoked by exp_062924882_lower and exp_062924882_lower_q, which close the numerical gap in the lepton-ladder bounds. It therefore participates in the replacement of the two original axioms by derived inequalities, completing one concrete step of the T10 necessity argument that the lepton rungs are fixed by the eight-tick structure and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.