Operations Research

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:

1. $\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);
2. 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$;
3. 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$;
4. Lemma 3: $\Phi_1(\lambda^\star)\le C\varepsilon K$, $K$ the number of steps;
5. 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]$;
6. Proposition 2: for the piecewise-linear path of eq. (9), $K=O(\log(1/\varepsilon)/\varepsilon^\beta)$;
7. 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);
8. $\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

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

1. Every equilibrium has at least two active miners (p. 38).
2. If miner $k+1$ is active in an equilibrium, so is miner $k$: the active miners are the $n$ cheapest (p. 38).
3. 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.$$

4. Summing (4.2) over the active miners (B.1): $(n-1)R-c^{(n)}H^*-\gamma (H^*)^2=0$.
5. 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}$$

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

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)

1. (B.2), first line: $\partial H^*/\partial c_i = -H^*/(c^{(n)} + 2\gamma H^*) < 0$.
2. (B.5): $R(c_i + \gamma g)/(R + \gamma g^2) = c_i + \gamma f_i$.
3. 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)$.
4. (B.4), first two lines: closed forms of $\partial h^*_i/\partial c_i$ and $\partial h^*_i/\partial c_j$.
5. 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$.
6. (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

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:

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

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)

1. Opening claim of the proof (p. 48). If every member of $\mathcal H$ outscores every member of $\mathcal M$, then $\mathbb T=H$ (deterministic).
2. 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}).$$

