exp_46327_upper
plain-language theorem explainer
The lemma supplies the concrete upper bound exp(4.6327) < 102.82 required to close the numeric interval for the predicted tau mass in the lepton ladder. Researchers deriving the forced muon and tau spectrum from T9 would cite it to verify the relative-error windows without free parameters. The proof splits the exponent, multiplies the separate bounds from the companion lemmas exp_four_upper and exp_06327_upper, and chains the product inequality via transitivity.
Claim. $e^{4.6327} < 102.82$
background
In the Necessity module the muon and tau masses are obtained from the electron structural mass (T9) together with the exact geometric constants E_passive = 11, cube faces = 6, wallpaper groups W = 17, and the fine-structure constant α. The module replaces earlier axioms with proven inequalities on the predicted masses; the present lemma supplies one of the numeric bounds needed to certify those inequalities lie inside the stated 2 % and 1 % relative-error windows.
proof idea
The proof rewrites the argument as 4 + 0.6327, applies the addition formula for exp, invokes the sibling lemmas exp_four_upper and exp_06327_upper, multiplies the resulting inequalities with nlinarith, evaluates the product numerically, and finishes with lt_trans from ArithmeticFromLogic.
why it matters
The bound is used directly by phi_pow_neg9627_lower_v2, which in turn supports the main T10 statement that the lepton ladder is forced from T9 with no free parameters. It therefore contributes to the claim that muon and tau masses are completely determined by the electron mass, E_p = 11, F = 6, W = 17, α, and φ. The result sits inside the eight-tick octave structure that fixes the geometric constants throughout the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.