exp_taylor_v2_2
plain-language theorem explainer
This definition supplies the exact rational value of the ninth-order Taylor polynomial for the exponential function evaluated at 0.6316. Physicists deriving the forced muon and tau masses from the electron mass cite it to obtain rigorous bounds on the real exponential. The definition consists of a direct abbreviation of the sum 1 + x + x²/2 + ... + x⁹/9! with x equal to 6316/10000.
Claim. Let $x = 6316/10000$. Define $t = 1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040 + x^8/40320 + x^9/362880$.
background
The module T10 proves that the lepton ladder is forced from the electron structural mass (T9) and geometric constants including E_passive = 11, cube faces = 6, W = 17, and the fine-structure constant α. This definition provides a rational proxy for the exponential function at the specific argument 0.6316 arising in the mass ratio calculations. It supports the comparison with the real exponential using the bound lemma from Mathlib.
proof idea
The definition directly encodes the Taylor polynomial of degree 9 for exp at the rational point 6316/10000. It is a one-line abbreviation with no additional lemmas or tactics applied.
why it matters
This supplies the concrete rational needed for the lemmas exp_06316_lower and exp_v2_2_q that verify the exponential bounds. Those lemmas feed into the mass prediction inequalities that complete the T10 necessity argument for the lepton generations. It closes a numerical gap in the chain from T9 electron mass to the full lepton spectrum using only Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.