exp_error_10_at_081416924
plain-language theorem explainer
The definition supplies the explicit rational error term for the tenth-order Taylor approximation of the exponential at argument 0.81416924. It is invoked by the two bounding lemmas that certify the partial sum stays below 2.25731. The expression is obtained by direct substitution of the scaled input fraction into the scaled Lagrange remainder form.
Claim. The error term is the rational number $e_{10} = (0.81416924)^{10} · 11 / (10! · 10)$, where 0.81416924 is the rational 81416924/100000000. This term is added to the tenth-order Taylor polynomial to produce an upper bound on exp(0.81416924).
background
The lepton generations necessity module shows that muon and tau masses are forced from the electron mass (T9) together with geometric constants E_passive = 11, cube faces = 6, wallpaper count W = 17, and the golden ratio fixed point. The exponential factor appears inside the step functions that map rung numbers to mass ratios on the phi-ladder. This definition supplies the concrete rational needed to control the growth of that exponential inside the mass bound proofs.
proof idea
The definition is a direct algebraic construction: set x to the rational 81416924/100000000, raise to the tenth power, multiply by 11, and divide by 10 factorial times 10. It is applied verbatim inside the native_decide tactic of the companion lemma that adds the Taylor sum to this error term.
why it matters
The definition closes the numerical verification step required for the T10 necessity theorem that replaces the original lepton mass axioms with derived inequalities. It is used by exp_081416924_upper and exp_081416924_upper_q, which feed the muon and tau mass bound lemmas. In the Recognition framework it supports the claim that the full lepton spectrum follows from the forcing chain T5-T8, the recognition composition law, and the eight-tick octave without additional inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.