Algorithmic Game Theory

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

Motivation

Green investors hold a growing share of financial wealth, and the stated purpose of much of this capital is to change how companies behave, not only to avoid exposure to climate risk. Whether exclusionary or impact-oriented portfolios actually move corporate emissions is an equilibrium question: investors' preferences shift the cost of capital, and companies choose emissions knowing this. De Angelis, Tankov and Zerbib, Climate Impact Investing (SSRN 3562534; Management Science 2022, doi:10.1287/mnsc.2022.4472), build a continuous-time model in which regular and green investors trade the shares of $n$ companies, green investors penalize climate externalities, and each company chooses an emission schedule to maximize its expected market value.

This mission formalizes the companies' side of that model: the reduction of each company's problem to a date-by-date payoff (Proposition 2), the explicit emission rate it yields when externalities depend on a company's own emissions (Corollary 3), and the equilibrium among companies when externalities also depend on the economy's average emissions (Proposition 4, §3.4 "Interaction effects"). The last result is the one the paper uses to argue that internalizing aggregate emissions pushes every company to emit less.

Setting

There are $n\ge1$ companies, a final date $T>0$ and a rate of time preference $\rho>0$. A schedule $\psi$ assigns to each date $s\in[0,T]$ the vector $\psi_s\in\mathbb R^n_+$ of emission rates. Company $i$ has a marginal abatement cost $c^i_s\ge0$. Green investors hold a wealth share $\alpha\in(0,1)$. The climate externalities $\theta^i_s(\psi_s)$ (as internalized by green investors) and $\theta^{c,i}_s(\psi_s)$ (as internalized by the companies) are functions of the whole emission profile.

Company $i$'s profit function is its discounted expected equilibrium price,

$$\mathcal J^i(\psi)=\int_0^T e^{-\rho t}\Big(d^i+\int_0^T c^i_s(\psi^i_s-\psi^i_b)\,ds+\int_0^t\theta^{c,i}_s(\psi_s)\,ds+\alpha\int_t^T\theta^i_s(\psi_s)\,ds-\gamma^*\int_t^T[\Sigma_s\mathbf 1]_i\,ds\Big)dt,$$

with $d$ the expected terminal dividends, $\psi_b$ the baseline emissions, $\gamma^*$ an aggregate risk-aversion constant and $\Sigma_s$ the dividend covariance. An optimal emission schedule (9) is a Nash equilibrium: no company raises $\mathcal J^i$ by changing its own schedule.

With the time factors

$$\beta^c_t=\frac{e^{-\rho t}-e^{-\rho T}}{1-e^{-\rho T}},\qquad\beta_t=\frac{1-e^{-\rho t}}{1-e^{-\rho T}},$$

the date-$t$ payoff (12) of company $i$ is $F_i(x)=\beta^c_t\theta^{c,i}_t(x)+\alpha\beta_t\theta^i_t(x)+c^i_tx^i$ for a profile $x\in\mathbb R^n$.

Without interaction, $\theta^i_t(x)=\kappa_{0,t}-\frac{\kappa_t}{2}(x^i)^2$ and similarly for $\theta^{c,i}$ with $\kappa^c$, where $\kappa_t,\kappa^c_t>0$ are sensitivities; the resulting rate is

$$\psi^{*,i}_t=\frac{c^i_t}{\beta^c_t\kappa^c_t+\alpha\beta_t\kappa_t}.\tag{13}$$

With an interaction effect of elasticity $\varepsilon\ge0$, the externalities become

$$\theta^i_t(\psi)=\kappa_{0,t}-\frac{\kappa_t}{2}\big[(\psi^i_t)^2+\varepsilon\psi^i_t\bar\psi_t\big],\qquad\bar\psi_t=\frac1n\sum_{j=1}^n\psi^j_t,$$

and similarly for $\theta^{c,i}$. The stage game at date $t$ has players $i=1,\dots,n$, strategies $x^i$ and payoffs $F_i$.

Formalization targets

Goal: Proposition 4(i)

For every $t\in[0,T]$, the stage game with interaction effect has exactly one Nash equilibrium, namely

$$\psi^{*,\varepsilon,i}_t=\psi^{*,i}_t-\frac{\varepsilon}{2n+\varepsilon}\Big(\psi^{*,i}_t+\frac{2n^2}{2n+(n+1)\varepsilon}\bar\psi^*_t\Big),\tag{15}$$

and it lies weakly below the schedule without interaction: $\psi^{*,\varepsilon,i}_t\le\psi^{*,i}_t$ for all $i$.

Milestones

1. (39): an integration by parts that rewrites the reduced objective as $\int_0^T$ of a weighted date-$t$ payoff, and the equivalence between maximizing $\mathcal J^i$ and the reduced objective.
2. Proposition 2: a schedule that maximizes (12) at every date is optimal for $\mathcal J^i$ against every admissible unilateral deviation.
3. Corollary 3: (13) is the unique maximizer of the date-$t$ payoff with own-emission externalities over $x\ge0$.
4. (40): a profile is a stage equilibrium if and only if $x^i=\psi^{*,i}_t-\frac{\varepsilon}{2n}\big(\sum_jx^j+x^i\big)$ for all $i$.
5. Sum identity: summing (40) gives $\sum_ix^i=\frac{2n}{2n+(n+1)\varepsilon}\sum_i\psi^{*,i}_t$.

