exp_four_upper
plain-language theorem explainer
The inequality exp(4) < 54.598151 supplies a concrete upper estimate used when splitting exponential terms for lepton mass bounds. Researchers establishing forced muon and tau masses from the electron mass and cube geometry cite it to close numeric seams in T10. The proof reduces exp(4) to a fourth power, applies a decimal bound on exp(1), and chains a numerical comparison.
Claim. $\exp(4) < 54.598151$
background
The module develops T10 Necessity, proving the lepton ladder is forced from T9 (electron structural mass) together with E_passive = 11, cube faces F = 6, wallpaper groups W = 17, alpha from T6, and pi. This lemma supplies one supporting exponential bound required to replace external axioms with proven inequalities on predicted muon and tau masses.
The strategy combines the electron mass with step functions derived from cube geometry and the golden ratio phi. Upstream results include the order definition le on LogicNat from ArithmeticFromLogic, though the present numeric lemma rests on standard real analysis facts imported via Mathlib.
proof idea
The tactic proof first shows (exp 1)^4 <= (2.7182818286)^4 via pow_le_pow_left₀ applied to the known bound exp_one_lt_d9, then verifies the numerical fourth power lies below 54.598151 by norm_num. It equates exp(4) to the power using exp_nat_mul after a norm_num rewrite, and concludes by lt_of_le_of_lt.
why it matters
The lemma is invoked directly by exp_46327_upper and exp_463407156_upper, which split larger exponentials to establish the main T10 theorem that muon and tau masses are completely determined by the electron mass, passive edges, faces, wallpaper groups, and alpha. It fills the numeric seam for the paper proposition replacing axioms in LeptonGenerations.lean and supports the eight-tick octave and D = 3 from the forcing chain, though it remains a supporting calculation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.