exp_180454125_lower
plain-language theorem explainer
The lemma establishes the strict inequality 6.07 < exp(1.80454125). Researchers bounding muon and tau masses in the Recognition Science lepton ladder cite it to constrain the phi-powered residue terms. The proof factors the exponential, applies the known lower bound on exp(1), invokes the sibling bound on the fractional part, compares the product via nlinarith, and chains the results with transitivity.
Claim. $6.07 < e^{1.80454125}$
background
This numerical lemma belongs to the T10 module proving that the muon and tau masses are forced from the electron structural mass (T9) together with cube-derived steps (E_passive = 11, faces = 6, W = 17) and the golden ratio phi. The lepton ladder is assembled by combining these geometric constants with alpha and pi bounds already obtained from the eight-tick octave and spherical geometry. The exponent 1.80454125 appears when converting a phi-ladder rung into an exponential form for mass-ratio verification.
proof idea
The proof splits the exponent additively as 1 + 0.80454125 and rewrites the exponential via exp_add. It invokes Real.exp_one_gt_d9 to obtain exp(1) > 2.7182818283. It calls the sibling lemma exp_080454125_lower to obtain exp(0.80454125) > 2.23567. nlinarith establishes the product lower bound using positivity of both exponentials. norm_num shows 6.07 lies below that product, after which lt_trans chains the two inequalities.
why it matters
The lemma supplies a concrete numerical step inside phi_pow_neg375_upper_proved, which in turn discharges the upper-bound hypothesis required for the muon-mass prediction. It therefore contributes to the T10 replacement of the two original axioms in LeptonGenerations.lean by derived inequalities. The surrounding module derives the full lepton ladder from T9 electron mass, the cube-face and wallpaper constants, and the phi self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.