At a leaf no nonempty proper literal subset triggers branching. A fixed literal belongs to fewer than M^{c-1} width-c clauses for c>=2 and to at most one unit clause. Counting both polarities and widths gives at most B=2 sum_{j=0}^{k-1} M^j<=4M^{k-1} occurrences per variable. With the selected M, B=O_k([sigma^{-1}log(2/sigma)]^{k-1}). Every nonempty leaf clause uses at least one incidence, so its clause count is at most Bn. Repeated disjoint two-case partitions ensure each original satisfying assignment occurs in exactly one leaf. Original variables remain declared throughout, including unused ones.