Operations Research

Why the topology of payment-channel networks matters

The Lightning Network (LN) is a second-layer payment system for Bitcoin. Instead of recording every payment on the blockchain, two parties lock funds in a payment channel and settle many payments off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it carries. Which channel topology supports a given pattern of payments at least total cost is therefore an economic design question for the network's participants.

Guasoni, Huberman and Shikhelman (SSRN 4439190, 2023; published in Management Science, 2024) study this question for a general cost function, assuming only a few qualitative properties derived in their earlier work on channel economics ([GHS22], Lightning Network Economics: Channels). This mission covers §3.1 of the paper, local channel reconfiguration: a relaying node can be bypassed at lower cost, odd cycles are never optimal, and a cost-minimizing network is bipartite with every net flow going from one side to the other. Three companion missions (II–IV of this series) cover hermetization by a routing hub (§3.2) and bounds on the global minimal cost (§3.3).

Setting

Let $V$ be a finite set of nodes. A payment flow is a vector $F=(f_i)_{i\in V}$ of net flows with $\sum_i f_i=0$. A Lightning Network on $V$ is an anti-symmetric real matrix $\Lambda=(\lambda_{u,v})_{u,v\in V}$, $\lambda_{u,v}=-\lambda_{v,u}$, where $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them and $\lambda_{u,v}=0$ means there is no channel. The network supports $F$ if

$$\sum_{j\in V}\lambda_{i,j}=f_i\qquad\text{for every } i\in V .$$

A channel cost function is $c:\mathbb R\to\mathbb R_{\ge0}$ with

• (MO) $c(x)>c(y)$ for $x>y\ge 0$;
• (SY) $c(-x)=c(x)$;
• (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for $x,y>0$.

The cost of a network is $c(\Lambda)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$, the sum of $c$ over its channels. A network is cost-minimizing for $F$ if it supports $F$ and no Lightning Network on the same node set $V$ that supports $F$ has smaller cost.

The paper's channel notation: $\overrightarrow{uv}^{\lambda}$ is a channel with net flow $\lambda$ from $u$ to $v$, and ${}^{a}\overleftrightarrow{xy}^{b}$ is a channel in which $y$ sends $a$ and $x$ sends $b$, so the net flow from $x$ to $y$ is $b-a$.

Formalization targets

Goal: Corollary 3.3

If $\Lambda$ is cost-minimizing for $F$, there is a set $A\subseteq V$ with $B=V\setminus A$ such that the channel graph ($i\sim j$ iff $\lambda_{i,j}\ne0$) is bipartite with parts $A,B$, and

$$\lambda_{i,j}>0\ \Longrightarrow\ i\in A,\ j\in B .$$

The statement is conditional and does not assert that a minimizer exists.

Milestones

1. Theorem 3.1. For distinct $u,v,w$ and $\lambda_1,\lambda_2>0$, the structure $\overrightarrow{uv}^{\lambda_1},\overrightarrow{vw}^{\lambda_2}$ is not cost-minimizing; if $\lambda_1\le\lambda_2$ the structure $\overrightarrow{uw}^{\lambda_1},{}^{\lambda_1}\overleftrightarrow{vw}^{\lambda_2}$ supports the same flow at strictly lower cost, and if $\lambda_1\ge\lambda_2$ so does ${}^{\lambda_2}\overleftrightarrow{uv}^{\lambda_1},\overrightarrow{uw}^{\lambda_2}$.
2. The in-and-out claim (proof of Corollary 3.2). In an arbitrary network supporting $F$, if $\lambda_{u,v}>0$ and $\lambda_{v,w}>0$ for some $u,v,w$, the network is not cost-minimizing.
3. Corollary 3.2. A network containing a cycle of odd length is not cost-minimizing.
4. Corollary 3.11 (a sibling corollary of Theorem 3.1, not on the path to the goal). If $f_{i_1},f_{i_2}>0>f_{j_1},f_{j_2}$ for distinct $i_1\ne i_2$, $j_1\ne j_2$, no star network is cost-minimizing.

Significance

Corollary 3.3 says that in an optimal Lightning Network every node is a pure sender or a pure receiver, and that no node relays payments. This sits in tension with the observed LN, which is organized around large routing hubs; the paper reconciles the two in §3.2 by allowing new nodes. Corollary 3.11 shows that the star, the intuitive candidate for a cheapest topology, is optimal only with a single net payer or a single net payee.

The results are proved in the paper, with short arguments in its Appendix A, and they have no machine-checked proof. This mission adds a precise version of the model, in which the meaning of "cost-minimizing", the sign conventions and the corrected cost axioms are fixed, and a formal proof of the chain Theorem 3.1 → odd cycles → bipartite structure for an arbitrary cost function satisfying the axioms.

Difficulty

Theorem 3.1 on its own is a two-line computation. The difficulty is in applying it inside an arbitrary network. When $u$ and $w$ already share a channel, adding $\lambda_1$ or $\lambda_2$ to it requires $c(a+b)\le c(a)+c(b)$ for reals of either sign. That inequality is not among the axioms and has to be derived from them. The odd-cycle step needs a pigeonhole argument on channel orientations around a cycle. The bipartite step needs either König's characterization of bipartite graphs or a direct construction of the parts from the flow directions. The naive formalization that re-states Theorem 3.1 only for a network with exactly two channels does not reach the corollaries.

Formalization scope

• The node set is an arbitrary finite type V, not $\{1,\dots,n\}$. The matrix is Λ : V → V → ℝ, because λ is a Lean keyword.
• Sign convention. Support is the row-sum display $\sum_j\lambda_{i,j}=f_i$ of §2.1, under which a net payer has $f_i>0$. The paper's examples (§2, Figure 1, proof of Theorem 3.1) use the opposite sign. Every statement here is invariant under $F\mapsto-F$, and Theorem 3.1 is stated with "the same flow" given by Supports, which is independent of the sign.
• Cost is the form $\tfrac12\sum_{i,j}c(\lambda_{i,j})$, which needs no order on $V$.
• Cost-minimizing compares with networks on the same node set $V$; a network with an added hub (§3.2) is not an alternative.
• Axiom correction (SA). The paper prints (SA) as "$c(x+y)<c(x)+c(y)$ for $x>y\ge0$", which fails at $y=0$, so every theorem would hold vacuously. The formalization uses $x,y>0$, the form verified in Appendix D. The stronger axiom (SA+) is not used in this mission.
• Cycles are injective maps Fin k → V, $k\ge3$ odd, with cyclic successor finRotate k. A channel is a nonzero entry in either direction.
• Bipartite is Mathlib's SimpleGraph.IsBipartiteWith A Aᶜ on the channel graph, with the flow-direction clause stated separately as the stronger content.
• The star is the network whose only channels join each $i\ne h$ to the hub $h$ with net flow $f_i$; Corollary 3.11 assumes $\sum_i f_i=0$.

Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (no $\sqrt{|x|}$ or linear cost); cost-minimization ranges over all networks on $V$, not over a fixed edge set; $V$ is not fixed to three nodes; the in-and-out claim is stated for arbitrary networks; and $A$ and $B$ are complementary, so they cannot overlap.

König's theorem is in Mathlib (SimpleGraph.two_colorable_iff_forall_loop_even) and proved on the platform (FamousTheorems.two_colorable_iff_no_odd_cycle_6b), so it is not posed here. The derived two-sided subadditivity of $c$, and a lemma rerouting a relayed flow inside an arbitrary network, are reusable in the other missions of the series. Contributions of such auxiliary lemmas are welcome.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023. https://ssrn.com/abstract=4439190 (published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872).
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, working paper, 2022 ([GHS22] in the paper; the source of the cost axioms).
• D. Kőnig, Theorie der endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft, Leipzig, 1936.
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2015 (as cited in the paper). https://lightning.network/lightning-network-paper.pdf

Opinions on large directed social networks

Linear models of opinion formation go back to DeGroot (DeGroot 1974), in which every individual repeatedly replaces their opinion by a weighted average of the opinions of the people they listen to, and to Friedkin and Johnsen (Friedkin–Johnsen 1990), who added a persistent internal opinion. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969v2, Mathematics of Operations Research, 2025) add a random external (media) signal whose law may depend on the individual's attributes, which models selective exposure, and ask what the opinions look like on a large random social network. The answer is the behaviour of a typical individual, a uniformly chosen vertex: its stationary opinion converges in law to the opinion of the root of the network's local weak limit, and the empirical distribution of all stationary opinions converges to the same law. Questions such as consensus or polarization are then questions about one limiting random variable, independent of the particular realization of the network.

