Expand description
Money and quantities as integers (15.3-6), and what a piece of work
turned out to cost.
The part crates/kernel/spec/Budget.lean specifies this module.
There is no ceiling here and no decision that reads one. Nobody can
price a piece of work before it runs, so the only brake this city has
is Halt: it shuts a scope to new work and stops the background
members inside it. What survives is the reporting half — BudgetUse
is a payload field of Progress::Unplanned and of the evidence a
finished run carries, which is how a person is told what was spent
rather than told in advance what may be.