exp_08104_upper
plain-language theorem explainer
The inequality establishes that exp(0.8104) is strictly less than 2.2489. Researchers deriving forced muon and tau masses from the electron mass in Recognition Science cite this bound to control upper limits on the phi-ladder steps. The proof applies the Taylor remainder bound for the exponential at order 10, equates the partial sum and error to precomputed rationals, and chains the result to the target via a cast from a rational comparison.
Claim. $exp(0.8104) < 2.2489$
background
In the module proving necessity of the lepton ladder, numerical exponential bounds support mass predictions that replace two axioms with inequalities derived from the electron structural mass and geometric constants. The argument 0.8104 appears in intermediate calculations combining E_passive = 11, cube faces = 6, wallpaper groups W = 17, and the fine-structure constant to produce the step functions on the phi-ladder. The lemma depends on three sibling results: the Taylor partial sum up to order 9 for x = 8104/10000, the explicit remainder term x^10 * 11 / (10! * 10), and the rational inequality verifying their sum lies below 22489/10000.
proof idea
The tactic proof first obtains hx_pos and hx_le1 by norm_num, then applies Real.exp_bound' with n = 10 to produce the Taylor-plus-remainder estimate. It equates the partial sum to the precomputed Taylor rational and the remainder to the error rational via simp and norm_num. A cast from the rational inequality lemma supplies the strict upper bound, after which the final normalization step reaches the decimal target 2.2489.
why it matters
This bound closes a numerical gap in the T10 necessity argument that forces the muon and tau masses from the electron mass (T9) and the eight-tick geometric constants. It is invoked directly by the downstream lemma that splits exp(1.8104) = exp(1) * exp(0.8104) to obtain the next rung bound. Within the Recognition framework the result helps replace axiomatic lepton assumptions with inequalities derived from the phi-ladder and cube geometry, tightening the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.