Rank-maximal assignments and the uncovered set: the McKelvey and Bordes inclusions through seven agents, and the failure of the Gillies variant from four
Abstract
In the assignment (house allocation) domain of n agents, n houses and strict preferences, an assignment μ majority dominates λ when more agents prefer their house under μ than under λ; because this relation has ties, there are three covering relations — Bordes, Gillies and McKelvey — and three uncovered sets. Brandt, Chen, Dong, Lederer and Schlenga (arXiv:2602.14816) report that for n ≤ 5 every rank-maximal assignment lies in the McKelvey uncovered set, and leave the general case open. We show the following. The McKelvey inclusion holds for n=6 and n=7, and in the stronger Bordes form; moreover the hypothesis can be weakened from rank-maximality to local rank-maximality — no exchange of two agents' houses and no cyclic exchange among three agents improves the count vector — and the conclusion still holds for n ≤ 7; exchanges of two agents alone suffice for n ≤ 4 and fail at n=5, while the covering quantifier cannot be localised in the same way — at n=6 a witness against a covering may have to move five of the six agents. These statements for n ≥ 5 rest on unsatisfiability certificates from a SAT solver (one instance per conjugacy class of Sym(n), ten at n=6 and fourteen at n=7) and are not formalised; the statements for n ≤ 4, the n=5 sharpness witness, and a census of the 331 776 four-agent profiles are verified in Lean 4 from the definitions. The Gillies variant behaves differently: from n=4 on there are profiles with a rank-maximal assignment outside the Gillies uncovered set — explicit witnesses for n=4,5,6,7 are verified in Lean, n=4 is the smallest such size, exactly 9 504 of the 331 776 four-agent profiles are of this kind, and a padding construction gives a witness for every n ≥ 4. The mechanism is the one the source names: a popular assignment Gillies covers everything it dominates. The general question remains open; we record why the obvious local arguments cannot settle it.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
79b317555539698f6d1c4b105e9cffc69cec72a59e7c129dc79d5dd6949cff05
Claim ledger
Stated results
RU1candidate2026-09-07
n = 6: every rank-maximal assignment is Bordes uncovered, hence lies in the (McKelvey) uncovered set the source means – the first case beyond the source's exhaustive n <= 5
This ledger entry is reported in prose and is not bound to a Lean theorem.RU2candidate2026-09-07
n = 7: every rank-maximal assignment is Bordes uncovered, hence in the source's uncovered set
This ledger entry is reported in prose and is not bound to a Lean theorem.RU3routine2026-09-07
n = 3: every rank-maximal assignment of every one of the 216 three-agent profiles is Bordes, Gillies and McKelvey uncovered
RU4known data2026-09-07
n = 4: every rank-maximal assignment of every one of the 331 776 four-agent profiles is Bordes uncovered, hence McKelvey uncovered – the source's statement, kernel-checked
RU5known data2026-09-07
n = 5 reproduced: over all 9 078 630 profiles up to agent/house relabelling, no rank-maximal assignment is Bordes or McKelvey covered; 544 720 of them have a Gillies-covered one
This ledger entry is reported in prose and is not bound to a Lean theorem.RU6candidate2026-09-07
The GILLIES uncovered set does not contain every rank-maximal assignment: explicit witnesses at n = 4, 5, 6, 7, none at n = 3, and at n = 4, 5, 6 the same assignment is simultaneously Bordes/McKelvey uncovered and Gillies covered
RU7measurement2026-09-07
Census at n = 4: exactly 9 504 of the 331 776 profiles (2.865%) have a rank-maximal assignment outside the Gillies uncovered set, and 0 have one outside the Bordes (hence McKelvey) uncovered set
RU8known2026-09-07
Controls: the source's Example ex:UCₛubseteq_PO reproduced (a Pareto-optimal assignment that is McKelvey covered, so the covering relation is non-empty and the n <= 7 theorems are not vacuous); a popular assignment is uncovered for all three relations (the other half of the source's sentence, one line); rank-maximal does not imply popular; the majority relation is irreflexive and has ties
RU9candidate2026-09-07
PROSE: for EVERY n >= 4 there is an n-agent profile with a rank-maximal assignment outside the Gillies uncovered set – a padding construction from the n = 4 witness
This ledger entry is reported in prose and is not bound to a Lean theorem.RU10candidate2026-09-07
Strengthening: for n <= 7 it is enough that the assignment admits no lexicographically improving swap of two agents' houses or 3-cycle of three agents' houses – LOCAL rank-maximality already forces Bordes uncoveredness; swaps alone suffice for n <= 4 and fail at n = 5
This ledger entry is reported in prose and is not bound to a Lean theorem.RU11measurement2026-09-07
Measurement: at n = 4 every assignment that Gillies covers a rank-maximal one is popular (12 672 such coverings, all popular); at n = 5 that characterisation fails – 32 560 of 731 360 coverings have a non-popular coverer
This ledger entry is reported in prose and is not bound to a Lean theorem.RU12candidate2026-09-07
Kernel-bound form of the strengthening: at n <= 4 a SWAP-OPTIMAL assignment – one whose count vector no exchange of two agents' houses improves – is already Bordes uncovered, hence McKelvey uncovered; and the radius-2 hypothesis is sharp, an explicit 5-agent profile has a swap-optimal, McKelvey-covered assignment
Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- n agents, n houses, every agent with a strict linear order over the houses. An *assignment* is a bijection agents → houses; there are n! of them. Write N_(μ,λ) for the agents who weakly prefer their house under μ to their house under λ; then
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7