Fix \(0<\tau \leq 1\) and the autonomous procedure class admitted by \(\Xi \). Suppose every such procedure attaining \(Q_{\rm acq}\geq \tau \) requires a hard compute cap at least \(L>0\): no implementation with a smaller almost-sure cap attains that score. If a uniform economic envelope \(b\) satisfies \(\overline B(T;\mathcal Z_{\rm aut})\leq b<L\), then no admitted autonomous execution reaches score \(\tau \) by \(T\).

An economically feasible separation additionally requires an actual assisted execution achieving the same score and satisfying the shared external constraints. The scalar relation \(U\leq b\) alone does not provide one: resource timing, memory, communication, contributor formation and evaluation must fit a supplied schedule.

The lower-bound premise must cover permitted representations, search, training and controller development. It is stronger than failure of a particular recipe. For the intended conceptual-discovery tasks, establishing such a lower bound remains part of the conjecture. The proposition makes a finite work lower bound operationally decisive when a separately justified economic envelope lies below it.