The length cost of a complete binary dependency tree
Abstract
Complete binary dependency expansions have an exact additive and strict depth cost.
A DependencyTree Q has a labelled root at every leaf or branch, and a branch has two ordered child trees. Complete means that the two children of every branch have the same height. Admissible candidate relations record the positive flat-candidate inequality at every branch; repeated leaves remain repeated occurrences in the leaf sum.
Assume 1 < z(q) for every label and z(q) >= 1 + z(a) + z(b) whenever candidate(q,a,b). Expanding a complete tree gives one unit for every branch and retains every leaf occurrence. A complete tree of height h has 2^h leaves and 2^h-1 branches, so the root is at least (2^h-1) plus the repeated leaf total, and therefore strictly exceeds 2^(h+1)-1.
This formalization is the exact reusable content of CFMP_GEOMETRIC_REALIZATION, Section 46.2. It treats the full-tree hypothesis explicitly and makes no claim that an arbitrary acyclic candidate family admits such a complete expansion.
Theorem 1.1 (Exact additive cost for a complete expansion).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatBranchDepthCost.full_binary_lower_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Induction on the tree combines the two child bounds. Equal child heights rewrite the parent height as child height plus one, and the two powers combine with pow_succ. The branch inequality then yields the exact additive lower bound.
Theorem 1.2 (Strict exponential depth cost).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/FlatBranchDepthCost.full_binary_strict_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact bound is combined with the strict leaf estimate: every one of the 2^h leaf occurrences is greater than one. This gives z(root) > 2^(h+1)-1, with no distinctness requirement on the leaf labels.