exp_four_lower
plain-language theorem explainer
54.598150 is strictly less than exp(4) in the reals and anchors lower bounds when splitting composite exponentials for lepton mass predictions. Workers deriving the forced muon and tau masses under T10 cite this numerical fact to chain inequalities without new axioms. The proof compares a decimal power of 2.7182818283 against exp(1) to the fourth, equates the target via exp_nat_mul, and closes with lt_trans.
Claim. $54.598150 < e^{4}$ in the real numbers.
background
The Necessity module for lepton generations replaces two axioms with proven bounds on muon and tau masses. These bounds are built from the electron structural mass (T9), cube-derived steps (E_passive = 11, faces = 6, W = 17), the fine-structure constant, pi, and the golden ratio phi from the eight-tick octave. The lemma supplies a concrete lower bound on exp(4) that permits decomposition of the larger exponents appearing in the muon and tau predictions.
proof idea
The tactic proof first invokes pow_lt_pow_left₀ to obtain (2.7182818283)^4 < exp(1)^4 from the known decimal lower bound on exp(1). A norm_num step confirms 54.598150 lies below that power. The equality exp(4) = exp(1)^4 follows from rewriting the multiplier and applying exp_nat_mul. The two strict inequalities are chained by lt_trans from ArithmeticFromLogic.
why it matters
The lemma is invoked directly by exp_462924882_lower and exp_46316_lower, which themselves feed the muon and tau mass bound theorems. It closes a numerical prerequisite inside the T10 necessity argument that forces the lepton ladder from the phi-ladder and eight-tick structure, without adding hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.