This mission formalizes that main result (Theorem 2) together with the fixed-graph stationarity theorem it rests on (Theorem 1).

Setting

A vertex-weighted directed graph on a vertex set $V$ gives each vertex $i$ an in-degree $d_i^-$, an ordered list of inbound neighbours $\ell(i,1),\dots,\ell(i,d_i^-)$ and weights $c(i,r)\in[0,1]$ with $\sum_r c(i,r)=c$ whenever $d_i^->0$. The parameters satisfy $c\in[0,1)$, $d\in(0,1]$, $c+d\le1$. The opinions $R_i^{(k)}\in[-1,1]$ evolve by recursion (1),

$$R_i^{(k+1)}=\sum_{r=1}^{d_i^-}c(i,r)\,R^{(k)}_{\ell(i,r)}+W_i^{(k)}+(1-c-d)R_i^{(k)},\qquad k\ge0,$$

where the external signals $W_i^{(k)}$ are independent, i.i.d. in time given the vertex mark, and bounded by $|W_i^{(k)}|\le d+c-\sum_rc(i,r)$. With the operator $\Delta f(i)=\sum_rc(i,r)f(\ell(i,r))+(1-c-d)f(i)$ this reads $R^{(k+1)}=\Delta R^{(k)}+W^{(k)}$. The stationary vector is $R=\sum_{r\ge0}\Delta^rW^{(r)}$.

The full mark of a vertex is $\mathbf X_i=(\mathbf A_i,Q_i,S_i,D_i^-,C(i,1),C(i,2),\dots)$: a generic attribute, an internal opinion, a stubbornness label, the in-degree and the weights. Marks are compared by the metric

$$\rho(\mathbf x,\tilde{\mathbf x})=\rho'(\mathbf a,\tilde{\mathbf a})+|q-\tilde q|+|s-\tilde s|+|d^--\tilde d^-|+\sum_j|c_j\mathbb 1(d^-\ge j)-\tilde c_j\mathbb 1(\tilde d^-\ge j)|.$$

A random graph sequence $G(V_n,E_n;\mathscr A_n)$ has vertex set $V_n=\{1,\dots,n\}$ and attributes $\mathscr A_n=\{\mathbf Y_i=(\mathbf A_i,Q_i,S_i)\}$; edges and weights are random given the attributes. The conditional expectation $E_n[\cdot]=E[\cdot\mid\mathscr A_n]$ conditions on the attributes only. The in-component of depth $k$ of a vertex $v$ is the set of vertices with a directed path of length at most $k$ to $v$. The sequence admits a strong coupling (Definition 4) with a rooted marked graph $\mathcal G(\boldsymbol{\mathcal X})$ if, for two independent uniform vertices $I_n,J_n$, every depth $k\ge1$ and every $\epsilon>0$, there are two independent copies of $\mathcal G(\boldsymbol{\mathcal X})$ whose depth-$k$ root in-components are, with conditional probability tending to one in probability, isomorphic to those of $I_n$ and $J_n$, with all marks $\epsilon$-close in $\rho$ and the two in-components of $I_n$ and $J_n$ disjoint. The Wasserstein distance is $d_1(\mu,\nu)=\inf\{E|X-Y|:X\sim\mu,Y\sim\nu\}$.

Formalization targets

Goal: Theorem 2

Assume a strong coupling, $d>0$, and a signal kernel $\nu(\mathbf x)$ with $d_1(\nu(\mathbf x),\nu(\tilde{\mathbf x}))\le K\rho(\mathbf x,\tilde{\mathbf x})$. Then there are laws $L_k$ of $(\mathcal R^{(0)},\dots,\mathcal R^{(k)})$ and $L^*$ of $\mathcal R^*$, not depending on $n$, with

$$\max_{0\le r\le k}E\bigl[|R^{(r)}_{I_n}-\mathcal R^{(r)}|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i^{(k)})\xrightarrow{P}E f(\mathcal R^{(k)}),$$ $$E\bigl[|R_{I_n}-\mathcal R^*|\bigm|\mathscr A_n\bigr]\xrightarrow{P}0,\qquad \frac1n\sum_{i=1}^nf(R_i)\xrightarrow{P}E f(\mathcal R^*),$$

for every continuous $f$ on $[-1,1]$, and $\mathcal R^{(k)}\Rightarrow\mathcal R^*$ geometrically fast:

$$d_1\bigl(\mathrm{law}\,\mathcal R^{(k)},\mathrm{law}\,\mathcal R^*\bigr)\le(1-d)^k\Bigl(\frac2d+2\Bigr).$$

Milestones

1. $\|\Delta\|_\infty\le1-d$ (proof of Theorem 1, p. 22).
2. Theorem 1 (p. 5): on a fixed locally finite graph, $R^{(k)}\Rightarrow R$ at a geometric rate, with a limit that does not depend on $R^{(0)}$.
3. Theorem 2(1) (p. 8): the fixed-time statement.

A supporting statement of the proposal, not a milestone, is the tail bound $\|R-B^{(k)}\|_\infty\le2\sum_{r>k}(1-d)^r$ for $B^{(k)}=\sum_{r\le k}\Delta^rW^{(r)}$ (proof of Theorem 2, p. 28).

Significance

Theorem 2 reduces the stationary opinion distribution of a large network to a single random variable $\mathcal R^*$ attached to the local limit. When the limit is a marked Galton–Watson tree, $\mathcal R^*$ has an explicit series representation whose mean and variance are computed in closed form later in the paper (the other two missions of this series), and these formulas are what explain consensus and polarization. Strong couplings exist ([Olvera-Cravioto 2022], cited on p. 8 of the paper) for Erdős–Rényi graphs, the Chung–Lu and Norros–Reittu models, the configuration model, stochastic block models and preferential attachment graphs, so the theorem applies to most random graph models used for social networks.

The result is proved in the paper; nothing in it has been formalized. On Prove2Me this is the first statement of a strong coupling, a form of local weak convergence for directed marked graphs, and of a stochastic recursion on a random graph. The definitions of in-components, the coupling event and the strong coupling are reusable for any local-limit statement about directed random graphs, and the contraction and time-reversal milestones are reusable for linear stochastic recursions.

Difficulty

The fixed-graph part is a contraction argument, but the coupled object is not the opinion process itself: $R^{(k)}$ does not converge almost surely, and only its time reversal $B^{(k)}$ does. The main difficulty is Theorem 2. A local limit controls one neighbourhood at a time, while the empirical averages need two uniformly chosen vertices to be asymptotically independent, which a one-vertex limit statement does not give. The errors in weights, signals and initial opinions enter at every vertex of a depth-$k$ neighbourhood, and the statements condition only on the attributes, with edges and weights integrated out. The stationary statement then requires an interchange of $n\to\infty$ and $k\to\infty$ that is uniform in $n$.

