Missions · Prove2Me

Completed

Combinatorics Mechanism Design Operations Research+1·Captain: mikedeng1

Scaling Blockchains: Can Committee-Based Consensus Help? II: With a Single Voter, Voting for the k Candidates Most Likely to Be Honest Is OptimalResearch Paper

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

Lemma 4 (p. 49). Permuting the parameters does not change a Poisson binomial law: $\Pr[X = \ell] = \Pr[X' = \ell]$ for all $\ell$ .
Lemma 5 (p. 49). If $p_i \le p'_i$ for every $i$ , then $X \le_{\mathrm{st}} X'$ .
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

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Climate Impact Investing 1: With an Average-Emissions Interaction Effect the Unique Equilibrium Emission Schedule Is ψ* − ε/(2n+ε)·(ψ* + 2n²ψ̄*/(2n+(n+1)ε)), Below the Schedule Without InteractionResearch Paper

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

(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.
Proposition 2: a schedule that maximizes (12) at every date is optimal for $\mathcal J^i$ against every admissible unilateral deviation.
Corollary 3: (13) is the unique maximizer of the date- $t$ payoff with own-emission externalities over $x\ge0$ .
(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$ .
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

9 thms3 active usersReviewed

Completed

Dynamical Systems Economics Operations Research+1·Captain: mikedeng1

Revenue Management in Crowdfunding 1: Optimal Pledge Level and Campaign Duration Under Triangular Valuations When Independent or Herding Backers DominateResearch Paper

Motivation

Reward-based crowdfunding platforms such as Kickstarter let a project creator collect pledges from the public for a fixed period. Two numbers are fixed before launch and cannot be changed afterwards: the pledge level $p$ each backer pays, and the campaign duration $T$ . A high pledge level earns more per backer but deters backers with low valuations; a long campaign gives more backers time to arrive but, because backers are paid out only at the end, discounts the project's value in their eyes. Zhang, Savin and Veeraraghavan (SSRN 3065267, published in Manufacturing & Service Operations Management, 2022, doi:10.1287/msom.2022.1147) model this trade-off as a revenue-management problem for a deterministic fluid model of the pledging process, with two kinds of backers: independent backers, who arrive on their own, and herding backers, who arrive at a rate proportional to the amount already pledged, in the spirit of the imitators of the Bass diffusion model. The mission formalizes the paper's model, its closed-form solution, and its main optimization result for valuations with a right-triangular distribution.

Setting

A campaign has a population $\hat I>0$ of independent backers, who arrive at rate $k>0$ times the number not yet arrived, and herding backers, who arrive at rate $\Lambda_h q p$ times the number of pledges made so far ( $\Lambda_h\ge0$ an arrival rate, $q\ge0$ a propensity). A backer's valuation $V$ is drawn from a law on $[0,\bar v]$ with survival function $\bar F_i$ (independent) or $\bar F_h$ (herding). A backer arriving at time $t\in[0,T]$ pledges iff $Ve^{-r(T-t)}\ge p$ , where $r>0$ is the backers' discount rate; that happens with probability $\bar F(pe^{r(T-t)})$ . The numbers $n^p_i,n^l_i$ of pledging and lost independent backers obey the linear system (1)–(4),

\frac{dn^p_i}{dt}=k(\hat I-n_i)\,\bar F_i(pe^{r(T-t)}),\qquad \frac{dn^l_i}{dt}=k(\hat I-n_i)\bigl(1-\bar F_i(pe^{r(T-t)})\bigr),\qquad n_i=n^p_i+n^l_i,

and the herding counts $n^p_h,n^l_h$ obey (8)–(10),

\frac{dn^p_h}{dt}=\Lambda_h q p\,(n^p_i+n^p_h)\,\bar F_h(pe^{r(T-t)}),\qquad \frac{dn^l_h}{dt}=\Lambda_h q p\,(n^p_i+n^p_h)\bigl(1-\bar F_h(pe^{r(T-t)})\bigr),

all starting from $0$ . The total number of pledges is $n(p,T)=n^p_i(T)+n^p_h(T)$ , the revenue is $\pi(p,T)=p\,n(p,T)$ , and the creator solves

\max\ \pi(p,T)\quad\text{over}\quad 0<p\le\bar v,\ \ 0\le T\le\tfrac1r\ln(\bar v/p).\qquad(18)

Two reduced revenue functions appear in the limiting regimes: without herding, $R_i(p,T)=k\hat Ipe^{-kT}\int_0^Te^{kx}\bar F_i(pe^{rx})dx$ (22); in the herding-dominated regime, the proxy $R_h(p,T)=p\int_0^T\bar F_h(pe^{ry})dy$ (27). A right-triangular law on $[0,\bar v]$ has mode $0$ ( $\bar F(y)=(1-y/\bar v)^2$ ) or mode $\bar v$ ( $\bar F(y)=1-(y/\bar v)^2$ ).

Formalization targets

Goal: Proposition 7

With $x^*_0$ , $x^*_1$ the explicit algebraic constants (34), (35):

(a) if $k=r$ and $\Lambda_h=0$ , the unique maximizer of (18) is

(p^*,T^*)=\Bigl(\bar v\tfrac{x^*_0-\sqrt{x^*_0}+1}{(x^*_0)^2+x^*_0+1},\ \tfrac1r\ln x^*_0\Bigr)\ \text{(mode 0)},\qquad \Bigl(\tfrac{\bar v}{\sqrt{1+x^*_1+(x^*_1)^2}},\ \tfrac1r\ln x^*_1\Bigr)\ \text{(mode }\bar v);

(b) the unique maximizer of $R_h$ over the same feasible set is $(\beta^*\bar v,\frac1r\ln\frac1{\beta^*})$ with $\beta^*$ the unique root in $(0,1)$ of $\ln\frac1\beta=\frac32(\beta-\frac43)^2-\frac16$ (mode 0), and $(\beta\bar v,\frac1r\ln\frac1\beta)$ with $\beta=\sqrt{-W(-3e^{-3})/3}$ (mode $\bar v$ ).

Milestones

Proposition 1 and Proposition 2: every solution of (1)–(4) and (8)–(10) equals the closed forms (5)–(7), (11)–(12), and these solve the systems.
Corollary 2: $n(p,T)$ equals the single integral (17); and (22): $\pi=R_i$ when $\Lambda_h=0$ .
Proposition 4(a), (b): with $\Lambda_h=0$ , $k=r$ , the optimal duration $T^*(p)$ for each fixed $p$ and the optimal pledge level $p^*(T)$ for each fixed $T>0$ , in closed form (23)–(26).
Proposition 5(a), (b): the same for $R_h$ , (28)–(31).

Significance

Proposition 7 is the paper's answer, for triangular valuations, to the question that motivates it: how a creator should set both levers together. Its four cases show how the optimal pledge level and duration move between campaigns dominated by low- or high-valuation independent backers and those dominated by herding backers; in particular herding-dominated campaigns call for markedly longer durations. Propositions 4 and 5 are the "limited-flexibility" policies for platforms where one lever is fixed by convention, and they are what the joint optimization is built from.

The model results (Propositions 1–2, Corollary 2) are proved in the manuscript's Appendix. The proofs of Propositions 4, 5 and 7 are in the paper's online Technical Appendix, which is not part of the source this mission cites; the decomposition into milestones follows the statements of the main text. None of these results has a machine-checked proof. A formalization produces verified closed forms for a nonlinear-in-parameters pricing problem and pins down three printing slips of the source (below).

Difficulty

Propositions 1 and 2 concern linear ordinary differential equations whose coefficients jump whenever the valuation law has an atom, so the classical theory does not apply directly; solutions are absolutely continuous and must be handled in integral form, and uniqueness needs a Grönwall-type argument for measurable coefficients. Corollary 2 is an integration by parts and a change of variables inside a double integral with an exponential of an inner integral. For the optimization results the obstacle is not the first-order condition but the global statement: each "optimal" claim asserts a unique global maximizer over a curved feasible region whose boundary $T=\frac1r\ln(\bar v/p)$ is active in some cases (Proposition 5) and inactive in others (Proposition 4, Proposition 7(a)). The first-order conditions are cubic or quartic equations whose roots are given by trigonometric and Cardano-type formulas, and part (b) involves transcendental equations; matching the right root and excluding boundary maxima is where the work lies.

Formalization scope

The model is a structure Campaign with real parameters Ihat, k, r, Lh ( $\Lambda_h$ ), q, vbar and the survival functions Fbi, Fbh. Standing assumptions: $\hat I,k,r,\bar v>0$ , $\Lambda_h,q\ge0$ , and each survival function is non-increasing, $[0,1]$ -valued, $1$ below $0$ and $0$ from $\bar v$ on. The positivity $p>0$ is added to the feasible set of (18), since $\ln(\bar v/p)$ needs it and $\pi(0,T)=0$ . The pledging probability $\mathbb P(Ve^{-r(T-t)}\ge p)$ is written $\bar F(pe^{r(T-t)})$ . The differential systems are stated in integral form with continuity on $[0,T]$ ; Propositions 1–2 assert both that every solution equals the closed forms and that the closed forms solve the system. "Optimal" always means: feasible, attaining the maximum, and the unique point that does. For a fixed $T$ the optimal pledge level is posed only for $T>0$ , because $\pi(\cdot,0)$ and $R_h(\cdot,0)$ vanish identically.

Three corrections of printing slips are part of the statements: (12) is stated with the factor $\Lambda_h q p$ of (9) and with the inner integration limits read as $u$ ; (39) has the second root $\beta=1$ , so uniqueness is posed on $(0,1)$ ; (40) is printed with $i$ and a complex Lambert $W$ , and is stated in the equivalent real form with $W(-3e^{-3})$ characterized as the unique $w\in(-1,0)$ with $we^w=-3e^{-3}$ . Printed decimals (one of which, $0.191\bar v$ in (36), is wrong: the exact value is $\approx0.198\bar v$ ) are not part of any statement.

Trivializing formalizations are ruled out: $n(p,T)$ is built from (5) and (11), not defined as (17); the differential systems are integral equations, not their closed forms and not a classical-derivative condition that no solution of a discontinuous system satisfies; optimality is a unique-maximizer statement, not an sSup or a first-order condition; and part (b) maximizes the explicit function (27), not a limit $\Lambda_h\to\infty$ .

The development needs interval integrals, the exponential, logarithm, square and cube roots from Mathlib, and a uniqueness argument for linear Volterra integral equations; the latter, and the change-of-variables identity behind (22) and Corollary 2, are reusable for other fluid models of diffusion. Proofs of any milestone, and alternative routes to Proposition 7 (for instance through the profile functions $T\mapsto\pi(p^*(T),T)$ ), are welcome.

Selected references

J. Zhang, S. Savin, S. Veeraraghavan, Revenue Management in Crowdfunding, manuscript of May 26, 2021, SSRN 3065267. https://ssrn.com/abstract=3065267 — published in Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1147
F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969, 215–227. https://doi.org/10.1287/mnsc.15.5.215
R. M. Corless, G. H. Gonnet, D. E. G. Hare, D. J. Jeffrey, D. E. Knuth, On the Lambert W function, Advances in Computational Mathematics 5, 1996, 329–359. https://doi.org/10.1007/BF02124750

10 thms3 active usersReviewed

Completed

Number Theory Operations Research Optimization·Captain: mikedeng1

Integer Factorization: Why Two-Item Joint Replenishment Is Hard 1: For Odd Composite M, Every Optimal Plan of an Explicit Two-Item Aperiodic JRP Instance Has q₂ = M and 1 < gcd(q₁, M) < MResearch Paper

Motivation

The joint replenishment problem (JRP) is one of the basic models of multi-item inventory control. Each item follows the economic order quantity (EOQ) model of Harris (1913): ordering costs a fixed amount, holding stock costs a rate proportional to the stock, and the classical trade-off between the two determines how often to reorder. In a JRP, items replenished together share part of the fixed cost, so the reorder cycles of the items should be coordinated. The problem has been studied for decades, with a large literature of heuristics and approximation algorithms (see the survey of Khouja and Goyal 2008; Porras and Dekker 2008 compare the two ways of charging joint costs), yet its exact complexity remained unclear even for very few items.

Schulz and Telha (arXiv:2007.09045, 2020; Operations Research, 2024) give a striking answer for the smallest non-trivial case, two items. They show that solving the two-item problem exactly is at least as hard as integer factorization (their Theorem 1), and, assuming the Riemann hypothesis, that the two-item periodic JRP is NP-hard under randomized reductions (Theorem 2). This mission formalizes the mathematical core of Theorem 1(a), for the aperiodic JRP: the paper's Lemma 1.

Timeline. The complexity of both JRP variants was open for a long time. Schulz and Telha announced the reduction from integer factorization to the two-item aperiodic JRP (Theorem 1(a)) in 2011. Cohen-Hillel and Yedidsion (2018) then proved that the aperiodic JRP with an arbitrary number of items is strongly NP-hard (they call it the periodic JRP). The 2020 preprint adds the reduction for the two-item periodic JRP (Theorem 1(b)) and, under the Riemann hypothesis, a randomized reduction from Partition to it (Theorem 2).

Setting

For an item with fixed ordering cost $K$ and holding cost rate $H$ , replenished every $q$ time units, the long-run cost per unit time is

\mathrm{EOQ}_{K,H}(q) = \frac{K}{q} + Hq .

Reorder cycles are positive integers $q \in \mathbb Z^+$ . In the aperiodic two-item JRP (objective (1) of the paper) items 1 and 2 have data $(K_1,H_1)$ and $(K_2,H_2)$ , and every joint replenishment earns a discount $K_0 \le K_1, K_2$ . With cycles $q_1, q_2$ , joint replenishments happen every $\mathrm{lcm}(q_1,q_2)$ time units, so the discount per unit time is $\mathrm{DC}(q_1,q_2;K_0) = K_0/\mathrm{lcm}(q_1,q_2)$ and the problem is

\min\left\{\mathrm{JRP}(q_1,q_2) = \mathrm{EOQ}_{K_1,H_1}(q_1) + \mathrm{EOQ}_{K_2,H_2}(q_2) - \frac{K_0}{\mathrm{lcm}(q_1,q_2)} \ :\ q_1,q_2 \in \mathbb Z^+\right\}.

For an integer $M$ , the instance of Lemma 1 has

K_1 = K_0 = M(M-1),\qquad H_1 = 4,\qquad K_2 = M^3(M^2-1),\qquad H_2 = M(M^2-1).

Item 2's own EOQ optimum is $q_2 = M$ . Fixing $q_2 = M$ leaves the one-variable problem (2) with objective

\mathrm{JRP}^{\mathrm{red}}(q_1) = M(M-1)\left(\frac{1}{q_1} - \frac{1}{\mathrm{lcm}(q_1,M)}\right) + 4q_1 .

In Lean these are eoq, aperiodicCost, lemma1Cost, eoq2 (item 2's cost) and jrpRed, and an optimal solution (IsOptimal) is a pair of positive integers whose value is no larger than that of any other pair of positive integers.

Formalization targets

Goal: Lemma 1

For every odd composite number $M$ , the instance above satisfies $K_0 \le K_1$ , $K_0 \le K_2$ , has all coefficients at most $M^5$ , has an optimal solution, and

\text{every optimal } (q_1,q_2) \text{ satisfies } \quad q_2 = M \quad\text{and}\quad 1 < \gcd(q_1,M) < M .

So $\gcd(q_1, M)$ is a non-trivial divisor of $M$ .

Milestones (the steps of the paper's proof, pp. 9–10)

$\mathrm{EOQ}_{K_2,H_2}(M\pm1) = \mathrm{EOQ}_{K_2,H_2}(M) + H_2/(M\pm1) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0$ .
For $q_2 \ne M$ : $\mathrm{JRP}(q_1,q_2) \ge \mathrm{EOQ}_{K_2,H_2}(M) + K_0 + 4 > \mathrm{JRP}(1,M)$ .
$\mathrm{JRP}(q_1, M) = \mathrm{EOQ}_{K_2,H_2}(M) + \mathrm{JRP}^{\mathrm{red}}(q_1)$ .
For $q_1$ coprime with $M$ : $\mathrm{JRP}^{\mathrm{red}}(q_1) \ge 4(M-1)$ .
For a divisor $p$ of $M$ with $3 \le p < M$ and a multiple $q$ of $p$ : $\mathrm{JRP}^{\mathrm{red}}(q) \le (M-1)(M-p)/q + 4q$ .
Some multiple $q$ of $p$ in $\left[\frac{M-1}{2} - \frac{p-1}{2}, \frac{M-1}{2} + \frac{p-1}{2}\right]$ has $\mathrm{JRP}^{\mathrm{red}}(q) < 4(M-1)$ .
Multiples $q_1$ of $M$ have $\mathrm{JRP}^{\mathrm{red}}(q_1) = 4q_1 \ge 4M$ , while $\mathrm{JRP}^{\mathrm{red}}((M-1)/2) \le 4(M-1)$ .

Significance

The result. Lemma 1 turns any exact algorithm for the two-item aperiodic JRP into a factoring algorithm: solve the instance, read off $\gcd(q_1, M)$ , and recurse on the two factors. Since the instance's coefficients have size $O(\log M)$ , a polynomial-time JRP algorithm would factor integers in polynomial time (Theorem 1(a)). This explains, in a precise sense, why the many exact and approximation methods for the JRP never produced a provably polynomial exact algorithm even for two items, and why the problem's difficulty is number-theoretic rather than combinatorial.

Formalizing it. The lemma has a complete, elementary proof in the paper; it has not been machine-checked. The formalization pins down every quantifier the prose leaves loose: that optimal solutions exist, that the claim is about every optimum, which coefficients are used, and that periods range over positive integers only. The proof steps (the item-2 pin, the coprime bound, the interval argument) are stated as separate milestones so they can be checked individually.

Difficulty

Each step is elementary, but the argument mixes discrete and continuous reasoning. The objective is not convex in $q_1$ : the term $-K_0/\mathrm{lcm}(q_1,M)$ jumps down at every period sharing a factor with $M$ . The obvious approach, comparing against the continuous EOQ minimizer, gives the right threshold $4(M-1)$ for coprime periods but says nothing about where a cheaper non-coprime period sits. The interval step needs the exact size of a window of integers around $(M-1)/2$ , that $p$ consecutive integers contain a multiple of $p$ , and a strict inequality between a quadratic's roots and that window. The existence of an optimum is not stated in the paper and needs a coercivity argument over $\mathbb Z^+ \times \mathbb Z^+$ .

Formalization scope

This mission formalizes the correctness of the reduction behind Theorem 1(a); polynomial running time is not formalized, and neither are Theorem 1 as a statement about algorithms, the recursion to a full factorization, nor primality testing.

Conventions: periods are natural numbers, and every quantification over a period requires it to be positive, because Lean evaluates $K/0 = 0$ , $\mathrm{lcm}(0,M) = 0$ and $\gcd(0,M) = M$ . Costs are real numbers. Coefficients are natural numbers cast to $\mathbb R$ . "Odd composite" is Odd M ∧ 1 < M ∧ ¬ M.Prime. "Size at most $5\log M$ " is stated as "every coefficient is at most $M^5$ ", equivalent in any logarithm base.

Two additions relative to the printed statement are disclosed in the goal's Formalization Note. The goal states the explicit instance of the proof (p. 9) rather than "there is an instance", since an existential instance could be chosen to make the claim easy and loses the polynomial-size construction the reduction needs. The goal also asserts that an optimal solution exists, so that "every optimal solution satisfies …" is not vacuously true. Neither periods equal to zero nor junk values of division can satisfy the optimality predicate.

All objects are defined in one file, JRPHard.Aperiodic.Setting; nothing beyond Mathlib's Nat.gcd, Nat.lcm, Nat.Prime and real arithmetic is needed. Proofs of any milestone, or alternative proofs of the goal, are welcome.

Selected references

A. S. Schulz and C. Telha, Integer factorization and Riemann's hypothesis: Why two-item joint replenishment is hard, arXiv:2007.09045v1, 2020; published as Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024. https://arxiv.org/abs/2007.09045
F. W. Harris, How many parts to make at once, Factory, The Magazine of Management 10(2), 1913; reprinted in Operations Research 38(6), 1990. https://doi.org/10.1287/opre.38.6.947
E. Porras and R. Dekker, A solution method for the joint replenishment problem with correction factor, International Journal of Production Economics 113(2), 834–851, 2008. https://doi.org/10.1016/j.ijpe.2007.11.008
M. Khouja and S. Goyal, A review of the joint replenishment problem literature: 1989–2005, European Journal of Operational Research 186(1), 2008. https://doi.org/10.1016/j.ejor.2007.03.007
M. Cohen-Hillel and L. Yedidsion, The periodic joint replenishment problem is strongly NP-hard, Mathematics of Operations Research 43(4), 2018. https://doi.org/10.1287/moor.2017.0904

9 thms3 active usersReviewed

Completed

Economics Operations Research Optimization+1·Captain: mikedeng1

Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition I: Comparative Statics of an Unconstrained Monopoly's Optimal R&D IntensityResearch Paper

Motivation

Firms deciding how much to spend on research and development face two different kinds of return to spending. More money can make the eventual innovation more valuable, or it can make the innovation arrive sooner. Lin (Management Science, 2022, doi:10.1287/mnsc.2022.4503) calls these two properties scalability and accelerability, and shows that they predict how R&D intensity responds to financing frictions and to competition. The benchmark of the whole paper is a single financially unconstrained firm with no rival. Its comparative statics, Proposition 1 of the paper, are what the constrained and competitive cases are compared against, and they already contain one of the paper's headline observations: a higher interest rate raises the optimal R&D intensity exactly when the project is accelerable.

Setting

A technology is a tuple $T=(A,\beta,\eta,\gamma)$ . At investment intensity $R$ (spending per unit of time), the expected payoff of the innovation and the arrival rate of discovery are

u(R)=A\,R^{\beta},\qquad \lambda(R)=\eta\,R^{\gamma},

with the standing assumptions $A>0$ , $\eta>0$ , $\beta,\gamma\in[0,1)$ and $\beta+\gamma<1$ (decreasing returns to scale). The project is scalable if $u'>0$ , here $\beta>0$ , and accelerable if $\lambda'>0$ , here $\gamma>0$ . Intensities are bounded below by $\underline R=1$ .

The firm discounts at rate $r>0$ . The discovery time $\tau_d$ is exponentially distributed with rate $\lambda(R)$ ; the firm pays $R$ per unit of time until $\tau_d$ and then receives $u(R)$ . Its R&D value at intensity $R$ is

\Pi(R)=\mathbb E\Big[e^{-r\tau_d}\,u(R)-R\int_0^{\tau_d}e^{-rt}\,dt\Big].

Lemma 1 of the paper identifies this with the perpetuity value

V(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}. \tag{5}

The value is positive only below $\bar R=(A\eta)^{1/(1-(\beta+\gamma))}$ , so the firm chooses $R$ from the range $[\underline R,\bar R]=[1,\bar R]$ of (7). The optimal intensity set is

R^*_{uc}=\{R\in[1,\bar R]:\ \Pi(R')\le\Pi(R)\ \text{for all } R'\in[1,\bar R]\}.

Its comparative statics are studied through $\ln V(R)=\ln(u\lambda-R)-\ln(\lambda+r)$ .

Formalization targets

Goal: Proposition 1 (p. 5)

For a set $S'$ to lie above a set $S$ means: every $x\in S$ and $y\in S'$ satisfy $x\le y$ , and $x<y$ whenever $x>\underline R$ . The goal states that $R^*_{uc}$ is nonempty and

if $\beta=\gamma=0$ then $R^*_{uc}=\{\underline R\}$ ;
if $\beta>0$ or $\gamma>0$ , then $R^*_{uc}$ at $A'>A$ lies above $R^*_{uc}$ at $A$ ;
if $\beta>0$ , then $R^*_{uc}$ at $\beta'>\beta$ (with $\beta'+\gamma<1$ ) lies above $R^*_{uc}$ at $\beta$ ;
if $\gamma=0<\beta$ , then $R^*_{uc}$ at $\eta'>\eta$ lies above $R^*_{uc}$ at $\eta$ ;
if $\gamma=0$ , $R^*_{uc}$ does not depend on $r$ ; if $\gamma>0$ , $R^*_{uc}$ at $r'>r$ lies above $R^*_{uc}$ at $r$ .

Milestones (p. 5 and Appendix A.2, p. 18)

Lemma 1 (5): $\Pi(R)=V(R)$ for every $R>0$ .
Without accelerability and with $A\beta\eta\ge1$ : $R^*_{uc}=\{(1/A\beta\eta)^{1/(\beta-1)}\}$ , a formula free of $r$ .
The cross partials of $\ln V$ on $1\le R$ , $u\lambda>R$ :

\frac{\partial^2\ln V}{\partial R\,\partial A}=\frac{\lambda}{(\lambda u-R)^2}\frac{\partial u}{\partial A}(1-\beta-\gamma)>0,\qquad \frac{\partial^2\ln V}{\partial R\,\partial r}=\frac{\lambda'}{(\lambda+r)^2},

together with (A.3) in $\beta$ and (A.4) in $\eta$ , with the signs the paper states.

Significance

Proposition 1 is the reference point for the rest of the paper: Proposition 2 (financially constrained monopoly), Corollary 1 (constrained firms under-invest without accelerability) and Propositions 3–4 (R&D races) are all read against it. Two of its clauses are not what a reader would guess. The speed factor $\eta$ has an unambiguous effect only when the project is not accelerable, because for accelerable projects a higher $\eta$ also raises the marginal cost of expanding $R$ through the heavier effective discount rate $\lambda+r$ (p. 5). And the interest rate raises intensity for accelerable projects: in the paper's words (p. 5), "a higher $r$ reduces the marginal cost of expanding $R_{uc}$ through the discount rate."

The paper proves Proposition 1 in Appendix A.2 with an informal appeal to Topkis's monotonicity theorem; the result has no machine-checked proof. Formalizing it makes three things explicit that the printed proof leaves implicit: the expectation-to-perpetuity identity (5) for an exponential discovery time, the domain on which $\ln V$ is defined and has increasing differences, and the fact that the range $[1,\bar R]$ itself moves with $A$ , $\beta$ and $\eta$ . The derivative claims of the paper are also made precise for optima that need not be unique or interior.

Difficulty

The statement is about an optimal set, and the parameter moves both the objective and the feasible range. The first obstacle is that the paper's derivative form $\partial R^*_{uc}/\partial s>0$ is false as printed when the optimum sits at the corner $\underline R$ : with $\gamma=0$ , $\beta=0.1$ , $\eta=1$ , $r=1$ and $A\in\{2,2.2\}$ the optimum is $1$ in both cases. Any proof therefore has to separate corner optima from interior ones. The second is that $\ln V$ is only defined where $u\lambda>R$ ; the increasing-differences inequalities hold there, but the comparison of two optima at two parameter values can pass through points where the value at one of the parameters is not positive. The third is that $V$ is not concave in general, so first-order conditions alone do not identify the optimal set.

Formalization scope

All declarations live in the namespace AccelScal.UCMonopoly. Lean conventions:

A Tech structure with fields A β η γ : ℝ; Tech.Standing bundles (2) and the added condition $A\eta>1$ , which the paper expresses as "conditional on investment taking place" (p. 5) and which makes the value at $\underline R$ positive and the range nondegenerate. The discount rate is a separate hypothesis $r>0$ .
$u$ , $\lambda$ and $\bar R$ use real powers (Real.rpow); every statement keeps $R\ge1$ (or $R>0$ for Lemma 1).
The R&D value ucPayoff is the expectation (4) under ProbabilityTheory.expMeasure (λ R), with the random payoff $\tilde u$ replaced by its mean $u(R)$ and the cash-flow term of (4), which does not depend on $R$ , dropped.
RstarUC T r is the set of maximizers of ucPayoff T r over Set.Icc 1 (Rbar T), the range of the same parameters.
" $\partial R^*_{uc}/\partial s>0$ " is OrderedAbove: weak order between all optima, strict when the smaller optimum exceeds $1$ . " $\partial R^*_{uc}/\partial r=0$ " is equality of the sets.
$u'=0\Leftrightarrow\beta=0$ and $\lambda'=0\Leftrightarrow\gamma=0$ on $R\ge1$ , so the hypotheses are stated on $\beta$ , $\gamma$ .
The cross partials $\partial^2\ln V/\partial R\,\partial s$ are the $s$ -derivative of the $R$ -derivative, on $1\le R$ , $R<u(R)\lambda(R)$ .

Trivializing formalizations are ruled out: the value is defined as an expectation, not by the closed form (5); the optimal set is a set of maximizers, never a selected optimum or a closed-form formula; nonemptiness is part of the goal, so no clause is vacuous; the range moves with the parameter; and every ordering keeps its strict part at interior optima.

Not posed: Lemma 1 (6) (the financially constrained value, which needs the first passage of a geometric Brownian motion), (A.5) (Proposition 1 makes no claim about $\gamma$ ), and a sign of (A.4) for $\gamma>0$ (the paper says it cannot be signed). A complete development needs the Laplace transform of the exponential law, derivatives of real powers and logarithms, and a monotone comparative statics argument on intervals; a reusable lemma of the form "strictly increasing differences on a moving interval domain orders the argmax sets" would serve other missions as well. Contributions of any of the milestones, or of such general lemmas, are welcome.

Selected references

D. Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2022.4503
D. M. Topkis, Minimizing a submodular function on a lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
X. Vives, Oligopoly Pricing: Old Ideas and New Tools, MIT Press, 1999. https://mitpress.mit.edu/9780262720403/
S. Athey, Monotone comparative statics under uncertainty, Quarterly Journal of Economics 117(1), 2002. https://doi.org/10.1162/003355302753399481

8 thms3 active usersReviewed

Completed

Economics Probability Statistics·Captain: mikedeng1

Quantifying the Impact of Impact Investing I: Mean and Variance of an Impact-Ranked Portfolio's Excess Return under IID Bivariate-Normal Impact Factors and AlphasResearch Paper

Motivation

Impact investing selects securities by a non-financial characteristic: an ESG rating, a carbon-intensity metric, a "sin stock" flag. A recurring question in finance is whether such a selection costs or earns the investor anything, and by how much. Lo and Zhang (SSRN 3944367; Management Science, doi:10.1287/mnsc.2022.01168) give a closed-form answer in a stylised model: the excess return of a portfolio formed by ranking securities on an impact factor is governed by the correlation between that factor and the securities' unobserved excess returns. The mathematical tool is the theory of induced order statistics (concomitants), introduced by Bhattacharya (1974) and David (1973) and surveyed in David and Nagaraja, Order Statistics (2004), §6.8. The same tools were used by Lo and MacKinlay (1990) to quantify data-snooping biases in asset-pricing tests.

Setting

There are $N$ securities. Security $i$ has an observable impact factor $X_i$ and an unobservable excess return $\alpha_i$ (the part of its return not explained by priced factors). Under Assumption (A1) the pairs $(X_i, \alpha_i)$ , $i = 1, \dots, N$ , are independent and identically distributed bivariate normal with means $(\mu_x, \mu_\alpha)$ , variances $(\sigma_x^2, \sigma_\alpha^2)$ and correlation $\rho \in (-1, 1)$ . As the paper does before its Proposition 2, the mission takes $\mu_x = 0$ , $\sigma_x = 1$ and $\mu_\alpha = 0$ .

An investor ranks the securities by $X$ . Let $\pi$ be the permutation sorting $X$ increasingly. The order statistics are $X_{i:N} = X_{\pi(i)}$ , and the induced order statistics are

\alpha_{[i:N]} = \alpha_{\pi(i)},

the excess return of the security whose impact factor has rank $i$ (display (6) of the paper). The vector $\alpha$ is not sorted by its own values; its order is induced by $X$ .

An impact portfolio holds the securities of a set of ranks $\mathcal S \subseteq \{1, \dots, N\}$ with weights $\{\omega_i : i \in \mathcal S\}$ summing to one; its excess return is

\tilde\alpha = \sum_{i \in \mathcal S} \omega_i\, \alpha_{[i:N]}.

Formalization targets

Goal: Proposition 6 (p. 21), with (31) corrected

\mathbb E[\tilde\alpha] = \sum_{i\in\mathcal S}\omega_i\,\mathbb E[\alpha_{[i:N]}] = \rho\,\sigma_\alpha \sum_{i\in\mathcal S}\omega_i\,\mathbb E[X_{i:N}],

\operatorname{Var}(\tilde\alpha) = \sum_{i\in\mathcal S}\omega_i^2 \operatorname{Var}(\alpha_{[i:N]}) + 2\sum_{i<j\in\mathcal S}\omega_i\omega_j \operatorname{Cov}(\alpha_{[i:N]}, \alpha_{[j:N]})

= \sigma_\alpha^2\Big((1-\rho^2)\sum_{i\in\mathcal S}\omega_i^2 + \rho^2\Big(\sum_{i\in\mathcal S}\omega_i^2 \operatorname{Var}(X_{i:N}) + 2\sum_{i<j\in\mathcal S}\omega_i\omega_j\operatorname{Cov}(X_{i:N}, X_{j:N})\Big)\Big).

The paper prints the last line with $1-\rho^2$ where $(1-\rho^2)\sum_{i\in\mathcal S}\omega_i^2$ is needed. The two agree only when $\sum_{i\in\mathcal S}\omega_i^2 = 1$ or $\rho^2 = 1$ . For $\rho = 0$ , $\mathcal S = \{1, 2\}$ and $\omega = (\tfrac12, \tfrac12)$ , the true variance is $\sigma_\alpha^2/2$ and the printed expression gives $\sigma_\alpha^2$ . The goal states the corrected identity.

Milestones

(A.21), p. 65: $e_i = \alpha_i - \rho\sigma_\alpha X_i$ is $N(0, \sigma_\alpha^2(1-\rho^2))$ , and $X_1, \dots, X_N, e_1, \dots, e_N$ are mutually independent.
(A.22), p. 65: $\alpha_{[i:N]} = \rho\sigma_\alpha X_{i:N} + e_{[i]}$ , and the vector of order statistics is independent of the vector of induced residuals $(e_{[i]})_i$ .
Proposition 2 (8), p. 14: $\mathbb E[\alpha_{[i:N]}] = \rho\sigma_\alpha \mathbb E[X_{i:N}]$ .
Proposition 2 (9), p. 14: $\operatorname{Var}(\alpha_{[i:N]}) = \sigma_\alpha^2(1 - \rho^2 + \rho^2\operatorname{Var}(X_{i:N}))$ .
Proposition 2 (10), p. 14: $\operatorname{Cov}(\alpha_{[i:N]}, \alpha_{[j:N]}) = \sigma_\alpha^2\rho^2\operatorname{Cov}(X_{i:N}, X_{j:N})$ for $i \ne j$ .

Significance

The result. Proposition 6 reduces the first two moments of any rank-based impact portfolio to three parameters ( $\rho$ , $\sigma_\alpha$ , the weights) and to moments of standard normal order statistics, which are tabulated. The sign of $\rho$ alone decides whether a portfolio of top-ranked securities has positive, zero or negative expected excess return. That is the paper's quantitative answer to whether impact investing helps or hurts returns. The variance formula is what the paper's later results build on: Sharpe and information ratios of impact portfolios, Treynor–Black weighting (Proposition 7) and combination with a passive index (Proposition 8).

Formalizing it. The proposition is proved in the paper; the mission is a machine-checked version of it. The proof needs a reusable, currently absent piece of probability in Lean: moments of induced order statistics of Gaussian pairs, including the behavior of residuals carried along by a sort keyed on an independent sample. No order-statistic or concomitant result of this kind is on the platform or in Mathlib. The mission also records a corrected form of (31), whose printed version is false whenever $\sum_{i\in\mathcal S}\omega_i^2 \neq 1$ .

Difficulty

The algebra from Proposition 2 to Proposition 6 is the bilinearity of variance and covariance. The substance is in Proposition 2, and specifically in the step from (A.21) to (A.22). The permutation $\pi$ that sorts $X$ is random, so $e_{[i]} = e_{\pi(i)}$ is a residual read at a random index. The tempting argument treats $e_{[i]}$ as "an $e$ ", which would give mean zero and variance $\sigma_\alpha^2(1-\rho^2)$ immediately. That argument is incomplete: it needs the joint law of $(e_{\pi(1)}, \dots, e_{\pi(N)})$ conditional on $X$ , which requires that $\pi$ is a function of $X$ only, that $e$ is independent of $X$ , and that the law of $e$ is invariant under permutations. None of this is written out on the page, and none of it is in Mathlib; integrability and measurability of the order statistics must also be established, since the Lean moments are defined without them.

Formalization scope

All declarations live in the namespace ImpactInvesting.Portfolio. Order statistics use Mathlib's Tuple.sort: orderStat x i = x (Tuple.sort x i) and inducedOrderStat x a i = a (Tuple.sort x i). Ranks are 0-based: i : Fin N is the paper's rank $i + 1$ . Ties are broken by index; they have probability zero under (A1), and no no-ties hypothesis is added.

Assumption (A1) is the predicate IsA1 P X α σα ρ. Each pair (X i, α i) has a Gaussian law (HasGaussianLaw), the pairs are mutually independent (iIndepFun), and the moments are fixed: $\mathbb E X_i = 0$ , $\operatorname{Var} X_i = 1$ , $\mathbb E\alpha_i = 0$ , $\operatorname{Var}\alpha_i = \sigma_\alpha^2$ , $\operatorname{Cov}(X_i,\alpha_i) = \rho\sigma_\alpha$ . Identical distribution follows, because a bivariate Gaussian law is determined by these moments. The normalisations $\mu_x = 0$ , $\sigma_x = 1$ , $\mu_\alpha = 0$ are hypotheses, not a without-loss-of-generality step; (8) is false without $\mu_\alpha = 0$ . The ranges $\sigma_\alpha > 0$ and $-1 < \rho < 1$ are explicit hypotheses. Moments are the Bochner integral P[·], Var[·; P] and cov[·, ·; P]. No integrability hypotheses are added: order statistics of Gaussian samples are in every $L^p$ , and proving this is part of the work. The portfolio is a Finset (Fin N) of ranks with weights w : Fin N → ℝ summing to one on it; $\sum_{i<j\in\mathcal S}$ is taken in the order of Fin N.

A formalization in which the "order statistics" are not sorted, or the induced statistics are sorted by $\alpha$ itself, would make the statements trivial or false; the definitions sort by $X$ and read $\alpha$ at the same permutation. The printed second line of (31) is not stated anywhere, because it is false.

Out of scope: the multi-factor return model (1)–(2) beyond the role of $\alpha$ , Treynor–Black weights (Proposition 7), combined portfolios (Proposition 8), the asymptotic expansions and limits (Propositions 3, A.1, A.2), and the omitted-factor model (Proposition 5, a separate mission). Contributions welcome: integrability and measurability of order statistics, the permutation-invariance lemma for residuals carried by a sort, and Gaussian regression decompositions; all of these are reusable beyond this mission.

Selected references

A. W. Lo and R. Zhang, Quantifying the Impact of Impact Investing, SSRN 3944367, draft of 29 June 2023; Management Science (2023). https://ssrn.com/abstract=3944367, https://doi.org/10.1287/mnsc.2022.01168
P. K. Bhattacharya, Convergence of sample paths of normalized sums of induced order statistics, Annals of Statistics 2 (1974), 1034–1039. https://doi.org/10.1214/aos/1176342823
H. A. David and H. N. Nagaraja, Order Statistics, 3rd ed., Wiley, 2003 (cited in the paper as 2004). https://doi.org/10.1002/0471722162
A. W. Lo and A. C. MacKinlay, Data-snooping biases in tests of financial asset pricing models, Review of Financial Studies 3 (1990), 431–467. https://doi.org/10.1093/rfs/3.3.431

8 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Lightning Network Economics: Channels I: The Expected Discounted Cost of a Bidirectional Payment Channel in Closed FormResearch Paper

Payment channels and the cost of locked capital

Blockchains such as Bitcoin settle every transaction on a public ledger. Each on-chain transaction pays a fee and waits for confirmation, so frequent small payments are expensive. The Lightning Network moves such payments off-chain: two parties lock funds in a shared payment channel and pay each other by updating the channel's balance, touching the blockchain only to open, close or re-fund it. A channel is not free either. The locked funds cannot be used elsewhere, and once one side's balance is exhausted the channel has to be reset on-chain.

Guasoni, Huberman and Shikhelman (Lightning Network Economics: Channels, Management Science, 2023) quantify this trade-off in a stochastic model and compare three ways of settling two opposite streams of payments: on-chain transactions, unidirectional channels, and one bidirectional channel. Their comparisons all rest on a single computation, the expected discounted cost of a channel in closed form (Theorem 1). This mission formalizes that computation.

The model

Two nodes exchange unit payments. Node 1 pays node 2 one unit at each jump of a Poisson process $N^{\lambda_1}_t$ with rate $\lambda_1$ ; node 2 pays node 1 one unit at each jump of an independent Poisson process $N^{\lambda_2}_t$ with rate $\lambda_2$ . The paper normalizes $\lambda_1\le\lambda_2$ . The net balance of node 1 is

X_t=N^{\lambda_2}_t-N^{\lambda_1}_t,\qquad X_0=0 .

In a bidirectional channel node 1 commits $l_1$ units and node 2 commits $l_2$ units. The money is the channel's capacity: the channel works as long as $-l_1<X_t<l_2$ . Locked capital has an opportunity cost of $r(l_1+l_2)$ per unit of time, where $r>0$ is the continuously compounded interest rate, and all costs are discounted at rate $r$ . When the balance reaches $-l_1$ (node 1 is exhausted) or $+l_2$ (node 2 is exhausted), the channel is reset at cost $B$ and the balance restarts at $0$ with the same commitments.

Let $J(n)$ be the expected total future cost when the balance equals $n$ . Conditioning on the first payment, which arrives after an exponential time with rate $\lambda_1+\lambda_2$ , gives the first-step equation (15)

J(n)=(l_1+l_2)\frac{r}{r+\lambda_2+\lambda_1}+J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1},\qquad -l_1<n<l_2,

with the reset conditions $J(-l_1)=J(0)+B$ and $J(+l_2)=J(0)+B$ . The cost of the channel is $c^{l_1,l_2}(\lambda_1,\lambda_2)=J(0)$ .

In a unidirectional channel only node 2 pays (rate $\lambda_2$ ) and only node 2 commits capital ( $l_2$ units). The cost satisfies $J(n)=l_2\frac{r}{r+\lambda_2}+J(n+1)\frac{\lambda_2}{r+\lambda_2}$ for $0\le n<l_2$ with $J(l_2)=J(0)+B$ , and $c^{0,l_2}(0,\lambda_2)=J(0)$ .

The roots of the characteristic equation $\lambda_2\alpha^2-(\lambda_1+\lambda_2+r)\alpha+\lambda_1=0$ are

\alpha_\pm=\frac{\lambda_1+\lambda_2+r\pm\sqrt{(\lambda_2-\lambda_1)^2+r^2+2r(\lambda_2+\lambda_1)}}{2\lambda_2}. \tag{4}

Formalization targets

Goal: Theorem 1 (ii)

For $0<\lambda_1\le\lambda_2$ , $r>0$ , any $B$ and natural commitments $l_1,l_2\ge1$ , the bidirectional cost system has a solution, and every solution satisfies

c^{l_1,l_2}(\lambda_1,\lambda_2)=l_1+l_2-B\,\frac{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})}{\alpha_-^{l_1}(1-\alpha_+^{l_1+l_2})-\alpha_+^{l_1}(1-\alpha_-^{l_1+l_2})+\alpha_+^{l_1+l_2}-\alpha_-^{l_1+l_2}}. \tag{3}

Milestones

Competing exponential clocks (proof of Theorem 1, p. 10): the minimum $\tau$ of independent exponential times with rates $\lambda_2,\lambda_1$ is exponential with rate $\lambda_2+\lambda_1$ , and $\tau^{\lambda_2}$ rings first with probability $\lambda_2/(\lambda_2+\lambda_1)$ . This is a published, proved platform theorem, reused as is.
The first term (p. 10): $E[e^{-r\tau}]=(\lambda_2+\lambda_1)/(\lambda_2+\lambda_1+r)$ and $E[\int_0^\tau e^{-rs}r(l_1+l_2)\,ds]=(l_1+l_2)\,r/(r+\lambda_2+\lambda_1)$ .
The last term (p. 10): $E[e^{-r\tau}J(X_{t+\tau})\mid X_t=n]=J(n+1)\frac{\lambda_2}{r+\lambda_2+\lambda_1}+J(n-1)\frac{\lambda_1}{r+\lambda_2+\lambda_1}$ .
General solution of (15) (§5.1): on the lattice $-l_1\le n\le l_2$ , (15) holds at the interior points if and only if $J(n)=l_1+l_2+k_1\alpha_-^n+k_2\alpha_+^n$ for constants $k_1,k_2$ .
The cost function (§5.1): the closed form of $J(n)$ at every balance $n$ , which gives (3) at $n=0$ .
Theorem 1 (i), (1): $c^{0,l_2}(0,\lambda_2)=l_2+B\big(((r+\lambda_2)/\lambda_2)^{l_2}-1\big)^{-1}$ .
Theorem 1 (i), (2): with $k=B\log(1+r/\lambda_2)$ and $B>0$ , the minimum of (1) over real sizes is $\frac{B}{2k}\big(-k+\sqrt{k(k+4)}+2\log(\tfrac12(k+\sqrt{k(k+4)}+2))\big)$ , attained at $l_2=\frac Bk\log(\tfrac12(k+\sqrt{k(k+4)}+2))$ .

What the closed form gives

Formula (3) is what the rest of the paper works with. Lemma 1 prices on-chain settlement of a stream of rate $\lambda$ at $C\lambda/r$ . Comparing that price with (1) and (3) yields the paper's thresholds on the on-chain fee below which no channel pays off (Theorem 2), the small-interest-rate asymptotics of the optimal symmetric channel, whose minimal cost scales like $3(2B\lambda/r)^{1/3}$ (Theorem 3), and the long-run number of channel payments per on-chain transaction (Proposition 2). Without an exact expression for the cost these comparisons would rest on simulation.

The paper proves Theorem 1 by a first-step argument and the solution of a linear difference equation. No part of it has been machine-checked. A formal proof would supply what the published argument passes over: that the first-step equation (15) and the reset conditions together have a unique solution on the lattice, that the denominator of (3) does not vanish, and the measure-theoretic computation of the coefficients of (15) from the exponential clocks. The later missions of this series (rate bounds, small-rate asymptotics, the balance walk) build on the same model.

Where the difficulty lies

The algebra of solving a second-order linear recurrence is routine. Two points are not. First, the solution has to be shown to exist and to be unique for every admissible set of parameters. This requires $\alpha_-\ne\alpha_+$ and a non-singular $2\times 2$ system for $k_1,k_2$ , whose determinant is the denominator of (3), and the paper does not discuss when that determinant vanishes. Second, the coefficients of (15) come from expectations over exponential times: the joint expectation of the discount factor $e^{-r\tau}$ and the indicator of which clock rang first. The paper factors it as $E[e^{-r\tau}]\,P(\tau=\tau^{\lambda_2})$ , which uses that the minimum is independent of the identity of the first clock, a fact it does not state.

Formalization scope

The rates are written lam₁, lam₂; the sizes $l_1,l_2$ are natural numbers with $l_1,l_2\ge1$ , because payments are of one unit and the balance lives on the lattice $\{-l_1,\dots,l_2\}$ . The cost function is a map $J:\mathbb Z\to\mathbb R$ whose values off the lattice are unconstrained.
The cost is defined by its equations, (15) with the reset conditions (IsBiCostFn) and the §5.2 system (IsUniCostFn), never by (3) or (1). Every statement about "the cost" asserts both that a solution exists and that every solution takes the stated value, so it is neither vacuous nor dependent on a choice of solution.
The unidirectional system is a separate definition: the bidirectional one at $l_1=0$ would force $B=0$ . For the same reason the Remark after Theorem 1 ("(1) follows from (3) by substituting $\lambda_1=l_1=0$ ") is not posed: with $\alpha_-=0$ and $l_1=0$ the denominator of (3) vanishes.
Powers are natural powers in (1) and (3), integer powers (zpow) in the general solution and in $J(n)$ , and real powers (Real.rpow) in the minimization (2), which is over real sizes $m>0$ as in the paper's proof.
The paper prints the exponent in the numerator of the $J(n)$ display as $l+n$ ; the statement uses $l_1+n$ , which is what the derivation gives and what reduces to (3) at $n=0$ .
The probabilistic milestones use Mathlib's expMeasure for the laws (through push-forward measures of measurable random variables) and IndepFun. Integrability is part of what is to be proved.
The hypothesis $\lambda_1\le\lambda_2$ is kept in the goal as printed. No sign of $B$ is assumed except $B>0$ in (2), without which the infimum is not attained.
Ruled out as trivializing: defining the cost as its closed form (which turns the goal into a definitional equality), fixing numerical parameters, restricting to $\lambda_1=\lambda_2$ , and treating the sizes as real numbers in the cost system.

Contributions welcome: proofs of the milestones in any order, and reusable lemmas on linear difference equations with constant coefficients and on Laplace transforms of exponential laws, neither of which Mathlib currently has in this form.

Selected references

P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, 2023. https://doi.org/10.1287/mnsc.2022.01664
J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, technical report, 2015 (as cited by Guasoni et al.). https://lightning.network/lightning-network-paper.pdf

13 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Probability+1·Captain: mikedeng1

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 1: A Non-Adaptive, Committed LP-Rounding Policy for ProbeTop-k Earns at Least (1 − e^{−k}k^k/k!) Times the LP BoundResearch Paper

Motivation

Hiring is a pipeline: a firm with $k$ openings and a large pool of applicants cannot interview everyone, so it must decide whom to interview, in what order, and whether to hire on the spot. The ProbeTop-k problem models this. Each applicant has a random value with a known distribution, an interview reveals the value, at most $T$ interviews may be conducted, and at most $k$ applicants are hired. The firm maximises the expected total value of its hires.

The same structure appears in stochastic probing, sequential testing and assortment problems, and its benchmark, the best adaptive, non-committed policy (one that may choose the next interview after seeing earlier values and may hire only at the end), is hard to compute. Practical policies are non-adaptive (fix the interview order in advance) and committed (hire or reject right after each interview). Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) ask how much is lost by restricting to such policies, and answer with an LP-rounding algorithm whose guarantee improves with $k$ .

Setting

An instance $I = (k, T, n, F)$ has $1 \le k \le T \le n$ . Applicant $i \in [n]$ has value $V_i$ supported on finitely many non-negative values $r_1, \dots, r_J$ , with $q_{ij} = \Pr(V_i = r_j)$ ; values are independent across applicants.

The linear relaxation $\mathrm{LP}_{ptk}(I)$ has variables $y_i$ (probability of interviewing $i$ ) and $x_{ij}$ (probability of hiring $i$ when $V_i = r_j$ ):

\mathrm{LP}_{ptk}(I) = \max \sum_{i=1}^n \sum_{j=1}^J r_j x_{ij} \quad \text{s.t.}\quad x_{ij} \le y_i q_{ij},\ \ \sum_i y_i \le T,\ \ \sum_{i,j} x_{ij} \le k,\ \ x_{ij} \ge 0,\ \ 0 \le y_i \le 1 .

From a solution $(x, y)$ define

p_i = \frac{\sum_j x_{ij}}{y_i}, \qquad v_i = \frac{\sum_j r_j x_{ij}}{\sum_j x_{ij}},

each $0$ when its denominator is $0$ .

The algorithm ALGptk solves the LP and takes a basic optimal solution $(x, y)$ . It then draws the interview set $S$ by the dependent rounding DR: applicants with $y_i = 1$ are always in $S$ ; a single fractional $y_a$ puts $a$ in $S$ with probability $y_a$ ; two fractional $y_a + y_b = 1$ put exactly one of them in $S$ , $a$ with probability $y_a$ . ALGptk interviews $S$ in decreasing order of $v_i$ , and on observing $V_i = r_j$ hires $i$ with probability $x_{ij}/(y_i q_{ij})$ if a position is still open. Its expected reward is $R_{ALG_{ptk}}(I)$ .

Formalization targets

Goal: Theorem 1

R_{ALG_{ptk}}(I) \;\ge\; \Big(1 - \frac{e^{-k}k^k}{k!}\Big)\, \mathrm{LP}_{ptk}(I) \qquad \text{for every valid instance } I \text{ with } k \text{ positions.}

The factor is $1 - 1/e$ at $k = 1$ and tends to $1$ as $k \to \infty$ .

Milestones

The paper's own steps, in attack order:

Lemma 2 (p. 16): a basic feasible solution has at most two fractional $y_i$ , and two fractional ones sum to $1$ .
(P1), (P2) (p. 17): DR has marginals $\mathbb{E}(Y_i) = y_i$ and never exceeds $T$ interviews.
$\mathbb{E}(P_i) = p_i$ (p. 18): the hiring coin has mean $p_i$ .
Lemma 3 (p. 18): $R_{ALG_{ptk}}(I) = \sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$ , where $Z_i = Y_i P_i$ , the $P_i$ are independent Bernoulli( $p_i$ ) indicators, and $N_{i-1}$ counts the earlier applicants with $Z_\ell = 1$ .
Lemma 4 (p. 18): with two fractional components, this quantity under DR is at least its value under independent rounding of $y$ .
LP identity (p. ec8): $\sum_{i,j} r_j x_{ij} = \sum_i y_i v_i p_i$ .
Proposition EC.1 (Yan 2011; p. ec2): the weighted rank function of a $k$ -uniform matroid has correlation gap at most $(1 - e^{-k}k^k/k!)^{-1}$ .
Independent version (p. ec8): with independent rounding, the reward is at least $(1 - e^{-k}k^k/k!)\,\mathrm{LP}_{ptk}(I)$ .

A companion milestone, Lemma 5 (p. 21), states that for weighted Bernoulli instances the LP has an optimal solution with $x_i = y_i q_i$ . It does not feed Theorem 1.

Significance

Theorem 1, combined with the fact that $\mathrm{LP}_{ptk}$ bounds every adaptive, non-committed policy (Lemma 1 of the paper), shows that a policy that is both non-adaptive and committed earns at least a fraction $1 - e^{-k}k^k/k!$ of the optimal adaptive, non-committed reward; the lost fraction $e^{-k}k^k/k!$ vanishes as $k$ grows. The factor is tight for this LP (App. B.6). The theorem also underlies a PTAS for ProbeTop-k (Corollary 1) and, through Lemma 5, the same guarantee for the Sequential Offering problem of Purohit et al. (Corollary 2).

The result is proved in the paper; to our knowledge nothing in it is machine-checked. A formalization would add to the platform:

an LP relaxation with basic feasible solutions as extreme points of a polytope;
an explicit model of a randomised, committed selection algorithm as a finite expectation;
the correlation gap of $k$ -uniform weighted rank functions, a tool that recurs across prophet inequalities, posted pricing and stochastic probing.

Proposition EC.1 is a cited result (Yan 2011), not proved in the paper. Formalizing it is part of the work.

Difficulty

The obvious argument compares the algorithm with the LP term by term, $\Pr(i \text{ hired}) \ge c\, y_i p_i$ for each $i$ . This fails because hiring is capped at $k$ : applicants late in the order are hired only if few earlier ones were. The guarantee must be obtained in aggregate, which is what the correlation gap does.

Two steps carry the weight:

Proposition EC.1 is a genuine extremal inequality over all distributions on subsets with given marginals.
Lemma 4 must show that the negative correlation DR introduces between the two fractional applicants never hurts a committed, order-dependent selection. It is a case analysis over sample paths that uses the decreasing order of $v_i$ .

Lemma 3 is a conditional-expectation identity, but in a fully explicit model it requires marginalising out the values and coins of all other applicants.

Formalization scope

Lean namespace HiringLP.ProbeTopK.

Representation.

Applicants are Fin n and support points Fin J. All quantities are real.
Instances are valid when $1 \le k \le T \le n$ , $r_j \ge 0$ , $q_{ij} \ge 0$ and $\sum_j q_{ij} = 1$ .
Basic feasible solutions are Set.extremePoints ℝ of the feasible set in $(x, y)$ -space. An optimal solution is feasible and objective-maximal among feasible points, and $\mathrm{LP}_{ptk}(I)$ is the objective at it.

Conventions.

$p_i$ , $v_i$ and the hiring probability $x_{ij}/(y_i q_{ij})$ are $0$ when their denominators vanish (the paper's footnote 2).
The interview order is a permutation required to be non-increasing in $v_i$ , with ties in any order.
DR is an explicit formula for the probability of each interview set.

The expected reward. $R_{ALG_{ptk}}(I)$ is a finite sum over the interview set, the value vector (independent, law $q$ ) and the vector of hiring coins (independent given the values). Applicant $i$ is hired exactly when it is interviewed, its coin succeeds, and fewer than $k$ earlier interviewed applicants had successful coins. The reward collects the realised values $r_{V_i}$ .

Ruled out.

Defining the reward as $\sum_i v_i\, \mathbb{E}(\mathbf 1\{N_{i-1} < k\} Z_i)$ . That is Lemma 3, which would make the goal a statement about its own proof.
Comparing with the objective at an arbitrary feasible point instead of an optimal one.

Infrastructure and contributions. The weighted rank function, independent rounding and marginals are separate, reusable definitions. Contributions are welcome on each milestone, especially Proposition EC.1. So is general infrastructure: extreme points of polytopes as basic solutions, and finite product distributions.

Selected references

B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, Operations Research, 2024; preprint arXiv:2210.04059v3, 2023. https://arxiv.org/abs/2210.04059
Q. Yan, Mechanism design via correlation gap, Proceedings of the 22nd ACM-SIAM Symposium on Discrete Algorithms (SODA), 710–719, 2011. Proceedings volume: https://doi.org/10.1137/1.9781611973082
S. Agrawal, Y. Ding, A. Saberi, Y. Ye, Correlation robust stochastic optimization, Proceedings of the 21st ACM-SIAM Symposium on Discrete Algorithms (SODA), 1087–1096, 2010. Proceedings volume: https://doi.org/10.1137/1.9781611973075
R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
M. Purohit, S. Gollapudi, M. Raghavan, Hiring under uncertainty, Proceedings of the 36th International Conference on Machine Learning (PMLR 97), 5181–5189, 2019. https://proceedings.mlr.press/v97/purohit19a.html

16 thms3 active usersReviewed

Completed

Algorithmic Game Theory Analysis Mechanism Design+1·Captain: mikedeng1

Mechanism Design under Approximate Incentive Compatibility 2: Under Local α-Power Envelopes, ε-IC Mechanisms Gain at Most Õ(ε^(α/(2α−1))) RevenueResearch Paper

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu picks the option that maximizes his utility, however small the advantage over the next-best option. In many settings this is implausible. Agents may face cognitive or computational costs, or the designer may only be able to certify incentives approximately, as in algorithmic mechanism design where exact incentive compatibility is replaced by ε-incentive compatibility: no deviation gains more than $\varepsilon$ .

Balseiro, Besbes and Castro (arXiv:2103.03403v2; Operations Research, 2024) ask how much a revenue-maximizing seller can gain when the buyer is only an $\varepsilon$ -optimizer, in the most basic setting: one seller, one item, one buyer. Without the relaxation the answer is classical: by Myerson (1981) and Riley–Zeckhauser (1983) the optimal mechanism is a posted price. The rounding argument usually attributed to Nisan shows that the gain from the relaxation is $O(\varepsilon^{1/2})$ for every distribution. This mission formalizes the paper's first main theorem, which shows that for regular instances the gain is much smaller and is determined by the local curvature of the revenue curve at the optimal price.

Setting

The buyer's value $v$ has a density $f$ on $S=[0,\bar v]$ , with $\bar v>0$ , $f\ge 0$ , $f=0$ off $S$ and $\int_0^{\bar v}f=1$ . Assumption 1 requires in addition that $f$ has bounded variation on $S$ . Write $F(v)=\int_0^v f$ , $\bar F=1-F$ , the revenue function $R(v)=v\bar F(v)$ (the revenue of a posted price $v$ ), and $\dot R(v)=\bar F(v)-vf(v)$ .

A mechanism $m=(x,t)$ assigns to every report $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$ . It is individually rational (IR) if $v x(v)-t(v)\ge 0$ for all $v\in S$ , and ε-incentive compatible (IC $_\varepsilon$ ) if

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

$\mathcal M(\varepsilon)$ is the set of such mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$ .

Definition 1 (local α-power envelopes). $R$ has a unique maximizer $p^\star\in(0,\bar v)$ on $S$ , and there are $\alpha>1$ , $\kappa_L,\kappa_U>0$ and a neighborhood $\mathcal N_\ell=(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ with

\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\qquad\forall v\in\mathcal N_\ell .

For the uniform distribution on $[0,1]$ , $p^\star=1/2$ and $\alpha=2$ .

Formalization targets

Goal: Theorem 1 (p. 16)

Under Assumption 1, local $\alpha$ -power envelopes at $p^\star$ and $\inf_{p\in S\setminus\mathcal N_\ell}|\dot R(p)|>0$ ,

\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\tilde O\big(\varepsilon^{\alpha/(2\alpha-1)}\big),

where $\tilde O$ allows a factor $\log(1/\varepsilon)$ and the constants depend on the instance but not on $\varepsilon$ .

Milestones

The paper's argument passes through the following stated results, in attack order:

$\mathcal M(\varepsilon)\subseteq\mathcal M_{\text{path}}(\varepsilon)$ for the relaxation that keeps IR on $[0,\mu]$ and IC only along a path $v\mapsto v^\star(v)$ (p. 17);
Lemma 1 (weak duality): $\Pi(m)\le\Phi_1(\lambda)+\Phi_2(\lambda)$ for every $m\in\mathcal M_{\text{path}}(\varepsilon)$ and every dual-feasible $\lambda$ ;
Lemma 2: an explicit dual solution $\lambda^\star(v)=\frac{d}{dv}\sum_{j\le k}F(w^j(v))$ on the $k$ -th step, where $w$ inverts $v^\star$ ;
Lemma 3: $\Phi_1(\lambda^\star)\le C\varepsilon K$ , $K$ the number of steps;
Lemma 4: $\int_x^{\bar v}\Delta\le R(x)+2(w(x)-x)$ when the dual virtual value $\Delta$ is nonnegative on $[x,\nu_0]$ ;
Proposition 2: for the piecewise-linear path of eq. (9), $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$ ;
the sandwich $vf-\bar F-C_L\varepsilon^\beta\le\Delta\le vf-\bar F+C_U\varepsilon^\beta$ a.e. on $[p^\star,\nu_0]$ (p. 48);
$\Delta\le-\dot R+C\varepsilon^\beta$ a.e. on $[0,p^\star]$ (pp. 51–52).

Significance

Theorem 1 is an instance-dependent impossibility result: no $\varepsilon$ -IC mechanism can extract more than $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ beyond the optimal posted price. Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$ , it strictly improves the universal $O(\varepsilon^{1/2})$ bound for these distributions; for $\alpha=2$ (a revenue curve with nonzero second derivative at $p^\star$ ) the rate is $\varepsilon^{2/3}$ . Together with Theorem 3 of the same paper, a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by a randomized mechanism, it identifies the exact rate up to the logarithm. The authors conjecture that the logarithmic factor can be removed.

The result is proved in the paper; no machine-checked proof of it or of any of its lemmas exists. A formalization would check an appendix argument of several pages of explicit estimates, and would produce reusable components: a weak duality theorem for a mechanism-design program over a path of incentive constraints, an explicit solution of the functional equation $\lambda(v)=f(v)+\dot w(v)\lambda(w(v))$ by iterates of $w$ , and estimates of iterated piecewise-linear maps.

Difficulty

The obvious approach is to bound the gain by perturbing the optimal posted price, which yields only the $\varepsilon^{1/2}$ rate of the rounding argument. Getting the exponent $\alpha/(2\alpha-1)$ requires an upper bound that is tight to first order, i.e. a nearly optimal dual certificate for an infinite-dimensional program. The dual depends on the choice of path: the paper's analysis shows that a parallel shift $w(x)=x+\delta$ cannot beat $\varepsilon^{1/2}$ , so the path must approach the diagonal near $p^\star$ while keeping the number of steps $K$ controlled. The estimates for $\Delta$ in milestones 7–8 require tracking $\lambda^\star(w(v))$ through $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$ iterations of $w$ , with a bounded-variation (possibly discontinuous) density. Measure-theoretic details absent from the paper also have to be supplied: changes of variables along a Lipschitz path, almost-everywhere differentiability of iterated compositions, and integrability of the dual variable.

Formalization scope

The Lean development lives in namespace ApproxIC.UpperBound. Every function of the value is a total function ℝ → ℝ and every condition quantifies over $S$ only. Committed conventions:

$F$ is the interval integral of $f$ ; $\dot R$ is the explicit expression $\bar F(v)-vf(v)$ , not a derivative of $R$ .
Mechanisms are required to be measurable (disclosed: $\mathbb E_v[t(v)]$ presumes it). $\Pi^\star$ is an sSup of the revenue image, which is nonempty and bounded above by $\bar v$ .
The goal is stated as $\forall m\in\mathcal M(\varepsilon),\ \Pi(m)-\Pi^\star(\mathcal M(0))\le C\varepsilon^{\alpha/(2\alpha-1)}\log(1/\varepsilon)$ for all $\varepsilon\in(0,\varepsilon_0]$ , with $C,\varepsilon_0$ chosen after the instance and before $\varepsilon$ . The infimum hypothesis on $|\dot R|$ ranges over $S\setminus\mathcal N_\ell$ .
Definition 1's constants are parameters of a predicate LocalPowerEnvelope.
Paths carry an added, disclosed assumption: $w$ is Lipschitz on $[0,\nu_0]$ (eq. (9)'s $w$ is). $\dot w$ is deriv w.
The thresholds are $\mathbb N$ -indexed with index $0$ equal to $\bar v$ , so the paper's $\nu_k$ is index $k+1$ .
Lemma 1's printed sign $(v-w(v))$ in $\Phi_2$ is read as $(w(v)-v)$ , as in its proof and in Lemma 4. Lemma 4's printed " $\Phi_2(\lambda)=\int_x^{\bar v}\Delta$ " is read as $\int_x^{\bar v}\Delta^+=\int_x^{\bar v}\Delta$ . Lemmas 3 and 4 are stated for Lemma 2's explicit $\lambda^\star$ .

The goal imports only the model file; paths, the dual and eq. (9) appear only in the milestones. A formalization in which $\tilde O$ 's constants are chosen after $\varepsilon$ , $\Pi^\star(\mathcal M(0))$ is replaced by a constant, or the revenue integral is allowed to vanish on non-measurable mechanisms is not this theorem and is ruled out by the statement.

A complete development needs interval integrals and the fundamental theorem of calculus for absolutely continuous functions, change of variables along monotone Lipschitz maps, BoundedVariationOn, real powers and logarithms, and iterates Nat.iterate. The duality lemma and the functional-equation solution are reusable for other single-agent screening problems with relaxed incentive constraints. Contributions to any milestone, and alternative proofs of the goal that bypass the path construction, are welcome.

Selected references

S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
J. Riley, R. Zeckhauser, Optimal Selling Strategies: When to Haggle, When to Hold Firm, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885622

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? 1: The Mining Game Has a Unique Equilibrium Whose Number of Active Miners Is Fixed by an Explicit Cost ConditionResearch Paper

Motivation

Proof-of-work blockchains such as Bitcoin keep their ledger secure by a contest: miners spend computing power ("hash rate") to solve a cryptographic puzzle, and the miner who solves it first earns the block reward. The probability of winning is proportional to a miner's share of the total hash rate, so mining is a rent-seeking contest in the sense of Tullock (1967), with heterogeneous costs. Whether such a contest stays decentralized, that is, whether many miners remain active or a few efficient ones take over, is a question about the structure of its equilibrium.

Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021) model a two-stage game: miners first invest in hardware, then compete in hash rate. This mission formalizes the second stage, the mining game, for a fixed cost vector. Its results (Propositions 4.1–4.4) are the foundation of the paper's comparative statics (Propositions 4.6, 4.8) and of its investment stage (Proposition 5.1), which are posed in the later missions of this series.

Setting

There are $N\ge 2$ miners, indexed $i=1,\dots,N$ . Miner $i$ has a cost-per-hash $c_i>0$ , and the miners are sorted so that $c_1\le c_2\le\dots\le c_N$ . All miners compete for a total reward $R>0$ and share a capacity parameter $\gamma\ge 0$ : a larger $\gamma$ means a tighter hashing capacity.

Each miner chooses a hash rate $h_i\ge 0$ . The aggregate hash rate is $H=\sum_{j=1}^N h_j$ , and miner $i$ 's objective is

\pi_i(h)=\begin{cases}\dfrac{h_i}{H}R-c_ih_i-\dfrac{\gamma}{2}h_i^2, & H>0,\\[4pt] 0, & H=0.\end{cases}

An equilibrium hash rate profile $h^*$ is a nonnegative profile in which no miner can increase its objective by changing its own hash rate to any other nonnegative value. A miner is active if $h^*_i>0$ ; $n$ denotes the number of active miners. The cumulative cost of the first $k$ miners is $c^{(k)}=c_1+\dots+c_k$ , and the marginal cost of miner $i$ at the equilibrium is $MC^*_i=c_i+\gamma h^*_i$ .

In Lean these objects are Params N (fields c, R, γ), Params.Standing, aggH, payoff, IsMiningEq, activeCount, cumCost, aggForm, partCond, margCost and profit, in the namespace PoWMining.Equilibrium.

Formalization targets

Goal: the number of active miners (Proposition 4.4)

An equilibrium exists, and in every equilibrium the number of active miners is the largest $2\le n\le N$ with

c_n<\frac{c^{(n)}+R\gamma/c_n}{n-1}.

This number is weakly increasing in $R$ and in $\gamma$ (with the costs held fixed). The goal identifies the degree of decentralization of the mining stage purely from the model parameters.

Milestones, in the order of the paper's proof

Every equilibrium has at least two active miners (p. 38).
If miner $k+1$ is active in an equilibrium, so is miner $k$ : the active miners are the $n$ cheapest (p. 38).
The first-order condition of an active miner (4.2):

\frac{R}{H^*}\Bigl(1-\frac{h^*_i}{H^*}\Bigr)=c_i+\gamma h^*_i.

Summing (4.2) over the active miners (B.1): $(n-1)R-c^{(n)}H^*-\gamma (H^*)^2=0$ .
Proposition 4.1: the equilibrium exists and is unique, $h^*_i=H^*(R-c_iH^*)/(R+\gamma (H^*)^2)$ for $i\le n$ and $0$ otherwise, and $H^*$ is the positive root

H^*=\frac{\sqrt{(c^{(n)})^2+4(n-1)R\gamma}-c^{(n)}}{2\gamma}\ (\gamma>0),\qquad H^*=\frac{(n-1)R}{c^{(n)}}\ (\gamma=0).\tag{4.1}

Proposition 4.2: $MC^*_i$ increases in $i$ , $MC^*_i<R/H^*\iff c_i<R/H^*\iff i\le n$ , and $c_i/MC^*_i$ increases while $\gamma h^*_i/MC^*_i$ decreases.

A companion statement, Proposition 4.3 (equilibrium profits are decreasing in $i$ , positive exactly for the active miners, and profit-per-hash of the active miners is decreasing), is posed as a theorem of the mission but is not on the goal's proof path.

Significance

The result. Proposition 4.4 says that participation in proof-of-work mining is decided by a single explicit inequality comparing the marginal miner's cost to the average cost of the cheaper miners, corrected by the capacity term $R\gamma/c_n$ . With $\gamma=0$ the condition reads $c_n<\frac{n}{n-1}\cdot\frac{c^{(n)}}{n}$ : the marginal miner's cost may exceed the average active cost only slightly, so cost heterogeneity drives inefficient miners out. The capacity constraint is what keeps them in. The paper's discussion of centralization, its comparative statics of hash rate shares (Propositions 4.6 and 4.8) and its analysis of hardware investment and entry (Proposition 5.1) all take the equilibrium of Proposition 4.1 and the active count of Proposition 4.4 as given.

Formalizing it. The results are proved in the paper (Appendix B, pp. 38–39); none of them is machine-checked. A formal development produces a complete, checked equilibrium analysis of a heterogeneous-cost Tullock contest with quadratic capacity costs: existence and uniqueness of a pure equilibrium, the explicit hash rates, and the participation threshold. The platform currently has no contest, rent-seeking or mining game.

Difficulty

The closed forms are straightforward to verify once the active set is known; the difficulty is the active set itself. The objective is concave in the own hash rate only when the other miners' aggregate is positive, and it jumps at $H=0$ , so the standard concave-game existence theorem does not apply directly on the whole strategy space, and the equilibrium has to be located among profiles with at least two active miners. Uniqueness requires excluding every equilibrium with a different active set, not only the one the formulas produce. For Proposition 4.4, the obvious route, substituting the closed form of $H^*$ into " $c_n<R/H^*$ ", produces a condition in terms of the equilibrium's own $n$ ; showing that the set of $k$ satisfying the printed inequality is an initial segment $\{2,\dots,n\}$ , so that "largest" picks out exactly the equilibrium count, is the step that needs care, and the monotonicity in $R$ and $\gamma$ is a comparison of two different equilibria.

Formalization scope

Miners are Fin N, with Lean index $i$ standing for the paper's miner $i+1$ . The standing assumptions Params.Standing are $N\ge 2$ , $R>0$ , $\gamma\ge 0$ , $c_i>0$ and Monotone c (the paper's sorting, p. 12).
The objective omits the fixed entry cost $K$ of (3.4): with the investment profile fixed it does not depend on the miner's own hash rate. The case $H=0$ is an explicit branch, not Lean's $x/0=0$ .
The equilibrium (Definition 3.2(i)) is the best-response property "for every $x\ge 0$ , deviating to $x$ does not raise the objective", which is equivalent to the paper's " $=\sup_{h_i\ge 0}$ " and avoids junk values of sSup.
"Increasing/decreasing" is weak (Monotone/Antitone), as in the paper's footnote 12. "Largest $n$ " is IsGreatest, not sSup on $\mathbb N$ . Both branches of (4.1) are kept as printed; $\gamma=0$ is allowed throughout.
Ruling out trivializations: the equilibrium is never defined by its closed form and the active count is never defined by the participation condition; the goal includes existence, so its statements about every equilibrium are not vacuous; $N$ and $n$ are general.
Needed infrastructure: elementary real analysis (concavity and one-variable first-order conditions), finite sums over Fin N, quadratic roots. Lemmas about the objective's concavity and best responses, and the initial-segment property of the participation condition, are reusable in the later missions of this series. Contributions of any milestone, or of further intermediate lemmas, are welcome.

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), 1967. https://doi.org/10.1111/j.1465-7295.1967.tb01923.x

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? 2: Signs of the Sensitivities of Equilibrium Hash Rates and Hash Rate Shares to Mining CostsResearch Paper

Motivation

In a proof-of-work cryptocurrency such as Bitcoin, miners spend computing power (hash rate) to win the right to add the next block and collect a reward. Whether this competition stays decentralized depends on how individual hash rates react to differences in mining costs: if a cost advantage translates into an ever larger share of the total hash rate, mining concentrates in a few hands. Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021) model mining as a game among miners with heterogeneous costs and limited capacity, and derive its equilibrium in closed form. Their Section 4.3 then asks how equilibrium hash rates and hash rate shares respond to a change in one miner's cost. This mission formalizes the answer, Proposition 4.6 of that preprint.

Setting

Fix $n \ge 2$ active miners. Miner $i$ has cost-per-hash $c_i > 0$ , and every miner bears the capacity cost $(\gamma/2)h_i^2$ with capacity parameter $\gamma \ge 0$ (a larger $\gamma$ means smaller capacity). The miners compete for a reward $R > 0$ , which miner $i$ wins in proportion to its hash rate $h_i$ over the aggregate hash rate $H = \sum_j h_j$ . Write $c^{(n)} = c_1 + \dots + c_n$ for the cumulative cost.

When exactly these $n$ miners are active, the paper's equilibrium (Proposition 4.1, posed in mission 1 of this series) is explicit. The aggregate hash rate $H^* = g$ is the positive root of $\gamma H^2 + c^{(n)}H - (n-1)R = 0$ :

g = \frac{\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} - c^{(n)}}{2\gamma}\ (\gamma > 0),\qquad g = \frac{(n-1)R}{c^{(n)}}\ (\gamma = 0),

