Operations Research

Motivation

A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves positions empty; sending too many hires beyond capacity at a cost. This trade-off is the same as overbooking in revenue management (airline seats, hotel rooms), with the difference that candidates are heterogeneous in both value and acceptance probability.

Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three hiring-pipeline models through linear programming relaxations. This mission formalizes their lower bound for the third model, Simultaneous Offering (§3.3 and §6 of the paper). The question it answers is practical: how much is lost if the firm restricts itself to value-ordered policies, which send offers to the $m$ most valuable candidates for some $m$, instead of searching over all $2^n$ offer sets? Value-ordered policies are natural, because a firm rarely wants to withhold offers from its best candidates, and the optimal one is computable by a short dynamic program. The paper shows (Example 1, p. 25) that they can be arbitrarily bad in general, and that they are provably good when every candidate's value is bounded below.

Setting

An instance $I=(k,n,p,v)$ has $k$ positions and $n$ candidates, $1\le k\le n$. Candidate $i$ accepts an offer independently with probability $p_i\in[0,1]$ and then contributes value $v_i\ge0$. Candidates are labelled so that $v_1\ge v_2\ge\dots\ge v_n$. The firm chooses an offer set $S\subseteq[n]$; with $A\subseteq S$ the random set of acceptances, the reward is

$$\sum_{i\in A}v_i-\big[\,|A|-k\,\big]^+,$$

the cost per candidate hired beyond capacity being normalised to $1$. $\mathrm{OPT}_{\mathrm{sim}}(I)$ is the best expected reward over offer sets. For $\tau>0$ the instance is $\tau$-bounded, $I\in\mathcal I^\tau_{\mathrm{sim}}$, if $v_i\ge\tau$ for all $i$; the interesting range is $\tau\in(0,1)$, since for $\tau\ge1$ offering to everyone is optimal.

The benchmark is the LP relaxation

$$\mathrm{LP}_{\mathrm{sim}}(I)=\max_{y,z}\ \sum_{i}v_ip_iy_i+z\quad\text{s.t.}\quad z\le k-\sum_ip_iy_i,\ \ z\le0,\ \ 0\le y_i\le1,$$

which charges the overage cost on the expected number of hires. Write $V_{\mathrm{high}}=\{i:v_i>1\}$ and $P_{\mathrm{high}}=\sum_{i\in V_{\mathrm{high}}}p_i$.

The algorithm $\mathrm{ALG}^s_{\mathrm{sim}}$, for $s\in[0,1]$, takes an optimal LP solution $y$, scales its total mass $\sum_iy_ip_i$ by $s$ to $\kappa$, and fills mass $\kappa$ from the most valuable candidate down: $y'_i=1$ while the prefix mass $\sum_{l\le i}p_l$ stays at most $\kappa$, one fractional entry, then zeros. Offers are then sent independently with probabilities $y'_i$, so the algorithm randomises between two value-ordered policies. Its expected reward is $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)$.

The guarantee involves the truncated Poisson mean $\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]=\sum_{j\ge0}\min\{j,k\}e^{-\lambda}\lambda^j/j!$ and

$$\alpha^\tau_k=\sup_{0\le s\le1}\Big(s-\frac{s}{\tau}+\frac{\mathbb E[\min\{\mathrm{Pois}(sk),k\}]}{\tau k}\Big).$$

Formalization targets

Goal: Theorem 3 (p. 30)

For $\tau\in(0,1)$, every $I\in\mathcal I^\tau_{\mathrm{sim}}$, every optimal solution of $\mathrm{LP}_{\mathrm{sim}}(I)$ and a maximiser $s^*\in[0,1]$ of the objective defining $\alpha^\tau_k$,

$$R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}(I)\ \ge\ \alpha^\tau_k\,\mathrm{LP}_{\mathrm{sim}}(I).$$

Milestones

