Public Goods Dominance-Welfare Contrast

Abstract

Private noncontribution dominance contrasts with maximal unanimous-contribution welfare.

Theorem 1.1 (Private incentives and social welfare point in opposite directions).

$$\forall n\in Nat,b\in Real,c\in Real,\left(2\le n\wedge \left(c<b\wedge \frac{b}{n}<c\right)\right)\Rightarrow \mathrm{let}u\left(i,a\right):=\frac{b}{n}\times \mathrm{sum}\left(j,\mathrm{Fin}\left(n\right),\mathrm{level}\left(a_j\right)\right)-c\times \mathrm{level}\left(a_i\right);\mathrm{let}W\left(a\right):=\mathrm{sum}\left(i,\mathrm{Fin}\left(n\right),u\left(i,a\right)\right);\left(\forall i\in \mathrm{Fin}\left(n\right),a\in \mathrm{Fin}\left(n\right)\to Bool,u\left(i,\mathrm{update}\left(a,i,1\right)\right)<u\left(i,\mathrm{update}\left(a,i,0\right)\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(n\right)\to Bool,W\left(a\right)=(b-c)\times \mathrm{sum}\left(j,\mathrm{Fin}\left(n\right),\mathrm{level}\left(a_j\right)\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(n\right)\to Bool,W\left(a\right)\le W\left(\mathrm{const}\left(1\right)\right)\right)\wedge W\left(\mathrm{const}\left(0\right)\right)<W\left(\mathrm{const}\left(1\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValueScale/PublicGoodsDominanceWelfareContrast.public_goods_dominance_welfare_contrast (✓ std3). ∎

Source. Repository-derived.

Commentary.

The imported contribution level, aggregate, and zero-compensation utility construct the source payoff. Changing one agent’s action to contribution changes that payoff by b/n-c, independently of the other actions.

Summing the same individual utilities counts every contribution benefit n times and its private cost once. The resulting welfare coefficient b-c is positive, so unanimous contribution is socially maximal even though noncontribution is privately strictly dominant.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValueScale/PublicGoodsDominanceWelfareContrast.public_goods_dominance_welfare_contrast
• Dependency: D5/S3/ConceptDynamics/DecisionValue/ContributionIncentiveThreshold