and the individual equilibrium hash rates are $h^*_i = f_i(g)$ with

f_i(G) = G\,\frac{R - c_i G}{R + \gamma G^2}. \tag{B.3}

All $n$ miners being active means $R - c_k g > 0$ for every $k$ . The hash rate share of miner $i$ is $h^*_i/H^* = f_i(g)/g$ .

A change in $c_i$ moves $h^*_i$ in two ways. The direct sensitivity $\Delta_{i,1} = \partial f_i/\partial c_i$ holds the aggregate fixed. The indirect sensitivity $\Delta_{i,2} = (\partial f_i/\partial g)(\partial g/\partial c_i)$ acts through the change of the aggregate. For shares, the paper's decomposition on p. 42 gives $\widetilde\Delta_{i,1} = \frac1g\,\partial f_i/\partial c_i$ and $\widetilde\Delta_{i,2} = \frac1g\,\frac{\partial g}{\partial c_i}\big(\frac{\partial f_i}{\partial g} - \frac{f_i}{g}\big)$ .

Formalization targets

Goal: Proposition 4.6 (p. 17)

For active miners $i \ne j$ , $h^*_i$ and $h^*_i/H^*$ are differentiable in $c_i$ and $c_j$ , and

\frac{\partial h^*_i}{\partial c_i} = \Delta_{i,1} + \Delta_{i,2} < 0,\qquad \frac{\partial h^*_i}{\partial c_j} = \Delta_{i,2},\qquad \Delta_{i,1} < 0,\qquad \Delta_{i,2} > 0 \iff \frac{h^*_i}{H^*} < \frac12,

