Economics

Motivation

How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.

Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements $b_1, b_2$.

Timeline of the relevant results:

• Budish (2011, doi:10.1086/664613): approximate CEEI with almost equal budgets for many agents, with an approximate market-clearing error.
• Segal-Halevi (AAMAS 2018, arXiv:1705.04212), a follow-up to the preprint of this paper: for four agents with arbitrary budgets, non-existence of CE persists even with generic budgets.
• Babaioff, Nisan and Talgam-Cohen (preprint 2017, journal 2021): exact CE for two additive agents with almost equal unequal budgets (Theorem 7.1), and for two agents with identical preferences and generic budgets (Theorem 8.1).

Setting

There are $m$ indivisible items $M$ and two agents. Agent $i$ has a valuation $v_i : 2^M \to \mathbb R$ that is additive, normalized ($v_i(M)=1$), non-negative, monotone and strict (different bundles have different values), and a budget $b_i > 0$, with $b_1 + b_2 = 1$. An allocation $\mathcal S = (\mathcal S_1, \mathcal S_2)$ gives every item to exactly one agent. Item prices $p_j \ge 0$ price a bundle at $p(S) = \sum_{j \in S} p_j$.

A bundle $S$ is demanded by agent $i$ at prices $p$ if $p(S) \le b_i$ and $p(T) > b_i$ for every bundle $T$ with $v_i(T) > v_i(S)$. A competitive equilibrium (CE) is a pair $(\mathcal S, p)$ in which each $\mathcal S_i$ is demanded by agent $i$. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if $v_i(\mathcal S_i) \ge b_i$ for both agents, and anti-proportional if $v_i(\mathcal S_i) \le b_i$ for both, strictly for one.

The truncated share of agent $i$ is

