exp_v2_1_q
plain-language theorem explainer
The lemma establishes that the Taylor sum to order 9 plus the given remainder term for exp at x=0.6327 is strictly less than 1.8827. Physicists closing the lepton mass predictions in Recognition Science cite this bound when converting the electron structural mass into forced muon and tau values via cube geometry. The proof is a one-line native_decide that evaluates the rational inequality directly.
Claim. Let $x = 6327/10000$. Then the partial sum $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! + x^{10}·11/(10!·10) < 1.8827$.
background
Module T10 proves the lepton ladder is forced from the electron mass (T9) together with E_passive=11, cube faces=6, wallpaper groups W=17, and α. The two upstream definitions supply the concrete numerical ingredients: exp_taylor_v2_1 is the degree-9 Taylor polynomial at x=6327/10000, while exp_error_v2_1 is the explicit remainder x^{10}·11/(10!·10). These replace earlier axioms with proven inequalities for the muon and tau mass bounds.
proof idea
One-line wrapper that applies native_decide to the rational arithmetic of the sum and the target inequality.
why it matters
The result feeds exp_06327_upper, which converts the bound into Real.exp(0.6327) < 1.8827 and thereby closes the numerical step in T10. It supplies the concrete control on the exponential that links the eight-tick octave and phi-ladder constants to the forced lepton generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.