\frac{\partial}{\partial c_i}\frac{h^*_i}{H^*} = \widetilde\Delta_{i,1} + \widetilde\Delta_{i,2} < 0,\qquad \frac{\partial}{\partial c_j}\frac{h^*_i}{H^*} = \widetilde\Delta_{i,2} > 0,\qquad \widetilde\Delta_{i,1} < 0.

Milestones (Appendix B, pp. 39–42)

(B.2), first line: $\partial H^*/\partial c_i = -H^*/(c^{(n)} + 2\gamma H^*) < 0$ .
(B.5): $R(c_i + \gamma g)/(R + \gamma g^2) = c_i + \gamma f_i$ .
The partial derivatives $\partial f_i/\partial c_i = -g^2/(R+\gamma g^2) < 0$ and $\partial f_i/\partial g = \frac{g}{R+\gamma g^2}\big(\frac Rg - 2(c_i + \gamma f_i)\big)$ .
(B.4), first two lines: closed forms of $\partial h^*_i/\partial c_i$ and $\partial h^*_i/\partial c_j$ .
The sign criterion: $c_i + \gamma f_i = \frac Rg(1 - f_i/g)$ , and $\Delta_{i,2} > 0 \iff c_i + \gamma f_i > \frac{R}{2g} \iff f_i/g < \frac12$ .
(B.6), first two lines: closed forms and signs of the share derivatives in $c_i$ and $c_j$ .

