exp_taylor_10_at_081416924
plain-language theorem explainer
This definition computes a rational number as the 10-term Taylor polynomial for exp at the point 0.81416924. It is referenced by lemmas that convert the approximation into strict upper bounds on the real exponential for lepton mass calculations. The construction is a direct substitution of the rational argument into the partial sum with factorial denominators.
Claim. Let $x = 81416924/100000000$. Define the truncated sum $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
The Necessity module derives muon and tau masses from the electron structural mass (T9) together with step functions from cube geometry, the fine-structure constant, and the golden ratio. This auxiliary definition supplies a rational proxy for the exponential that appears when converting geometric constants into mass ratios on the phi-ladder. The module imports AlphaDerivation, PhiSupport, and GapProperties to ground the constants E_passive = 11, faces = 6, and W = 17.
proof idea
The definition is a direct term-mode construction: bind the rational argument x = 81416924/100000000 and return the explicit sum of the first ten Taylor terms with their factorial denominators.
why it matters
It supplies the concrete rational value used by the downstream lemmas exp_081416924_upper and exp_081416924_upper_q to bound Real.exp(0.81416924). Those bounds close the replacement of axioms by proven inequalities for the lepton ladder, completing the necessity argument that runs from T0-T9 through the eight-tick octave and cube-derived constants. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.