Formalization scope

All random objects of the $m$-th model live on one probability space, and the $m$-th graph has $m+1$ vertices (the paper's $G_{m+1}$), so a uniform vertex always exists. Signals are written $W_i^{(k)}=\zeta(\mathbf X_i,U_i^{(k)})$ and initial opinions $R_i^{(0)}=\varphi(\mathbf X_i,V_i)$ with i.i.d. uniforms independent of the graph: this quantile representation is equivalent in law to the paper's conditionally i.i.d. signals. Neighbour indices are 0-based. The conditional quantities given $\mathscr A_n$ are regular conditional distributions given the attribute vector, and "random variables whose distribution does not depend on $\mathscr A_n$" are encoded by fixed limit laws, with the paper's $E[|\cdot|\mid\mathscr A_n]\to0$ read as $d_1$ convergence in probability of the conditional laws, which is equivalent. Theorem 1 is stated on countably many vertices, with its geometric rate given as an explicit bound for 1-Lipschitz test functions of finitely many coordinates.

Disclosed choices: the strong coupling is stated on the given space with measurable events inside the coupling events (the event "an isomorphism exists" need not be measurable), with isomorphisms that preserve the order of inbound neighbours (which the proof uses), and through its second bullet, which implies the first. The paper's conditional independence of weight vectors given $\mathscr A_n$ is not imposed. The strong coupling also requires the depth-$k$ in-components of $I_n$ and $J_n$ to be disjoint on the coupling event: the proof of Theorem 7 uses this, and without it Definition 4 admits a graph whose vertices all listen to a single hub, whose shared signals keep $\frac1n\sum_if(R_i^{(k)})$ random. The page puts no condition on $R^{(0)}$ beyond conditional independence of the signals, but Theorem 2(1) at time $0$ is false then (take $R^{(0)}\equiv(-1)^n$); the statement assumes a $d_1$-Lipschitz initial kernel with the same $K$, which covers the paper's own simulations. The geometric rate uses the constant of the proof.

Trivializing readings are excluded: every tsum is absolutely summable under the hypotheses, conditional laws are regular conditional distributions of measurable random variables, the averages have no division by zero, and the limit laws are forced onto $[-1,1]$ by the convergence, so no integral defaults to $0$. Theorem 7 of the paper (the two-vertex coupling) is not a milestone. Contributions of proofs of any milestone, and of general lemmas on regular conditional distributions and Wasserstein couplings, are welcome.

Selected references

• N. Fraiman, T.-C. Lin and M. Olvera-Cravioto, Opinion dynamics on directed complex networks, Mathematics of Operations Research, 2025; preprint arXiv:2209.00969v2, 2024. https://arxiv.org/abs/2209.00969v2
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69 (1974), 118–121. https://doi.org/10.1080/01621459.1974.10480137
• N. E. Friedkin and E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15 (1990), 193–206. https://doi.org/10.1080/0022250X.1990.9990069
• M. Olvera-Cravioto, Strong couplings for static locally tree-like random graphs, Journal of Applied Probability 59(4) (2022), 1261–1285 (reference [33] of the paper, where the random graph models admitting strong couplings are listed).

Motivation

Industries in which capacity can be built but not sold back (energy generation, manufacturing, mining) are studied through irreversible investment models: a firm controls a nondecreasing investment process and trades the cost of capacity against uncertain future revenues. When many small firms compete, each firm's revenue depends on aggregate production through the market price, and the natural equilibrium notion is a mean-field equilibrium: every firm optimizes against a given aggregate, and the aggregate generated by the optimal behaviour is the one that was assumed.

Aïd, Basei and Ferrari (arXiv:2305.00541; Operations Research, 2025) add a macroeconomic regime to this picture. The economy switches between two states according to a continuous-time Markov chain, and volatilities and prices depend on the state. They prove that a stationary mean-field equilibrium exists and is unique, and that the equilibrium firm invests at regime-dependent barriers. Related stationary mean-field games with singular controls include Cao and Guo (Stochastic Processes and their Applications, 2022) and Cao, Dianetti and Ferrari (doi:10.1287/moor.2022.1323); the stability of the reflected regime-switching diffusions that appear in the equilibrium is due to Budhiraja and Liu (Mathematics of Operations Research, 2012).

Setting

A real Brownian motion $B$ and an independent two-state Markov chain $\varepsilon$ with generator

$$P=\begin{pmatrix}-p_1&p_1\\p_2&-p_2\end{pmatrix},\qquad \pi=\Big(\frac{p_2}{p_1+p_2},\frac{p_1}{p_1+p_2}\Big),\qquad p_1,p_2\in(0,1),$$

live on a complete probability space; $\mathbb F$ is their augmented natural filtration. A control $I$ is an adapted, nonnegative, nondecreasing càdlàg process with $I_{0-}=0$. The production capacity is

$$X^I_t=x\exp\Big(-\Big(\delta t+\tfrac12\int_0^t\sigma^2_{\varepsilon_s}ds\Big)+\int_0^t\sigma_{\varepsilon_s}dB_s+I_t\Big),\qquad x>0,$$

and investment costs $\kappa\,X^I_t\circ dI_t$, the integral (2.3) that charges a jump $\Delta I_t$ the amount $X^I_{t-}(e^{\Delta I_t}-1)$. Given aggregate productions $Q=(Q_1,Q_2)\in(0,\infty)^2$, the price in regime $i$ is $\eta_i=\varphi_i+\zeta_iQ_i^{-\alpha}$, and a firm starting from $(x,i)$ maximizes, over the admissible set $\mathcal A$ of (2.5),

$$J_{(x,i)}(I,Q)=\mathbb E_{(x,i)}\Big[\int_0^\infty e^{-\rho t}\big(\eta_{\varepsilon_t}X^I_tdt-c(X^I_t)^2dt-\kappa X^I_t\circ dI_t\big)\Big].$$

A stationary mean-field equilibrium (Definition 2.2) is a pair $(I^\star,Q^\star)$ such that $I^\star$ maximizes $J_{(x,i)}(\cdot,Q^\star)$ over $\mathcal A$, and the controlled pair $(X^{I^\star}_t,\varepsilon_t)$ has a stationary distribution $p_\infty$ with

$$Q^\star_j=\frac1{\pi_j}\int_0^\infty x\,p_\infty(dx,j),\qquad j=1,2.$$

The barrier control at levels $a_1,a_2>0$ is

$$I^\star_t=0\vee\sup_{0\le s\le t}\Big(\ln(a_{\varepsilon_s}/x)+\int_0^s\big(\delta+\tfrac12\sigma^2_{\varepsilon_u}\big)du-\int_0^s\sigma_{\varepsilon_u}dB_u\Big),$$

the minimal investment keeping $X^{I^\star}_t\ge a_{\varepsilon_t}$. Finally $\phi_i(\theta)=\frac12\sigma_i^2\theta^2+(\delta+\frac12\sigma_i^2)\theta-p_i$ and $\bar\phi=\phi_1\phi_2-p_1p_2$, whose negative roots are $\theta_1<\theta_2<0$.

Formalization targets

Goal: Theorem 4.1

Under Assumption 2.1, $\rho>2\max\{\sigma_1^2,\sigma_2^2\}$, and $1+\theta_2<0$: for every $(x,i)$ there are barriers $a^\star\in(0,\infty)^2$ and $Q^\star\in(0,\infty)^2$ with

$$(I^\star(a^\star),Q^\star)\ \text{a stationary MFE, and every stationary MFE } (I,Q)\text{ has } Q=Q^\star,\ I=I^\star\ \text{a.s.}$$

Milestones, in the order the proof uses them

1. Proposition 4.1: a $C^2$ solution of the free-boundary problem (4.10) is the value function, and the barrier control is optimal.
2. Proposition 4.2 (corrected): the stopping problem (4.13) has threshold regions, a $C^1$ value satisfying (4.17), and an optimal hitting time.
3. Proposition 4.3 ((4.18) corrected): $V(x,i)=k_i+\int_{a_i}^xv(y,i)dy$.
4. The root structure of (4.29): $\theta_1<\theta_2<0<\theta_4$ are the nonzero roots of $\bar\phi$.
5. Proposition 4.6: the stationary distribution function of the capacity reflected at $0<a_1<a_2$ is the explicit $\Pi(\ln x,i)$ of (4.32).
6. Corollary 4.7: the regime-wise stationary means (4.35)–(4.36).
7. Step 1 of the proof of Theorem 4.1: the stopping value and the barriers decrease in $Q$.
8. Theorem 2.4(ii): $\mathbb P(X_\infty\ge x)/x^{\theta_2}\to C>0$.

Significance

The theorem gives a fully explicit equilibrium in a model with common noise in the form of regime switching: the barriers solve a finite system of algebraic equations, and the stationary distribution of capacities is known in closed form, with a Pareto tail of exponent $\theta_2$. This makes comparative statics of market concentration and of the industry's response to regime persistence computable, which is what Section 3 of the paper does numerically.

The result is proved on paper; none of it is formalized. A complete development would yield a machine-checked verification theorem for regime-switching singular control, a checked link between singular control and optimal stopping, and a checked stationary law for a reflected regime-switching geometric Brownian motion. The printed text contains slips the formalization corrects in the open: the continuation and stopping regions of Proposition 4.2 are printed swapped, a term of (4.18) carries a spurious factor $a_i$, and an integration by parts in the proof drops $\kappa$.

Difficulty

The obvious route, solving the variational inequality (4.8) by guessing a smooth-fit solution, fails here: the two regimes couple the ordinary differential equations, and the smooth-fit and smooth-pasting equations become nonlinear in both barriers at once, so existence and uniqueness of their solution cannot be read off. The regularity a verification argument needs ($C^2$ value, a threshold structure of the investment region) is therefore the hard part, and with regime switching it is not covered by the one-dimensional theory. The stationary law requires positive recurrence of a reflected diffusion with switching and the identification of its limit law. The fixed point $Q=\mathcal RQ$, where $(\mathcal RQ)_j=\pi_j^{-1}\int_0^\infty x\,p^Q_\infty(dx,j)$ is built from the stationary law under the barrier control optimal for $Q$, needs continuity and a priori bounds of $\mathcal R$ for existence, and a monotonicity argument for uniqueness; the printed uniqueness argument treats ordered pairs of fixed points explicitly, and uniqueness of the optimal control itself is not argued on the page but is part of the goal.

Formalization scope

Lean represents regimes as Fin 2 (index 0 is regime 1) and time as $\mathbb R_{\ge0}$. The model consists of: the chain, pinned by its closed-form transition function $e^{tP}$; Mathlib's IsBrownianReal for $B$; independence of $B$ and $\varepsilon$; the augmented filtration; $M=\int\sigma_\varepsilon dB$ through the platform relation EthierKurtz.HasBrownianItoIntegral, with continuous paths; the state (2.4); the integral (2.3), computed as $\int e^{-\rho t}Y_t\,d(e^{I})_t$; the admissible set (2.5) with $[0,\infty]$-valued expectations; $J$ of (2.6); Definition 2.2; and the barrier control (4.11). $\mathbb E_{(x,i)}$ is the expectation conditioned on $\varepsilon_0=i$.

Standing constants: $\delta,\sigma_i,\rho,c,\kappa,\varphi_i,\zeta_i>0$, $p_i\in(0,1)$, $0<\alpha<1$, $\min_i\varphi_i>\rho+\delta$, and Assumption 2.1. The root condition $1+\theta_2<0$ is stated as "$\bar\phi$ has no root in $[-1,0)$". Pinned hypotheses, each disclosed in the item that carries it: the stationary distribution is the weak limit of the time-$t$ laws; $Q_i>0$; $a_i>0$ wherever (4.11) is used; $0<a_1<a_2$ for the §4.2 statements; $(\rho+\delta)\kappa<\varphi_i$ on the goal; and "$\sim$" in Theorem 2.4(ii) as a ratio tending to a positive constant.

The equilibrium is defined from the model: optimality against every admissible control, including those with an initial jump, and the limit law of the actually controlled process. It is never defined through the paper's closed forms (4.23) or (4.32), which would make the goal a statement about formulas. The barrier control is the printed formula, not an arbitrary control keeping $X\ge a$.

Not formalized: Section 3 (numerics), Proposition 4.4 and Corollary 4.5 (semi-explicit value functions), the continuity part of Step 1, and Steps 2–4 of the proof as separate items. Contributions toward a general verification theorem for regime-switching singular control, regularity of regime-switching stopping problems, and stationary laws of reflected switching diffusions are reusable beyond this mission.

Selected references

• R. Aïd, M. Basei, G. Ferrari, A Stationary Mean-Field Equilibrium Model of Irreversible Investment in a Two-Regime Economy, arXiv:2305.00541v1, 2023; Operations Research, 2025. https://arxiv.org/abs/2305.00541
• A. Budhiraja, X. Liu, Stability of constrained Markov-modulated diffusions, Mathematics of Operations Research 37(4):626–653, 2012.
• H. Cao, X. Guo, MFGs for partially reversible investment, Stochastic Processes and their Applications 150:995–1014, 2022.
• H. Cao, J. Dianetti, G. Ferrari, Stationary discounted and ergodic mean-field games of singular controls, Mathematics of Operations Research, 2022. https://doi.org/10.1287/moor.2022.1323
• G. Ferrari, N. Rodosthenous, Optimal control of debt-to-GDP ratio in an N-state regime switching economy, SIAM Journal on Control and Optimization 58(2):755–786, 2020.

Motivation

Inverse optimization asks for the objective of an optimization problem when only its optimal decisions are observed. It was formalized for linear programs by Ahuja and Orlin (Operations Research 2001) and has since been used to infer costs, preferences and utilities from observed choices, for instance in routing, pricing and the imitation of expert planners (see the survey discussion in Chan, Lee and Terekhov, Management Science 2019, and the noisy-data setting of Aswani, Shen and Siddiq, Operations Research 2018).

Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) study a contextual version: the problems a decision-maker faces change from instance to instance, and the observed expert decisions constrain a fixed but unknown cost vector. Their question is not how to estimate the cost, but which decisions to take so that the loss against the expert is as small as possible in the worst case. This mission formalizes the answer in the offline setting, where a finite data set is given in advance. The text used is the arXiv preprint v3 (1 July 2023); all theorem numbers refer to it.

