Market-clearing prices exist in the linear 0/1 market

Proved

AGT.market_clearing_existence

by Shuze Chen · Aug 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algorithmic-game-theorygame-theorynash-equilibrium

Market-clearing prices exist in the linear market with 0/1 utilities. The market (§1.8.1 of Algorithmic Game Theory): a finite set $A$ of divisible goods, good $a$ available in $s_a \ge 1$ units; a finite set $B$ of buyers, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set $\Gamma_j \subseteq A$ of goods; every good interests at least one buyer; a buyer values any goods from her interest set equally and everything else not at all. Then there are prices $p_a > 0$ and spending amounts $x_{ja} \ge 0$ (money spent by buyer $j$ on good $a$ ) such that

$x_{ja} \ne 0$ only when $a \in \Gamma_j$ and $p_a = \min_{b \in \Gamma_j} p_b$ — each buyer spends only on cheapest goods in her interest set, an optimal bundle for 0/1 utilities;
$\sum_a x_{ja} = m_j$ for every buyer $j$ — budgets are exactly exhausted;
$\sum_j x_{ja} = p_a \, s_a$ for every good $a$ — every good sells out exactly.

This is the existence content of Theorem 1.17 of the book.

A note on the rendering. The book's Theorem 1.17 asserts that the ascending tight-set algorithm of §1.8.1 (via Lemmas 1.15–1.16 and max-flow) computes such prices in polynomial time; the running-time half is a statement about an algorithm and has no formal counterpart here, so this milestone is the existence content. Allocations are recorded as money spent rather than quantity, so the clearing condition is a product, not a quotient — no division by prices occurs anywhere in the statement.

Preamble

import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.BigOperators

Formal statement

namespace AGT

/-- **Theorem 1.17 of *Algorithmic Game Theory* (existence form)**.  The
market of §1.8.1: finitely many divisible goods `A`, good `a` available in
`supply a` units; finitely many buyers `B`, buyer `j` bringing `money j` and
interested in the goods `interest j`.  Utilities are linear 0/1: a buyer
only values (any amount of) the goods she is interested in.

Conclusion: market-clearing prices and an allocation exist.  `spend j a` is
the money buyer `j` spends on good `a`; each buyer spends her entire budget,
spends it only on interested goods of minimum price among her interest set
(an optimal bundle for 0/1 utilities), and every good sells out exactly —
total spending on `a` equals `price a * supply a`.

The book proves this by the iterated tight-set/max-flow algorithm
(Lemmas 1.15–1.16) and additionally shows polynomial running time; the
algorithmic half has no formal counterpart here.  Hypotheses: every buyer is
interested in at least one good and every good interests at least one buyer,
exactly the standing assumptions of §1.8.1; positive supplies and budgets
rule out degenerate zero prices. -/
theorem market_clearing_existence {A B : Type*} [Fintype A] [Fintype B]
    (supply : A → ℕ) (hsupply : ∀ a, 0 < supply a)
    (money : B → ℝ) (hmoney : ∀ j, 0 < money j)
    (interest : B → Finset A) (hbuyer : ∀ j, (interest j).Nonempty)
    (hgood : ∀ a : A, ∃ j : B, a ∈ interest j) :
    ∃ (price : A → ℝ) (spend : B → A → ℝ),
      (∀ a, 0 < price a) ∧
      (∀ j a, 0 ≤ spend j a) ∧
      (∀ j a, spend j a ≠ 0 →
        a ∈ interest j ∧ ∀ b ∈ interest j, price a ≤ price b) ∧
      (∀ j, ∑ a, spend j a = money j) ∧
      (∀ a, ∑ j, spend j a = price a * (supply a : ℝ)) := by
  sorry

end AGT

Source

N. Nisan, T. Roughgarden, E. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press 2007, https://doi.org/10.1017/CBO9780511800481, Section 1.8.1, Lemmas 1.15-1.16 and Theorem 1.17, pp. 22-26 (existence form)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `AGT.market_clearing_existence`

Let $A$ and $B$ be arbitrary finite types (of "goods" and "buyers", say, though the statement itself only calls them $A$ and $B$ ). Neither is assumed nonempty by a typeclass; nonemptiness is constrained only indirectly by the hypotheses below.

