Sec. 3.3, proof of the Lemma — core payoffs are tight on an optimal assignment and zero off it

Proved

AssignmentGame.CoreCorners.core_tight_on_optimal_matching

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

assignment-gamecooperative-gamesp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ (sellers) and $N$ (buyers) be finite sets and $a_{ij} \ge 0$ . Let $P \subseteq M \times N$ be an optimal assignment: a matching (no seller and no buyer in two pairs of $P$ ) whose total gain equals the worth of the all-player coalition,

\sum_{(i,j) \in P} a_{ij} = \operatorname{worth}(M, N).

Then every core vector $(u, v)$ satisfies

$u_i + v_j = a_{ij}$ for every pair $(i, j) \in P$ ;
$u_i = 0$ for every seller $i$ not assigned by $P$ ;
$v_j = 0$ for every buyer $j$ not assigned by $P$ .

This is the step of the proof of the Lemma (p. 121) where, after labelling the optimal assignment as $11, 22, \dots, kk$ , the authors use $u_i = a_{ii} - v_i$ for $i \le k$ and $u_i = v_j = 0$ for $i, j > k$ . It is what turns the lattice operations of the Lemma into core vectors that exhaust $\operatorname{worth}(M, N)$ .

Preamble

import Mathlib
import Definitions.Def_AssignmentGame_CoreCorners_Game

open Finset

Formal statement

namespace AssignmentGame.CoreCorners

/-- Sec. 3.3, proof of the Lemma, p. 121: on an optimal assignment `P` every core vector splits
each `a i j`, `(i, j) ∈ P`, exactly between the two partners, and pays zero to every player not
assigned by `P`. -/
theorem core_tight_on_optimal_matching {M N : Type*} [Fintype M] [Fintype N]
    (a : M → N → ℝ) (ha : ∀ i j, 0 ≤ a i j)
    (P : Finset (M × N)) (hP : IsMatching Finset.univ Finset.univ P)
    (hopt : ∑ p ∈ P, a p.1 p.2 = worth a Finset.univ Finset.univ)
    (u : M → ℝ) (v : N → ℝ) (huv : (u, v) ∈ core a) :
    (∀ p ∈ P, u p.1 + v p.2 = a p.1 p.2) ∧
    (∀ i : M, (∀ p ∈ P, p.1 ≠ i) → u i = 0) ∧
    (∀ j : N, (∀ p ∈ P, p.2 ≠ j) → v j = 0) := by sorry

end AssignmentGame.CoreCorners

Source

Shapley and Shubik, The Assignment Game I: The Core, Int. J. Game Theory 1 (1971), p. 121, Sec. 3.3, proof of the Lemma

Read-back

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

This theorem takes the following data:

arbitrary finite types $M$ (sellers) and $N$ (buyers);
a real matrix $a$ with $a_{ij} \ge 0$ for all $i, j$ ;
a finite set $P \subseteq M \times N$ that is a matching in the full player sets, meaning no seller and no buyer appears in two distinct pairs, though not everyone has to be matched;
the optimality condition

\sum_{(i,j)\in P} a_{ij} = w_a(M,N),

where $w_a(M,N)$ is the largest such sum over all partial matchings in $M \times N$ , with the empty matching allowed;

a pair $(u,v)$ with $u : M \to \mathbb{R}$ and $v : N \to \mathbb{R}$ that lies in $\mathrm{Core}(a)$ .

Membership in the core means both of the following:

\sum_i u_i + \sum_j v_j = w_a(M,N)

and

\sum_{i\in A} u_i + \sum_{j\in B} v_j \ge w_a(A,B) \ \text{ for all } A\subseteq M,\ B\subseteq N,

where $w_a(A,B)$ is the maximal matching value using only sellers in $A$ and buyers in $B$ .

The conclusion is the conjunction of three statements:

$u_i + v_j = a_{ij}$ for every $(i,j) \in P$ .
$u_i = 0$ for every seller $i$ that appears in no pair of $P$ .
$v_j = 0$ for every buyer $j$ that appears in no pair of $P$ .

Degenerate cases:

$M$ empty. $P$ must be empty, so part 1 is vacuous and part 3 says $v \equiv 0$ . The symmetric statement holds when $N$ is empty.
Zero-valued pairs in $P$ . $P$ may contain a pair with $a_{ij} = 0$ . Part 1 then forces $u_i + v_j = 0$ for that pair.
Empty $P$ . $P = \varnothing$ is allowed whenever $w_a(M,N) = 0$ , for example when $a \equiv 0$ . The theorem then asserts that every core vector is identically zero.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph