exp_062924882_lower
plain-language theorem explainer
The lemma proves that exp(0.62924882) exceeds 1.87620. Researchers deriving forced muon and tau masses from the electron structural mass in Recognition Science cite this numerical anchor when replacing axiomatic bounds with derived inequalities. The proof applies the order-10 Taylor remainder estimate for the exponential, equates the partial sum and error to precomputed rationals, and chains the inequalities via linarith and calc.
Claim. $1.87620 < e^{0.62924882}$
background
The Necessity module for lepton generations proves that the muon and tau masses are forced from the electron mass (T9) together with cube geometry constants E_passive = 11, faces = 6, W = 17, the fine-structure constant α, and the golden ratio φ. This lemma supplies a concrete lower bound on an exponential factor that appears inside the mass step functions of the phi-ladder. It depends on the module-local definitions exp_taylor_10_at_062924882 (the truncated series sum) and exp_error_10_at_062924882 (the explicit remainder term), plus the general bound h_lower from Numerics.Interval.Trig.
proof idea
The proof invokes Real.exp_bound at n=10 to obtain an absolute error interval between exp(x) and its Taylor polynomial. It equates the Taylor sum to exp_taylor_10_at_062924882 and the error expression to exp_error_10_at_062924882 by simp and norm_num. The rational inequality from exp_062924882_lower_q is cast to reals, after which linarith shows that 1.87620 plus the error lies below the Taylor sum. A final calc chain combines this with the remainder bound to conclude the desired strict inequality.
why it matters
The result is invoked by the downstream lemma exp_462924882_lower, which in turn supports the muon mass prediction bounds required for the T10 necessity theorem. It therefore contributes to replacing the two axioms in LeptonGenerations.lean with proven inequalities derived from the eight-tick octave and cube geometry. The numerical verification anchors the phi-ladder mass formula without introducing external constants beyond those already forced by the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.