Alignment Workspace

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

Rounds and decisions that touch it

None recorded.