For any rational polynomial f, repeated-node divided differences equal the corresponding finite linear combination of its node derivatives. Specialize multiplicities r+1 at ell0, r elsewhere, total order 7r.
Method: native-induction. Induction: polynomial degree. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.