On [0,M], positive-series estimates give positivity/monotonicity and |exp(x)-exp(y)|<=3^(ceil(M)+1)*|x-y|; on [0,1] improve the bound to 3. Prove e<3 by a factorial tail.
Method: native-order. Induction: none. Risk: high.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.