While this submission is a draft, it cannot be used by other submissions.

Proof of `The Extreme Values of the Fairness Parameter` (2nd statement)

groundedproofs/Lax117284Proofs/ExtremeFairness.lean · lax-117284

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The empty schedule is feasible and serves every client on no day, which is enough.