Setting

Actions live in $\mathbb R^n$ and costs in $\mathbb R^d$, both with the Euclidean norm, and $d\ge2$. The unknown cost $c^\star$ lies on the unit sphere $S^d=\{c:\|c\|=1\}$.

An instance is a pair $(\mathcal X,f)$: a feasible set $\mathcal X\in\mathcal B$, i.e. a nonempty compact subset of $\mathbb R^n$ with diameter at most $1$, and a context function $f\in\mathcal F$, i.e. a $1$-Lipschitz map $\mathbb R^n\to\mathbb R^d$. Given a cost $c$, the forward problem is

$$\psi(c,\mathcal X,f)=\operatorname*{arg\,min}_{x\in\mathcal X} f(x)'c,$$

a set of minimizers.

The offline data are $\mathcal D=\{(\mathcal X_i,f_i,x^\star_i)\}_{i=1}^N$ with $x^\star_i\in\psi(c^\star,\mathcal X_i,f_i)$. The costs compatible with them form the knowledge set

$$C(\mathcal D)=\{c\in S^d:\ c'f_i(x^\star_i)\le c'f_i(x)\ \ \forall x\in\mathcal X_i,\ i=1,\dots,N\}.$$

A policy maps the data and a new instance $(\mathcal X,f)$ to an action $x^\pi\in\mathcal X$, and its regret on the instance is $(f(x^\pi)-f(x^\star))'c^\star$ with $x^\star\in\psi(c^\star,\mathcal X,f)$. The worst-case regret $\mathcal{WCR}^\pi(\mathcal D)$ is the supremum of the regret over $c^\star\in C(\mathcal D)$, $\mathcal X\in\mathcal B$ and $f\in\mathcal F$.