• Lemma 10 (p. 27): $\mathrm{LP}_{\mathrm{sim}}(I)\ge\mathrm{OPT}_{\mathrm{sim}}(I)$.
• Lemma 11 (p. 27): some optimal LP solution is a filled prefix $y=(1,\dots,1,y_j,0,\dots,0)$ with $y_j>0$.
• Lemma 12 (p. 28): the total mass of such a solution is $P_{\mathrm{high}}$ if $P_{\mathrm{high}}>k$ and $\min\{k,P_{\mathrm{total}}\}$ otherwise (posed under the disclosed hypothesis $v_i>0$, $v_i\ne1$, $p_i>0$).
• Monotonicity (App. D.5, p. ec16): $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ is decreasing in $x$.
• Proposition EC.2 (p. ec3): $\mathbb E[\min\{\mathrm{Pois}(k),k\}]=k(1-e^{-k}k^k/k!)$.
• Lemma 13 (p. 29): if $P_{\mathrm{high}}\le k$, then $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)\ge\big(s-s/\tau+\mathbb E[\min\{\mathrm{Pois}(sk),k\}]/(\tau k)\big)\mathrm{LP}_{\mathrm{sim}}(I)$ for every $s\in[0,1]$.
• The $\mathrm{ALG}^1$ bound (p. 30): on every $\tau$-bounded instance, $R_{\mathrm{ALG}^1_{\mathrm{sim}}}(I)\ge(1-e^{-k}k^k/(k!\tau))\,\mathrm{LP}_{\mathrm{sim}}(I)$.
• Lemma 14 (p. 29): if $P_{\mathrm{high}}>k$, deflating the acceptance probabilities to an instance with $P_{\mathrm{high}}=k$ does not increase the ratio $R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}/\mathrm{LP}_{\mathrm{sim}}$ (posed under the disclosed hypothesis $v_i\ne1$).

Significance

Theorem 3 makes value-ordered policies an $\alpha^\tau_k$-approximation on $\tau$-bounded instances, through Lemma 10. The factor tends to $1$ as $k\to\infty$ for fixed $\tau$: at $s=1$ it is at least $1-e^{-k}k^k/(k!\tau)=1-O(1/\sqrt k)$ (Corollary 4). The paper's Theorem 4, the subject of the companion mission in this series, shows that no value-ordered policy beats the same expression with the supremum over $s\ge0$, so the analysis is tight wherever the two suprema coincide. The interpretation of $\tau$ is how soft the capacity is: the bound degrades exactly as the overage cost dominates candidate values.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it has been machine-checked. A complete development would give the platform an overbooking-type stochastic selection model with an exact expected reward, an LP benchmark, and the truncated-Poisson constant that recurs in prophet-inequality and online-matching analyses (the $k$-uniform correlation gap of Yan 2011). Proposition EC.2 and the monotonicity of $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ are reusable on their own.

Difficulty

The obvious argument compares the algorithm's random number of hires with the LP's expected number and loses everything to the overage term: the LP pays $[\mathbb E|A|-k]^+$, the algorithm pays $\mathbb E[|A|-k]^+$, and Jensen's inequality points the wrong way. The gap must be controlled by a sum of independent Bernoulli variables against a Poisson variable of the same mean, uniformly over how the mass is spread across candidates. A second difficulty is the regime $P_{\mathrm{high}}>k$, where the LP optimum deliberately exceeds capacity; a direct bound there does not reduce to the first case, and the paper's reduction (Lemma 14) changes the instance rather than the algorithm. Tie cases $v_i=1$ make the LP optimum non-unique, which the formal statements must handle explicitly.

Formalization scope

Candidates are Fin n (0-based), all quantities are real. The sorted labelling $v_1\ge\dots\ge v_n$ is part of instance validity (Antitone I.v), as the paper assumes after relabelling; ties may be ordered arbitrarily. Every expectation is an explicit finite sum over the $2^n$ hire sets with independent probabilities $y'_ip_i$; there is no measure theory. The truncated Poisson mean is the series of the Poisson pmf. $\mathrm{LP}_{\mathrm{sim}}(I)$ is the supremum of the objective over the feasible set, which is the LP value; $\alpha^\tau_k$ is the supremum over $[0,1]$. $s^*$ is any maximiser of the $\alpha^\tau_k$ objective over $[0,1]$; one exists by continuity. A candidate with $p_i=0$ receives $y'_i=0$, which changes no reward.

The algorithm's reward is the exact expected reward of the run with independent offers, never the bound produced in the paper's proof, and the comparison is with the LP value at an optimal solution, not with the objective at an arbitrary feasible point; $\alpha^\tau_k$ is the supremum of the specific Poisson expression, not a free constant.

