Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.131121719190Formalized record≥ 2.15Open frontier

9 provers on it18 of 19 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

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

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 1: Random Sampling Vickrey Is Ex-Post IC-IR and a 2(d+1)-Approximation to Welfare for d-SOS ValuationsResearch Paper

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Main theorem

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

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

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

Supporting results

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

7 thms3 active usersReviewed

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

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

Analysis Operations Research Optimization+1·Captain: mikedeng1

Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality II: The Optimal Competitive Ratio Tends to the i.i.d. Prophet Constant as p Tends to 1Research Paper

Motivation

Optimal stopping with samples sits between two classical problems. In the secretary problem a decision maker sees items in random order, knows nothing about their values, and must stop on one; the best guarantee is $1/e$ . In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee against the expected maximum is the constant $\alpha^*\approx0.745$ : Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017) showed that it is achieved. Real decision makers usually have neither nothing nor everything: they have a history of past observations.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) model this as $p$ -DOS (sample-driven optimal stopping): each of $N$ items is independently placed in a history set with probability $p$ , the decision maker sees the history first and then the remaining items online, and must stop on one online item. At $p=0$ this is the secretary problem; as $p\to1$ the history reveals the distribution and the problem approaches the i.i.d. prophet setting. This mission formalizes the paper's Theorem 8, which makes the second statement precise: the optimal guarantee tends to $\alpha^*$ .

Timeline. Hill and Kertz (1982) compared stop-rule and supremum expectations for i.i.d. variables; Kertz (1986) completed the comparison, giving the worst-case constant $\approx0.745$ through the integral equation used below; Correa et al. (2017) gave a matching algorithm. Kaplan, Naori and Raz (2020) studied the sample-driven model with a weaker bound for small $p$ ; Correa, Dütting, Fischer and Schewior (2019) and Rubinstein, Wang and Weinberg (2020) studied i.i.d. values with samples from an unknown distribution. The present paper (2020–2021) gives the exact limit program and Theorem 8.

Setting

Fix $p\in(0,1)$ . A stopping rule is a nonnegative function $q(t,\ell)$ of a time $t\in[p,1]$ and a rank $\ell\ge1$ . For $k\ge1$ let

F_k(q)=\sum_{\ell=1}^{k}\int_p^1 q(t,\ell)\sum_{j=\ell}^{k}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^{\ell}\,dt .

The limit program SDCLP $_p$ maximizes $\alpha\in[0,1]$ over pairs $(q,\alpha)$ with

t\,q(t,\ell)+\int_p^t\sum_{s\ge1}q(\tau,s)\,d\tau\le1\quad(t\in[p,1],\ \ell\ge1),\qquad \alpha\le\frac{F_k(q)}{1-p^k}\quad(k\ge1).

Its optimal value is $\alpha(p)$ . The paper obtains SDCLP $_p$ as the limit $N\to\infty$ of the linear programs that describe the best algorithm for $p$ -DOS with adversarial values (§4.1–4.2); Theorem 8 is a statement about the program's value.

Two constants are defined by equations. $\tilde\alpha(p)$ is the unique root in $(0,1)$ of

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

and $\alpha^*$ is the solution of $\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1$ . A threshold rule (12) is given by times $p=t_1\le t_2\le\cdots\le1$ with $T_i=\prod_{j\le i}t_j$ : on $[t_i,t_{i+1})$ it equals $T_i/t^{i+1}$ for ranks $\ell\le i$ and $0$ for larger ranks.

Formalization targets

Goal: Theorem 8

0\le\tilde\alpha(p)\le\alpha(p)\le\alpha^*\quad(p\in(0,1)),\qquad \lim_{p\to1^-}\tilde\alpha(p)=\lim_{p\to1^-}\alpha(p)=\alpha^*.

Milestones, in the order the proof uses them

B.4: $\sum_{\ell=1}^{j}\binom{j-1}{\ell-1}(1-t)^{j-\ell}t^\ell=t$ .
Lemma 4: a maximal $\alpha$ satisfies $\alpha\ge\inf_{k\ge1}\frac{1}{1-p^k}\sum_{j\le k}\int_p^1 t\,q(t,j)\,dt$ when $q$ is non-increasing in $\ell$ .
Lemma 5: for a threshold rule, the system "every term of that infimum equals $\alpha$ " is equivalent to explicit equations (15)–(16).
Lemma 6 (i), (ii): the times $t_1=p$ , $t_2=pe^{\alpha(1-p)^2/p}$ , $(t_k/t_{k+1})^{k-1}=\gamma_k/\gamma_{k-1}$ increase, and their limit is at most $1$ exactly under condition (18).
B.6: $T_i/t_i^{i-1}=p\gamma_{i-1}$ and $\mu_k=p(1-\alpha+\alpha p^{k-2})/(k-2)$ .
Lemma 6 (iii): under (18) the threshold rule is feasible with value $\alpha$ .
Lemma 7: (19) has a unique root, continuous in $p$ .
B.8: the ratio $h(p,\eta)$ of the two sides of (19) tends to $\int_0^1\frac{dy}{y(1-\ln y)+1/\eta-1}$ as $p\to1$ .

Significance

The result. Theorem 8 shows that sample access interpolates continuously between the secretary and prophet worlds and that, with almost full information, no more than the known-distribution guarantee $\alpha^*$ is lost or gained. The explicit rule behind $\tilde\alpha(p)$ is a concrete threshold algorithm, and the companion Theorem 9 of the paper ( $\tilde\alpha(p)\ge\alpha^*p$ , a separate mission) turns it into sample-complexity bounds: $O(n/\varepsilon)$ samples suffice for $\alpha^*-O(\varepsilon)$ .

