exp_taylor_v2_1
plain-language theorem explainer
The definition supplies the rational value of the degree-9 Taylor polynomial for exp at 0.6327. It is cited in proofs establishing strict upper bounds on the real exponential for use in lepton mass calculations within the T10 necessity argument. The construction enumerates the series coefficients explicitly as a single rational expression.
Claim. Let $x = 6327/10000$. Define $p(x) = 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$, where $p(x)$ is computed in the rationals.
background
In the module establishing that the lepton ladder is forced from prior results on the electron mass, geometric constants from the cube, and the fine-structure constant, numerical bounds on the exponential function appear in the accuracy statements for muon and tau masses. The definition provides a concrete rational proxy for exp(0.6327) to facilitate exact rational arithmetic in subsequent lemmas. Upstream results include exact values for passive edges E_passive = 11 and wallpaper groups = 17, which enter the step formulas for muon and tau masses.
proof idea
The definition is a direct construction that adds the first ten terms of the Taylor series for the exponential function, with each term formed by dividing the appropriate power of the input rational by the corresponding factorial.
why it matters
This definition feeds the lemmas exp_06327_upper and exp_v2_1_q, which in turn support the mass matching bounds in the main theorem lepton_ladder_forced_from_T9. It closes part of the numerical verification for the T10 claim that muon and tau masses are determined without free parameters by the electron structural mass, E_passive=11, F=6, W=17, and alpha. The construction aligns with the framework's emphasis on deriving all constants from the forcing chain and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.