The angle between two vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, with $\theta(c,0)=\theta(0,\hat c)=0$. The uncertainty angle of a set $C$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\ \theta(c,\hat c),$$

and a circumcenter $\hat c(C)$ is a point of $S^d$ attaining the infimum. Geometrically, $\alpha(C)$ is the aperture of the narrowest revolution cone containing $C$ and $\hat c(C)$ is its axis. The circumcenter policy answers an instance with any $x^\pi\in\psi(\hat c(C(\mathcal D)),\mathcal X,f)$. Write $g(a)=\mathbf 1\{a<\pi/2\}\sin a+\mathbf 1\{a\ge\pi/2\}$.

Formalization targets

Goal: Theorem 1 (offline minimax regret), p. 12

For every realizable data set,

$$\mathcal{WCR}^{\pi}(\mathcal D)\ \le\ g\big(\alpha(C(\mathcal D))\big)$$

for the circumcenter policy $\pi$, whatever circumcenter and whatever minimizer it picks. Conversely, for every $\bar\alpha\in[0,\pi]$ there is an information set $C\subseteq S^d$ with $\alpha(C)=\bar\alpha$ on which every policy suffers regret at least $g(\bar\alpha)$ on some instance. The upper bound and the lower bound are one statement.

Milestones

1. Lemma 1 (p. 11). For a proxy cost $c^\pi\in S^d$ and a true cost $c^\star\in S^d$, the worst-case regret over instances and over minimizers $x^\pi\in\psi(c^\pi,\mathcal X,f)$ is attained and equals $g(\theta(c^\star,c^\pi))$:

$$\mathcal L(c^\pi,c^\star)=\begin{cases}\sin\theta(c^\star,c^\pi)&\theta(c^\star,c^\pi)<\pi/2,\\1&\text{otherwise.}\end{cases}$$

2. Lemma 2 (p. 12). Every nonempty $C\subseteq\mathbb R^d$ has a circumcenter; it is unique when $C\setminus\{0\}\neq\emptyset$ and $\alpha(C)<\pi/2$.

Significance

Theorem 1 identifies the minimax offline regret of contextual inverse optimization with a single geometric number of the knowledge set, $\sin\alpha(C(\mathcal D))$ (or $1$), and shows that one explicit policy, acting as if the cost were the circumcenter, attains it uniformly over all instances. It reduces the design of offline policies to computing a circumcenter, and it is the benchmark that the paper's online analysis (§4–§5) compares against: the online policies are judged by how fast they shrink the uncertainty angle.

The results are proved in the paper (App-3–App-9). To our knowledge none of them has a machine-checked proof. Formalizing them yields a verified statement of the minimax value, a reusable notion of uncertainty angle and circumcenter for arbitrary subsets of $\mathbb R^d$, and the exact tightness of the bound, including the regime $\alpha\ge\pi/2$ where nature can force the maximal regret.

Difficulty

The upper bound is not a direct consequence of the definitions: the regret involves an arbitrary compact action set and an arbitrary $1$-Lipschitz context, and the only link between the circumcenter's choice and $c^\star$ is that $x^\pi$ is optimal for the wrong cost. Lemma 1 is where this link is turned into an angle, and its value must be matched exactly, not up to constants. Lemma 2 requires care because the objective $\hat c\mapsto\sup_{c\in C}\theta(c,\hat c)$ is a supremum over an arbitrary, possibly non-closed, set and the angle convention at $0$ breaks continuity. The lower bound must hold for every policy, including ones that exploit tie-breaking, so the hard instance must be chosen after the policy.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin d). The angle vecAngle is defined directly with value $0$ when either argument is $0$; Mathlib's InnerProductGeometry.angle (which is $\pi/2$ there) is not used. $\alpha$ is a real infimum over the sphere of a real supremum over $C$; the angles lie in $[0,\pi]$, so both are genuine when $C$ is nonempty. Action sets are nonempty compact sets of diameter at most $1$ (nonemptiness is added: an empty feasible set has no action), contexts are $1$-Lipschitz, and data are indexed by Fin N.

Committed conventions and pins:

• $d\ge2$ is the paper's standing assumption (p. 7). $n\ge1$ is added on Lemma 1 and on Theorem 1: in $\mathbb R^0$ every regret is $0$ and the lower bounds would be false.
• Theorem 1's upper bound assumes realizable data (some $c_0\in S^d$ explains every observation), as the paper's data model does; this makes $C(\mathcal D)$ nonempty.
• Worst-case regrets are never written as real suprema. The upper bound quantifies over every $c^\star\in C(\mathcal D)$, instance, circumcenter, policy minimizer and expert minimizer. Lemma 1 is stated with IsGreatest, and the lower bound of Theorem 1 in attained form, which implies the paper's statement about the supremum.
• In the lower bound the quantifiers are ordered as in the paper: the set $C$, then the policy (any map from instances to feasible actions), then nature's instance.

A formalization that bounds the regret only for one selected minimizer of the forward problem, or that chooses the hard instance before the policy, proves a different and weaker theorem and is excluded.

The development needs: compactness and lower semicontinuity on the sphere (existence of a circumcenter), elementary spherical geometry for the uniqueness and for $\sin\theta$ as the value of a two-point instance, and monotonicity of $g$ on $[0,\pi]$. The angle, uncertainty angle and circumcenter definitions are reusable for the online missions of this series. Proofs of the two lemmas are the natural first contributions.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv preprint v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015v3
• R. K. Ahuja, J. B. Orlin, Inverse optimization, Operations Research 49(5):771–783, 2001. https://doi.org/10.1287/opre.49.5.771.10607
• T. C. Y. Chan, T. Lee, D. Terekhov, Inverse optimization: closed-form solutions, geometry, and goodness of fit, Management Science 65(3):1115–1135, 2019. https://doi.org/10.1287/mnsc.2017.2992
• A. Aswani, Z.-J. Shen, A. Siddiq, Inverse optimization with noisy data, Operations Research 66(3):870–892, 2018. https://doi.org/10.1287/opre.2017.1705
• R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18(3–4):483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z

Motivation

In budget-feasible procurement an auctioneer with a budget $B$ wants to buy services from $n$ strategic sellers. Each seller $i$ has a private cost $c_i\ge0$, the auctioneer has a public valuation $v$ over sets of sellers, and the mechanism must choose whom to pay and how much, so that sellers have no reason to misreport and the total payment never exceeds $B$. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a buyer with a fixed budget faces sellers whose costs it cannot observe.

Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239v2, Operations Research 2025) show that deterministic clock auctions, which repeatedly lower personalized prices and let sellers drop out, achieve constant approximations for monotone submodular valuations. Their Appendix B asks whether an even simpler family suffices: posted-price mechanisms, which approach each seller once with a take-it-or-leave-it offer. This mission formalizes their answer for additive valuations, Theorem 13 (p. 25): no deterministic posted-price mechanism achieves an approximation better than $\sqrt n/2$.

