exp_four_upper
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 in Recognition Science
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.
scope and limits
- Does not establish the exact decimal expansion of exp(4).
- Does not derive the bound from phi or cube geometry.
- Does not apply to arbitrary real exponents without additional splitting lemmas.
- Does not address units, mass scaling, or physical interpretation.
formal statement (Lean)
285private lemma exp_four_upper : Real.exp (4 : ℝ) < (54.598151 : ℝ) := by
proof body
Tactic-mode proof.
286 have hpow : (Real.exp (1 : ℝ)) ^ (4 : ℕ) ≤ (2.7182818286 : ℝ) ^ (4 : ℕ) := by
287 exact pow_le_pow_left₀ (Real.exp_pos (1 : ℝ)).le (Real.exp_one_lt_d9).le 4
288 have hnum : (2.7182818286 : ℝ) ^ (4 : ℕ) < (54.598151 : ℝ) := by norm_num
289 have hEq : Real.exp (4 : ℝ) = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by
290 calc
291 Real.exp (4 : ℝ) = Real.exp ((4 : ℕ) * (1 : ℝ)) := by norm_num
292 _ = (Real.exp (1 : ℝ)) ^ (4 : ℕ) := by simpa using (Real.exp_nat_mul (1 : ℝ) 4)
293 rw [hEq]
294 exact lt_of_le_of_lt hpow hnum
295