exp_062924882_lower_q
plain-language theorem explainer
The lemma confirms that 1.87620 plus a controlled remainder is strictly less than the 10-term Taylor sum for exp at 0.62924882. Lepton mass derivations in Recognition Science rely on this to bound the predicted muon mass from the electron mass and phi-ladder steps. The proof is a direct native_decide call that checks the rational inequality after unfolding the Taylor and error definitions.
Claim. $1.87620 + x^{10}·11/(10!·10) < 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$ where $x = 0.62924882$.
background
The module proves T10: the lepton ladder is forced from the electron mass (T9) and geometric constants from cube geometry (E_passive = 11, six faces, W = 17) together with alpha and phi. The upstream definitions supply the partial sum of the exponential series up to order 9 and the explicit remainder term x^10 · 11 / (10! · 10) evaluated at the fixed point x = 0.62924882 that encodes the mass step to the muon rung.
proof idea
One-line wrapper that applies native_decide to the inequality after the definitions of exp_taylor_10_at_062924882 and exp_error_10_at_062924882 are substituted.
why it matters
It supplies the rational comparison used by the downstream lemma exp_062924882_lower to obtain the real-number bound 1.87620 < exp(0.62924882). This closes one numerical step in the T10 proof that the muon and tau masses are determined by the phi-ladder and the eight-tick structure without additional assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.