$$b_i^- = \max\{ v_i(\mathcal S'_i) : \mathcal S' \text{ PO},\ v_i(\mathcal S'_i) \le b_i \},$$

the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if $v_i(\mathcal S_i) \ge b_i^-$. The exceptional set $R_i$ (Definition 6.2) consists of the budget pairs $(b_i, 1-b_i)$ for which two PO allocations $\mathcal S(r), \mathcal S(r+1)$, consecutive in agent $i$'s order of preference, satisfy $b_i / v_i(\mathcal S(r+1)_i) = (1-b_i)/(1-v_i(\mathcal S(r)_i))$. It is finite. The rectangle $T_i$ (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.

In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.

Formalization targets

Goal: Theorem 8.1 (p. 20)

If $v_1 = v_2$, $b_1 > b_2$, and $(b_1,b_2) \notin R_i$ for some agent $i$, then

$$\exists\, (\mathcal S, p) \text{ a CE with } v_j(\mathcal S_j) \ge b_j^- \text{ for } j = 1, 2.$$

Milestones

1. Proposition 5.1 (p. 12): every budget-proportional, and every anti-proportional, PO allocation is supported in a CE.
2. Lemma 6.3 (p. 15): no budget-proportional allocation, no PO anti-proportional allocation, $(b_1,b_2) \notin R_i$ and $T_i = \emptyset$ imply a CE with truncated shares.
3. Constant-sum claim (p. 20): with identical preferences every allocation is PO and none is anti-proportional.
4. Lemma 8.2 (p. 20): if every allocation is PO and $(b_1,b_2) \notin R_i$ for some $i$, a CE exists; if moreover no PO allocation is anti-proportional, the same CE gives truncated shares.

Significance

Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).

The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle $T_i$ and the exceptional set $R_i$, whose informal versions leave conventions implicit (the maximization runs over PO allocations only; $R_i$ is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.

Difficulty

The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all $2^m$ bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs $R_i$, which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.

Formalization scope

Items are Fin m; agents are Fin 2, with indices $0, 1$ for the paper's agents $1, 2$, so $b_1 > b_2$ is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to $1$. All quantities are real.

Committed conventions and disclosed restrictions:

• Strictness is injectivity of each valuation on bundles. The paper allows one exception, identical items; that exception is dropped, so markets with identical items are not covered by these statements.
• The budget-proportional share is written $b_i\,v_i(M)$, which equals $b_i$ under normalization.
• The truncated share is stated without a max: $v_i(\mathcal S_i) \ge v_i(\mathcal S'_i)$ for every PO $\mathcal S'$ with $v_i(\mathcal S'_i) \le b_i$.
• "$(b_1,b_2)$ does not belong to $R_i$ for some agent $i$" is read as an existential over $i$.
• $R_i$ is encoded with consecutive PO allocations and the cross-multiplied equation, equivalent to the page's quotient form.
• The constant-sum sentence of p. 20 says "at most their truncated share"; the definition it paraphrases (anti-proportional, p. 12) uses the budget-proportional share, and that is what is stated.

Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set $R_i$ for one agent, never all unequal budgets.

Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.

Selected references

• M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150, https://doi.org/10.1287/moor.2020.1062
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• E. Segal-Halevi, Competitive Equilibrium for Almost All Incomes, Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212

Motivation

Competitive equilibrium is a way to divide goods when each participant has a budget reflecting her entitlement. With divisible goods, proportional value is a natural fairness target. Indivisible goods make that target unavailable in some markets: a single item cannot give two agents positive fractions of its value. The question becomes what fairness a market outcome can guarantee without dividing an item or assuming that agents value items additively. Babaioff, Nisan and Talgam-Cohen, §2.3 and §3 place this question in a discrete Fisher market, where budgets determine purchasing power but leftover money has no value to agents.

The paper introduces an $\ell$-out-of-$d$ maximin share to express the entitlement of an agent whose budget is at least $\ell/d$. Its Proposition 3.2 says that every competitive equilibrium provides this share. The result applies to any number of agents and to arbitrary cardinal preferences; it does not require the additive assumptions used for the paper's equilibrium existence results. The same paper compares the conclusion with the earlier one-out-of-$(n+1)$ guarantee for nearly equal budgets and explains that other rational shares can give a stronger benchmark in a given market. Babaioff, Nisan and Talgam-Cohen, §3.3

Setting

Let $M$ be a finite set of indivisible items and $N$ a finite set of agents. Agent $i$ has a valuation $v_i(S)$ for each bundle $S\subseteq M$ and a positive budget $b_i$. The budgets are normalized by $\sum_{i\in N}b_i=1$. An allocation $S=(S_i)_{i\in N}$ partitions all items: each item belongs to exactly one agent's bundle. A price vector gives each item $j$ a nonnegative real price $p_j$, and the price of a bundle is $p(S)=\sum_{j\in S}p_j$. Babaioff, Nisan and Talgam-Cohen, §2.1–2.2

An allocated bundle $S_i$ is demanded when it costs at most $b_i$ and every bundle that $i$ strictly prefers costs more than $b_i$. A competitive equilibrium (CE) is an allocation and price vector for which each agent demands her allocated bundle. Demand compares $S_i$ with every subset of $M$, including bundles assigned to other agents and unions of several such bundles. Money is an allocation device in this model; an agent's valuation concerns her bundle alone. Babaioff, Nisan and Talgam-Cohen, Definition 2.1

For $d>0$ and $0\le\ell\le d$, consider every partition $(T_1,\ldots,T_d)$ of $M$ into $d$ labeled parts. Empty parts are permitted. For each partition, an adversary can leave the agent any $\ell$ parts, so the smallest value of a union of exactly $\ell$ parts is her guarantee for that partition. The agent chooses the partition that maximizes this worst-case value. This is her $\ell$-out-of-$d$ maximin share. The allocation $S$ guarantees the share when $v_i(S_i)$ is at least the resulting maximin value. Babaioff, Nisan and Talgam-Cohen, Theorem 1.2 and Definition 3.1

Formalization targets

Equilibrium fairness

For every agent $i$, every competitive equilibrium, and every pair of natural numbers $\ell,d$ with $d>0$ and $\ell/d\le b_i$, the goal is Proposition 3.2:

$$v_i(S_i)\ge \max_{(T_1,\ldots,T_d)} \min_{L\subseteq[d],\,|L|=\ell} v_i\!\left(\bigcup_{t\in L}T_t\right).$$

The three milestones record the paper's intermediate claims in order: the total price of all items is at most the total budget; among $d$ parts, some $\ell$ have price at most $\ell/d$ of the total; and a bundle an agent can afford is no better for her than the bundle she demands. The goal quantifies over every eligible rational share rather than selecting a single fixed denominator. Babaioff, Nisan and Talgam-Cohen, proof of Proposition 3.2

Related equilibrium properties

Two companions record the first welfare theorem, which makes a CE allocation Pareto optimal under strict preferences, and the appendix's coalition form of justified envy. The latter excludes the single case in which the comparing agent's bundle and the coalition's union are both empty, because the printed strict comparison is false there. These companions provide context for the equilibrium notion; neither changes the valuation generality of Proposition 3.2. Babaioff, Nisan and Talgam-Cohen, Theorem 2.4 and Claim A.8

Significance

The proposition gives a fairness conclusion conditional on equilibrium existence. It covers agents with different entitlements and nonadditive valuations, using a share that the agent herself evaluates through a partition of the items. The result does not assert that an equilibrium exists for every market. It says that any equilibrium already present meets all the stated rational-share benchmarks simultaneously. The paper uses this to relate competitive outcomes to maximin guarantees previously studied for nearly equal budgets. Babaioff, Nisan and Talgam-Cohen, §3

A machine-checked development would add a reusable account of finite allocations, bundle prices, demand, and maximin shares, plus a certified bridge between equilibrium and fairness. The draft Lean items in this mission are open statements with sorry; the local build checks their types and imports, not their mathematical proofs. The equivalence of the chosen maximin encoding with the finite max–min formula is checked separately in a sorry-free sanity file. Formal proofs of the goal and its milestones remain solver work.

Difficulty

The main formal issue is to keep the quantifiers and boundary cases aligned with the fairness definition. The guarantee concerns every partition into $d$ parts, including empty parts, and the worst choice among subsets of exactly $\ell$ parts. A benchmark formed from one convenient partition, from at most $\ell$ parts, or from a restricted family of affordable bundles would have a different meaning. The total price comparison also depends on every item being allocated exactly once. The appendix companion has a separate edge case: strict envy cannot follow from demand when the two compared bundles coincide as the empty set.

Formalization scope

Items are Fin m, agents are Fin n, and valuations are real-valued functions on finite item sets. An allocation is a function from items to agents, so feasibility and market clearing are part of its type. A partition into $d$ parts is a function from items to Fin d; it allows empty parts. Prices and budgets are real. The goal assumes positive budgets with sum one, nonnegative prices through the CE predicate, and $d>0$. The case $\ell=0$ is allowed; the budget condition implies $\ell\le d$. The Lean maximin guarantee is written as a quantified comparison rather than using a real supremum or infimum, avoiding default values on empty extrema. A sanity theorem relates it to the finite max–min expression under its proper domain conditions.

The paper's normalization and arbitrary-preference scope are retained in the goal. Strict preferences are used only for the first-welfare and appendix companions. There, injective valuations exclude the paper's exception for identical items, and the appendix claim additionally excludes the case in which the comparing agent's bundle and the coalition's union are both empty. The mission's setting is repeated locally because no published platform definition has the same bundle market and budget conventions; the related housing, divisible-goods, and convex-economy models use different objects.

Contributions should preserve full market clearing, demand over every item bundle, nonnegative prices, all $d$-part partitions, and exactly $\ell$ selected parts. The definitions and finite averaging milestone can be reused in other fair-division developments. Proving the three source milestones and the goal, or improving the formal treatment of the appendix edge case, are within scope.

Selected references

• M. Babaioff, N. Nisan, and I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, Mathematics of Operations Research, 2021; arXiv:1703.08150v2, DOI:10.1287/moor.2020.1062. The mission cites the pinned preprint's pages and numbering.

Motivation

Many allocation problems divide indivisible goods among agents who are entitled to different shares but cannot pay with real money: course seats among students, shifts among workers, inherited items among heirs. A standard mechanism gives each agent a budget of artificial currency and lets a market run. When budgets are equal this is the competitive equilibrium from equal incomes (CEEI) of Varian (1974), the basis of the course-allocation mechanism of Budish (2011). With indivisible items, however, an equilibrium can fail to exist: one item and two agents with equal budgets already admit none, because whoever does not get the item could afford it at any price the owner can pay.

Babaioff, Nisan and Talgam-Cohen (arXiv 2017; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) ask whether this failure is robust or a knife edge, and answer for two agents with additive preferences: an arbitrarily small, strict inequality between the budgets restores existence. Budish's approximate CEEI perturbs budgets randomly for the same reason; this mission formalizes the exact two-agent result.

Setting

A discrete Fisher market has a set $M$ of $m$ indivisible items and two agents. Agent $i$ has a valuation $v_i$ assigning a real value to every bundle $S\subseteq M$, and a budget $b_i>0$. Valuations are additive ($v_i(S)=\sum_{j\in S}v_i(\{j\})$), normalized ($v_i(M)=1$), non-negative, monotone ($v_i(S)<v_i(T)$ when $S\subsetneq T$) and strict (different bundles have different values). Budgets are normalized, $b_1+b_2=1$; money has no value to the agents.

An allocation $\mathcal S=(\mathcal S_1,\mathcal S_2)$ is a partition of all items between the agents. Item prices $p_j\ge 0$ give bundle prices $p(S)=\sum_{j\in S}p_j$. Agent $i$ demands $S$ if $p(S)\le b_i$ and $p(T)>b_i$ for every bundle $T$ with $v_i(T)>v_i(S)$. A competitive equilibrium (CE) is a pair $(\mathcal S,p)$ in which each agent demands her own bundle. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent.

Agent $i$'s budget-proportional share is $b_i$ (her budget times $v_i(M)=1$). Her truncated share is the best value she gets in a PO allocation that gives her at most that share:

$$b_i^-=\max\{v_i(\mathcal S_i):\ \mathcal S\ \text{PO},\ v_i(\mathcal S_i)\le b_i\}.$$

The Lean development uses the same names: bundle σ i for $\mathcal S_i$, price, IsCE, IsPO, IsStandardValuation, GetsTruncatedShare.

Formalization targets

Goal: Theorem 7.1 (p. 17)

For every two-agent additive market there is $\epsilon>0$ such that every budget pair with

$$b_2<b_1\le b_2+\epsilon$$

admits a CE $(\mathcal S,p)$ in which $v_j(\mathcal S_j)\ge b_j^-$ for both agents. The goal fixes no value of $\epsilon$; it asserts only that one exists for each market.

Milestones

1. Proposition 4.1 (p. 10): for a PO allocation with non-empty bundles and budget-exhausting prices, CE is equivalent to a pairwise swap condition, Condition (1).
2. Lemma 4.3 (p. 11): a budget-exhausting combination pricing $p_j=\alpha v_1(\{j\})+\beta v_2(\{j\})$ ($\alpha,\beta\ge0$, $\max\{\alpha,\beta\}>0$) at a PO allocation is a CE.
3. Proposition 5.1 (p. 12): budget-proportional and anti-proportional PO allocations are supported in a CE.
4. Lemma 5.5 (p. 14): without budget-proportional or PO anti-proportional allocations, agent $i$'s augmented-share minimizer is agent $k$'s truncated-share maximizer.
5. Lemma 6.3 (p. 15): if the budgets avoid the finite exceptional set $R_i$ and the rectangle of allocations $T_i$ is empty, a CE with truncated shares exists.
6. Case 1 of the proof (p. 18): a CE at budgets $(\tfrac12,\tfrac12)$ remains a CE, after rescaling prices, when agent 1's budget is raised slightly.
7. $R_i$ avoidance (p. 19): almost equal but unequal budgets lie outside $R_i$.

Two companion statements are drafted without being milestones: Theorem 4.4 (second welfare theorem) and Theorem 5.2 (a budget-proportional allocation implies a CE).

Significance

The result. Theorem 7.1 shows that the non-existence of CEEI with indivisible goods is a measure-zero phenomenon for two additive agents: equal budgets are the only bad point near equality, and the equilibrium obtained is also fair in the truncated-share sense. It justifies tie-breaking by tiny budget differences in practice. It is the two-agent base case of the paper's main open question (§9.1, p. 20), whether generic almost-equal budgets guarantee a CE for more than two agents; the paper also leaves open two agents with arbitrary generic budgets and non-identical preferences (p. 21). For arbitrary, not almost-equal, budgets, Segal-Halevi (AAMAS 2018) shows that genericity does not guarantee existence for four additive agents.

Formalizing it. No machine-checked proof of any result of this paper is known. The paper's own argument for one case of the goal is incomplete: in Case 2(b) of the proof of Theorem 7.1 (p. 19) it asserts that the two candidate allocations are mirror images of each other and that the rectangles $T_1,T_2$ are empty. Both claims fail on an explicit three-item market. Theorem 7.1 itself held in every one of 6000 markets checked numerically during planning, including that one, where a CE with truncated shares exists at prices proportional to one agent's valuation. A formal proof therefore has to supply an argument the paper does not contain; the two false steps are not posed as milestones.

Difficulty

The milestones 1–5 are finite combinatorics on the Pareto frontier with sign bookkeeping. The difficulty sits in Case 2(b) of the goal: every allocation gives one agent more than $\tfrac12$ and the other less. The natural route, invoking Lemma 6.3, needs some $T_i$ to be empty, and in that case both can be non-empty. Lemma 6.3 does not cover it, and the paper's symmetry argument cannot be repaired by choosing $\epsilon$ smaller, since in the counterexample the two candidate allocations stay the same for every small $\epsilon$. A complete proof must show directly that one of the two "as fair as possible" allocations is supported by suitable prices.

Formalization scope

Items are Fin m and agents Fin 2; the paper's agents 1, 2 are indices 0, 1, so "$b_1>b_2$" reads b 1 < b 0. An allocation is a map σ : Fin m → Fin 2, which builds in that every item is allocated exactly once. All quantities are real numbers. Demand quantifies over every bundle, with strict inequality $p(T)>b_i$. Prices are non-negative by definition of a CE. The truncated share is a maximum over PO allocations only.

Two conventions are disclosed restrictions or additions:

1. Strictness without identical items. The paper allows identical items as the single exception to strict preferences (p. 6). Here each valuation is injective on bundles, so markets with identical items are excluded.
2. Rescaled prices in Case 1. The page says the perturbed CE uses unchanged prices; at normalized budgets the prices must be divided by $1+\epsilon$, and the milestone says so.

In the goal $\epsilon$ is chosen after the valuations and before the budgets. A formalization in which $\epsilon$ depends on the budgets, demand ranges over a restricted family of bundles, allocations need not allocate every item, prices may be negative, or the truncated share is a maximum over all allocations, would be a different and in several cases trivial statement; all of these are ruled out.

The definitions file GenericBudgets.AlmostEqual.Setting holds the market, CE, PO, the fairness notions, combination pricing, Condition (1), $T_i$ and $R_i$, and is reusable for any two-agent indivisible-goods market with budgets. Proofs of the milestones, a repaired argument for Case 2(b), and general $n$-agent versions of the CE and PO infrastructure are welcome.

Selected references

• M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150v2, https://doi.org/10.1287/moor.2020.1062
• H. R. Varian, Equity, envy, and efficiency, Journal of Economic Theory 9(1), 1974. https://doi.org/10.1016/0022-0531(74)90075-1
• E. Budish, The combinatorial assignment problem: approximate competitive equilibrium from equal incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• E. Segal-Halevi, Competitive equilibrium for almost all incomes, Proceedings of AAMAS 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212