Two statements carry disclosed hypotheses, because the printed versions fail at ties: Lemma 12 assumes $v_i>0$, $v_i\ne1$, $p_i>0$, and Lemma 14 assumes $v_i\ne1$. Counterexamples are in the items' Formalization Notes. Theorem 3 and Lemma 13 need neither and hold for every optimal LP solution.

A complete development needs Poisson series manipulations (the closed form, concavity of $\lambda\mapsto\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]$), a Bernoulli-to-Poisson comparison for $\mathbb E\min\{\sum_iD_i,k\}$, and fractional-knapsack structure for the LP. Contributions of alternative proofs of any milestone, and of the Poisson facts as standalone results, are welcome.

Selected references

• B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3 (2023); Operations Research (2024). https://arxiv.org/abs/2210.04059
• Q. Yan, Mechanism Design via Correlation Gap, Proceedings of SODA 2011, 710–719. https://doi.org/10.1137/1.9781611973082.56
• M. T. Goodrich, R. Tamassia, Algorithm Design: Foundations, Analysis, and Internet Examples, Wiley, 2001, Chapter 5 (fractional knapsack).

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

Optimal stopping with partial information sits between two classical problems. In the secretary problem a decision maker sees values in random order, knows nothing about how they are generated, and must stop on the best one; the optimal guarantee is $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee, relative to the expected maximum, is the constant $\alpha^*\approx 0.745$: Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better on every distribution, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017, doi:10.1145/3033274.3085137) gave a rule that achieves it. Practical settings, such as pricing from historical data, lie in between: the distribution is unknown, but samples of it are available.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) interpolate between the two problems with the $p$-sample-driven optimal stopping problem: each of $N$ adversarial values is independently revealed in advance (a sample) with probability $p$, and the remaining values arrive online in random order. At $p=0$ this is the secretary problem; as $p\to1$ it approaches the i.i.d. prophet inequality. They show that the optimal competitive ratio $\alpha(p)$ of the limit problem is the value of an infinite-dimensional linear program, and they construct an explicit threshold rule whose guarantee $\tilde\alpha(p)$ is the root of a scalar equation.

Prior work on learning a distribution from samples obtained guarantees $\alpha^*-O(\varepsilon)$ with $O(n^2/\varepsilon)$ samples (Correa, Dütting, Fischer, Schewior, 2019) and with $O(n/\varepsilon^6)$ samples (Rubinstein, Wang, Weinberg, 2020). Theorem 9 of the paper, the goal of this mission, gives such a guarantee with $O(n/\varepsilon)$ samples.

Setting

Fix $p\in(0,1)$. The guarantee of the explicit threshold rule is the number $\tilde\alpha(p)\in(0,1)$ solving

$$\ln p+\frac{\tilde\alpha(1-p)^2}{p}=\sum_{i=1}^{\infty}\frac{\ln\bigl(1-\tilde\alpha+\tilde\alpha[(i+1)p^i-ip^{i+1}]\bigr)}{i(i+1)}.\tag{19}$$

Lemma 7 of the paper shows that (19) has exactly one root in $(0,1)$. The i.i.d. prophet constant $\alpha^*\in(0,1)$ is the solution of

$$\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1 .$$

The proof of Theorem 9 (Appendix B.9) works with three auxiliary functions of $p$, each depending on $\alpha^*$ as a parameter:

$$a(p)=\sum_{i\ge1}\frac{\ln\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)}{i(i+1)}+\alpha^*(2p-p^2),\qquad b(p)=\frac1{p^2}\sum_{i\ge1}\frac{1}{i(i+1)\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)},$$ $$c(p)=\sum_{i\ge1}\frac{p^{i-1}-p^i}{\tfrac1{p\alpha^*}-1+p^i(1+i(1-p))}.$$

Appendix B.7 also names the two sides of (19): $f(p,\alpha)=\ln p+\alpha(1-p)^2/p$ and $g(p,\alpha)=\sum_{i\ge1}\ln(1+\alpha(p^i(1+i(1-p))-1))/(i(i+1))$. In Lean, IsAlphaTilde p a and IsAlphaStar s are shared predicates in SampleDrivenOS.Limit; aB9 s p, bB9 s p, cB9 s p, fB7 p α, and gB7 p α are in SampleDrivenOS.Linear.

