Optimization

Motivation

Many outpatient clinics offer two ways in: an appointment booked online, and walk-in hours on the day. Some patients have no choice (acute cases arrive as walk-ins), but many can pick either channel, and they pick the one that costs them less: a long appointment delay pushes them into the walk-in room, a crowded walk-in room pushes them to book or to give up. A clinic deciding how to split its daily capacity between the two channels therefore faces a game, not a forecasting problem.

Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science 2023, doi:10.1287/mnsc.2023.4676) model this game and compare three operational levers: the capacity split, how much delay information the booking system reveals, and triage, that is, reserving walk-in hours for acute patients only (as some practices do, e.g. Centre Pediatrics 2021). This mission formalizes the triage comparison, Proposition 6 of the paper: closing walk-in hours to patients who could book pays off exactly when lost demand is cheap relative to overtime.

Setting

Patients. Exogenous walk-ins arrive at rate $\lambda_E$ and are always served on the day, possibly in overtime. Strategic patients arrive as a Poisson process of rate $\lambda>0$. A served patient gains $R>0$.

Capacity. The clinic has total capacity $\mu>0$ per day, split into appointment hours $\mu_S$ and walk-in hours $\mu_W=\mu-\mu_S$, with $\mu_S\in[0,\mu)$.

The appointment queue. Appointments form a single-server queue with deterministic service time $1/\mu_S$. In the observable setting a patient sees the queue: with $k$ patients waiting, the delay is $(k+\tilde u)/\mu_S$, $\tilde u$ uniform on $[0,1]$. A patient schedules when this delay is at most a threshold $\delta$, and scheduling at delay $d$ is worth $u^2_S(d)=R-C_D d$. The fraction of strategic patients who do not schedule is the blocking probability $\pi(\delta,\mu_S)$ of this M/D/1/K−1+p queue, where $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$. With $\rho=\lambda/\mu_S$ it has the closed form $\pi(\delta,\mu_S)=1-1/(q_0+\rho)$, where $q_0$ is built from the Poisson weights $\alpha_j=\rho^je^{-\rho}/j!$ by the Brun–Garcia recursion (Online Appendix C, (26)–(27), Corollary C.1). With no appointment hours, $\pi(\delta,0)=1$.

Walking in and balking. A patient who does not schedule walks in with probability proportional to $p_W$ or balks with probability proportional to $p_B$. Walking in is worth $u^2_W(p_W)=R-C_W\,w\big((\lambda_E+p_W\lambda)/\mu_W\big)$, with $w$ convex, strictly increasing and $w(0)=0$; balking is worth $0$. An observable equilibrium $(\delta,p_W,p_B)$ is a solution of conditions (6)–(10): the threshold $\delta$ makes scheduling at least as good as the walk-in/balk mixture up to $\delta$ and worse beyond it, $p_W+p_B=\pi(\delta,\mu_S)$, and patients walk in (balk) only if walking in is worth at least (at most) zero.

Costs. The provider pays $C_L$ per balking patient and $C_O\,o(\cdot)$ for overtime, with $o$ convex and strictly increasing. In the strategic model patients choose freely, and the cost at allocation $\mu_S$ and equilibrium $(\delta,p_W,p_B)$ is

$$Z^s=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big). \qquad\text{(Ob.P)}$$

In the triage model strategic patients may only schedule or balk, so they behave with threshold $R/C_D$ and

$$Z^t=C_L\,\pi(R/C_D,\mu_S)\,\lambda+C_O\,o\Big(\frac{\lambda_E}{\mu_W}\Big). \qquad\text{(T.Ob.P)}$$

Let $\underline\mu_W$ solve $R-C_W\,w(\lambda_E/\underline\mu_W)=0$ (15): below these walk-in hours the exogenous walk-ins alone make walking in worthless.

Formalization targets

Goal: Proposition 6

Suppose $\mu>\underline\mu_W$ and set

$$\underline\alpha=\frac{o'(\lambda_E/\mu)}{\mu},\qquad \overline\alpha=\frac{o'(\lambda_E/\underline\mu_W)}{\underline\mu_W}\max\Big\{\frac{\lambda_E}{\lambda\,\pi(R/C_D,\mu-\underline\mu_W)},1\Big\}.$$

Then

$$\frac{C_L}{C_O}\le\underline\alpha\ \Longrightarrow\ \inf Z^t\le\inf Z^s,\qquad \frac{C_L}{C_O}\ge\overline\alpha\ \Longrightarrow\ \inf Z^s\le\inf Z^t,$$

where the infima are over allocations $\mu_S\in[0,\mu)$ and, on the strategic side, over the equilibria at each allocation. The Lean statement says this without infima: every strategic configuration is matched by a triage allocation that costs no more, and every triage allocation is matched by a strategic allocation at which an equilibrium exists and every equilibrium costs no more.

Milestones

1. Proposition C.2 ($\mu_S$-part): $\mu_S\mapsto\pi(\delta,\mu_S)$ is continuous and strictly decreasing on $(0,\infty)$.
2. Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
3. Proposition 2 (1): if $\mu_W\le\underline\mu_W$, every equilibrium is schedule-and-balk, $p_W=0$, $\delta=R/C_D$, $p_B=\pi(R/C_D,\mu_S)$.
4. From the proof of part 1: $\lambda\,(1-\pi(\delta,\mu_S))\le\lambda\,(1-\pi(R/C_D,\mu_S))$ at every equilibrium.
5. From the proof of part 2: if nobody balks, $(\lambda p_W+\lambda_E)/\mu_W\le\lambda_E/\underline\mu_W$.
6. From the proof of part 2: if patients mix between walking in and balking, $(\lambda p_W+\lambda_E)/\mu_W=\lambda_E/\underline\mu_W$.

Significance

Proposition 6 turns a qualitative trade-off into two explicit thresholds on the ratio of the lost-demand cost to the overtime cost. Free choice reduces balking but lets strategic patients crowd the walk-in hours; triage removes that crowding at the price of more balking. The thresholds $\underline\alpha$ and $\overline\alpha$ depend only on the overtime function, the capacity and the blocking probability, so a clinic can evaluate them from its own data. The paper also shows (Remark 4, Appendix D.8) that the same insight holds in the unobservable setting, with capacity playing an additional role; that variant is not part of this mission.

The result is proved in the paper (Online Appendix E.3, pp. 35–37) and has no machine-checked proof. The formalization adds three things. It fixes the equilibrium concept precisely, including the mixture weights and the endpoint conventions. It states the comparison of optimal costs without presupposing that the optima are attained; the paper's proof begins "denote the optimal capacity allocations" without proving existence. And it ties the blocking probability to the paper's closed form, so the monotonicity in $\mu_S$ that the proof invokes becomes a statement about an explicit function rather than about a queue described in words.

Difficulty

The comparison itself is a chain of convexity inequalities at a single allocation. The hard part is the blocking probability. The paper proves that $\pi(\delta,\mu_S)$ decreases in $\mu_S$ by a sample-path argument on the queue, but a formal development has only the closed form, in which $K=\lceil\delta\mu_S\rceil$ jumps at every $\mu_S$ where $\delta\mu_S$ is an integer, $p$ jumps from $1$ to $0$ there, and $\rho=\lambda/\mu_S$ moves continuously. Monotonicity and continuity must be shown across these seams, through alternating sums whose terms cancel heavily. The obvious route, differentiating the closed form for fixed $K$, does not give the sign without a further structural argument on the coefficients $a_j$.

Existence of an equilibrium (milestone 2) is an intermediate-value argument in $\delta$, which in turn needs continuity of $\pi$ in $\delta$ and positivity of $\pi$.

Formalization scope

Everything lives in the namespace OutpatientWalkIn.Triage. The definition Queue contains the closed-form blocking probability blockProb lam δ μS; the definition Setting contains the model, the standing assumptions, the utilities, the equilibrium IsObsEq, the costs obsCost and triageCost, and the thresholds alphaLow, alphaHigh.

Conventions:

• Standing assumptions, hypotheses of every theorem: $\lambda>0$, $\lambda_E\ge0$, $R,C_D,C_W>0$, $C_L,C_O\ge0$, $\mu>0$; $w$ convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1); $o$ convex and strictly increasing on $[0,\infty)$ (Assumption 2).
• Allocations range over $\mu_S\in[0,\mu)$ on both sides, so that $\mu_W>0$; the paper's $\mu_S=\mu$ leaves the exogenous walk-ins with no walk-in hours.
• $\pi(\delta,0)=1$; the observable setting is defined directly (the paper's $C_G=0$).
• The equilibrium carries the guard $p_W+p_B>0$, which by (8) is $\pi(\delta,\mu_S)>0$ and excludes no equilibrium of the paper.
• Added hypotheses of the goal: $C_O>0$, $\lambda_E>0$, $\underline\mu_W>0$ given by (15), and differentiability of $o$ at $\lambda_E/\mu$ and $\lambda_E/\underline\mu_W$ (where $o'$ is evaluated). Without them Lean's $C_L/0=0$ and the zero derivative of a non-differentiable function would make $\underline\alpha=0$ and turn part 1 into a different claim.
• "Costs less" is "costs no more" (p. 26).

A formalization that compares the two models at one fixed allocation only, that lets the prover choose a cheap equilibrium when several might exist, or that replaces $\pi$ by an arbitrary decreasing function, is not the paper's theorem; the statements here rule these out.

Contributions welcome: properties of the closed-form $\pi$ (positivity, $\pi\le1$, monotonicity and continuity in both arguments), the existence of equilibria, and the convexity estimates of the final comparison. The queue file is reusable for any M/D/1/K model with partial joining.

Selected references

• N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, SSRN 3558209 (version of 2022-07-05); Management Science, 2023. https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
• O. Brun, J.-M. Garcia, Analytical solution of finite capacity M/D/1 queues, Journal of Applied Probability 37(4), 2000 (the source of the $a_j$ recursion, cited in the paper's Online Appendix C).
• P. Naor, The regulation of queue size by levying tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200

Motivation

Decoded quantum interferometry (DQI) is a quantum algorithm, introduced by Jordan, Shutty, Wootters, Zalcman, Schmidhuber, King, Isakov, Khattar and Babbush (arXiv:2408.08292), that turns an approximate optimization problem over a finite field into a decoding problem for a linear code. It applies to max-LINSAT: given linear constraints over $\mathbb F_p$, satisfy as many of them as possible. For structured instances such as optimal polynomial intersection the authors find DQI reaching approximation ratios that no known polynomial-time classical algorithm reaches, which makes it one of the few concrete candidates for a quantum advantage in optimization.

Whether DQI is useful on an instance depends on one number: the expected fraction of constraints satisfied by the string it outputs. Theorem 4.1 of the paper computes this number, in the limit of many constraints, for the best DQI state of a given degree. Every comparison of DQI with classical algorithms in the paper (simulated annealing, Prange's algorithm, the OPI and max-XORSAT benchmarks) is a comparison against this formula, and the follow-up analysis of imperfect decoders (Theorem 10.1) is a perturbation of it.

Setting

Fix a prime $p$. A max-LINSAT instance is a matrix $B\in\mathbb F_p^{m\times n}$ with rows $\mathbf b_1,\dots,\mathbf b_m$ and subsets $F_1,\dots,F_m\subseteq\mathbb F_p$; constraint $i$ asks that $\mathbf b_i\cdot\mathbf x\in F_i$ (Definition 2.1). Throughout, $m>n$ and every $F_i$ has the same size $r\in\{1,\dots,p-1\}$. Put $f_i(a)=+1$ if $a\in F_i$ and $-1$ otherwise, and

$$f(\mathbf x)=\sum_{i=1}^m f_i(\mathbf b_i\cdot\mathbf x),\qquad s(\mathbf x)=\#\{i:\mathbf b_i\cdot\mathbf x\in F_i\}.$$

For a real polynomial $P$ of degree at most $\ell$, the DQI state is $|P(f)\rangle=\sum_{\mathbf x\in\mathbb F_p^n}P(f(\mathbf x))|\mathbf x\rangle$, normalized so that $\sum_{\mathbf x}P(f(\mathbf x))^2=1$. Measuring it in the computational basis returns $\mathbf x$ with probability $P(f(\mathbf x))^2$, so the expected number of satisfied constraints is

$$\langle s\rangle=\sum_{\mathbf x}P(f(\mathbf x))^2\,s(\mathbf x),$$

and $\langle s^{(m,\ell)}\rangle_{\rm opt}$ is its supremum over all such $P$.

The dual code is $C^\perp=\{\mathbf d\in\mathbb F_p^m:B^T\mathbf d=0\}$ and $d^\perp$ is the least Hamming weight of a nonzero codeword. The condition $2\ell+1<d^\perp$ says that syndromes of errors of weight up to $\ell$ (and a little more) determine the error.

The analysis passes through rescaled constraint functions $g_i=(f_i-\bar f)/\varphi$ with Fourier transforms $\tilde g_i$, the elementary symmetric polynomials $P^{(k)}$ evaluated at the $g_i(\mathbf b_i\cdot\mathbf x)$, and the $(\ell+1)\times(\ell+1)$ symmetric tridiagonal matrix $A^{(m,\ell,d)}$ with diagonal $0,d,2d,\dots,\ell d$ and off-diagonal entries $a_k=\sqrt{k(m-k+1)}$, at $d=(p-2r)/\sqrt{r(p-r)}$.

Formalization targets

Goal: Theorem 4.1 (the semicircle law)

Fix $p$, $r$ and $\mu\ge0$. For any sequence of instances with $m\to\infty$, $\ell/m\to\mu$ and $2\ell+1<d^\perp$, writing $\rho=r/p$,

$$\lim\frac{\langle s^{(m,\ell)}\rangle_{\rm opt}}{m}=\begin{cases}\big(\sqrt{\mu(1-\rho)}+\sqrt{\rho(1-\mu)}\big)^2,&\rho\le1-\mu,\\ 1,&\text{otherwise.}\end{cases}$$

For $\rho=\tfrac12$ the curve is $\tfrac12+\sqrt{\mu(1-\mu)}$, a semicircle, which gives the theorem its name.

Milestones

1. The normalization of the rescaled $g_i$, (37)–(40).
2. Lemma A.1: under a common quadratic identity, $P(x_1+\dots+x_m)$ is a fixed linear combination of elementary symmetric polynomials.
3. The counting identity (68), $\sum_{|\mathbf y|=k}|\tilde g(\mathbf y)|^2=\binom mk$, and the Fourier picture (65) of the DQI state.
4. Lemma 9.1 (norm $=\|\mathbf w\|^2$ when $2\ell<d^\perp$) and Lemma 9.2 (the expected count is $\frac{mr}p+\frac{\sqrt{r(p-r)}}p\mathbf w^TA^{(m,\ell,d)}\mathbf w$ when $2\ell+1<d^\perp$).
5. The finite-size identity (131): $\langle s^{(m,\ell)}\rangle_{\rm opt}/m=\rho+\sqrt{\rho(1-\rho)}\,\lambda_{\max}^{(m,\ell,d)}/m$.
6. Lemma 9.3, $\lambda_{\max}^{(m,\ell,d)}/m\to\mu d+2\sqrt{\mu(1-\mu)}$, with its lower half (114) and the Gershgorin bound (129).
7. The algebra (132) and (136)–(137) that produce the closed form.

Significance

The result. Theorem 4.1 makes DQI's performance a closed-form function of two numbers, $r/p$ and $\ell/m$, and moves every question about an instance into coding theory: how large a $d^\perp$ the instance's dual code has, and whether it can be decoded efficiently up to $\ell$ errors. The OPI advantage claim of the paper, the comparison with Prange's algorithm on max-XORSAT, and the imperfect-decoding bound of Theorem 10.1 all start from this formula. The finite-size identity (131) is also useful on its own: it gives the exact optimum for any instance, not only in the limit.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization would check the Fourier bookkeeping of §8.2.1 and §9 (normalizations $\sqrt{p^{n-k}\binom mk}$, character sums over $\mathbb F_p$), the claim that every degree-$\ell$ DQI state is a combination of the $|P^{(k)}\rangle$ and conversely, and the eigenvalue asymptotics of the tridiagonal matrix. Two points of the printed text need care and are stated correctly here: Lemma 9.2 writes its decomposition in the $f_i$ where the normalization requires the rescaled $g_i$, and the "otherwise $=1$" branch of Theorem 4.1 is argued only briefly on p. 34.

Difficulty

The algebraic steps are finite but long, and every one carries a normalization that a careless formalization gets wrong. The asymptotic step is the main obstacle. Lemma 9.3 needs a lower bound on $\lambda_{\max}$ from a test vector of growing width and a matching upper bound from Gershgorin's theorem, and the upper bound holds only under $d\ge-(m-2\ell)/\sqrt{\ell(m-\ell)}$, which is exactly the regime $\rho\le1-\mu$. In the other regime that hypothesis fails and the Gershgorin bound overshoots, so the limit $1$ needs a separate argument; the observation that $\langle s\rangle_{\rm opt}$ "increases in $r$", printed on p. 34, does not give it at fixed $p$ and $r$. A second difficulty is that $\langle s\rangle_{\rm opt}$ is a supremum over polynomials, while Lemma 9.2 is a statement about weight vectors $\mathbf w$; identifying the two needs both directions of Lemma A.1's correspondence and the normalization of Lemma 9.1.

Formalization scope

All objects live in the namespace DQI.Semicircle and one definitions file. $\mathbb F_p$ is ZMod p with [Fact p.Prime]; vectors are Fin n → ZMod p; constraints are indexed by Fin m from $0$. $\omega_p^a=\exp(2\pi i\,a/p)$ is computed from the representative of $a$ in $\{0,\dots,p-1\}$. Polynomials are real with natDegree ≤ ℓ; weight vectors are real. The optimum $\langle s\rangle_{\rm opt}$ is the real supremum over exactly the normalized polynomials of degree at most $\ell$ evaluated at $f(\mathbf x)$; its set is nonempty (constant polynomials) and bounded by $m$. The dual-distance condition is "every nonzero $\mathbf d$ with $B^T\mathbf d=0$ has weight $>t$"; $d^\perp$ is never an infimum, and $m>n$ (the paper's standing assumption) guarantees a nonzero codeword, so the condition forces $2\ell<m$. $\lambda_{\max}$ is the supremum of the real spectrum. The limit "$m\to\infty$ with $\ell/m$ fixed" is any sequence of instances with $m_j\to\infty$ and $\ell_j/m_j\to\mu$, with $p$ and $r$ fixed along it. Convergence of the ratio includes irrational $\mu$ with integer sizes.

Added hypotheses, all disclosed in the items: Lemma 9.2 decomposes in the $g_i$ rather than the printed $f_i$; (129) assumes $\ell\ge1$ to avoid dividing by $\sqrt0$; Lemma 9.3 imposes its hypothesis on $d$ only when $\ell_j\ge1$; (114) is stated as a $\liminf$ with an explicit $\varepsilon$.

A formalization that replaces $\langle s\rangle_{\rm opt}$ by a supremum over all states (which gives $1$), drops "nonzero" from the distance condition (which makes it unsatisfiable), or states the goal at a single $m$ is not this theorem and is ruled out by the definitions above.

Needed infrastructure: Fourier analysis on $\mathbb F_p^n$ (character orthogonality, Parseval), elementary symmetric polynomials and their reduction modulo a quadratic, Rayleigh quotients and Gershgorin discs for real symmetric matrices, and elementary limits. The tridiagonal-matrix bounds and the quadratic-reduction lemma are reusable beyond DQI. Proofs of any milestone, alternative arguments for the "otherwise" branch, and sharper finite-$m$ bounds on $\lambda_{\max}$ are welcome.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025. https://arxiv.org/abs/2408.08292
• S. Gershgorin, Über die Abgrenzung der Eigenwerte einer Matrix, Izv. Akad. Nauk SSSR, Ser. Fiz.-Mat. 6, 749–754, 1931.
• R. G. Gallager, Low-Density Parity-Check Codes, IRE Trans. Inform. Theory 8(1), 21–28, 1962. https://doi.org/10.1109/TIT.1962.1057683

Motivation

Every Bitcoin transaction recorded on the blockchain pays a fee, and the blockchain processes only a few transactions per second. The Lightning Network is a layer-two protocol that moves repeated payments off chain: two parties lock funds in a payment channel, exchange payments by updating the channel's balance, and touch the blockchain only to open, close or reset the channel. Whether a channel is worth opening is an economic question. Locked funds forgo interest, and a channel whose balance is exhausted must be reset on chain at a cost.

Guasoni, Huberman and Shikhelman (Management Science, 2023) model this trade-off with Poisson payment streams and continuous discounting, and obtain closed-form channel costs (their Theorem 1). Their Theorem 2 turns those costs into necessary conditions: a channel can be cheaper than settling every payment on chain only if the on-chain fee exceeds an explicit threshold depending on the reset cost, the payment rate and the interest rate. This mission formalizes Theorem 2, its two proofs, and the on-chain benchmark (Lemma 1) against which every channel is measured.

Setting

Node 1 pays node 2 one unit at the jumps of a Poisson process with rate $\lambda_1$, and node 2 pays node 1 at the jumps of an independent Poisson process with rate $\lambda_2$. The discount rate $r>0$ is the opportunity cost of capital per unit of time, $B$ is the cost of resetting a channel, and $C$ is the cost of one on-chain transaction. Node $i$ commits the amount $l_i$ to the channel.

On-chain settlement. If every payment of a stream with rate $\lambda$ is settled on chain, the expected discounted cost is $\mathbb E\big[\sum_{n\ge1}e^{-r\tau_n}C\big]=C\lambda/r$, where $\tau_n$ is the $n$-th arrival time (Lemma 1). Two streams of rate $\lambda$ cost $2C\lambda/r$.

Unidirectional channel. If only one node pays, at rate $\lambda$, a channel of size $m$ costs (Theorem 1(i), equation (1))

$$\mathrm{uniCost}(m)=m+B\Big(\big(\tfrac{r+\lambda}{\lambda}\big)^{m}-1\Big)^{-1}.$$

Bidirectional channel. With

$$\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}$$

(equation (4)), a channel with sizes $l_1,l_2$ costs $\mathrm{biCost}(l_1,l_2)$, the expression (3) in $\alpha_\pm^{l_1}$, $\alpha_\pm^{l_2}$ and $\alpha_\pm^{l_1+l_2}$. In the symmetric case $\lambda_1=\lambda_2=\lambda$ it simplifies, with $\alpha=\alpha_+$, to

$$l_1+l_2+\frac{B(\alpha^{l_1}+\alpha^{l_2})}{(\alpha^{l_1}-1)(\alpha^{l_2}-1)}.$$

A channel costs less than on-chain transactions if, for some size, its cost is strictly below the on-chain cost of the streams it carries.

Formalization targets

Goal: Theorem 2

For $B,r,\lambda>0$ and any fee $C$:

1. if $\mathrm{uniCost}(m)<\lambda C/r$ for some $m>0$, then

$$C>\log\Big(1+B\log\big(1+\tfrac r\lambda\big)\Big);\tag{5}$$

2. if $\mathrm{biCost}(l_1,l_2)<2C\lambda/r$ for some $l_1,l_2>0$ with $\lambda_1=\lambda_2=\lambda$, then

$$C>3\Big(\frac{B\kappa^4}{4}\Big)^{1/3}-\frac B{12}\kappa^2,\qquad \kappa=\log\frac{r+2\lambda+\sqrt{r(4\lambda+r)}}{2\lambda}.\tag{6}$$

Milestones

• Lemma 1: the on-chain cost $C\lambda/r$.
• Part (i) chain: the change of variable $\kappa=\log(1+r/\lambda)$ that turns the excess cost into $F(m)=C/(1-e^\kappa)+B/(e^{\kappa m}-1)+m$; the unique minimizer $\hat m=\cosh^{-1}(B\kappa/2+1)/\kappa$ and the minimum value; inequality (16); the sufficient condition (17)–(20) for on-chain settlement to be strictly cheaper; Theorem 2(i).
• Part (ii) chain: the symmetric cost and $\lambda/r=\alpha/(\alpha-1)^2$; the reduction (21) to equal sizes; the hyperbolic form and the bounds $1/x^2-1/3<\operatorname{csch}^2x<1/x^2$ of (22); the minimization (24) of the lower bound (23); Theorem 2(ii).
• Expansions: the right-hand sides of (5) and (6) equal $Br/\lambda+o(r)$ and $3(Br^2/(4\lambda^2))^{1/3}-Br/(12\lambda)+o(r)$ as $r\to0^+$.

Significance

Theorem 2 gives the qualitative conclusion of the paper in quantitative form: channels pay off only when on-chain fees are high, reset costs low, payment rates high, or interest rates low. Read as a contrapositive, it says that below the thresholds, settling on chain is at least as cheap for every channel size, so no optimization over sizes is needed to rule a channel out. The expansions show the two thresholds scale differently in the interest rate, linearly for a unidirectional channel and as $r^{2/3}$ for a symmetric bidirectional one. The paper's subsequent asymptotic results (Theorem 3) rely on the same reductions.

The theorem is proved in the paper; nothing here is open. To our knowledge none of it is formalized. A formalization adds a machine-checked verification of a proof that contains several informal steps: a minimizer of a two-variable function is assumed to exist, two inequalities are stated non-strictly where strict ones are needed, and one sentence states an "if and only if" with $\le$ where $<$ is meant. Lemma 1 also requires the discounted sum over a Poisson process to be integrable, which the paper's renewal argument takes for granted.

Difficulty

The bidirectional cost (3) is a ratio of differences of real powers of two algebraic numbers, and its minimum over two sizes has no closed form, so the threshold cannot be read off an explicit optimum. The paper replaces the optimum by reductions whose rigorous versions are the substance of the work: the passage from (3) to the symmetric form, the reduction of a two-variable minimization to the diagonal (asserted in the paper through a Hessian computation and the existence of a minimizer, neither of which is carried out), and a lower bound on $\operatorname{csch}^2$ that holds on all of $(0,\infty)$ and is not in Mathlib. The obvious approach of bounding the cost at its minimizer fails for the same reason it fails on paper: no minimizer is given. For part (i), the minimizer involves $\cosh^{-1}$, and the minimal value still depends on $C$ through two terms, so a condition on $C$ alone does not follow by rearrangement. Lemma 1 requires an exchange of expectation and infinite sum over a Poisson process, which the paper's renewal argument assumes.

Formalization scope

• Costs as closed forms for real sizes. uniCost and biCost are the paper's expressions (1) and (3) with real sizes and real powers (Real.rpow). Theorem 2's proofs minimize over real sizes, and the hypotheses quantify over real sizes, so the statements imply their versions for natural sizes. The probabilistic derivation of (1) and (3) from the balance random walk is the subject of the sibling mission Channels I.
• Explicit on-chain costs. The comparisons are with $\lambda C/r$ and $2C\lambda/r$, written out; there is no opaque on-chain cost function.
• Strict and existential. "Costs less" is strict and asserted for some size; the conclusions on $C$ are strict. No sign is imposed on $C$; $B,r,\lambda>0$.
• Lemma 1 uses the published definition QueueingFundamentals.Foundations.IsExpInterarrivals of i.i.d. exponential interarrival times; the conclusion asserts integrability as well as the value $C\lambda/r$.
• Corrections recorded in the statements. (17)–(20) is stated with the strict conclusion $F>0$ that (17) gives, for all $m>0$; (21) is stated in midpoint form, $H(m,m)\le H(l_1,l_2)$ for $m=(l_1+l_2)/2$, which requires no minimizer.
• Two different $\kappa$. In part (i) $\kappa=\log(1+r/\lambda)$; in part (ii) $\kappa=\log\alpha_+$. They are never identified.
• Asymptotics are little-o along $r\to0^+$ (𝓝[>] 0) with $B$ and $\lambda$ fixed.

Ruled out as trivializing: fixing $B$, $r$ or $\lambda$; restricting to natural sizes without saying so; an existentially chosen $\kappa$; weakening either strict inequality; or an on-chain cost under which the comparison is vacuous.

Needed infrastructure: real-power calculus and convexity on $(0,\infty)$, $\cosh^{-1}$ and $\sinh$ bounds, little-o expansions of $\log$ and $\cosh^{-1}$ near their base points, and the Laplace transform of Gamma laws for Lemma 1. The csch inequality (22) and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome independently.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, published online Nov. 6, 2023, pp. 1–14. https://doi.org/10.1287/mnsc.2022.01664
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, technical report, 2016. https://lightning.network/lightning-network-paper.pdf
• G. Huberman, J. D. Leshno, C. Moallemi, Monopoly without a Monopolist: An Economic Analysis of the Bitcoin Payment System, Review of Economic Studies 88(6), 2021. https://doi.org/10.1093/restud/rdab014

Motivation

Proof-of-work blockchains such as Bitcoin pay a block reward to the miner that first solves a computational puzzle. The chance of winning is proportional to a miner's share of the total computing power (hash rate), so mining is a contest in which every miner pays for hash rate and the reward is split in proportion to it. Over time mining moved from general-purpose hardware to specialized chips, and this raised the question of whether access to better hardware concentrates mining in a few hands, which would weaken the decentralization the protocol relies on for security. Arnosti and Weinberg (arXiv:1811.08572) showed that cost asymmetries alone already concentrate mining in a proportional-share contest.

Capponi, Ólafsson and Alsabah (arXiv:2106.09783v1, 2021; published in Management Science, 2023) model this as a two-stage game. Miners first decide how much to invest in the newest hardware, which lowers their cost per unit of hash rate. They then compete in the mining stage. Their Proposition 5.1 describes the equilibrium of the investment stage: which miners invest, how much, and how the number of active miners depends on the fixed cost of entering. This mission formalizes that result, corrected where the printed statement is false.

Setting

There are $N\ge2$ miners. Miner $i$ starts with a cost-per-hash $\tilde c_i$, sorted so that $\tilde c_1\le\dots\le\tilde c_N$. The newest hardware has cost-per-hash $\tilde c_0$, with $0<\tilde c_0<\tilde c_i$ for every $i$. In the first stage miner $i$ replaces a fraction $\beta_i\in[0,1]$ of its hardware, which leaves it with cost-per-hash

$$c_i(\beta_i)=\tilde c_i-\beta_i(\tilde c_i-\tilde c_0)+\frac{\eta(\tilde c_i-\tilde c_0)}{2}\beta_i^2,$$

where $\eta\ge0$ measures adjustment costs ((3.1)–(3.2)). Write $\bar\beta=\min\{1/\eta,1\}$, read as $1$ when $\eta=0$.

In the second stage, the mining stage, miner $i$ chooses a hash rate $h_i\ge0$. With $H=\sum_jh_j$, its payoff is

$$\pi_i=\frac{h_i}{H}R-c_ih_i-\frac{\gamma}{2}h_i^2-K\,\mathbf 1\{i\notin A(0),\ \beta_i>0\}\quad(H>0),\qquad \pi_i=0\quad(H=0),$$

with reward $R>0$, capacity parameter $\gamma\ge0$ and fixed entry cost $K>0$ ((3.4)). An equilibrium hash rate profile $h^*(\beta)$ is a profile from which no miner gains by changing its own hash rate (Definition 3.2(i)). Proposition 4.1 of the paper shows that it exists and is unique, and posing that result is the subject of mission 1 of this series. The active set is $A(\beta)=\{i:h^*_i(\beta)>0\}$, and $A(0)$ is the set of miners active without investment. The entry cost $K$ is paid by a miner outside $A(0)$ that invests.

An equilibrium investment $\beta^*\in[0,1]^N$ is a profile from which no miner can raise its payoff by changing $\beta_i$, the mining stage being replayed at the new profile (Definition 3.2(ii)). The threshold profile $\beta^{(n)}$ invests $\bar\beta$ in miners $1,\dots,n$ and $0$ in the others; this is the form (5.1).

Formalization targets

Goal: Proposition 5.1, corrected

Assume $K$ is generic: no potential entrant's gross mining profit at $\beta^{(i)}$ equals $K$. Then:

1. there is exactly one $n\in\{2,\dots,N\}$ for which $\beta^{(n)}$ is an equilibrium investment, and at it exactly $n$ miners are active and $A(0)\subseteq A(\beta^{(n)})$;
2. every equilibrium investment $\beta^*$ satisfies $A(0)\subseteq A(\beta^*)$ and $\beta^*_i=\bar\beta$ for every $i\in A(0)$;
3. $n$ is nonincreasing in $K$:

$$K\le K'\ \Longrightarrow\ n(K')\le n(K).$$

Milestones

• Proposition B.1: at a fixed set of $n$ active miners, $\partial\pi^*_i/\partial c_i<0$ and $\partial\pi^*_i/\partial c_j>0$.
• (5.2): the cost reduction $c_i(0)-c_i(\bar\beta)$ equals $(\tilde c_i-\tilde c_0)/(2\eta)$ for $\eta>1$ and $(1-\eta/2)(\tilde c_i-\tilde c_0)$ for $\eta\le1$, and $\bar\beta$ uniquely minimizes $c_i$ on $[0,1]$.
• Best responses (p. 44): at every equilibrium investment, active miners invest $\bar\beta$ and inactive ones invest $0$.
• Order preservation (p. 45): for $\eta>0$, investing $\bar\beta$ preserves the strict order of costs.
• Participation at $|A(0)|$ (p. 45): after miners $1,\dots,|A(0)|$ invest, the participation inequality of Proposition 4.4 holds for miner $|A(0)|$.

Significance

The result says three things about the effect of hardware upgrades on decentralization. Incumbents never drop out: every miner active before investment invests the cost-minimizing amount and stays active. Entry is ordered: in the threshold equilibrium the miners that enter are the most efficient ones. A higher fixed cost of entry admits weakly fewer miners. The paper's later propositions (5.2–5.5), which describe how hash rates and shares move after investment, start from this equilibrium.

Formalizing it adds two things. First, a machine-checked statement of what is actually true. The printed uniqueness is false, and the corrected statement separates what holds for every equilibrium from what holds within the threshold family. Second, a formal two-stage game in which the second stage is replayed at every deviation of the first, through an explicit equilibrium selection. None of the results of the paper has been formalized before; the platform has no contest or rent-seeking game.

Difficulty

The printed proof argues that an active miner's profit decreases in its own cost "irrespective of the cost parameters of other miners", citing Proposition B.1. Proposition B.1 is a derivative at a fixed set of active miners. Investment can change that set, so the proof needs a global monotonicity of the equilibrium profit across changes of the active set, in the own cost and in the presence of rivals. That step is not in the paper.

The obvious uniqueness argument also fails. Take two potential entrants with nearly equal initial costs and room in the market for only one of them. Either one can enter while the other stays out, and both profiles are equilibria. The numbers are $\tilde c=(1.074,1.419,2.914,2.923)$, $\tilde c_0=0.31$, $\eta=0.5$, $\gamma=0.5$, $R=1$ and any $K\in(0.0168,0.0308)$: both $(1,1,1,0)$ and $(1,1,0,1)$ are equilibrium investments. So no proof can rest on "a miner never invests while a cheaper one does not", which the paper asserts on p. 45.

Formalization scope

Miners are Fin N and 0-based: Lean miner i is the paper's miner $i+1$. Hash rates, costs and parameters are real numbers. The mining stage is defined for an arbitrary cost vector, not assumed sorted, because investment can reorder costs. The equilibrium property "$=\sup$" is written as "no deviation is profitable", over $h_i\ge0$ and over $\beta_i\in[0,1]$. The mining equilibrium enters as a selection $h^*$ with the hypothesis that $h^*(\beta)$ is an equilibrium hash rate profile for every $\beta\in[0,1]^N$. Proposition 4.1 makes it unique; it is not defined by a closed form. The fixed cost enters only the investment stage, inside the $H>0$ branch of (3.4). Derivatives are HasDerivAt statements along one coordinate. "Decreasing" is weak, as in the paper's footnote 12.

The goal is the corrected Proposition 5.1. The printed uniqueness among all investment profiles is not posed, and neither is the p. 45 claim that a miner cannot invest while a cheaper miner does not. Both are false by the instance above. Three hypotheses are added to the paper's: $\tilde c_0>0$; $\tilde c_0<\tilde c_i$ for every $i$ (the paper allows equality, under which $c_i$ is constant and every $\beta_i$ is a best response); and the genericity of $K$, which excludes finitely many values. Without the selection hypothesis the goal would be about an arbitrary function. Without the existence in part 1 the "every equilibrium" clause could be vacuous. Both are in the statement, so neither trivialization is available.

A complete development needs the mining-stage results of mission 1 of this series: existence and uniqueness of the mining equilibrium (Proposition 4.1) and the participation condition (Proposition 4.4). Since one draft cannot import another, this mission redefines the mining stage in its own namespace PoWMining.Investment. The new work is a global comparative-statics argument for the mining equilibrium across changes of the active set. It is reusable for any proportional-share contest with convex costs. Contributions are welcome on the milestones in any order, on that global monotonicity, and on the existence half of part 1.

Selected references

• A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint arXiv:2106.09783v1, 2021 (Proposition 5.1 p. 21, proofs pp. 43–46). https://arxiv.org/abs/2106.09783v1
• N. Arnosti, S. M. Weinberg, Bitcoin: A Natural Oligopoly, Innovations in Theoretical Computer Science (ITCS), 2019. https://arxiv.org/abs/1811.08572

Motivation

Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.

A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter $\gamma$, which measures how quickly a miner's operating cost grows with its scale, and the mining reward $R$. The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.

Setting

There are $n \ge 2$ active miners, indexed $i = 1, \dots, n$, with costs per hash $0 < c_1 \le c_2 \le \dots \le c_n$ (sorted, without loss of generality), a reward $R > 0$ and a capacity parameter $\gamma > 0$. Miner $i$ choosing hash rate $h_i$ earns $(h_i/H)R - c_ih_i - (\gamma/2)h_i^2$, where $H = \sum_j h_j$ is the aggregate hash rate (the paper's (3.4)). The cumulative cost is $c^{(n)} = c_1 + \dots + c_n$.

In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of $\gamma H^2 + c^{(n)}H - (n-1)R = 0$, and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:

$$g = g(c_1,\dots,c_n,\gamma,R) = \frac{\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} - c^{(n)}}{2\gamma},\qquad f_i = f_i(c_1,\dots,c_n,\gamma,R) = g\,\frac{R - c_i g}{R + \gamma g^2},$$

with $H^* = g$ and $h^*_i = f_i$. Miner $i$ is active exactly when $R - c_i g > 0$. The hash rate share of miner $i$ is $h^*_i/H^*$.

The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For $x \in \{\gamma, R\}$, (B.4) splits the derivative of $h^*_i$ into a direct part, $\Delta^{(x)}_{i,1} = \partial f_i/\partial x$ with $g$ held fixed, and an indirect part through the aggregate, $\Delta^{(x)}_{i,2} = (\partial f_i/\partial g)(\partial g/\partial x)$.

Formalization targets

Goal: Proposition 4.8 (p. 20)

For every active miner $i$,

$$\frac{\partial h^*_i}{\partial\gamma} = \Delta^{(\gamma)}_{i,1}+\Delta^{(\gamma)}_{i,2},\quad \Delta^{(\gamma)}_{i,1}<0,\quad \Delta^{(\gamma)}_{i,2}>0 \iff \frac{h^*_i}{H^*}<\frac12,$$ $$\frac{\partial h^*_i}{\partial R} = \Delta^{(R)}_{i,1}+\Delta^{(R)}_{i,2} > 0,\quad \Delta^{(R)}_{i,1}>0,\quad \Delta^{(R)}_{i,2}<0 \iff \frac{h^*_i}{H^*}<\frac12,$$

and the derivatives of $h^*_i/H^*$ with respect to $\gamma$ and to $R$ are increasing in $i$, for $1 \le i \le n$.

Milestones (the steps of the appendix proof)

1. (B.2), p. 39: $\partial H^*/\partial\gamma = -(H^*)^2/(c^{(n)}+2\gamma H^*) < 0$ and $\partial H^*/\partial R = (n-1)/(c^{(n)}+2\gamma H^*) > 0$.
2. p. 40: $\partial f_i/\partial\gamma = -g^3(R-c_ig)/(R+\gamma g^2)^2 < 0$ and $\partial f_i/\partial R = g^2(c_i+\gamma g)/(R+\gamma g^2)^2 > 0$.
3. (B.4), pp. 40–41: closed forms of $\partial h^*_i/\partial\gamma$ and $\partial h^*_i/\partial R$.
4. (B.6), pp. 42–43: closed forms of the share derivatives, and the p. 43 rewrites in which $i$ enters only through $f_i$ and $c_i + \gamma f_i$.

Significance

The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger $\gamma$ lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the $\gamma$ and $R$ columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).

Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the $\gamma$ and $R$ directions, the sign analysis, and the monotonicity in $i$. The proof text on p. 43 says "decreasing in $i$" where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).

Difficulty

Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate $g$ is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity $\gamma g^2 + c^{(n)}g = (n-1)R$, i.e. $\sqrt{(c^{(n)})^2+4(n-1)R\gamma} = c^{(n)} + 2\gamma g$, and the first-order identity $c_i + \gamma f_i = (R/g)(1 - f_i/g)$. The sign of the indirect parts is not visible from the raw derivative: it requires rewriting $\partial f_i/\partial g$ so that the threshold $f_i/g = 1/2$ appears. The positivity of $\partial h^*_i/\partial R$ needs a separate bound, since its indirect part can be negative. The monotonicity in $i$ is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on $f_i$ (decreasing in $i$) from that on $c_i + \gamma f_i$ (increasing in $i$), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.

Formalization scope

Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner $i+1$, so "increasing in $i$" is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost ($c^{(n)}$), gH ((4.1)/(B.3), with both branches of (4.1)), fH ($f_i$ with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: $n\ge2$, $R>0$, $\gamma>0$, $c_k>0$, costs sorted, and $R - c_kg > 0$ for every $k$ (all $n$ miners active). The condition $\gamma > 0$ is the paper's: (B.3) defines $g$ only for $\gamma>0$. The definition Sensitivities defines the four $\Delta$'s as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.

The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That $f_i$ and $g$ are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and $\partial f_i/\partial g$ are posed in mission 2. This mission uses those identities but does not pose them.

Trivializing formalizations are ruled out: the $\Delta$'s are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with $c = (1,1)$, $\gamma = 1$, $R = 3$ give $g = 1$, $h^*_i = 1/2$); and the monotonicity is stated for derivatives asserted to exist.

Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for $g$ (the root identity, positivity, $c^{(n)}+2\gamma g > 0$) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.

Selected references

• A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint, 2021. https://arxiv.org/abs/2106.09783v1
• G. Tullock, The Welfare Costs of Tariffs, Monopolies, and Theft, Western Economic Journal 5(3), 224–232, 1967 (the rent-seeking model the paper builds on). https://doi.org/10.1111/j.1465-7295.1967.tb01923.x
• S. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. https://bitcoin.org/bitcoin.pdf

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 9 (p. 17)

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Selected references

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