Proof of Theorem 1: the core of $v$ is $\{(3,0,0,6,3)\}$

Proved

MonotonicSolutions.CoreRules.core_youngV

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

cooperative-gamescorecounterexamplep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $v$ be the five-player game of the proof of Theorem 1: identical to the game $w$ (defined from $S_1 = \{3,5\}$ , $S_2 = \{1,2,3\}$ , $S_3 = \{1,3,4\}$ , $S_4 = \{2,4,5\}$ , $S_5 = \{1,2,4,5\}$ with $w(S_1)=w(S_2)=3$ , $w(S_3)=w(S_4)=w(S_5)=9$ , $w(N)=11$ , and $w(S) = \max_{S_k\subseteq S} w(S_k)$ or $0$ otherwise), except that $v(S_5) = v(N) = 12$ .

Then the core of $v$ consists of exactly one point:

C(v) = \{\bar{\bar x}\}, \qquad \bar{\bar x} = (3, 0, 0, 6, 3).

Compared with the core point $(0,1,2,7,1)$ of $w$ , players 2 and 4 receive less, although every coalition containing them has weakly increased in value.

Formalization Note The core is the published Supermodularity.Cooperative.Core Finset.univ; $\bar{\bar x}$ is ![3, 0, 0, 6, 3] (paper's player $k$ = Lean index $k-1$ ).

Preamble

import Mathlib
import Definitions.Def_Supermodularity_Cooperative_Core
import Definitions.Def_MonotonicSolutions_CoreRules_Game
import Definitions.Def_MonotonicSolutions_CoreRules_YoungGames

Formal statement

namespace MonotonicSolutions.CoreRules

theorem core_youngV :
    Supermodularity.Cooperative.Core Finset.univ youngV.1 = {![3, 0, 0, 6, 3]} := by sorry

end MonotonicSolutions.CoreRules

Source

Young, Monotonic Solutions of Cooperative Games, Int. J. Game Theory 14 (1985), p. 69, proof of Theorem 1 (the unique core element of v is (3, 0, 0, 6, 3))

Read-back

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

The game $v$ has players $0, \dots, 4$ and is defined from $C_0 = \{2,4\}$ , $C_1 = \{0,1,2\}$ , $C_2 = \{0,2,3\}$ , $C_3 = \{1,3,4\}$ , $C_4 = \{0,1,3,4\}$ as follows:

$v(N) = 12$ ;
for any other $S$ , $v(S)$ is the maximum of $\mathrm{val}_k$ over the $C_k \subseteq S$ , where $(\mathrm{val}_0, \dots, \mathrm{val}_4) = (3,3,9,9,12)$ ;
$v(S) = 0$ if $S$ contains no $C_k$ .

The statement asserts that the core of $v$ is exactly one point:

\operatorname{Core}(N, v) = \{(3,\,0,\,0,\,6,\,3)\}.

The coordinates are listed for players $0, 1, 2, 3, 4$ . The core is an imported definition whose code was not provided. Its description elsewhere in the chapter is the set of efficient vectors $x$ with $v(S) \le \sum_{i \in S} x_i$ for every coalition $S$ .

Degenerate cases. The statement is about one concrete game. There are no parameters, so no degenerate cases arise.

Human review

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

View graph

Proof of Theorem 1: the core of vvv is {(3,0,0,6,3)}\{(3,0,0,6,3)\}{(3,0,0,6,3)}

Proof of Theorem 1: the core of $v$ is $\{(3,0,0,6,3)\}$