exp_taylor_10_at_080454125
plain-language theorem explainer
This definition supplies the exact rational value of the truncated Taylor series for the exponential at argument 0.80454125. Researchers establishing strict numerical bounds on lepton mass predictions in the T10 necessity argument would invoke it to anchor lower estimates for Real.exp. The construction proceeds by direct substitution of the rational x into the sum of the first ten power terms.
Claim. Let $x = 80454125/100000000$. Define the rational number $s_{10}(x) := 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 T10 Necessity proves that the muon and tau masses are forced once the electron structural mass (T9) and the geometric constants are fixed. The lepton ladder is assembled from step functions built on E_passive = 11, cube faces = 6, wallpaper count W = 17, the fine-structure constant α, and π arising from spherical geometry. All of these quantities trace back to the eight-tick octave and the cube geometry already derived upstream.
proof idea
The definition is a direct one-line construction: it binds the rational x to 80454125/100000000 and writes the explicit sum of the first ten Taylor terms with the corresponding factorial denominators.
why it matters
The definition is the exact rational anchor used by the two downstream lemmas exp_080454125_lower and exp_080454125_lower_q. Those lemmas convert the rational sum into a strict lower bound on Real.exp(0.80454125), which in turn supplies the numerical inequalities required to close the forced-ladder argument for the muon and tau. It therefore participates in the T10 step that replaces the original axioms with proven bounds inside the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.