exp_taylor_10_at_7144
plain-language theorem explainer
This definition supplies the exact rational value of the 10-term Taylor polynomial for exp at the point 0.7144. It is invoked by the bounding lemmas that close the numerical step in the electron-mass necessity argument. The construction is a direct term-mode expansion using rational powers and factorial denominators.
Claim. Let $x = 7144/10000$. Define the rational $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 establishes that the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier in the chain. This definition supplies a concrete rational that appears inside the numerical verification of an exponential upper bound. The upstream structure 'for' records the meta-realization axioms required by the self-reference forcing, supplying the structural context in which the mass-topology and gap properties are applied.
proof idea
Direct definition that evaluates the standard 10-term Taylor sum at the fixed rational 7144/10000 using ordinary rational arithmetic and the usual factorial coefficients.
why it matters
The definition is used by exp_07144_upper and exp_07144_upper_q to obtain the strict inequality Real.exp(0.7144) < 2.042961. These bounds feed the necessity argument that the electron mass is forced from T8 and the phi-ladder constants inside the Recognition Science framework. It closes a concrete numerical gap required by the T9 claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.