1-out-of-5 Maximin-Share Allocations Always Exist for Four Agents

For four agents with nonnegative additive valuations, a complete 1-out-of-5 maximin-share allocation always exists, improving the previous 1-out-of-6 guarantee.

Together with known exact-MMS counterexamples, this completely characterizes the four-agent case: the guarantee holds exactly for $d\geq5$.

The main technical contribution is a balanced-residual partition lemma: removing rejected bundles with one of the four highest-ranked goods apiece leaves a remainder that still admits the required number of unit-valued balanced bundles.

In its central $2+2$ case, three unit bundles repair two pairs of colliding high-valued goods.

The theorem is machine-checked in Lean 4.