Companions

• Proposition 4(ii): as $n\to\infty$ with $\psi^{*,i}_t,\bar\psi^*_t$ fixed, (15) tends to $\psi^{*,i}_t-\frac{\varepsilon}{\varepsilon+2}\bar\psi^*_t$ (16).
• Corollary 3 at schedule level: (13) is optimal for $\mathcal J^i$.
• Proposition 4 at schedule level: a nonnegative, admissible (15) satisfies the Nash condition (9) for the profit functions.

Significance

The result quantifies how a shared concern for aggregate emissions changes individual behaviour. Each company's emission falls by an amount proportional to its own no-interaction rate and to the economy's average, and in a large market the reduction is $\frac{\varepsilon}{\varepsilon+2}$ times the average emission. With $\varepsilon=1$, equal weight on own and average emissions, a company cuts its emissions by one third of the average (p. 30). The comparison with (13) is the paper's argument that interaction effects reinforce the impact of green investing.

Formalizing it makes the modelling layer precise: what "optimal schedule" means once the stochastic layer is evaluated, under which integrability conditions the integration by parts holds, and on which domain the equilibrium lives. The results are proved on the page with short arguments; none of them is machine-checked anywhere. The time-factor module is shared with the companion mission on climate uncertainty.

Difficulty

The algebra of (15) is short; the care lies elsewhere. First, the average $\bar\psi_t$ contains company $i$'s own emission, so the derivative of $\theta^i_t$ in $\psi^i_t$ includes the term $\varepsilon\psi^i_t/n$. Treating $\bar\psi_t$ as fixed, the mean-field reading, gives a different equilibrium, $\psi^{*,i}_t-\frac{\varepsilon}{2}\bar\psi_t$, which is not (15). Second, the page's proof imposes first-order conditions, which characterize equilibria of the game on $\mathbb R^n$, while the model's schedules are nonnegative and (15) can be negative (for instance when $c^i_t=0$ and $\varepsilon>0$). Third, Proposition 2 is an exchange of the order of integration on $\{0\le s\le t\le T\}$ that must be justified from integrability alone, without continuity of the schedule.

Formalization scope

The paper's model is stochastic: Brownian cash-flow news, subjective measures obtained by Girsanov's theorem, and CARA investors. None of this is formalized, and Propositions 1 and 5 are out of scope as equilibrium statements. The formal statements start from the companies' objective in the evaluated form of p. 64, the expected equilibrium price under the companies' measure.

Conventions committed to in Lean:

• Companies are indexed by Fin n with $n>0$; profiles are Fin n → ℝ; $\Sigma_s\mathbf 1$ is Matrix.mulVec (Sig s) 1, and only its $i$-th coordinate is used.
• Time factors, the quadratic externality and (13) live in the shared module TimeFactors. $\rho>0$ and $T>0$ are standing hypotheses; $\kappa_t,\kappa^c_t>0$ on $[0,T]$ (Corollary 3's standing assumption, inherited by Proposition 4 through (13)) and $c^i_t\ge0$ (implicit on the page) are disclosed. Positivity of $\kappa_{0,t},\kappa^c_{0,t}$ is not used and is dropped.
• A schedule is admissible for company $i$ if it is Borel measurable and nonnegative on $[0,T]$ and $c^i\psi^i$, $\theta^i(\psi)$, $\theta^{c,i}(\psi)$ are integrable there; $c^i$ and $[\Sigma\mathbf 1]_i$ are assumed integrable. Measurability is required by footnote 7; Lean encodes it through the schedule's zero extension outside $[0,T]$. Integrability is not on the page; without it the integrals would silently default to $0$.
• The page writes $d$ in $\mathcal J^i$ for the coordinate $d^i$.
• The goal's stage game is played on $\mathbb R^n$; this is a disclosed correction of the page's domain $\mathbb R^n_+$, which its own first-order proof does not respect. The schedule-level companion restores $\mathbb R_+$ under the proviso that (15) is nonnegative.
• "Lower" is the weak inequality: at $\varepsilon=0$ or $c\equiv0$ the two schedules coincide.
• Proposition 4(ii)'s "$\simeq$ for $n\gg\varepsilon$" is pinned down as a limit $n\to\infty$ with the no-interaction quantities held fixed.

A statement that assumes (40) or defines equilibrium as the solution of the first-order system would be trivial; the goal quantifies over all profiles and uses the Nash predicate, and no milestone assumes the conclusion of another.

The development needs interval integrals and Fubini on a triangle (both available in Mathlib's measure theory), and elementary algebra over Fin n sums. The profit-function layer and the stage-game predicates are reusable for other emission games built on the same model. Proofs of any item are welcome, as are proofs of the necessity direction of Proposition 2.

Selected references

• T. De Angelis, P. Tankov, O. D. Zerbib, Climate Impact Investing, SSRN 3562534, version of 25 June 2021. https://ssrn.com/abstract=3562534
• T. De Angelis, P. Tankov, O. D. Zerbib, Climate Impact Investing, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4472
• W. Nordhaus, Estimates of the Social Cost of Carbon: Concepts and Results from the DICE-2013R Model and Alternative Approaches, Journal of the Association of Environmental and Resource Economists 1(1/2), 2014. https://doi.org/10.1086/676035