Formalizing it. The result is proved on paper; no part of it is machine-checked. A formal proof contributes a verified treatment of an infinite-dimensional linear program over $L^1([p,1]\times\mathbb N)$ , of series defined through implicit equations, and of a Riemann-sum limit obtained by l'Hôpital's rule. One clause, $\alpha(p)\le\alpha^*$ , is not proved in the paper: it is imported from the i.i.d. prophet inequality literature via the interpretation of $\alpha(p)$ as a competitive ratio. A formal proof of that clause directly from SDCLP $_p$ would be new.

Difficulty

The lower bound $\tilde\alpha(p)\le\alpha(p)$ needs an explicit feasible point of an infinite program; checking feasibility of the threshold rule requires exact telescoping of series with products of the times $t_k$ , which are defined recursively through fractional powers. The limit $\tilde\alpha(p)\to\alpha^*$ is a $0/0$ limit of infinite series whose terms change scale as $p\to1$ : every individual term tends to zero, so termwise passage to the limit gives no information, and the integral in the defining equation of $\alpha^*$ appears only in an aggregate limit of the whole series. The upper bound $\alpha(p)\le\alpha^*$ cannot come from evaluating any single solution: it is a statement about every feasible $q$ , and the paper obtains it only through an external argument.

Formalization scope

A stopping rule is q : ℝ → ℕ → ℝ; ranks are 1-based (values at rank $0$ are never used), and constraints are imposed pointwise on $[p,1]$ as printed. The integral of the series in (10) is a lower Lebesgue integral of an $[0,\infty]$ -valued series, so it cannot collapse to a junk value; each $q(\cdot,\ell)$ is required integrable on $[p,1]$ .
$\alpha(p)$ is sSup of the set of feasible $\alpha$ ; it contains $0$ and is bounded by $1$ , so it is the true supremum (checked in a sorry-free verification file). The program ranges over all feasible $q$ , never only threshold rules.
(11) is quantified over $k\ge1$ only, so $1-p^k\neq0$ .
Threshold rules use the half-open intervals $[t_i,t_{i+1})$ of (7); (12) prints closed intervals, which overlap at the $t_i$ .
The series in (18), (19), (26) and $\mu_k$ are written with the summation index shifted to start at $0$ ; with $p,\alpha\in(0,1)$ every logarithm's argument lies in $[1-\alpha,1]$ , so they converge absolutely and tsum is the true sum.
Lemma 6's recursion is $t_{k+1}=t_k(\gamma_{k-1}/\gamma_k)^{1/(k-1)}$ for $k\ge2$ , the unique positive solution of (17).
$\tilde\alpha$ and $\alpha^*$ are predicates (IsAlphaTilde, IsAlphaStar), not chosen functions; the goal holds for every root selection. Existence and uniqueness of $\alpha^*$ (with $\beta=1/\alpha^*$ ) is already posed as the open item CorreaThreshold.Adaptive.beta_star_existsUnique and is not posed again.
" $p\to1$ " is the one-sided filter 𝓝[<] 1.
Lemma 6 (iii) carries hypothesis (18), which the paper states in the sentence after the lemma; without it the claim is false.

Trivializing formalizations are ruled out: replacing $\alpha(p)$ by $\tilde\alpha(p)$ or by the value of a truncated program, fixing $p$ , restricting $q$ to threshold rules in the definition of $\alpha(p)$ , or replacing $\alpha^*$ by $0.745$ each changes the theorem and is not done.

A complete development needs: binomial identities, interval integrals of $t^{-i}$ and of piecewise-defined functions, real powers and logarithms of recursively defined sequences, summability of series in $\ell^1$ , continuity of the root of a monotone family of equations, and limits of Riemann-type sums on $(0,1]$ . The last two are reusable beyond this mission. Proofs of individual milestones are welcome independently of the goal.

Selected references

J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021. https://arxiv.org/abs/2011.06516v2
T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, The Annals of Probability 10(2), 336–345, 1982 (reference [26] of the paper).
R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 88–112, 1986 (reference [28]).
J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted price mechanisms for a random stream of customers, ACM EC 2017 (reference [17]).
H. Kaplan, D. Naori, D. Raz, Competitive analysis with a sample and the secretary problem, SODA 2020 (reference [27]).
J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet inequalities for i.i.d. random variables from an unknown distribution, ACM EC 2019 (reference [15]).
A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal single-choice prophet inequalities from samples, ITCS 2020 (reference [40]).

14 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

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

Operations Research Optimization Probability·Captain: mikedeng1

Achieving High Individual Service Levels Without Safety Stock? Optimal Rationing Policy of Pooled Resources II: The Max-Weighted-Service Policy Is Almost Surely Asymptotically OptimalResearch Paper

Motivation

Firms that serve several customers from shared capacity, such as a warehouse supplying several retailers, a flexible production line building several products, or an assemble-to-order system, often sign contracts that guarantee each customer an individual service level. Typical targets are the probability of filling a customer's whole demand (Type-I), the expected fraction of demand filled (Type-II or Type-III), each required to be at least a target $\beta_j$ . Once demand is realized, the firm must decide how to ration the pooled resources among customers. Jiang, Wang and Zhang (SSRN 3385089, published in Operations Research, doi:10.1287/opre.2022.2386) ask how much capacity suffices and which rationing policy meets all targets at least cost. The exact optimal policy is an infinite-dimensional program over randomized policies, (11). This mission formalizes the paper's answer to the second question: a simple, learnable policy is asymptotically optimal.

