Recursion (1), proved in $Model/Sorted.lean$ as $EstFFJ.lemma1$. The branch in which $j$ is passed over needs $X₁$ to admit every set the old thresholds admitted, and the branch in which $j$ is taken needs the converse; both are Hall's theorem applied to the map sending a job to the threshold it runs behind.