Proof of Theorem 1: the core of $w$ is $\{(0,1,2,7,1)\}$

Proved

MonotonicSolutions.CoreRules.core_youngW

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

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

Let $w$ be the five-player game of the proof of Theorem 1: with $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\}$ , $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$ if $S$ contains no $S_k$ ) otherwise.

Then the core of $w$ , the set of $x \in \mathbb{R}^5$ with $\sum_{i \in S} x_i \ge w(S)$ for all $S$ and $\sum_{i \in N} x_i = w(N)$ , consists of exactly one point:

C(w) = \{\bar x\}, \qquad \bar x = (0, 1, 2, 7, 1).

Formalization Note The core is the published Supermodularity.Cooperative.Core Finset.univ, and the paper's player $k$ is the Lean index $k-1$ , so $\bar x$ is ![0, 1, 2, 7, 1] in the same order.

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_youngW :
    Supermodularity.Cooperative.Core Finset.univ youngW.1 = {![0, 1, 2, 7, 1]} := 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 core of w is x̄ = (0, 1, 2, 7, 1))

Read-back

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

The game $w$ 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:

$w(N) = 11$ ;
for any other $S$ , $w(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,9)$ ;
$w(S) = 0$ if $S$ contains no $C_k$ .

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

\operatorname{Core}(N, w) = \{(0,\,1,\,2,\,7,\,1)\}.

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 $x \in \mathbb{R}^5$ with $\sum_i x_i = w(N)$ and $w(S) \le \sum_{i \in S} x_i$ for all $S$ . The exact meaning of this statement depends on that unseen code.

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 www is {(0,1,2,7,1)}\{(0,1,2,7,1)\}{(0,1,2,7,1)}

Proof of Theorem 1: the core of $w$ is $\{(0,1,2,7,1)\}$