exp_taylor_10_at_062924882
plain-language theorem explainer
This definition supplies the tenth-order Taylor polynomial for exp evaluated at the rational 0.62924882. It is invoked by the two bounding lemmas that sandwich the real exponential inside the lepton-mass necessity proofs. The body is a direct inline expansion of the series with factorial denominators, yielding a single rational value.
Claim. Let $x = 62924882/100000000$. Define the partial sum $s_{10}(x) := 1 + x + x^2/2! + x^3/3! + x^4/4! + x^5/5! + x^6/6! + x^7/7! + x^8/8! + x^9/9!$.
background
The definition sits inside the module that replaces the two lepton-mass axioms with derived bounds, completing the T10 necessity argument that the muon and tau masses are forced once the electron mass (T9) and the geometric constants are fixed. The surrounding development uses the cube-derived quantities E_passive = 11, six faces, W = 17 wallpaper groups, and the fine-structure constant α together with the golden-ratio ladder to fix the rung spacings.
proof idea
One-line wrapper that substitutes the target rational for x and writes out the nine powered terms scaled by the reciprocal factorials; no external lemmas are called.
why it matters
It supplies the concrete rational anchor required by exp_062924882_lower and exp_062924882_lower_q, which close the numerical gap in the muon and tau mass bounds. Those lemmas feed the main T10 necessity theorems that convert the geometric forcing chain (T0–T8) into explicit mass predictions inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.