exp_error_v2_2
plain-language theorem explainer
This definition supplies the scaled Lagrange remainder for the degree-10 Taylor polynomial of exp at argument 0.6316. Lepton-generation necessity proofs cite it to convert the polynomial into a strict numerical inequality used for muon and tau mass bounds. The body is a direct algebraic expression that encodes the standard remainder estimate multiplied by the factor 11.
Claim. Let $e_{v2_2} = (0.6316)^{10} · 11 / (10! · 10)$. This quantity upper-bounds the truncation error of the Taylor series for exp(0.6316) after ten terms.
background
The T10 module derives the muon and tau masses from the electron structural mass (T9) together with the geometric constants E_passive = 11, cube faces = 6, wallpaper count W = 17, and the fine-structure constant α. The exponential appears when the rung steps on the phi-ladder are exponentiated. This definition supplies the concrete remainder term that turns the Taylor polynomial into a rigorous inequality for exp(0.6316).
proof idea
The definition is a direct algebraic expression: set x = 6316/10000, then return x^10 * 11 / (Nat.factorial 10 * 10). It implements the standard bound on the remainder of the exponential Taylor series of order 10.
why it matters
This error term is required by the lemmas exp_06316_lower and exp_v2_2_q, which together establish that exp(0.6316) lies strictly above 1.8806. Those lemmas close the numerical verification step inside the proof that the muon and tau masses are forced by the Recognition Science forcing chain (T0-T8) and the Recognition Composition Law. It therefore discharges part of the T10 necessity claim for the lepton generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.