exp_v2_4_q
plain-language theorem explainer
Physicists deriving bounds on muon and tau masses cite this lemma to confirm that 2.2463 plus the tenth-order remainder term lies strictly below the ninth-degree Taylor sum for exp at 0.8093. It forms part of the numerical verification chain inside the lepton generations necessity module. The proof reduces to a single native_decide tactic that evaluates the two rational expressions directly.
Claim. Let $x = 8093/10000$. Then $22463/10000 + x^{10}·11/(10!·10) < 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 Necessity module proves that the muon and tau masses are forced from the electron structural mass (T9) together with geometric constants: E_passive = 11, cube faces = 6, W = 17, α, and π, all derived from the eight-tick structure and φ. The parameter 0.8093 enters mass-ratio calculations that combine these constants on the φ-ladder. Upstream, exp_taylor_v2_4 supplies the partial sum of the exponential series through degree 9 at x = 8093/10000, while exp_error_v2_4 supplies the explicit remainder bound x^10·11/(10!·10).
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compare the two rational numbers 22463/10000 + exp_error_v2_4 and exp_taylor_v2_4.
why it matters
The lemma supplies the rational comparison required by exp_08093_lower, which in turn establishes the strict real inequality 2.2463 < exp(0.8093). This numerical step closes a gap in the T10 necessity argument that the lepton ladder is forced once the electron mass and the cube-derived constants (α, π, E_passive, W) are in place. It therefore supports replacement of the original axioms in LeptonGenerations.lean with proven bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.