Algorithmic Game Theory

Why investment races matter

Two firms developing competing innovations face a decision that a single firm does not: a rival's discovery can end the value of continuing the project. If the first discovery wins the payoff, each firm chooses how much to spend per period while knowing that greater spending may change both its payoff on success and its speed of discovery. The investment decision therefore depends on what the rival chooses. Danmo Lin's model separates these two channels and asks when competition itself raises a firm's chosen R&D intensity Lin (2022).

This mission concerns the paper's race of two financially unconstrained firms. The result is a comparative statics claim about a firm's best response to its rival, together with existence of a symmetric pure-strategy equilibrium. The paper proves the result in Appendix A.6. The problem here is to give machine-checked statements and ultimately a proof for the same stochastic race, including its strategy ranges and first-arrival payoffs.

The two-firm race

Firm $i\in\{1,2\}$ chooses a fixed investment intensity $R_i$, the amount it pays per unit time while the race continues. Its technology has parameters $(A_i,\beta_i,\eta_i,\gamma_i)$. If it discovers first, its mean project payoff is $u_i(R_i)=A_iR_i^{\beta_i}$. Its discovery time $\tau_i$ is exponentially distributed with rate $\lambda_i(R_i)=\eta_iR_i^{\gamma_i}$. The discovery times are independent, represented by the product law $\mathcal E(\lambda_1,\lambda_2)$, and the earlier discovery wins. Both firms stop paying at $\min\{\tau_1,\tau_2\}$. The loser receives no discovery payoff. Future cash flows are discounted at rate $r>0$ Lin (2022), §3.1.

The technology conditions are $A_i,\eta_i>0$, $0\le\beta_i,\gamma_i<1$, and $\beta_i+\gamma_i<1$. A project is scalable when its discovery payoff increases with investment, corresponding here to $\beta_i>0$. It is accelerable when investment increases its discovery rate, corresponding to $\gamma_i>0$. The model permits the two firms' parameters to differ. The lower intensity is $1$; the upper intensity is $\bar R_i=(A_i\eta_i)^{1/(1-\beta_i-\gamma_i)}$. The standing condition $A_i\eta_i>1$ makes $[1,\bar R_i]$ a nondegenerate range in which investment takes place Lin (2022), (2), (7).

Write $P_i(R_1,R_2)$ for Firm $i$'s expected discounted payoff from the first-arrival race. Its best-response set $BR_i(R_{-i})$ contains every maximizer of $P_i$ over its own fixed interval $[1,\bar R_i]$, holding the rival's intensity fixed. A pure Nash equilibrium is a pair $(R_1,R_2)$ in which each intensity belongs to that firm's best-response set. This set-valued definition keeps the claim meaningful when there is more than one maximizer.

Formalization targets

The first milestone identifies each expected payoff with the closed form in Lemma 2:

$$P_i(R_1,R_2)=V_i(R_1,R_2) =\frac{u_i(R_i)\lambda_i(R_i)-R_i}{r+\lambda_1(R_1)+\lambda_2(R_2)}.$$

The second milestone is the Appendix A.6 cross-partial identity. For Firm 1, the expression $V_1\,\partial^2_{R_1R_2}V_1-(\partial_{R_1}V_1)(\partial_{R_2}V_1)$ equals $\lambda'_2(u_1\lambda_1-R_1)^2\lambda'_1/(r+\lambda_1+\lambda_2)^4$. It is strictly positive when both discovery rates rise with intensity and Firm 1's project surplus is nonzero Lin (2022), (A.27)–(A.28).

The goal is Proposition 3. When both projects are accelerable, higher rival investment orders the best-response sets upward, with strict movement for an old response above $1$. When neither project is accelerable, the best-response sets are constant in the rival's intensity. For identical firms, the theorem asserts a symmetric pure Nash equilibrium:

$$\exists R\in[1,\bar R]\quad R\in BR_1(R)\cap BR_2(R).$$

Best-response sets are required to be nonempty for every positive rival intensity. The ordering statements therefore make substantive claims about actual choices Lin (2022), Proposition 3.

What the result establishes

The result distinguishes a change in the timing of innovation from a change in its eventual payoff. In an accelerable project, a rival who spends more discovers faster, and the firm's optimal investment response moves upward. If investment cannot affect discovery speed, a rival's intensity does not alter the firm's best-response set in this model. The equilibrium clause says the symmetric game has at least one profile at which neither firm gains by changing its own intensity. These are statements about competition's effect on project spending, rather than only about the numerical value of a firm Lin (2022), §3.1.

The mathematical result is proved in the paper; the mission seeks a Lean formalization of that known result. The expectation-to-value identity requires a reusable treatment of independent exponential discovery times and discounted spending stopped at the first arrival. The best-response statement then supplies a precise set-valued comparative statics target. A verified development of these ingredients could be reused for other innovation races and first-arrival games. This mission does not claim that such a machine-checked proof already exists.

Mathematical difficulty

The payoff is an expectation over two random times, with the prize awarded only to the earlier discovery and spending stopped at their minimum. The closed form must agree with that stochastic expression for each positive pair of intensities. The comparison of best responses involves all maximizers, including possible ties and boundary choices. A derivative of one selected optimizer is not a well-defined substitute when the optimizer is set-valued; moreover, strict response cannot be demanded at the lower endpoint. Equilibrium existence must hold for the same best-response correspondence that defines the competitive race. These points make a direct translation of the paper's derivative notation insufficient Lin (2022), Appendix A.5–A.6.

Formalization scope

Lean uses real intensities, real technology parameters, Real.rpow for the power functions, and ProbabilityTheory.expMeasure for each discovery time. Their product measure encodes independence. Firm 1's discovery time is the first coordinate throughout, including Firm 2's payoff. The two firms have separate technology records. A best response maximizes the expectation from (8) over the own interval $[1,\bar R_i]$; that interval never depends on the rival's action. The named closed form $V_1$ is separate from the expectation and appears in the Appendix A.6 milestone. The random payoff on discovery is represented by its mean $u_i(R_i)$, as the paper's calculation uses only that mean. The other cash-flow component of the underlying firm value is independent of the R&D choice and is omitted from the race payoff.

The hypotheses $A_i\eta_i>1$, $r>0$, and positive intensities are explicit. The comparison allows any positive rival intensity, while each firm's own maximization uses (7). The paper's derivative claims about $R_i^*$ are posed as orderings of complete best-response sets; strictness is asserted for an old response above $1$. Both firms must be accelerable for the increasing-response clause, and the symmetric equilibrium clause applies to identical technologies. The strict inequality in (A.28) includes the necessary nonzero-surplus condition, since its square vanishes at the upper endpoint. These choices and the printed endpoint issue are recorded in the mission's moderation notes.

The target excludes empty best-response sets, rival-dependent feasible ranges, payoffs defined by the closed form (9), an equilibrium asserted without mutual best-response membership, and comparisons that discard the strict interior part. A complete development will need integration and exponential-distribution facts, continuity and maximizer existence on compact intervals, ordered best-response sets, and a fixed-point argument for the symmetric correspondence. The first-arrival probability and integration results can be reused beyond this paper; contributions to those interfaces and to the two stated milestones are welcome.

Selected references

• Danmo Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. DOI: 10.1287/mnsc.2022.4503.

Motivation

Two-sided platforms for dating, freelancing and housing do more than list participants: they decide whom each participant is shown. When search is costly and agents leave the market over time, the platform's choice of assortments (which types of agents meet which, and how often) determines who matches, and agents respond strategically by deciding which matches to accept. A platform that ignores those responses can design meetings that agents then decline.

Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search in a stationary flow economy and ask how much welfare a platform can secure when it controls only meetings, while agents retain the decision to accept. Computing the optimal assortments is NP-hard to approximate within 24/23 (their Theorem 4.2), so the relevant question is whether a constant fraction of the best conceivable welfare is reachable at all. Their Theorem 4.1 answers it with the factor 4, measured against the platform's first best, a benchmark in which the platform also dictates acceptance.

