exp_taylor_10_at_481212
plain-language theorem explainer
This definition supplies the explicit ten-term Taylor polynomial for the exponential at the rational point 481212/1000000. A researcher checking the numerical step in the electron-mass necessity argument cites it to obtain a rational lower bound that forces log(phi) below 0.481212. The construction is a direct finite sum in rationals with no lemmas or tactics applied.
Claim. Let $x = 481212/1000000$. Define the truncated exponential 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 Recognition Science chain. This particular definition supplies a concrete rational value used to bound the logarithm of the golden ratio from above. The upstream structure records the meta-realization axioms that close the self-reference loop required by the forcing chain.
proof idea
The definition is a direct algebraic expansion: it assembles the partial sum of the exponential series up to degree nine evaluated at the fixed rational argument. No lemmas are called; the body is the explicit polynomial written in rationals.
why it matters
The value feeds the lemma exp_taylor_481212_gt_target, which combines with the error bound to prove log_upper_numerical and thereby log(1.618034) < 0.481212. This numerical step supports the T9 necessity claim that the electron mass is forced by the eight-tick octave and the phi-ladder. It closes one concrete inequality inside the overall electron-mass derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.