Theorem 2 — faces along an increasing chain meet; regular implies complete

Proved

CoresConvexGames.Stability.chain_faces_inter_nonempty

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

cooperative-gamecorep2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $N=\{1,\dots,n\}$ be a finite set of players and $v:2^N\to\mathbb R$ a game, i.e. a set function with $v(\emptyset)=0$ . For a payoff vector $a\in\mathbb R^N$ and a coalition $S\subseteq N$ write $a(S)=\sum_{i\in S}a_i$ . The core $C$ is the set of payoff vectors $a$ with $a(N)=v(N)$ and $a(S)\ge v(S)$ for all $S\subseteq N$ ; for $\emptyset\ne S\subseteq N$ the face $C_S$ is $\{a\in C: a(S)=v(S)\}$ , and $C_\emptyset=C$ . Suppose the core configuration $\{C_S\}$ is regular. Then for any strictly increasing sequence of coalitions $S_1\subsetneq S_2\subsetneq\cdots\subsetneq S_m$ ( $m\ge1$ ),

C_{S_1}\cap C_{S_2}\cap\cdots\cap C_{S_m}\ne\emptyset .

In particular (take $m=1$ ), a regular core configuration is complete: every face $C_S$ is nonempty.

This is the basic geometric consequence of regularity. It is what places the marginal vectors in the core and supplies the core points on prescribed hyperplanes used in the proofs of Theorems 3, 5 and 8.

Formalization Note Players are Fin n (a relabelling of Shapley's arbitrary finite $N$ ), a game is f : Finset (Fin n) → ℝ, and the core is the published Supermodularity.Cooperative.Core Finset.univ f. A sequence of length $m\ge1$ is a map Fin (m + 1) → Finset (Fin n), and "increasing" is StrictMono (strict inclusion). The "in particular" clause is stated as a second conjunct. The standing game assumption $v(\emptyset)=0$ is a hypothesis.

Preamble

import Mathlib
import Definitions.Def_CoresConvexGames_Stability_CoreFace
import Definitions.Def_CoresConvexGames_Stability_IsCompleteConfiguration
import Definitions.Def_CoresConvexGames_Stability_IsRegularConfiguration

Formal statement

namespace CoresConvexGames.Stability

/-- Shapley (1971), p. 18, Theorem 2: in a regular core configuration, the faces along any
strictly increasing sequence `S_1 ⊂ S_2 ⊂ ⋯ ⊂ S_m` (`m ≥ 1`) of coalitions have a common
point; in particular (`m = 1`) a regular core configuration is complete. -/
theorem chain_faces_inter_nonempty {n : ℕ} (f : Finset (Fin n) → ℝ) (hf0 : f ∅ = 0)
    (hreg : IsRegularConfiguration f) :
    (∀ (m : ℕ) (S : Fin (m + 1) → Finset (Fin n)), StrictMono S →
      (⋂ k, CoreFace f (S k)).Nonempty) ∧
    IsCompleteConfiguration f := by sorry

end CoresConvexGames.Stability

Source

Shapley, Cores of Convex Games, Int. J. Game Theory 1, 1971, https://doi.org/10.1007/BF01753431, p. 18, §3.2, Theorem 2, equation (15)

Read-back

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

Fix $n \in \mathbb{N}$ , $N = \{0, \dots, n-1\}$ and a game $f$ (real-valued on subsets of $N$ ). For $S \subseteq N$ , let $C_S$ be the set of $x \in \mathbb{R}^n$ such that:

$x \in \operatorname{Core}(N, f)$ , an external definition whose body is not shown; and
if $S \neq \emptyset$ , then $\sum_{i \in S} x_i = f(S)$ .

The configuration is regular when $C_N \neq \emptyset$ and $C_S \cap C_T \subseteq C_{S \cup T} \cap C_{S \cap T}$ for all $S, T \subseteq N$ .

Hypotheses.

$f(\emptyset) = 0$ .
The configuration of $f$ is regular.

Conclusion. Both of the following hold.

For every $m \in \mathbb{N}$ and every sequence of $m+1$ coalitions that is strictly increasing under inclusion,

S_0 \subsetneq S_1 \subsetneq \dots \subsetneq S_m \subseteq N,

the faces have a common point:

\bigcap_{k=0}^{m} C_{S_k} \neq \emptyset.

The configuration is complete: $C_S \neq \emptyset$ for every $S \subseteq N$ , including $S = \emptyset$ .

A strictly increasing sequence can have at most $n+1$ terms, so for large $m$ part 1 is vacuous. The chain may start at $S_0 = \emptyset$ , whose face is the whole core.

Degenerate cases: for $m = 0$ , part 1 says that each single face $C_{S_0}$ is nonempty. When $n = 0$ the only coalition is $\emptyset$ , and both parts reduce to $\operatorname{Core}(\emptyset, f) \neq \emptyset$ . That is already part of the regularity hypothesis, since $C_N = C_\emptyset$ when $n = 0$ .

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