For P=sum_alpha c_alpha*X^alpha, coordinate magnitudes<=R with R>=1 and coordinate differences<=delta imply |P(x)-P(y)|<=delta*sum_alpha |c_alpha|*|alpha|*R^(|alpha|-1), omitting degree-zero terms. Compute the bound from the coefficient table.
Method: native-induction. Induction: monomial length and finite coefficient list. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.