exp_463407156_upper
plain-language theorem explainer
The lemma supplies an upper bound showing the exponential of 4.63407156 is less than 103. Researchers closing muon mass predictions from the electron mass and phi-ladder in Recognition Science cite it to discharge a composite exponential term. The tactic proof splits the argument into a sum, invokes two prior exponential bounds, multiplies them via nlinarith, and chains the result to 103 by transitivity.
Claim. $e^{4.63407156} < 103$
background
The module proves the lepton ladder is forced from the electron mass (T9) together with cube geometry constants E_passive = 11, faces = 6, W = 17, and the golden ratio phi from T4. This numeric lemma closes an exponential term required for the phi to the power -9.63 lower bound inside the mass formula yardstick * phi^(rung - 8 + gap(Z)). Upstream results supply the separate bounds exp(4) < 54.598151 and exp(0.63407156) < 1.88528, plus transitivity of the order on the reals.
proof idea
The proof rewrites the argument as a sum to factor the exponential into a product. It applies the prior lemmas bounding each factor separately. Nlinarith combines those bounds with positivity to control the product. Norm_num verifies the numerical product lies below 103. Transitivity then yields the target inequality.
why it matters
It feeds the theorem that discharges the phi^(-9.63) lower hypothesis, completing a required numeric step for T10 lepton generation necessity. The result links the phi-ladder mass formula to the eight-tick octave and the alpha band (137.030, 137.039). It touches the open seam between the phi endpoint bounds and the electron mass derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.