Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

(A.1): ωˉiII(β∗/βi)+Ai=ωˉ0(β∗/βi)\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)ωˉiII​(β∗/βi​)+Ai​=ωˉ0​(β∗/βi​)

Proved
IncentivesInTeams.Conglomerate.appendix_A1

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

incentive-structuresp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1team-theory

Consider a conglomerate model whose component weights are probability weights, a joint strategy β∗\beta^*β∗, constants AiA_iAi​, a subunit iii and a strategy βi∈Bi\beta_i \in B_iβi​∈Bi​. Let WIIW^{II}WII be the incentive structure (3.5) built from β∗\beta^*β∗ and the constants AiA_iAi​. Then

ωˉiII(β∗/βi)+Ai=ωˉ0(β∗/βi),\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i),ωˉiII​(β∗/βi​)+Ai​=ωˉ0​(β∗/βi​),

where ωˉiII\bar\omega_i^{II}ωˉiII​ is the expected value of subunit iii's payoff under WIIW^{II}WII and ωˉ0\bar\omega_0ωˉ0​ is the expected organization payoff.

Up to the constant AiA_iAi​, a subunit's expected reward under WIIW^{II}WII equals the expected payoff of the whole organization, whatever strategy the subunit plays while the others follow β∗\beta^*β∗. This is the identity to which the paper reduces Theorem 1.

Preamble
import Mathlib
import Definitions.Def_IncentivesInTeams_Conglomerate_Model
Formal statement
namespace IncentivesInTeams.Conglomerate

theorem appendix_A1 {ι : 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) (A : ι → ℝ) (i : ι)
    (b : SubStrategy (S i) (Z i) (M₀ i) (M i) (D i)) (hb : b ∈ T.B i) :
    T.expect (T.WII βs A i (βs.update i b)) + A i = T.expOrgPayoff (βs.update i b) := by sorry

end IncentivesInTeams.Conglomerate
Source
Groves, Incentives in Teams, Econometrica 41(4), 1973, p. 629, Appendix, PROOF OF THEOREM 1, (A.1), and the two displays at the top of p. 630
Read-back

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

Setting. ι\iotaι is a finite set of subunits. S0S_0S0​ and each SkS_kSk​ are finite. The weights P0P_0P0​ and PkP_kPk​ are assumed to be probability weights (nonnegative, each summing to 111), with P(s)=P0(s0)∏kPk(sk)P(s)=P_0(s_0)\prod_kP_k(s_k)P(s)=P0​(s0​)∏k​Pk​(sk​) and E[X]=∑sP(s)X(s)\mathbb E[X]=\sum_sP(s)X(s)E[X]=∑s​P(s)X(s). The payoffs are v0:D0×S0→Rv_0:D_0\times S_0\to\mathbb Rv0​:D0​×S0​→R and vk:Dk×D0×Sk→Rv_k:D_k\times D_0\times S_k\to\mathbb Rvk​:Dk​×D0​×Sk​→R.

A joint strategy β\betaβ consists of:

  • head functions ζ0:S0→Z0\zeta_0:S_0\to Z_0ζ0​:S0​→Z0​, γ0k:Z0→M0k\gamma_0^k:Z_0\to M_{0k}γ0k​:Z0​→M0k​ and δ0:Z0×∏kMk→D0\delta_0:Z_0\times\prod_kM_k\to D_0δ0​:Z0​×∏k​Mk​→D0​;
  • subunit functions ζk:Sk→Zk\zeta_k:S_k\to Z_kζk​:Sk​→Zk​, γk:Zk×M0k→Mk\gamma_k:Z_k\times M_{0k}\to M_kγk​:Zk​×M0k​→Mk​ and δk:Zk×M0k→Dk\delta_k:Z_k\times M_{0k}\to D_kδk​:Zk​×M0k​→Dk​.

Its information maps are ykβ(s)=(ζk(sk),γ0k(ζ0(s0)))y_k^\beta(s)=(\zeta_k(s_k),\gamma_0^k(\zeta_0(s_0)))ykβ​(s)=(ζk​(sk​),γ0k​(ζ0​(s0​))) and y0β(s)=(ζ0(s0),(γk(ykβ(s)))k)y_0^\beta(s)=(\zeta_0(s_0),(\gamma_k(y_k^\beta(s)))_k)y0β​(s)=(ζ0​(s0​),(γk​(ykβ​(s)))k​). The payoff components are

