exp_error_v2_3
plain-language theorem explainer
This definition supplies the rational remainder term for the tenth-order Taylor expansion of exp at argument 0.8104. Lepton mass derivations in the Recognition Science framework cite it when converting the Taylor polynomial into a certified upper bound on exp(0.8104). The body is a direct algebraic expression that evaluates x^10 times 11 over 10 factorial times 10 with x equal to 8104/10000.
Claim. Let $e = (8104/10000)^{10} * 11 / (10! * 10)$. This rational supplies the explicit truncation error used to bound the Taylor series of the exponential function at 0.8104.
background
Module T10 Necessity derives the muon and tau masses from the electron structural mass (T9), the golden ratio phi (T4), and geometric constants extracted from cube geometry: E_passive equals 11, six faces, wallpaper count W equals 17, and the fine-structure constant alpha. The lepton ladder therefore reduces to step functions built from these quantities and the eight-tick octave. The present definition supplies a concrete rational that controls the remainder when the exponential appears inside those step functions.
proof idea
The definition is a direct algebraic computation: set x to 8104/10000, then return x to the tenth power multiplied by 11 and divided by 10 factorial times 10. It is invoked inside the lemmas that apply Mathlib's exp_bound' to certify exp(0.8104) less than 2.2489.
why it matters
The term closes the numerical gap between the tenth-order Taylor sum and the target bound 2.2489, allowing the downstream lemmas exp_08104_upper and exp_v2_3_q to discharge the exponential inequality required by the lepton mass necessity theorems. It therefore supports the claim that the entire lepton ladder is forced by the Recognition Science constants without extra axioms, consistent with the T0-T8 forcing chain and the RCL composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.