exp_06316_lower
plain-language theorem explainer
The lemma certifies the strict inequality 1.8806 < exp(0.6316) as a numerical certificate inside the lepton mass bounds. Physicists deriving forced muon and tau masses from the Recognition Science ladder would invoke it when replacing the original axioms with explicit inequalities. The tactic proof combines Mathlib's exp_bound for |x|<=1 at order 10 with precomputed Taylor and remainder rationals, then chains the rational comparison via linarith.
Claim. $1.8806 < e^{0.6316}$
background
Module T10 proves the lepton ladder forced from the electron mass (T9) together with cube-derived steps E_passive=11, faces=6, W=17, alpha, pi and phi. This lemma supplies one concrete exponential lower bound used to close the muon and tau mass inequalities. Upstream results supply the order-10 Taylor polynomial exp_taylor_v2_2, the corresponding remainder exp_error_v2_2, and the rational comparison exp_v2_2_q proved by native_decide; Real.exp_bound from Mathlib supplies the approximation guarantee for |x|<=1.
proof idea
The tactic first obtains |0.6316|<=1 and calls Real.exp_bound n=10. It then rewrites the partial sum and remainder exactly to the sibling definitions exp_taylor_v2_2 and exp_error_v2_2. The pre-proved exp_v2_2_q gives 1.8806 + error < taylor; linarith and a final calc chain convert this into 1.8806 < taylor - error <= exp(0.6316).
why it matters
The lemma is an intermediate numerical certificate inside the T10 necessity argument that replaces two lepton-mass axioms with derived bounds. It is invoked by the companion lemma exp_46316_lower that handles the larger exponent for the tau. In the Recognition framework it supplies one explicit link between the eight-tick octave geometry and the observed lepton mass ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.