exp_taylor_10_at_7145
plain-language theorem explainer
The rational value of the 10-term Taylor polynomial for the exponential at argument 7145/10000 is supplied exactly as a fraction. Necessity proofs for the electron mass in Recognition Science invoke this value to obtain a concrete lower bound on the real exponential inside interval arithmetic. The body is a direct finite sum of the standard series terms evaluated in rationals.
Claim. Let $x = 7145/10000$. Define the partial sum $s = 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 proves that the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier in the forcing chain. This auxiliary definition supplies an exact rational lower bound for the exponential at 0.7145, which enters the numerical verification steps of the mass formula. The upstream structure records the meta-realization properties required by the self-reference axioms that anchor the necessity argument.
proof idea
The definition directly constructs the sum by substituting the rational argument into the first ten terms of the exponential series and performing the arithmetic in rationals. No external lemmas are applied; the body is a literal expansion of the truncated polynomial.
why it matters
This supplies the exact rational needed for the lower-bound lemma that compares the Taylor sum to the true real exponential, which in turn supports the module-level necessity result that the electron mass matches the forced value from the phi-ladder. It closes a numerical gap inside the T9 argument deriving the mass from T8 and the alpha-band constants. The parent results are the two lemmas that consume this value to establish the strict inequality 2.0431648 < Real.exp(0.7145).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.