Setting

There are $n$ customers $N=\{1,\dots,n\}$ and $m$ resources. The capacity vector $c\in\mathbb R^m_{\ge0}$ is fixed. The demand $\tilde D\in\mathbb R^n_{\ge0}$ is random with law $F$ . After observing a demand vector $D$ , the firm chooses a solution $(s,y)$ from a compact set $P(c,D)$ . Here $s_j\le D_j$ is the demand of customer $j$ that is fulfilled and $y_{ij}$ is the amount of resource $i$ given to customer $j$ . The solution costs $f(y)$ , with $f$ linear, and customer $j$ receives service $R_j(s_j,D_j)\ge0$ .

A deterministic policy $\varphi$ maps each demand vector to a feasible solution $(s(\varphi,c,D),y(\varphi,c,D))$ . A randomized policy $\lambda$ picks a deterministic policy at random.
The service level of customer $j$ under $\lambda$ is $\int E_{\tilde D}[R_j(s_j(\varphi,c,\tilde D),\tilde D_j)]\,d\lambda(\varphi)$ , and the expected cost is $\int E_{\tilde D}[f(y(\varphi,c,\tilde D))]\,d\lambda(\varphi)$ .
The capacity $c$ is feasible if some $\lambda$ meets every target $\beta_j\in(0,1)$ . $\mathrm{Obj}(11)$ is the least expected cost among such $\lambda$ .
For weights $w\in\mathbb R^n_{\ge0}$ , the Max-Weighted-Service problem (16) is $\min_{(y,s)\in P(c,D)} f(y)-\sum_j w_jR_j(s_j,D_j)$ . The policy $\varphi_w$ picks one of its optimal solutions for every $D$ .
Algorithm 1 draws independent samples $D^{(1)},\dots,D^{(T)}$ from $F$ . It starts from $w^{(1)}=0$ and updates the weights by

w^{(t+1)}_j=\Big[w^{(t)}_j+\gamma_T\big(\beta_j-R_j(s_j(\varphi_{w^{(t)}},c,D^{(t)}),D^{(t)}_j)\big)\Big]^+,\qquad \gamma_T=T^{-(1/2+\epsilon)}.

It then adopts $\varphi_w$ at a uniformly drawn iterate $w$ .

The Lean development uses the same letters: detService, detCost, IsFeasible, obj11, mwsObjective, mwsIter, stepSize, G, Gstar, Lterm.

Formalization targets

Goal: Theorem 3 (p. 17)

Under Assumptions 1 and 3, if $c$ is feasible and $\epsilon\in(0,1/2)$ , then almost surely

\limsup_{T\to\infty}\frac1T\sum_{t=1}^TE_{\tilde D^t}\big[f(y(\varphi_{w^{(t)}},c,\tilde D^t))\big]\le\mathrm{Obj}(11),\qquad \liminf_{T\to\infty}\frac1T\sum_{t=1}^TE_{\tilde D^t}\big[R_j(s_j(\varphi_{w^{(t)}},c,\tilde D^t),\tilde D^t_j)\big]\ge\beta_j\ \ \forall j.

Here $\tilde D^t$ is a fresh copy of the demand, so each expectation is taken with the iterate fixed. The statement holds for every tie-breaking rule in (16).

Milestones (pp. 52–54)

