Contribution Incentive Threshold

Abstract

Binary contribution is dominant exactly at the source compensation threshold.

Theorem 1.1 (Contribution becomes dominant at the compensation threshold).

$$\begin{gathered} n\in \mathbb{N},2\le n,b,c,\tau \in \mathbb{R}, \\ b>c>\frac{b}{n}, \\ \mathrm{payoff}(\rho ,i,a)=\frac{b}{n}\sum _{j\in \mathrm{Fin}(n)}{a}_j-c{a}_i+\rho a_i, \\ \mathrm{Weak}(\rho )⟺\forall i\in \mathrm{Fin}(n),a:\mathrm{Fin}(n)\to \{0,1\},\mathrm{payoff}(\rho ,i,\mathrm{update}(a,i,0))\le \mathrm{payoff}(\rho ,i,\mathrm{update}(a,i,1)), \\ \mathrm{Strict}(\rho )⟺\forall i\in \mathrm{Fin}(n),a:\mathrm{Fin}(n)\to \{0,1\},\mathrm{payoff}(\rho ,i,\mathrm{update}(a,i,0))<\mathrm{payoff}(\rho ,i,\mathrm{update}(a,i,1)) \\ \Rightarrow (\mathrm{Weak}(\tau )⟺\tau \ge c-\frac{b}{n})\wedge \\ (\tau >c-\frac{b}{n}\Rightarrow \mathrm{Strict}(\tau ))\wedge \\ \mathrm{IsLeast}(\{\rho \in \mathbb{R}\mid \mathrm{Weak}(\rho )\},c-\frac{b}{n}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValue/ContributionIncentiveThreshold.contribution_incentive_threshold (✓ std3). ∎

Source. Repository-derived.

Commentary.

There are n at least two agents and each binary profile records whether each agent contributes. The aggregate is constructed from the selected action and the finite sum over every other agent.

The compensated utility is the common per-agent benefit b/n times total contribution, minus the contributor’s cost c, plus compensation rho. The source restrictions b greater than c greater than b/n are public.

Updating one agent from non-contribution to contribution changes utility by b/n-c+rho, independently of the other actions. Hence weak dominance is equivalent to rho at least c-b/n and strict dominance follows above that threshold.

The public conclusion also states that c-b/n is the least member of the set of compensations inducing weak dominance. Funding, allocation, and fairness are identified by the source as separate normative questions and are not promoted to universal mathematical claims.

Repository and pinned Mathlib searches found no exact theorem packaging the source payoff construction and all three threshold clauses.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValue/ContributionIncentiveThreshold.contribution_incentive_threshold