Significance

The proposition separates the effect of a cost change into a direct part, always negative, and an indirect part through the aggregate, whose sign is set by the hash rate share alone. A miner with less than half the total hash rate partly offsets a cost increase, because rivals' responses lower the aggregate; a dominant miner amplifies it. The same indirect term is exactly the response of $h^*_i$ to a competitor's cost. For shares the answer is unconditional: a miner's share falls with its own cost and rises with a rival's. These signs (Table 1 of the paper) are what the paper's later discussion of cost advantages and concentration rests on.

The result is proved in the paper by direct calculation. It has not been machine-checked anywhere known to this series, and no comparative statics of a contest or mining game exists on the platform. Formalizing it checks the differentiation of the closed forms, including the case $\gamma = 0$ , and fixes the definition of $\widetilde\Delta_{i,1}, \widetilde\Delta_{i,2}$ , which the paper uses without defining.

Difficulty

Each step is elementary calculus, but the steps do not close by naive differentiation. The derivative of $h^*_i$ in $c_i$ , computed from the explicit formula, is a rational function of $c_i$ , $g$ and the square root in $g$ . Its sign is not visible until the square root is eliminated through $\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} = c^{(n)} + 2\gamma g$ and the first-order condition of the miner is used to rewrite $c_i + \gamma f_i$ . The equivalence (4.5) depends on the activity condition $R - c_k g > 0$ ; without it $f_i$ can be negative and the sign claims fail. The case $\gamma = 0$ uses the second branch of $g$ , which has no square root, so the paper's middle expression in (B.2) does not apply there.

Formalization scope

Miners are indexed by Fin n, 0-based. Costs are a vector c : Fin n → ℝ. The objects cumCost, gH (both branches of (4.1)), fH (with the aggregate as a free argument G), hstar, share and the four sensitivities are defined in PoWMining.CostStatics.Setting. The standing assumptions $n \ge 2$ , $R > 0$ , $\gamma \ge 0$ , $c_k > 0$ and $R - c_k g > 0$ for all $k$ are bundled in Standing. The last of these is the paper's "for active miners", read at a state where small changes do not alter the set of active miners (pp. 15–16). Costs need not be sorted.

Partial derivatives are one-variable derivatives along Function.update c i, and every derivative claim is a HasDerivAt statement. The sensitivities are defined by deriv, never by their closed forms. A definition $\Delta_{i,1} := -g^2/(R+\gamma g^2)$ would make " $\Delta_{i,1} < 0$ " a positivity check and turn the goal into milestone 4; this is ruled out. Sign claims about a deriv-defined quantity are always paired with the corresponding HasDerivAt claim, so a non-differentiable junk value of $0$ cannot satisfy them. $\gamma = 0$ is allowed throughout.

The sensitivities are derivatives of the closed forms (B.3) of the $n$ active miners, as in the paper's proof. That these closed forms are the equilibrium of the game is Proposition 4.1, and the first-order condition behind milestone 5 is Proposition 4.2; both are posed in mission 1 of this series and are not restated here. Printed slip: the middle term of (B.5) has a sign error ( $c_i - \gamma g\frac{R-c_ig}{R+\gamma g^2}$ for $c_i + \gamma g\frac{R-c_ig}{R+\gamma g^2}$ ); only the outer equality, which the proof uses, is stated.

Proofs need only real arithmetic, Real.sqrt and one-variable derivative rules. Contributions of any milestone are welcome; a lemma computing the derivative of gH along a single cost coordinate is reused by several of them and by the companion mission on capacity and reward.

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 (Proposition 4.6, p. 17; proof pp. 39–42).
S. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. https://bitcoin.org/bitcoin.pdf

8 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Mechanism Design under Approximate Incentive Compatibility 3: Hard/Soft Floor Mechanisms Are Optimal Among Deterministic ε-IC Mechanisms and Gain Θ(ε)Research Paper

Motivation

Classical mechanism design assumes that agents best-respond exactly: a buyer who gains even an infinitesimal amount by misreporting will misreport. In practice agents face cognitive and computational costs, and a buyer may ignore a deviation that gains less than some small amount $\varepsilon$ . A seller facing such a buyer only needs to satisfy the incentive constraints up to $\varepsilon$ , and the natural question is how much revenue this relaxation is worth.

Balseiro, Besbes and Castro (arXiv:2103.03403v2, 2022; Operations Research, 2024) study this question in the simplest setting, one seller and one buyer with a single item. Their answer separates deterministic and randomized mechanisms. This mission formalizes the deterministic half: Theorem 2, which identifies the optimal deterministic $\varepsilon$ -incentive-compatible mechanism and shows that its revenue gain over the classical optimum is exactly linear in $\varepsilon$ .

Setting

The buyer's value $v$ for the item is drawn from a distribution $F$ with a density $f\ge0$ supported in $S=[0,\bar v]$ , $\bar v>0$ , with $\int_0^{\bar v}f=1$ . Assumption 1 adds that $f$ has bounded variation on $S$ . Write $F(v)=\int_0^v f$ , $\bar F=1-F$ , and $R(v)=v\,\bar F(v)$ for the revenue of a posted price $v$ .

A direct mechanism $m=(x,t)$ assigns to each reported value $v$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$ . It is individually rational (IR) if $v\,x(v)-t(v)\ge0$ for all $v\in S$ , and $\varepsilon$ -incentive compatible (IC $_\varepsilon$ ) if

v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\text{for all }v,v'\in S.

$\mathcal M(\varepsilon)$ denotes the feasible mechanisms, and $\mathcal M_d(\varepsilon)=\{m\in\mathcal M(\varepsilon):x(S)\subseteq\{0,1\}\}$ the deterministic ones. The revenue is $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ and $\Pi^\star(\mathcal M)=\sup_{m\in\mathcal M}\Pi(m)$ . At $\varepsilon=0$ the optimum $\Pi^\star(\mathcal M(0))$ is attained by a posted price at any maximizer $p^\star$ of $R$ on $S$ .

The hard/soft floor mechanism $m_d(p,s)$ , $p\le s$ , allocates the item to every report $v\ge p$ ; a report in $[p,s)$ pays its own value and a report $v\ge s$ pays $s$ :

x_d(v)=\mathbf 1\{v\ge p\},\qquad t_d(v)=v\,\mathbf 1\{v\in[p,s)\}+s\,\mathbf 1\{v\ge s\}.

Formalization targets

Goal: Theorem 2 (pp. 24–25)

Under Assumption 1:

for every $\varepsilon>0$ some $m_d(p,p+\varepsilon)$ , $p\in[0,\bar v]$ , lies in $\mathcal M_d(\varepsilon)$ , earns at least as much as every mechanism of $\mathcal M_d(\varepsilon)$ , and maximizes $\Pi(m_d(p',p'+\varepsilon))$ over $p'\in[0,\bar v]$ ;

\Pi^\star(\mathcal M_d(\varepsilon))-\Pi^\star(\mathcal M(0))=\Theta(\varepsilon),

that is, there are $c,C,\varepsilon_0>0$ with $\Pi^\star(\mathcal M(0))+c\varepsilon\le\Pi^\star(\mathcal M_d(\varepsilon))\le\Pi^\star(\mathcal M(0))+C\varepsilon$ for all $\varepsilon\in(0,\varepsilon_0]$ .

Milestones

§2.1, p. 13: a posted price at $p^\star\in\arg\max_S R$ is optimal for $(\mathcal P_0)$ , so $\Pi^\star(\mathcal M(0))=R(p^\star)$ .
Appendix B, p. 53: $m_d(r,r+\varepsilon)\in\mathcal M_d(\varepsilon)$ for every $r\in S$ .
Appendix B, p. 53: $\Pi(m_d(r,r+\varepsilon))=\int_r^{r+\varepsilon}vf(v)\,dv+(r+\varepsilon)\bar F(r+\varepsilon)=r\bar F(r)+\int_r^{r+\varepsilon}\bar F(v)\,dv$ .
Appendix B, eq. (23), pp. 52–53: every $m\in\mathcal M_d(\varepsilon)$ has payments bounded pointwise by those of some $m_d(r,r+\varepsilon)$ , hence $\Pi(m)\le\Pi(m_d(r,r+\varepsilon))$ .

Significance

Theorem 2 settles what deterministic mechanisms can do against an $\varepsilon$ -optimizing buyer: the gain is linear in $\varepsilon$ , no more and no less. The lower half shows that any optimal approximately incentive compatible mechanism gains at least order $\varepsilon$ ; the upper half shows that a seller who wants more must randomize. Together with the paper's Theorems 1 and 3 (other missions of this series), which give the rate $\varepsilon^{\alpha/(2\alpha-1)}$ for randomized mechanisms under a curvature condition on $R$ , it locates the full spectrum of achievable gains between $\varepsilon$ and $\varepsilon^{1/2}$ . The hard/soft floor form is also a practical design: a posted price followed by a pay-your-bid band of width $\varepsilon$ .

The result is proved in the paper's online appendix. To the best of our knowledge it has no machine-checked proof; the classical posted-price optimality has a formalization on Prove2Me under the stronger assumption of a strictly positive density, and this mission needs it for densities that may vanish.

Difficulty

The obvious argument for "an optimal deterministic mechanism is a hard/soft floor" starts from an optimal mechanism, which need not exist a priori, and takes its allocation right-continuous "without loss of generality". Neither step is available for an arbitrary measurable mechanism: the allocation set $\{x=1\}$ may have no least element, and changing $x$ on a null set can break IC $_\varepsilon$ at individual points. The domination milestone is therefore stated for every deterministic mechanism. The revenue identity needs integration by parts for an absolutely continuous $F$ whose density may vanish or be discontinuous, and the comparison with $\Pi^\star(\mathcal M(0))$ needs the classical posted-price optimality without positivity of $f$ . The lower bound needs the optimal price to sit strictly inside $(0,\bar v)$ and $\bar F$ to stay bounded away from zero just above it.

Formalization scope

Values are reals and every function is a total function $\mathbb R\to\mathbb R$ ; only its values on $S=[0,\bar v]$ matter. Mechanisms are required to be measurable (implicit in $\mathbb E_v[t(v)]$ ); IR and IC $_\varepsilon$ then make $t$ bounded on $S$ , so revenue integrals are genuine. $\Pi^\star$ is a supremum (sSup) of a nonempty set of revenues bounded above by $\bar v$ . The goal's $\Theta(\varepsilon)$ is the conjunction of the paper's $\mathcal O$ and $\Omega$ (p. 13), with constants depending on the distribution but chosen before $\varepsilon$ , written as "some deterministic mechanism earns at least $\Pi^\star(\mathcal M(0))+c\varepsilon$ , every one earns at most $\Pi^\star(\mathcal M(0))+C\varepsilon$ "; $\Pi^\star(\mathcal M(0))$ stays a supremum and is not replaced by $R(p^\star)$ . The payment region of $m_d$ is $[p,s)$ as in the proof (the theorem prints $[p,s]$ , which double-counts at $v=s$ ). The hard floor ranges over $[0,\bar v]$ , so the soft floor $p+\varepsilon$ may exceed $\bar v$ .

The domination statement quantifies over all of $\mathcal M_d(\varepsilon)$ , not over monotone or right-continuous mechanisms, and the $\Theta(\varepsilon)$ constants may not depend on $\varepsilon$ ; either restriction would trivialize the result.

The development needs interval integrals, integration by parts for absolutely continuous functions, and continuity of $\bar F$ . The posted-price optimality milestone is reusable for every single-buyer revenue question and is welcome as a stand-alone contribution.

Selected references

S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403v2
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
J. Riley, R. Zeckhauser, Optimal Selling Strategies: When to Haggle, When to Hold Firm, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885622

7 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research+1·Captain: mikedeng1

Scaling Blockchains: Can Committee-Based Consensus Help? I: With a Vote-Probability Gap δ, an Honest Committee Is Elected with Probability at Least 1 − 2m²e^{−δ²n/2}Research Paper

Motivation

Many proof-of-stake blockchains do not let every participant produce blocks. Instead, token holders elect a small committee of block producers, and the committee runs a Byzantine agreement protocol among itself. EOS, for example, elects 21 producers by approval voting: each token holder approves a set of candidates, and the 21 candidates with the most approvals form the committee. Byzantine agreement protocols are safe only while a large enough fraction of the committee is honest, typically more than two thirds, so the security of the whole chain rests on a question of social choice: does approval voting, with voters who see only noisy information about the candidates, elect a committee with enough honest members?

Benhaim, Falk and Tsoukalas (arXiv:2110.08673v2, Management Science 2023) model this election and analyse it. Their main result, Theorem 3, shows that whatever strategies the voters use, as long as the honest candidates are approved with probability at least a fixed margin $\delta$ above the dishonest ones, the probability of electing an honest committee converges to one exponentially fast in the number of voters. This mission formalizes that result.

Setting

There are $n$ voters and $m$ candidates (block producers), and a committee of size $k\le m$ is to be elected. Each voter $i$ submits an approval ballot $\mathcal C_{v_i}$ , a subset of the candidates. The score of candidate $j$ is the number of voters approving it,

\operatorname{score}(j)=X_j=\bigl|\{\,i : j\in\mathcal C_{v_i}\}\bigr| .

The elected committee $\mathbb T$ consists of $k$ candidates with the highest scores. When several candidates tie at the lowest elected score, or when fewer than $k$ candidates have a non-zero score, the paper resolves the choice adversarially. Formally, a set $T$ of candidates is an admissible committee if $|T|=k$ and $X_b\le X_a$ for every $a\in T$ and $b\notin T$ .

Each candidate is honest or dishonest. Let $\mathcal M$ denote the set of dishonest candidates. For a tolerance $p\in[0,1]$ (for instance $p=1/3$ ), the committee is honest, written $\mathbb T=H$ , if it has at least $\lceil(1-p)k\rceil$ honest members. Because ties and filling are adversarial, $\mathbb T=H$ means that every admissible committee has at least $\lceil(1-p)k\rceil$ members outside $\mathcal M$ .

The ballots are random: they are drawn on a probability space, independently across voters, while the approvals inside a single ballot may depend on each other in any way. The vote probability $p_{ij}=\Pr[j\in\mathcal C_{v_i}]$ is the probability that voter $i$ approves candidate $j$ . The candidates' types are fixed throughout, and all randomness is in the ballots.

Formalization targets

Goal: Theorem 3 (p. 22)

Suppose there are a set $\mathcal H$ of honest candidates with $|\mathcal H|\ge(1-p)k$ and a $\delta>0$ with $\min_{i,\,j\in\mathcal H}p_{ij}\ge\max_{i,\,j\in\mathcal M}p_{ij}+\delta$ . Then

\Pr[\mathbb T=H]\ \ge\ 1-2m^2e^{-\delta^2 n/2}.

Milestones (in the order the proof on p. 48 uses them)

Opening claim of the proof (p. 48). If every member of $\mathcal H$ outscores every member of $\mathcal M$ , then $\mathbb T=H$ (deterministic).
Theorem 1 (pp. 15–16). Each vote count is Poisson binomial:

\Pr[X_j=x]=\sum_{|A|=x}\ \prod_{i\in A}p_{ij}\prod_{i\notin A}(1-p_{ij}).

Theorem 6 (p. 50). Chernoff–Hoeffding for a Poisson binomial $X$ with mean $n\bar p$ : $\Pr[X>n\bar p+t]\le e^{-2t^2/n}$ and $\Pr[X<n\bar p-t]\le e^{-2t^2/n}$ for $t>0$ .
(82). For $j_h\in\mathcal H$ , $j_m\in\mathcal M$ : $\Pr[X_{j_h}\le X_{j_m}]\le 2e^{-\delta^2n/2}$ .
(83). $\Pr[X_{j_m}<X_{j_h}\ \forall j_h\in\mathcal H,\ j_m\in\mathcal M]\ge1-2m^2e^{-\delta^2n/2}$ .

Significance

The theorem is the paper's answer to its title question. Its bound holds for every voting behaviour, including the threshold and cardinal strategies the paper studies and strategies with arbitrary correlation inside a ballot. So the security guarantee does not depend on voters coordinating or on knowing the signal model. All it needs is that signals are informative by a margin $\delta$ . The bound also shows the trade-off quantitatively: the failure probability grows quadratically in the number of candidates $m$ and decays exponentially in the number of voters $n$ . This is the basis of the paper's Corollaries 1 and 2 on the threshold and cardinal strategies.

The paper proves the result on paper (Appendix B.2, p. 48), using a Chernoff–Hoeffding bound it cites from Dubhashi and Panconesi. As far as the platform's index shows, no machine-checked version of the result or of its committee model exists. The mission contributes the first formal model of $k$ -winner approval voting with adversarial tie-breaking on Prove2Me, a formal statement of the Poisson-binomial law of approval counts, and the one-sided Hoeffding bound for sums of independent Bernoulli variables in the $e^{-2t^2/n}$ form. The formalization also records three places where the printed text needs correcting (see Formalization scope).

Difficulty

There are two difficulties. The first is the committee predicate. Ties and under-filled committees are resolved by an adversary, so $\mathbb T=H$ is a statement about every admissible committee, not about one top- $k$ list. The reduction from honesty to the score-separation event has to handle both the case where all of $\mathcal H$ is elected and the case where some member of $\mathcal H$ is left out, so that every elected candidate outscores it.

The second is the concentration step. The vote counts of different candidates are not independent, because each voter's ballot ties the approvals together, so no argument that treats the $m$ counts as independent variables applies. The paper's own step from the gap to (82), the split (80)/(81), uses strict inequalities and is false when the two thresholds coincide at an attained integer value; the printed Hoeffding bound (Theorem 6) is strict as well, so the printed chain does not close as written at that boundary.

Formalization scope

Voters are Fin n and candidates Fin m, both 0-based. A random ballot is a measurable map Ω → (Fin m → Bool) on a probability space (Ω, P). The ballots are mutually independent (iIndepFun), and each voter's ballot law is otherwise arbitrary. This generalises the paper's Gaussian signal model and its strategy classes, which are not formalized, and the paper's per-type probabilities $p^h_i,p^m_i$ become per-candidate $p_{ij}$ . The cap $|\mathcal C_v|\le t$ of Definition 2 is not imposed. The printed statements are special cases.
$\mathbb T=H$ is the predicate "every set $T$ with $|T|=k$ and no outsider scoring above a member has $|T\setminus\mathcal M|\ge\lceil(1-p)k\rceil$ ", with an integer ceiling. A formalization in which some admissible committee is honest, or in which the committee is chosen by a fixed tie-breaking rule, is a different and weaker theorem. Without the condition $|T|=k$ the predicate would be trivial. An admissible committee exists for every score vector when $k\le m$ .
Standing assumptions that are made explicit: $k\le m$ (p. 9), $0\le p\le1$ ( $p$ is the tolerated fraction, which the paper never bounds; the opening claim of the proof fails for $p<0$ ), independence across voters (§5.1.2), and measurability of each ballot.
The min/max gap of Theorem 3 is stated pairwise for all voters $i,i'$ , all $j_h\in\mathcal H$ and all $j_m\in\mathcal M$ . This is equivalent when both sets are nonempty and avoids undefined extrema otherwise.
Corrected slips: Theorem 6 is stated for $t>0$ and $n\ge1$ , since it is false for negative $t$ and divides by $n$ . (80)/(81) are not posed, and (82) is stated as a bound on $\Pr[X_{j_h}\le X_{j_m}]$ .
Infrastructure needed: Mathlib's independence, Measure.real, sub-Gaussian concentration for bounded independent variables, and Finset.powersetCard. The committee definitions and the Poisson-binomial law can be reused by later missions on voting and on the companion single-voter result. Proofs of any milestone are welcome, and so are alternative routes to the goal.

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.08673v2 (DOI 10.1287/mnsc.2022.03177)
D. P. Dubhashi, A. Panconesi, Concentration of Measure for the Analysis of Randomized Algorithms, Cambridge University Press, 2009. https://doi.org/10.1017/CBO9780511581274
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.1080/01621459.1963.10500830