Weak duality: $\sum_jw_j\beta_j+E[f(y(\varphi_w))]-\sum_jw_jE[R_j(s_j(\varphi_w),\tilde D_j)]\le\mathrm{Obj}(11)$ for every $w\ge0$ .
Lemma 4 (Azuma's inequality) and Lemma 5 (Borel–Cantelli), both already proved on the platform and referenced.
(57): a pathwise regret bound for the iterates against $G(w^*)=\sup_{w\ge0}G(w)$ .
The noise vanishes: $\gamma_T\sum_{t\le T}L_t\to0$ almost surely, for the martingale terms $L_t$ of (55).
Lemma 6: $w^{(T+1)}_j/(T\gamma_T)\to0$ almost surely.

Significance

Theorem 3 replaces an optimization over probability measures on a space of functions by a sequence of finite-dimensional problems (16) and a one-line dual update. Problem (16) is often solved greedily: under a polymatroid structure the paper's Theorem 4 turns it into an index rule. The result therefore justifies a practical rationing heuristic with a guarantee: a firm that runs Algorithm 1 on historical demand gets a policy whose average cost is asymptotically no worse than the optimum of (11), and whose service levels asymptotically meet every individual target.

On the formal side, the statement and its milestones combine a projected stochastic subgradient method, a triangular array of bounded martingale differences, and the weak duality of a semi-infinite program. The paper proves the result; none of it has been machine-checked. A formal proof must also repair the paper's argument for (28): the stochastic-dominance induction on p. 54 does not establish an almost-sure limit.

Difficulty

The obvious argument treats the iterates as a standard online gradient method with a fixed step. That handles the expected regret but not the almost-sure claim. The noise terms $L_t$ depend on the horizon $T$ , both through $\gamma_T$ and through every earlier iterate, so they form a triangular array, not a single martingale. Classical stochastic-approximation theorems with decreasing steps do not apply. Feasibility of $c$ enters only through the dual bound $G(w^*)\le\mathrm{Obj}(11)$ . The expectations $E_{\tilde D^t}$ are over a fresh copy with the random iterate held fixed, and that must be kept separate from the sample $D^{(t)}$ the iterate itself uses. The service half (28) needs a bound on the growth of the dual weights (Lemma 6), and that bound itself needs the cost to be bounded on feasible allocations.

Formalization scope

Indices are 0-based: customers and resources are Fin n and Fin m. The Lean iterate at index $t$ is the page's $w^{(t+1)}$ , and $\sum_{t=1}^T$ becomes a sum over $0,\dots,T-1$ .
Randomized policies are finite mixtures of measurable deterministic policies. Every quantity here depends on a mixture only through finitely many expectations, so this is no restriction.
Selections: the theorems quantify over every selection $w\mapsto\varphi_w$ of optimal solutions of (16). It is assumed jointly measurable in $(w,D)$ , so that the iterates are random variables.
Sampling: all horizons $T$ read the first $T$ entries of one i.i.d. sequence. That single probability space is what "almost surely as $T\to\infty$ " requires.
Limits: $\limsup\le$ and $\liminf\ge$ are written as "for every $\varepsilon>0$ , eventually in $T$ ".
Norms: the Euclidean norm in (57) is a written-out sum of squares, because Lean's default norm on Fin n → ℝ is the sup norm.
Added hypotheses, beyond Assumptions 1 and 3 and the standing assumptions of §1.1:
- $R_j\ge0$ and jointly measurable;
- $s\le D$ on $P(c,D)$ for $D\ge0$ ; instances whose page-level $P(c,D)$ is empty for negative $D$ extend it by $P(c,D^+)$ ;
- $|f|\le K$ on feasible allocations, which the paper's proof of Lemma 6 uses implicitly.

Two formalizations would make (27) trivial, and both are ruled out. $\mathrm{Obj}(11)$ is the infimum of the cost over feasible mixtures; it is neither defined from the algorithm nor identified with $G(w^*)$ . Feasibility and $|f|\le K$ keep that infimum from being Lean's junk value $0$ . The selection depends on $w$ alone, not on $\beta$ or on the sample path.

The development needs Bochner integrals, independence (iIndepFun), conditional expectation and the referenced Azuma and Borel–Cantelli results. The triangular-array strong law for bounded martingale differences with summable exponential tails is reusable beyond this mission. Contributions toward any milestone, or a repaired proof of (28), are welcome.

Selected references

J. Jiang, S. Wang, J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, SSRN 3385089 (version of 31 July 2021); Operations Research (2023). https://ssrn.com/abstract=3385089, https://doi.org/10.1287/opre.2022.2386
K. Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967) 357–367. https://doi.org/10.2748/tmj/1178243286
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer (2001) 135–165. https://doi.org/10.1007/978-1-4757-3403-4_7
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19 (2009) 1574–1609. https://doi.org/10.1137/070704277

11 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

Linear algebra Quantum Information·Captain: mikedeng1

Improvements in Quantum SDP-Solving with Applications 2: A Two-Outcome Measurement Implemented With Bias ε Gives a (1, a+1, ε)-Block-Encoding of Its POVM Element MResearch Paper

Motivation

Many recent quantum algorithms for linear algebra and optimization take their input as a block-encoding: a unitary circuit whose top-left block, after projecting a set of ancilla qubits onto $|0\rangle$ , approximates the matrix of interest. The quantum semidefinite-programming solver of van Apeldoorn and Gilyén (arXiv:1804.05058) introduces the quantum operator model, in which every constraint matrix of the SDP is given this way (Definition 2, p. 4). Block-encodings are also the input format of quantum singular value transformation and of Hamiltonian simulation by qubitization (Low and Chuang, arXiv:1610.06546).

A natural question is where block-encodings come from in applications. In §4.1, on shadow tomography, the constraint matrices are the elements $E_j$ of two-outcome measurements, and what a user can do is perform those measurements, not write down their matrices. The closing remark of §4.1 (pp. 24–25) answers the question for that setting: if a two-outcome measurement can be implemented on a quantum computer with small bias, then a block-encoding of its measurement operator can be built from the same circuit with one extra qubit and one CNOT gate. The remark is credited to the same observation by Low and Chuang (arXiv:1707.05391).

Setting

A two-outcome POVM on a finite-dimensional system is a pair $\{M, I - M\}$ of operators with $M$ and $I - M$ positive semidefinite. A mixed state (density matrix) is a positive semidefinite operator $\rho$ with $\operatorname{Tr}\rho = 1$ ; outcome $M$ occurs with probability $\operatorname{Tr}(M\rho)$ .

An implementation of the measurement on a quantum computer, as the paper fixes it, takes the input $\rho$ , attaches $a$ ancilla qubits in the state $|0\rangle^{\otimes a}$ , applies a unitary $U$ to system and ancillas, measures in the computational basis, and accepts when the last qubit reads $|0\rangle$ :

\rho \to \rho\otimes|0\rangle\langle 0|^{\otimes a} \to U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger \to \operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big).

The implementation has bias at most $\varepsilon$ if, for every state $\rho$ ,