Formalization targets

Goal: Theorem 9 (p. 17)

$$\text{for every }p\in(0,1):\qquad \tilde\alpha(p)\ \ge\ \alpha^*p .$$

It is stated for every root $\tilde\alpha$ of (19) and every solution $\alpha^*$ of the integral equation; neither existence nor uniqueness is assumed.

Milestones (Appendix B.7 and B.9, in the order the proof uses them)

1. B.7: $f(p,\cdot)$ is strictly increasing on $[0,1]$ and $g(p,\cdot)$ non-increasing on $[0,1)$.
2. B.9: if (19) holds with "$\le$" at $\alpha^*p$ in place of $\tilde\alpha$ (after the substitution $\tilde\alpha=f(p)p$), then $\tilde\alpha(p)\ge\alpha^*p$.
3. B.9: that inequality is equivalent to $\alpha^*\le a(p)$.
4. B.9: $a$ is differentiable on $(0,1)$ with $a'(p)=2\alpha^*(1-p)-b(p)+c(p)$, also in term-by-term form.
5. B.9: $b(p)\ge 1/p$.
6. B.9: $c(p)\le\frac1p\int_0^1\frac{dy}{1/(p\alpha^*)-1+y(1-p\ln y)}-\alpha^*(1-p)$.
7. B.9: using the defining equation of $\alpha^*$,

$$\frac1p\int_0^1\frac{dy}{\tfrac1{p\alpha^*}-1+y(1-p\ln y)}\le\frac1p-\frac{1-p}{p}\Bigl(\frac1{p\alpha^*}-\frac1e\Bigr)\ln\frac{\tfrac1{p\alpha^*}+\tfrac pe}{\tfrac1{p\alpha^*}+\tfrac pe-1}.$$

8. B.9: for all $s\in[0.74,0.75]$ and $p\in(0,1)$, $\bigl(\frac1{ps}-\frac1e\bigr)\ln\frac{1/(ps)+p/e}{1/(ps)+p/e-1}\ge0.8$.
9. B.9: if $\alpha^*\in[0.74,0.75]$, then $c(p)\le\frac1p-\alpha^*(1-p)(1+\frac1p)$.
10. B.9: under the same hypothesis, $\frac{d}{dp}a(p)\le0$ on $(0,1)$.

Significance

The explicit rule's guarantee $\tilde\alpha(p)$ is a lower bound on the optimal ratio $\alpha(p)$, and Theorem 8 (a separate mission of this series) shows $\tilde\alpha(p)\to\alpha^*$ as $p\to1$. Theorem 9 makes that convergence quantitative and uniform: the guarantee is at least linear in $p$, so with $p=1-\varepsilon$, an online set of size $n=\varepsilon N$ and $O(n/\varepsilon)$ samples the rule earns $\alpha^*-O(\varepsilon)$ of the expected maximum. This improves the sample complexity of the earlier learning-based results by a polynomial factor, in a model more general than theirs.

The theorem is proved in the paper; it has no machine-checked proof. The proof is elementary real analysis on explicit series and integrals, and one of its steps is a numerical check that the paper does not carry out in print. A formalization turns that numerical claim into a certified inequality and checks a chain of estimates in which one inequality sign is misprinted (see Formalization scope).

Difficulty

The statement is about two implicitly defined numbers. $\tilde\alpha(p)$ has no closed form, and $\alpha^*$ is defined by an integral equation. Evaluating both numerically at finitely many $p$ proves nothing for the remaining $p$, and the inequality is tight at $p=1$ ($\tilde\alpha(1)=\alpha^*$), so no uniform slack is available near $p=1$.

Concavity of $\tilde\alpha$ would give the result immediately, and the paper reports it numerically, but the authors were unable to prove it; the argument must avoid it. The remaining work handles infinite series whose terms depend on $p$ through both $p^i$ and $i(1-p)$: differentiating such a series term by term requires uniform control of the derivative series, comparing it with an integral needs a monotonicity argument, and one step needs a bound valid on an entire two-parameter region rather than at a point.

