The algebraic repeated-node functional of order N sends X^j to 0 if j<N, and X^(N+s) to h_s(t_0,...,t_N), without assuming distinct nodes.
Method: native-induction. Induction: N and monomial degree. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.