exp_taylor_481212_gt_target
plain-language theorem explainer
The lemma certifies that the 10-term Taylor polynomial for exp at 0.481212 exceeds 1.618034 plus its explicit remainder bound. Recognition Science researchers verifying the forced electron-mass rung cite this rational check when confirming the strict logarithmic inequality log(1.618034) < 0.481212. The proof is a one-line native_decide evaluation of the concrete rational comparison.
Claim. Let $x = 481212/1000000$. Let $T_{10}(x) = 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$ be the 10-term Taylor sum for $e^x$. Let $E_{10}(x) = x^{10} · 11 / (10! · 10)$ be the error bound. Then $1.618034 + E_{10}(x) < T_{10}(x)$.
background
The declaration belongs to the T9 necessity module, which shows that the electron mass formula is forced from T8 ledger quantization together with the geometric constants (phi-ladder, J-uniqueness) derived earlier. The two upstream definitions supply the exact rational objects: exp_taylor_10_at_481212 computes the partial sum up to the $x^9/9!$ term at the fixed argument 481212/1000000, while exp_error_10_at_481212 supplies the concrete Lagrange-style tail bound $x^{10}·11/(10!·10)$ that dominates the remainder. These rational expressions permit kernel-level comparison without floating-point rounding.
proof idea
The proof is a one-line wrapper that applies native_decide to the concrete rational inequality 1618034/1000000 + exp_error_10_at_481212 < exp_taylor_10_at_481212, which the kernel evaluates directly.
why it matters
This numerical fact supplies the key comparison used by the downstream theorem log_upper_numerical to convert the Taylor bound into the strict inequality log(1.618034) < 0.481212 via Mathlib's exp_bound lemma. It thereby closes one verification step inside the T9 necessity argument that the electron mass rung is determined by the eight-tick octave and the phi-ladder. The parent result log_upper_numerical in turn feeds the larger claim that the mass formula is forced from T8 and the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.