Lemma 1 — an intermediate face between $C_S$ and $C_T$

Proved

CoresConvexGames.Stability.exists_intermediate_face

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$ . Write $S\subset\subset T$ if $S\subsetneq T$ and $|T|-|S|\ge 2$ . Suppose the core configuration $\{C_S\}$ is regular.

If $S\subset\subset T$ and $a\in C_S\cap C_T$ , then for any two distinct preassigned players $j,k\in T\setminus S$ there exist a coalition $Q$ and a payoff vector $b$ with

S\subsetneq Q\subsetneq T,\qquad b\in C_S\cap C_Q\cap C_T,\qquad b_i=a_i\ (i\in S),\qquad j\in Q,\ k\notin Q .

The lemma inserts an intermediate coalition between two nested coalitions whose faces meet; it is the step that lets chains of coalitions be refined one player at a time.

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. The hypothesis $j\ne k$ is implicit in the page's "two preassigned elements" (for $j=k$ the conclusion $j\in Q$ , $k\notin Q$ is impossible). The standing game assumption $v(\emptyset)=0$ is a hypothesis.

Preamble

import Mathlib
import Definitions.Def_CoresConvexGames_Stability_CoreFace
import Definitions.Def_CoresConvexGames_Stability_IsRegularConfiguration

Formal statement

namespace CoresConvexGames.Stability

/-- Shapley (1971), p. 18, Lemma 1 (with its "Moreover" clause). `S ⊂⊂ T` is
`S ⊂ T ∧ S.card + 2 ≤ T.card`; the two preassigned elements `j, k` of `T − S` are distinct. -/
theorem exists_intermediate_face {n : ℕ} (f : Finset (Fin n) → ℝ) (hf0 : f ∅ = 0)
    (hreg : IsRegularConfiguration f) (S T : Finset (Fin n)) (hST : S ⊂ T)
    (hcard : S.card + 2 ≤ T.card) (a : Fin n → ℝ) (ha : a ∈ CoreFace f S ∩ CoreFace f T)
    (j k : Fin n) (hj : j ∈ T \ S) (hk : k ∈ T \ S) (hjk : j ≠ k) :
    ∃ (Q : Finset (Fin n)) (b : Fin n → ℝ), S ⊂ Q ∧ Q ⊂ T ∧
      b ∈ CoreFace f S ∩ CoreFace f Q ∩ CoreFace f T ∧
      (∀ i ∈ S, b i = a i) ∧ j ∈ Q ∧ k ∉ Q := 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, Lemma 1 (including the "Moreover" clause)

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.
$S, T \subseteq N$ satisfy $S \subsetneq T$ and $|S| + 2 \le |T|$ .
$a \in C_S \cap C_T$ .
$j, k \in T \setminus S$ with $j \neq k$ .

Conclusion. There exist a coalition $Q$ and a vector $b \in \mathbb{R}^n$ such that:

S \subsetneq Q \subsetneq T, \qquad b \in C_S \cap C_Q \cap C_T, \qquad b_i = a_i \ \ \forall i \in S, \qquad j \in Q, \qquad k \notin Q.

Nothing is asserted about $b_i$ for $i \notin S$ .

Degenerate cases:

$n \le 1$ : two distinct $j, k$ cannot exist, so the hypotheses are unsatisfiable and the statement holds vacuously.
$S = \emptyset$ : this is allowed. Then $C_S$ is the whole core and the agreement condition $b_i = a_i$ is vacuous.
$T = N$ : this is allowed.

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

Lemma 1 — an intermediate face between CSC_SCS​ and CTC_TCT​

Lemma 1 — an intermediate face between $C_S$ and $C_T$