exp_error_v2_4
plain-language theorem explainer
This definition supplies the rational truncation error for the 10-term Taylor series of exp(0.8093). It is invoked by the bounding lemmas that certify the exponential inequalities used in forcing the muon and tau masses from the electron mass and geometric constants. The body evaluates the scaled Lagrange remainder directly as a rational number.
Claim. Define the error term $e = (8093/10000)^{10} * 11 / (10! * 10) in Q$.
background
The lepton generations necessity module derives muon and tau masses as forced from the electron structural mass (T9) together with step functions from cube geometry, alpha, and the golden ratio. The exponential enters the mass formula when exponentiating rung increments on the phi-ladder. This definition computes the exact rational remainder for the Taylor expansion of exp(0.8093) to support machine-checked bounds that replace the original axioms.
proof idea
The definition binds x to 8093/10000 and returns x^10 multiplied by 11 divided by the product of 10 factorial and 10. It is a direct algebraic definition with no lemmas or tactics applied.
why it matters
This definition feeds exp_08093_lower and exp_v2_4_q, which establish the strict bounds on exp(0.8093) required for the T10 lepton mass predictions. It closes the numerical gap between the partial Taylor sum and the true exponential using the standard remainder estimate, preserving the intervals derived from the Recognition Science constants and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.