exp_06327_upper
plain-language theorem explainer
The lemma establishes that exp(0.6327) is strictly less than 1.8827. Researchers deriving muon and tau mass ratios from the electron mass in the lepton ladder would cite this numerical certificate when chaining exponential factors. The proof applies the Taylor remainder bound with a 10-term expansion, equates the partial sum and error term to precomputed rationals, and discharges the final comparison by native decision.
Claim. The inequality $e^{0.6327} < 1.8827$ holds.
background
In the Recognition Science framework the module proves T10: the lepton mass ladder is forced once the electron structural mass is fixed by T9. The muon and tau masses are completely determined by the electron structural mass, the passive cube edges E_p = 11, cube faces F = 6, wallpaper groups W = 17, and the fine-structure constant α. This lemma supplies one of the tight numerical upper bounds on an exponential factor that appears in the step functions of the mass formula.
proof idea
The proof first records positivity and the bound 0.6327 ≤ 1 by norm_num. It invokes Real.exp_bound' with n = 10 to obtain exp(x) ≤ Taylor sum up to order 9 plus the explicit remainder term. The partial sum is rewritten as exp_taylor_v2_1 and the remainder as exp_error_v2_1 by simplification and norm_num. Their sum is shown strictly less than 1.8827 by exact_mod_cast from exp_v2_1_q, after which the final equality to 1.8827 is discharged by norm_num.
why it matters
The bound is invoked by the downstream lemma exp_46327_upper to control the exponential factor at 4.6327 in the tau mass prediction. It contributes to the main theorem of the module that the lepton ladder is forced from T9 together with the geometric constants E_p, F, W and α. Within the Recognition Science program this closes one of the numerical certificates needed to replace the two axioms in LeptonGenerations.lean, advancing the claim that all lepton masses follow from the eight-tick octave and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.