Formalization scope

• Numbers, not processes. No probability, program or algorithm appears in Lean. Everything is a real-valued function on $\mathbb R$.
• Predicates, not choice. $\tilde\alpha(p)$ and $\alpha^*$ enter as IsAlphaTilde p a (with $0<a<1$) and IsAlphaStar s (with $0<s<1$). Statements quantify over every solution. Both exist, so the goal is not vacuous: existence of $\tilde\alpha$ is Lemma 7 (posed in the second mission of this series), and existence and uniqueness of $\alpha^*=1/\beta^*$ are posed as CorreaThreshold.Adaptive.beta_star_existsUnique (512ff915-7ec1-4d24-87b3-bc8adfee6bad).
• Series. Every series is a Lean tsum over i : ℕ with the paper's index $i\ge1$ shifted to i + 1. For parameters in $(0,1)$ all series are summable, so tsum is the true sum; summability is part of what solvers prove, never a hypothesis. Differentiability of $a$ is likewise a conclusion (HasDerivAt), never assumed.
• Total functions. Real.log 0 = 0 makes the integrands' values at $y=0$ equal their limits, so the interval integrals are the true integrals. Every division ($1/p$, $1/(ps)$) is at a positive argument under the stated ranges, and every logarithm's argument is positive.
• $\alpha^*\approx0.745$. The paper uses this approximation through the interval $\alpha^*\in[0.74,0.75]$ of its numerical check. Milestones 9 and 10 carry that interval as a hypothesis; the goal does not. The lower bound $\alpha^*>0.745$ is posed as CorreaThreshold.Adaptive.inv_beta_star_gt (ce70487c-b155-4e47-9ce8-8348dc1b1645). The upper bound $\alpha^*\le0.75$ (numerically $\alpha^*\approx0.74544$) is posed nowhere and is welcome as a lemma.
• A printed slip. The paper prints the conclusion of milestone 9 as "$c(p)\ge\dots$". The surrounding argument requires and announces "$\le$", and the formal statement uses $\le$.
• Ruled-out trivializations. Fixing $p$, replacing $\alpha^*$ by the numeral $0.745$ (a weaker statement, since $0.745<\alpha^*$), stating $a$'s monotonicity through deriv (which is $0$ at non-differentiable points), or replacing $\tilde\alpha$ by a chosen value all change the theorem. None is used.
• Reusable infrastructure. Welcome contributions include term-by-term differentiation of tsums under a dominating series, Riemann-sum comparisons for monotone integrands, a Chebyshev-type integral inequality for two decreasing functions, and certified interval arithmetic for a two-variable inequality such as milestone 8.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021 (journal version: Mathematics of Operations Research, 2024). https://arxiv.org/abs/2011.06516v2
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017; Mathematics of Operations Research 46(4), 2021. https://doi.org/10.1145/3033274.3085137
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982 (reference [26] of the paper). https://doi.org/10.1214/aop/1176993767
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 1986 (reference [28] of the paper).
• J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution, ACM EC 2019. https://doi.org/10.1145/3328526.3329627
• A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal Single-Choice Prophet Inequalities from Samples, ITCS 2020. https://doi.org/10.4230/LIPIcs.ITCS.2020.60

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 proof-of-stake blockchains do not let every token holder take part in consensus. Instead, token holders elect a small committee of block producers, and the committee runs a Byzantine agreement protocol. EOS, for instance, elects 21 producers by an up-to-30-vote approval ballot (paper, p. 9, citing EOS voting guide 2018). Byzantine agreement protocols are safe only if a supermajority of the committee is honest, typically more than two thirds. Whether the electorate can reliably seat such a supermajority depends on how voters vote and on how much they know about the candidates.

Benhaim, Falk and Tsoukalas (arXiv:2110.08673, Management Science 2023) model this election as approval voting under limited information. Each voter sees a noisy private signal of every candidate's type and turns it into a posterior probability that the candidate is honest. This mission formalizes the paper's single-voter result, Proposition 2: a voter who decides the committee alone should approve exactly the $k$ candidates most likely to be honest. The same statement covers voters who pool their signals (Proposition 4), because once the shared posteriors are computed the pooled electorate acts as one voter. A companion mission (I of this series) formalizes the paper's main result for many voters, exponential convergence of the success probability.

