exp_081416924_upper
plain-language theorem explainer
The lemma establishes that exp(0.81416924) is strictly less than 2.25731, supplying a verified numerical bound for the lepton mass step functions. Physicists deriving forced muon and tau masses from the electron mass and cube geometry cite it to close the T10 inequalities without external axioms. The proof applies the Taylor remainder estimate at order 10, equates the partial sum and error to precomputed rationals, and reduces the comparison to a native decidable fact.
Claim. $e^{0.81416924} < 2.25731$
background
The module proves T10 necessity: the muon and tau masses are forced from the electron structural mass (T9) together with geometric constants E_passive = 11, cube faces = 6, wallpaper groups W = 17, alpha, and pi. The lepton ladder steps combine these quantities with the golden ratio phi on the phi-ladder mass formula. This lemma supplies one concrete exponential bound required to replace the two axioms in LeptonGenerations.lean with derived inequalities for the predicted masses.
proof idea
The tactic proof first confirms the argument lies in [0,1] by norm_num. It invokes Real.exp_bound' with n=10 to obtain the Taylor-plus-remainder inequality. It then equates the 10-term sum to exp_taylor_10_at_081416924 and the remainder term to exp_error_10_at_081416924 via simp and norm_num. The sum of these rationals is shown less than 225731/100000 by exact_mod_cast from the sibling lemma exp_081416924_upper_q, after which norm_num yields the target decimal bound.
why it matters
This bound is used directly by exp_181416924_upper, which splits the larger exponential at 1.81416924 to support the tau mass prediction. It therefore contributes to the overall lepton_rungs_forced result that discharges the axiomatic mass steps in favor of quantities derived from the eight-tick octave, RCL, and cube geometry. The lemma closes a numerical gap in the T10 strategy without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.