All missions

Motivation

When one breached contract forces the next party to breach its own contract, a single failure travels down a loss chain: agent 1 (the initiator) causes a loss $\ell_1$ to agent 2, which can then no longer honour its agreement with agent 3 and causes it a loss $\ell_2$, and so on until agent $n$ causes a loss $\ell_n$ to a final victim. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) ask how the total loss should be shared among the agents of the chain, with the aim of encoding the answer in a smart contract that settles such disputes automatically.

Their central rules are the fixed-fraction rules $\varphi^\lambda$, under which every agent pays a fixed fraction $\lambda$ of the loss it caused and the initiator also pays the remaining fraction $1-\lambda$ of the total. An axiomatic characterization (their Theorem 1) singles out the whole family $\lambda\in[0,1]$ but not a particular member. This mission formalizes the paper's game-theoretic argument for the midpoint $\lambda=1/2$: the cooperative game that records which coalitions are liable for which losses has the midpoint allocation as both its Shapley value and its nucleolus, the two best-known single-valued solutions of cooperative game theory.

Setting

Agents are $N=\{1,\dots,n\}$ with $n\ge1$. A loss problem is a vector $\ell=(\ell_1,\dots,\ell_n)\in\mathcal L^n=\mathbb R^n_{\ge0}$, where $\ell_i$ is the loss agent $i$ causes to agent $i+1$; the total loss is $L=\ell_1+\dots+\ell_n$. The fixed-fraction rule with parameter $\lambda$ assigns

$$\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\ (i\ge2).$$

A transferable-utility game on $N$ is a function $v$ assigning a real number to every coalition $S\subseteq N$. The liability game of $\ell$ is

$$v_\ell(S)=\begin{cases}\sum_{i\in S}\ell_i&\text{if }1\in S,\\0&\text{otherwise:}\end{cases}$$

a coalition is liable for the losses its members caused only if it contains the initiator, without whom no loss would have occurred. The contribution of player $i$ to the grand coalition is $M_i(v)=v(N)-v(N\setminus\{i\})$.

Two solution concepts are compared with $\varphi^{1/2}(\ell)$.

• The Shapley value gives player $i$

$$\mathrm{Sh}_i(v)=\sum_{S\subseteq N\setminus\{i\}}\frac{|S|!\,(n-|S|-1)!}{n!}\bigl(v(S\cup\{i\})-v(S)\bigr).$$

• An imputation is a vector $x$ with $\sum_{i\in N}x_i=v(N)$ and $x_i\ge v(\{i\})$ for all $i$. The excess of $S$ at $x$ is $e(S,x)=v(S)-\sum_{i\in S}x_i$, and the excess vector $\theta(x)$ lists the $2^n$ excesses in non-increasing order. The nucleolus $\nu(v)$ (Schmeidler 1969) is the imputation whose excess vector is lexicographically smallest.

A game is convex if $v(\emptyset)=0$ and $v(S)+v(T)\le v(S\cup T)+v(S\cap T)$ for all $S,T$.

Formalization targets

Goal: Theorem 3 (p. 15)

For every $\ell\in\mathcal L^n$,

$$\mathrm{Sh}(v_\ell)=\varphi^{1/2}(\ell)\qquad\text{and}\qquad \nu(v_\ell)=\varphi^{1/2}(\ell),$$

where the second identity is stated as: $\varphi^{1/2}(\ell)$ is an imputation of $v_\ell$ with lexicographically minimal sorted excess vector, and every imputation with this property equals $\varphi^{1/2}(\ell)$.

Milestones (Appendix A, proof of Theorem 3, p. 24)

1. $v_\ell$ is convex.
2. (§4.2, p. 15; referenced, already on the platform) the core of a convex game is non-empty and contains its Shapley value, which applies to $v_\ell$ by milestone 1.
3. $M_1(v_\ell)=L$ and $M_i(v_\ell)=\ell_i$ for $i\ne1$.
4. Every nucleolus $\nu$ of $v_\ell$ satisfies $\nu_i=M_i(v_\ell)/2=\ell_i/2=\varphi^{1/2}_i(\ell)$ for $i\ne1$, and $\nu_1=\varphi^{1/2}_1(\ell)$.
5. The Shapley value of $v_\ell$ is a nucleolus of $v_\ell$.

Significance

