Mechanism Design

Motivation

Ride-hailing, freelancing and delivery platforms are intermediaries that post a price to buyers and a price to sellers and then match the two sides. Both sides are forward-looking: an agent who arrives can wait before requesting, and an agent who requests waits until she is matched, at a cost per unit of time. Chen and Hu, Pricing and Matching with Forward-Looking Buyers and Sellers (SSRN 2859864; Manufacturing & Service Operations Management 22(4), 2020, doi:10.1287/msom.2018.0769), measure simple pricing and matching policies against an upper bound that holds for every policy. This mission formalizes that upper bound in its mechanism-design form: no incentive-compatible two-sided dynamic mechanism earns more than the expected value of a clairvoyant assignment problem in virtual values.

The bound extends the virtual-value approach of Myerson (1981) and its bilateral-trade version by Myerson and Satterthwaite (1983) from a single static trade to a market with random arrivals on both sides, waiting costs and a timing constraint that matched units change hands at the same instant.

Setting

Over a horizon $[0,T]$, buyers arrive as a Poisson process of rate $\lambda^d>0$. A buyer has type $\phi=(t_\phi,v_\phi)$: arrival time $t_\phi$ and valuation $v_\phi\in[\underline v,\bar v]$, drawn with continuous positive density $f^d$ and c.d.f. $F^d$, independently of the arrival time. Sellers arrive as an independent Poisson process of rate $\lambda^s>0$, with types $\psi=(t_\psi,c_\psi)$ and costs $c_\psi\in[\underline c,\bar c]$ of continuous positive density $f^s$ and c.d.f. $F^s$. The paper assumes $\underline c\le\bar v$ and that the virtual value $V^d(v)=v-(1-F^d(v))/f^d(v)$ and the virtual cost $V^s(c)=c+F^s(c)/f^s(c)$ are increasing (Assumptions 1–2). Write $H^T$ for the realized arrivals.

A direct mechanism $y^T$ assigns to every buyer an outcome $(s_\phi,m_\phi,p_\phi)$: the time $s_\phi\in[t_\phi,T]$ at which she leaves, the indicator $m_\phi\in\{0,1\}$ that she receives a unit, and her payment $p_\phi$. Every seller receives $(s_\psi,m_\psi,p_\psi)$ likewise, $p_\psi$ now paid to her. The balancing condition requires that at every $t\in[0,T]$ the number of buyers who receive a unit at $t$ equals the number of sellers who deliver one at $t$. The buyer's utility is $U^d=v_\phi m_\phi-p_\phi-b(s_\phi-t_\phi)$ and the seller's is $U^s=p_\psi-c_\psi m_\psi-h(s_\psi-t_\psi)$, with waiting costs $b,h\ge0$. The intermediary's profit is

$$\Pi(y^T)=\sum_{\phi\in H^T}p_\phi-\sum_{\psi\in H^T}p_\psi .$$

Incentive compatibility (ICd) asks that no buyer gain, in the interim expectation $E_{-\phi}$ over all other agents, by reporting another valuation or a later arrival time $t_{\hat\phi}\in[t_\phi,T]$; individual rationality (IRd) asks that her interim utility be nonnegative. (ICs) and (IRs) are the seller counterparts. Problem (B′) maximizes $E[\Pi(y^T)]$ over feasible mechanisms subject to these constraints; its value is $J^*$.

The comparison object is the clairvoyant assignment problem (B): knowing $H^T$ in advance, choose a partial matching $x$ of buyers to sellers maximizing

$$\sum_{\phi,\psi}\Big(V^d(v_\phi)-V^s(c_\psi)-b\,(t_\psi-t_\phi)^+-h\,(t_\phi-t_\psi)^+\Big)x_{\phi\psi};$$

its optimal value is $\bar J(H^T)\ge0$.

Formalization targets

Goal: the mechanism-design bound

For every feasible, well-defined mechanism satisfying (ICd), (IRd), (ICs) and (IRs),

$$E\big[\Pi(y^T)\big]\le E\big[\bar J(H^T)\big],$$

with $\bar J(H^T)$ integrable. This is the last display of the proof of Lemma 1 (Online Appendix p. 4), $J^*\le\bar J^1\le\bar J^2\le E[\bar J(H^T)]$.