Setting

There are $n$ sellers $N=\{0,\dots,n-1\}$, a budget $B>0$, private costs $c_i\ge0$, and a valuation $v:2^N\to\mathbb R_{\ge0}$. The valuation is additive if there are values $v_i\ge0$ with $v(S)=\sum_{i\in S}v_i$ for every $S\subseteq N$.

A deterministic posted-price mechanism knows $n$, $B$ and $v$, but not $c$. It approaches sellers one at a time. At each step it looks at the history of earlier offers (the seller, the price, and whether the seller accepted) and either stops or names a seller not yet approached and a price $p_i$. The seller accepts if $p_i\ge c_i$ and rejects otherwise, and is never approached again. The output $M(v,c)$ is the set of sellers who accepted; each of them is paid its price. The mechanism is budget feasible if for every additive $v$ and every cost profile $c\ge0$ the accepted prices sum to at most $B$.

For an instance, $\mathrm{OPT}$ is the largest value $v(O)$ of a set $O$ with $\sum_{i\in O}c_i\le B$. A mechanism is a $\rho$-approximation on a class if $\mathrm{OPT}\le\rho\,v(M(v,c))$ on every instance of the class.

In Lean the sellers are Fin n, a mechanism is M : (Finset (Fin n) → ℝ) → PostedPrice n with PostedPrice n a rule next : List (Fin n × ℝ × Bool) → Option (Fin n × ℝ) on histories, run (M v) c is its history on the costs c, and accepted and payment read off the output and the total payment.

Formalization targets

Goal: Theorem 13 (p. 25)

For every $n\ge1$, every $B>0$ and every budget-feasible deterministic posted-price mechanism $M$, there are an additive $v$, costs $c\ge0$ and a set $O$ with

$$\sum_{i\in O}c_i\le B,\qquad v(O)>0,\qquad \frac{\sqrt n}{2}\,v\big(M(v,c)\big)\le v(O).$$

This is $\mathrm{OPT}/v(M)\ge\sqrt n/2$ on some instance, written without division.

Milestones: the three cases of the proof (p. 25)

All three concern one valuation $v_0$: a high-value seller $b_h$ worth $\sqrt n$ and $n-1$ small sellers worth $1$ each, with $c_{b_h}=B$.

1. Case 1. If the first positive offer goes to a small seller $i$, before $b_h$ is approached, then on the costs $c_i=p_i$, $c_j=B$ otherwise, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n=v_0(\{b_h\})$.
2. Case 2. If every earlier offer is $0$ and $b_h$ is offered $B$, then on small costs $B/(n-1)$, $v_0(M)=\sqrt n$ and $\frac{\sqrt n}2 v_0(M)<n-1$ for $n\ge3$, the value of the budget-feasible set of small sellers.
3. Case 3. If every earlier offer is $0$ and $b_h$ is offered $p_h<B$, then on all costs $B$, $v_0(M)\le1$ and $\frac{\sqrt n}2 v_0(M)<\sqrt n$.

Significance

The theorem separates two families of simple mechanisms. Deterministic clock auctions achieve a constant approximation for monotone submodular valuations (Theorem 1 of the same paper, a $4.75$-approximation), while deterministic posted prices cannot achieve better than $\sqrt n/2$ even for additive valuations, the simplest class. Clock auctions are therefore not merely sufficient but needed among these simple formats: the ability to lower a price after a refusal is what the constant approximation rests on. The bound also explains why the paper's positive result for posted prices (Theorem 15, symmetric submodular valuations) must give up a logarithmic factor.

The result is proved in the paper; it has not been formalized. A formal version fixes what "deterministic posted-price mechanism" means, an adaptive rule on histories that never sees costs, and makes the adversary argument checkable: the hard instance depends on the mechanism, and the case analysis must be exhaustive over all such rules. The mission also provides a reusable model of sequential take-it-or-leave-it mechanisms with budget constraints.

Difficulty

The statement is a lower bound over all mechanisms, so the instance must be chosen after the mechanism. The mechanism is adaptive: which seller it approaches next and at what price can depend on every earlier answer. The proof handles this by noting that, on the hard family, every seller rejects a non-positive offer, so all instances share the run up to the first positive offer or the offer to $b_h$. Making that "common prefix" precise for an arbitrary history-dependent rule, and covering the mechanisms that fall outside the three printed cases (those that never approach $b_h$, or offer $b_h$ more than $B$), is the work of the formal proof. A naive attempt that fixes one instance for all mechanisms fails: a mechanism tailored to that instance is optimal on it.

Formalization scope

• Sellers are Fin n; valuations are functions Finset (Fin n) → ℝ, and additivity carries nonnegative weights. Costs are real and nonnegative.
• The budget satisfies $B>0$, an addition to §2's "a budget $B$"; with $B=0$ nothing can be bought.
• A mechanism may depend on the valuation (and on $n$ and $B$, which are fixed outside it) but not on costs. Prices are arbitrary reals. The run asks the rule for at most $n$ offers; a proposal of an already approached seller ends the run.
• Budget feasibility is a property of the mechanism on every additive instance, as defined on p. 24, not of a single run.
• $\mathrm{OPT}$ is never a supremum: the goal exhibits a budget-feasible set $O$ with $v(O)>0$. The condition $v(O)>0$ rules out the trivial instance with $\mathrm{OPT}=0$, where every bound holds.
• The Case 2 cost is $B/(n-1)$; the page prints $1/(n-1)$, which is budget feasible for the small sellers only when $B\ge1$.
• The cases' hypotheses ("before $b_h$", "price $0$") are read off the run on the profile with all costs $B$; "price $0$" is rendered as "price at most $0$".
• Out of scope: running time, truthfulness (posted-price mechanisms are truthful by construction), and randomized mechanisms.

Contributions welcome: proofs of the three cases, the "common prefix" lemma for runs on cost profiles that agree on every seller approached, and the assembly of the goal.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239v2
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78

Motivation

A budget-feasible procurement auction buys services from strategic sellers under a hard budget. Each of $n$ bidders can provide a service at a private cost; the auctioneer values each set of acquired services through a set function $v$ and must keep total payments within a budget $B$. The question, introduced by Singer (FOCS 2010), is how much of the optimal value a truthful mechanism can secure when it does not know the costs. The model covers crowdsourcing, influence maximization with paid seeds, and experimental design with paid participants.

For subadditive valuations, the most general class with non-trivial guarantees, the timeline is short:

• Dobzinski, Papadimitriou and Singer (EC 2011) gave a randomized mechanism with an $O(\log^2 n)$ approximation and a deterministic one with $O(\log^3 n)$.
• Bei, Chen, Gravin and Lu (STOC 2012; SIAM J. Comput. 46(4), 2017) gave a randomized mechanism with an $O(\log n / \log\log n)$ approximation.
• Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239; Operations Research 2025) matched that bound with a deterministic clock auction, Mechanism 4 of their paper, Theorem 8.

Clock auctions are prized beyond truthfulness: they are obviously strategy-proof, they protect the privacy of the winners' costs, and a bidder only ever decides whether to accept a price that keeps falling.

Setting

There are $n$ bidders $N = \{1, \dots, n\}$. Bidder $i$ has a private cost $c_i \ge 0$, the least payment for which it provides its service, and it accepts an offered price $p$ exactly when $c_i \le p$. The auctioneer has a budget $B > 0$ and a valuation $v : 2^N \to \mathbb{R}_{\ge 0}$. The valuation is subadditive:

