exp_four_upper
plain-language theorem explainer
The inequality exp(4) < 54.598151 supplies a numeric upper bound on the exponential that appears when splitting composite exponents in lepton mass formulas. Researchers proving forced muon and tau masses from the electron structural mass and cube-derived constants would cite it to justify the splitting step in T10 derivations. The proof reduces exp(4) to a fourth power via the natural multiplication identity, applies a monotonicity bound on the base, and chains it to a direct numerical comparison.
Claim. $e^{4} < 54.598151$
background
The module proves T10 necessity: the muon and tau masses are forced from the electron structural mass (T9) together with the geometric constants E_p = 11 (passive cube edges), F = 6 (cube faces), W = 17 (wallpaper groups), and the fine-structure constant α. This lemma is a supporting numeric bound used when composite exponents such as 4.6327 are decomposed as 4 + 0.6327 in the mass-prediction inequalities. It sits inside the same file as the main lepton-ladder theorems and depends on the order relation le defined on LogicNat in ArithmeticFromLogic.
proof idea
The tactic proof first obtains (exp(1))^4 ≤ (2.7182818286)^4 by applying pow_le_pow_left₀ to the known bound Real.exp_one_lt_d9. It then confirms (2.7182818286)^4 < 54.598151 by norm_num. A short calc block rewrites exp(4) as (exp(1))^4 using exp_nat_mul, after which lt_of_le_of_lt chains the two inequalities.
why it matters
The lemma is invoked directly inside exp_46327_upper and exp_463407156_upper, which themselves feed the main T10 statement that the lepton ladder is completely determined by the electron mass, E_p=11, F=6, W=17 and α. It therefore closes a concrete numeric seam required to replace the original axioms in LeptonGenerations.lean with proven inequalities, completing the necessity claim that begins from the eight-tick octave and golden-ratio fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.