\Big|\operatorname{Tr}\Big((I\otimes|0\rangle\langle 0|)\,U\big(\rho\otimes|0\rangle\langle 0|^{\otimes a}\big)U^\dagger\Big) - \operatorname{Tr}(M\rho)\Big| \le \varepsilon. \qquad (14)

Write $K = (I\otimes\langle 0|^{\otimes a})\,U^\dagger(I\otimes|0\rangle\langle 0|)U\,(I\otimes|0\rangle^{\otimes a})$ , an operator on the system. A unitary $V$ on $a'$ ancilla qubits and the system is an $(\alpha, a', \varepsilon)$ -block-encoding of $A$ (Definition 2) if $\|A - \alpha(\langle 0|^{\otimes a'}\otimes I)V(|0\rangle^{\otimes a'}\otimes I)\| \le \varepsilon$ in the operator norm. Finally $U' = U\otimes I_2$ adds one fresh qubit, and $I\otimes\mathrm{CNOT}$ is a CNOT gate whose control is the measured qubit and whose target is the fresh qubit.

Formalization targets

Goal (§4.1, p. 25)

\text{(14)} \;\Longrightarrow\; U'^\dagger(I\otimes\mathrm{CNOT})U' \text{ is a } (1,\ a+1,\ \varepsilon)\text{-block-encoding of } M .

The subnormalization is $1$ , the ancilla count is $a' = a + 1$ and the error is the same $\varepsilon$ as the bias; none of these is weakened.

Milestones (all p. 25, in the order of the derivation)

The trace identity: $\rho\otimes|0\rangle\langle 0|^{\otimes a} = (I\otimes|0\rangle^{\otimes a})\rho(I\otimes\langle 0|^{\otimes a})$ , hence the acceptance probability equals $\operatorname{Tr}(K\rho)$ .
The equivalence $\forall\rho:\ |\operatorname{Tr}([K - M]\rho)| \le \varepsilon \iff \|K - M\| \le \varepsilon$ , with $\rho$ over density matrices.
The CNOT identity $K = (I\otimes\langle 0|^{\otimes a'})\,U'^\dagger(I\otimes\mathrm{CNOT})U'\,(I\otimes|0\rangle^{\otimes a'})$ .

Significance

The result. It converts an operational primitive, performing a measurement, into the input format that block-encoding algorithms consume, with an additive error equal to the measurement's bias and at the cost of one qubit and one CNOT. In the paper it is what makes the shadow-tomography application of §4.1 meaningful: the cost of the SDP solver is stated in terms of block-encodings of the $E_j$ , and this remark lets one replace that by the cost of controlled implementations of the measurements. More generally it shows that the quantum operator model is no stronger than the ability to measure.

Formalizing it. The paper proves the remark in a few displayed lines, one of which ("it is easy to see") is left to the reader and whose CNOT direction is not printed. No machine-checked version exists. A formal proof fixes the register conventions, makes the direction of the CNOT explicit, and contributes a reusable fact about matrices: for a Hermitian $X$ , $\sup_\rho |\operatorname{Tr}(X\rho)| = \|X\|$ over density matrices. The block-encoding predicate itself is already published on the platform and is reused.

Difficulty

The algebra of milestones 1 and 3 is bookkeeping over tensor-product index sets, and the main cost there is choosing representations that make the registers line up.

The one step with mathematical content is the direction " $\Rightarrow$ " of milestone 2. The bias condition controls $|\operatorname{Tr}(X\rho)|$ only for density matrices $\rho$ , that is, it bounds the numerical radius of $X = K - M$ , while a block-encoding needs the operator norm. For a general matrix these differ by up to a factor of two, so the step needs $X$ to be Hermitian: $M$ is Hermitian as a POVM element, and $K$ is Hermitian because it is a compression of the projector $I\otimes|0\rangle\langle 0|$ . A formal proof must use both facts and exhibit a state that attains the norm.

Formalization scope

The Lean development lives in the namespace QuantumSDP18.MeasureBE. Its conventions are:

The system register is an arbitrary finite type $\iota$ (a $w$ -qubit system is $\iota = \{0,1\}^w$ ). Operators are complex matrices; $\dagger$ is the conjugate transpose; the operator norm is the platform's QAlgorithms.specNorm.
The ancilla register is Qubits c × Bool, so $a = c + 1 \ge 1$ and the Bool factor is the last, measured qubit. The basis state $|0\rangle$ of any register is its all-false index.
(14) ranges over all density matrices (PosSemidef with trace $1$ ), and its absolute value is the modulus of a complex trace.
The CNOT is the platform's QAlgorithms.cnot (control first), placed on the measured qubit (control) and the fresh qubit (target). With the opposite direction the block is $U^\dagger U$ and the goal is false; the chosen direction is the only reading under which the page's identity holds.
The block-encoding predicate is the platform's QAlgorithms.IsBlockEncoding, which puts the ancilla register first, as Definition 2 does; the circuit, written system-first as on p. 25, is reindexed to match.
Added hypothesis: $\varepsilon \ge 0$ (a bias is nonnegative). It matters only for a zero-dimensional system, where (14) holds vacuously.

The goal keeps both POVM hypotheses ( $M \succeq 0$ and $I - M \succeq 0$ ), and the bias condition quantifies over all states rather than one fixed state, under which the conclusion would be false. A formalization in which (14) ranges over arbitrary matrices, or which drops the CNOT and states only $\|K - M\| \le \varepsilon$ , is a different theorem.

