exp_v2_3_q
plain-language theorem explainer
The lemma supplies a rational upper bound showing that the ninth-order Taylor sum for exp at 0.8104 plus a scaled remainder term stays strictly below 2.2489. Researchers deriving forced muon and tau masses under T10 necessity would cite it when converting the exponential factor in the lepton ladder into concrete inequalities. The verification is performed by direct evaluation of the two rational expressions via the native_decide tactic.
Claim. Let $x = 8104/10000$. Let $T_9(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$ and let $E(x) = x^{10} · 11 / (10! · 10)$. Then $T_9(x) + E(x) < 2.2489$.
background
The module proves T10 necessity: the muon and tau masses are forced once the electron mass (T9) and the geometric constants from cube geometry, wallpaper groups, and α are fixed. The exponential factor at argument 0.8104 encodes a combination of these constants in the mass-scaling formula on the phi-ladder. Upstream, exp_taylor_v2_3 is defined as the explicit partial sum of the exponential series through the ninth power at x = 8104/10000, while exp_error_v2_3 supplies the concrete rational bound on the next term scaled by 11/10.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic on the inequality between the two explicitly defined rational numbers exp_taylor_v2_3 and exp_error_v2_3.
why it matters
The bound is used by exp_08104_upper to obtain Real.exp(0.8104) < 2.2489, which feeds directly into the muon_mass_pred_bounds and tau_mass_pred_bounds that replace the earlier axioms in the lepton ladder. It therefore closes a numerical step in the T10 forcing chain that runs from the eight-tick octave and phi-ladder through the cube-derived constants to the observed lepton spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.