Milestones

1. Lemma S.1 (Supplemental Note p. 1): $E_{-\phi}[p_\phi]\le v_\phi E_{-\phi}[m_\phi]-\int_{\underline v}^{v_\phi}E_{-\phi}[m_{\phi_{v'}}]\,dv'-bE_{-\phi}[s_\phi-t_\phi]$ under (ICd′) and (IRd).
2. Lemma S.2: $E[\sum_\phi p_\phi]\le E[\sum_\phi V^d(v_\phi)m_\phi-b(s_\phi-t_\phi)]$.
3. Lemma S.4: $E[\sum_\psi p_\psi]\ge E[\sum_\psi V^s(c_\psi)m_\psi+h(s_\psi-t_\psi)]$.
4. The pathwise step $\bar J^2\le E[\bar J(H^T)]$: for every profile and every balanced assignment of outcomes, buyer virtual surplus net of waiting, less seller virtual cost plus waiting, is at most the value of (B).

Lemma S.3 (Supplemental Note p. 3), the seller envelope bound with information rent $\int_{c_\psi}^{\bar c}E_{-\psi}[m_{\psi_{c'}}]\,dc'$, is posed as a further theorem of the mission, the mirror image of Lemma S.1; it is not listed as a milestone.

Here (ICd′) and (ICs′) are the one-dimensional constraints in which the reported arrival time is the true one; Lemmas S.1–S.4 are stated under these weaker hypotheses, as in the paper.

Significance

Lemma 1 of the paper, $J^{\pi,M}\le E[\bar J(H^T)]$ for every pricing policy $\pi$ and matching policy $M$, is the benchmark against which the paper's main theorem measures its waiting-adjusted fixed-price policy, and $E[\bar J(H^T)]$ is in turn bounded by a deterministic fluid value (Lemma 2). Lemma 1 is the composition of two facts: the revelation principle $J^{\pi,M}\le J^*$ (Lemma 3) and the mechanism-design bound $J^*\le E[\bar J(H^T)]$ posed here. The second carries the analytic content: it is where the envelope theorem, the exchange of integrals that turns payments into virtual values, and the timing argument appear.

The result is proved in the paper; its proofs are in the Online Appendix (Section A.2) and the Supplemental Note (Section A). No machine-checked proof of it, or of a dynamic two-sided Myerson bound of this kind, is known. A formal proof would also yield a reusable two-sided, Poisson-arrival version of the interim envelope and revenue-equivalence identities.

Difficulty

Each agent's type is two-dimensional, an arrival time and a valuation or cost, and arrival can only be misreported later. The relaxation to (ICd′)/(ICs′) makes the screening problem one-dimensional, but the interim expectation $E_{-\phi}$ ranges over a random population whose size is itself random. Turning $E[\sum_{\phi\in H^T}p_\phi]$ into an integral of interim payments requires the Mecke formula for the Poisson process, and the envelope argument must be carried out for interim utilities that are only known to be suprema of affine functions, using no differentiability of the mechanism. The pathwise step is combinatorial: the balancing condition at each instant pairs buyers with sellers discharged together, and those pairs must be compared with an optimal matching of (B), with duplicate types and unmatched agents handled.

A frequent first idea, bounding payments by valuations directly, gives only the first-best surplus $E[\sum (v_\phi-c_\psi)]$, which is not the target; the information rents must be extracted.

Formalization scope

The primitives are the published bilateral-trade environment MechanismDesign.BilateralTrade.Environment (densities on intervals, cdfB, cdfS, psiB $=V^d$, psiS $=V^s$, Regular $=$ Assumptions 1–2), and (B) is AssignmentGame.CoreLP.worth of the published assignment game, with sellers as rows and buyers as columns. The conventions committed to are:

1. Arrivals. Each side is a Poisson($\lambda T$) number of agents with i.i.d. types, arrival time uniform on $[0,T]$ and independent of the mark; this is equal in law to the Poisson process restricted to $[0,T]$. Profiles are multisets of types: agents are named by their types, as in the paper, and coincide only with probability zero.
2. Mechanisms map the reported buyer and seller profiles to an outcome for each type, $(s,m,p)$ with $t\le s\le T$ and $m\in\{0,1\}$ for listed agents and the balancing condition at every $t\in[0,T]$. The causality conditions of the paper (stopping times with respect to the filtration $\mathcal H_t$) and the timing variables $\tau,a$ are dropped. This enlarges the class of mechanisms; it is the clairvoyant class through which the paper's own proof passes ($\bar J^1\le\bar J^2$), and the bound for the larger class implies the paper's.
3. Interim expectations. $E_{-\phi}[g(y_{\hat\phi})]$ is the expectation, over an independent copy of $H^T$, of $g$ at the outcome of the report $\hat\phi$ inserted among the buyers (the Slivnyak–Mecke reading of "expectation taken with respect to $H^T\setminus\{\phi\}$").
4. Incentive constraints are quantified over every type and every report in the type spaces, not almost everywhere, with reported arrivals $t_{\hat\phi}\in[t_\phi,T]$.
5. Added hypotheses. Continuity of $f^d$, $f^s$ on their supports, without which $V^d,V^s$ are defined only almost everywhere; and WellDefined: outcomes are Borel in the listed types, interim payments are integrable, and total absolute payments are integrable. Integrability of $\bar J(H^T)$ and of the virtual-surplus sums is part of each conclusion.

A trivializing formalization is ruled out: the mechanism class is not restricted beyond the paper's feasibility, the constraints are not vacuous (the null mechanism satisfies them, so $J^*\ge0$), and expectations are of integrable functions. The goal quantifies over mechanisms rather than taking a supremum, which is equivalent because the class is nonempty.

A complete development needs the Mecke formula for the Poisson-count representation, an envelope theorem for suprema of affine functions on an interval, Fubini on the type space, and an exchange argument for matchings. All of these are reusable beyond this mission. Contributions of any of them, of the milestones in any order, or of alternative proofs are welcome.

Selected references

• Y. Chen and M. Hu, Pricing and Matching with Forward-Looking Buyers and Sellers, Manufacturing & Service Operations Management 22(4):717–734, 2020; submitted manuscript SSRN 2859864. https://ssrn.com/abstract=2859864, https://doi.org/10.1287/msom.2018.0769
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1):58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• R. B. Myerson and M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2):265–281, 1983. https://doi.org/10.1016/0022-0531(83)90048-0
• P. Milgrom and I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2):583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• G. Last and M. Penrose, Lectures on the Poisson Process, Cambridge University Press, 2017 (Mecke equation, Theorem 4.1). https://doi.org/10.1017/9781316104477

Motivation

Firms increasingly account for, and offset, the greenhouse-gas emissions of their entire supply chain, not only their own operations. Emissions in a supply chain are often jointly produced: the footprint of one process (transport, packaging, a molten-bulk delivery) depends on the abatement efforts of several firms at once. When each firm is charged for "its" emissions, the question is how to allocate the footprint of a jointly produced process so that every firm has the right incentive to abate.

Caro, Corbett, Tan and Zuidwijk (working paper, 2012; published in Manufacturing & Service Operations Management 15(4), 2013) model this as a moral-hazard problem in teams. Their §4 shows that a social planner who wants the first-best efforts must, under joint production, double-count emissions: the marginal payments across firms for one process exceed the carbon price. This mission formalizes §5, which looks at a different institutional arrangement observed in practice. One firm, the carbon leader (the paper's example is the cosmetics company Natura), voluntarily pays for all supply-chain emissions at a carbon price $p$ and compensates the other firms to induce abatement.

Timeline. Holmström (1982) showed that a budget-balanced sharing rule cannot implement efficient efforts in a team. Strausz (1999) showed that sequential moves can restore efficiency. Battaglini (2006) studied joint production with multidimensional output. Caro et al. (2012) placed the carbon leader in this line: a Stackelberg leader whose commitment plays the role of Strausz's sequential structure.

Setting

There are finite sets of firms $\mathcal N$ and processes $\mathcal I$. Firm $n$ chooses efforts $\mathbf e_n\in[0,A]^{m_n}$, one for each of its abatement actions, and the effort profile $\mathbf e$ lies in the box $[0,A]^M$. Firm $n$ earns profit $V_n(\mathbf e_n)$, which is differentiable, concave and componentwise decreasing: effort is costly. Process $i$ emits $f_i(\mathbf e)\ge0$, which is differentiable, convex and componentwise decreasing on the box. The influence matrix $B$ has $b_{n,i}=1$ if firm $n$ influences process $i$, that is, if $\sum_j\partial f_i/\partial e_{n,j}<0$, and $b_{n,i}=0$ otherwise.

The first best at carbon price $c$ maximizes the social value $\sum_n V_n(\mathbf e_n)-c\sum_i f_i(\mathbf e)$ over the box. At the societal cost $c=p_S$ its maximizer is $\mathbf e^*$, assumed unique.

The carbon leader is a firm $N$, written L in Lean. Every other firm $n$ has a reservation profit $\bar\pi_n$. The signed transfer $g_n$ is recorded as a payment by firm $n$; a negative value means compensation from the leader. The leader faces two problems.

• $P_E$ (6)–(8): it sets $g_n(\mathbf e_n)$, contingent on firm $n$'s own effort. It maximizes $V_N(\mathbf e_N)-p\sum_i f_i(\mathbf e)+\sum_{n\ne N}g_n(\mathbf e_n)$ subject to participation, $V_n-g_n\ge\bar\pi_n$, and incentive compatibility, $\mathbf e_n$ being a best response. Its optimal value is $z^E$, attained at efforts $\mathbf e^E$.
• $P_F$ (9)–(11): the same problem, except that the payments $g_n(\mathbf f)$ may depend only on the emissions vector $\mathbf f=\mathbf f(\mathbf e)$, because efforts cannot be verified.

Formalization targets

Goal: Proposition 5 (p. 16)

Let $(g^E,\mathbf e^E)$ be optimal for $P_E$ and define, for $n\neq N$,

$$g_n(\mathbf f)=p\sum_{i\in\mathcal I}b_{n,i}f_i+k_n,\qquad k_n=V_n(\mathbf e^E_n)-p\sum_{i\in\mathcal I}b_{n,i}f_i(\mathbf e^E)-\bar\pi_n.\qquad(12)$$

Then $(g,\mathbf e^E)$ is feasible for $P_F$, its value equals $z^E$, and every feasible solution of $P_F$ has value at most $z^E$:

$$\max P_F \;=\; z^E \;=\; \max P_E .$$

Milestones (proof in App. A.4, p. 26)

1. Reduction of $P_E$ (p. 15). $z^E=\max_{\mathbf e}\big[\sum_n V_n(\mathbf e_n)-p\sum_i f_i(\mathbf e)\big]-\sum_{n\ne N}\bar\pi_n$, attained at $\mathbf e^E$.
2. Participation under (12). $V_n(\mathbf e^E_n)-g_n(\mathbf f(\mathbf e^E))=\bar\pi_n$ for $n\ne N$.
3. First-order identity. $\partial V_n(\mathbf e^E)/\partial e_{n,j}=p\sum_i b_{n,i}\,\partial f_i(\mathbf e^E)/\partial e_{n,j}$ for $n\neq N$.
4. Incentive compatibility under (12). $\mathbf e^E_n$ maximizes $V_n(\mathbf x)-g_n(\mathbf f(\mathbf e^E_{-n},\mathbf x))$ over firm $n$'s box.
5. Upper bound. Every feasible solution of $P_F$ has value at most $z^E$.

Companion: Lemma 6 (p. 17)

If $0\le p<p_S$, each $V_n$ is supermodular and each $f_i$ is submodular, then $\mathbf e^E\le\mathbf e^*$ componentwise.

Significance

The result. Proposition 5 says that, when efforts are unobservable, a carbon leader that can commit loses nothing compared with contracting on efforts. A linear rule, the form footprint accounting already takes in practice, achieves the benchmark. The rule charges each firm the full price $p$ on every footprint it influences, so emissions are double-counted internally, yet the supply chain as a whole pays for carbon once. This is how the paper reconciles its §4 impossibility (a planner must double-count) with a footprint-balanced scheme: the leader moves first and is excluded from the incentive constraints. Lemma 6 then says that a leader paying a price below the societal cost induces weakly less effort than the first best.

Formalizing it. Both results are proved in the paper. As far as the platform's catalog shows, neither is machine-checked anywhere. The proof of Proposition 5 combines a reduction of a bilevel problem with a first-order argument for concave games on a box. The appendix compresses these into three sentences, one of which contains a misprint ("since f is concave" for convex). Formalizing it makes the leader–follower conventions explicit: the leader's tie-breaking choice of follower efforts, and the unilateral deviation in (11).

Difficulty

The paper calls $P_F$ a constrained version of $P_E$, but their feasible sets are not literally nested: $P_F$'s payments are functions of the emission vector and $P_E$'s of a firm's own effort. Establishing the common upper bound therefore requires care with the two payment domains and the participation constraint (10).

The incentive compatibility of (12) is the substantive step. It is a global best-response claim on a closed effort box, while the appendix states only a first-order identity at an interior point. The influence indicator $b_{n,i}=0$ also has to agree with every action-level derivative, rather than only their sum. For Lemma 6, the optimum at price $p$ need not be unique.

Formalization scope

• Indices. Firms, actions and processes are finite types. Efforts are e : (n : ι) → act n → ℝ, and a unilateral deviation is Function.update.
• Partial derivatives. A partial derivative is the one-variable deriv along one coordinate. Every theorem that uses one assumes differentiability.
• Optimality. "Optimal" means feasible with value at least that of every feasible point, never sSup. $z^E$ is the $P_E$ objective at an optimal pair.
• Influence matrix. $B$ is a real 0/1 matrix, and its defining sign condition is assumed at every profile in the box.
• Interiority. $\mathbf e^E$ is assumed interior, the page's "A is a sufficiently large bound to guarantee interior solutions"; the box itself stays closed.
• Followers' efforts. In $P_E$ and $P_F$ the leader chooses the followers' efforts subject to the best-response constraints, as the page assumes.
• Hypotheses not imposed. The row and column sums of $B$, the strictness of $c_n$ and $g_n\le0$ are unused and not imposed.

Rule (12) is a function of the emission vector only, and the deviation in (11) moves only firm $n$'s efforts. A formalization in which payments may depend on efforts, or in which a deviation also moves the leader, would make the goal trivial and is ruled out. A sorry-free instance with two firms checks that every hypothesis of the goal can be satisfied. Supermodularity reuses the published Supermodularity.Monotonicity.SupermodularOn. All other definitions live in CarbonDoubleCount.Leader.Setting.

Proofs of the milestones, or alternative routes such as a Lagrangian argument for incentive compatibility, are welcome. A general lemma that a concave differentiable function on a box is maximized at an interior stationary point would be reusable beyond this mission.

Selected references

• F. Caro, C. J. Corbett, T. Tan, R. Zuidwijk, Double-Counting in Supply Chain Carbon Footprinting, working paper dated December 21, 2012; Manufacturing & Service Operations Management 15(4), 2013. https://doi.org/10.1287/msom.2013.0443
• B. Holmström, Moral Hazard in Teams, Bell Journal of Economics 13(2), 1982. https://doi.org/10.2307/3003457
• R. Strausz, Efficiency in Sequential Partnerships, Journal of Economic Theory 85, 1999. https://doi.org/10.1006/jeth.1998.2488
• M. Battaglini, Joint Production in Teams, Journal of Economic Theory 130(1), 2006. https://doi.org/10.1016/j.jet.2005.03.003
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

Motivation

Carbon accounting assigns emissions from a shared supply-chain process to firms that can reduce them. If more than one firm can change the same emissions, charging each firm only a share may leave each with too little incentive to abate. Caro, Corbett, Tan and Zuidwijk study the conflict between avoiding double counting in an emissions ledger and inducing the effort a social planner would choose. Their working paper, published in Manufacturing & Service Operations Management in 2013, states an impossibility result for differentiable, increasing carbon-payment rules. It covers multiple firms, processes, and abatement actions, where a process can be influenced by several firms.

The question matters when a carbon footprint is used as a payment base rather than only as a report. A payment rule changes a firm's private incentive to exert costly effort. The rule may also include transfers between firms, so its incentive effect cannot be judged by looking at a single firm's allocated emissions alone. The paper asks what aggregate marginal payment is necessary if decentralized choices are to reproduce the social first best.

Timeline. Holmström (1982) showed for a team with one joint output and one-dimensional efforts that no budget-balanced sharing rule supports the efficient efforts as a Nash equilibrium (stated in the paper as Proposition 1, p. 11). Charging every team member the full social cost ("charging everything to everyone") is known to restore efficiency, as the paper recalls on p. 12. Caro, Corbett, Tan and Zuidwijk (2012 working paper, 2013 journal version) extend the impossibility to many processes, many abatement actions per firm and an explicit influence structure between firms and processes. They also characterize the linear rules that achieve the first best.

Setting

Let $N$ be a finite set of firms and $I$ a finite set of emission-producing processes. Firm $n$ chooses a vector $e_n=(e_{n,j})_j$ of abatement efforts in $[0,A]^{m_n}$, with $A>0$. The full profile is $e=(e_n)_n$. Firm $n$'s profit before carbon payments is $V_n(e_n)$, concave and componentwise decreasing in its effort. Process $i$'s footprint is $f_i(e)$, convex and componentwise decreasing in the collective effort, and nonnegative on the feasible box. The functions are differentiable, as assumed in the paper's model.

The influence matrix $B=(b_{n,i})$ has entries in $\{0,1\}$. An entry is one when the sum of the partial derivatives of $f_i$ with respect to firm $n$'s actions is negative. The paper treats this matrix as independent of the effort profile. Joint carbon production means that a process has at least two influencing firms: for some $i$, $\sum_n b_{n,i}\ge 2$.

The societal cost per unit of footprint is $p_S>0$. The social first best $e^*$ maximizes

$$S(e)=\sum_{n\in N}V_n(e_n)-p_S\sum_{i\in I}f_i(e)$$

over the effort box. The paper assumes that this solution is unique and that the effort bound is large enough for the relevant optimum to be interior. The first-best footprint is $f(e^*)=(f_i(e^*))_{i\in I}$.

A carbon-based payment rule $h_n(\phi)$ charges firm $n$ as a function of the observed footprint vector $\phi$, rather than the unobserved effort profile. In the social-planner setting of equation (5), $h_n(\phi)=p_S\widehat f_n(\phi)+g_n(\phi)$, where $\widehat f_n$ is its footprint allocation and the transfers balance: $\sum_n g_n(\phi)=0$ for $\phi\ge0$. A Nash equilibrium is a feasible effort profile where no firm improves $V_n(e_n)-h_n(f(e))$ by changing its own entire effort vector while the other firms hold theirs fixed. At a footprint vector $\phi$, the rule double-counts process $i$ when $\sum_n \partial h_n/\partial f_i(\phi)>p_S$.

Formalization targets

The goal is Proposition 2, evaluated at the first-best footprint:

$$\text{joint production}\ \land\ e^*\text{ is Nash under differentiable increasing }h \quad\Longrightarrow\quad \exists i\in I:\ \sum_n\frac{\partial h_n}{\partial f_i}(f(e^*))>p_S.$$

The paper defines double counting existentially over footprint levels. Its Appendix A.1 proves the stronger assertion at $f(e^*)$, which is the target here. The rule remains of the form (5), with balanced internal transfers on the nonnegative footprint domain.

Two source statements form the milestone list. The necessary part of Lemma 7 gives equation (14): at an interior first best that is also a Nash equilibrium, the sum over processes of each footprint derivative times the gap between the firm's marginal payment and $p_S$ is zero, both with and without the influence indicator $b_{n,i}$. Equation (18) says that if aggregate marginal payments do not exceed $p_S$ at $f(e^*)$, every individual process contribution to that sum is zero. The mission also drafts the sufficient part of Lemma 7 and Proposition 3, which characterizes the linear rules $h=p_S A_{\mathrm{mat}}f+k$ with $0\le A_{\mathrm{mat}}\le1$: they implement $e^*$ precisely when $A_{\mathrm{mat}}\ge B$.

Significance

Proposition 2 identifies a limit on footprint-based incentives under joint production. With more than one firm able to lower a process's emissions, a differentiable increasing rule that implements the first best cannot keep every aggregate marginal charge at or below the social carbon price. Balanced transfers among firms do not remove that requirement. Proposition 3 supplies a complementary characterization for linear payments, identifying which firms must bear the full marginal charge for the processes they influence. These are results proved in the paper, not open conjectures.

The formalization contributes a precise, reusable model of finite effort profiles, process footprints, unilateral deviations, and coordinate marginal payments. It also separates a global Nash best-response condition from first-order identities, so the necessary condition in Lemma 7 has mathematical content. The listed Lean theorems are draft statements with proof holes; they do not yet have machine-checked proofs. Completing them would formally verify the paper's stated claims under the declared model conventions.

Difficulty

The obstacle is the interaction between a shared footprint and unilateral decisions. A firm's payment derivative with respect to a process footprint is multiplied by that firm's own effect on the process, while the social objective prices the total footprint at $p_S$. A condition on the sum of marginal payments alone does not specify the charge faced by each influential firm. With several actions and processes, the necessary condition is a sum over process contributions, so it cannot simply be read as a coordinatewise equality without further assumptions. These issues occur even though all effort and process index sets are finite.

Formalization scope

Lean represents firms, each firm's action indices, and processes by finite types. Efforts and footprints are real-valued functions. The firm and collective effort boxes are closed coordinatewise intervals, with $A>0$; optimality and Nash equilibrium quantify over all feasible profiles or unilateral deviations. Coordinate partial derivatives use one-variable derivatives after replacing the corresponding coordinate. Payment rules are functions on real footprint vectors and “increasing” means componentwise nondecreasing.

The source's sign test for $b_{n,i}$ does not name an effort profile. The formalization pins it to every profile in the effort box, matching the paper's use of a fixed influence matrix. Interiority is required only of the named first best. The paper's “without loss of generality” nonempty row and column sums for $B$ are omitted because the results do not use them; the strict part of its cost monotonicity is likewise unused. Its participation condition (3) is outside the decentralized game (4) and is not added to Nash equilibrium. Equation (5) and transfer balance are imposed only for nonnegative footprint vectors, as printed. The effort bound $A$ and Proposition 3's matrix $A_{\mathrm{mat}}$ have distinct names.

The first best is a feasible global maximum, not a default-valued real supremum; Nash equilibrium tests full unilateral deviations, not stationarity. These choices rule out a vacuous first-best target and a first-order surrogate for the game. The supporting definitions of finite effort boxes, coordinate derivatives, social value, and Nash best response are useful beyond the final impossibility statement. Contributions that prove the source's necessary and sufficient conditions, the linear characterization, or the goal against these definitions are within scope.

Selected references

• B. Holmström, Moral Hazard in Teams, Bell Journal of Economics 13(2), 324–340, 1982. DOI.
• F. Caro, C. J. Corbett, T. Tan and R. Zuidwijk, Double-Counting in Supply Chain Carbon Footprinting, working paper dated December 21, 2012, especially §§3–4 and Appendix A. Author-hosted manuscript. Published in Manufacturing & Service Operations Management 15(4), 2013. DOI.

Why market entry and exit matter

Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.

The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.

The market and the adjustment process

A market has a finite set $W$ of workers and a finite, nonempty set $F$ of firms. Worker $i$'s utility from employment at firm $j$ for salary $s$ is $u_i(j;s)$. Firm $j$ produces $y^j(C)$ from a set $C\subseteq W$ and earns profit $\pi^j(C;s)=y^j(C)-\sum_{i\in C}s_i$. Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary $\sigma_{ij}$, and permitted salaries increase by a common unit $\delta>0$: $\sigma_{ij}+k\delta$ for $k\in\mathbb N$.

Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by $\delta$ next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.

An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.

Formalization targets

The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.

The goal is Theorem 5. Write $A$, $A^+$ and $A^-$ for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are

$$\forall i\in W,\quad u_i(A)\leq u_i(A^+),\qquad \forall j\in F,\quad \pi^j(A^-)\leq\pi^j(A).$$

The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same $\delta$ and satisfy the conditions of Theorem 4.

What the result establishes

The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.

The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.

The main difficulty

Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.

Formalization scope

Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; $\delta$ is positive. An allocation assigns every worker to a firm, as the paper's $f:\{1,\ldots,m\}\to\{1,\ldots,n\}$ does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.

“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.

Why private information changes bargaining

An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.

The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.

The finite Bayesian choice problem

Let $I$ be a nonempty finite set of players. Player $i$ has a nonempty finite type set $A_i$, and the group has a nonempty finite set $C$ of possible choices. A type profile is $\alpha\in\prod_{i\in I}A_i$. The utility $U_i(c,\alpha)\in\mathbb R$ is player $i$'s payoff when choice $c$ occurs and $\alpha$ is the true profile. A nonnegative function $P$ on type profiles, summing to one, is the common prior. Write $R_i(a_i)$ for the probability that player $i$ has type $a_i$, and $P_i(\alpha\mid a_i)$ for the posterior probability of $\alpha$ conditional on that type. Every $R_i(a_i)$ is positive, so the conditional probabilities are defined.

A choice mechanism $\pi$ asks each player for a response and assigns a probability $\pi(c\mid s)$ to each choice $c$ at each response profile $s$. For the direct mechanisms used here, the response set of player $i$ is $A_i$: a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is $a_i$ instead reports $b_i$, while the others report truthfully, the player's conditional expected utility is $Z_i(\pi,b_i\mid a_i)$. The posterior $P_i(\alpha\mid a_i)$ weights true profiles; the mechanism sees the profile with only coordinate $i$ replaced by $b_i$; and utility is evaluated at the true profile $\alpha$.

The mechanism is Bayesian incentive-compatible when $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for every player and pair of types. Its interim payoff vector $V(\pi)$ has one coordinate $V_{i,a_i}(\pi)=Z_i(\pi,a_i\mid a_i)$ for every player-type pair. The set $F$ contains the vectors attained by all direct choice mechanisms; $F^*$ contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says $F^*$ is nonempty, convex, compact, and contained in $F$. The nonemptiness claim includes the mechanism that selects each choice with probability $1/|C|$, independent of all reports.

Formalization targets

Fix a conflict outcome $c^*\in C$: the choice that occurs if bargaining fails. Its conflict payoff vector $t$ gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects $c^*$ regardless of reports. It is incentive-compatible and generates $t$, so $t\in F^*$. The individually rational incentive-feasible set is

$$F^*_+=\{x\in F^*: x_{i,a_i}\ge t_{i,a_i}\text{ for all }i,a_i\}.$$

For $x\in F^*_+$, the generalized Nash product of equation (18) is

$$N(x)=\prod_{i\in I}\prod_{a_i\in A_i} (x_{i,a_i}-t_{i,a_i})^{R_i(a_i)}.$$

A bargaining solution is a vector in $F^*_+$ that maximizes $N$ over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:

$$\neg\operatorname{Efficient}(\pi_{c^*}) \quad\Longrightarrow\quad \exists!x\in F^*_+\;\forall y\in F^*_+,\;N(y)\le N(x).$$

The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; $F^*$ has the four properties in Theorem 1; the conflict vector belongs to $F^*$; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.

What the result provides

Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.

The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of $\mathbb R^2$. It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.

The mathematical obstacle

The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.

The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights $R_i(a_i)$ matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.

Formalization scope

Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions $\prod_i A_i$; interim vectors are real functions on the disjoint union $\sum_i A_i$, with the product topology. A mechanism is a real function $\pi:C\to(\prod_i A_i)\to\mathbb R$ subject to explicit nonnegativity and sum-to-one constraints. Both $F$ and $F^*$ quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every $R_i(a_i)$ is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of $P_i$ and $R_i$ that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.

Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on $F^*_+$, where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.

A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.

Selected references

• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. DOI: 10.2307/1912346.
• John F. Nash, The Bargaining Problem, Econometrica 18(2), 155–162, 1950. DOI: 10.2307/1907266.
• John C. Harsanyi and Reinhard Selten, A Generalized Nash Solution for Two-Person Bargaining Games with Incomplete Information, Management Science 18(5), P80–P106, 1972. DOI: 10.1287/mnsc.18.5.80.