Needed infrastructure: Kronecker products and reindexing of matrices, the unitarity of permutation matrices and of Kronecker products, and the variational characterization of the operator norm of a Hermitian matrix through its eigenvectors. The last is reusable beyond this mission. Proofs of the three milestones are welcome independently.

Selected references

J. van Apeldoorn, A. Gilyén, Improvements in quantum SDP-solving with applications, arXiv preprint, 2018 (ICALP 2019). https://arxiv.org/abs/1804.05058
G. H. Low, I. L. Chuang, Hamiltonian simulation by qubitization, arXiv preprint, 2016 (Quantum 3, 163, 2019). https://arxiv.org/abs/1610.06546
G. H. Low, I. L. Chuang, Hamiltonian simulation by uniform spectral amplification, arXiv preprint, 2017. https://arxiv.org/abs/1707.05391
S. Aaronson, Shadow tomography of quantum states, STOC 2018. https://arxiv.org/abs/1711.01053

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 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 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

Completed

Theoretical Computer Science·Captain: Chutong

CLRS — Chapter 20, §20.2: Breadth-First Search — Correctness and Running TimeTextbook

Shortest paths in an unweighted graph

Breadth-first search computes which vertices can be reached from a source and the fewest edges needed to reach each one. Its predecessor information also records a shortest route. This mission belongs to the CLRS fourth-edition formalization series and targets Chapter 20, §20.2, including the algorithm's linear running-time guarantee. The section placement is given in the publisher's table of contents.

Graph, source, and outputs

A directed graph consists of vertices numbered $0,\ldots,n-1$ and outgoing adjacency rows. The field adj[u] is an integer sequence, and degree[u] determines its meaningful prefix. Every entry in that prefix must name a valid vertex. Let $m$ be the sum of these row lengths: parallel arcs count separately, and self-loops are permitted. An undirected graph is represented by symmetric directed entries, with both directions counted in $m$ .

The caller supplies a valid source $s$ , with $0\le s<n$ . Consequently, the source contract excludes the empty graph. The distance output uses $-1$ for an unreachable vertex; otherwise it records a nonnegative number of edges. The parent output uses $-1$ at the source and unreachable vertices. Other reached vertices have a predecessor. No particular choice between equally short routes is required.

Formalization targets

The headline CLRS.BFS.correctness_and_running_time asks for one actual terminating bfs.Call whose result satisfies correctness, preservation, allocation, and running time together. Write $D$ and $P$ for its output arrays and $s\leadsto v$ for a finite directed walk in the initial graph. For every vertex $v$ ,

D[v]=-1\iff\neg(s\leadsto v).

When $D[v]\ge0$ , the returned distance is attained and minimal:

\exists\text{ a walk }s\leadsto v\text{ of length }D[v],\qquad D[v]\le\text{length}(p)\text{ for every walk }p:s\leadsto v.

Moreover, $D[s]=0$ , $P[s]=-1$ , and each reached $v\ne s$ satisfies

P[v]\to v,\qquad D[P[v]]+1=D[v].

The running-time target is uniform over inputs, heaps, adjacency order, and initial counters:

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

Here $T$ is the increment of graph_work for that same call. The supporting milestone correctness_and_explicit_running_time retains the stronger numerical target

T\le 6n+2m+5

with the identical correctness and storage contract. Both statements are open; the numerical bound is a requested obligation, not an established result.

A reusable shortest-path contract

The result allows a later caller to read shortest distances and predecessor edges while continuing with the returned heap. The caller-facing predicate CLRS.BFS.Post before after result g source includes both the mathematical result and caller-storage preservation. It requires a fresh result object and two distinct fresh arrays, and preserves every previously allocated sequence, object, and collection. The goals combine that postcondition with the same terminating Call and its cost. Input graph storage therefore remains available for further traversals.

The textbook supplies the mathematical algorithm and analysis; the work here is their formal verification against a mutable source program. The finite-prefix specification gives callers useful facts without prescribing irrelevant sequence entries outside the vertex range. The source's discovery state is encoded by distance $-1$ , and its queue is a fresh sequence with head and tail indices. These are implementation choices within the stated BFS contract. The familiar correctness and complexity claims are discussed in CLRS, fourth edition, §20.2.

What must be justified

Returning a reachable predecessor alone does not establish shortestness. The contract also requires minimum distance and a correct unreachable sentinel. Cycles, repeated adjacency entries, and edges to vertices already discovered must not produce repeated queue insertion or invalidate the cost bound. An execution theorem must establish termination and the result together; reasoning only about executions that happen to return leaves a missing obligation.

Formalization scope

CLRS.GraphTraversal.GraphRep connects the input heap to a finite mathematical graph. Adjacency rows may share references, because traversal only reads them. Validity includes allocated rows and nonnegative degrees. The explicit initialization loop is counted even though the result constructor already gives the same default values. Outputs are fresh, so their mutation cannot change aliased input storage.

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 complete source entry is bfs.algo; its shared dependency is graph_input.algo. Contributors may add proof lemmas or named observations while retaining the main source-facing 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

`bfs.algo`

# CLRS, fourth edition, Chapter 20, Section 20.2: breadth-first search.
# Adjacency rows contain vertex identifiers; degree gives each finite row length.
# The graph is read-only. A valid source lies between 0 and graph.size - 1.

from graph_input import UnweightedGraph


class BFSResult:
    distance: Seq
    parent: Seq

    def __init__(self) -> None:
        tick("graph_work")
        self.distance = const(-1)
        self.parent = const(-1)


