Construct H_(ell,k) for multiplicities s_ell>0 and distinct nodes such that H_(ell,k)^(j)(x_i)=delta_(i,ell)*delta_(j,k) for j<s_i. Include the k! normalization explicitly.
Method: native-induction. Induction: truncated reciprocal-series degree. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.