exp_combined_lt_target
plain-language theorem explainer
The lemma shows the 10-term rational Taylor sum for exp at x=481211/1000000 plus its Lagrange error bound is strictly less than 1.618033. Electron mass necessity proofs in Recognition Science cite it to keep the exponential factor below phi. The proof is a one-line native_decide that evaluates the rational inequality directly.
Claim. Let $x = 481211/1000000$. 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 belongs to the T9 necessity module proving the electron mass formula is forced from T8 ledger quantization and geometric constants. The sibling definitions supply the partial Taylor sum up to degree 9 and the error bound x^10 * 11 / (10! * 10) at the fixed rational point 481211/1000000. Upstream results provide the unit elements in LogicInt and LogicRat for the rational arithmetic together with the phi-closed property of 1.
proof idea
The proof is a one-line wrapper that invokes native_decide on the sum of the two rational helpers exp_taylor_10_at_481211 and exp_error_10_at_481211 compared against 1618033/1000000.
why it matters
It feeds the real-number statement taylor_sum_lt_target, which supports the electron mass necessity theorem under T9. The bound confirms the exponential term remains below the self-similar fixed point phi in the forcing chain from T5 J-uniqueness through T8. The module derives the mass formula using constants such as alpha in the 137 band and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.