exp_462924882_lower
plain-language theorem explainer
A lower bound establishes that exp(4.62924882) exceeds 102.1 over the reals. Workers deriving forced muon and tau masses from the Recognition Science lepton ladder cite it to close a numerical gap in the phi-power estimates. The proof factors the argument via the exponential addition rule, multiplies two pre-proved component lower bounds, and chains the result by transitivity.
Claim. $102.1 < e^{4.62924882}$ holds over the reals.
background
The lemma belongs to the T10 module that replaces two axioms with proven bounds on predicted muon and tau masses. It draws on the electron structural mass from T9 together with step functions built from cube edges, faces, wallpaper groups, alpha, and pi. Upstream lemmas supply the component bounds exp(4) > 54.598150 and exp(0.62924882) > 1.87620, each obtained from Taylor truncation or power comparison; transitivity of < is taken from the arithmetic foundations.
proof idea
Split the argument as 4 + 0.62924882 and apply the addition formula. Invoke the two component lower bounds, multiply them with nlinarith while using positivity of exp, compare the product to 102.1 by norm_num, then finish with lt_trans.
why it matters
The result feeds directly into phi_pow_neg962_upper_proved, which supplies the upper estimate needed for the lepton mass bounds in the T10 necessity theorem. It therefore contributes to the claim that the muon and tau masses are forced once the electron mass, phi from T4, and the eight-tick geometric constants are fixed. The numerical step keeps the phi-ladder mass formula inside the observed ranges without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.