Theorem. Lineage cost is additive over disjoint child subtrees [ftip-00CI]
✍️source

    Let the root \(r\) of a finite lineage tree have children \(v_1,\ldots ,v_k\). Then

    \[ C_{\rm lin}(\mathcal T)=c_r+ \sum _{j=1}^{k}C_{\rm lin}(\mathcal T_{v_j}). \]

    This finite accounting identity follows from assigning each local cost to exactly one node.

    Proof. 

      The node set is the disjoint union of \(\{r\}\) and the node sets of the child subtrees. Splitting the finite sum in Definition [ftip-00CH] over that disjoint union gives the equality componentwise.