exp_181416924_upper
plain-language theorem explainer
This lemma supplies an upper bound showing that the real exponential of 1.81416924 is strictly less than 6.1385. It is cited in derivations of forced muon and tau masses once the electron mass and golden-ratio logarithms are fixed. The tactic proof splits the argument additively, multiplies independent exponential bounds, and chains the product inequality via transitivity.
Claim. $e^{1.81416924} < 6.1385$
background
The LeptonGenerations.Necessity module replaces two axioms on muon and tau mass predictions with derived inequalities that follow from the electron structural mass (T9), cube-face counts, wallpaper groups, and the golden ratio φ fixed at T6. Exponential bounds appear when logarithmic comparisons to φ are converted back to multiplicative mass ratios on the phi-ladder. The present lemma depends on order transitivity from ArithmeticFromLogic and on the companion bound for the fractional part 0.81416924.
proof idea
The argument is decomposed as 1 + 0.81416924 by norm_num and Real.exp_add. The integer part is bounded by Real.exp_one_lt_d9 while the fractional part invokes the sibling lemma exp_081416924_upper. The product of the two upper bounds is formed by nlinarith (using positivity of both exponentials), norm_num shows that product lies below 6.1385, and lt_trans completes the chain.
why it matters
The bound is invoked inside phi_pow_neg377_lower_proved to control the logarithm of φ raised to a negative power that appears in lepton-rung calculations. It therefore participates in the T10 program that eliminates the original lepton axioms by deriving all masses from the eight-tick octave, cube geometry, and the Recognition Composition Law. No further scaffolding is required for this numerical step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.