Theorem. Budget-preserving layer admission [ftip-00F4]

✍️sourceAGENTDRAFTED

Let a candidate layer cost \(c\geq 0\), remaining budget be \(b\geq 0\), and admission require \(c\leq b\). After admission, set \(b'=b-c\); then \(b'\geq 0\) and the total admitted cost is at most the initial budget.

Proof. Subtracting a nonnegative cost no larger than \(b\) preserves nonnegativity; induction over admissions gives the total bound.