8 thms3 active usersReviewed

Completed

Information Theory Linear algebra Quantum Error Correction+1·Captain: mikedeng1

Reversing quantum dynamics with near-optimal quantum and classical fidelity I: The Reversal Operation Attains at Least the Square of the Optimal Average Entanglement FidelityResearch Paper

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

\mathcal A(X)=\sum_iA_iXA_i^\dagger .

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$ .

For a state $\rho$ the paper defines the reversal operation

\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$ ), by the average entanglement fidelity

\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$ , the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$ , and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$ ,

\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .

Milestones

The milestones follow the paper's proof:

Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$ , not on its decomposition.
(14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ( $P_C$ the support projector of $\rho$ ), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$ , and $\mathcal B(\rho)\le\mathcal A(\rho)$ .
(28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$ .
(33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$ .

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$ , and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ .

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$ . It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$ , the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$ , and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$ . The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$ .
$X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$ .
$F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$ .
In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$ ; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$ .
Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$ , and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$ , never the right-hand side of the proof's chain.
Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$ . Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817

7 thms3 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Mechanism Design under Approximate Incentive Compatibility 1: Nisan's Rounding Bounds the Revenue Gain of ε-IC Mechanisms by O(ε^(1/2))Research Paper

Motivation

Classical mechanism design assumes that agents are perfect optimizers: a mechanism is incentive compatible if no buyer gains anything, however small, by misreporting. In practice buyers face cognitive and computational costs, and a buyer may not bother to deviate for a gain below some threshold $\varepsilon$ . Balseiro, Besbes and Castro, Mechanism Design under Approximate Incentive Compatibility (arXiv:2103.03403v2, 2022; Operations Research, 2024), ask how much additional revenue a seller can extract when the incentive constraints only need to hold up to $\varepsilon$ .

A known benchmark answers this at order $\sqrt\varepsilon$ . It comes from a rounding argument attributed to Noam Nisan, used in mechanism design to transform an approximately incentive compatible mechanism into an exactly incentive compatible one (see e.g. Balcan, Blum, Hartline and Mansour, FOCS 2005). The paper states this benchmark as its Proposition 1 and proves it in its online appendix "for completeness". This mission formalizes that benchmark; the paper's sharper, instance-dependent rates are the subject of the other missions of this series.

Setting

A seller sells a single item to one buyer. The buyer's value $v$ is drawn from a distribution $F$ with a density $f\ge 0$ supported in $S=[0,\bar v]$ , $\bar v>0$ , with $\int_0^{\bar v} f=1$ .

A direct mechanism $m=(x,t)$ assigns to each reported value $v\in S$ an allocation probability $x(v)\in[0,1]$ and a payment $t(v)\in\mathbb R$ (payments may be negative). Given $\varepsilon\ge 0$ , the mechanism is

individually rational (IR) if $v\cdot x(v)-t(v)\ge 0$ for all $v\in S$ ;
$\varepsilon$ -incentive compatible (IC $_\varepsilon$ ) if $v\cdot x(v)-t(v)\ge v\cdot x(v')-t(v')-\varepsilon$ for all $v,v'\in S$ .

$\mathcal M(\varepsilon)$ denotes the set of mechanisms satisfying IR and IC $_\varepsilon$ (problem $(\mathcal P_\varepsilon)$ of the paper). For $\varepsilon=0$ this is the classical feasible set, and $\mathcal M(0)\subset\mathcal M(\varepsilon)$ . The revenue of $m$ is $\Pi(m)=\mathbb E_v[t(v)]=\int_0^{\bar v}t(v)f(v)\,dv$ , and the optimal revenue under $\varepsilon$ -IC is

\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m).

The quantity of interest is the revenue gain $\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))$ .

In the Lean development the model is ApproxIC.Rounding.Model (fields vbar, f) with the predicate Model.Standing; mechanisms are Mech (fields x, t); the sets and values are Mset M ε, revenue M m and optRev M ε.

Formalization targets

Goal: Proposition 1 (p. 15)

\Pi^\star(\mathcal M(\varepsilon))-\Pi^\star(\mathcal M(0))=\mathcal O(\varepsilon^{1/2}),

in the paper's notation (p. 13): there are $C>0$ and $\varepsilon_0>0$ , which may depend on the distribution, such that for every $\varepsilon\in(0,\varepsilon_0]$ and every $m\in\mathcal M(\varepsilon)$ ,

\Pi(m)-\Pi^\star(\mathcal M(0))\le C\sqrt\varepsilon .

Milestones (Appendix A, proof of Proposition 1, p. 38)

Fix $m=(x,t)\in\mathcal M(\varepsilon)$ and $\delta\in(0,1)$ , and let $v^\star_\delta(v)\in\arg\max_{w\in S}\{v\cdot x(w)-(1-\delta)t(w)\}$ .

The rounded mechanism $\tilde m=(x(v^\star_\delta(\cdot)),(1-\delta)t(v^\star_\delta(\cdot)))$ lies in $\mathcal M(0)$ .
For $v'=v^\star_\delta(v)$ : $t(v')\ge t(v)-\varepsilon/\delta$ .
The non-asymptotic bound

\Pi(m)-\Pi^\star(\mathcal M(0))\le\frac{\delta}{1-\delta}\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\le 2\delta\,\Pi^\star(\mathcal M(0))+\frac{\varepsilon}{\delta}\qquad(\delta\le 1/2).

Significance

The result. Proposition 1 gives a distribution-free shape for the value of relaxing incentive compatibility: an $\varepsilon$ -optimizing buyer can be exploited for at most order $\sqrt\varepsilon$ extra revenue. It is the starting point against which the paper measures its main contributions: an instance-dependent upper bound of order $\tilde{\mathcal O}(\varepsilon^{\alpha/(2\alpha-1)})$ (Theorem 1) and a matching lower bound (Theorem 3) for distributions whose revenue curve has local $\alpha$ -power envelopes around the optimal price, and the $\Theta(\varepsilon)$ rate for deterministic mechanisms (Theorem 2). Since $\alpha/(2\alpha-1)>1/2$ for every $\alpha>1$ , these show that the $\sqrt\varepsilon$ benchmark is not tight for such distributions. The rounding step itself (milestone 1) is the standard device for converting approximately incentive compatible mechanisms into exactly incentive compatible ones, and is reused across mechanism design.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal single-buyer model with $\varepsilon$ -IC mechanisms that the other missions of the series share, and a formal version of Nisan's rounding argument for a continuum of types.

Difficulty

The paper's proof is short, but it is written for an argmax that is attained and a rounded mechanism that is tacitly measurable. In a formal treatment, the selection $v^\star_\delta$ must be chosen so that $\tilde m$ is measurable and its expected payment is defined. Exact incentive compatibility forces $\tilde x$ to be nondecreasing on $S$ , and that monotonicity has to be established and then turned into measurability. The revenue comparison $\mathbb E_v[\tilde t(v)]\ge(1-\delta)(\mathbb E_v[t(v)]-\varepsilon/\delta)$ needs the integrability of $t\cdot f$ , which comes from IR and IC $_\varepsilon$ bounding $t$ on $S$ , not from an assumption. The milestone-3 bound carries no attainment hypothesis, so a proof must also handle the case in which the maximum over $S$ is not attained. Finally, $\Pi^\star(\mathcal M(0))$ is a supremum, and its nonnegativity (used in $\delta/(1-\delta)\le 2\delta$ ) and its finiteness must be derived from the feasible set.

Formalization scope

Values, allocations and payments are total functions $\mathbb R\to\mathbb R$ ; every condition quantifies over $S=[0,\bar v]$ only, and the revenue integral is over $[0,\bar v]$ .
Standing assumptions (the density half of the paper's Assumption 1): $\bar v>0$ , $f\ge 0$ , $f=0$ off $[0,\bar v]$ , $f$ integrable on $[0,\bar v]$ with integral $1$ . The bounded-variation half of Assumption 1 is not used by Proposition 1 and is not assumed.
Added hypothesis: mechanisms in $\mathcal M(\varepsilon)$ have measurable $x$ and $t$ , so that $\mathbb E_v[t(v)]$ is meaningful.
$\Pi^\star$ is the supremum (sSup) of the revenue image of $\mathcal M(\varepsilon)$ , which is nonempty (the zero mechanism) and bounded above by $\bar v$ ; the goal and milestone 3 are stated for every $m\in\mathcal M(\varepsilon)$ , which is equivalent to the bound on the supremum. $\Pi^\star(\mathcal M(0))$ is never replaced by the posted-price revenue.
$\varepsilon^{1/2}$ is Real.sqrt ε. The constants $C$ and $\varepsilon_0$ are quantified after the distribution and before $\varepsilon$ ; quantifying them after $\varepsilon$ would make the goal trivial.
Milestones 1 and 2 take the argmax selection $v^\star_\delta$ as a map vs with values in $S$ attaining the maximum, as the page assumes. The rounded mechanism is set to $0$ off $S$ ; its measurability is part of the conclusion, not a hypothesis.
Restricting $\mathcal M(\varepsilon)$ to deterministic mechanisms, to nonnegative payments, or defining $\Pi^\star(\mathcal M(0))$ by the optimal posted-price revenue would change the statement and is ruled out.

Needed infrastructure: monotone functions are measurable, interval integrals of bounded measurable functions against an integrable density, and suprema of bounded real sets, all in Mathlib. Contributions of the rounding lemma in reusable form (for general type sets) are welcome.

Selected references

S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05), pp. 605–614, 2005. https://doi.org/10.1109/SFCS.2005.50

5 thms3 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization+1·Captain: mikedeng1

Dynamic Matching: Characterizing and Achieving Constant Regret II: In (SPP)-Acyclic Networks the Static Planning Solution Is Given by Surplus Vectors in {−1, 0, 1}ⁿResearch Paper

Motivation

Centralized markets such as kidney exchanges, ride-sharing platforms and online labor markets match agents who arrive over time. Kerimov, Ashlagi and Gurvich (SSRN 3824407; Management Science, 2023, doi:10.1287/mnsc.2021.01215) study such a market with $n$ agent types and $d$ feasible multi-way matches. Their main result is that, when a fluid linear program called the static-planning problem (SPP) has a unique non-degenerate solution, a periodic resolving policy keeps the regret against the hindsight optimum bounded by a constant of order $1/\epsilon$ at all times, where the general position gap $\epsilon$ is the smallest positive basic variable of (SPP).

The constant $1/\epsilon$ is only informative if one can say what $\epsilon$ is. Section 5 of the paper does this for a class of networks it calls (SPP)-acyclic: there the optimal solution of (SPP) is an explicit signed sum of arrival rates, so $\epsilon$ is an imbalance between sums of arrival probabilities. This mission formalizes that structural result and the lemmas it rests on. It needs no probability: only the combinatorics of the network and linear programming.

Setting

A matching network has agent types $\mathcal A = \{1,\dots,n\}$ and matches $\mathcal M = \{1,\dots,d\}$ . Match $m$ uses one agent of each type in a set $\mathcal A(m)$ with $|\mathcal A(m)| \ge 2$ , every type belongs to some match, and the matching matrix $M \in \{0,1\}^{n\times d}$ has $M_{im} = 1$ iff $i \in \mathcal A(m)$ . Arrival probabilities $\lambda$ satisfy $\lambda_i > 0$ , $\sum_i \lambda_i = 1$ , and match values satisfy $r_m > 0$ .

The matching network graph $\mathcal G$ is the bipartite graph whose vertices are the types and the matches, with an edge between type $i$ and match $m$ iff $i \in \mathcal A(m)$ .

For a right-hand side $b \in \mathbb R^n$ , the static-planning problem is

\max\ r\cdot z\quad\text{s.t.}\quad Mz + s = b,\quad z \in \mathbb R^d_{\ge 0},\ s \in \mathbb R^n_{\ge 0},

and (SPP) is the case $b = \lambda$ . For a solution $(z^*, s^*)$ write $\mathcal M_+ = \{m : z^*_m > 0\}$ (active matches), $\mathcal M_0 = \mathcal M \setminus \mathcal M_+$ (redundant matches), $\mathcal Q_+ = \{j : s^*_j > 0\}$ and $\mathcal Q_0 = \mathcal A \setminus \mathcal Q_+$ .

The network satisfies the general position condition (GP) if (SPP) has a unique optimal solution $(z^*, s^*)$ and it is non-degenerate: $|\mathcal M_+| + |\mathcal Q_+| = n$ . The optimal basis matrix $\mathcal B$ is formed by the columns of $M$ indexed by $\mathcal M_+$ and the unit vectors $e_j$ , $j \in \mathcal Q_+$ .

The (SPP)-residual graph is $\mathcal G$ with the redundant matches removed, and the network is (SPP)-acyclic if it satisfies GP and its (SPP)-residual graph has no cycle.

Formalization targets

Goal: Theorem 5.1 (p. 25)

Assume GP and (SPP)-acyclicity. Then there are vectors $y^l \in \{-1,0,1\}^n$ , $l \in \mathcal M_+ \cup \mathcal Q_+$ , with

z^*_m = y^m\lambda > 0\ (m \in \mathcal M_+),\qquad s^*_j = y^j\lambda > 0\ (j \in \mathcal Q_+),

and every right-hand side $\tilde\lambda > 0$ with $y^l\tilde\lambda > 0$ for all $l$ has, as its unique optimal solution, $z_m = y^m\tilde\lambda$ on $\mathcal M_+$ , $s_j = y^j\tilde\lambda$ on $\mathcal Q_+$ , and zero elsewhere.

Milestones

(4), p. 20. Under GP, $\mathcal B$ is invertible and $(z^*_{\mathcal M_+}, s^*_{\mathcal Q_+}) = \mathcal B^{-1}\lambda > 0$ .
§4.2, p. 20. Under GP the same basis remains optimal for every $\tilde\lambda > 0$ with $\|\tilde\lambda - \lambda\|_\infty \le \zeta_0$ , for some $\zeta_0 > 0$ .
Lemma C.1, p. 44. A connected acyclic matching network graph has at least $n - d + 1$ leaves; under GP with $\mathcal M_0 = \emptyset$ and a connected acyclic residual graph, $|\mathcal Q_+| = n - d$ and some over-demanded queue takes part in exactly one match.

A further theorem item, Lemma 5.1 (p. 24), states that under GP a network with only two-way matches, in which every cycle contains an even number of matches, is (SPP)-acyclic.

Significance

Theorem 5.1 turns the regret constant of the paper's main theorem into a quantity one can read off the data: every positive basic variable, and therefore $\epsilon$ , is $\sum_i y_i\lambda_i$ with coefficients in $\{-1,0,1\}$ . Its second sentence describes the whole region of right-hand sides on which the same basis stays optimal, an open polyhedral cone cut out by the inequalities $y^l\tilde\lambda > 0$ , which is how the paper relates GP to the arrival rates in §5.1.

On the formal side, the mission builds a reusable model of the matching network, its bipartite incidence graph and the static-planning linear program with a variable right-hand side. Prove2Me does not yet contain the structural theory of optimal bases of such programs. Theorem 5.1 and its milestones are proved in the paper (Appendix C and §4.2); none of them is machine-checked yet.

Difficulty

The representation $z^* = \mathcal B^{-1}\lambda$ holds for every network in general position, so the content of the theorem lies in two places.

The entries of $\mathcal B^{-1}$ . Inverses of $0/1$ matrices have arbitrary rational entries in general: the triangle network (three types, matches $\{1,2\},\{2,3\},\{1,3\}$ ) has an optimal basis whose inverse has entries $\pm\tfrac12$ . The claim needs the acyclic structure of the residual graph in an essential way.
The second sentence. Exhibiting numbers $y^l$ with $y^l\lambda = z^*_l$ is trivial and says nothing. The statement requires the same vectors to produce the unique optimal solution for a whole open set of right-hand sides, which forces them to be the rows of $\mathcal B^{-1}$ . This step therefore also involves the optimality conditions of (SPP) and the uniqueness part of GP.

Formalization scope

Types are Fin n, matches Fin d, both 0-based. The topology is the structure MatchingNetwork with the fields $|\mathcal A(m)| \ge 2$ and "every type is in a match"; $\lambda$ and $r$ are separate vectors with the standing predicates $\lambda_i > 0$ , $\sum_i\lambda_i = 1$ and $r_m > 0$ , which are hypotheses of every theorem. The optimal solution $(z^*, s^*)$ is an argument together with the GP hypothesis, never a default or a choice. The graph is a SimpleGraph on Fin n ⊕ Fin d; the residual graph keeps redundant matches as isolated vertices, which affects neither acyclicity nor the degrees of type vertices. The column index type of $\mathcal B$ is $\mathcal M_+ \sqcup \mathcal Q_+$ , and the inverse is a two-sided inverse over these index types, not Matrix.inv, which is $0$ on singular matrices.

Conventions the statements commit to:

in Theorem 5.1, "induces the optimal solution" is read as the unique optimal solution, and $\tilde\lambda$ is any positive vector, not necessarily summing to one;
"for all sufficiently small $\zeta_0$ " in milestone 2 is the existence of one $\zeta_0 > 0$ ;
Lemma C.1's count of $n - d + 1$ leaves is stated without natural-number subtraction;
Lemma C.1's second half carries the standing reduction of Appendix C ( $\mathcal M_0 = \emptyset$ , one connected component) as hypotheses;
"every cycle contains an even number of matches" in Lemma 5.1 is stated as "every cycle of the bipartite graph has length divisible by 4".

The paper's own text says "all entries of $Y$ are either $-1$ , $0$ , or $-1$ " (p. 25); this is read as $-1$ , $0$ or $1$ , as in the theorem's statement.

A formalization that keeps only the first sentence of Theorem 5.1, or that lets the vectors $y^l$ be unrelated to the basis, is trivially satisfiable and is not the theorem.

Needed infrastructure: optimality conditions for linear programs in equality form (reduced costs, uniqueness of a non-degenerate optimum), Mathlib's acyclic graphs and trees (SimpleGraph.IsAcyclic, IsTree.card_edgeFinset), and degree counting on bipartite graphs. The paper proves Theorem 5.1 in Appendix C by an explicit construction along paths of the residual graph; any correct argument is welcome. Lemmas on the inverse of a basis matrix whose bipartite row–column graph is a forest would be reusable well beyond this mission.

Selected references

S. Kerimov, I. Ashlagi, I. Gurvich, Dynamic Matching: Characterizing and Achieving Constant Regret, SSRN 3824407 (version of September 14, 2022); Management Science (2023). https://ssrn.com/abstract=3824407, https://doi.org/10.1287/mnsc.2021.01215
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.1 (sensitivity analysis of an optimal basis).

10 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Operations Research·Captain: mikedeng1

Offline Multi-Action Policy Learning: Generalization and Optimization 2: Depth-L Decision Trees Satisfy log N_H(ε,Π_L) ≤ (2^L−1)log p + 2^L log d + (2^L−1)log(L/ε+1)Research Paper

Motivation

Offline policy learning chooses a treatment rule from logged data: given $n$ observations of features $X_i$ , the action $A_i$ taken and the reward obtained, pick a policy $\pi:\mathcal X\to\{1,\dots,d\}$ from a class $\Pi$ whose expected reward is close to the best in the class. Zhou, Athey and Wager (arXiv:1810.04778v2) bound the regret of their cross-fitted augmented inverse-propensity-weighted learner by a quantity of order $\kappa(\Pi)\sqrt{V_*/n}$ , where $\kappa(\Pi)$ is an entropy integral built from Hamming covering numbers of $\Pi$ . A bound of this kind is only useful for a concrete policy class if $\kappa(\Pi)$ is finite and explicit.

Decision trees are the class the paper uses in practice: they are interpretable, they are the standard object in personalized-treatment applications, and the paper's computational sections (a mixed-integer program and a tree-search algorithm) optimize over them. Lemma 4 of the paper is the bridge between the general regret theory and trees: it bounds the Hamming covering number of the class $\Pi_L$ of depth- $L$ trees, and hence $\kappa(\Pi_L)$ . Covering and complexity bounds for trees in the 0–1 (two-action) setting go back to VC-dimension arguments; the multi-action Hamming-cover version here is the one this paper's regret bound consumes.

Setting

Features are points $x\in\mathbb R^p$ with components $x(1),\dots,x(p)$ ; there are $d$ actions, written $1,\dots,d$ . A deterministic policy is a map $\pi:\mathbb R^p\to\{1,\dots,d\}$ .

Hamming distance and covers. Fix points $x_1,\dots,x_n$ (repetitions allowed). For two policies,

H(\pi_1,\pi_2)=\frac1n\sum_{j=1}^n\mathbf 1\{\pi_1(x_j)\ne\pi_2(x_j)\}.

The $\varepsilon$ -Hamming covering number $N_H(\varepsilon,\Pi,\{x_1,\dots,x_n\})$ is the least $K$ such that some $\pi_1,\dots,\pi_K\in\Pi$ have every $\pi\in\Pi$ within Hamming distance $\varepsilon$ of some $\pi_i$ . The covering number of the class is the worst case over point sets,

N_H(\varepsilon,\Pi)=\sup\{N_H(\varepsilon,\Pi,\{x_1,\dots,x_m\}) : m\ge1\},

and the entropy integral is $\kappa(\Pi)=\int_0^1\sqrt{\log N_H(\varepsilon^2,\Pi)}\,d\varepsilon$ .

Decision trees. A depth- $L$ tree has $L$ layers: $L-1$ layers of branch nodes and a final layer of leaves, so $2^{L-1}-1$ branch nodes and $2^{L-1}$ leaves; a depth-1 tree is a single leaf. A branch node carries a split variable $i\in\{1,\dots,p\}$ and a threshold $b\in\mathbb R$ , and sends $x$ to its left child if $x(i)<b$ and to its right child otherwise. Each leaf carries an action. $\Pi_L$ is the set of policies computed by depth- $L$ trees. In the Lean development these are DTree p d L, DTree.eval and treePolicies p d L; the Hamming layer is hammingDist, hammingCoverNumOn, hammingCoverNum and entropyIntegral.

Formalization targets

Goal: Lemma 4, part 1 (p. 27)

For $p,d,L\ge1$ and $\varepsilon>0$ , $N_H(\varepsilon,\Pi_L)$ is finite and

\log N_H(\varepsilon,\Pi_L)\le(2^L-1)\log p+2^L\log d+(2^L-1)\log\Big(\frac L\varepsilon+1\Big).

Milestones (App. F)

Display (66), p. 67: for any reals $r_1,\dots,r_m$ there are $\lceil L/\varepsilon\rceil$ thresholds $b_i$ such that every indicator $\mathbf 1_b(r)=\mathbf 1\{r<b\}$ is within Hamming distance $\varepsilon/L$ of some $\mathbf 1_{b_i}$ with respect to $r_1,\dots,r_m$ .
App. F, Step 2, p. 69: for any $n\ge1$ points, $p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ depth- $L$ trees $\varepsilon$ -cover $\Pi_L$ , i.e. $N_H(\varepsilon,\Pi_L,\{x_1,\dots,x_n\})\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ .
App. F, Step 2, p. 69: $N_H(\varepsilon,\Pi_L)\le p^{2^L-1}\lceil L/\varepsilon\rceil^{2^L-1}d^{2^L}$ .

Companion: Lemma 4, part 2 (p. 27)

\kappa(\Pi_L)\le\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1}.

It is posed as printed, as a second theorem of the mission rather than a milestone of the goal.

Significance

The result. Lemma 4 makes the abstract regret theory of the paper concrete: with part 2 it gives Theorem 4, the regret bound $O_p\big((\sqrt{(2^L-1)\log p+2^L\log d}+\tfrac43L^{1/4}\sqrt{2^L-1})\sqrt{V_*/n}\big)$ for learning depth- $L$ trees, which for fixed $L,p,d$ is $O_p(\sqrt{V_*/n})$ . The covering bound grows only logarithmically in $1/\varepsilon$ , which is the property the paper's Assumption 3 asks of a policy class. The same counting gives covering bounds for any class of piecewise-constant rules on axis-aligned partitions of bounded depth.

Formalizing it. The result is proved in the paper (App. F) but, as far as known, has no machine-checked proof. The paper omits the induction that combines per-node threshold grids into a cover of whole trees ("a straightforward but lengthy induction (omitted)"), and its appendix counts $2^L-1$ branch nodes where §6.1's trees have $2^{L-1}-1$ . A formal proof fixes both: it supplies the omitted induction and confirms that the printed bound holds for the class actually defined in §6.1. The milestones are reusable statements about threshold indicators and tree covers. The companion part 2 is posed with the printed constant $4/3$ , although the printed derivation evaluates $\int_0^1(L/\varepsilon^2)^{1/4}d\varepsilon$ as $\frac43L^{1/4}$ where the integral equals $2L^{1/4}$ ; whether the printed bound holds is part of what the mission settles.

