exp_080454125_lower
plain-language theorem explainer
The lemma establishes the strict numerical inequality 2.23567 < exp(0.80454125) as a verified lower bound on the exponential. Physicists deriving forced muon and tau masses from the electron mass in the lepton ladder would cite it to close the numerical steps in the T10 necessity argument. The proof applies the Taylor remainder bound of order 10, equates the partial sum and error to precomputed rationals, and discharges the comparison by linear arithmetic after casting from a companion rational lemma.
Claim. $2.23567 < e^{0.80454125}$
background
In the T10 module that forces the lepton ladder from the electron structural mass (T9) and geometric constants, this lemma supplies one of the concrete exponential bounds needed to replace the original axioms on muon and tau mass predictions. The local setting combines the golden ratio phi, the eight-tick octave, cube-face counts (E_passive = 11, faces = 6), wallpaper groups (W = 17), and the fine-structure constant alpha to determine the rung steps on the phi-ladder. Upstream results include the order-10 Taylor polynomial exp_taylor_10_at_080454125, the matching remainder term exp_error_10_at_080454125, and the rational comparison exp_080454125_lower_q that supplies the key lower estimate.
proof idea
The proof calls Real.exp_bound with absolute-value hypothesis and n = 10 to obtain the Taylor-plus-remainder inequality. It then equates the explicit sum and error expressions to the module definitions exp_taylor_10_at_080454125 and exp_error_10_at_080454125 by simplification and norm_num. A cast from exp_080454125_lower_q provides the rational lower bound, after which linarith chains the comparisons to reach the target inequality.
why it matters
The lemma feeds directly into exp_180454125_lower, which itself supports the broader T10 claim that lepton rungs are forced by the Recognition Science constants without extra axioms. It contributes to the module goal of deriving muon and tau masses from the electron mass together with phi-ladder steps arising from cube geometry and the eight-tick structure. No open scaffolding remains at this leaf; the result is fully proved and closes one numerical verification step in the lepton necessity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.