Termination of finite-cap surplus selection

If the baseline node count exceeds the budget, the procedure returns immediately with empty $\mathrm{\Lambda }$, which is vacuously downward closed. Otherwise the initial set $\{0\}$ is downward closed. Assume the current $\mathrm{\Lambda }$ is downward closed and the algorithm admits $\mathrm{\ell }$. For any $\mu \le \mathrm{\ell }$ coordinatewise with $\mu \mathrm{\ne }\mathrm{\ell }$, choose $j$ with ${\mu }_j<{\mathrm{\ell }}_j$. Then ${\mathrm{\ell }}_j>0$, so admissibility gives $\mathrm{\ell }-e_j\in \mathrm{\Lambda }$, and $\mu \le \mathrm{\ell }-e_j$; downward closure gives $\mu \in \mathrm{\Lambda }$. Thus $\mathrm{\Lambda }\cup \{\mathrm{\ell }\}$ is downward closed, and induction over additions preserves the invariant.

Every accepted addition is a previously unaccepted element of finite $\mathrm{\Gamma }$, and the procedure records each computed or budget-uncomputed candidate so it cannot be processed repeatedly. Each candidate's node set and detail expansion are finite. Hence there are at most $\mathrm{\mid }\mathrm{\Gamma }\mathrm{\mid }$ additions and finitely many candidate inspections; when none remains computable the algorithm returns budget-exhausted or frontier-exhausted, while the undersized initial budget returns budget-too-small.