$$v(S \cup T) \le v(S) + v(T) \quad \text{for all } S, T \subseteq N.$$

It is not assumed monotone, nor normalized.

A set $O$ is budget feasible at true costs if $\sum_{i \in O} c_i \le B$; the optimum $\mathrm{OPT}$ is the largest value of such a set. A mechanism outputs a set $W$ and payments $p_i$ for $i \in W$; it is budget feasible if $\sum_{i \in W} p_i \le B$, and it is a $\rho$-approximation if $\mathrm{OPT} \le \rho \cdot v(W)$ on every instance.

Mechanism 4 runs in phases $t = 1, 2, \dots$ and keeps a set $A$ of active bidders and two solutions $S_{\mathrm{prev}}$ and $S_{\mathrm{curr}}$, all starting from $A = N$, $S_{\mathrm{prev}} = S_{\mathrm{curr}} = \emptyset$. While some active bidder lies outside $S_{\mathrm{prev}} \cup S_{\mathrm{curr}}$, a phase

1. increments $t$;
2. replaces $S_{\mathrm{prev}}$ by the more valuable of $S_{\mathrm{prev}}$ and $S_{\mathrm{curr}}$;
3. offers the price $B/t$ to every active bidder outside $S_{\mathrm{prev}}$; those with $c_i > B/t$ leave for good;
4. sets $S_{\mathrm{curr}}$ to the output of a 2-approximation oracle on the pool $A \setminus S_{\mathrm{prev}}$ at the current price level.

At price $B/t$ a set of candidates is affordable exactly when it has at most $t$ members, so the oracle $\mathrm{alg}(t, X)$ returns a subset of $X$ with at most $t$ members whose value is at least half that of every such subset. The paper uses the demand-query algorithm of Badanidiyuru, Dobzinski and Oren for this step. The mechanism returns the more valuable of the two solutions, $S_{\mathrm{final}}$, and pays each of its members its current price.

Formalization targets

Goal: Theorem 8

There is an absolute constant $C > 0$ such that for every $n \ge 3$, every instance $(v, c, B)$ as above, every oracle with the 2-approximation guarantee and every run of Mechanism 4 of at least $n$ phases,

$$\sum_{i \in S_{\mathrm{final}}} p_i \le B \qquad\text{and}\qquad v(O) \le C \cdot \frac{\log n}{\log \log n}\cdot v(S_{\mathrm{final}}) \ \text{ for every budget-feasible } O.$$

The constant is left unspecified, as in the paper's $O(\cdot)$; the proof gives roughly $40$ for large $n$.

Milestones

• Value monotonicity (p. 15): the value of the output never decreases as more phases run.
• The block bound (p. 15): a set $Z$ of $k \ge 1$ bidders, each of cost at most $B/k$, satisfies $v(Z) \le 4\,v(S_{\mathrm{final}})$.
• The subadditive cover (p. 16): if $O = Z_1 \cup \dots \cup Z_{r+1}$ then $v(O) \le \sum_{i} v(Z_i)$.
• The counting chain (p. 16): natural numbers $z_1, \dots, z_r \ge 1$ with $\frac{1}{z_1+1} + \sum_{i=1}^{r-1} \frac{z_i}{z_{i+1}+1} \le 1$ satisfy $z_r \ge (r/2)^r$.

Significance

Theorem 8 shows that randomization buys nothing asymptotically for budget-feasible procurement with subadditive valuations: the best known approximation factor is achieved by a deterministic mechanism, and moreover by a clock auction, which adds obvious strategy-proofness and transparency. It improves the previous best deterministic factor from $O(\log^3 n)$ to $O(\log n / \log\log n)$. The same template, two maintained solutions and a gradually refined benchmark, drives the paper's constant-factor auctions for submodular valuations (the companion missions of this series).

Nothing in this paper is formalized yet, and no budget-feasible mechanism exists on the platform. The mission produces a machine-checked model of a clock auction with an abstract demand oracle, a monotonicity lemma for two-solution auctions, and the counting argument behind the $\log n/\log\log n$ factor, which is a self-contained real inequality.

Difficulty

The obvious argument looks only at the phase whose size bound matches a large block $Z$ of the optimal set and invokes the oracle there. It fails because part of $Z$ may already sit in $S_{\mathrm{prev}}$, which is never offered to the oracle again, and because the output is decided in the last phase, when the bidders of $Z$ may have been priced out. Both gaps have to be closed with properties of the run (what the oracle guaranteed when $S_{\mathrm{prev}}$ was formed, and that the value of the output never decreases), not of a single phase.

The second case of the analysis, where every block is small, is a counting argument whose final contradiction is asymptotic and involves $\log\log$ terms that are only meaningful for large $n$. A statement with a single uniform constant must also cover small $n$, which the printed argument leaves implicit.

Formalization scope

• Bidders are Fin n, sets are Finset (Fin n), values and costs are real. Non-negativity of $v$ and $c$ are hypotheses; subadditivity is IsSubadditive v. No monotonicity or normalization is assumed.
• The budget is strictly positive, $B > 0$; the paper says only "a budget $B$".
• The oracle is an arbitrary function alg : ℕ → Finset (Fin n) → Finset (Fin n) satisfying IsTwoApproxOracle v alg; feasibility at price $B/t$ is encoded as cardinality at most $t$.
• The argmax steps keep $S_{\mathrm{prev}}$ on ties. Every bidder starts at the price $B$, which is never paid.
• The loop runs with a fuel $F$: it stops when its condition fails or after $F$ phases. The paper does not prove termination, and the loop need not terminate (zero-cost bidders never reject). The goal is stated for every $F \ge n$.
• $\mathrm{OPT} \le \rho\, v(S_{\mathrm{final}})$ is stated for every budget-feasible $O$, never through a supremum. The constant $C$ is quantified before $n$ and the instance; a constant chosen after the instance would make the statement trivial. The threshold $n \ge 3$ keeps $\log\log n > 0$.
• Out of scope: running time ("polynomial-time" has no Lean model here), determinism (automatic for a Lean function), and the clock-auction property, which is built into the definition (prices $B/t$ only fall; a rejecting bidder leaves for good). Truthfulness is a consequence of the clock format and is not stated.

Contributions welcome: proofs of the milestones and the goal; a concrete demand-oracle implementation satisfying IsTwoApproxOracle; and a definition of the block decomposition $Z_1, \dots, Z_{r+1}$ with the cost chain of p. 16, which this mission does not state.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239
• X. Bei, N. Chen, N. Gravin, P. Lu, Budget Feasible Mechanism Design: From Prior-Free to Bayesian, STOC 2012. https://doi.org/10.1145/2213977.2214039; journal version Worst-Case Mechanism Design via Bayesian Analysis, SIAM J. Comput. 46(4):1428–1448, 2017.
• A. Badanidiyuru, S. Dobzinski, S. Oren, Optimization with Demand Oracles, EC 2012. https://doi.org/10.1145/2229012.2229024
• S. Dobzinski, C. Papadimitriou, Y. Singer, Mechanisms for Complement-Free Procurement, EC 2011. https://doi.org/10.1145/1993574.1993602
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78

Budget-feasible procurement with posted prices

In budget-feasible procurement an auctioneer with a fixed budget $B$ wants to buy services from strategic sellers whose costs are private. The auctioneer values sets of services through a valuation function $v$, and wants a mechanism that pays the sellers at most $B$ in total while acquiring a set of nearly maximal value. The model was introduced by Singer (FOCS 2010) and is used for crowdsourcing, influence maximization and data acquisition, where a platform recruits workers or data owners under a fixed spending cap.