def bfs(graph: UnweightedGraph, source: Int) -> BFSResult:
    tick("graph_work")
    result = BFSResult()
    vertex: Int = 0

    tick("graph_work")
    while vertex < graph.size:
        tick("graph_work")
        result.distance[vertex] = -1
        result.parent[vertex] = -1
        vertex += 1
        tick("graph_work")

    tick("graph_work")
    queue: Seq = const(-1)
    head: Int = 0
    tail: Int = 1
    queue[0] = source
    result.distance[source] = 0

    tick("graph_work")
    while head < tail:
        tick("graph_work")
        vertex = queue[head]
        head += 1
        index: Int = 0

        tick("graph_work")
        while index < graph.degree[vertex]:
            tick("graph_work")
            neighbor: Int = graph.adj[vertex][index]
            if result.distance[neighbor] == -1:
                tick("graph_work")
                result.distance[neighbor] = result.distance[vertex] + 1
                result.parent[neighbor] = vertex
                queue[tail] = neighbor
                tail += 1
            index += 1
            tick("graph_work")

        tick("graph_work")

    tick("graph_work")
    return result

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.

6 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Fair and Consistent Prize Allocation in Competitions 1: A Prize Allocation Rule Satisfies Order Preservation, Endowment Monotonicity and Consistency iff It Is an Interval RuleResearch Paper

Motivation

Sports leagues, tournaments, esports events and research competitions all end with a ranking of the participants and a sum of prize money to divide among them. How the money is split according to the ranking is a design choice with visible consequences: Winner-Takes-All schemes reward only the top, equal division ignores the ranking, and most real prize schedules sit in between. The economics of tournaments has studied prize structures as incentive devices, but it has not asked which schedules follow from principles of fairness and coherence.

Dietzenbacher and Kondratev (arXiv:2008.08985, Management Science 2023) take the axiomatic approach of fair allocation theory to this question. The central axiom is consistency, the variable-population principle that has characterized solutions in bankruptcy, taxation, bargaining and cooperative games (Aumann and Maschler 1985; Young 1987; Lensberg 1988; Thomson 1988; Hart and Mas-Colell 1989): if any subgroup of competitors pools its prizes and re-divides them among themselves by the same rule, nobody's prize changes. This mission formalizes the paper's first main result, which identifies exactly the rules that are consistent, weakly respect the ranking, and never take money away when the endowment grows.

Setting

Let $U$ be a countable set of at least three potential competitors. A competition is a triple $(N, \mathcal R, E)$ : a nonempty finite set $N \subseteq U$ , a ranking $\mathcal R : N \to \{1, \dots, |N|\}$ (a bijection; $i$ is ranked above $j$ if $\mathcal R(i) < \mathcal R(j)$ ), and a prize endowment $E \ge 0$ . For a nonempty $S \subseteq N$ , the subranking $\mathcal R_S$ lists $S$ in the order of $\mathcal R$ .

A prize allocation rule $\varphi$ assigns to every competition an allocation $\varphi(N, \mathcal R, E) \in \mathbb R^N_+$ with $\sum_{i \in N} \varphi_i(N, \mathcal R, E) = E$ . Two basic rules are Equal Division, $\mathrm{ED}_i = E/|N|$ , and Winner-Takes-All, $\mathrm{WTA}_i = E$ if $\mathcal R(i) = 1$ and $0$ otherwise.

The axioms of the main theorem are, for every competition and $i, j \in N$ :

order preservation: $\mathcal R(i) < \mathcal R(j) \Rightarrow \varphi_i(N, \mathcal R, E) \ge \varphi_j(N, \mathcal R, E)$ ;
endowment monotonicity: $E < E' \Rightarrow \varphi_i(N, \mathcal R, E) \le \varphi_i(N, \mathcal R, E')$ ;
consistency: for every nonempty $S \subseteq N$ and $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).

Anonymity (prizes depend only on $|N|$ , the position and $E$ ) and endowment continuity are auxiliary properties.

An interval rule is given by pairwise disjoint open intervals $(a_k, b_k)$ , $k = 1, 2, \dots$ , with $a_k \in \mathbb R_+$ and $b_k \in \mathbb R_+ \cup \{+\infty\}$ . With $n = |N|$ and $r = \mathcal R(i)$ ,

\varphi_i(N, \mathcal R, E) = \begin{cases} a_k & \text{if } n a_k \le E \le (n - r + 1) a_k + (r - 1) b_k; \\ E - (n - r) a_k - (r - 1) b_k & \text{if } (n - r + 1) a_k + (r - 1) b_k \le E \le (n - r) a_k + r b_k; \\ b_k & \text{if } (n - r) a_k + r b_k \le E \le n b_k; \\ E / n & \text{otherwise.} \end{cases}

At endowment $n a_k$ everyone receives $a_k$ ; as $E$ grows, prizes are raised to $b_k$ one competitor at a time from the top; when $E/n$ lies in no $[a_k, b_k]$ the endowment is divided equally. ED has $a_k = b_k = 0$ ; WTA has $a_1 = 0$ , $b_1 = +\infty$ .

Formalization targets

Goal: Theorem 1 (p. 13)

\varphi \text{ satisfies order preservation, endowment monotonicity and consistency} \iff \varphi \text{ is an interval rule.}

Both directions are part of the goal.

Milestones, in the order the proof uses them