The theorem takes as given:

a function $\mathrm{supply} : A \to \mathbb{N}$ with $\mathrm{supply}(a) > 0$ for every $a \in A$ (supplies are natural numbers, so in particular $\mathrm{supply}(a) \ge 1$ );
a function $\mathrm{money} : B \to \mathbb{R}$ with $\mathrm{money}(j) > 0$ for every $j \in B$ ;
a function $\mathrm{interest} : B \to \mathcal{P}_{\mathrm{fin}}(A)$ $interest : B \to P_{fin} (A)$ assigning to each $j \in B$ $j \in B$ a finite subset $\mathrm{interest}(j) \subseteq A$ $interest (j) \subseteq A$ , with two hypotheses:
- for every $j \in B$ , the set $\mathrm{interest}(j)$ is nonempty;
- for every $a \in A$ , there exists some $j \in B$ with $a \in \mathrm{interest}(j)$ .

It asserts the existence (not uniqueness) of a pair of functions $\mathrm{price} : A \to \mathbb{R}$ and $\mathrm{spend} : B \times A \to \mathbb{R}$ satisfying the conjunction of the following five conditions:

Positive prices. For every $a \in A$ :

\mathrm{price}(a) > 0.

Nonnegative spending, on all pairs. For every $j \in B$ and every $a \in A$ — not only pairs with $a \in \mathrm{interest}(j)$ :

\mathrm{spend}(j, a) \ge 0.

Nonzero spending only on cheapest interesting goods. For every $j \in B$ and every $a \in A$ : if $\mathrm{spend}(j, a) \ne 0$ , then both

a \in \mathrm{interest}(j) \qquad\text{and}\qquad \forall\, b \in \mathrm{interest}(j),\ \mathrm{price}(a) \le \mathrm{price}(b).

Here the inner quantifier ranges over the goods $b$ in buyer $j$ 's own interest set only; the condition says $a$ has weakly minimal price within $\mathrm{interest}(j)$ , with a non-strict inequality $\le$ . This is a one-directional implication: nothing forces a buyer to spend anything on a cheapest interesting good, and nothing is claimed for pairs with $\mathrm{spend}(j, a) = 0$ . By contraposition it does force $\mathrm{spend}(j, a) = 0$ whenever $a \notin \mathrm{interest}(j)$ .

Budgets exactly exhausted. For every $j \in B$ , summing over all goods $a \in A$ (the whole type, not just $\mathrm{interest}(j)$ ):

\sum_{a \in A} \mathrm{spend}(j, a) = \mathrm{money}(j),

an exact equality — each buyer spends their entire money.

Exact market clearing. For every $a \in A$ , summing over all buyers $j \in B$ :

\sum_{j \in B} \mathrm{spend}(j, a) = \mathrm{price}(a) \cdot \mathrm{supply}(a),

an exact equality, where $\mathrm{supply}(a)$ is the natural number cast into $\mathbb{R}$ .

Degenerate cases the hypotheses allow. The hypotheses jointly force $A$ to be empty if and only if $B$ is empty: if $A$ is empty then each $\mathrm{interest}(j)$ would be an empty subset, contradicting its required nonemptiness unless $B$ is also empty; if $B$ is empty then no good can lie in any buyer's interest set, so $A$ must be empty. When both $A$ and $B$ are empty, every hypothesis and every one of the five conditions holds vacuously (the sums in conditions 4 and 5 are over empty index sets), and the theorem's conclusion is trivially witnessed by the empty functions. When both are nonempty, condition 4 with $\mathrm{money}(j) > 0$ forces each buyer to have some $a$ with $\mathrm{spend}(j, a) > 0$ , but no condition bounds how many buyers may spend on the same good or requires any good's supply to be "sold" to a particular buyer — allocation of goods is not mentioned at all; only real-valued spending and prices appear.

The declaration's proof is sorry (left unproved); this read-back describes the statement only.

Human review

Endorsed by Community (Bot) · Aug 27, 2026
Endorsed by Shuze Chen · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Market-clearing prices exist in the linear 0/1 market

Read-back: AGT.market_clearing_existence

Read-back: `AGT.market_clearing_existence`