The mission formalizes the existence part of Theorem 4.1 and the chain of results in §4 of the paper that leads to it.

Setting

There are finitely many types on two sides, a set $\mathcal M$ and a set $\mathcal W$; write $\Theta=\mathcal M\cup\mathcal W$ and let $\theta'$ denote a generic type on the side opposite to $\theta$. Agents of type $\theta$ enter at rate $\alpha_\theta>0$ and each agent leaves unmatched at rate $\delta>0$. When an agent of type $m$ meets one of type $w$, both observe one symmetric utility $u$ drawn from a law $F_{mw}$ on $\mathbb R$ with no atoms and finite mean; they match, and leave with utility $u$ each, if both accept.

The platform picks an assortment $\lambda_\theta(\theta')\ge0$ for each type: type $\theta$ meets type $\theta'$ at rate $\lambda_\theta(\theta')$. Agents use thresholds $\tau_\theta$ and accept exactly when $u\ge\tau_\theta$, so a pair matches when $u\ge\max(\tau_m,\tau_w)$. With population masses $\eta_\theta$ and matching rates $\xi_\theta$, the assortments induce a stationary equilibrium when, for every type,

$$\alpha_\theta=(\delta+\xi_\theta)\eta_\theta,\qquad \eta_m\lambda_m(w)=\eta_w\lambda_w(m),\qquad \sum_{\theta'}\lambda_\theta(\theta')\le1,$$ $$\xi_\theta=\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty dF_{\theta\theta'},\qquad \tau_\theta=\frac{\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty u\,dF_{\theta\theta'}}{\delta+\xi_\theta}.$$

These are constraints (6a)–(6f) of the paper; the last one, (6e), says each threshold equals the type's expected utility, which is the agents' best response. The welfare is the flow of realized utility,

$$\mathrm{SW}=\sum_{m}\sum_{w}\big(\eta_m\lambda_m(w)+\eta_w\lambda_w(m)\big)\int_{\max(\tau_m,\tau_w)}^\infty u\,dF_{mw}.$$

The first-best relaxation (§4.1) drops (6e) and replaces $\max(\tau_m,\tau_w)$ by a free pairwise threshold $\tau_{mw}$: the platform chooses both the meetings and which matches happen. Its welfare $\mathrm{FB}$ is the same expression with $\tau_{mw}$.

Formalization targets

Goal: Theorem 4.1

For every market satisfying the standing assumptions there are assortments, thresholds, rates and masses satisfying (6a)–(6f) such that, for every first-best feasible candidate $Q$,

$$\mathrm{FB}(Q)\le 4\,\mathrm{SW}.$$

Milestones

1. Proposition 4.4. The first best equals the linear program $\max\,2\sum_{m,w}\rho_{mw}\beta_{mw}$ subject to $\beta\ge0$, $\sum_w\beta_{mw}\le\alpha_m$, $\sum_m\beta_{mw}\le\alpha_w$, where $\rho_{mw}=\max_{\tau\ge0}\int_\tau^\infty u\,dF_{mw}/(\delta+\int_\tau^\infty dF_{mw})$.
2. Lemma 4.5. The maximizer of $A(\tau)=\int_\tau^\infty u\,dF/(\delta+\int_\tau^\infty dF)$ over $\tau\ge0$ is a fixed point of $A$, and $A$ increases before it and decreases after it.
3. Lemma 4.6. The LP has an optimal solution whose support is a forest on $\Theta$.
4. Lemma 4.7. An edge-weighted forest keeps half its weight on a union of vertex-disjoint stars.
5. Lemma 4.9. In a star-shaped market (one side has a single type) the LP is a fractional knapsack with a greedy optimum.
6. §4.2.2 remark, Lemmas 4.10–4.12. The idealized thresholds $\hat\tau_{w_i}$ exist, coincide with or lie below $\rho_{mw_i}$, and bound the equilibrium thresholds from above and the pair thresholds $\max(\tau_m,\tau_{w_i})$ from below.
7. Proposition 4.8. In a star-shaped market some induced stationary equilibrium satisfies $\mathrm{FB}(Q)\le2\,\mathrm{SW}$ for every first-best feasible $Q$.

Significance

Theorem 4.1 is a price-of-anarchy statement for platform design: restricting the platform to meetings, and letting agents choose acceptance selfishly, costs at most a factor 4 against a platform that dictates everything. Since every equilibrium candidate is also a first-best candidate with the same welfare, it gives a 4-approximation to the optimal directed search as well. The construction behind it has a structure that is itself informative: the equilibrium consists of disjoint submarkets in each of which one side has a single type.

The results are proved in the paper; none of them has a machine-checked proof in Lean or another proof assistant on record. Formalizing them yields a checked model of stationary search markets with threshold play, a checked reduction of the first best to a generalized assignment LP, and two graph lemmas (forest support of LP optima, the star-forest halving) that recur in rounding arguments for generalized assignment and budgeted allocation.

Difficulty

The first best is easy to reach once Proposition 4.4 linearizes it; the obstacle is incentives. Turning a first-best solution into an equilibrium by keeping its meeting rates fails, because agents raise or lower their thresholds relative to the pairwise thresholds the platform would choose, and constraint (6e) couples every type's threshold to all thresholds on the opposite side through $\max(\tau_m,\tau_w)$. The paper therefore has to control equilibrium thresholds without computing them, which it does only in star-shaped markets, and it needs a case analysis there (Case 1 and Subcases 2(a), 2(b) of Proposition 4.8) in which the meetings of the first best are sometimes discarded. Each of the reductions loses a factor: 2 in the passage from a forest to stars and 2 inside each star.

Formalization scope

The sides are separate finite types M and W with one law F m w per pair, serving both sides. The standing assumptions are $\delta>0$; $\alpha_\theta>0$ for every type; each $F_{mw}$ a probability measure with no atoms (NullSingletonClass, the paper's "continuous distribution"); and an integrable identity under each $F_{mw}$. The positivity of $\alpha_\theta$ and the integrability are added: the paper uses both implicitly. Tails are taken over $[a,\infty)$. LP feasibility includes $\beta\ge0$, which the paper leaves implicit; Lemma 4.6 also assumes nonnegative capacities. $\rho_{mw}$ is the supremum of $A$ over $[0,\infty)$, never defined as a fixed point.

"Approximation of the first-best optimum" is stated against every first-best feasible candidate, so no supremum appears. An induced stationary equilibrium always includes the best-response constraint (6e); a formalization that drops it, or that lets the equilibrium use pairwise thresholds, makes the goal compare the first best with itself and is ruled out. With an empty side both welfares vanish and the goal holds, as in the paper.

The "polynomial-time" part of Theorem 4.1 is not posed: the paper's computational model (oracle access to the laws, footnote 15) is not specified precisely enough to formalize. The source is the arXiv v2 preprint (18 Aug 2021); the Management Science version may number results differently. Proofs of any milestone, auxiliary lemmas about tail integrals of atomless laws, and LP vertex arguments are all welcome.

Selected references

• N. Immorlica, B. Lucier, V. Manshadi, A. Wei, Designing Approximately Optimal Search on Matching Platforms, Management Science, 2023; preprint arXiv:2102.09017v2. https://arxiv.org/abs/2102.09017
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• D. Chakrabarty, G. Goel, On the approximability of budgeted allocations and improved lower bounds for submodular welfare maximization and GAP, SIAM Journal on Computing 39(6), 2010. https://doi.org/10.1137/080735503
• S. Banerjee, S. Gollapudi, K. Kollias, K. Munagala, Segmenting two-sided markets, WWW 2017. https://doi.org/10.1145/3038912.3052578

Motivation

In many auctions a bidder's value for what is sold depends on information held by other bidders: the value of an oil-drilling lease depends on every bidder's geological survey, the value of a piece of art on what other experts know about its provenance. This is the interdependent values model of Milgrom and Weber (1982). With interdependent values the standard private-value tools fail: the Vickrey–Clarke–Groves (VCG) mechanism is no longer incentive compatible, exact efficiency in ex-post equilibrium requires a single-crossing condition, and with multidimensional signals maximizing welfare is generically impossible even in Bayes–Nash equilibrium (Jehiel and Moldovanu 2001). Without some structural condition on how values respond to others' information, even a single-item auction can force every truthful randomized mechanism to lose a factor of order $n$ (Example 1.3, after Eden et al. 2018), when values treat the signals as complements.

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384, Mathematics of Operations Research 2024) identify such a condition, submodularity over signals (SOS), and show that under SOS simple randomized mechanisms recover a constant fraction of the optimal welfare in rich settings. This mission formalizes their result for combinatorial auctions with multidimensional signals and separable SOS valuations, where the mechanism is a random-sampling variant of VCG with explicit payments.

Timeline of the line of work:

• Milgrom and Weber (1982): the interdependent values model.
• Jehiel and Moldovanu (2001): with multidimensional signals, welfare maximization is generically impossible even in Bayes–Nash equilibrium.
• Chawla, Fu and Karlin (2014): revenue approximation in interdependent value settings under single crossing.
• Roughgarden and Talgam-Cohen (2016): characterization of ex-post IC for single-parameter settings by monotone allocation rules.
• Eden, Feldman, Fiat and Goldner (2018): welfare approximation for single-item auctions under a relaxed c-single crossing condition; an SOS notion also appears there.
• Eden, Feldman, Fiat, Goldner and Karlin (2019, arXiv v2): welfare approximation under SOS, without single crossing, for downward-closed single-parameter settings and combinatorial auctions; the subject of this mission.

Setting

There are $n$ agents and $m$ items; a bundle is a set $T \subseteq [m]$. Each agent $i$ privately holds a signal $s_{iT} \ge 0$ for every bundle $T$, and $s_T = (s_{1T}, \dots, s_{nT})$ collects all agents' signals for $T$. Agent $i$'s value for bundle $T$ is $v_{iT}(s_T) \ge 0$, a known function of $s_T$, weakly increasing in every signal and strictly increasing in $s_{iT}$; the empty bundle is worth $0$.

A function $w$ of the signal vector is SOS when raising a single coordinate helps at least as much at a coordinatewise lower profile of the other coordinates: for every coordinate $j$, $x, \delta \ge 0$ and profiles $s' \le s$ off $j$,

$$w(s_{-j}, x + \delta) - w(s_{-j}, x) \le w(s'_{-j}, x + \delta) - w(s'_{-j}, x).$$

The valuations are separable SOS when

$$v_{iT}(s_T) = g_{-iT}(s_{-iT}) + h_{iT}(s_{iT}),$$

with $g_{-iT}$ (depending only on the other agents' signals for $T$) and $h_{iT}$ weakly increasing and $g_{-iT}$ SOS.

An allocation gives agent $i$ the bundle $T_i$, with the bundles pairwise disjoint. A deterministic mechanism maps reported signals to an allocation and payments. It is ex-post incentive compatible (IC) if, whatever the true signals, no agent gains by misreporting when the others report truthfully, where the agent's utility is her value at the true signals for the bundle she receives minus her payment; it is ex-post individually rational (IR) if the truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support is.

Random-Sampling VCG (RS-VCG) partitions the agents uniformly at random into $A$ and $B$. For $j \in B$ it sets the proxy weight

$$w_{jT} := v_{jT}(\tilde s_{jT}, \tilde s_{AT}, 0_{B - jT}),$$

the value with the bundle-$T$ signals of the other members of $B$ replaced by $0$. It allocates to $B$ a feasible allocation $\{T_i\}_{i\in B}$ maximising $\sum_{i \in B} w_{iT_i}$, and a winner $i \in B$ pays

$$p_i(\tilde s) = g_{-iT_i}(\tilde s_{-iT_i}) - g_{-iT_i}(\tilde s_{AT_i}, 0_{B-iT_i}) - \sum_{j \in B\setminus\{i\}} w_{jT_j} + w_{-i},$$

where $w_{-i}$ is the maximum proxy welfare of an allocation to $B \setminus \{i\}$.

Formalization targets

Goal: Theorem 5.1 (p. 17)

For separable SOS valuations, RS-VCG is ex-post IC and IR for every partition, and for every true profile $s$ and every feasible allocation $(S^*_i)$,

$$\sum_i v_{iS^*_i}(s_{S^*_i}) \le 4\, \mathbb{E}_B\Bigl[\sum_i v_{iT_i(B)}(s_{T_i(B)})\Bigr].$$

Milestones

1. Observation 2.2 (p. 12): a separable SOS valuation is SOS.
2. Display (5) (p. 17): $\mathbb{E}_B[w_{iT}\cdot\mathbf 1_{i\in B}] \ge \frac{v_{iT}(s_T)}{2}\cdot\frac12$ for every agent $i$ and bundle $T$.
3. Payment sign (p. 17): the payments $p_i(\tilde s)$ are nonnegative.
4. IC display (p. 18): for every partition, truthful reporting maximises each agent's utility.
5. IR display (p. 18): for every partition, the truthful utility is nonnegative.

Significance

The theorem shows that VCG-style reasoning survives interdependence when the dependence on other agents' information enters additively and submodularly: separability makes the payment absorb the effect of the others' signals, so that each agent of $B$ faces the proxy welfare as its objective. It gives a constant-factor welfare guarantee in ex-post equilibrium for combinatorial auctions with multidimensional interdependent signals, a setting in which exact efficiency is generically out of reach. The construction is the template for the paper's single-dimensional results in §6.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a reusable Lean model of interdependent-value combinatorial auctions (multidimensional signals, ex-post IC/IR, universal truthfulness of random mixtures) and of the SOS condition, and a checked account of the VCG accounting identity in this setting.

Difficulty

The approximation part rests on the Key Lemma 3.1: a uniformly random half of the other agents' signals set to zero keeps, in expectation, half of an SOS value. The obvious argument — monotonicity alone — gives no constant: with values depending on many signals, zeroing half of them can destroy almost all of the value, and the SOS condition is exactly what rules this out. The incentive part is where the obvious transfer of VCG fails: the proxy weight $w_{iT}$ of agent $i$ is not its value, and the true value $v_{iT}$ depends on signals that the proxy zeroes. Without separability, the payment of a VCG-style rule would itself depend on the agent's report (the paper's remark at the start of §5), and alignment of the agent's utility with the proxy objective breaks. Ties in the argmax and agents receiving the empty bundle must be handled for every tie-breaking rule.

Formalization scope

Agents are Fin n and items Fin m, with $n, m$ arbitrary; bundles are Finset (Fin m). Signals are NNReal, one per (agent, bundle), and $v_{iT}$ is a function of the bundle-$T$ signal vector. The empty bundle is worth $0$; monotonicity, strict own-signal monotonicity and the separable decomposition are assumed for nonempty bundles. The function $g_{-iT}$ is written on the whole vector with the hypothesis that it ignores coordinate $i$. The decomposition $(g, h)$ is data of the mechanism, since the payments use $g$.

The allocation is produced by an arbitrary selector returning a feasible maximiser of the proxy welfare for every partition and report; all statements hold for every such selector. $w_{-i}$ is a maximum over the finite set of feasible allocations to $B \setminus \{i\}$. Agents of $A$, and agents of $B$ that receive the empty bundle, pay $0$ (the paper defines payments for winners only). The expectation over the partition is the uniform average $2^{-n}\sum_{B \subseteq [n]}$, never an existential or universal over $B$; the approximation is stated for every feasible comparator allocation, with welfare at true values under truthful reports, never for proxy welfare or through a supremum. IC and IR are stated for each partition with the paper's explicit payments, not with existentially chosen payments.

A complete development needs finite averages over subsets, the Key Lemma 3.1 for SOS functions (posed in the companion mission on RS-V and not restated here), and finite argmax reasoning; the SOS layer and the combinatorial mechanism model are reusable for the other missions of this series. Proofs of the milestones, and of the d-SOS variant mentioned after the proof (a $2(d+1)$-approximation, not posed here), are welcome.

The source is the arXiv preprint arXiv:1903.08384v2 (2 June 2019); all page and display numbers refer to it, not to the journal version in Mathematics of Operations Research (2024).

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019; Mathematics of Operations Research, 2024. https://arxiv.org/abs/1903.08384
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00241
• S. Chawla, H. Fu, A. R. Karlin, Approximate Revenue Maximization in Interdependent Value Settings, EC 2014. https://doi.org/10.1145/2600057.2602858
• A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, EC 2018. https://arxiv.org/abs/1806.03865
• T. Roughgarden, I. Talgam-Cohen, Optimal and Robust Mechanism Design with Interdependent Values, ACM TEAC 4(3), 2016. https://doi.org/10.1145/2897185

Motivation

Proof-of-work blockchains such as Bitcoin pay a block reward to the miner that first solves a computational puzzle. The chance of winning is proportional to a miner's share of the total computing power (hash rate), so mining is a contest in which every miner pays for hash rate and the reward is split in proportion to it. Over time mining moved from general-purpose hardware to specialized chips, and this raised the question of whether access to better hardware concentrates mining in a few hands, which would weaken the decentralization the protocol relies on for security. Arnosti and Weinberg (arXiv:1811.08572) showed that cost asymmetries alone already concentrate mining in a proportional-share contest.

Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021; published in Management Science, 2023) model this as a two-stage game. Miners first decide how much to invest in the newest hardware, which lowers their cost per unit of hash rate. They then compete in the mining stage. Their Proposition 5.1 describes the equilibrium of the investment stage: which miners invest, how much, and how the number of active miners depends on the fixed cost of entering. This mission formalizes that result, corrected where the printed statement is false.

Setting

There are $N\ge2$ miners. Miner $i$ starts with a cost-per-hash $\tilde c_i$, sorted so that $\tilde c_1\le\dots\le\tilde c_N$. The newest hardware has cost-per-hash $\tilde c_0$, with $0<\tilde c_0<\tilde c_i$ for every $i$. In the first stage miner $i$ replaces a fraction $\beta_i\in[0,1]$ of its hardware, which leaves it with cost-per-hash

$$c_i(\beta_i)=\tilde c_i-\beta_i(\tilde c_i-\tilde c_0)+\frac{\eta(\tilde c_i-\tilde c_0)}{2}\beta_i^2,$$

where $\eta\ge0$ measures adjustment costs ((3.1)–(3.2)). Write $\bar\beta=\min\{1/\eta,1\}$, read as $1$ when $\eta=0$.

In the second stage, the mining stage, miner $i$ chooses a hash rate $h_i\ge0$. With $H=\sum_jh_j$, its payoff is

$$\pi_i=\frac{h_i}{H}R-c_ih_i-\frac{\gamma}{2}h_i^2-K\,\mathbf 1\{i\notin A(0),\ \beta_i>0\}\quad(H>0),\qquad \pi_i=0\quad(H=0),$$

with reward $R>0$, capacity parameter $\gamma\ge0$ and fixed entry cost $K>0$ ((3.4)). An equilibrium hash rate profile $h^*(\beta)$ is a profile from which no miner gains by changing its own hash rate (Definition 3.2(i)). Proposition 4.1 of the paper shows that it exists and is unique, and posing that result is the subject of mission 1 of this series. The active set is $A(\beta)=\{i:h^*_i(\beta)>0\}$, and $A(0)$ is the set of miners active without investment. The entry cost $K$ is paid by a miner outside $A(0)$ that invests.

An equilibrium investment $\beta^*\in[0,1]^N$ is a profile from which no miner can raise its payoff by changing $\beta_i$, the mining stage being replayed at the new profile (Definition 3.2(ii)). The threshold profile $\beta^{(n)}$ invests $\bar\beta$ in miners $1,\dots,n$ and $0$ in the others; this is the form (5.1).

Formalization targets

Goal: Proposition 5.1, corrected

Assume $K$ is generic: no potential entrant's gross mining profit at $\beta^{(i)}$ equals $K$. Then:

1. there is exactly one $n\in\{2,\dots,N\}$ for which $\beta^{(n)}$ is an equilibrium investment, and at it exactly $n$ miners are active and $A(0)\subseteq A(\beta^{(n)})$;
2. every equilibrium investment $\beta^*$ satisfies $A(0)\subseteq A(\beta^*)$ and $\beta^*_i=\bar\beta$ for every $i\in A(0)$;
3. $n$ is nonincreasing in $K$:

$$K\le K'\ \Longrightarrow\ n(K')\le n(K).$$

Milestones

• Proposition B.1: at a fixed set of $n$ active miners, $\partial\pi^*_i/\partial c_i<0$ and $\partial\pi^*_i/\partial c_j>0$.
• (5.2): the cost reduction $c_i(0)-c_i(\bar\beta)$ equals $(\tilde c_i-\tilde c_0)/(2\eta)$ for $\eta>1$ and $(1-\eta/2)(\tilde c_i-\tilde c_0)$ for $\eta\le1$, and $\bar\beta$ uniquely minimizes $c_i$ on $[0,1]$.
• Best responses (p. 44): at every equilibrium investment, active miners invest $\bar\beta$ and inactive ones invest $0$.
• Order preservation (p. 45): for $\eta>0$, investing $\bar\beta$ preserves the strict order of costs.
• Participation at $|A(0)|$ (p. 45): after miners $1,\dots,|A(0)|$ invest, the participation inequality of Proposition 4.4 holds for miner $|A(0)|$.

Significance

The result says three things about the effect of hardware upgrades on decentralization. Incumbents never drop out: every miner active before investment invests the cost-minimizing amount and stays active. Entry is ordered: in the threshold equilibrium the miners that enter are the most efficient ones. A higher fixed cost of entry admits weakly fewer miners. The paper's later propositions (5.2–5.5), which describe how hash rates and shares move after investment, start from this equilibrium.

Formalizing it adds two things. First, a machine-checked statement of what is actually true. The printed uniqueness is false, and the corrected statement separates what holds for every equilibrium from what holds within the threshold family. Second, a formal two-stage game in which the second stage is replayed at every deviation of the first, through an explicit equilibrium selection. None of the results of the paper has been formalized before; the platform has no contest or rent-seeking game.

Difficulty

The printed proof argues that an active miner's profit decreases in its own cost "irrespective of the cost parameters of other miners", citing Proposition B.1. Proposition B.1 is a derivative at a fixed set of active miners. Investment can change that set, so the proof needs a global monotonicity of the equilibrium profit across changes of the active set, in the own cost and in the presence of rivals. That step is not in the paper.

The obvious uniqueness argument also fails. Take two potential entrants with nearly equal initial costs and room in the market for only one of them. Either one can enter while the other stays out, and both profiles are equilibria. The numbers are $\tilde c=(1.074,1.419,2.914,2.923)$, $\tilde c_0=0.31$, $\eta=0.5$, $\gamma=0.5$, $R=1$ and any $K\in(0.0168,0.0308)$: both $(1,1,1,0)$ and $(1,1,0,1)$ are equilibrium investments. So no proof can rest on "a miner never invests while a cheaper one does not", which the paper asserts on p. 45.

Formalization scope

Miners are Fin N and 0-based: Lean miner i is the paper's miner $i+1$. Hash rates, costs and parameters are real numbers. The mining stage is defined for an arbitrary cost vector, not assumed sorted, because investment can reorder costs. The equilibrium property "$=\sup$" is written as "no deviation is profitable", over $h_i\ge0$ and over $\beta_i\in[0,1]$. The mining equilibrium enters as a selection $h^*$ with the hypothesis that $h^*(\beta)$ is an equilibrium hash rate profile for every $\beta\in[0,1]^N$. Proposition 4.1 makes it unique; it is not defined by a closed form. The fixed cost enters only the investment stage, inside the $H>0$ branch of (3.4). Derivatives are HasDerivAt statements along one coordinate. "Decreasing" is weak, as in the paper's footnote 12.

The goal is the corrected Proposition 5.1. The printed uniqueness among all investment profiles is not posed, and neither is the p. 45 claim that a miner cannot invest while a cheaper miner does not. Both are false by the instance above. Three hypotheses are added to the paper's: $\tilde c_0>0$; $\tilde c_0<\tilde c_i$ for every $i$ (the paper allows equality, under which $c_i$ is constant and every $\beta_i$ is a best response); and the genericity of $K$, which excludes finitely many values. Without the selection hypothesis the goal would be about an arbitrary function. Without the existence in part 1 the "every equilibrium" clause could be vacuous. Both are in the statement, so neither trivialization is available.

A complete development needs the mining-stage results of mission 1 of this series: existence and uniqueness of the mining equilibrium (Proposition 4.1) and the participation condition (Proposition 4.4). Since one draft cannot import another, this mission redefines the mining stage in its own namespace PoWMining.Investment. The new work is a global comparative-statics argument for the mining equilibrium across changes of the active set. It is reusable for any proportional-share contest with convex costs. Contributions are welcome on the milestones in any order, on that global monotonicity, and on the existence half of part 1.

Selected references

• A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint arXiv:2106.09783v1, 2021 (Proposition 5.1 p. 21, proofs pp. 43–46). https://arxiv.org/abs/2106.09783v1
• N. Arnosti, S. M. Weinberg, Bitcoin: A Natural Oligopoly, Innovations in Theoretical Computer Science (ITCS), 2019. https://arxiv.org/abs/1811.08572

Motivation

Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.

A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter $\gamma$, which measures how quickly a miner's operating cost grows with its scale, and the mining reward $R$. The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.

Setting

There are $n \ge 2$ active miners, indexed $i = 1, \dots, n$, with costs per hash $0 < c_1 \le c_2 \le \dots \le c_n$ (sorted, without loss of generality), a reward $R > 0$ and a capacity parameter $\gamma > 0$. Miner $i$ choosing hash rate $h_i$ earns $(h_i/H)R - c_ih_i - (\gamma/2)h_i^2$, where $H = \sum_j h_j$ is the aggregate hash rate (the paper's (3.4)). The cumulative cost is $c^{(n)} = c_1 + \dots + c_n$.

In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of $\gamma H^2 + c^{(n)}H - (n-1)R = 0$, and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:

$$g = g(c_1,\dots,c_n,\gamma,R) = \frac{\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} - c^{(n)}}{2\gamma},\qquad f_i = f_i(c_1,\dots,c_n,\gamma,R) = g\,\frac{R - c_i g}{R + \gamma g^2},$$

with $H^* = g$ and $h^*_i = f_i$. Miner $i$ is active exactly when $R - c_i g > 0$. The hash rate share of miner $i$ is $h^*_i/H^*$.

The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For $x \in \{\gamma, R\}$, (B.4) splits the derivative of $h^*_i$ into a direct part, $\Delta^{(x)}_{i,1} = \partial f_i/\partial x$ with $g$ held fixed, and an indirect part through the aggregate, $\Delta^{(x)}_{i,2} = (\partial f_i/\partial g)(\partial g/\partial x)$.

Formalization targets

Goal: Proposition 4.8 (p. 20)

For every active miner $i$,

$$\frac{\partial h^*_i}{\partial\gamma} = \Delta^{(\gamma)}_{i,1}+\Delta^{(\gamma)}_{i,2},\quad \Delta^{(\gamma)}_{i,1}<0,\quad \Delta^{(\gamma)}_{i,2}>0 \iff \frac{h^*_i}{H^*}<\frac12,$$ $$\frac{\partial h^*_i}{\partial R} = \Delta^{(R)}_{i,1}+\Delta^{(R)}_{i,2} > 0,\quad \Delta^{(R)}_{i,1}>0,\quad \Delta^{(R)}_{i,2}<0 \iff \frac{h^*_i}{H^*}<\frac12,$$

and the derivatives of $h^*_i/H^*$ with respect to $\gamma$ and to $R$ are increasing in $i$, for $1 \le i \le n$.

Milestones (the steps of the appendix proof)

1. (B.2), p. 39: $\partial H^*/\partial\gamma = -(H^*)^2/(c^{(n)}+2\gamma H^*) < 0$ and $\partial H^*/\partial R = (n-1)/(c^{(n)}+2\gamma H^*) > 0$.
2. p. 40: $\partial f_i/\partial\gamma = -g^3(R-c_ig)/(R+\gamma g^2)^2 < 0$ and $\partial f_i/\partial R = g^2(c_i+\gamma g)/(R+\gamma g^2)^2 > 0$.
3. (B.4), pp. 40–41: closed forms of $\partial h^*_i/\partial\gamma$ and $\partial h^*_i/\partial R$.
4. (B.6), pp. 42–43: closed forms of the share derivatives, and the p. 43 rewrites in which $i$ enters only through $f_i$ and $c_i + \gamma f_i$.

Significance

The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger $\gamma$ lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the $\gamma$ and $R$ columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).

Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the $\gamma$ and $R$ directions, the sign analysis, and the monotonicity in $i$. The proof text on p. 43 says "decreasing in $i$" where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).

