For 1<=j<k let T_j count width-j insertions along a path, including inserted clauses later deleted. Only marked clauses were inserted; initial unmarked clauses are not counted. Units persist, so T_1<=2n. For 2<=j<k, marked-degree bounds give at most 4nM^{j-1} surviving marked clauses. Charge each deleted MARKED width-j clause to a newly inserted strict subset of width i<j. One insertion receives fewer than 2M^{j-i} such charges. Unmarked deletions receive no charge. Therefore T_j<=4nM^{j-1}+2 sum_{i<j} M^{j-i}T_i, giving T_j<=4(3M)^{j-1}n by induction. Every branch inserts something, so summing T_j bounds path length.