Theorem. Budget admission preserves a hard componentwise bound [ftip-00CK]

Consider a finite sequence of continuations. Start from \(a_0\preceq b\). At step \(i\), admit only if \(a_i+\bar c_i\preceq b\), and require the realized cost to satisfy \(c_i\preceq \bar c_i\). With \(a_{i+1}=a_i+c_i\), every accumulated cost satisfies \(a_i\preceq b\).

This finite result is a contract theorem, not a prediction that a real executor respects its declared bound.