exp_taylor_10_at_481211
plain-language theorem explainer
This definition supplies a rational 10-term Taylor polynomial for the exponential at the argument 481211/1000000. It is cited inside the T9 necessity module to obtain machine-decidable bounds that feed the electron-mass forcing argument. The definition is realized by direct term-mode substitution of the rational argument into the truncated series.
Claim. Let $x = 481211/1000000$. The partial sum is $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 geometric constants obtained from the earlier forcing chain. This definition supplies a rational proxy for the exponential series that appears in the bounding steps of that argument. It depends on the meta-realization certificate structure, which records the coherence properties required for self-referential forcing without further design choices.
proof idea
The definition is a direct term-mode expression that binds the rational 481211/1000000 to a local variable and assembles the explicit sum of the first ten factorial-denominated powers. No lemmas are invoked; it functions as a one-line wrapper that materializes the polynomial for exact rational arithmetic.
why it matters
The definition is invoked by the lemmas exp_combined_lt_target, taylor_sum_eq_rational and taylor_sum_lt_target that together certify the partial sum plus remainder lies strictly below 1.618033. It thereby supplies a computational anchor inside the T9 necessity proof for the electron mass. In the Recognition framework the step closes a numerical gap between the recognition composition law, the eight-tick octave and the concrete mass assignment on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.