taylor_sum_lt_target
plain-language theorem explainer
The partial sum of the exponential Taylor series at argument 0.481211 together with its Lagrange remainder bound lies strictly below 1.618033. Researchers verifying the numerical steps in the electron-mass necessity argument of Recognition Science would cite this bound when establishing the required logarithmic inequality. The proof is a short tactic sequence that rewrites the real sum and error to rational equivalents, casts the combined strict inequality, and normalizes the target constant.
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 + x^{10}·11/(10!·10) < 1.618033$.
background
This lemma sits inside the module that carries out T9, the necessity proof that the electron mass formula is forced by T8 ledger quantization together with the geometric constants obtained earlier. The Taylor expansion and remainder are introduced solely to produce a concrete numerical bound that can be inverted to a logarithmic statement. The helper definitions compute the rational 10-term sum and the rational error term $x^{10}·11/(10!·10)$ at the fixed argument 481211/1000000; upstream lemmas equate the corresponding real expressions to these rationals and establish that their sum is less than the rational 1618033/1000000.
proof idea
The proof rewrites the left-hand side via taylor_sum_eq_rational and error_term_eq_rational, invokes the combined inequality exp_combined_lt_target, casts the result to reals, and normalizes the right-hand side to 1.618033 by a single norm_num step.
why it matters
The bound feeds directly into the theorem log_lower_numerical that establishes 0.481211 < log(1.618033). That numerical fact closes one link in the T9 necessity chain, confirming that the electron mass is forced once T8 and the phi-ladder constants are in place. The argument therefore supplies a concrete numerical checkpoint inside the larger claim that the mass formula is not an independent input but a derived consequence of the Recognition Science forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.