exp_08093_lower
plain-language theorem explainer
A strict lower bound establishes that the exponential at 0.8093 exceeds 2.2463. Researchers deriving numerical inequalities for muon and tau masses in the lepton ladder would cite it when closing T10 necessity bounds. The proof applies a Taylor expansion of order 10 with remainder estimate, equates the sum and error to precomputed rational values, and chains a rational comparison through linarith.
Claim. $2.2463 < e^{0.8093}$ holds.
background
The module proves that the muon and tau masses are forced from the electron structural mass (T9) together with cube-derived constants E_passive = 11, faces = 6, W = 17, the fine-structure constant, and the golden ratio. This lemma supplies one concrete exponential lower bound used inside composite estimates for those mass predictions. Upstream, the Taylor polynomial exp_taylor_v2_4 and remainder exp_error_v2_4 are defined at the same argument 0.8093, while exp_v2_4_q supplies the rational inequality that drives the final comparison. The surrounding 8-tick phase structure and successor operation from arithmetic foundations anchor the overall forcing chain.
proof idea
The tactic proof first checks the absolute-value hypothesis for the general exponential bound lemma at n = 10. It then equates the partial sum to the sibling Taylor definition and the remainder term to the sibling error definition via simp and norm_num. The rational comparison lemma exp_v2_4_q is cast to reals and fed to linarith to obtain the lower estimate. A final calc block chains the target constant below the Taylor-minus-error quantity and below the true exponential.
why it matters
The lemma feeds the composite bound exp_18093_lower, which itself supports the proven muon and tau mass inequalities that replace the original axioms in the lepton-generations file. It therefore closes numerical scaffolding inside the T10 necessity result that the lepton ladder is forced by the eight-tick octave and phi-ladder. No open questions remain for this specific bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.