Setting

There are $m$ candidates $c_1,\dots,c_m$ and a committee size $k \le m$. A voter approves a set $\mathcal C$ of candidates (the ballot). The score of a candidate is the number of voters approving it (Definition 1); with a single voter it is $1$ on $\mathcal C$ and $0$ elsewhere. The $k$ highest-scoring candidates are elected. When fewer than $k$ candidates have non-zero score the committee is filled adversarially, and ties at the lowest elected score are broken adversarially (Definition 3). The committees the rule can produce are therefore the admissible committees: sets $T$ with $|T| = k$ and $\mathrm{score}(b) \le \mathrm{score}(a)$ for every $a \in T$ and $b \notin T$.

Each candidate is honest or malicious. Write $\mathrm{Hon}$ for the set of honest candidates. For a tolerance $p \in [0,1]$, the committee is honest, $\mathbb T = H$, if it has at least $\lceil (1-p)k \rceil$ honest members. Since the adversary chooses after the types are realised, $\mathbb T = H$ means that every admissible committee $T$ satisfies $|T \cap \mathrm{Hon}| \ge \lceil (1-p)k\rceil$.

The voter's information is summarised by the posterior probabilities $s_j = \Pr[c_j = H \mid s^*_j] \in [0,1]$ ((3)). Given the signals, the types are independent, so a set $\mathrm{Hon}$ has probability $\prod_{j \in \mathrm{Hon}} s_j \prod_{j \notin \mathrm{Hon}} (1-s_j)$. The success probability of a ballot $\mathcal C$ is $\Pr[\mathbb T = H \mid s]$, the total weight of the sets $\mathrm{Hon}$ for which $\mathbb T = H$ holds under the scores of $\mathcal C$ ((6) with $n = 1$).

The number of honest members of a fixed set $S$ is then a Poisson binomial random variable $X_S$ with parameters $(s_j)_{j\in S}$, the law of a sum of independent Bernoulli variables (Definition 7):

$$\Pr[X_S = \ell] = \sum_{A \subseteq S,\ |A| = \ell}\ \prod_{i\in A} s_i \prod_{j \in S\setminus A}(1-s_j).$$

$X \le_{\mathrm{st}} Y$ (the usual stochastic order, Definition 9) means $F_Y(x) \le F_X(x)$ for all $x$.

Formalization targets

Goal: Proposition 2 (p. 20)

For every $m \ge k$, every $p\in[0,1]$, every posterior vector $s\in[0,1]^m$, every set $\mathcal C^\star$ of $k$ candidates with $s_b \le s_a$ for all $a\in\mathcal C^\star$, $b\notin\mathcal C^\star$, and every ballot $\mathcal C$,

$$\Pr[\mathbb T = H \mid s]_{\mathcal C} \;\le\; \Pr[\mathbb T = H \mid s]_{\mathcal C^\star}.$$

This is the cardinal strategy with $z = k$ (Definition 6) being globally optimal. The statement is made pointwise in $s$ and for every top-$k$ set, whatever the tie-breaking among equal posteriors.

Milestones

