exp_063407156_upper
plain-language theorem explainer
The lemma establishes that exp(0.63407156) is strictly less than 1.88528. It supplies a numerical bound required for exponentiations in the forced muon and tau mass predictions of the lepton ladder. The proof applies the order-10 Taylor remainder for the exponential, equates the partial sum and error to precomputed rationals, and reduces the inequality via native decision on their sum.
Claim. $exp(0.63407156) < 1.88528$
background
The module proves T10 necessity: the muon and tau masses are forced from the electron structural mass (T9) together with step functions built from cube geometry (E_passive = 11, faces = 6, W = 17), the fine-structure constant α, and the golden ratio φ. This lemma supplies one concrete numerical bound appearing in the mass-ratio exponentiations that replace the two axioms previously present in LeptonGenerations.lean.
proof idea
The proof calls Real.exp_bound' with n=10 to obtain the truncation inequality. It substitutes the explicit Taylor sum exp_taylor_10_at_063407156 and remainder exp_error_10_at_063407156 via simp and norm_num, then casts the native_decide result from exp_063407156_upper_q to reach the rational 188528/100000. Final norm_num reduces the right-hand side to 1.88528.
why it matters
The bound is invoked by exp_463407156_upper, which factors the larger exponent 4.63407156 as 4 plus the present argument and multiplies the known exp(4) bound by this result. It closes a numerical step inside the T10 proof that the lepton rungs are uniquely determined by the eight-tick octave and the derived constants α and π. No new hypotheses are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.