Balkanski, Garimidi, Gkatzelis, Schoepflin and Tan (arXiv:2107.09239, Operations Research 2025) study deterministic clock auctions for this problem: mechanisms that offer each seller a sequence of non-increasing prices, where a seller who rejects an offer leaves for good. Clock auctions are obviously strategyproof and robust to collusion, which makes them attractive in practice. A posted-price mechanism is the most restrictive kind: every seller receives a single take-it-or-leave-it offer.

Appendix B of the paper asks how much is lost by restricting to posted prices. For additive valuations no deterministic posted-price mechanism beats $\sqrt{n}/2$ (Theorem 13). For symmetric submodular valuations, where the value of a set depends only on how many sellers it contains, no such mechanism achieves a factor better than $\log n/4$ (Theorem 14), and Theorem 15, the subject of this mission, shows that a simple posted-price mechanism achieves a logarithmic factor.

Setting

There are $n$ sellers (bidders) $N = \{1, \dots, n\}$. Seller $i$ has a private cost $c_i \ge 0$ and accepts an offered price $p$ exactly when $c_i \le p$. The auctioneer has a budget $B > 0$, and throughout this mission every cost satisfies $c_i \le B$, as the paper assumes for Mechanism 5.

A valuation $v : 2^N \to \mathbb{R}_{\ge 0}$ is symmetric submodular if there are numbers $r_1 \ge r_2 \ge \cdots \ge r_n \ge 0$ such that

$$v(S) = \sum_{i=1}^{|S|} r_i \qquad \text{for all } S \subseteq N.$$

The case $r_i \equiv 1$ counts the sellers bought.

A set $O \subseteq N$ is budget feasible at true costs if $\sum_{i \in O} c_i \le B$; the optimum $\mathrm{OPT}$ is the largest value $v(O)$ over such sets.

Mechanism 5 (p. 27) sets aside an arbitrary seller $j$ and keeps a counter $a$ of accepted offers, initially $0$, and a winning set $W$, initially empty. It visits every other seller once, offering

$$p_i = \frac{B}{2\ln n} \text{ if } a = 0, \qquad p_i = \frac{B}{a\cdot 2\ln n} \text{ if } a \ge 1;$$

a seller who accepts joins $W$ and increments $a$. If nobody accepted, $j$ is offered the whole budget $B$. Winners are paid their offered price. In Lean the mechanism is BudgetClock.PostedSym.mech5 n B c j, the loop is scan n B c j, and the valuation class is IsSymmetricSubmodular n v.

Formalization targets

Goal: Theorem 15

There is an absolute constant $C > 0$ such that for every $n \ge 2$, every symmetric submodular $v$, every budget $B > 0$, every cost vector with $0 \le c_i \le B$ and every choice of the set-aside seller $j$, the winning set $W$ of Mechanism 5 and its prices $p$ satisfy

$$\sum_{i \in W} p_i \le B \qquad\text{and}\qquad v(O) \le C\,\ln n \cdot v(W) \ \text{ for every budget-feasible } O.$$

The constant is left unspecified, as in the paper's $O(\log n)$; the goal survives any improvement of it.

Milestones

1. Budget feasibility (proof of Theorem 15, p. 27): the payments made during the scan stay strictly below $B$, and the payments of the final output are at most $B$.
2. Case 1 (p. 28): if no scanned seller accepts, then $W = \{j\}$ and $v(O) \le (2\ln n + 1)\,v(W)$ for every budget-feasible $O$.
3. Case 2 (p. 28, corrected): if at least one scanned seller accepts, then $v(O) \le (2\ln n + 2)\,v(W)$ for every budget-feasible $O$.

Significance

Theorem 15 locates the price of posting prices for symmetric submodular valuations: together with Theorem 14 (no deterministic posted-price mechanism beats $\log n/4$) it shows that the best such mechanism loses a factor of order exactly $\log n$, while the clock auctions of the main body of the paper achieve constant factors for all monotone submodular valuations. The gap between one-shot offers and descending clocks is therefore a genuine separation, not an artefact of the analysis.

The result is proved in the paper. Its formal value lies in pinning down the mechanism and the constants. Checking the printed argument against a precise model exposes three slips: the pseudocode never adds the set-aside seller to $W$, the printed payment bound fails for $2 \le n \le 6$, and the constant $2\ln n + 1$ of Case 2 ignores the set-aside seller and is false (see the milestone notes). None of them affects the $O(\log n)$ claim, and the formal statements record the corrected forms. To our knowledge no machine-checked proof of any result of this paper exists.

Difficulty

The mechanism decides each offer without knowing the remaining costs, and the optimum is defined at the true costs, which the mechanism never learns for rejected sellers. The only information available is a lower bound on each rejected seller's cost, and these lower bounds shrink as the counter $a$ grows. The difficulty is to convert the history of offers into an upper bound on how many sellers any budget-feasible set can hold, uniformly in the order of the scan and the choice of $j$, while keeping the total payment, a harmonic-type sum, below the budget for every $n \ge 2$. The set-aside seller is the subtle point: it receives no offer when $a \ge 1$, so nothing is known about its cost, and a count that forgets it is wrong.

Formalization scope

• Sellers are Fin n; costs are a real vector with $0 \le c_i \le B$; the budget is a real $B > 0$ (the paper says only "a budget $B$"; $B > 0$ is an added hypothesis, since a zero budget makes every offer zero).
• The scan visits $[n]\setminus\{j\}$ in increasing index order. The paper's "arbitrarily ordered" sellers and "arbitrary agent $j$" are covered because every statement quantifies over all cost vectors and all $j$; relabelling sellers changes only the costs.
• A seller accepts iff $c_i \le p_i$. The mechanism returns the winning set and the price offered to each seller (zero for a seller who was never offered anything).
• The set-aside seller $j$ joins $W$ when it accepts the offer $B$. The printed pseudocode omits this step, but the proof relies on it, and without it the goal is false when every scanned seller rejects.
• The symmetric submodular sequence is indexed from $0$ in Lean (r 0 is $r_1$).
• $\mathrm{OPT}$ is never a supremum: the approximation is stated as $v(O) \le C\ln n\cdot v(W)$ for every budget-feasible $O$ at true costs, which avoids dividing by $v(W)$.
• The constant $C$ is quantified before $n$ and all instance data, so it is uniform. The threshold $n \ge 2$ is required: $\ln 1 = 0$, and at $n = 1$ the price $B/(2\ln n)$ is a division by zero, which Lean evaluates to $0$.
• Out of scope: running time, determinism (every Lean function is deterministic) and the posted-price property (built into the definition: each seller receives at most one offer).
• A formalization in which $C$ depends on $n$ or on the instance, or in which $\mathrm{OPT}$ is taken over a set that excludes $j$, would make the goal trivial or different; both are ruled out by the statement's quantifier order and by quantifying over all budget-feasible $O \subseteq N$.

A complete development needs elementary facts about finite sums, the harmonic numbers ($H_m \le 1 + \ln m$, available in Mathlib) and a reasoning principle for the left fold that defines the scan; the latter is reusable for any sequential posted-price mechanism. Proofs of the three milestones, and of the goal from them, are all welcome.

Selected references

• E. Balkanski, P. Garimidi, V. Gkatzelis, D. Schoepflin, X. Tan, Deterministic Budget-Feasible Clock Auctions, arXiv:2107.09239v2, 2021; Operations Research, 2025. https://arxiv.org/abs/2107.09239
• Y. Singer, Budget Feasible Mechanisms, FOCS 2010. https://doi.org/10.1109/FOCS.2010.78
• A. Badanidiyuru, R. Kleinberg, Y. Singer, Learning on a Budget: Posted Price Mechanisms for Online Procurement, EC 2012. https://doi.org/10.1145/2229012.2229026
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1), 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x