Difficulty

The one-dimensional step (66) is elementary once the Hamming distance between two threshold indicators is identified with a count of points between the thresholds. The difficulty is in passing from single thresholds to whole trees. Replacing each branch node's threshold independently by its nearest grid threshold, with grids built on all $n$ points, does not give an $\varepsilon$ cover: the errors at different nodes of the same layer add up, and the naive bound is $(2^{L-1}-1)\varepsilon/L$ rather than $\varepsilon$ . The points that reach a node depend on the thresholds above it, so the approximation has to respect the tree structure, while the number of candidate trees must still be counted as a product over nodes. The passage from finite point sets to $N_H(\varepsilon,\Pi_L)$ , which is a supremum over all point sets in $\mathbb N\cup\{\infty\}$ , and the arithmetic with $\lceil L/\varepsilon\rceil$ and real logarithms are routine but must be done in the stated types.

Formalization scope

Features range over all of $\mathbb R^p$ (Fin p → ℝ); the paper's $\mathcal X$ is a bounded subset of $\mathbb R^p$ , and a bound over $\mathbb R^p$ implies the bound over every $\mathcal X\subseteq\mathbb R^p$ . Actions are Fin d, split variables Fin p (0-based); policies are deterministic.
Point sets are sequences Fin m → (Fin p → ℝ) with repetitions allowed, $m\ge1$ ; covers are proper (centres in $\Pi_L$ ). $N_H(\varepsilon,\Pi)$ is in ℕ∞, $\kappa(\Pi)$ a lower Lebesgue integral in ℝ≥0∞ over $(0,1]$ .
Depth follows §6.1: DTree p d 1 are leaves, DTree p d 0 is empty. The bounds are the printed ones, which over-count for this convention; the Lean was not switched to the appendix's convention, which would change $\Pi_L$ .
Standing hypotheses: $p\ge1$ , $d\ge1$ , $L\ge1$ ("Let $L$ be any fixed positive integer"), $\varepsilon>0$ (needed for $\lceil L/\varepsilon\rceil$ ).
The goal asserts finiteness of $N_H(\varepsilon,\Pi_L)$ explicitly. Without it the inequality would be trivially true for an infinite covering number, because Lean's toNat ⊤ = 0 and Real.log 0 = 0. The covering number is an infimum that is $0$ only for an empty class, and $\Pi_L$ is nonempty under the hypotheses, so the cover is not trivialized either.
Not posed: the $O(\log 1/\varepsilon)$ remark of Lemma 4.1 (a remark on the right-hand side); Theorem 4 (p. 28, the combination with the regret theorem, which belongs to the companion mission on regret); the mixed-integer program and tree search of §6.2–6.3 and App. G (computational).

Contributions welcome: proofs of the milestones, the omitted per-node induction as a stand-alone lemma, and the companion part 2.

Selected references

Z. Zhou, S. Athey, S. Wager, Offline Multi-Action Policy Learning: Generalization and Optimization, arXiv preprint, 2018 (v2). https://arxiv.org/abs/1810.04778
L. Breiman, J. Friedman, R. Olshen, C. Stone, Classification and Regression Trees, Wadsworth, 1984. https://doi.org/10.1201/9781315139470
D. Bertsimas, J. Dunn, Optimal classification trees, Machine Learning 106, 1039–1082, 2017. https://doi.org/10.1007/s10994-017-5633-9
S. Athey, S. Wager, Policy Learning With Observational Data, Econometrica 89(1), 133–161, 2021. https://doi.org/10.3982/ECTA15732

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Fair and Consistent Prize Allocation in Competitions 2: Anonymity, Order Preservation, Winner Strict Endowment Monotonicity and Local Consistency Characterize Single-Parametric RulesResearch Paper

Prize money in rank-order competitions

Tournaments, races, poker finals and sports leagues end with a ranking of the participants and a sum of prize money to be split among them. The split is usually fixed by a published schedule, and different events use very different schedules: some pay almost everything to the winner, some pay many places, some decay geometrically from one place to the next. Dietzenbacher and Kondratev (arXiv:2008.08985, published in Management Science, 2023) treat the choice of schedule axiomatically: they state fairness, solidarity and consistency properties that a prize allocation rule may satisfy and characterize the families of rules that satisfy them. Their paper has three characterization theorems. Theorem 1 (interval rules) is the subject of a companion mission; this mission formalizes Theorem 2, the characterization of single-parametric rules under local consistency.

Axiomatic characterizations of allocation rules through consistency have a long history in fair division: bankruptcy problems (Aumann and Maschler, 1985), taxation (Young, 1987), bargaining (Lensberg, 1987) and cooperative games (Peleg, 1986; Hart and Mas-Colell, 1989); the paper's §1 surveys this literature. The paper is, by its own account, the first to apply this approach to prize allocation in rank-order competitions.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite set $N\subseteq U$ , a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$ ) and a prize endowment $E\ge0$ . For $S\subseteq N$ the subranking $\mathcal R_S$ lists $S$ in the order of $\mathcal R$ . A prize allocation rule $\varphi$ assigns to each competition nonnegative prizes $\varphi_i(N,\mathcal R,E)$ , $i\in N$ , with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$ .

The axioms of Theorem 2 are:

anonymity: the prize depends only on $|N|$ , the position and $E$ , not on who the competitors are;
order preservation: a higher-ranked competitor never receives less than a lower-ranked one;
winner strict endowment monotonicity: when $E$ increases, nobody receives less, and the winner receives strictly more;
local consistency: if a block $S$ of consecutively ranked competitors (the condition $|\mathcal R(i)-\mathcal R(j)|\le|S|-1$ for all $i,j\in S$ ) re-divides the total prize it received, using the rule on the reduced competition $(S,\mathcal R_S,\sum_{j\in S}\varphi_j(N,\mathcal R,E))$ , each member gets the same prize as before.

A representation is a continuous, non-decreasing $f:\mathbb R_+\to\mathbb R_+$ with $f(x)\le x$ . The single-parametric rule with representation $f$ pays $x$ to the winner, $f(x)$ to the runner-up, $f(f(x))$ to the third, and in general

\varphi_i(N,\mathcal R,E)=f^{(\mathcal R(i)-1)}(x),\qquad\text{where } x\ge0 \text{ solves } \sum_{k=1}^{|N|}f^{(k-1)}(x)=E .

Equal Division ( $f(x)=x$ ), Winner-Takes-All ( $f=0$ ), Winner-Takes-Surplus ( $f(x)=\min\{a,x\}$ ) and the arithmetic rule $f(x)=\max\{0,x-1\}$ are examples.

Formalization targets

Goal: Theorem 2 (p. 18)

\varphi \text{ satisfies anonymity, order preservation, winner strict endowment monotonicity and local consistency} \iff \varphi \text{ is a single-parametric rule.}

Both directions are part of the goal.

Milestones, in the order the proof on pp. 31–32 uses them

Converse (p. 31): every single-parametric rule satisfies the four axioms.
The representation (p. 31): on a two-competitor competition, the allocation path $E\mapsto(\varphi_1,\varphi_2)$ is the graph $\{(x,f(x))\}$ of a well-defined representation $f$ .
Two-competitor form (p. 31): by anonymity, the rule is the single-parametric rule with representation $f$ on every competition with two competitors.
Propagation (pp. 31–32): if the single-parametric rule $\varphi'$ with representation $f$ first exceeds $\varphi$ at position $i$ , then $\varphi'_j\ge\varphi_j$ for every $j>i$ .
Uniqueness (p. 32): a locally consistent rule that follows $f$ on two competitors coincides with $\varphi'$ everywhere.

The paper's Lemma 1 (endowment monotonicity implies endowment continuity, p. 10) is used at the start of the proof; it is formalized in the companion mission on interval rules, and the milestones here take endowment continuity as a hypothesis.

Companions

Existence and uniqueness of $x$ (p. 18): for every representation $f$ , $|N|\ge1$ and $E\ge0$ the equation $\sum_{k=1}^{|N|}f^{(k-1)}(x)=E$ has exactly one solution $x\ge0$ .
Corollary 5 (p. 19): a single-parametric rule satisfies winner-loser strict order preservation iff $f(x)<x$ for $x>0$ ; strict order preservation iff $0<f(x)<x$ for $x>0$ ; strict endowment monotonicity iff $f$ is increasing.
Corollary 6 (p. 20): anonymity, order preservation, endowment additivity and local consistency characterize the geometric rules $\varphi_i=\lambda^{\mathcal R(i)-1}E/\sum_{k=1}^{|N|}\lambda^{k-1}$ , $\lambda\in[0,1]$ .

Significance

Theorem 2 reduces an infinite family of allocation schedules, one for every number of competitors and every endowment, to one function of one real variable. A designer who accepts the four axioms only has to choose how the prize of one position determines the prize of the next; the schedule for every field size and every endowment then follows. Corollaries 5 and 6 translate further axioms into shape conditions on that function, and identify the geometric schedules used in practice (the paper fits one to a poker final, p. 20) as the scale-invariant case. Local consistency is the property that a league split into consecutive divisions pays every division the same as the whole league would.

The result is proved in the paper; nothing here is open. No part of it has been formalized before: the platform has no model of prize allocation rules or of consistency axioms over variable populations. The mission produces that model (competitions over a universe of competitors, subrankings, the axioms) and a machine-checked proof of the characterization, including the "readily checked" converse that the paper leaves to the reader.

Difficulty

The converse requires that the parameter $x$ be well defined: the map $x\mapsto\sum_{k}f^{(k-1)}(x)$ must be shown continuous, strictly increasing and onto $\mathbb R_+$ , so that it can be inverted, and local consistency then requires identifying the parameter of a reduced competition with an iterate of the original one. In the forward direction the representation $f$ is defined only implicitly, as the second coordinate of the two-competitor allocation path; its continuity and monotonicity come from inverting the strictly increasing winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$ , which needs both endowment continuity and the strict part of winner strict endowment monotonicity. Without the strict part the runner-up's prize is not a function of the winner's, and the paper's Example 5 shows that local consistency alone then does not determine the rule from its two-competitor restriction. The extension from two to many competitors is a comparison argument over positions that uses local consistency only on adjacent pairs.

Formalization scope

Competitions. A ranking is a duplicate-free nonempty List U, best competitor first; $N$ is its set of entries and $\mathcal R(i)$ is the 1-based position pos l i. The subranking $\mathcal R_S$ is the sublist of entries in $S$ . $U$ is any type with decidable equality; the goal and the corollaries carry the page's standing assumptions [Countable U] and the existence of three distinct elements. Milestones that do not need them omit them.
Rules are functions List U → ℝ → U → ℝ. A prize allocation rule is nonnegative and exhausts $E$ on every ranking and every $E\ge0$ ; values elsewhere are irrelevant, and every axiom quantifies only over rankings, $E\ge0$ and competitors in $N$ .
Representations are functions on $\mathbb R$ constrained on $[0,\infty)$ only: ContinuousOn and MonotoneOn on Set.Ici 0, and $0\le f(x)\le x$ for $x\ge0$ . Requiring global continuity or monotonicity on $\mathbb R$ would shrink the family and is not done. The sum $\sum_{k=1}^{|N|}f^{(k-1)}(x)$ uses the iterate f^[k] with the index shifted to $k=0,\dots,|N|-1$ ; " $x$ is chosen such that" is an existential, and uniqueness of $x$ is a separate item.
Trivializing encodings ruled out. The rule is defined on every competition over $U$ , not on a fixed competitor set; local consistency ranges over exactly the blocks of consecutive positions (using full consistency instead would make the "if" direction false for most $f$ ); the goal is a biconditional; the family requires continuity of $f$ and is not restricted to a closed form.
Infrastructure. The model and the axioms shared with the companion missions on interval and parametric rules are one common set of definitions; this mission adds three: local consistency, single-parametric rules, and geometric rules. Lemma 1 and the facts about inverting a continuous strictly increasing function on $\mathbb R_+$ are reusable beyond this mission. Proofs of any item, and of the companions, are welcome.

Selected references

B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 2023. https://arxiv.org/abs/2008.08985 , https://doi.org/10.1287/mnsc.2022.4520
R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36, 1985. https://doi.org/10.1016/0022-0531(85)90102-4

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Fair and Consistent Prize Allocation in Competitions 3: Anonymity, Order Preservation, Winner Strict Endowment Monotonicity and Top Consistency Characterize Parametric RulesResearch Paper

Motivation

Rank-order competitions — sports tournaments, poker final tables, golf tours, crowdsourcing contests, sales leagues — end with a ranking of the participants and a pot of prize money that has to be split according to that ranking. Organisers publish prize tables that change with the number of entrants and with the size of the purse, and these tables are usually justified only by tradition. Dietzenbacher and Kondratev (arXiv:2008.08985v2, published in Management Science 2023, doi:10.1287/mnsc.2022.4520) take the axiomatic approach of fair-division theory and ask which prize allocation rules are characterised by natural requirements of fairness and coherence across competitions of different sizes.

Consistency — invariance of a rule under "re-running the allocation" for a subgroup with the money it collectively received — has a long history in axiomatic allocation: bankruptcy problems (Aumann and Maschler 1985), taxation (Young 1987), bargaining (Lensberg 1987, 1988) and cooperative games (Peleg 1986; Hart and Mas-Colell 1989). The paper applies it to competitions. Full consistency together with order preservation and endowment monotonicity yields the interval rules (Theorem 1); weakening consistency to local consistency yields the single-parametric rules (Theorem 2). This mission concerns the weakest version, top consistency, which only constrains the top segment of the ranking and describes real prize schemes such as the golf tournament of Table 1(b) of the paper. It is the third mission of a series on this paper; the first two treat Theorems 1 and 2.

Setting

Fix a countable set $U$ of at least three potential competitors. A competition $(N,\mathcal R,E)$ consists of a finite nonempty set $N\subseteq U$ , a ranking $\mathcal R:N\to\{1,\dots,|N|\}$ (a bijection; competitor $i$ is ranked above $j$ when $\mathcal R(i)<\mathcal R(j)$ ), and a prize endowment $E\ge0$ . For $S\subseteq N$ the subranking $\mathcal R_S:S\to\{1,\dots,|S|\}$ orders $S$ as $\mathcal R$ does.

A prize allocation rule $\varphi$ assigns to each competition a vector $\varphi(N,\mathcal R,E)\in\mathbb R_+^N$ with $\sum_{i\in N}\varphi_i(N,\mathcal R,E)=E$ . The axioms are:

anonymity: $\varphi_i(N,\mathcal R,E)=\varphi_j(N',\mathcal R',E)$ whenever $|N|=|N'|$ and $\mathcal R(i)=\mathcal R'(j)$ ;
order preservation: $\mathcal R(i)<\mathcal R(j)$ implies $\varphi_i\ge\varphi_j$ ;
winner strict endowment monotonicity: if $E<E'$ then $\varphi_i(N,\mathcal R,E)\le\varphi_i(N,\mathcal R,E')$ for all $i$ , strictly for the winner $\mathcal R(i)=1$ ;
top consistency: for each $S\subseteq N$ with $\mathcal R(i)\le|S|$ for every $i\in S$ , and each $i\in S$ ,

\varphi_i(N,\mathcal R,E)=\varphi_i\Big(S,\mathcal R_S,\sum_{j\in S}\varphi_j(N,\mathcal R,E)\Big).

A rule is parametric if there are continuous non-decreasing $f_1,f_2,\dots:\mathbb R_+\to\mathbb R_+$ with $f_1(x)=x$ and $f_{k+1}(x)\le f_k(x)$ such that $\varphi_i(N,\mathcal R,E)=f_{\mathcal R(i)}(x)$ , where $x\ge0$ solves $\sum_{k=1}^{|N|}f_k(x)=E$ . The winner gets $x$ and position $k$ gets $f_k(x)$ . Equal Division ( $f_k(x)=x$ ) and Winner-Takes-All ( $f_k=0$ for $k\ge2$ ) are parametric.

Formalization targets

Goal: Theorem 3 (p. 22)

\varphi \text{ is anonymous, order preserving, winner strictly endowment monotonic and top consistent}\iff\varphi\text{ is a parametric rule.}

Both directions are part of the goal.

Milestones (proof of Theorem 3, pp. 32–33)

Every parametric rule satisfies the four axioms (the "readily checked" direction).
Under order preservation, endowment continuity and winner strict endowment monotonicity, the winner's prize $E\mapsto\varphi_1(N,\mathcal R,E)$ is strictly increasing, continuous and unbounded on $\mathbb R_+$ , so each $x\ge0$ is the winner's prize for exactly one $E$ .
The induction step: a representation $f_1,\dots,f_n$ valid on all competitions with at most $n$ competitors extends, by a new continuous non-decreasing $f_{n+1}\le f_n$ , to all competitions with $n+1$ competitors.

Lemma 1 of the paper (endowment monotonicity implies endowment continuity, p. 10) is used in the proof; it is formalized in the first mission of this series and will be referenced from there.

Companion: Corollary 8 (p. 22)

Replacing winner strict endowment monotonicity by endowment additivity (equivalently scale invariance) characterises the proportional rules $\varphi_i=\lambda_{\mathcal R(i)}E/\sum_{k\le|N|}\lambda_k$ with $\lambda_1>0$ and $\lambda_{k+1}\le\lambda_k$ .

Significance

Theorem 3 says that the four axioms leave exactly one degree of freedom per position: a monotone function of the winner's prize. This gives organisers a complete menu of prize schemes that are fair in the anonymous, order-preserving sense and that keep the top of the table unchanged when lower-ranked entrants leave — the property that matters when competitors are eliminated one at a time and paid at the moment of elimination. It contains the single-parametric rules of Theorem 2, the Winner-Takes-Surplus rules, the geometric rules and the proportional rules (Corollary 8) as special cases, and the paper shows in a Remark (p. 33) that the four axioms are logically independent.

The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. The formalization adds a reusable layer for variable-population allocation problems — rankings of finite subsets of a fixed universe, subrankings, and consistency axioms restricted to families of subsets — that is not in Mathlib. Formal proofs of both directions, of the milestones, and of Corollary 8 are all welcome.

Difficulty

The "if" direction is a computation, but it requires showing that the parameter $x$ is well defined and moves monotonically with $E$ , which uses $f_1(x)=x$ and the intermediate value theorem. The "only if" direction must construct the functions $f_k$ from an abstract rule. The natural first idea — define $f_k(x)$ as the prize of position $k$ when the winner receives $x$ — needs the winner's prize to be invertible as a function of $E$ , which uses continuity (supplied by Lemma 1, not assumed), strict monotonicity only for the winner, and unboundedness, which comes from order preservation together with exhaustion of the endowment. Top consistency then has to transfer the representation from competitions of size $n$ to size $n+1$ , and anonymity has to transfer it from one ranked set to every other one of the same size; the induction over the number of competitors must keep all smaller sizes, since top consistency reduces to every top segment.

Formalization scope

A ranked set $(N,\mathcal R)$ is a duplicate-free nonempty List U, best competitor first; $\mathcal R(i)$ is the 1-based index pos l i, and $\mathcal R_S$ is the sublist of entries in $S$ . $U$ is an arbitrary type with decidable equality; the paper's standing assumptions (countable, at least three elements) are hypotheses of the goal and of Corollary 8, and are omitted from milestones that do not use them.
A rule is a function φ : List U → ℝ → U → ℝ; it is required to be a prize allocation rule (nonnegative prizes summing to $E$ ) on rankings and $E\ge0$ , and every axiom quantifies only over that domain. Endowments are reals with $E\ge0$ .
The representation $f_1,f_2,\dots$ is f : ℕ → ℝ → ℝ, indexed from 1 as on the page ( $f_0$ unused); continuity, monotonicity, nonnegativity and $f_1(x)=x$ are required on $[0,\infty)$ . The parameter $x$ is given existentially; it is unique, so this is the page's "where $x\in\mathbb R_+$ is such that".
Endowment continuity is coordinatewise continuity on $[0,\infty)$ .

Trivializing formalizations are ruled out: rules act on every finite ranked subset of $U$ , not on a fixed competitor set; top consistency quantifies over exactly the top segments (full or local consistency would change the theorem — the rule of Example 6 is parametric but not locally consistent); the goal is a biconditional; the parametric family includes $f_1=\mathrm{id}$ , the decreasing chain $f_{k+1}\le f_k$ , and continuity of every $f_k$ .

Corollary 7 of the paper is not included: its "only if" parts ("for each $k$ ") fail as written when $U$ is finite, since $f_k$ for $k>|U|$ is not determined by the rule.

Selected references

B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science, 2023. https://arxiv.org/abs/2008.08985v2, https://doi.org/10.1287/mnsc.2022.4520
R. J. Aumann and M. Maschler, Game theoretic analysis of a bankruptcy problem from the Talmud, Journal of Economic Theory 36(2):195–213, 1985. https://doi.org/10.1016/0022-0531(85)90102-4
S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57(3):589–614, 1989. https://doi.org/10.2307/1911054

9 thms3 active usersReviewed

Completed

Analysis Control Theory Economics+1·Captain: mikedeng1

Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost II: Condition 2, High Switching Cost, Not-Hiring Value Functions Meet the Optimality ConditionsResearch Paper

Motivation

Firms that outsource work to an agent whose effort they cannot observe often punish poor performance by suspending the relationship for a while, even though restarting costs money: a new set-up, re-training, re-mobilisation. Cao, Sun and Tian (Management Science, 2024) study this trade-off in a continuous-time principal–agent model with Poisson arrivals and a fixed switching cost paid every time work (re)starts. They characterise the optimal dynamic contract in three regimes: never hire the agent, hire and keep the agent working forever, or a control-band contract with suspension episodes of fixed length. The model extends the Poisson-arrival contracting framework of Sun and Tian (2018) by adding the switching cost.

The proof follows a guess-and-verify pattern. A stochastic verification theorem (Theorem 1 of the paper) turns any pair of functions satisfying a system of quasi-variational inequalities into an upper bound on the principal's value. Propositions 2–7 then supply such a pair in each parameter region. This mission covers one region: the agent is much more impatient than the principal (Condition 2) and the switching cost is high.

Setting

A principal earns revenue $R$ per arrival of a Poisson process. Without the agent's effort the arrival rate is $\underline\mu\ge0$ ; with effort it is $\mu>\underline\mu$ , and effort costs the agent $b>0$ per unit of time. While the agent works, the principal's total cost rate is $c\ge b$ . Each time work starts or restarts, the principal pays a switching cost $K>0$ . The principal discounts at rate $r$ and the agent at rate $\rho$ , with $0<r\le\rho$ . Write $\Delta\mu=\mu-\underline\mu$ . Assumption 1 is $R\Delta\mu>c$ .

The derived constants are

\beta=\frac{b}{\Delta\mu},\qquad \bar w=\frac{\beta\mu}{\rho},\qquad \underline v=\frac{\underline\mu R}{r},\qquad \bar V=\frac{R\mu-c-(\rho-r)\bar w}{r},\qquad \bar K_2=\bar V-\underline v-\bar w .

The variable $w\ge0$ is the agent's promised utility. The revenue threshold is

\hat R=\Big[\frac cb+\frac{(\rho-r)\mu}{\Delta\mu(\rho-r-\mu)}\cdot\frac{\rho-\mu}{\rho}\Big]\beta .

Condition 2 is: $\mu<\rho-r$ and $R\ge\hat R$ .

For a function $f$ on $\mathbb R_+$ with left derivative $f'$ , the working-state operator and the suspension-state operator are

(\mathcal A_I f)(w)=(\mu+r)f(w)-\mu f(w+\beta)+\rho(\bar w-w)f'(w)-(\mu R-c)+(\rho-r)w,

(\mathcal A_\emptyset f)(w)=rf(w)-\rho wf'(w)+(\rho-r)w-R\underline\mu .

The first is a delay-differential operator: it evaluates $f$ at $w+\beta$ . A pair $(V_I,V_\emptyset)$ satisfies the optimality condition (20)–(22) if

(\mathcal A_IV_I)(w)\ge0,\quad(\mathcal A_\emptyset V_\emptyset)(w)\ge0,\qquad 0\le V_I(w)-V_\emptyset(w)\le K,\qquad V_I(0)\ge\underline v,\ V_\emptyset(0)\ge\underline v .

Formalization targets

Goal: Proposition 4

Under Condition 2, let $V_I$ be the line from $\underline v$ at $w=0$ to $\bar V$ at $w=\bar w$ , and let $V_I$ be constant $\bar V$ beyond $\bar w$ (display (31)). Then

K>\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset\equiv\underline v)\ \text{satisfies (20)–(22)},

