THEOREM 1 (Groves 1973): $W^{II}$ is an optimal incentive structure in the class $\mathscr{J}$

Proved

IncentivesInTeams.Conglomerate.own_profit_optimal

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

incentive-structuresmechanism-designp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1team-theory

Consider a conglomerate organization (Conditions S.1–S.5) with finitely many subunits, finite component state spaces carrying probability weights, independent components (product law), arbitrary strategy sets $B_0$ , $B_i$ , and payoff components $v_0$ , $v_i$ . Let $\beta^*$ be a joint strategy satisfying Assumption A, and let $A_i$ be arbitrary constants. Let $W^{II}$ be the incentive structure (3.5),

\omega_i^{II}(\beta, s) = v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + C_i^{II}(y_0(s)),

with $C_i^{II}$ the head's conditional expectation, under $\beta^*$ and given his information $y_0$ , of all payoff components other than subunit $i$ 's, minus $A_i$ (3.3). Then $W^{II}$ belongs to the class $\mathscr{J}$ of (3.2), and it is optimal: for every subunit $i$ and every $\beta_i \in B_i$ ,

\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*),

with strict inequality whenever $\beta_i$ is not equivalent to $\beta_i^*$ .

In words: rewarding each subunit with its own profit plus the head's expectation of everybody else's profit makes truthful reporting and the team-optimal decision rule the unique best reply of each subunit manager, using only information the head already has.

Formalization Note. Finite component state spaces, the one-exchange message protocol of §4.A, fixed message and observation codomains, and the factorized form of the conditional expectation in (3.3) are the conventions of the model file. The factorized form agrees with the literal (3.3) wherever the latter is defined; the literal quotient, which is $0$ on null conditioning events, would make the theorem false as soon as a subunit can send a message $\gamma_i^*$ never sends. Equivalence of strategies is the paper's footnote 5, over all $\beta \in B$ .

Preamble

import Mathlib
import Definitions.Def_IncentivesInTeams_Conglomerate_Model

Formal statement

namespace IncentivesInTeams.Conglomerate

theorem own_profit_optimal {ι : Type*} [Fintype ι] [DecidableEq ι] {S₀ : Type*} [Fintype S₀] {S : ι → Type*}
    [∀ i, Fintype (S i)] {Z₀ : Type*} {Z M₀ M : ι → Type*} {D₀ : Type*} {D : ι → Type*}
    (T : Model S₀ S Z₀ Z M₀ M D₀ D) (hT : T.WeightsOK)
    (βs : JointStrategy S₀ S Z₀ Z M₀ M D₀ D) (hA : T.AssumptionA βs) (A : ι → ℝ) :
    T.InClassJ (T.WII βs A) ∧ T.IsOptimal (T.WII βs A) βs := by sorry

end IncentivesInTeams.Conglomerate

Source

Groves, Incentives in Teams, Econometrica 41(4), 1973, p. 625, §3.B, THEOREM 1 (proof: Appendix, pp. 629–630)

Read-back

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

The theorem concerns a model $T$ built on a family of type parameters. It also involves a joint strategy $\beta$ and a vector of real numbers $A = (A_i)_{i \in \iota}$ . The notions it uses are "model", "joint strategy", "weights OK", "Assumption A", "WII", "class $J$ " and "optimal". They all come from the imported bundle Definitions.Def_IncentivesInTeams_Conglomerate_Model in the namespace IncentivesInTeams.Conglomerate. That file is not included in the code given to this auditor, so none of them can be unfolded here. Each is treated below as an opaque predicate or construction, and its content is left undetermined.

Parameters and their assumptions.

$\iota$ is an index type. It is assumed to be finite and to have decidable equality, and nothing else.
$S_0$ is a finite type.
$S = (S_i)_{i\in\iota}$ is a family of types, each $S_i$ finite.
$Z_0$ is a type and $D_0$ is a type. No finiteness or other structure is assumed for either.
$Z = (Z_i)_{i\in\iota}$ $Z = (Z_{i})_{i \in ι}$ , $M_0 = (M_{0,i})_{i\in\iota}$ $M_{0} = (M_{0, i})_{i \in ι}$ , $M = (M_i)_{i\in\iota}$ $M = (M_{i})_{i \in ι}$ and $D = (D_i)_{i\in\iota}$ $D = (D_{i})_{i \in ι}$ are families of types indexed by $\iota$ $ι$ . No finiteness or other structure is assumed for them.
- Note that the code declares $M_0$ as a family indexed by $\iota$ , like $Z$ , $M$ and $D$ . It is not a single type like $S_0$ , $Z_0$ and $D_0$ .
$T$ is a model over these parameters. The code writes this as Model $S_0\, S\, Z_0\, Z\, M_0\, M\, D_0\, D$ .
$h_T$ is a hypothesis that $T$ satisfies the bundle's predicate "weights OK".
$\beta$ is a joint strategy over the same eight parameters.
$h_A$ is a hypothesis that $T$ and $\beta$ together satisfy the bundle's predicate "Assumption A".
$A = (A_i)_{i\in\iota}$ is an arbitrary vector of real numbers, one per index. It has no sign, bound or normalisation constraint.

Conclusion. Write $W^{II}_T(\beta, A)$ for the object the bundle's construction "WII" produces from $T$ , $\beta$ and $A$ . The theorem asserts the conjunction of two claims:

W^{II}_T(\beta, A) \in J_T \qquad\text{and}\qquad W^{II}_T(\beta, A) \text{ is optimal for } \beta \text{ in } T.

The first claim says that $W^{II}_T(\beta, A)$ satisfies $T$ 's predicate "in class $J$ ".
The second says that $W^{II}_T(\beta, A)$ and $\beta$ together satisfy $T$ 's predicate "is optimal".

Both claims are stated for every real vector $A$ , and in the same form for every $A$ . The only other inputs are $T$ and $\beta$ , and the only hypotheses are $h_T$ and $h_A$ ; neither hypothesis mentions $A$ . What "optimal" means, and over which alternatives it is measured, cannot be read off this code.

Degenerate cases. Nothing in the statement rules out the following:

$\iota$ empty. Then every family is empty, and $A$ is the unique empty real vector.
$\iota$ with one element.
$S_0$ empty, or some $S_i$ empty.
$Z_0$ , $D_0$ or any $Z_i$ , $M_{0,i}$ , $M_i$ , $D_i$ empty or infinite.
$A$ equal to the zero vector, or with negative or arbitrarily large entries.

The statement itself contains no division, natural-number subtraction, integral, supremum or extended-real arithmetic. Any such operation, and any default value it returns, would sit inside the unseen definitions. So would the answers to three further questions, which cannot be settled from the code provided:

whether "weights OK" or "Assumption A" can be satisfied at all, and so whether the theorem could hold vacuously;
whether these hypotheses hold automatically, or fail, when $\iota$ or $S_0$ is empty;
what "WII", "class $J$ " and "optimal" reduce to in those cases.

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

THEOREM 1 (Groves 1973): WIIW^{II}WII is an optimal incentive structure in the class J\mathscr{J}J

THEOREM 1 (Groves 1973): $W^{II}$ is an optimal incentive structure in the class $\mathscr{J}$