1. Lemma 4 (p. 49). Permuting the parameters does not change a Poisson binomial law: $\Pr[X = \ell] = \Pr[X' = \ell]$ for all $\ell$.
2. Lemma 5 (p. 49). If $p_i \le p'_i$ for every $i$, then $X \le_{\mathrm{st}} X'$.
3. Lemma 1 (p. 19). If $p_1 \ge \dots \ge p_m$ lie in $[0,1]$ and $x$ is a positive integer, then over all $k$-element index sets $P$, $\Pr[X_P > x]$ is maximised by $P = \{1,\dots,k\}$.

The paper's Lemma 6 (p. 52), that $\le_{\mathrm{st}}$ is preserved under independent sums, is already proved on the platform as StochasticOrders.Usual.usual_order_convolution (theorem a8208567-b950-4dc8-a0da-eb915fea422c), stated for the measure-theoretic order StochasticOrders_Usual_UsualOrder (definition 62d803de-7bc8-4f9d-a0f1-7f956fc2888f). It is not posed again. Its carrier is a probability space rather than the finite sums used here.

Significance

Proposition 2 is the paper's benchmark for strategic voting. With full information pooled in one decision maker, the best achievable ballot is the top $k$ by posterior. The paper's Proposition 3 shows that the threshold strategies common in practice are not optimal against this benchmark, and Proposition 4 transfers the result to electorates that share signals. Lemma 1 is the underlying fact: among committees of fixed size, the one built from the largest honesty probabilities has the stochastically largest number of honest members. The fact applies to any Poisson binomial selection problem, for example choosing $k$ independent components to maximise the probability that enough of them work.

The results are proved in the paper (Appendix B.2, p. 45, and Appendices C–D, pp. 49–52, where Lemma 6 is proved on p. 52). None of them has been machine-checked. The formalization produces a reusable finite Poisson binomial layer (probability mass function, cdf, tail, permutation invariance, monotonicity in the parameters) and the first approval-voting committee model on the platform.

Difficulty

The informal argument (p. 20) is that a single voter "can unilaterally decide the committee", so the best choice is the top $k$. That shortcut does not survive the adversarial rule. A ballot with fewer than $k$ approvals lets the adversary fill the committee, and a ballot with more than $k$ lets the adversary pick among the approved. The comparison is therefore between the worst admissible committee of an arbitrary ballot and the unique admissible committee of $\mathcal C^\star$.

The paper's proof also states success as $\Pr[X > (1-p)k]$ and applies Lemma 1 at the possibly non-integer threshold $x = (1-p)k$. Definition 3 asks for $X \ge \lceil (1-p)k\rceil$, so the relevant threshold is $\lceil(1-p)k\rceil - 1$, which can be $0$ or negative, outside Lemma 1's hypothesis $x > 0$. Lemma 1 itself needs a comparison of Poisson binomial tails for parameter vectors that differ in every coordinate, not just in one.

Formalization scope

Candidates are Fin m and are 0-based (the paper's $c_j$ is index $j-1$). Probabilities are finite sums of product weights over Finset (Fin m); there is no measure theory. The Poisson binomial law is defined by the counting formula (84), which is exactly the product-measure probability of each outcome of independent Bernoulli trials. The threshold is Int.ceil ((1 - p) * k) compared with the integer cast of a cardinality. Stochastic order is expressed through cdfs at natural thresholds, which is equivalent to all real thresholds for laws supported on $\{0,\dots,n\}$.

Standing assumptions the page leaves implicit are explicit hypotheses: $k \le m$ (p. 9), $0 \le p \le 1$ ($p$ is a tolerated fraction), and parameters in $[0,1]$ wherever probabilities are used. Lemma 4 is stated without the range hypothesis, which makes it more general than the printed lemma.

Three printed readings are corrected and disclosed in the items. Lemma 4's "$\sigma(p_i)$" means $p_{\sigma(i)}$. Lemma 1's "argmax $=\{p_1,\dots,p_k\}$" is formalized as "$\{1,\dots,k\}$ attains the maximum", since ties make the argmax a family of sets. The success threshold is Definition 3's $\lceil(1-p)k\rceil$, not the proof's "$> (1-p)k$".

The ballot in Proposition 2 is unrestricted in size, which covers every cap $t \ge k$ of Definition 2. Optimality is stated pointwise in the posteriors, which implies optimality in expectation over any signal law. The Gaussian signal model (2)–(4) is not formalized.

The adversary is universal: the success event quantifies over every admissible committee. A formalization that let the election pick the best admissible committee, or that ignored admissibility and compared arbitrary $k$-sets, would make the goal trivial or independent of the ballot, and is ruled out. Proofs of all four theorems and any general Poisson binomial facts (normalisation, tail–cdf identities) are welcome.

Selected references

• A. Benhaim, B. H. Falk, G. Tsoukalas, Scaling Blockchains: Can Committee-Based Consensus Help?, Management Science, 2023; preprint arXiv:2110.08673v2, 2022. https://arxiv.org/abs/2110.08673 — DOI https://doi.org/10.1287/mnsc.2022.03177
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5
• Aurora EOS, EOS voting guide, 2018 (cited by the paper as EOS A (2018)). https://medium.com/@auroraeos/eos-voting-guide-3bf4e0be251b