exp_error_10_at_481211
plain-language theorem explainer
This definition supplies the rational remainder term for the 10-term Taylor expansion of exp at the point 481211/1000000. It is referenced by three lemmas in the same module that bound the partial sum plus error below 1.618033. The body binds the input rational and evaluates the explicit algebraic expression for the bound.
Claim. Let $x = 481211/1000000$. Define the error term as $x^{10} · 11 / (10! · 10)$.
background
The module establishes T9 necessity: the electron mass formula is forced from T8 ledger quantization together with the geometric constants obtained earlier. The Taylor expansion at this specific rational is used to verify that exp(0.481211) lies below the golden-ratio fixed point phi derived in T6. The definition imports phi bounds, alpha derivations, and gap properties to support the numerical comparison.
proof idea
One-line definition that binds x to the rational 481211/1000000 and returns the direct computation x^10 * 11 / (Nat.factorial 10 * 10).
why it matters
The value feeds error_term_eq_rational, exp_combined_lt_target and taylor_sum_lt_target, which together show the Taylor sum plus remainder at 0.481211 is strictly less than 1.618033. These steps close part of the T9 necessity argument that the electron mass is forced by the phi-ladder and the eight-tick octave from T7. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.