\bar K_2<K\le\bar V-\underline v\ \Longrightarrow\ (V_I,\ V_\emptyset)\ \text{satisfies (20)–(22)},

where in the second case $V_\emptyset$ is the line from $\underline v$ to $\bar V-K$ on $[0,\bar w]$ , constant $\bar V-K$ beyond (display (32)).

Milestones

Lemma EC.2(vi), second claim: if $\rho>r+\mu$ , then $\bar V-\frac{\rho-r}{\rho-r-\mu}\bar w\ge\underline v$ if and only if $R\ge\hat R$ .
Proposition 4, first part: the case $K>\bar V-\underline v$ .
Proposition 4, second part: the case $\bar K_2<K\le\bar V-\underline v$ .

Significance

Through the paper's verification theorem, Proposition 4 yields the "not hiring" half of the main Theorem 2 in the Condition 2 regime. If $K\ge\bar K_2$ , the principal's value is at most $\underline v$ , so it is optimal never to engage the agent (Theorem 3). The threshold $\bar K_2=\bar V-\underline v-\bar w$ is the switching cost above which the value of hiring, net of the set-up cost and of the agent's promised rent, falls below the outside value. Together with the companion missions of this series (Condition 1 with high cost, Condition 2 with medium cost, and the low-cost control-band regime), this result completes the partition of the parameter space behind Theorem 2.

The result is proved in the paper and has no machine-checked proof yet. This mission states the analytic certificate of the guess-and-verify argument, not the contract-optimality theorem. The contribution it asks for is a formal proof that these explicit functions satisfy the quasi-variational inequalities, including the left-derivative behaviour at the kink $w=\bar w$ and the algebra that links Condition 2 to the sign of $\mathcal A_IV_I$ .

Difficulty

The functions are piecewise linear, so the difficulty is not analytic depth but bookkeeping that is easy to get wrong:

The operator $\mathcal A_I$ is non-local. It evaluates $V_I$ at $w+\beta$ , and which branch of (31) applies there depends on how $\bar w$ compares with $\beta$ , which Condition 2 settles.
At the kink $w=\bar w$ the functions are not differentiable, so the left-derivative convention must be used explicitly.
The sign of $\mathcal A_IV_I$ on $[0,\bar w]$ reduces to an inequality between $\bar V$ , $\underline v$ and $\bar w$ , and showing that this inequality is the revenue condition $R\ge\hat R$ requires unfolding (8)–(10) and (28).

The naive check, that $\mathcal A_IV_I$ vanishes or is positive because $V_I$ is "close to" a solution of the delay equation, does not work: $V_I$ is not a solution of (25), and the inequality is strict in general.

Formalization scope

All parameters are real numbers in one structure Params. Its predicate Standing collects the paper's standing assumptions: $0\le\underline\mu<\mu$ , $0<b\le c$ , $K>0$ , $0<r\le\rho$ and $R\Delta\mu>c$ . Two of these are added to the page and disclosed: $\underline\mu\ge0$ , since it is an arrival rate, and $b>0$ , since (31)–(32) divide by $\bar w=\beta\mu/\rho$ .

Functions are ℝ → ℝ, and every condition is quantified over $w\ge0$ only. The derivative in $\mathcal A_I$ and $\mathcal A_\emptyset$ is the left derivative derivWithin f (Set.Iic w) w, as the paper prescribes on p. 15. Inequality (20) is required for $w>0$ : on $\mathbb R_+$ the left derivative at $0$ does not exist. Inequalities (21) and (22) are required exactly as printed. "Satisfy the optimality condition (20)–(22)" means exactly these three conditions; the paper's Theorem 1 additionally asks for monotonicity and concavity, but Proposition 4 does not claim them and they are not added.

The threshold $\hat R$ is the printed formula. Its denominator $\rho-r-\mu$ is positive under Condition 2, so Lean's convention $x/0=0$ never applies there.

None of the conditions is weakened: (21) keeps both bounds, (22) is kept, and the operators are not pre-simplified with the closed form of $\bar V$ . A formal proof therefore has to carry out the sign computation itself. The stochastic contract model (Poisson point processes, promise keeping, incentive compatibility), the verification Theorem 1 and the optimality Theorems 2–3 are not formalized.

Two hat symbols elsewhere in the paper are distinct objects from those used here: $\hat{\mathrm w}$ of Lemma 3 and the bold $\hat{\mathbf w}$ of Proposition 6. Neither appears in this mission. Proofs of the milestones, and proofs of the goal that use them, are welcome.

Selected references

P. Cao, P. Sun, F. Tian, Punish Underperformance with Suspension: Optimal Dynamic Contracts in the Presence of Switching Cost, Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4845
P. Sun, F. Tian, Optimal Contract to Induce Continued Effort, Management Science 64(9), 4193–4217, 2018. https://doi.org/10.1287/mnsc.2017.2795

5 thms3 active usersReviewed

Completed

Operations Research Optimization Probability+1·Captain: mikedeng1

Pricing in On-Demand and One-Way Vehicle-Sharing Networks 1: Static Prices Earn at Least K/(N+K−1+Λ/μ) of the Fluid Optimum, via Increasingly Tight Availability BoundsResearch Paper

Why static prices in vehicle sharing

In one-way car sharing, bike sharing and ride hailing, a vehicle that serves a trip from location $i$ to location $j$ ends up at $j$ . Prices therefore do two jobs: they collect revenue and they steer the fleet. The best dynamic (state-dependent) pricing policy reacts to where every vehicle is, but computing it is a Markov decision problem over a state space that grows combinatorially with the fleet. A static policy, one fixed price per origin–destination pair, is easy to compute and to post, and the question is how much it gives up.

Waserhole and Jost (2016) bounded the loss when travel times are negligible. Banerjee, Freund and Lykouris (arXiv:1803.07841, Operations Research 2022) gave guarantees for large fleets. Benjaafar and Shen (SSRN 3998297; Operations Research Technical Note, 2023, doi:10.1287/opre.2023.2446) prove a bound valid for every fleet size $K$ that accounts for travel times, and then a sequence of progressively tighter bounds. This mission formalizes that chain.

Setting

There is a finite set $\mathcal N$ of $N$ locations and $K\ge 1$ vehicles. Trip requests from $i$ to $j$ arrive at rate $\Lambda_{ij}\ge 0$ ; the pairs with positive demand form $\mathcal A=\{(i,j):\Lambda_{ij}>0\}$ , and the network $(\mathcal N,\mathcal A)$ is strongly connected. A trip from $i$ to $j$ lasts on average $1/\mu_{ij}$ . A quantile policy $q=(q_{ij})$ , $q_{ij}\in[0,1]$ , is the fraction of requests that accept the posted price; the effective rates are $\lambda_{ij}=q_{ij}\Lambda_{ij}$ and $\lambda_i=\sum_j\lambda_{ij}$ . Each served trip earns $I_{ij}(q_{ij})$ , and $q\mapsto qI_{ij}(q)$ is concave.

The fluid problem (2) is

\max_q\ R_s(q)=\sum_{(i,j)\in\mathcal A}\Lambda_{ij}q_{ij}I_{ij}(q_{ij})\quad\text{s.t.}\quad\sum_j\Lambda_{ij}q_{ij}=\sum_j\Lambda_{ji}q_{ji}\ \forall i,\quad \sum_{(i,j)\in\mathcal A}\frac{\Lambda_{ij}q_{ij}}{\mu_{ij}}\le\Delta,\quad q_{ij}\in[0,1],

with $\Delta\ge K$ . Its optimal solution $q^s$ is the static policy; it is assumed to induce a strongly connected network. The value $R_s(q^s)$ is the fluid optimum.

Under a static policy the fleet moves through a closed queueing network: a single-server pick-up queue at each location, served at rate $\lambda_i$ , and an infinite-server transit queue for each pair, with mean time $1/\mu_{ij}$ . The paper invokes the BCMP theorem for this network; the mission writes its stationary law as the product form. With $r$ a positive solution of the traffic equations (9), $r_i=\sum_j r_j\lambda_{ji}/\lambda_j$ , a state $x$ (vehicle counts at locations and in transit, total $K$ ) has weight

w(x)=\prod_i\Bigl(\frac{r_i}{\lambda_i}\Bigr)^{x_i}\prod_{(i,j)}\frac{1}{x_{ij}!}\Bigl(\frac{r_i\lambda_{ij}}{\lambda_i\mu_{ij}}\Bigr)^{x_{ij}}.

The availability $\alpha_i(K)$ is the weight share of the states with $x_i\ge 1$ : the probability that a customer at $i$ finds a vehicle. The reward rate of the static policy is (3):

R(q^s)=\sum_{(i,j)\in\mathcal A}\alpha_i\,\Lambda_{ij}q^s_{ij}I_{ij}(q^s_{ij}).

Finally $\Lambda=\sum_{\mathcal A}\Lambda_{ij}$ , $1/\mu=\sum_{\mathcal A}\Lambda_{ij}/(\Lambda\mu_{ij})$ , and $\lambda/\mu=\sum_{\mathcal A}\Lambda_{ij}q^s_{ij}/\mu_{ij}$ .

Formalization targets

Goal: Theorem 2, static half (p. 9)

With $B^j_0(q^s)=B^j_0=0$ and, for $1\le i\le K$ ,

B^K_i(q^s)=\frac{K}{N+K-1+\frac{\lambda}{\mu}\bigl(1-B^{K-1}_{i-1}(q^s)\bigr)},\qquad B^K_i=\frac{K}{N+K-1+\frac{\Lambda}{\mu}\bigl(1-B^{K-1}_{i-1}\bigr)},

the goal is: for every $i=1,\dots,K$ ,

\frac{R(q^s)}{R_s(q^s)}\ \ge\ B^K_i(q^s)\ \ge\ B^K_i\ \ge\ \frac{K}{N+K-1+\Lambda/\mu},

and $B^K_{i+1}>B^K_i$ for $i=1,\dots,K-1$ .

The paper's Theorem 2 begins with one more inequality, $R(q^s)/R(q^*)\ge R(q^s)/R_s(q^s)$ , where $q^*$ is the best state-dependent policy. That inequality is Proposition 1 (p. 6). Its proof needs the stationary behaviour of the network under an arbitrary state-dependent policy with matrix-exponential trip times, together with Jensen's inequality and Little's law; that model is not formalized here. Proposition 1 is not part of this mission. The goal is the remaining chain, and it implies the paper's theorem once Proposition 1 is available.

Milestones

Equal availability under balanced flows (p. 7, Appendix p. 23): $\alpha_i(K)=\alpha_j(K)$ .
The ratio equals the availability (pp. 7–8): $R(q^s)/R_s(q^s)=\alpha$ .
Equation (5) (p. 8): $\alpha(K)=K/\bigl(K+N-1+\frac{\lambda}{\mu}(1-\alpha(K-1))\bigr)$ .
Theorem 1, static half (p. 7): $R(q^s)/R_s(q^s)\ge K/(K+N-1+\Lambda/\mu)$ .
Equation (6) and $0\le\alpha(K-i)\le(K-i)/(N+K-i-1)$ (p. 9).
$B^K_K(q^s)=\alpha(K)$ (p. 10).
$B^K_{i+1}(q^s)>B^K_i(q^s)$ (p. 10).

Significance

The bound $K/(N+K-1+\Lambda/\mu)$ holds for every fleet size, tends to $1$ at rate $O(1/K)$ , and reduces to the Waserhole–Jost bound when travel times vanish. The sequence $B^K_i(q^s)$ gives a computable certificate between that bound and the exact ratio $B^K_K(q^s)=\alpha(K)$ , which an operator can evaluate from $N$ , $K$ and the fluid solution alone. Equation (5), a one-step recursion in the fleet size for a network mixing single-server and infinite-server stations, is the reusable core: the two sibling missions (the demand-free bound of Theorem 3 and the split-network bound of Theorem 4) rest on the same recursion.

The results are proved in the paper; none is formalized elsewhere as far as a search of the platform shows. The platform has the multiclass BCMP framework and single-server closed Jackson networks, but not availability in networks with infinite-server stations, nor equation (5). This mission adds a product-form availability layer, the equal-availability lemma, the recursion (5), and the bound chain.

Difficulty

The paper derives (5) from the random observer (arrival) theorem and Little's law, and neither is available as a formal tool, so the recursion has to be obtained from the product form itself, as an identity between sums over the state spaces with $K$ and $K-1$ vehicles. Equal availability needs uniqueness, up to scale, of the positive solution of the traffic equations on a strongly connected network (a Perron–Frobenius-type fact for an irreducible stochastic matrix). In the bound chain, $B^K_i(q^s)\ge B^K_i$ needs the recursion map to be monotone in both the workload and the previous value, which holds only once $0\le B\le 1$ is established; strict monotonicity in $i$ is a double induction.

The obvious shortcut, defining $\alpha$ by the recursion (5), makes Theorem 1 a one-line consequence of $\alpha(K-1)\ge 0$ and deletes the content of the first three milestones; the mission rules it out by defining $\alpha$ as the product form.

Formalization scope

Locations form a Fintype with Nonempty; $N$ is its cardinality. Demand, travel rates, rewards and policies are functions on all ordered pairs, self-pairs included; sums over $\mathcal A$ are sums over all pairs, which agree because each summand carries $\Lambda_{ij}$ . Strong connectivity, of $(\mathcal N,\mathcal A)$ and of the network induced by $q^s$ , uses nonempty paths (Relation.TransGen), so every location has positive accepted demand and $\mathcal A\ne\emptyset$ . Every ordered pair has a transit queue; a pair with $\lambda_{ij}=0$ has load $0$ and stays empty ( $0^0=1$ ). All arithmetic on $K$ , $N$ and $i$ is in $\mathbb R$ ; $B(K,0)=0$ for every $K\ge 0$ , including the $B^0_0$ that the paper's definition omits. $R_s(q^s)>0$ is a hypothesis of the ratio statements, since otherwise the ratio is $0/0$ . The statements keep the paper's hypothesis that $q^s$ is optimal for (2) with $\Delta\ge K$ ; the proofs use only feasibility and balanced flows, and the queueing milestones are stated for every balanced quantile policy inducing a strongly connected network.

The product form is a definition: the mission does not prove that it is the stationary law of the network's Markov chain (the BCMP theorem). The general closed product-form network (single-server and infinite-server stations on an arbitrary finite station set) is a separate definition and is reusable beyond this mission. Contributions welcome: proofs of (5) via normalizing constants, the traffic-equation uniqueness lemma, and the elementary bound-sequence inequalities.

Selected references

S. Benjaafar, X. Shen, Pricing in On-Demand (and One-Way) Vehicle Sharing Networks, SSRN abstract 3998297, version of 2023-01-10. https://ssrn.com/abstract=3998297 ; Technical Note, Operations Research, 2023. https://doi.org/10.1287/opre.2023.2446
F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, Closed, and Mixed Networks of Queues with Different Classes of Customers, J. ACM 22(2), 1975. https://doi.org/10.1145/321879.321887
S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research 70(3), 2022. https://arxiv.org/abs/1803.07841
A. Waserhole, V. Jost, Pricing in Vehicle Sharing Systems: Optimization in Queuing Networks with Product Forms, EURO J. Transportation and Logistics 5, 2016. https://doi.org/10.1007/s13676-014-0054-4
D. K. George, C. H. Xia, Fleet-Sizing and Service Availability for a Vehicle Rental System via Closed Queueing Networks, European J. Operational Research 211(1), 2011. https://doi.org/10.1016/j.ejor.2010.12.015
M. Reiser, S. S. Lavenberg, Mean-Value Analysis of Closed Multichain Queuing Networks, J. ACM 27(2), 1980. https://doi.org/10.1145/322186.322195

12 thms3 active usersReviewed

Completed

Linear algebra Quantum Information·Captain: mikedeng1

Improvements in Quantum SDP-Solving with Applications 1: A Unitary Preparing a Purification of a Subnormalized Density Operator ϱ Gives an Exact (1, w+a+1, 0)-Block-Encoding of ϱResearch Paper

Motivation

Quantum algorithms for semidefinite programming need a way to use an input matrix inside a quantum circuit. In the quantum state input model, an oracle prepares a purification of a density operator. In the quantum operator input model, a unitary instead exposes that operator as a block of a larger unitary. The two kinds of access serve different subroutines. Lemma 12 of van Apeldoorn and Gilyén’s 2018 preprint connects them for a subnormalized density operator. The same paper uses this connection when comparing its input models for quantum SDP solving.

The result concerns a precise finite-dimensional construction. It matters even without the paper’s query-complexity estimates: it specifies which registers must be present, what happens to probability mass outside the accepted flag state, and which block of the resulting unitary equals the desired operator. These details are easy to lose when a statement is shortened to “purification gives a block-encoding.”

Setting

A w-qubit register has basis labels in $\{0,1\}^{w}$ . A subnormalized density operator $\varrho$ on that register is a positive semidefinite complex matrix with $\operatorname{Tr}\varrho\leq1$ . Its trace may be strictly below one. A purification is a unit vector $|\varphi\rangle$ on three registers: the w-qubit system, one flag qubit, and a c-qubit junk register. The operator $\varrho$ is the flag-zero block after tracing out the junk. In entries,

\varrho_{ij}=\sum_{t\in\{0,1\}^{c}}\varphi_{i,0,t}\,\overline{\varphi_{j,0,t}}.

Thus probability in the flag-one branch does not contribute to $\varrho$ . Let $a=c+1$ , so a unitary $G$ preparing $|\varphi\rangle$ acts on $w+a$ qubits and $|\varphi\rangle=G|0\rangle^{\otimes(w+a)}$ . The result adds an initial w-qubit system and one extra qubit. Its register swap $S$ exchanges the initial $(\text{system},\text{extra})$ register with the $(\text{prepared system},\text{flag})$ register and leaves the c junk qubits fixed. The construction is

V=(I_{2^{w+1}}\otimes G^{\dagger})S(I_{2^{w+1}}\otimes G).

A $(\alpha,k,\varepsilon)$ block-encoding of an operator $A$ is a unitary on the system and k ancilla qubits whose all-zero ancilla block differs from $A/\alpha$ in operator norm by at most $\varepsilon/\alpha$ . Here the scale is one and the error is zero. The block of $V$ is taken at the all-zero state of the extra qubit and the entire register of $G$ .

Formalization targets

The goal is Lemma 12 with the ancilla count given by its displayed construction:

\left\|\varrho-(I_{2^w}\otimes\langle0|^{\otimes(w+a+1)})V (I_{2^w}\otimes|0\rangle^{\otimes(w+a+1)})\right\|=0.

The target includes that $V$ is unitary, making it an exact $(1,w+a+1,0)$ block-encoding of $\varrho$ . The theorem identifies $V$ explicitly, so its use of one $G$ and one $G^{\dagger}$ is part of the construction. The source’s Lemma 12 prints $(1,w+a,0)$ , while its proof says $V$ has $2w+a+1$ qubits and takes the block at $1+w+a$ ancillas. This mission uses the proof’s consistent count and labels the correction. The four milestones follow the proof’s stated steps: unitarity of $V$ , identification of its zero block, elimination of the flag-one component, and equality of the remaining SWAP sandwich with $\varrho$ .

Significance

The exact identity shows that a state-preparation unitary can be used where the paper’s quantum operator model expects a block-encoding. It also covers genuinely subnormalized operators, for which a normalized-state argument is insufficient: a preparation may have nonzero amplitude in the flag-one branch even though only the flag-zero branch defines $\varrho$ . The explicit ancilla count prevents such lost probability mass from being silently included in the output block.

Formalizing this known result gives a reusable interface between a purification predicate and a block-encoding predicate. The mission statement is open on Prove2Me; the paper’s mathematical argument is known. A related open block-encoding statement in Nannicini’s treatment concerns a normalized density matrix and a circuit-level construction with a different ancilla arrangement. It does not state this paper’s subnormalized, flag-qubit identity. The finite-register definitions and SWAP identities can be reused by later matrix-level quantum algorithms, whether or not the paper’s larger complexity bounds are formalized.

Difficulty

The first apparent shortcut is to use the ordinary purification identity without the flag qubit. That recovers the trace over both flag outcomes, which can have trace one even when $\operatorname{Tr}\varrho<1$ . The required block must select flag zero. A second source of error is register order: the paper displays the system first, while the existing Lean block-encoding predicate places the ancilla register first. Equality of matrix blocks depends on the explicit reindexing. Complex conjugation also matters: swapping the vector and covector amplitudes would produce a transpose of $\varrho$ instead of $\varrho$ for complex states.

Formalization scope

The Lean system register is QAlgorithms.Qubits w; the flag and extra register are each Bool; and the junk is QAlgorithms.Qubits c. The identity $a=c+1$ makes the flag register present even at $c=0$ . The all-zero state is the all-false basis label. Matrices are over $\mathbb C$ , tensor products are matrix Kronecker products, and $S$ is a permutation matrix fixing the junk. The paper’s printed identity factor beside the swap has size $2^a$ ; the consistent factor is $2^{a-1}=2^c$ , since the swap already acts on two $w+1$ -qubit registers.

The referenced QAlgorithms.IsBlockEncoding definition includes unitarity and measures error with the operator norm. Lean reindexes $V$ to put its $(\text{extra},\text{prepared system},\text{flag},\text{junk})$ ancilla first. The theorem requires $G$ unitary, $\varrho$ subnormalized, and the exact purification relation between $G|0\rangle$ and $\varrho$ . The purification relation prevents a vacuous claim about an unrelated matrix. The optional quantum gate-count clause of the printed lemma is outside this matrix-level formalization; the register swap is explicitly the swap of $w+1$ qubit pairs. A circuit-level gate-count theorem would require an additional gate-list representation.

The needed reusable components are finite complex matrices, unitary permutation matrices, Kronecker products, partial traces, and the operator norm. Contributions can address the four milestone identities, the main theorem, or a circuit-level refinement of the gate count. None of the statements introduces the proof’s Schmidt decomposition as an assumption.

Selected references

J. van Apeldoorn and A. Gilyén, Improvements in Quantum SDP-Solving with Applications, arXiv preprint, 2018, arXiv:1804.05058v1, Definition 1 (p. 3), Definition 2 (p. 4), Lemma 12 and proof (pp. 15–16).
G. Nannicini, Quantum Algorithms for Optimizers, arXiv preprint, 2024, arXiv:2408.07086, Definition 7.11 and the normalized density-matrix construction.

8 thms3 active usersReviewed

Completed

Dynamical Systems Economics Operations Research+1·Captain: mikedeng1

Minimum Earnings Regulation and the Stability of Marketplaces I: The Marketplace Is Stable Exactly When M ≤ w* Under Tight Labor Supply (p* ≤ w) and M ≤ H(R(p)) Under Loose SupplyResearch Paper

Motivation

Minimum hourly earnings rules for ride-hailing drivers are meant to protect income during periods when drivers spend part of their time idle. A platform pays a wage per hour carrying riders, yet drivers care about earnings per hour logged onto the platform. When many drivers enter after a wage increase, utilization can fall and offset the increase. A regulation that uses the preceding period's utilization to set the next wage can therefore create feedback in the marketplace. Asadpour, Lobel, and van Ryzin model this feedback and identify the exact minimum earnings targets compatible with bounded wages and continuing service (Asadpour, Lobel, and van Ryzin, 2022, §§3–4).

The question matters to marketplace design because a target that cannot be sustained within the model cannot be reached through a bounded wage policy, even if the platform changes prices over time. The theorem separates two economic regimes. When labor supply is tight, the decisive number is the price where demand equals supply. When supply is loose, the decisive number is the greatest revenue the platform can obtain from riders, converted into affordable driver earnings. This mission concerns the paper's threshold theorem and the four lemmas that state its main analytic ingredients.

Setting

In each discrete period $t$ , a platform chooses a rider price $p_t\ge0$ and a wage per ride hour $w_t\ge0$ . At price $p$ , riders demand $D(p)$ hours of trips. At expected hourly earnings $z$ , drivers supply $S(z)$ hours. The quantity of completed rides and driver utilization are

Q(p,z)=\min\{D(p),S(z)\},\qquad u(p,z)=\frac{Q(p,z)}{S(z)}.

Drivers earn wages only while carrying riders. Thus an earnings equilibrium is a positive sequence $z_t$ satisfying $z_t=w_tu(p_t,z_t)$ in every period. The platform's period profit is $\pi(p,w,z)=(p-w)Q(p,z)$ . A minimum earnings target $M>0$ requires

w_{t+1}\ge\frac{M}{u(p_t,z_t)}.

The rule uses utilization in one period to set a wage floor in the next. A policy is stable if its prices and wages are feasible, it satisfies equilibrium and the wage rule, wages have a finite upper bound across all periods, and profit is nonnegative in all but finitely many periods. This definition permits a finite transition with losses but excludes a wage sequence that grows without bound (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Definitions 1–2 and (5)).