Difficulty

Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate $g$ is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity $\gamma g^2 + c^{(n)}g = (n-1)R$, i.e. $\sqrt{(c^{(n)})^2+4(n-1)R\gamma} = c^{(n)} + 2\gamma g$, and the first-order identity $c_i + \gamma f_i = (R/g)(1 - f_i/g)$. The sign of the indirect parts is not visible from the raw derivative: it requires rewriting $\partial f_i/\partial g$ so that the threshold $f_i/g = 1/2$ appears. The positivity of $\partial h^*_i/\partial R$ needs a separate bound, since its indirect part can be negative. The monotonicity in $i$ is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on $f_i$ (decreasing in $i$) from that on $c_i + \gamma f_i$ (increasing in $i$), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.

Formalization scope

Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner $i+1$, so "increasing in $i$" is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost ($c^{(n)}$), gH ((4.1)/(B.3), with both branches of (4.1)), fH ($f_i$ with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: $n\ge2$, $R>0$, $\gamma>0$, $c_k>0$, costs sorted, and $R - c_kg > 0$ for every $k$ (all $n$ miners active). The condition $\gamma > 0$ is the paper's: (B.3) defines $g$ only for $\gamma>0$. The definition Sensitivities defines the four $\Delta$'s as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.

The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That $f_i$ and $g$ are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and $\partial f_i/\partial g$ are posed in mission 2. This mission uses those identities but does not pose them.

Trivializing formalizations are ruled out: the $\Delta$'s are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with $c = (1,1)$, $\gamma = 1$, $R = 3$ give $g = 1$, $h^*_i = 1/2$); and the monotonicity is stated for derivatives asserted to exist.

Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for $g$ (the root identity, positivity, $c^{(n)}+2\gamma g > 0$) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.

Selected references

• A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint, 2021. https://arxiv.org/abs/2106.09783v1
• G. Tullock, The Welfare Costs of Tariffs, Monopolies, and Theft, Western Economic Journal 5(3), 224–232, 1967 (the rent-seeking model the paper builds on). https://doi.org/10.1111/j.1465-7295.1967.tb01923.x
• S. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. https://bitcoin.org/bitcoin.pdf

Motivation

In an auction with interdependent values, a bidder's value can depend on information held by other bidders. An estimate of a shared resource's usefulness, for example, may improve when another participant reports a stronger signal. The auctioneer must decide whom to serve using reported signals, while each participant has an incentive to report a signal that improves her allocation or payment. This combination makes a welfare guarantee and truthful reporting harder to obtain together than in a setting where each bidder's value depends only on her own information. Eden, Feldman, Fiat, Goldner, and Karlin study this problem under a diminishing-returns condition on signals and give mechanisms for several allocation settings in their arXiv preprint, §§1–4.

This mission concerns their single-parameter, downward-closed setting. Each agent either receives service or does not; the feasible groups of served agents are specified in advance. The result gives a direct welfare guarantee for a randomized allocation rule whose deterministic components can each be paired with truthful payments. It is one of four separate missions drawn from the same preprint. The source here is arXiv:1903.08384v2, dated June 2019; theorem labels and pages in this mission refer to that preprint, not to the 2024 Mathematics of Operations Research version.

Setting

There are $n$ agents. Agent $i$ has a signal $s_i\in\mathbb R_+=[0,\infty)$, and a complete profile is $s=(s_1,\ldots,s_n)$. If served, agent $i$ receives value $v_i(s)\ge0$. The value is weakly increasing in each coordinate and strictly increasing in agent $i$'s own signal. A family $\mathcal I$ of subsets of agents is downward closed when every subset of a feasible set is feasible. The welfare of a feasible served set $S$ at the true profile is $\sum_{i\in S}v_i(s)$. These conventions come from Definitions 2.1–2.2 and §4 of the source.

A function $v$ is $d$-submodular over signals, or $d$-SOS, when increasing coordinate $j$ by the same nonnegative increment yields at most $d$ times as much extra value at a larger profile of the other coordinates as at a smaller one. For $d=1$ this is called SOS. This condition compares marginal gains from one signal while holding that signal's starting value fixed. It is the condition in Definition 2.13 of the preprint, p. 11.

The Random Sampling Vickrey mechanism, RS-V, chooses a uniformly random partition of agents into $A$ and $B$. For each $i\in B$, it computes the proxy weight $w_i=v_i(s_A,s_i,0_{B\setminus\{i\}})$ from the reported profile: it keeps the signals in $A$ and agent $i$'s own signal, and sets the other signals in $B$ to zero. It then serves a feasible subset $S\subseteq B$ maximizing $\sum_{i\in S}w_i$. Its true welfare is the sum of $v_i(s)$ for the served agents, evaluated at the true profile. The mechanism is specified in §4, p. 14 of the preprint.

For a deterministic allocation and payment rule, ex-post incentive compatibility means that, when all other agents report truthfully, no agent can gain by changing her own report. Ex-post individual rationality means that truthful participation gives nonnegative utility. Utility uses the true value of the allocation and the payment determined by reports. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support has these properties, as in Definitions 2.3–2.8 of the preprint, pp. 9–10.

Formalization targets

Main theorem

For every downward-closed $\mathcal I$, every $d$-SOS valuation family meeting the setting above, and every feasible maximizing selector used to break RS-V ties, each partition component admits ex-post IC-IR payments, and for every $S\in\mathcal I$ and signal profile $s$,

$$\sum_{i\in S}v_i(s)\ \le\ 2(d+1)\,\mathbb E_B\!\left[\sum_{i\in x_B(s)}v_i(s)\right].$$

Here $x_B(s)$ is the set served by RS-V with candidate set $B$. At $d=1$, the factor is $4$. This is Theorem 4.1, p. 14 of the preprint. The universal payment claim reads the theorem alongside its proof and the paper's definition of universal ex-post IC-IR.

Supporting results

The milestones follow the paper's stated results: Proposition 2.1 characterizes which deterministic allocation rules admit ex-post IC-IR payments; the opening of §4 states monotonicity of RS-V's allocation; Lemma 2.3 extends the $d$-SOS marginal bound to a set of signal coordinates; Lemma 3.1 bounds value after randomly zeroing the other agents' signals; and display (4) specializes that expectation to one RS-V proxy weight. Each has its own source quote and page in the milestone list.

Significance

The theorem says that a mechanism that only sees reported signals can remain truthful component by component while obtaining welfare within a factor determined by the SOS parameter. The guarantee compares against every feasible allocation at the true profile, so it applies to the optimal welfare without requiring a separately chosen optimum in the statement. The same preprint uses the random-zeroing estimate beyond this single-parameter mechanism, including in its combinatorial-auction sections Eden et al., §§3–6.

The theorem and supporting results are proved on paper. This mission asks for machine-checked proofs of their stated formalizations. A complete development will also provide reusable definitions for signal profiles, SOS valuations, ex-post incentives, finite random-partition averages, and allocation selectors. No machine-checked proof is claimed by this proposal.

Difficulty

The agent's value depends on reports from other agents, so maximizing reported welfare directly does not by itself give an ex-post incentive guarantee. RS-V instead allocates using proxy values, which raises a second issue: high proxy welfare need not equal high true welfare for a particular partition. The central mathematical task is to control the loss caused by zeroing signals in a uniform random partition. The incentive claim also needs to hold for every maximizing tie choice, rather than for a specially chosen selector. These are the obstacles behind the source's separate monotonicity and random-zeroing statements Eden et al., §§3–4.

Formalization scope

Agents are Fin n, with arbitrary finite $n$; signals are nonnegative real numbers, including zero, and valuations and payments are real valued. A served set is a Finset, and feasibility is a downward-closed set of such sets. The selector is a function of the reported profile and the partition, constrained to return a feasible maximizer among subsets of $B$. Every such selector is covered. Payments for a partition are functions of reports alone. The random choice of $B$ is the finite uniform average over all $2^n$ subsets, while Lemma 3.1 averages over all $2^{n-1}$ subsets of the other agents when an agent $i$ exists. Welfare uses true values, not proxy weights.

The printed Definition 2.1 says the value of agent $j$ is strictly increasing in $s_i$; the formalization reads this as agent $j$'s own signal. The symbol $\mathbb R_+$ includes zero because the mechanism sets signals to zero. The printed Lemma 3.1 omits a range for $d$; its standalone statement adds $d\ge0$, since it is false for negative $d$ near zero. Theorem 4.1 needs no separate bound on $d$, because its strict own-signal monotonicity and $d$-SOS hypothesis already imply $d\ge1$ for a nonempty agent set. The formalization excludes vacuous selectors by requiring the returned set to be feasible and to maximize the specified proxy objective. These choices and their source locations are recorded in the moderation notes.

Contributions may establish the SOS lemmas, the monotone-allocation and payment characterization, and the final finite-average welfare bound. The basic definitions and finite averaging infrastructure can be reused in the later missions of this preprint once the separately drafted models are consolidated.

Selected references

• Alon Eden, Michal Feldman, Amos Fiat, Kira Goldner, and Anna R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. Preprint.

Motivation

Many allocation problems divide work, not goods: shifts among employees, teaching loads among faculty, cleaning duties among housemates, maintenance tasks among the owners of a shared resource. For divisible goods the standard fair and efficient solution is the competitive rule (competitive equilibrium from budgets): give every agent a budget, find prices at which every agent demands what she receives, and the outcome is Pareto optimal and envy-free (weighted by budgets). For goods with additive utilities this rule is single-valued and is the solution of the Eisenberg–Gale convex program, which yields polynomial-time algorithms.

For chores (bads) the competitive rule keeps its fairness and efficiency guarantees but loses the convex structure: Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (BMSY17) showed it is generally multi-valued, with competitive allocations corresponding to critical points, not maximizers, of the Nash social welfare on the Pareto frontier. Brânzei and Sandomirskiy (arXiv:1907.01766v2, Mathematics of Operations Research, 2024) enumerate all competitive utility profiles in strongly polynomial time when the number of agents or the number of chores is fixed. Their counting result is the target of this mission.

Setting

There are $n$ agents and $m$ divisible chores, one unit of each. Agent $i$'s value for one unit of chore $j$ is $v_{i,j}<0$, and her budget is $b_i<0$. A feasible allocation is $z\in\mathbb R^{n\times m}_{\ge0}$ with $\sum_i z_{i,j}=1$ for every chore $j$; agent $i$'s utility is $u_i(z_i)=\sum_j v_{i,j}z_{i,j}$, the utility profile is $u(z)=(u_1(z_1),\dots,u_n(z_n))$, and $\mathcal U(v)$ is the set of utility profiles of feasible allocations.

A feasible allocation $z$ is competitive for budgets $b$ if there are prices $p\in\mathbb R^m_{<0}$ such that for every agent $i$ the bundle $z_i$ costs $p(z_i)=\sum_j p_jz_{i,j}\le b_i$ and maximizes $u_i$ among all bundles $x\ge0$ with $p(x)\le b_i$. A competitive utility profile is $u(z)$ for a competitive $z$.

$z$ is Pareto optimal if no feasible allocation makes every agent weakly better off and some agent strictly better off; the Pareto frontier $\mathcal U^*(v)$ consists of their utility profiles. For weights $\tau\in\mathbb R^n_{>0}$ the face $f_\tau$ of the Pareto frontier is the set of maximizers of $\langle\tau,u\rangle=\sum_i\tau_iu_i$ over $u\in\mathcal U(v)$.

The proof runs through graphs. The consumption graph $G_z$ links agent $i$ and chore $j$ when $z_{i,j}>0$. The maximal weighted welfare (MWW) graph $G_\tau(v)$ links $i$ and $j$ when $\tau_i|v_{i,j}|\le\tau_{i'}|v_{i',j}|$ for every agent $i'$. A family of graphs is rich if every Pareto optimal profile in $\mathbb R^n_{<0}$ is $u(z)$ for a feasible $z$ whose consumption graph is in the family. Along a path $\mathcal P=(i_1,j_1,\dots,i_L,j_L,i_{L+1})$ the product of disutilities is $\pi(\mathcal P)=\prod_{k=1}^L|v_{i_k,j_k}|/|v_{i_{k+1},j_k}|$.

Formalization targets

Goal: Corollary 25 (p. 27)

For $n,m\ge1$, $v\in\mathbb R^{n\times m}_{<0}$ and $b\in\mathbb R^n_{<0}$,

$$\#\{f\text{ face of the Pareto frontier}: f\cap\mathbb R^n_{<0}\ne\emptyset\}\le B,\qquad \#\{\text{competitive utility profiles for } b\}\le B,$$ $$B=\min\Big\{(2m-1)^{\frac{n(n-1)}{2}},\ (2n-1)^{\frac{m(m-1)}{2}}\Big\}.$$

Milestones

1. Lemmas 36–38 (pp. 50–51): competitive allocations are characterized by the maximal bang-per-buck condition with budget exhaustion; prices satisfy $p_j=v_{i,j}b_i/u_i(z_i)$ on consumed chores; competitiveness is equivalent to inequalities (14) and to weighted-welfare maximality with weights $b_i/u_i(z_i)$.
2. Theorem 9 and Corollary 10 (p. 14): the first and second welfare theorems, and Pareto indifference.
3. Lemma 14 (p. 17): Pareto optimality $\iff$ no simple profitable trading cycle $\iff$ $G_z\subseteq G_\tau(v)$ for some $\tau>0$ $\iff$ weighted-welfare maximality. Corollary 15 is included as a companion statement.
4. Lemma 18, Lemma 19, Corollary 21 (pp. 21–23): faces correspond to MWW graphs; MWW graphs, and those with no lonely agents, form rich families; the latter correspond to the faces meeting $\mathbb R^n_{<0}$.
5. Lemma 22 (p. 23): $\mathrm{MWW}_{non\text{-}lonely}(v)=\mathrm{MWW}_{non\text{-}lonely}(v^T)$.
6. Lemma 23, first bullet (p. 24): a rich family of at most $B$ graphs exists.
7. Lemma 26 (p. 29): a competitive profile is determined by its consumption graph through formula (4).

Significance

The result. Corollary 25 says that the competitive rule for chores, although multi-valued and non-convex, has at most polynomially many outcomes when $n$ or $m$ is fixed, and that the Pareto frontier has polynomially many faces meeting the negative orthant. It is the exact mathematical content of the paper's algorithmic Theorem 17: an enumeration that tries every graph of a rich family and recovers at most one candidate profile from each cannot miss a competitive profile and cannot produce more than $B$ of them. For $n=2$ the bound $2m-1$ is attained in Example 1 of the paper by the face count.

Formalizing it. The result is proved in the paper; nothing is known to be machine-checked. The mission builds a reusable layer for linear Fisher-type economies with bads: the competitive rule with negative prices and budgets, welfare theorems, the trading-cycle and weighted-welfare criteria of Pareto optimality, and the graph-theoretic description of the faces of a polytope of feasible utilities. Lemma 14 and Lemma 18 are of independent use for any linear allocation model.

Difficulty

The obvious argument for goods, uniqueness of the equilibrium utility profile via a strictly concave program, fails: for chores there may be several competitive profiles, even on a single closed face (in Example 1 of the paper, both competitive profiles lie on one edge of the frontier). The count must therefore pass through combinatorics. Two steps carry the weight. First, the faces of the Pareto frontier, a continuous object, must be put in bijection with a finite set of graphs, and the graphs must be chosen so that each competitive profile is realized by an allocation whose consumption graph is exactly an MWW graph, not merely contained in one. Second, the size bound cannot come from counting bipartite graphs, which gives only $2^{nm}$; it has to exploit the structure of MWW graphs, and its second term, polynomial in $n$ for fixed $m$, requires the agent–chore symmetry of Lemma 22, whose natural route goes through the second welfare theorem.

Formalization scope

Agents are Fin n, chores Fin m (0-based); values, budgets and prices are real functions; graphs are Finset (Fin n × Fin m) of edges; a path is a record of its length $L$, $L+1$ agents and $L$ chores. Faces are the sets of maximizers of $\langle\tau,u\rangle$ over $\mathcal U(v)$ for $\tau\in\mathbb R^n_{>0}$, the dual representation of p. 16. Counts are Set.encard in $\mathbb N\cup\{\infty\}$ and the bound $B$ is computed in $\mathbb N$. Added relative to the paper: $n\ge1$ and $m\ge1$ (the paper's sets of agents and chores are non-empty) where a statement needs them. Not formalized: the running-time claims (Theorem 17, the second bullet of Lemma 23), item 4 of Lemma 38 (critical points of the Nash social welfare), and the sentence on p. 27 that each face carries at most one competitive profile, which is false for closed faces.

The following formalizations would trivialize the goal and are ruled out: a competitive allocation without the budget constraint $p(z_i)\le b_i$; non-negative values, budgets or prices; faces exposed by $\tau\ge0$ or by $\tau$ of arbitrary sign; counts over sets assumed finite; Pareto optimality restricted to a subclass of allocations.

All definitions live in CompetitiveChores.RichFamily; Mathlib supplies only finite sums and products, Finset, and Set.encard. Contributions welcome: proofs of the appendix lemmas (pure linear algebra on finite sums), of Lemma 14 (the cycle-cancelling argument of Appendix B), and of the two-agent splits-and-cuts count inside Lemma 23.

Selected references

• S. Brânzei and F. Sandomirskiy, Algorithms for Competitive Division of Chores, arXiv:1907.01766v2 (2023); Mathematics of Operations Research (2024). https://arxiv.org/abs/1907.01766v2
• A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Competitive division of a mixed manna, Econometrica 85(6), 2017. https://doi.org/10.3982/ECTA14438
• A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Dividing bads under additive utilities, Social Choice and Welfare 52, 2019. https://doi.org/10.1007/s00355-018-1157-x
• N. Devanur, C. Papadimitriou, A. Saberi and V. Vazirani, Market equilibrium via a primal–dual algorithm for a convex program, Journal of the ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack $\varepsilon$. Approximate incentive compatibility ($\varepsilon$-IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.

Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With $\varepsilon$-IC the feasible set grows, and the paper determines the order of the additional revenue as $\varepsilon\downarrow 0$.

Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an $\varepsilon$-IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by $O(\sqrt\varepsilon)$ for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only $\Theta(\varepsilon)$ (Theorem 2), and give a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.

Setting

A seller sells one item to one buyer. The buyer's value $v$ has a cumulative distribution function $F$ with density $f$ supported on $S=[0,\bar v]$, $\bar v>0$. Assumption 1 requires $f$ to have bounded variation on $S$. Write $\bar F=1-F$, the revenue curve $R(v)=v\,\bar F(v)$ (the revenue of a posted price $v$), and $\dot R(v)=\bar F(v)-v f(v)$.

A direct mechanism $m=(x,t)$ gives a buyer who reports $v$ the item with probability $x(v)\in[0,1]$ and charges $t(v)$. It is individually rational (IR) if $v\,x(v)-t(v)\ge 0$ for all $v\in S$, and $\varepsilon$-incentive compatible (IC$_\varepsilon$) if

$$v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S.$$

$\mathcal M(\varepsilon)$ is the set of IR and IC$_\varepsilon$ mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$. A best reporting mapping $v^\star$ for $m$ picks, for each value $v$, a report in $\arg\max_{w\in S}\{v\,x(w)-t(w)\}$.

Local $\alpha$-power envelopes (Definition 1): $R$ has a unique maximizer $p^\star$ on $S$, interior, and there are $\alpha>1$, $\kappa_L,\kappa_U>0$ and $\ell>0$ with $(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ and

$$\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\,\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\quad\text{on }(p^\star-\ell,p^\star+\ell).$$

The parameter $\alpha$ measures how flat $R$ is at its peak; $\alpha=2$ is the generic smooth case.

Perturbed delayed mechanisms (§5.1). For $\mu,\delta>0$ the buyer is steered to report $v^\star(v\,|\,\mu,\delta)$, equal to $0$ below $p^\star-\delta$, to $v-\mu$ on $[p^\star-\delta,p^\star+\delta+\mu]$, and to $p^\star+\delta$ above. With $w$ its generalized inverse, the allocation $x_{pd}$ solves on $[0,p^\star+\delta]$ the ordinary and delay differential equations

$$\dot x(v)=\frac{x(v)}{w(v)-v}\ \ (v\le p^\star-\delta),\qquad x(0)=\frac{\varepsilon}{p^\star-\delta},\qquad \dot x(v)=\frac{x(v)-x(v^\star(v))}{w(v)-v}\ \ (p^\star-\delta\le v\le p^\star+\delta),$$

is $1$ above $p^\star+\delta$, and the payment $t_{pd}$ is given explicitly in terms of $x_{pd}$ and $v^\star$.

Formalization targets

Goal: Theorem 3 (p. 27)

Under Assumption 1 and local $\alpha$-power envelopes there are $C>0$ and $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ some $m\in\mathcal M(\varepsilon)$ satisfies

$$\Pi(m)\ \ge\ \Pi^\star(\mathcal M(0))+C\,\varepsilon^{\alpha/(2\alpha-1)} .$$

The constants may depend on the distribution, but not on $\varepsilon$.

Milestones

1. Lemma 5 (p. 59): solutions of (ODE)-(DDE) are non-decreasing on $[0,p^\star+\delta]$.
2. Proposition 3 (p. 31): if $x_{pd}(v)\to 1$ as $v\uparrow p^\star+\delta$, then $v^\star(\cdot\,|\,\mu,\delta)$ is a best reporting mapping for $m_{pd}$.
3. Proposition 4 (p. 33): the system has a unique solution on $[0,p^\star+\delta]$, which is positive, non-decreasing and given in closed form (eq. (25)).
4. Lemma 6 (p. 60): with $\Gamma(t)=\sum_{j=0}^{\lfloor t\rfloor+1}\frac{(-1)^je^{-j}}{j!}(t+1-j)^j$,

$$2(t+1)e^{-1}e^{-t}<\Gamma(t)\le2(t+2)e^{-(t+1)}\qquad(t\ge0).$$

5. Proposition 5 (p. 34): for $\mu>\varepsilon e$ some $\delta\in[\mu^2/(4\varepsilon)-\mu,\ \mu^2/(4\varepsilon)]$ makes $x_{pd}$ reach $1$ at $p^\star+\delta$, and then $m_{pd}\in\mathcal M(\varepsilon)$.
6. Proposition 6 (p. 35): the revenue identity

$$\Pi(m_{pd})=\int_0^{p^\star+\delta}x_{pd}(v)\big(vf(v)-\bar F(v+\mu)\dot w(v)\big)dv+R(p^\star+\delta)+\int_{p^\star+\delta}^{p^\star+\delta+\mu}\bar F(v)\,dv .$$

Significance

The result. Theorem 3 shows that the $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound of Theorem 1 is tight up to the logarithm. Since $\alpha/(2\alpha-1)<1$ for $\alpha>1$, the revenue gain from approximate incentive compatibility is supralinear in $\varepsilon$: a seller who exploits $\varepsilon$-optimizing buyers gains strictly more than the order-$\varepsilon$ gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature $\alpha$ of the revenue curve at the optimal price determines the exponent, which ranges from $1$ (as $\alpha\downarrow1$) to $1/2$ (as $\alpha\to\infty$), the latter matching Nisan's universal bound.

Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of $\varepsilon$-IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on $\Gamma$, which the paper derives from the renewal function of uniform interarrival times.

Difficulty

The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order $\varepsilon$ (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples $x(v)$ to $x(v-\mu)$); choosing the delay $\delta$ so that the allocation reaches exactly $1$ at $p^\star+\delta$, which requires the sharp two-sided bound on $\Gamma$ and an intermediate value argument; and verifying global $\varepsilon$-IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain $\bar F(p^\star+\delta+\mu)\,\mu$ against losses of order $\kappa_U(\delta+\mu)^\alpha$, with $\mu$ of order $\varepsilon^{\alpha/(2\alpha-1)}$.

Formalization scope

Values are reals, every function is a total function $\mathbb R\to\mathbb R$ whose values matter only on $S=[0,\bar v]$, and the density is integrable on $S$ with total mass $1$. Mechanisms are required to be measurable, which the expectation $\mathbb E_v[t(v)]$ presumes. $\Pi^\star$ is a supremum (sSup); the goal is stated with an explicit witness $m\in\mathcal M(\varepsilon)$, which is equivalent because the revenue image is nonempty and bounded above by $\bar v$. $\dot R$ is defined as $\bar F-vf$, not as a derivative. The $\Omega$ constants are quantified after the distribution and before $\varepsilon$.

The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At $p^\star-\delta$ the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.

Disclosed additions relative to the page: $\mu\le p^\star-\delta$ in the §5.1 statements (presumed by the paper's definition of $w$); Propositions 3–6 and Lemma 5 are stated for any price $p^\star$ with $0<\delta<p^\star$ and $p^\star+\delta+\mu<\bar v$, since their proofs never use optimality of $p^\star$; in Proposition 6 the integrand $\psi\cdot f$ is written in product form because $\psi$ divides by $f$.

A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and $\Gamma$ results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.

Selected references

• S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
• M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, FOCS 2005, 605–614. https://doi.org/10.1109/SFCS.2005.50
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
• P. Milgrom, I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
• R. D. Driver, Ordinary and Delay Differential Equations, Springer, 1977 (reprint 2012). https://doi.org/10.1007/978-1-4684-9467-9