The result. Theorem 1 of the paper leaves a one-parameter family of rules, and a designer who writes the rule into a contract must still choose $\lambda$. Theorem 3 gives a reason for $\lambda=1/2$ that does not depend on the axioms: if losses are treated as the worth of coalitions, two solution concepts that are built on unrelated principles (average marginal contributions on one side, lexicographic minimization of complaints on the other) both return $\varphi^{1/2}(\ell)$. Together with the paper's Theorem 2 (equidistance from ideal allocations, a separate mission of this series) it makes the midpoint the paper's recommended rule.

Formalizing it. The paper proves Theorem 3 by citing two results of Muto, Nakayama, Potters and Tijs (1988) on big boss games, the nucleolus formula (their Theorem 4.2) and the coincidence of Shapley value and nucleolus for convex big boss games (their Theorem 4.5); the paper itself proves only convexity and the marginal contributions. A formal proof must therefore establish the nucleolus of $v_\ell$ directly from Schmeidler's lexicographic definition. No nucleolus definition exists on the platform (searched 2026-10-14), and this mission introduces one. The Shapley value and convex games are reused from the platform's published definitions, and the core-contains-the-Shapley-value theorem for convex games is already proved there.

Difficulty

Convexity and the marginal contributions are finite case analyses. The Shapley identity is a weighted sum over all coalitions not containing a player and needs the combinatorial identities behind the weights; for $v_\ell$ only the position of the initiator relative to $S$ matters.

The substantive part is the nucleolus. Its definition compares sorted vectors of $2^n$ excesses, so an argument cannot treat one coalition at a time: showing that a candidate is lexicographically minimal requires controlling how a change of the payoff vector permutes the order of all excesses. The obvious first idea, minimizing only the largest excess (the least core), generally leaves a set of imputations rather than a point, so the comparison must go down the whole sorted list. Coalitions whose excesses tie, which happens for instance when some $\ell_i=0$, are where informal arguments about sorted excess vectors are usually loose, and a formal proof has to handle them.

Formalization scope

• Agents are Fin n with the initiator at index 0; [NeZero n] encodes $n\ge1$, which the paper assumes because $1\in N$. Loss vectors are Fin n → ℝ with the hypothesis IsLoss ℓ ($\ell_i\ge0$).
• A game is Finset (Fin n) → ℝ. The Shapley value is the published Supermodularity.Cooperative.ShapleyValue and convexity the published Supermodularity.Cooperative.IsConvexGame (the supermodular form, equivalent to the increasing-marginal-contribution form used on p. 24).
• The nucleolus is defined in the mission's Nucleolus file: imputations with efficiency and individual rationality, excess $v(S)-\sum_{i\in S}x_i$ over all $2^n$ coalitions including $\emptyset$ and $N$, sorted by ≥ into a list, and compared with List.Lex (· < ·). Including $\emptyset$ and $N$ does not change the order, since their excess is $0$ at every imputation.
• The goal states both identities. The nucleolus half is not replaced by membership in the core or by minimality of the largest excess, the minimization runs over imputations and not over all of $\mathbb R^n$, and uniqueness is stated explicitly rather than taken from Schmeidler's theorem.
• The paper never defines the nucleolus or the Shapley value; the standard definitions (Schmeidler 1969; Shapley 1953) are used.

Contributions welcome: proofs of the milestones; general lemmas on sorted excess vectors (e.g. Kohlberg-type criteria for the nucleolus), which are reusable for every later nucleolus result; Schmeidler's existence and uniqueness theorem; and the general big boss game results of Muto et al. (1988).

Selected references

• J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3):1773–1786, 2024 (accepted manuscript, 2023). https://doi.org/10.1287/mnsc.2023.4772
• S. Muto, M. Nakayama, J. Potters, S. Tijs, On big boss games, The Economic Studies Quarterly 39(4):303–321, 1988. https://doi.org/10.11398/economics1986.39.303
• D. Schmeidler, The nucleolus of a characteristic function game, SIAM Journal on Applied Mathematics 17(6):1163–1170, 1969. https://doi.org/10.1137/0117107
• L. S. Shapley, A value for n-person games, in Contributions to the Theory of Games II, Annals of Mathematics Studies 28, Princeton University Press, 1953, pp. 307–317. https://doi.org/10.1515/9781400881970-018
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1:11–26, 1971. https://doi.org/10.1007/BF01753431

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

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

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

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