exp_081416924_upper_q
plain-language theorem explainer
The lemma establishes a strict rational upper bound on the 10th-order Taylor sum for exp at x = 0.81416924 together with its remainder estimate. Researchers verifying numerical steps in the lepton mass ladder would cite it when confirming bounds needed for muon and tau predictions from T9. The proof is a one-line wrapper that invokes native_decide to confirm the inequality by direct rational evaluation.
Claim. Let $x = 81416924/100000000$. Then the partial sum $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$ plus the remainder term $x^{10}·11/(10!·10)$ satisfies $x^{10}·11/(10!·10) +$ partial sum $< 225731/100000$.
background
In the T10 Necessity module the lepton ladder is forced from the electron mass (T9) together with geometric constants E_passive = 11, cube faces = 6, wallpaper count W = 17, and the fine-structure constant α. The present inequality supplies a machine-checkable bound on the exponential that appears when converting those constants into mass ratios on the phi-ladder.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the rational comparison of the two upstream definitions (the explicit Taylor sum up to degree 9 and the remainder x^10·11/(10!·10)) against the target fraction 225731/100000.
why it matters
The lemma is invoked by exp_081416924_upper to obtain Real.exp(0.81416924) < 2.25731, which closes a numerical step in the necessity argument that the muon and tau masses are forced by the eight-tick octave, phi, and cube geometry. It removes an axiom from the earlier LeptonGenerations file without adding hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.