AI 中文总结
研究四个具有非负加法估值代理的五选一最大最小份额分配问题，通过平衡剩余划分引理证明其总是存在并改进了保证，刻画了该情况下的条件，且定理经机器验证。
AI 中文摘要
对于具有非负加法估值的四个代理，完整的五选一最大最小份额分配总是存在，改进了之前六选一的保证。结合已知的精确最大最小份额反例，这完全刻画了四个代理的情况：当且仅当\(d\geq5\)时保证成立。主要技术贡献是一个平衡剩余划分引理：移除每个包含四个最高排名商品之一的被拒绝捆绑包后，剩余部分仍允许所需数量的单位价值平衡捆绑包。在其核心的\(2 + 2\)情况下，三个单位捆绑包修复两对冲突的高价值商品。该定理在Lean 4中经过机器验证。
英文摘要
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.
Comments8 pages. The complete Lean 4 formalization (kernel-checked; axioms: propext, Classical.choice, Quot.sound) is included in the ancillary files