Lemma 1 (p. 10): endowment monotonicity implies endowment continuity.
Lemma 2 (p. 11): order preservation, endowment monotonicity and consistency imply anonymity.
Lemma 3 (p. 11): two endowment monotonic, consistent rules that agree on all two-competitor competitions agree on all competitions.
The "if" direction (p. 28): every interval rule satisfies the three axioms.
Step 1 (p. 28): for two competitors, if $\varphi(N, \mathcal R, x_1 + x_2) = (x_1, x_2)$ then $\varphi(N, \mathcal R, 2x_1) = (x_1, x_1)$ or $\varphi(N, \mathcal R, 2x_2) = (x_2, x_2)$ .
Step 2 (p. 29): the two-competitor restriction has the interval form (9),

\varphi(N, \mathcal R, E) = (E - a_k, a_k) \text{ on } [2a_k, a_k + b_k], \quad (b_k, E - b_k) \text{ on } [a_k + b_k, 2b_k], \quad (E/2, E/2) \text{ otherwise.}

Further statements of §2.3

Lemma 4 (endowment additivity ⇔ scale invariance) and Corollaries 1–4, which single out WTA (winner-loser strict order preservation), ED (strict endowment monotonicity), the Winner-Takes-Surplus rules (winner strict endowment monotonicity) and the pair {ED, WTA} (additivity) inside the family of Theorem 1, are included as supporting theorems.

Significance

Theorem 1 replaces three qualitative requirements by an explicit, countably parametrized family. The family is broad (Equal Division, Winner-Takes-All, the "dollar at a time" rule of Example 1, and their concatenations along the endowment axis), so the theorem is the starting point for every sharper characterization in the paper: strengthening one axiom at a time selects WTA, ED or a Winner-Takes-Surplus rule (Corollaries 1–4), and the second and third missions of this series replace consistency by its local and top variants to obtain the single-parametric and parametric rules. Lemma 3 also isolates a general principle: a monotone consistent rule is determined by its behaviour on pairs.

On the formal side, Mathlib and the platform have no model of variable-population allocation with rankings. This mission provides one (competitions over a universe, subrankings, prize allocation rules and the consistency family of axioms) together with the first machine-checkable statement of a characterization theorem in this area. The paper's proofs are complete; nothing here is open mathematics, and none of it has been formalized before.

Difficulty

Consistency only constrains the rule across competitions; on its own it says nothing about how two competitors share a given endowment. The obvious plan, to read the intervals off the two-competitor allocation path and extend by Lemma 3, fails at the first step: an order preserving, monotone two-competitor path need not be a staircase of horizontal and vertical segments, and nothing about two competitors alone forces it to be. The staircase shape (Step 1) is a genuinely multi-competitor phenomenon that also relies on anonymity, which is not assumed and must be derived (Lemma 2, a six-case analysis over how two competitions share competitors). The countable family of intervals then has to be extracted from the path (Step 2), including endpoints at $+\infty$ and the gaps where the rule is equal division.

Formalization scope

A ranked set $(N, \mathcal R)$ is a duplicate-free nonempty List U, best first; $|N|$ is its length and $\mathcal R(i)$ = pos l i, the 1-based index. The subranking is the sublist of members of $S$ . A rule is a function φ : List U → ℝ → U → ℝ; its values on non-rankings, negative endowments and non-members are irrelevant, and every axiom and the interval-rule definition quantify only over rankings, $E \ge 0$ and $i \in N$ . The standing assumption on $U$ is carried as [Countable U] plus three distinct elements on every statement whose proof needs a third competitor (Lemma 2, Steps 1–2, Theorem 1, Corollaries 1–4); it is unnecessary for Lemmas 1, 3, 4 and for the "if" direction. Interval endpoints $b_k$ are extended reals (EReal), the intervals are indexed by $\mathbb N$ (finitely many intervals are padded with $a_k = b_k = 0$ ), $a_k \le b_k$ , and disjointness is of the open intervals. The four cases are implications; "otherwise" means $E \notin [n a_k, n b_k]$ for every $k$ .

The following formalizations would trivialize or change the theorem and are ruled out: a fixed competitor set or a finite $U$ of size two (consistency then has no reduced competitions to act on, and Corollary 1(i) fails); consistency restricted to two-element subsets or to some subsets only; a one-directional goal; interval rules without $+\infty$ endpoints (which excludes WTA and makes the "only if" direction false); and anonymity as an extra hypothesis.

The definitions are reusable by the two companion missions of this series (local and top consistency), which use the same model. Contributions welcome: proofs of the milestones, a general lemma that consistent monotone rules are determined by pairs, and proofs that ED, WTA and the Example 1 rule are interval rules.

Selected references

B. J. Dietzenbacher and A. Y. Kondratev, Fair and Consistent Prize Allocation in Competitions, arXiv:2008.08985v2, 2021; Management Science 69 (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), 195–213. https://doi.org/10.1016/0022-0531(85)90102-4
W. Thomson, A study of choice correspondences in economies with a variable number of agents, Journal of Economic Theory 46 (1988), 237–254. https://doi.org/10.1016/0022-0531(88)90131-7
T. Lensberg, Stability and the Nash solution, Journal of Economic Theory 45 (1988), 330–341. https://doi.org/10.1016/0022-0531(88)90274-8
S. Hart and A. Mas-Colell, Potential, value, and consistency, Econometrica 57 (1989), 589–614. https://doi.org/10.2307/1911054

9 thms3 active usersReviewed