ukβ(s)=vk(δk(ykβ(s)),δ0(y0β(s)),sk),u0β(s)=v0(δ0(y0β(s)),s0),u_k^\beta(s)=v_k(\delta_k(y_k^\beta(s)),\delta_0(y_0^\beta(s)),s_k),\qquad u_0^\beta(s)=v_0(\delta_0(y_0^\beta(s)),s_0),ukβ​(s)=vk​(δk​(ykβ​(s)),δ0​(y0β​(s)),sk​),u0β​(s)=v0​(δ0​(y0β​(s)),s0​),

and the expected organization payoff is

ωˉ0(β)=E[∑kukβ+u0β].\bar\omega_0(\beta)=\mathbb E\Big[\sum_ku_k^\beta+u_0^\beta\Big].ωˉ0​(β)=E[k∑​ukβ​+u0β​].

The functions built from β∗\beta^*β∗. Fix β∗\beta^*β∗ and real constants (Ak)k∈ι(A_k)_{k\in\iota}(Ak​)k∈ι​. For yˉ=(z0,m)\bar y=(z_0,m)yˉ​=(z0​,m):

  • the head factor is
H(yˉ)=cavg⁡P0({t:ζ0∗(t)=z0}, t↦v0(δ0∗(yˉ),t));H(\bar y)=\operatorname{cavg}_{P_0}\big(\{t:\zeta^*_0(t)=z_0\},\ t\mapsto v_0(\delta^*_0(\bar y),t)\big);H(yˉ​)=cavgP0​​({t:ζ0∗​(t)=z0​}, t↦v0​(δ0∗​(yˉ​),t));
  • for each jjj, the subunit factor is
Fj(yˉ)=cavg⁡Pj({t:γj∗(ζj∗(t),γ0j∗(z0))=mj}, t↦vj(δj∗(ζj∗(t),γ0j∗(z0)),δ0∗(yˉ),t)),F_j(\bar y)=\operatorname{cavg}_{P_j}\Big(\{t:\gamma^*_j(\zeta^*_j(t),\gamma_0^{j*}(z_0))=m_j\},\ t\mapsto v_j\big(\delta^*_j(\zeta^*_j(t),\gamma_0^{j*}(z_0)),\delta^*_0(\bar y),t\big)\Big),Fj​(yˉ​)=cavgPj​​({t:γj∗​(ζj∗​(t),γ0j∗​(z0​))=mj​}, t↦vj​(δj∗​(ζj∗​(t),γ0j∗​(z0​)),δ0∗​(yˉ​),t)),

where cavg⁡w(E,X)=∑EwX/∑Ew\operatorname{cavg}_w(E,X)=\sum_EwX/\sum_Ewcavgw​(E,X)=∑E​wX/∑E​w, with value 000 when the denominator is 000;

  • the incentive payoff is
WiII(β,s)=uiβ(s)+H(y0β(s))+∑j≠iFj(y0β(s))−Ai.W^{II}_i(\beta,s)=u_i^\beta(s)+H(y_0^\beta(s))+\sum_{j\ne i}F_j(y_0^\beta(s))-A_i.WiII​(β,s)=uiβ​(s)+H(y0β​(s))+j=i∑​Fj​(y0β​(s))−Ai​.

Theorem. Take a joint strategy β∗\beta^*β∗, constants AAA, a subunit iii, and a subunit-iii strategy b∈Bib\in B_ib∈Bi​. Let β∗/b\beta^*/bβ∗/b be β∗\beta^*β∗ with subunit iii's strategy replaced by bbb. Then

E[WiII(β∗/b,⋅)]+Ai=ωˉ0(β∗/b).\mathbb E\big[W^{II}_i(\beta^*/b,\cdot)\big]+A_i=\bar\omega_0(\beta^*/b).E[WiII​(β∗/b,⋅)]+Ai​=ωˉ0​(β∗/b).

β∗\beta^*β∗ is not required to lie in any strategy set, and no positivity of any conditioning event is assumed.

Degenerate cases.

  • The weight hypothesis forces every state set to be nonempty.
  • Wherever a conditioning event has weight 000, the corresponding HHH or FjF_jFj​ takes the value 000.
  • If ι={i}\iota=\{i\}ι={i}, the sum over j≠ij\ne ij=i is empty. The claim then reads E[uiβ∗/b+H(y0β∗/b)−Ai]+Ai=ωˉ0(β∗/b)\mathbb E[u_i^{\beta^*/b}+H(y_0^{\beta^*/b})-A_i]+A_i=\bar\omega_0(\beta^*/b)E[uiβ∗/b​+H(y0β∗/b​)−Ai​]+Ai​=ωˉ0​(β∗/b).
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me