taylor_sum_eq_rational
plain-language theorem explainer
This lemma equates the explicit 10-term Taylor partial sum for the exponential at 0.481211 to the rational value precomputed in the module. Researchers deriving the forced electron mass under T9 would cite it when establishing strict numerical inequalities against the golden ratio. The proof is a one-line wrapper that unfolds the rational definition and reduces the arithmetic by normalization.
Claim. Let $x = 0.481211$. Then $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$ equals the rational 10-term Taylor polynomial for the exponential evaluated at the same $x$.
background
The module proves that the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier. The relevant helper defines the rational Taylor sum at the concrete point 481211/1000000 as the finite sum of the first ten terms. This lemma sits inside the necessity argument that converts the rational expression into a real-number bound used to compare against the target value 1.618033.
proof idea
The proof is a one-line wrapper that applies simp to unfold the rational Taylor definition and then norm_num to verify the numerical identity by direct arithmetic reduction.
why it matters
It supplies the equality step required by the downstream inequality that places the partial sum strictly below 1.618033. That inequality closes part of the T9 necessity chain showing the electron mass is forced once the phi-ladder and eight-tick octave are fixed. The declaration therefore bridges the rational helper to the final comparison against the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.