The revenue function is $R(p)=pD(p)$ , and the labor cost function is $C(z)=zS(z)$ . Write $H$ for the inverse of $C$ on positive expenditure. The paper assumes that $D$ is positive, continuous, and strictly decreasing; $S$ is strictly increasing, differentiable, and positive except possibly at zero; $R$ has a unique peak at $p^*$ ; and demand and supply cross at $w^*$ , so $D(w^*)=S(w^*)$ (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Regularity assumptions).

Each theorem in this mission retains these standing assumptions, including when a particular result uses only some of them.

Formalization targets

Exact stability threshold

The goal is Theorem 1 of the paper. For every $M>0$ , stability is characterized by

\operatorname{Stable}(D,S,M)\quad\Longleftrightarrow\quad M\le z^*,\qquad z^*=\begin{cases}w^*,&p^*\le w^*,\\H(R(p^*)),&p^*>w^*.\end{cases}

The equality case $p^*=w^*$ belongs to the first branch. The theorem gives an if and only if statement about all feasible sequences of prices and wages, rather than a condition for one chosen stationary policy (Asadpour, Lobel, and van Ryzin, 2022, p. 11, Theorem 1 and (7)).

Supporting results

The milestones reproduce Lemmas 1–4 and two claims in the Online Appendix. Lemma 1 establishes the inverse labor cost's existence, regularity, and monotonicity. Lemma 2 identifies continuous, unique equilibrium earnings for a given price and positive wage. Lemma 3 states that stability admits a policy with price equal to wage. Lemma 4 rewrites the wage rule in that regime. The appendix claims compare the loose-supply threshold with $w^*$ and show that the tight-supply wage-growth factor exceeds one above $w^*$ (Asadpour, Lobel, and van Ryzin, 2022, pp. 9–10 and Online Appendix p. 4).

Significance

The theorem identifies the full stable range of targets in this model. In the tight-supply case, raising the target above the demand–supply crossing cannot be stabilized by choosing a different sequence of prices. In the loose-supply case, the highest stable target is tied to the cost of supplying drivers at the platform's peak potential revenue. The distinction explains why the same regulation can have different limits across markets with different demand and supply curves (Asadpour, Lobel, and van Ryzin, 2022, p. 11 and Figure 2).

The paper proves this result mathematically. The remaining formalization task is to represent its sequence model and analytic assumptions in Lean and prove the threshold statement and its supporting lemmas there. Its inverse-cost, equilibrium, and policy-stability interfaces can also be reused for the companion results on utilization shocks and static stability in the same paper. Those companion theorems are separate missions in this series.

Difficulty

The short threshold formula hides two distinct obligations: a policy must satisfy the earnings equilibrium and lagged wage rule at every period, while the impossibility direction must exclude every stable feasible policy, including policies that vary prices over time. The equilibrium earnings formula changes regime when supply at the posted wage crosses demand. At the boundary the two formulas must agree, and the argument must still handle wages that approach or cross the demand–supply point. Boundedness and profit conditions also interact with a finite initial period in which profit may be negative.

The paper's printed explanation for one strict inequality in the tight-supply converse is insufficient: two decreasing factors do not determine the direction of their product. The formal target keeps the inequality the paper uses, while the appendix quotation remains as printed (Asadpour, Lobel, and van Ryzin, 2022, Online Appendix p. 4).

Formalization scope

Prices, wages, earnings, demand, supply, cost, and revenue are real valued. The curves' regularity is imposed on $[0,\infty)$ ; differentiability of supply is imposed on $(0,\infty)$ together with continuity at zero. Revenue is strictly increasing up to $p^*$ and strictly decreasing afterward, encoding the unique peak. The crossing $w^*$ and inverse $H$ are parameters with their characterizing properties, so the statements hold for their uniquely determined values. The inverse is only used at positive costs.

Lean indexes the first period by $0$ , so its rule applies to $w_{t+1}$ for every $t\ge0$ and places no floor on $w_0$ . The paper starts at period $1$ and likewise leaves the first wage free. “Bounded wages” means a single real upper bound for every period; “all but finitely many periods” is represented by an eventually true condition on $\mathbb N$ .

An equilibrium requires $z_t>0$ . This explicit domain condition prevents a zero-supply input from making $u=0/0$ and then $M/u=0$ under Lean's total real division, which would make the regulation vacuous. Lemma 2 correspondingly uses $w>0$ . Its branch condition $S(w)<D(p)$ agrees with the paper's $w<S^{-1}(D(p))$ wherever that inverse exists and remains meaningful when demand is outside the range of supply. These domain choices are stated with the items they affect. A complete development needs real-analysis facts about continuous strictly monotone functions and inverses, eventual properties of sequences, and elementary bounds on the utilization ratio. Contributions establishing these interfaces or the stated milestones are within scope.

Selected references

Arash Asadpour, Ilan Lobel, and Garrett van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN preprint 3502607, version of August 24, 2022; published in Manufacturing & Service Operations Management, 2022. SSRN preprint. The local formalization uses the dated preprint's page and theorem numbering.

8 thms3 active usersReviewed

Completed

Theoretical Computer Science·Captain: Chutong

CLRS — Chapter 20, §20.5: Strongly Connected Components (Kosaraju) — Correctness and Running TimeTextbook

The mutual-reachability partition

Two vertices belong to the same strongly connected component when each can reach the other by a directed path. The partition separates the mutually reachable parts of a directed graph without requiring the whole graph to be connected. This mission formalizes the two-pass DFS algorithm of CLRS, fourth edition, Chapter 20, §20.5, often called Kosaraju's algorithm. The fourth-edition contents place this material after DFS in §20.3.

Graph and returned component labels

The input graph has $n$ vertices numbered from zero and $m$ adjacency occurrences. Its representation is an array of integer adjacency arrays plus a degree sequence. Parallel arcs and self-loops are allowed; duplicate occurrences contribute separately to $m$ . Empty and disconnected graphs are included. Symmetric entries can represent an undirected graph, but no symmetry is assumed.

The source scc calls the shared dfs entry, constructs the transpose by reversing every adjacency occurrence, and calls the same dfs_ordered entry on that transpose. The first pass produces increasing finish order. A linear pass reverses the order prefix for the second traversal; no comparison sort is performed. The returned object is the second traversal's DFSResult.

Its component array contains integer labels, and components contains their count $k$ . Labels are contiguous identifiers $0,\ldots,k-1$ , each used by at least one vertex. They are not canonical vertex representatives and need not be stable under adjacency reordering. Only the component fields are specified by the SCC postcondition; the remaining result fields describe the second DFS pass on the transpose.

Formalization targets

The headline CLRS.SCC.scc_correctness_and_running_time requires a single terminating scc.Call whose result labels exactly the initial graph's mutual-reachability classes. For every valid pair $u,v$ ,

\operatorname{component}[u]=\operatorname{component}[v] \iff (u\leadsto v)\land(v\leadsto u).

The component count must satisfy

0\le k\le n,\qquad k=0\iff n=0,

and every label below $k$ must occur. The component array and result object are fresh, and the complete call preserves all previously allocated caller storage. Its named-event cost obeys one uniform bound:

\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).

A supporting SCC milestone requests the explicit bound

T\le20+21n+6m

for the same call and complete postcondition. This includes both DFS traversals, input-order construction, transpose construction, finish-order reversal, and fixed setup work.

The other supporting milestone, transpose_correctness_and_running_time, requests a fresh graph with exactly reversed adjacency occurrences, unchanged vertex and occurrence counts, caller-storage preservation, and a uniform linear event bound. Reversal retains multiplicity, not just the existence of edges. These are open goals; no mathematical or execution proof is supplied.

Composing a verified traversal

The desired result gives later callers an exact test for component membership by comparing labels. Its count and coverage clauses make the labels usable for a compact representation of the partition. An algorithm using the partition need not repeat the analysis of recursive exploration or inspect compiler transitions.

The separate DFS mission supplies CLRS.DFS.ordered_correctness_and_explicit_running_time as an open dependency, with the full forest and storage contract and the numerical budget $4+6n+2m$ for any valid supplied root permutation. Its identity-order companion, CLRS.DFS.correctness_and_explicit_running_time, requests $7+8n+2m$ for the first pass. These explicit budgets can be combined with transpose construction and finish-order reversal to establish this mission's complete event bound. This mission imports the same definitions and requests the new component theorem; it does not duplicate the DFS program. The main statement contains no hypothesis asserting that DFS or SCC is already correct. The mathematical two-pass algorithm and its linear bound are textbook results; formal verification of these particular generated calls is the contributor task. See CLRS, fourth edition, §§20.3 and 20.5.

What must be justified

A DFS tree in an arbitrary directed graph is not necessarily a strongly connected component. The second traversal's particular order and reversed edges are essential to the requested equivalence. Both directions matter: vertices assigned the same label must be mutually reachable, and mutually reachable vertices must not receive different labels. The cost obligation cannot omit the transpose or order-processing loops, and repeated arcs must be counted rather than treated as free duplicates.

Formalization scope

Reachability is defined by finite paths in the original graph, including zero-edge paths at valid vertices. Transposition preserves each edge occurrence. Every transpose row, including an empty row, is separately allocated before any edges are appended, so the program does not accidentally share mutable row storage. Caller input rows may alias because they remain read-only.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. The reproduction manifest records raw generation and platform import-path adaptations separately. Stable generated definitions supply the public Call relations.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete entry is scc.algo; its dependencies are dfs.algo and graph_input.algo. The DFS source is shown unchanged to make the imports and counted work explicit. Supporting theorem references reuse the DFS mission's definitions and open contract.

`graph_input.algo`

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

`dfs.algo`

# CLRS fourth edition, Section 20.3: depth-first search.
# dfs_ordered takes a permutation of the vertices as its outer-loop order.
# Result.order lists vertices in increasing finish time; reverse its valid
# prefix before using it as the second-pass order in the SCC algorithm.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph


class DFSResult:
    color: Seq
    parent: Seq
    discover: Seq
    finish: Seq
    order: Seq
    component: Seq
    clock: Int
    finished: Int
    components: Int

    def __init__(self) -> None:
        tick("graph_work")
        self.color = const(0)
        self.parent = const(-1)
        self.discover = const(0)
        self.finish = const(0)
        self.order = const(-1)
        self.component = const(-1)
        self.clock = 0
        self.finished = 0
        self.components = 0


def visit(graph: UnweightedGraph, result: DFSResult, u: Int, label: Int) -> None:
    tick("graph_work")
    result.clock += 1
    result.discover[u] = result.clock
    result.color[u] = 1
    result.component[u] = label
    neighbors: Seq = graph.adj[u]
    j: Int = 0
    tick("graph_work")
    # @scan_neighbors
    while j < graph.degree[u]:
        tick("graph_work")
        v: Int = neighbors[j]
        if result.color[v] == 0:
            tick("graph_work")
            result.parent[v] = u
            visit(graph, result, v, label)
        j += 1
        tick("graph_work")
    tick("graph_work")
    result.color[u] = 2
    result.clock += 1
    result.finish[u] = result.clock
    result.order[result.finished] = u
    result.finished += 1


def dfs_ordered(graph: UnweightedGraph, order: Seq) -> DFSResult:
    tick("graph_work")
    result: DFSResult = DFSResult()
    i: Int = 0
    tick("graph_work")
    # @scan_roots
    while i < graph.size:
        tick("graph_work")
        u: Int = order[i]
        if result.color[u] == 0:
            tick("graph_work")
            visit(graph, result, u, result.components)
            result.components += 1
        i += 1
        tick("graph_work")
    tick("graph_work")
    return result


def dfs(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    order: Seq = const(0)
    i: Int = 0
    tick("graph_work")
    # @identity_order
    while i < graph.size:
        tick("graph_work")
        order[i] = i
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(graph, order)

`scc.algo`

# CLRS fourth edition, Section 20.5: strongly connected components.
# The first DFS records increasing finish order. The second DFS visits the
# transpose in decreasing first-pass finish order. Its forest labels are SCCs.
# Adjacency rows in the transpose are separately allocated, including empty rows.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph
from dfs import DFSResult, dfs, dfs_ordered


def transpose(graph: UnweightedGraph) -> UnweightedGraph:
    tick("graph_work")
    adj: Seq[Seq] = const(const(0))
    degree: Seq = const(0)
    u: Int = 0
    tick("graph_work")
    # @allocate_rows
    while u < graph.size:
        tick("graph_work")
        adj[u] = const(0)
        u += 1
        tick("graph_work")

    u = 0
    tick("graph_work")
    # @scan_sources
    while u < graph.size:
        tick("graph_work")
        neighbors: Seq = graph.adj[u]
        j: Int = 0
        tick("graph_work")
        # @reverse_edges
        while j < graph.degree[u]:
            tick("graph_work")
            v: Int = neighbors[j]
            adj[v][degree[v]] = u
            degree[v] = degree[v] + 1
            j += 1
            tick("graph_work")
        u += 1
        tick("graph_work")

    tick("graph_work")
    return UnweightedGraph(graph.size, adj, degree)


def scc(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    first: DFSResult = dfs(graph)
    tick("graph_work")
    reversed_graph: UnweightedGraph = transpose(graph)
    tick("graph_work")
    order: Seq = const(-1)
    i: Int = 0
    tick("graph_work")
    # @decreasing_finish_order
    while i < graph.size:
        tick("graph_work")
        order[i] = first.order[graph.size - 1 - i]
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(reversed_graph, order)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

13 thms3 active usersReviewed

Completed

Theoretical Computer Science·Captain: Chutong

CLRS — Chapter 20, §20.3: Depth-First Search — Correctness and Running TimeTextbook

A traversal forest that later algorithms can reuse

Depth-first search records a directed graph's exploration as a predecessor forest with discovery and finish times. Those outputs are used by algorithms that depend on the ordering of exploration, including strongly connected components. This mission targets CLRS, fourth edition, Chapter 20, §20.3; its companion component mission targets §20.5. Both references are fixed by the fourth-edition contents.

Ordered exploration and event times

The input is an unweighted directed graph on $n$ vertices, represented by integer adjacency arrays of arrays and a degree sequence. The number $m$ counts adjacency occurrences, including parallel arcs. Self-loops, disconnected graphs, and the empty graph are included. Prefix entries identify vertices; entries outside those prefixes have no specified meaning.

The reusable entry dfs_ordered receives an allocated root-order sequence whose first $n$ entries form a permutation of the vertices. The ordinary entry dfs constructs identity order and invokes it. Both use the same recursive visit routine. The result includes parent, discovery, finish, color, finish-order, and forest-component arrays, together with event, finished-vertex, and component counts.

Let $d[v]$ and $f[v]$ be discovery and finish times. An ancestor is defined by zero or more returned parent-child links. The output order lists vertices in increasing finish time. The companion SCC source explicitly reverses this prefix; the DFS result itself is not advertised as decreasing order.

Formalization targets

The headline CLRS.DFS.correctness_and_running_time concerns the complete identity-order call. It requests the complete forest and storage contract and one uniform runtime bound:

\exists C\in\mathbb N,\ C>0:\quad T\le C(1+n+m).

The constant is independent of the graph, heap, and initial clocks. Two supporting milestones make the counted work available for composition. CLRS.DFS.ordered_correctness_and_explicit_running_time covers every valid supplied root permutation and requests

T_{\mathrm{ordered}}\le 4+6n+2m.

CLRS.DFS.correctness_and_explicit_running_time covers the complete identity-order entry and requests

T_{\mathrm{dfs}}\le 7+8n+2m.

The identity-order wrapper contributes $3+2n$ marked events outside its ordered call, so the numerical targets compose directly. The explicit ordered budget also supports the second pass of SCC, where the caller supplies decreasing first-pass finish order. Each milestone includes the full postcondition and bounds that same terminating call. All three statements are open contributor tasks; no DFS correctness or runtime proof is supplied.

For every vertex, the returned event times must satisfy

1\le d[v]<f[v]\le2n,

with all $2n$ discovery and finish events distinct. Every non-root parent is an actual input predecessor. Ancestors correspond exactly to nested event intervals:

u\text{ is an ancestor of }v\iff d[u]\le d[v]\ \land\ f[v]\le f[u].

Unrelated intervals are disjoint. The white-path property additionally equates descendants of $u$ with vertices reachable from $u$ using only vertices whose discovery time is at least $d[u]$ . Root-order priority requires every earlier input-order vertex to finish before a later tree root is discovered. These are required structural properties of the ordered traversal; the generated Call relation fixes the concrete adjacency-scanning order.

The finish-order prefix is a vertex permutation with strictly increasing finish times. All output colors are black, the event clock is $2n$ , and the finished count is $n$ . Component labels are contiguous nonempty forest-tree identifiers; equal labels mean the same predecessor tree, not necessarily the same strongly connected component. Every target is an open theorem for contributors.

Reuse beyond a single traversal

A caller can retain the fresh result and continue with its heap, using the unchanged graph and all other pre-existing storage. The caller-facing predicate CLRS.DFS.Post before after result g inputOrder includes both the mathematical result and caller-storage preservation, matching the argument order and preservation placement used by BFS. It requires a fresh result object and six distinct fresh arrays. The goals combine that postcondition with the same terminating Call and its cost. Once proved, the explicit ordered contract supports a later caller's own root permutation without copying the DFS implementation or repeating its analysis.

This scope matters for the textbook SCC construction: its second traversal needs an order supplied by a first traversal. Merely returning timestamps would omit the structural properties that make those timestamps useful. Formalizing the complete contract makes the existing mathematical DFS analysis available through the generated public Call interface; no DFS proof is supplied here.

What must be justified

Valid parent edges and distinct timestamps alone do not identify a DFS forest. The open contract also relates ancestry, interval nesting, white paths, and the outer loop's priority. Directed reachability must not be confused with membership in one DFS tree: an edge may point into a tree that finished earlier. The event-count argument must cover recursive calls and the full outer scan, including already visited vertices, while the empty graph still returns allocated outputs.

Formalization scope

The graph and root-order sequence are read-only and may share input storage where their representation conditions permit it. Recursive calls share a fresh result object. Its component count equals the number of nonempty forest trees; labels follow tree-discovery order. The identity-order entry includes constructing that order in its own cost. The ordered entry's input permutation is supplied by its caller and is preserved.

The shared prerequisites are the published Algo2Lean runtime, module-call support, and unweighted graph representation and specifications. All three missions reuse these same definitions by reference, without introducing duplicate prerequisite bundles. The existing Dijkstra graph definition uses weighted, object-linked adjacency lists; the shared unweighted module supplies the arrays-of-arrays storage contract used here.

The definitions use Algo2Lean v0.1.4, source commit 0f79d5e4242e6477531c9ee4410409f5b1c92f76, in project mode with standalone=false. The source root contains the explicitly named modules below; the entry file is identified for each mission. Raw generated definitions and platform import-path adaptations are recorded separately in the reproduction manifest. Stable generated definitions supply the public Call relations; optional named-line interfaces are not part of the goal statements.

The clock graph_work counts the marked source blocks, function entries, and evaluated loop guards, including final false guards. Each marked block contains a fixed amount of source work. Costs are differences between the caller's actual initial and final counters; other clocks are preserved. This model uses mathematical integer sequences and unbounded integers. It does not assert machine wall-clock time, integer bit complexity, stack-space bounds, or Lean proof-checking time. Construction of the caller's input graph is outside the traversal entry point.

All theorem bodies are open contributor tasks. Supplied definitions and well-formed goal statements are not correctness, termination, or running-time proofs. The requested results concern the displayed program's actual executions, not an assumed-correct replacement algorithm or a hypothesis containing its conclusion.

The complete entry is dfs.algo, with graph_input.algo as its shared dependency. CLRS.DFS.Forest and Post expose the reusable mathematical and storage contracts. Contributions should establish these open obligations against the displayed source.

`graph_input.algo`

# Unweighted directed graph: vertices are 0, ..., size-1.
# Row adj[u][0:degree[u]] lists outgoing targets, with one slot per arc.
# Traversals require nonnegative degrees and in-range targets. Duplicate arcs
# and self-loops are allowed. The constructor stores the supplied references.

class UnweightedGraph:
    size: Int
    adj: Seq[Seq]
    degree: Seq

    def __init__(self, size: Int, adj: Seq[Seq], degree: Seq) -> None:
        self.size = size
        self.adj = adj
        self.degree = degree

`dfs.algo`

# CLRS fourth edition, Section 20.3: depth-first search.
# dfs_ordered takes a permutation of the vertices as its outer-loop order.
# Result.order lists vertices in increasing finish time; reverse its valid
# prefix before using it as the second-pass order in the SCC algorithm.
# graph_work counts the explicitly marked blocks and loop-guard evaluations.

from graph_input import UnweightedGraph


class DFSResult:
    color: Seq
    parent: Seq
    discover: Seq
    finish: Seq
    order: Seq
    component: Seq
    clock: Int
    finished: Int
    components: Int

    def __init__(self) -> None:
        tick("graph_work")
        self.color = const(0)
        self.parent = const(-1)
        self.discover = const(0)
        self.finish = const(0)
        self.order = const(-1)
        self.component = const(-1)
        self.clock = 0
        self.finished = 0
        self.components = 0


def visit(graph: UnweightedGraph, result: DFSResult, u: Int, label: Int) -> None:
    tick("graph_work")
    result.clock += 1
    result.discover[u] = result.clock
    result.color[u] = 1
    result.component[u] = label
    neighbors: Seq = graph.adj[u]
    j: Int = 0
    tick("graph_work")
    # @scan_neighbors
    while j < graph.degree[u]:
        tick("graph_work")
        v: Int = neighbors[j]
        if result.color[v] == 0:
            tick("graph_work")
            result.parent[v] = u
            visit(graph, result, v, label)
        j += 1
        tick("graph_work")
    tick("graph_work")
    result.color[u] = 2
    result.clock += 1
    result.finish[u] = result.clock
    result.order[result.finished] = u
    result.finished += 1


def dfs_ordered(graph: UnweightedGraph, order: Seq) -> DFSResult:
    tick("graph_work")
    result: DFSResult = DFSResult()
    i: Int = 0
    tick("graph_work")
    # @scan_roots
    while i < graph.size:
        tick("graph_work")
        u: Int = order[i]
        if result.color[u] == 0:
            tick("graph_work")
            visit(graph, result, u, result.components)
            result.components += 1
        i += 1
        tick("graph_work")
    tick("graph_work")
    return result


def dfs(graph: UnweightedGraph) -> DFSResult:
    tick("graph_work")
    order: Seq = const(0)
    i: Int = 0
    tick("graph_work")
    # @identity_order
    while i < graph.size:
        tick("graph_work")
        order[i] = i
        i += 1
        tick("graph_work")
    tick("graph_work")
    return dfs_ordered(graph, order)

Selected references

Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022. Publisher; fourth-edition table of contents.
Lunjia Hu and Chutong Yang, Algo2Lean, software release v0.1.4. Lunjia Hu is the project creator. Hosted compiler; fixed release source.

10 thms3 active usersReviewed

All missions

Scaling Blockchains: Can Committee-Based Consensus Help? II: With a Single Voter, Voting for the k Candidates Most Likely to Be Honest Is OptimalResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2 (p. 20)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Climate Impact Investing 1: With an Average-Emissions Interaction Effect the Unique Equilibrium Emission Schedule Is ψ* − ε/(2n+ε)·(ψ* + 2n²ψ̄*/(2n+(n+1)ε)), Below the Schedule Without InteractionResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4(i)

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Revenue Management in Crowdfunding 1: Optimal Pledge Level and Campaign Duration Under Triangular Valuations When Independent or Herding Backers DominateResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Integer Factorization: Why Two-Item Joint Replenishment Is Hard 1: For Odd Composite M, Every Optimal Plan of an Explicit Two-Item Aperiodic JRP Instance Has q₂ = M and 1 < gcd(q₁, M) < MResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 1

Milestones (the steps of the paper's proof, pp. 9–10)

Significance

Difficulty

Formalization scope

Selected references

Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition I: Comparative Statics of an Unconstrained Monopoly's Optimal R&D IntensityResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (p. 5)

Milestones (p. 5 and Appendix A.2, p. 18)

Significance

Difficulty

Formalization scope

Selected references

Quantifying the Impact of Impact Investing I: Mean and Variance of an Impact-Ranked Portfolio's Excess Return under IID Bivariate-Normal Impact Factors and AlphasResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 6 (p. 21), with (31) corrected

Milestones

Significance

Difficulty

Formalization scope

Selected references

Lightning Network Economics: Channels I: The Expected Discounted Cost of a Bidirectional Payment Channel in Closed FormResearch Paper

Payment channels and the cost of locked capital

The model

Formalization targets

Goal: Theorem 1 (ii)

Milestones

What the closed form gives

Where the difficulty lies

Formalization scope

Selected references

Selection and Ordering Policies for Hiring Pipelines via Linear Programming 1: A Non-Adaptive, Committed LP-Rounding Policy for ProbeTop-k Earns at Least (1 − e^{−k}k^k/k!) Times the LP BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty