Item 80: Affordable service on an adaptive docket
Deference line — second wave · difficulty open · project normativity · open · node item-80
The predictable-window cheapest-date scheduler is Lean-proved for a declared finite workload: liability at most the budget, zero residual, claim-to-service factor one (Workload.liability_le, residual_zero). Nothing is proved when the docket grows in response to service — a disposal's successor, a reconsideration, a compiler conflict opening an adjudication — or when it is adversarially generated. The units are fixed: intensity λ_s is what conditional_normative_inductor's liability hypothesis is produced from, and the connector from the workload budget to the enforcer's assessed net worth is an integration item, not part of this one.
Deliverable shape: a stated theorem for a declared adaptive workload class with an exact-rational fixture, or an impossibility witness for a natural class. Acceptance check: the round's runner is discovered by python3 tests/run.py and passes.
Context: CONSOLIDATION.md §9.2 of the mathematical-consolidation round; the normative-affordability round's CLOSED_LOOP_EXISTENCE.md. A solution ships: the class, the theorem, and what it does to the residual term.
Deliverable shape: a stated theorem for a declared adaptive workload class with an exact-rational fixture, or an impossibility witness for a natural class.
Acceptance check: the round's runner is discovered by python3 tests/run.py and passes.
Registered results bearing on this item
None registered.
Where it hangs
- held by normativity
Rounds and decisions that touch it
None recorded.