3. 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$.
4. (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}$.
5. (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

Motivation

A manufacturer that makes several products to stock for price-sensitive customers controls three levers at once: the prices it posts, which shape demand; outsourcing, which clears a large backlog at a cost; and scheduling, which decides which product the single server makes next. Ata and Barjesteh (Operations Research 71(1), 2023) study this multiclass make-to-stock queue in the heavy-traffic regime, where the queue is nearly saturated and the system is approximated by a Brownian control problem. The approximation collapses to a one-dimensional problem in the workload, the total amount of work in the system. Its solution is a two-barrier policy whose state-dependent drift translates back into a dynamic pricing rule, an outsourcing threshold and a scheduling priority (§7 of the paper).

The one-dimensional problem belongs to the family of drift-rate control problems for Brownian motion under a long-run average cost criterion (Ata, Harrison and Shepp, Ann. Appl. Probab. 2005; Rubino and Ata, Oper. Res. 2009). Problems of this kind are solved by a Bellman equation with free boundaries and a verification argument; the present paper adds two-sided singular control (outsourcing at the bottom, idling at the top) to a quadratic drift cost and a piecewise linear state cost.

Setting

There are $K\ge1$ products with mean production times $m_k>0$ and holding, backorder and outsourcing cost rates $h_k,b_k,r_k>0$. A symmetric positive definite matrix $H$ describes the curvature of the revenue rate. Write $a=m'H^{-1}m$ and

$$h^\star=\min_k\frac{h_k}{m_k},\qquad b^\star=\min_k\frac{b_k}{m_k},\qquad \kappa=\min_k\frac{r_k}{m_k}.$$

The drift cost and the effective holding cost are

$$c(x)=\min\{\zeta'H\zeta:\ m'\zeta=x\},\qquad h(w)=h^\star w\ (w\ge0),\quad h(w)=-b^\star w\ (w<0).$$

Let $B$ be a Brownian motion with drift $\mu\ge0$ and variance $\sigma^2>0$, started at $0$, with respect to a filtration $\mathbb F$. An admissible control consists of a progressively measurable drift rate $\theta$ and nondecreasing, right-continuous, adapted processes $L$ (effective outsourcing) and $U$ (idleness) with $L(0)=U(0)=0$. The workload is

$$W(t)=B(t)-\int_0^t\theta(s)\,ds-U(t)+L(t),$$

and admissibility also requires $\mathbb E|W(t)|/t\to0$. The equivalent workload formulation (EWF) is to minimize

$$\limsup_{t\to\infty}\frac1t\,\mathbb E\Big[\int_0^tc(\theta(s))\,ds+\int_0^th(W(s))\,ds+\kappa L(t)\Big]. \tag{29}$$

A barrier policy with barriers $l<u$ keeps $W$ in $[l,u]$, increases $L$ only when $W=l$ and $U$ only when $W=u$.

For $\gamma\ge0$ put $l_\gamma=-\frac1{b^\star}(\gamma+\mu\kappa+\frac a4\kappa^2)$ and $u_\gamma=\gamma/h^\star$. Let $v^-_\gamma$ solve the Riccati equation

$$v'=\frac a{2\sigma^2}(v^2-\kappa^2)-\frac{2\mu}{\sigma^2}(v+\kappa)+\frac{2(h(l_\gamma)-h(w))}{\sigma^2}\ \text{on }[l_\gamma,0],\qquad v(l_\gamma)=-\kappa,$$

and $v^+_\gamma$ solve $v'=\frac a{2\sigma^2}v^2-\frac{2\mu}{\sigma^2}v+\frac{2(h(u_\gamma)-h(w))}{\sigma^2}$ on $[0,u_\gamma]$ with $v(u_\gamma)=0$. The paper's $\gamma^\star$ is the unique $\gamma$ with $v^-_{\gamma}(0)=v^+_{\gamma}(0)$; $v$ pastes $v^-_{\gamma^\star}$ and $v^+_{\gamma^\star}$ at $0$, and the candidate drift is $\theta(w)=\frac a2v(w)$.

Formalization targets

Goal: Theorem 1

For every filtered probability space carrying such a Brownian motion,

$$\lim_{t\to\infty}\frac{J_{\text{cand}}(t)}t=\gamma^\star\quad\text{for every barrier policy at }(l_{\gamma^\star},u_{\gamma^\star})\text{ with drift }\theta(W),\qquad \limsup_{t\to\infty}\frac{J(t)}t\ge\gamma^\star\ \text{for every admissible control},$$

where $J$ is the expected cumulative cost in (29). The constant $\gamma^\star$ is the paper's construction, not a parameter.

Milestones

1. Lemma 1 and Lemma 2: the closed forms $c(x)=x^2/a$ and its conjugate $\varphi(y)=\frac a4y^2$, maximized at $\psi(y)=\frac a2y$.
2. Proposition 2: a barrier policy whose $(\gamma,f)$ solves the ODE (35)–(36) has long-run average cost $\gamma$.
3. Lemma 3: any solution of the Riccati-form Bellman equation (43)–(45) has $\gamma>0$, $l=l_\gamma<0$, $u=u_\gamma>0$.
4. Lemmas 18–20 and Corollary 6: sign and monotonicity of the Riccati solutions.
5. §6.3 well-posedness, Lemma 4(i)–(ii), Corollary 1: uniqueness of $v^\pm_\gamma$, their monotone dependence on $\gamma$, and the unique crossing $\gamma^\star$.
6. Proposition 3 and Corollary 2: $(l_{\gamma^\star},u_{\gamma^\star},\gamma^\star,v)$ is the unique solution of (43)–(45), and $f=\int v$ solves the Bellman equation (37)–(39), uniquely up to a constant.

Significance

The theorem identifies an explicit optimal policy for a two-sided singular drift-control problem: two barriers and a strictly increasing, non-positive drift, all determined by a scalar root $\gamma^\star$ of a monotone equation. In the paper it drives the proposed pricing, outsourcing and scheduling policy (§7) and its asymptotic analysis; the Riccati structure is what makes $\gamma^\star$ computable by line search.

The result is proved in the paper; none of it has been machine-checked. Formalizing it gives a checked verification theorem for an average-cost Brownian control problem with singular controls, and checked statements of the Riccati comparison lemmas on which it rests. Several printed statements of the paper are corrected here (see the scope section), so the formal versions are the first fully precise ones.

Difficulty

The optimality half of Theorem 1 is a verification argument: apply Itô's formula to $f(W(t))$ for an arbitrary admissible control with jumps in $L$ and $U$, use the Bellman inequality pointwise, and control $\mathbb E f(W(t))/t$ with the growth condition (32). Mathlib does not yet have Itô's formula for continuous semimartingales with finite-variation, possibly discontinuous parts, and the candidate's average cost (Proposition 2) needs the same tool plus the fact that a reflected diffusion spends zero time at the barriers.

The deterministic half is not routine either. The obvious reading of the paper, solving each Riccati problem for every $\gamma\ge0$ and passing $\gamma\to\infty$, fails: the solutions blow up in finite time, so $v^\pm_\gamma$ exist only for $\gamma$ in a bounded initial interval, and the crossing argument must be run on that interval. The comparison arguments of Lemmas 18–20 also need second derivatives of solutions whose right-hand side has a kink at $w=0$.

Formalization scope

Time is indexed by $\mathbb R$ and only $t\ge0$ matters. The Brownian motion is defined locally (drift, variance, start at $0$, independence of increments from the filtration). Expected costs are computed in $[0,\infty]$, so a control with infinite cost counts as $+\infty$. The integrals in (34) are Lebesgue–Stieltjes integrals against the paths of $L$ and $U$, jumps included. Derivatives at the barriers are one-sided; $C^1$ and $C^2$ up to the boundary are ContDiffOn on the closed interval. Minima and maxima (in $c$, (37), (40)) are stated as attained.

Standing assumptions added to every statement, all implicit in the paper: $K\ge1$; $m_k,h_k,b_k,r_k>0$; $H$ symmetric positive definite; $\mu\ge0$, $\sigma>0$; $B$ starts at $0$; $L,U$ right-continuous; $\theta$ progressively measurable with locally integrable paths; $l<u$ in the Bellman equations.

Corrected statements. Lemmas 18–20 are printed for solutions on $[0,\infty)$, which do not exist; they are posed on every bounded interval where a solution exists. The §6.3 claim that $v^\pm_\gamma$ exist for every $\gamma\ge0$ is replaced by uniqueness, solvability at $\gamma=0$ and order-connectedness of the solvability sets. Lemma 4's limits as $\gamma\to\infty$ become unboundedness on those sets. Theorem 1's comparison class is every admissible control, which the paper's proof treats, and which contains the stationary Markov policies to which §6 restricts attention.

Not posed. The existence of the reflected diffusion realizing the candidate policy is presupposed by the paper and not claimed: the first half of the goal quantifies over all barrier policies with the given data. The second half is a statement about every admissible control and is not vacuous.

$\gamma^\star$, $v$, $f$ and $\theta$ are built from the Riccati solutions by choice, exactly as the paper constructs them; taking them as hypotheses-constrained parameters, or defining $c$ by its closed form, would trivialize the goal and is ruled out. Contributions are welcome on the Riccati lemmas (pure real analysis, reusable for other drift-control problems), on Itô's formula for semimartingales with finite-variation parts, and on Skorokhod-type existence of reflected diffusions.

Selected references

• B. Ata and N. Barjesteh, An Approximate Analysis of Dynamic Pricing, Outsourcing, and Scheduling Policies for a Multiclass Make-to-Stock Queue in the Heavy Traffic Regime, Operations Research 71(1):341–357, 2023. https://doi.org/10.1287/opre.2022.2361 (accepted manuscript: https://ssrn.com/abstract=3464763)
• B. Ata, J. M. Harrison and L. A. Shepp, Drift rate control of a Brownian processing system, Annals of Applied Probability 15(2):1145–1160, 2005. https://doi.org/10.1214/105051604000000855
• M. Rubino and B. Ata, Dynamic control of a make-to-order, parallel-server system with cancellations, Operations Research 57(1):94–108, 2009. https://doi.org/10.1287/opre.1080.0532
• J. M. Harrison, Brownian Models of Performance and Control, Cambridge University Press, 2013. https://doi.org/10.1017/CBO9781139087698