Lemma 18 ([A short extension of an earlier low set]). Consider an already constructed edge from a parent U to a child W , in its old working frame. Its low cutoff H_-⊆U has a global downset extension H_-^* agreeing with it on U . This …

Use the boundary notation of U in that old frame for this proof. If the edge was a switch relative to the tag of U , its low cutoff is a rank prefix of U D_a . Thus (J D_a)∩≤r is the required global downset, using at most two leaves. If the edge was same, its low cutoff on U equals P_b minus its unpruned carry union, without the fresh injection. The old list on U has at most five entries by Lemma 16. If its run began at the root, all carry entries are simple: the root base or injections, possibly rank-trimmed. If it began at a switch, the only possibly complicated carry entry is the first of that switch pair. If it is present in the carry, replace the carried pair by; if it is absent from the carry, every carried entry is already simple. This gives a global upset agreeing with the carry union on U . It has at most five terms, each with at most four leaves. Indeed an injection with a rank trim has three leaves; a root base or a second switch base with a trim has at most two; and the flattened pair has two. Taking P_b minus this union gives a global downset with at most 1+5·4=21 leaves. An empty carry is represented by false.