Corollary: Finite internal differential expressions

With the smooth weights and fixed tensor maps in (eq:L)–(eq:K6), each $K_5$ placement and $K_{47}$ is a finite differential expression in its respective independent tree product, of total kernel derivative order at most four. The displayed $K_6$ expression has total kernel derivative order at most two.

Proof. Insert (eq:L). In a $K_5$ placement, the derivative of the incoming line has order one, the differentiated $L$ has kernel order at most two, and the outer divergence adds at most one. For $K_{47}$, the differentiated $L$ has order at most two, the other $L$ order one, and the outer divergence adds at most one. Derivatives falling on smooth weights only lower these upper kernel derivative counts.

In $K_6$, the incoming derivative has order one and the outer divergence adds at most one. All products are defined by Proposition prop:tree.