exp_taylor_10_at_063407156
plain-language theorem explainer
This definition supplies a 10-term Taylor polynomial in rationals for the exponential function evaluated at 0.63407156. It is cited by the upper bounding lemmas for that exponential inside the lepton generations necessity module. The definition is a direct term-mode expansion of the series without external lemmas.
Claim. Let $x = 63407156/100000000$. The value is $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
The module on T10 necessity proves the lepton ladder is forced from the electron mass (T9) together with cube geometry constants and the golden ratio. This supplies the rational Taylor approximant used to bound the exponential term that appears in the mass ratio calculations. Upstream results on alpha derivation and phi support fix the numerical inputs that determine the exponent 0.63407156.
proof idea
This is a direct definition that computes the 10-term Taylor sum for exp at the specific rational x = 63407156/100000000. It uses a let-binding for the argument and explicit addition of the factorial-denominated powers up to degree 9.
why it matters
It supports the upper bound lemmas that close the inequalities for predicted muon and tau masses. This advances the T10 step by providing concrete numerical bounds derived from the eight-tick octave and recognition composition law. It touches the question of tightening these bounds to exact equalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.