Theorem: B4: exact optimization of a declared schedule class

The least certified frontier bound over all legal schedules of a finite declared decomposition is obtained by the recurrence

with terminal value $\left|F(J,k)\right|$. Here $w$ is the module peak in Definition def:frontier, or $\left|F\right|+1$ for a delivery.

The recurrence is a finite search and proves schedule optimality within that decomposition.

Proof. Each action increases the delivered prefix or completed-module set. There are finitely many states and no cycle in the recurrence. For a fixed first action, the overall bound is the maximum of its local peak and the optimal remaining bound. Minimizing over all legal first actions exhausts all schedules. Backward induction proves the formula.