exp_18104_upper
plain-language theorem explainer
This lemma establishes the strict inequality exp(1.8104) < 6.114. It is invoked inside the lepton-generation necessity proofs to close a numerical step in the lower bound for a negative power of the golden ratio. The proof factors the argument as 1 + 0.8104, applies separate exponential bounds, multiplies them, and chains the resulting inequalities.
Claim. $e^{1.8104} < 6.114$
background
The module proves that the muon and tau masses are forced once the electron mass (T9) and the geometric constants (cube edges, faces, wallpaper groups, α, π) are fixed. Numerical exponential bounds appear because the mass formula involves powers of φ combined with logarithmic comparisons. The lemma depends on the sibling bound exp_08104_upper for the fractional part and on lt_trans from the arithmetic foundation for chaining strict inequalities.
proof idea
The proof rewrites 1.8104 as 1 + 0.8104 via exp_add, invokes Real.exp_one_lt_d9 on the integer part and exp_08104_upper on the fractional part, obtains the product inequality by nlinarith, compares the explicit numerical product to 6.114 by norm_num, and finishes with lt_trans.
why it matters
The bound feeds directly into phi_pow_neg3762_lower_v2, which supplies a key inequality for the forced lepton rungs in T10. It closes a concrete numerical gap in the necessity argument that replaces the original axioms for muon and tau masses, consistent with the φ-ladder and eight-tick structure already derived in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.