exp_taylor_v2_3
plain-language theorem explainer
The definition supplies the rational value of the ninth-order Taylor polynomial for exp at argument 8104/10000. Researchers closing numerical bounds on predicted muon and tau masses within the lepton ladder cite this truncation to control the real exponential. It is assembled by explicit term-by-term summation of the series coefficients over the rationals.
Claim. Let $x = 8104/10000$. Define the rational $s = 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$.
background
Module T10 proves that the muon and tau masses are forced from the electron mass (T9) together with step functions built from cube geometry, the golden ratio from T4, and constants such as E_passive = 11, faces = 6, W = 17, and α. The lepton ladder is assembled from the electron structural mass, these geometric steps, and φ. This definition supplies a concrete rational proxy for the exponential that enters the mass-ratio bounds.
proof idea
The body directly enumerates the first ten terms of the exponential Taylor series at the fixed rational x = 8104/10000 and returns their sum as a single element of ℚ.
why it matters
It supports the bounding lemmas exp_08104_upper and exp_v2_3_q that establish Real.exp(0.8104) < 2.2489, which close the inequalities required for the lepton-mass predictions in T10. The value 0.8104 arises from the combination of cube-derived constants and the eight-tick structure already forced upstream. It is a numerical scaffolding step with no open question attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.