All missions

Motivation

Classical Max Cut asks for a partition of the vertices of a weighted graph that maximises the total weight of edges crossing it. Its best-known approximation algorithm, due to Goemans and Williamson, rounds a semidefinite relaxation and guarantees ratio $0.878$. Quantum Max Cut is the analogous problem for a family of local Hamiltonians: each edge contributes a two-qubit term that rewards the two qubits for being antisymmetric, and one asks for the maximum energy of the sum. Estimating it precisely is QMA-complete (Piddock and Montanaro), so attention has turned to efficient approximation algorithms, and to the question of which classes of quantum states can certify a good fraction of the optimum.

A short history of the approximation ratio on weighted graphs:

• 2010. Briët, de Oliveira Filho and Vallentin give an efficient algorithm approximating the best product-state energy within $0.956$; combined with the $1/2$ bound of the next item, this approximates the optimum within $0.478$, as observed by Gharibian and Liu.
• 2012, product states, ratio $1/2$. The best product state always has energy at least half the optimum (Gharibian and Kempe), and this is tight: on a single edge the optimum is the entangled singlet while every product state gets at most half its energy.
• 2019. Gharibian and Parekh round an SDP relaxation of the quantum problem to product states, reaching $0.498$.
• 2020. Anshu, Gosset and Morenz (arXiv:2003.14394) show that allowing two-qubit entangled blocks breaks the $1/2$ barrier on every weighted graph: some tensor product of one- and two-qubit states reaches $0.55$ of the optimum. This mission formalizes that result.

Setting

Let $G=(V,E,w)$ be a simple graph on $V=\{0,\dots,n-1\}$ with nonnegative edge weights $w_e\ge0$ (the paper's standing assumption). Each vertex carries a qubit; a state is a vector $\psi\in\mathbb C^{\{0,1\}^n}$, and it is a unit state if $\sum_x|\psi(x)|^2=1$. With the Pauli matrices $X,Y,Z$ acting on qubit $i$ written $X_i,Y_i,Z_i$, the quantum Max Cut Hamiltonian is

$$H_G=\sum_{\{i,j\}\in E}w_{ij}\,h_{ij},\qquad h_{ij}=\tfrac12\bigl(I-X_iX_j-Y_iY_j-Z_iZ_j\bigr),$$

each edge counted once. The term $h_{ij}$ equals twice the projector onto the singlet $(|01\rangle-|10\rangle)/\sqrt2$, so $H_G$ is positive semidefinite, and

$$\mathrm{OPT}(G)=\|H_G\|=\max_{\psi\ \text{unit}}\langle\psi|H_G|\psi\rangle .$$

Two weight statistics appear throughout: the total weight $W=\sum_{e\in E}w_e$ and, for a vertex $v$, $\max_{e\sim v}w_e$, the largest weight of an edge incident to $v$ (zero for an isolated vertex).

A tensor product of 1- and 2-qubit states $\varphi=\varphi_1\otimes\cdots\otimes\varphi_L$ is obtained by partitioning the qubits into blocks of size one or two (a pair need not be an edge of $G$), choosing a unit vector of $\mathbb C^2$ or $\mathbb C^4$ for each block, and multiplying the block amplitudes. Product states (all blocks of size one) and singlets placed on a matching are examples; a generic entangled state of three qubits is not.

Formalization targets

Goal: Theorem 3 (p. 5)

For every graph with nonnegative weights there is a tensor product $\varphi$ of 1- and 2-qubit states such that

$$\frac{\langle\varphi|H_G|\varphi\rangle}{\mathrm{OPT}(G)}\;\ge\;0.55 .$$

The constant is the exact minimum of the optimisation problem (28) of the paper.

Milestones

The proof combines an upper bound on $\mathrm{OPT}(G)$ with three candidate states:

1. Eq. (10) and Lemma 1 (pp. 6–7): on a star with nonnegative weights, $\|L(G)\|\le\sum_ew_e+\max_ew_e$ for the weighted Laplacian, and $\|H_G\|\le\max_ew_e+\sum_ew_e$.
2. Weighted eq. (15) (p. 9): $\mathrm{OPT}(G)\le W+\frac12\sum_{v}\max_{e\sim v}w_e$.
3. Weighted eqs. (18)–(19) and eq. (24) (pp. 8, 10): a computational basis state $|z\rangle$ with $\langle z|H_G|z\rangle/\mathrm{OPT}(G)\ge\frac13+\frac23\,W/\bigl(2W+\sum_v\max_{e\sim v}w_e\bigr)$.
4. Lemma 2 (p. 10): a matching $M$ and a forest $F$ in $E$ with $\sum_v\max_{e\sim v}w_e=\sum_{e\in M}w_e+\sum_{e\in F}w_e$.
5. Eq. (25) (p. 10): singlets on $M$ and uniformly random bits elsewhere have average energy $\frac32m+\frac12W$, $m=\sum_{e\in M}w_e$.
6. Eq. (26) (p. 11): a basis state with energy at least $f=\sum_{e\in F}w_e$.
7. Eq. (27) (p. 11): the best of the three states has ratio at least $\max\{2f,\,3m+W,\,(4W+f+m)/3\}/(2W+f+m)$.
8. Eqs. (28)–(29) (p. 11): $\max\{2y,3x+1,(4+x+y)/3\}\ge0.55\,(2+x+y)$ for $0\le x\le y\le1$.

Significance

The result shows that the $1/2$ limitation of product states for quantum Max Cut is not a limitation of efficiently describable states: allowing entanglement only within disjoint pairs of qubits already guarantees a fraction strictly above $1/2$ on every weighted graph, including those (a single heavy edge) where product states are stuck at exactly $1/2$. The accompanying algorithmic statement (an efficient randomized algorithm with ratio $\ge0.53$) improved the best known efficient approximation ratio at the time. The upper bound of Lemma 1 is a quantitative form of monogamy of entanglement on a star: the centre qubit cannot be maximally entangled with all of its neighbours.

The theorem is proved in the paper; none of it is formalized. A complete development gives a machine-checked model of a frustrated quantum spin Hamiltonian on arbitrary weighted graphs, a formal upper bound on its ground-state energy, and an explicit certified family of entangled states. The final step, (28)–(29), is evaluated in the paper "by a computer"; a formal proof replaces that evaluation.

Difficulty

The obvious upper bound, $\|H_G\|\le\sum_ew_e\|h_e\|=2W$, is too weak: it allows every edge to be maximally entangled simultaneously, and with it no ratio above $1/2$ follows. The improvement needs the star bound of Lemma 1, which the paper derives from the Lieb–Mattis theorem on the spin of the ground state of bipartite antiferromagnets, restricting the problem to the Hamming-weight-one sector where the Hamiltonian becomes a weighted graph Laplacian. Neither Lieb–Mattis nor the angular-momentum decomposition of $(\mathbb C^2)^{\otimes n}$ is available in Mathlib. The combinatorial side (Lemma 2) needs a careful choice of a maximal incident edge at each vertex and an argument that these edges form no cycle. Eq. (25) is an exact energy computation for a state that is entangled across a matching.

Formalization scope

• Representation. Qubits are Fin n, basis configurations Fin n → Fin 2, states (Fin n → Fin 2) → ℂ, operators complex matrices indexed by configurations; onSite i σ places a $2\times2$ matrix on qubit $i$. The graph is a SimpleGraph (Fin n); weights are w : Sym2 (Fin n) → ℝ with ∀ e, 0 ≤ w e in every statement. $H_G$ sums over the ordered representatives $i<j$ of the edges, so each edge is counted once. The energy is the real part of $\langle\psi|H|\psi\rangle$.
• No $\mathrm{OPT}$ as a supremum. $\mathrm{OPT}(G)$ is not defined. Since $H_G\succeq0$, a bound $\langle\varphi|H_G|\varphi\rangle\ge c\,\mathrm{OPT}(G)$ is stated as $c\,\langle\psi|H_G|\psi\rangle\le\langle\varphi|H_G|\varphi\rangle$ for every unit $\psi$, with $\varphi$ chosen before $\psi$. Ratios are cleared of denominators; $0.55$ is the real $11/20$. Where the paper bounds $\mathrm{PROD}(G)$ (eqs. (19), (24)), the item exhibits a computational basis state, which is a product state.
• The class. A tensor product of 1- and 2-qubit states is given by an involution $p$ of the qubits (the block of $i$ is $\{i,p(i)\}$), a unit vector of $\mathbb C^2$ for every fixed point, a unit vector of $\mathbb C^4$ for every pair, and the product of block amplitudes. The norm and disjointness conditions are part of the definition, so the class does not contain every state and the goal cannot be met by a top eigenvector.
• Conventions. $\max_{e\sim v}w_e=0$ for an isolated vertex and $\max_{e\in E}w_e=0$ for an edgeless graph. A star is a graph all of whose edges contain one centre; other vertices may be isolated. A forest is an edge set whose spanning subgraph is acyclic; a matching is an edge set whose distinct edges are disjoint. The singlet on $\{i,j\}$, $i<j$, is $(|01\rangle-|10\rangle)/\sqrt2$ with qubit $i$ first.
• Weighted forms. Eqs. (15) and (18)–(19) are written in the paper for unit weights and reused in weighted form in the proof of Theorem 3; the items state the weighted forms.
• Not formalized. The second sentence of Theorem 3 (an efficient randomized algorithm with ratio $\ge0.53$), the words "efficiently compute" in Lemma 2 and eq. (26) (existence only), the polynomial bound on the maximum weight (relevant only to running time), Theorems 1, 2, 4 and 5.
• Infrastructure. Useful general results include the Pauli algebra of onSite, energies of computational basis states (equal to cut values), partial-trace style computations for tensor products of blocks, and a Laplacian/Gershgorin bound; the Hamiltonian layer is reusable for later quantum Max Cut missions. Contributions of any of these as separate lemmas are welcome.

Selected references

• A. Anshu, D. Gosset, K. Morenz, Beyond product state approximations for a quantum analogue of Max Cut, TQC 2020; arXiv:2003.14394v1 (2020). https://arxiv.org/abs/2003.14394
• S. Gharibian, O. Parekh, Almost optimal classical approximation algorithms for a quantum generalization of Max-Cut, APPROX/RANDOM 2019. https://arxiv.org/abs/1909.08846
• J. Briët, F. M. de Oliveira Filho, F. Vallentin, The positive semidefinite Grothendieck problem with rank constraint, ICALP 2010. https://arxiv.org/abs/0910.5765
• S. Gharibian, J. Kempe, Approximation algorithms for QMA-complete problems, SIAM J. Comput. 41(4) (2012). https://arxiv.org/abs/1101.3884
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
• S. Piddock, A. Montanaro, The complexity of antiferromagnetic interactions and 2D lattices, arXiv preprint (2015). https://arxiv.org/abs/1506.04014
• E. Lieb, D. Mattis, Ordering energy levels of interacting spin systems, J. Math. Phys. 3 (1962). https://doi.org/10.1063/1.1724276

Motivation

A quantum computer that runs long computations must protect its data with a quantum error-correcting code and must compute on the encoded data without letting errors spread. The simplest gates with that property are transversal gates: a code is laid out in several code blocks, and a transversal gate couples each physical subsystem of one block only to the corresponding subsystem of the other blocks, so a single fault never becomes several faults inside one block (Gottesman 1997; Aliferis, Gottesman, Preskill 2006). Every known code has some encoded gate that is not transversal, and fault-tolerant schemes pay for the missing gates with expensive constructions such as magic-state distillation. Whether some code has a universal transversal gate set was a long-standing question.

Timeline.

• 2007: Zeng, Cross and Chuang show that transversal gates are not universal for stabilizer codes on qubits (arXiv:0706.1382).
• 2008: Chen, Chung, Cross, Zeng and Chuang extend this to stabilizer codes on qudits (arXiv:0801.2360).
• 2008–2009: Eastin and Knill prove the statement for every code that detects an arbitrary error on any single subsystem, stabilizer or not (arXiv:0811.4262; Phys. Rev. Lett. 102, 110502, 2009). This is the result of the present mission, now called the Eastin–Knill theorem.

Setting

A composite quantum system $\mathcal Q$ consists of finitely many physical subsystems $j$, subsystem $j$ having dimension $d_j$. Operators on $\mathcal Q$ are complex matrices on $\mathbb C^{d_1}\otimes\cdots\otimes\mathbb C^{d_n}$. A product operator is $\bigotimes_j U_j$ with $U_j$ acting on subsystem $j$, and $\mathcal T$ is the group of unitary product operators ($U_j \in \mathcal U(d_j)$).

A quantum code is a subspace of the state space, represented by the orthogonal projector $P$ onto it; its dimension $\operatorname{rank} P$ is the dimension of the encoded system, and the code is nontrivial when this dimension is at least $2$. An error $E$ is detectable when $PEP \propto P$. The code is local-error-detecting when every error on any single subsystem is detectable: $P\,(I\otimes E\otimes I)\,P \propto P$ for every operator $E$ acting on one subsystem.

A unitary $U$ is logical when it preserves the code space,

$$(I-P)\,U\,P = 0 \qquad \text{(Eq. (1))},$$

and $\mathcal G$ denotes the logical unitary product operators. An encoded unitary is a unitary operator $W$ of the code space ($PWP = W$, $W^\dagger W = WW^\dagger = P$). A set $S$ of unitaries is universal when every encoded unitary is approximated to arbitrary accuracy by the actions $PUP$, $U \in S$, on the code space.

For a code made of blocks $b$, each with subsystems at the same positions $j$ and a block code $P_b$, the joint code is $P = \bigotimes_b P_b$. The transversal part $j$ collects subsystem $j$ of every block, and a transversal unitary is a product of unitaries, one on each transversal part.

Formalization targets

Goal: Corollary 1

For block codes $P_b$, each local-error-detecting, with $\operatorname{rank}\bigotimes_b P_b \ge 2$, the set $\mathcal G$ of transversal logical unitaries is not universal:

$$\{\,W : PWP = W,\ W^\dagger W = WW^\dagger = P\,\}\ \not\subseteq\ \overline{\{\,PUP : U \in \mathcal G\,\}}.$$

Theorem 1 (milestone)

The same conclusion for product operators on the physical subsystems of a single local-error-detecting code with $\operatorname{rank} P \ge 2$.

Milestones on the way

In attack order: Lemma 1 (logical unitaries form a group); Lemma 2 (logical unitaries in a closed group of unitaries form a closed subgroup); $\mathcal T$ is a compact group; the derivative step $(I-P)DP = 0$; elements of the Lie algebra of $\mathcal T$ are sums of local Hermitian operators; $DP \propto P$ for a logical sum of local Hermitians; the identity component $\mathcal C$ of $\mathcal G$ acts on the code space as a scalar; $\mathcal G$ has finitely many actions on the code space up to phase; Theorem 1; and the detectability of an error on a single transversal part.

Significance

The result. The theorem rules out the simplest route to fault tolerance for every code that detects single-subsystem errors, which includes every code of distance at least $2$. It explains why every fault-tolerant architecture needs a non-transversal ingredient (state injection and distillation, code switching, gauge fixing, measurements with feed-forward), and it is the starting point for later refinements: approximate and covariant versions for continuous symmetries (Faist et al. 2020), and restrictions on the level of the Clifford hierarchy reachable transversally (Bravyi–König 2013).

Formalizing it. The result is proved; no machine-checked proof of it is known to exist. The mission produces a checked statement of the theorem for arbitrary finite-dimensional subsystems and arbitrary (non-stabilizer) codes, together with a reusable layer: tensor-product operators on index-typed subsystems, codes as projectors, logical operators, local error detection, encoded universality and block codes. Related platform items are QAlgorithms_Defs_QECC (qubit stabilizer codes, detectability for submodule codes) and QAlgorithms.GottesmanIntro.knillLaflamme (the error-correction criterion), which use a different model of codes and are not imported here.

Difficulty

The paper's argument runs through Lie theory: $\mathcal G$ is a closed subgroup of the compact group $\mathcal T$, so it is a compact Lie group with finitely many connected components; its identity component is generated by exponentials of its Lie algebra, and local error detection forces that Lie algebra to act on the code space by scalars. None of this is about the code alone; the difficulty is the passage from a closed matrix group to its Lie algebra and back (exponential coordinates, connectedness of the identity component, finiteness of the component group of a compact Lie group). Mathlib has the matrix exponential and compactness of the unitary group but not Cartan's closed-subgroup theorem or the Lie algebra of a closed matrix group.

A frequent first idea, that $\mathcal G$ itself is a finite group, is false: every global phase $e^{i\theta}I$ is a logical product unitary, so $\mathcal G$ always contains a circle. Only the action of $\mathcal G$ on the code space is finite, and only up to phase; a statement that ignores the phase is false.

Formalization scope

Subsystem $j$ is a finite index type $\alpha_j$ (so $d_j = |\alpha_j|$), and the system has basis $\prod_j \alpha_j$; operators are Matrix over ℂ, unitaries are Matrix.unitaryGroup. A code is its projector (Hermitian, idempotent) and its dimension is Matrix.rank; "nontrivial" is $2 \le \operatorname{rank} P$. Closure is in the standard topology on complex matrices, which is the topology of any norm. Exponentials are NormedSpace.exp with the factor $i$ of the physics convention (footnote 1).

Disclosed restatements:

1. "Lie group/Lie subgroup" (Lemma 2, $\mathcal T$) is stated as closed or compact subgroup; Cartan's theorem is not in Mathlib.
2. "$D$ in the Lie algebra" is stated through the one-parameter group $t\mapsto e^{itD}$.
3. The real coefficients $\alpha_j$ in $D = \sum_j \alpha_j H_j$ are absorbed into the Hermitian $H_j$.
4. The page's "the constant of proportionality must be one" is a slip (global phases lie in $\mathcal C$); the identity-component and finite-actions milestones state $CP \propto P$ and $GP = c\,FP$.
5. Corollary 1's code blocks are a tensor product of block codes $P_b$ with common positions $j$ and possibly different codes and dimensions; a single block is Theorem 1.

Universality is defined only through approximation of encoded unitaries, local error detection quantifies over every matrix on one subsystem, and $\mathcal G$ is the full intersection of $\mathcal T$ with the logical unitaries, so no hypothesis trivializes the conclusion; at rank $1$ the conclusion is false, which is why the rank hypothesis is $\ge 2$ and not $P \ne 0$.

A complete development needs the Lie algebra of a closed subgroup of Matrix.unitaryGroup, connectedness of the identity component via exponentials, and finiteness of the component group of a compact matrix group. These parts are reusable far beyond this mission, and contributions of them, as well as alternative proofs of Theorem 1 that avoid Lie theory, are welcome.

Selected references

• B. Eastin, E. Knill, Restrictions on Transversal Encoded Quantum Gate Sets, Phys. Rev. Lett. 102, 110502 (2009). https://arxiv.org/abs/0811.4262
• B. Zeng, A. Cross, I. L. Chuang, Transversality versus Universality for Additive Quantum Codes, IEEE Trans. Inf. Theory 57 (2011). https://arxiv.org/abs/0706.1382
• X. Chen, H. Chung, A. W. Cross, B. Zeng, I. L. Chuang, Subsystem stabilizer codes cannot have a universal set of transversal gates for even one encoded qudit, Phys. Rev. A 78, 012353 (2008). https://arxiv.org/abs/0801.2360
• D. Gottesman, Stabilizer Codes and Quantum Error Correction, PhD thesis, Caltech (1997). https://arxiv.org/abs/quant-ph/9705052
• S. Bravyi, R. König, Classification of topologically protected gates for local stabilizer codes, Phys. Rev. Lett. 110, 170503 (2013). https://arxiv.org/abs/1206.1609
• P. Faist et al., Continuous symmetries and approximate quantum error correction, Phys. Rev. X 10, 041018 (2020). https://arxiv.org/abs/1902.07714

Motivation

Arrival streams to service systems (call centres, hospitals, web servers) are rarely stationary: their rate changes with the time of day, with external events, or with the state of a self-exciting mechanism. Two asymptotic regimes are standard. When the rate varies slowly relative to service times, the system is approximated by a sequence of stationary systems, one per rate level (the pointwise stationary approximation). When the rate varies rapidly, the opposite simplification is expected: the fluctuations average out, and the arrival stream looks like a homogeneous Poisson process with the long-run average rate.

Zheng, Honnappa and Glynn (arXiv:1807.06805v1, published as a Technical Note in Operations Research, 2021) make the rapid regime precise for a general class of arrival processes. The arrival process need not be a doubly stochastic Poisson process; a Hawkes process is allowed. Their Theorem 1 says that, after a time acceleration combined with an independent thinning, the arrival process converges in law on path space to a Poisson process. The remaining results of the paper (total-variation behaviour, first-order corrections in the Markov-modulated case, the infinite-server queue) refine this limit and are not part of this mission.

Setting

A probability space $(\Omega,\mathcal F,P)$ carries a filtration $\mathcal F=(\mathcal F_t)_{t\ge0}$ and an arrival counting process $N=(N(t))_{t\ge0}$: $N(0)=0$, $N$ is integer valued, non-decreasing and right-continuous, and it is simple, meaning that it increases by exactly one at each arrival epoch. $N$ has an $\mathcal F$-compensator $A=(A(t))_{t\ge0}$: a predictable process with $A(0)=0$ and non-decreasing right-continuous paths such that

$$M(t)=N(t)-A(t)$$

is an $\mathcal F$-martingale. When $A(t)=\int_0^t\lambda(s)\,ds$, the process $\lambda$ is the stochastic intensity of $N$.

Assumption 1. There is a deterministic $\lambda^*\in(0,\infty)$ with $A(t)/t\Rightarrow\lambda^*$ as $t\to\infty$.

For $0<\varepsilon\le1$, let $\beta^\varepsilon=(\beta^\varepsilon_i)_{i\ge1}$ be iid Bernoulli($\varepsilon$) random variables independent of $N$. The thinned, accelerated process and its scaled compensator are

$$N_\varepsilon(t)=\sum_{i=1}^{N(t/\varepsilon)}\beta^\varepsilon_i,\qquad A_\varepsilon(t)=\varepsilon A(t/\varepsilon).$$

$N_\varepsilon$ runs $N$ at speed $1/\varepsilon$ and keeps each arrival independently with probability $\varepsilon$, so the mean rate stays of order $\lambda^*$ while the intensity $\lambda_\varepsilon(t)=\lambda(t/\varepsilon)$ fluctuates on the time scale $\varepsilon$. The σ-algebra $\mathcal G^\varepsilon_t$ is generated by $\mathcal F_{t/\varepsilon}$ and the marks $\beta^\varepsilon_i$ of the arrivals $1\le i\le N(t/\varepsilon)$ that have occurred.

$D[0,\infty)$ is the space of right-continuous real paths on $[0,\infty)$ with left limits, with the Skorokhod $J_1$ topology.

Formalization targets

Goal: Theorem 1 (p. 4)

Under Assumption 1,

$$N_\varepsilon\Rightarrow N_0\quad\text{in }D[0,\infty)\text{ as }\varepsilon\downarrow0,$$

where $N_0$ is a Poisson process with constant intensity $\lambda^*$. The goal fixes no rate of convergence and no constants; it asserts convergence in law on path space and the identity of the limit.

Milestones

1. §2, p. 3. $N_\varepsilon$ is a simple point process: every path is a counting path with unit jumps, and each $N_\varepsilon(t)$ is a random variable.
2. §2, p. 3. $A_\varepsilon$ is the $\mathcal G^\varepsilon$-compensator of $N_\varepsilon$:

$$E\big[N_\varepsilon(t+s)-A_\varepsilon(t+s)\,\big|\,\mathcal G^\varepsilon_t\big]=N_\varepsilon(t)-A_\varepsilon(t),\qquad s,t\ge0 .$$

3. Proof of Theorem 1, p. 4. For each $t\ge0$, $A_\varepsilon(t)\to\lambda^*t$ in probability as $\varepsilon\downarrow0$.
4. Theorem 13.4.IV of Daley and Vere-Jones (1988), as the proof applies it: if simple counting processes $N_n$ have compensators $A_n$ (each with respect to its own filtration) with $A_n(t)\to\lambda t$ in probability for every $t$, then $N_n\Rightarrow$ Poisson($\lambda$) in $D[0,\infty)$.

Significance

Theorem 1 justifies replacing a rapidly fluctuating arrival stream by a homogeneous Poisson stream of rate $\lambda^*$ in the analysis of the system it feeds. If $Z$ collects the other primitives of a queue (service and patience times) and is independent of $N_\varepsilon$, then $(Z,N_\varepsilon)\Rightarrow(Z,N_0)$, and any performance functional continuous at $(Z,N_0)$ converges to its value under Poisson input (p. 4). The second half of the paper shows that this approximation holds in law on path space but not in total variation, which is why the $J_1$ statement is the right form of the result.

The result is proved on paper, in two lines that cite a general limit theorem. No part of it has been machine-checked. This mission produces the first formal statement and proof of a Poisson limit for point processes driven by their compensators, the cited theorem (milestone 4), which applies well beyond this paper: superposition limits, rare-event thinning, and Hawkes-process limits all reduce to it. Milestone 2 is a reusable thinning lemma for compensators.

Difficulty

Milestones 1 and 3 are elementary: the first is pathwise, the second is a time change in Assumption 1. Milestone 2 is a conditional-expectation computation with a random number of summands, and needs the marks to be independent of all the information in $\mathcal F_\infty$, not only of $N$ (see the scope section).

The difficulty is milestone 4. Convergence of the compensators at each fixed time identifies the limit only through a martingale characterisation of the Poisson process (Watanabe's theorem). Path-space convergence additionally needs $J_1$ tightness of the counting processes. Finite-dimensional convergence of $N_\varepsilon$ is not enough: the statement is about laws on $D[0,\infty)$, and the step from fixed times to path space is part of the work. The goal also does not follow from milestones 1 to 4 verbatim: the goal assumes the marks independent of $N$ only and does not assume $E\,N(t)<\infty$, while milestone 2 needs both stronger hypotheses.

Formalization scope

All declarations live in the namespace RapidRatePoisson.WeakConv. Conventions:

• Time and $\varepsilon$ are ℝ≥0. Every statement involving $t/\varepsilon$ assumes $\varepsilon>0$. Processes are ℝ≥0 → Ω → ℝ. Marks are ℕ → Ω → Bool, indexed from 1, and markSeq β is the random sequence $(\beta_1,\beta_2,\dots)$.
• "Simple counting process" is the published MartingaleHT.InfiniteServer.IsUnitJumpCountingPath, required of every path.
• The compensator is the predictable one, with $A(0)=0$ (IsCompensator: Mathlib's IsStronglyPredictable and Martingale with respect to a Filtration ℝ≥0). This is the standard meaning of the term. The page's paraphrase without predictability makes Theorem 1 false: for $N$ Poisson(1) and $A=t/2+J$, with $J$ an independent increasing pure-jump process of mean $t/2$ with finitely many jumps, $N-A$ is a martingale and $A(t)/t\to1/2$, but $N_\varepsilon$ is Poisson(1) for every $\varepsilon$.
• Assumption 1's "⇒" to a constant is convergence in probability (Mathlib's TendstoInMeasure).
• "⇒ in $D[0,\infty)$" is the published coupling-form PuhaWardFluid.Limit.ConvInDist with $J_1$ on real paths, which is equivalent to weak convergence of the laws. "As $\varepsilon\downarrow0$" is stated along every sequence $\varepsilon_n\to0$ in $(0,1]$, which is equivalent by metrizability. The limit $N_0$ ranges over every process satisfying the published RankBasedSDI.LoadBalancing.IsPoissonProcess with rate $\lambda^*$ on any probability space.
• "Independent of $N$" in the goal is independence of markSeq (β ε) from the whole path of $N$, for each $\varepsilon$ separately.
• Milestone 2 adds two disclosed hypotheses: the marks are independent of $\bigvee_t\mathcal F_t$, and $E\,N(t)<\infty$. The first is needed because the page's own step that replaces $\mathcal G^\varepsilon_t$ by $\mathcal F_{t/\varepsilon}$ fails otherwise (a mark built from an $\mathcal F_0$ coin and the parity of $N(1)$ is independent of $N$, yet it reveals the future). The second is needed because a martingale $N-A$ does not make $N(t)$ integrable.
• Milestone 4's statement is the form the proof applies; the paper does not print it.

The trivialising readings are ruled out. The goal is convergence in $D[0,\infty)$ with $J_1$, not finite-dimensional or one-time-marginal convergence. The limit carries the Poisson predicate and is not an arbitrary process. The compensator is predictable, not the literal "increasing process making $N-A$ a martingale". A sorry-free check (not uploaded) shows the goal's hypotheses can be met together: the deterministic instance $N=A=\lfloor t\rfloor$ with the trivial filtration, $\lambda^*=1$, and uniform marks on $[0,1]^{\mathbb N}$.

Needed infrastructure: martingale characterisation of the Poisson process, $J_1$ tightness criteria for counting processes, and conditional expectation over random index sets. All of it is reusable beyond this mission. Contributions to milestone 4 and its supporting lemmas are especially welcome.

Selected references

• Z. Zheng, H. Honnappa, P. W. Glynn, Approximating Systems Fed by Poisson Processes with Rapidly Changing Arrival Rates, Operations Research (Technical Note), 2021; preprint arXiv:1807.06805v1, 2018. https://arxiv.org/abs/1807.06805
• D. J. Daley, D. Vere-Jones, An Introduction to the Theory of Point Processes, Springer, 1988 (Theorem 13.4.IV). https://doi.org/10.1007/978-1-4757-2001-3
• T. C. Brown, A martingale approach to the Poisson convergence of simple point processes, Annals of Probability 6(4), 615–628, 1978. https://doi.org/10.1214/aop/1176995481
• O. Kallenberg, Foundations of Modern Probability, Springer, 1997. https://doi.org/10.1007/b98838
• S. N. Ethier, T. G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986. https://doi.org/10.1002/9780470316658

Motivation

In a fork-join network every arriving job is split into several tasks that are processed in parallel and then joined; the job leaves only when its last task is done. Such networks model parallel computing (map-reduce jobs split across machines), assembly and order fulfilment (an order waits for every component), and health care (a patient waits for several test results). When different job types compete for the same parallel resources, the order in which a shared resource serves the types determines how long jobs wait for their slowest task, and therefore how many jobs are in the system.

Optimal control of such networks is hard even with exponential distributions, because the state is the vector of all buffer contents and the dimension grows with the number of types and servers. E. Özkan (arXiv:2002.01496, Mathematics of Operations Research 2022) studies the problem in the conventional heavy-traffic diffusion regime, in which every shared server is critically loaded, and proposes a scheduling policy that tracks the solution of a linear program. The main result is that the policy is asymptotically optimal for the probability that the total holding cost exceeds any threshold. The approach generalizes the network of Figure 2 with a single shared server, controlled by Özkan and Ward (Mathematics of Operations Research 44, 2019), and follows the asymptotic-optimality programme of Bell and Williams (doi:10.1214/aoap/1015345343).

Setting

There are $J\ge1$ job types $\mathcal J$, $I$ shared servers $\mathcal I$ and a set of dedicated servers. Shared server $i$ processes the types $\mathcal J_i$, $|\mathcal J_i|\ge2$; type $j$ is processed by the shared servers $\mathcal I_j\neq\emptyset$ and by its own dedicated servers $\mathcal K_j$ (possibly none). A type-$j$ job forks into one task per server in $\mathcal K_j\cup\mathcal I_j$. Inter-arrival times of type $j$ are $\bar u_{jn}/\lambda_j$ with $\bar u_{jn}$ i.i.d., mean $1$ and variance $\beta_j^2$; service times are i.i.d. with means $1/\mu_k$, $1/\mu_{ij}$ and squared coefficients of variation $\sigma_k^2$, $\sigma_{ij}^2$; all sequences are independent and have exponential moments (Assumption 1).

Let $Q_k(t)$ and $Q_{ij}(t)$ be the numbers of tasks waiting in front of dedicated server $k$ and of shared server $i$ (type $j$). The number of type-$j$ jobs in the system is $N_j=\max_{k\in\mathcal K_j}Q_k\vee\max_{i\in\mathcal I_j}Q_{ij}$, and the cost rate is $\sum_jh_jN_j$ with $h_j\ge0$. The control is how each shared server divides its effort among its buffers: an admissible policy is head-of-line within each buffer and work-conserving, and it may even anticipate the future (Definition 1).

A sequence of systems indexed by $r$ has arrival rates $\lambda^r_j\to\lambda_j$ with every shared server in heavy traffic, $\sum_{j\in\mathcal J_i}\lambda_j/\mu_{ij}=1$ and $r(\sum_{j\in\mathcal J_i}\lambda^r_j/\mu_{ij}-1)\to\theta_i$, while each dedicated server is either in heavy traffic, $r(\lambda^r_j-\mu_k)\to\theta_k\in\mathbb R$ (the set $\mathcal K^H$), or in light traffic, $\to-\infty$ (Assumption 2). All systems start empty. Diffusion scaling is $\hat N^r_j(t)=N^r_j(r^2t)/r$, and similarly $\hat Q^r_k$ and the workload $\hat W^r_i$ with $W^r_i=\sum_{j\in\mathcal J_i}Q^r_{ij}/\mu_{ij}$.

For $b=(q_k;w_i)\ge0$ the LP (18) minimizes $\sum_jh_jy_j$ subject to $y_j\ge q_k$ ($k\in\mathcal K_j$), $y_j\ge q_{ij}\ge0$ and $\sum_{j\in\mathcal J_i}q_{ij}/\mu_{ij}=w_i$; its value is $z(b)$. The QP (19) picks the LP optimum of least Euclidean norm. The proposed policy (Definition 2) works in review periods: at the start of a period server $i$ computes the QP-selected target $q^*_{ij}$ for the current state. If no buffer exceeds $\lceil q^*_{ij}\rceil$, the server serves one job. Otherwise it serves the excess jobs while idling one type $m$ that maximizes $(q^*_{im}-Q_{im})/\lambda_m$, until no excess is left.

Formalization targets

Goal: Theorem 2 (p. 16)

With $(\tilde Q_k,\tilde W_i)$ the limit of Proposition 2 — a semimartingale reflected Brownian motion (SRBM) with data $(\mathbb R^{a_1}_+,\Theta,\Sigma,R,0)$ in the heavy-traffic coordinates and $\tilde Q_k=0$ for light-traffic dedicated servers — for every run of the proposed policy, every $\epsilon>0$ and every $t\ge0$,

$$\lim_{r\to\infty}\mathbf P\Big(\sum_{j}h_j\hat N^r_j(t)>\epsilon\Big)=\mathbf P\big(z(\tilde Q(t),\tilde W(t))>\epsilon\big).$$

Milestones

1. Lemma 1 Parts 1–3 and Lemma 2: the LP (18) represents the cost; $z$ is Lipschitz; the QP has a unique solution, Lipschitz in $b$, also pathwise.
2. Proposition 2: under every admissible policy $(\hat Q^r_k,\hat W^r_i)\Rightarrow(\tilde Q_k,\tilde W_i)$.
3. Lemma EC.1.2 and Lemma 5: exponential tail bounds for partial sums and for arrival and service processes after the review epochs.
4. Lemma 4: with probability tending to one every review period in $[0,r^2T]$ is short and stable, and ends near the target.
5. Proposition 3: $\|\sum_jh_j\hat N^r_j-z(\hat Q^r,\hat W^r)\|_T\to0$ in probability under the proposed policy.

Significance

Theorem 2, together with the lower bound of Theorem 1 (which holds for every admissible policy and is not part of this mission), shows that the proposed policy is asymptotically optimal for the objective $\mathbf P(\sum_jh_jN_j(t)>\epsilon)$ simultaneously for all $\epsilon$ and $t$. The paper then derives asymptotic optimality for the discounted cost (Theorem 3). The policy needs only the solution of an LP and a QP at review epochs, so it scales to large networks where dynamic programming does not.

The results are proved in the paper, with the exception of Proposition 2, whose proof is omitted as following "from standard methodology"; its milestone is therefore a statement the paper asserts. None of the results is formalized. A formal development would produce reusable pieces: Lipschitz sensitivity of LP values and of minimum-norm LP solutions, Chernoff-type bounds for maxima of i.i.d. partial sums, and a precise model of a fork-join network under head-of-line, work-conserving control.

Difficulty

The cost $\sum_jh_jN_j$ is not a function of the workloads alone, so the usual heavy-traffic argument (diffusion limit of the workload plus a continuous mapping) only gives a lower bound. Achieving it requires state-space collapse for the cost: the buffers in front of each shared server must stay within $o(r)$ of the LP-optimal split at all times up to $r^2T$, under a policy whose review periods are random and whose target moves with the state. The proof controls up to $M^r=O(r^2)$ review periods per server at once, which needs tail bounds of order $r^ke^{-Cr}$ uniformly over periods. The light-traffic behaviour of a shared server that idles one type during a Step-3 period depends on heavy traffic of the full server. The natural shortcut — proving tightness of the scaled buffers directly — fails, because the LP may have many optimal solutions; the QP selection and its Lipschitz property (Lemma 1 Part 3) are what make the target trackable.

Formalization scope

• Indices are Fin J, Fin I, Fin K (0-based); dedicated servers carry an owner map, and the standing structure ($|\mathcal I_j|\ge1$, $|\mathcal J_i|\ge2$, $\max_jh_j>0$, positive rates) is part of the Network definition. Sums over $\mathcal J_i$ and maxima over $\mathcal I_j$ range over incident pairs only.
• Time is real ($t\ge0$); the systems are indexed by $r\in\mathbb N$. Counting processes are $\mathbb N$-valued suprema of partial sums. Review epochs take values in $[0,\infty]$.
• A run satisfies the dynamics (2)–(7) of Definition 1 and the empty start for almost every sample path. Work conservation (6) is encoded pathwise on intervals.
• $z(b)$ is the infimum of the LP objective; the QP optimum is a predicate, never a choice function. The policy is encoded with the paper's arbitrary choices left existential. "In an admissible and non-preemptive way" is read as: only buffers in excess of $\lceil q^*_{ij}\rceil$ are served, the idled type is not served, and no two jobs are in partial service at once.
• The SRBM uses the published definitions Reiman84.QueueLength.IsDriftedBM and IsReflectionPair; since $R$ is a positive diagonal matrix it is absorbed into the regulator. Weak convergence in Proposition 2 is the published PuhaWardFluid.Limit.ConvInDist.
• Added hypotheses: Assumptions 1–2 and the empty start everywhere; $\Sigma$ positive definite (asserted on p. 10) in Theorem 2 and Proposition 2; finite second moments of the primitives. No continuity-point hypothesis $\mathbf P(z=\epsilon)=0$ is added to Theorem 2.
• Trivializing formalizations are excluded: the goal is stated for every run of the policy and every SRBM realization (not for some), the policy predicate imposes only the rules of Definition 2, $z$ and $q^*$ are the LP value and the QP minimizer, and all constants in Lemmas 4, 5 and EC.1.2 are chosen before $r$.
• Not posed: Theorems 1 and 3, Proposition 1, Lemma 3, Lemmas 6–8, display (35) and §6. Contributions of the LP/QP sensitivity results and of the Chernoff bounds are useful beyond this mission.

Selected references

• E. Özkan, Control of Fork-Join Processing Networks with Multiple Job Types and Parallel Shared Resources, arXiv:2002.01496v1, 2020; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2002.01496
• E. Özkan, A. R. Ward, On the control of fork-join networks, Mathematics of Operations Research 44:532–564, 2019.
• S. L. Bell, R. J. Williams, Dynamic scheduling of a system with two parallel servers in heavy traffic with resource pooling: asymptotic optimality of a threshold policy, Annals of Applied Probability 11:608–649, 2001. https://doi.org/10.1214/aoap/1015345343
• R. J. Williams, An invariance principle for semimartingale reflecting Brownian motions in an orthant, Queueing Systems 30:5–25, 1998.
• W. Whitt, Stochastic-Process Limits: An Introduction to Stochastic-Process Limits and Their Application to Queues, Springer, 2002.

Motivation

A controller watches a one-dimensional random state $X$ (an inventory level, a cash reserve, an exchange rate) and may push it upward at any time, paying a proportional cost $C$ per unit of push. A running cost $f(U_t)$ is paid on the controlled state $U$. Minimizing the discounted sum of the two costs is the classical singular control problem, called singular because the optimal push is typically not absolutely continuous in time. Since Beneš, Shepp and Witsenhausen (1980) the expected answer has been a barrier strategy: reflect the state at a fixed lower level $b^*$ and do nothing above it.

For Brownian motion and diffusions this is well understood. For processes with jumps, the known proofs rely on the scale function of a spectrally one-sided Lévy process (jumps of one sign only). Yamazaki (Math. Oper. Res. 2017) solved the spectrally negative case this way. Financial and inventory data have jumps of both signs, and for a general Lévy process no scale function exists. Noba and Yamazaki (arXiv:2008.03021, Math. Oper. Res. 2023) prove that a barrier strategy is still optimal for a general Lévy process when the running cost is convex, and that the optimal barrier solves one explicit equation.

Setting

Let $X=(X_t)_{t\ge0}$ be a real Lévy process with $X_0=0$, described by its triplet $(\gamma,\sigma,\Pi)$: $\mathbb E[e^{iuX_t}]=e^{-t\Psi(u)}$ with

$$\Psi(u)=-i\gamma u+\tfrac12\sigma^2u^2+\int_{\mathbb R\setminus\{0\}}\big(1-e^{iuz}+iuz\,1_{\{|z|<1\}}\big)\,\Pi(dz).$$

Under $\mathbb P_x$ the process starts at $x$, i.e. it is $x+X$.

A strategy is a nondecreasing, right-continuous process $R$ adapted to the natural filtration of $X$, with $R_{0-}=0$; an initial jump $R_0>0$ is allowed. The controlled process is $U_t=X_t+R_t$ (2.2). For a discount rate $q>0$, a unit cost $C\in\mathbb R$ and a running cost $f$, the cost of $\pi=R$ from $x$ is

$$v_\pi(x)=\mathbb E_x\Big[\int_0^\infty e^{-qt}f(U_t)\,dt+C\int_{[0,\infty)}e^{-qt}\,dR_t\Big]\qquad(2.3),$$

and $\pi$ is admissible if the same expectation with $|f|$ in place of $f$ and without $C$ is finite (2.4). The value function is $v(x)=\inf_\pi v_\pi(x)$.

The barrier strategy at $b$ is $R^b_t=-\inf_{s\le t}\{(X_s-b)\wedge0\}$; then $U^b$ is $X$ reflected at the lower barrier $b$, and its cost is $v_b(x)$ (3.6). With $f'_+$ the right derivative of $f$ and $U^0$ the process reflected at $0$ and started at $0$, set

$$\rho(b)=\mathbb E\Big[\int_0^\infty e^{-qt}f'_+(U^0_t+b)\,dt\Big]\ (3.9),\qquad b^*=\inf\{b\in\mathbb R:\rho(b)+C\ge0\}\ (3.8).$$

Standing assumptions: $f$ is convex, of polynomial growth, and $f'_+(-\infty)<-Cq<f'_+(\infty)$ (Assumption 1); $\int_{\mathbb R\setminus(-1,1)}e^{\bar\theta|z|}\Pi(dz)<\infty$ for some $\bar\theta>0$ (Assumption 2(ii)).

Formalization targets

Goal: Theorem 2 (p. 13)

For every starting point $x$, the barrier strategy at $b^*$ is admissible and

$$v_{\pi^{b^*}}(x)\le v_\pi(x)\qquad\text{for every strategy }\pi\text{ admissible from }x,$$

under Assumptions 1 and 2(ii) only. The paper first assumes $X$ is not a driftless compound Poisson process (Assumption 2(i)) and, for unbounded variation, that $f\in C^2$ with $f''$ of polynomial growth (Assumption 3); §4.2 and §5 remove both, and the goal carries neither.

Milestones

The fifteen milestones follow the paper's proof:

• the barrier strategies and $b^*$: Lemmas 2–4, the finiteness of $b^*$ (p. 6), Lemma 6 (derivative of $v_b$ in the barrier), Theorem 1 (optimality among barriers), Lemma 8 (convexity, $C^1$ and smooth fit of $v_{b^*}$), Lemma 9;
• verification: Proposition 1 (the verification lemma) and Lemmas 10–11 (the variational inequality for $v_{b^*}$);
• the approximation of §4.2: Lemmas 12, 14, 15;
• the compound Poisson case of §5: Lemma 16.

Significance

The theorem gives a complete solution, for all Lévy processes with exponential moments, of the singular control problem with convex running cost: the optimal policy is a barrier, and the barrier is the root of a monotone function of $b$. It contains the Brownian, spectrally negative and spectrally positive cases, and processes of bounded and unbounded variation, subordinators and compound Poisson processes. Because $\rho$ depends only on the law of the reflected process $U^0$, $b^*$ can be computed by Monte Carlo or, when the Wiener–Hopf factorization is known, by transform inversion (Remark 4).

The result is proved in the paper; it has no machine-checked proof. Formalizing it requires a Lévy-process layer that Mathlib does not yet have: reflected Lévy processes, first-passage times, and an Itô formula for semimartingales with jumps used against Lebesgue–Stieltjes integrators. The milestones isolate statements that do not need all of it: Lemma 12 is real analysis about a smoothed convex function, Theorem 1 compares barrier strategies only, and Proposition 1 is a reusable verification lemma for singular control.

Difficulty

The standard route computes $v_b$ in closed form, picks $b^*$ by smooth fit, and checks the variational inequality. For a general Lévy process $v_b$ has no closed form: the scale function, which carries the one-sided proofs, does not exist when jumps of both signs are present. The paper works instead with derivatives of $v_b$ with respect to the barrier, expressed through the first down-crossing time $\tau^-_b$ (Lemma 6). This needs the regularity of $0$ for $\mathbb R\setminus\{0\}$, which fails for driftless compound Poisson processes, hence the separate treatment of §5. In the unbounded-variation case, $v_{b^*}$ is $C^2$ only if $f$ is, so the verification lemma cannot be applied directly. The paper smooths $f$, solves the smoothed problems, and passes to the limit through the barriers $b^*_{(\varepsilon)}$ and the values $v^{(\varepsilon)}$ (Lemmas 14–15).

Formalization scope

Two definition files. SingCtrlLevy.Barrier.Levy gives the triplet, $\Psi$, the Lévy process (measurable, $X_0=0$, independent and stationary increments, càdlàg paths, characteristic function $e^{-t\Psi}$), bounded variation, the driftless compound Poisson triplet, Assumptions 2(ii) and 3, the classes $C^n_{\mathrm{poly}}$ and the generator $\mathcal L$. SingCtrlLevy.Barrier.Model gives strategies, the cost, the barrier strategy, $\rho$, $b^*$, $\tau^-_b$, Assumption 1, the smoothing $f^{(\varepsilon)}$ of (4.35) and $X^{[\varepsilon]}_t=X_t+\varepsilon t$.

Conventions:

• One probability space with $X_0=0$; $\mathbb P_x$ is the law of $x+X$.
• Time is $\mathbb R_{\ge0}$; time integrals are over $[0,\infty)$.
• Admissibility is per starting point: the barrier strategy from $x$ has $R^b_0=(b-x)^+$, so the admissible set is read as strategies chosen for the start $x$ with (2.4) at that $x$.
• $dR$ is the Lebesgue–Stieltjes measure of the path extended by $0$ to negative times, so the initial jump $R_0$ is charged at $t=0$.
• (2.4) is a lower Lebesgue integral in $[0,\infty]$; costs are Bochner integrals, genuine exactly under (2.4).
• $v$ is valued in the extended reals; $\tau^-_b$ is valued in $[0,\infty]$, with $e^{-q\infty}=0$.
• $f'_\pm$ are one-sided derivatives; Assumption 1(iii) is written as "some $f'_+(y)<-Cq$ and some $f'_+(y)>-Cq$", equivalent to the limit form since $f'_+$ is nondecreasing.
• Milestones of §§2–4 carry Assumption 2(i), standing until the end of §4. Lemmas 9, 14 and 15 carry unbounded variation (the scope of §4.2, and of Assumption 3 in Lemma 9). Lemma 16 carries the driftless compound Poisson hypothesis instead of Assumption 2(i).

$b^*$ is the infimum of the set $\{b:\rho(b)+C\ge0\}$, never "the optimal barrier", and $\pi^{b^*}$ is the explicit reflection at $b^*$. The goal ranges over every nondecreasing, right-continuous, adapted strategy satisfying (2.4), and the value function is never replaced by a junk infimum. None of the three trivializes the statement.

Welcome contributions: measurability and integrability lemmas for reflected Lévy processes, first-passage regularity (Lemma 1 of the paper), an Itô formula for $C^2$ functions of Lévy processes plus nondecreasing càdlàg controls, and the real-analysis lemmas on $f^{(\varepsilon)}$. The Lévy layer and the verification lemma can be reused beyond this mission.

Selected references

• K. Noba and K. Yamazaki, On singular control for Lévy processes, Mathematics of Operations Research, 2023; arXiv:2008.03021v3 (2022). https://arxiv.org/abs/2008.03021
• K. Yamazaki, Inventory control for spectrally positive Lévy demand processes, Mathematics of Operations Research 42(1), 212–237, 2017. https://doi.org/10.1287/moor.2016.0802
• V. E. Beneš, L. A. Shepp and H. S. Witsenhausen, Some solvable stochastic control problems, Stochastics 4(1), 39–83, 1980. https://doi.org/10.1080/17442508008833156
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-3-642-37632-0
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005. https://doi.org/10.1007/978-3-662-10061-5

Motivation

Many goods are maintained by several parties at once: a shared infrastructure, a fishery, an industry's reputation, a public research base. Each party bears the full cost of its own investment while every party enjoys the benefit, so each prefers that someone else pay. This free rider problem is classically studied as a war of attrition, and continuous-time versions are a standard tool in operations research for timing decisions under uncertainty.

Kim and Kwon (arXiv:2208.11217, published in Operations Research, 2024) model the stock of the common good as a declining diffusion and let two players invest in it at fixed plus proportional cost. Their point concerns the stability of mixed strategy equilibria, in which players randomize the time of investment. When the good can be invested in only once, Georgiadis, Kim and Kwon (Games and Economic Behavior 131, 2022) showed that any asymmetry in costs destroys the mixed equilibrium; Theorem 1 of the present paper recovers this. When investment can be repeated indefinitely, an impulse control game, the paper shows that a mixed equilibrium survives moderate asymmetry. The verification argument extends the single-player impulse control analysis of Alvarez and Lempa (SIAM Journal on Control and Optimization 47(2), 2008) to a randomized two-player setting.

Setting

The stock $X$ lives on an interval $\mathcal I=(a,b)$ with $a>-\infty$ and, absent investment, solves $dX_t=\mu(X_t)\,dt+\sigma(X_t)\,dW_t$ with $\mu<0<\sigma$, natural boundaries, Lipschitz coefficients with linear growth, and the transversality condition $\mathbb E_x[|X_t|e^{-rt}]\to0$. Write $\mathcal Af=\tfrac12\sigma^2f''+\mu f'-rf$, let $\psi$ and $\varphi$ be the increasing and decreasing positive solutions of $\mathcal Af=0$, and let $(R_r\pi)(x)=\mathbb E_x\int_0^\infty\pi(X_t)e^{-rt}dt$ for the common flow profit $\pi$, continuous and increasing.

Player $i\in\{1,2\}$ may invest at any time, paying $c_i+k\zeta$ to raise the stock by $\zeta\ge0$, with $c_1>c_2>0$ and $k>0$. Time is split into periods, each ending at an investment. Players randomize through a uniform randomizer per player and period: an investment occurs when a survival process $M^{(i)}_{m,t}$ falls below the randomizer. Simultaneous attempts are settled by a fair coin. Player $i$'s payoff is the expected discounted profit minus its own discounted investment costs, (22).

The profile $\nu^*$ has threshold $\theta^*$, atom probability $q$ and targets $z_1,z_2$. In the first stage of a period, player 1 waits and player 2 invests with probability $q$ when the stock reaches $\theta^*$ from above. In the second stage each player $i$ invests at hazard rate $\lambda_i(X_t)$, positive exactly on the common mixed region $\Gamma=(a,\theta^*)$. Every investment by player $i$ raises the stock to $z_i$. With $I(x)=((R_r\pi)'(x)-k)/\varphi'(x)$ and $J(x)=(R_r\pi)(x)-kx-I(x)\varphi(x)$, Assumption 5 states that $\theta^*<z_2$ solve $I(z_2)=I(\theta^*)$ and $J(z_2)-J(\theta^*)=c_2$. These are the single-player optimal thresholds for cost $c_2$.

Formalization targets

Goal: Theorem 3

Under the standing assumptions and Assumptions 1, 2, 4 and 5, there is $\hat c>c_2$ such that for every $c_1\in(c_2,\hat c)$ there are $z_1$ and $q$ with

$$0<q<1,\qquad \theta^*<\hat x<z_1<z_2,$$

together with payoff functions satisfying the §4.2 conditions, such that $\nu^*(\theta^*,z_1,z_2,q)$ with the rates (29) is a subgame perfect equilibrium. Here $\hat x$ is the minimizer of $I$ (Lemma 2). The goal leaves $\hat c$ unquantified, as the paper does: the §4.4 example gives $\hat c\approx0.01729$ for $c_2=0.015$.

Milestones

Lemma 2 (shape of $I$, $J$) and identity (B.20); Lemma B.8 (i) and (ii) (closed-form payoff functions satisfy the §4.2 conditions); Lemmas B.7 and B.6 and Theorem 2 (the verification theorem); Lemma B.8 (scalar conditions (B.21)–(B.23) suffice); parts (i) and (ii) of the proof of Theorem 3 (the scalar conditions hold for $c_1$ near $c_2$).

Significance

The result shows that the instability of mixed equilibria in timing games of public good provision is an artefact of one-shot investment. With repeated investment, player 2 can promise a probability $q$ of investing at $\theta^*$, which raises player 1's continuation value and pulls player 1's investment threshold to $\theta^*$, so that both players share the same mixed region. Theorem 2 is, to the authors' knowledge, the first verification theorem for a mixed strategy equilibrium of an impulse control game. Proposition 7 of the paper compares this equilibrium with a pure strategy one from a social planner's view, and it presupposes Theorem 3.

Theorem 3 and its lemmas are proved in the paper. None of it is formalized in any proof assistant. A formalization would provide a machine-checked randomized impulse game, with periods, survival processes, tie coins and deviations adapted to a player's own information. It would also provide a verification theorem in that setting and the real-analysis chain behind the explicit construction. The diffusion layer reuses the published definitions of Kwon's variable contributions game (same authors, same model).

Difficulty

The analytic half (Lemma 2, Lemma B.8, the proof of Theorem 3) is real analysis on $\varphi$, $R_r\pi$, $I$ and $J$. Its delicate point is the global maximum of $\hat U_1(z)-kz$: the local maximum at $z_1$ beats the boundary value at $\theta^*$ only under (B.23), which holds only for $c_1$ close to $c_2$.

The verification half is the hard part. The obvious approach, a Dynkin formula on $[0,\infty)$ for the candidate payoff, does not apply. The opponent's investments arrive at a state-dependent hazard rate, so the argument must kill the process at that rate within each period and then sum the per-period identities. The limit over periods needs monotone convergence, using $T_m\to\infty$ and the lower bound $\pi\ge\pi_L$. Player 2's atom at $\theta^*$ creates a discontinuity in time of player 1's payoff, and a deviation by player 1 at exactly that instant produces a tie whose expected value must be bounded with the boundary condition $U_1(\theta^*)=qU_1(z_2)+(1-q)V_1(\theta^*)$.

Formalization scope

The Lean development uses the published VarContrib.RegularMPE.Model, Setting (μ, σ, π, k, r, I, x₀, the generator gen, the resolvent R, the controlled state equation IsStateSol) and EthierKurtz.HasBrownianItoIntegral. Everything else lives in the namespace InvestCommonGood.MixedTSSPE, in three definition files. Model holds $S'$, $m'$, $L$, $I$, $J$, the standing assumptions and Assumptions 1, 2, 4, 5. Game holds the randomizers, plays, $\nu^*$, deviations, the payoff (22) and the SPE. Conditions holds the §4.2 conditions, (28), (29) and the closed forms of Lemma B.8.

Committed conventions:

• players are 0 (player 1) and 1 (player 2); times are ℝ≥0, and random times are WithTop ℝ≥0, where ⊤ means never;
• the cumulative hazard takes values in $[0,\infty]$;
• the SPE is read as a Nash equilibrium of the subgame from every state $x\in\mathcal I$ and either stage;
• a deviating player sees the controlled path and its own randomizers, but not the opponent's randomizers or the coins;
• payoffs are compared only when the profit is integrable and the cost series is summable with an integrable sum;
• every equilibrium statement holds for every play satisfying the play relations, and the existence of plays (solutions of the controlled state equation) is not posed.

Standing hypotheses beyond the printed text, each used by the paper without proof:

• $R_r\pi\in C^2(\mathcal I)$ with $\mathcal A(R_r\pi)+\pi=0$;
• the resolvent representation (B.19);
• the hitting-time normalization of $\varphi$ and $\psi$.

Pinned readings: Assumption 5 includes $\theta^*<z_2$, and Assumption 4 includes the convergence of $\int_x^b\varphi\rho m'$. The §4.2 conditions include positivity of the denominators of (29) on $(a,\theta^*)$.

The goal concludes the equilibrium property of the randomized game itself. "There exist $z_1$, $q$ satisfying (B.21)–(B.23)" or "the §4.2 conditions are satisfiable" are milestones, not substitutes for the goal. Contributions are welcome on either half: the real-analysis chain is self-contained, and the verification lemmas are reusable for other randomized timing games.

Selected references

• Y. Kim, H. D. Kwon, Investment in the common good: free rider effect and the stability of mixed strategy equilibria, arXiv:2208.11217v1, 2022; Operations Research, 2024. https://arxiv.org/abs/2208.11217
• H. D. Kwon, Game of variable contributions to the common good under uncertainty, Operations Research, 2022. https://arxiv.org/abs/1904.00500
• L. H. R. Alvarez, J. Lempa, On the optimal stochastic impulse control of linear diffusions, SIAM Journal on Control and Optimization 47(2) 703–732, 2008.
• G. Georgiadis, Y. Kim, H. D. Kwon, The absence of attrition in a war of attrition under complete information, Games and Economic Behavior 131 171–185, 2022.
• N. Touzi, N. Vieille, Continuous-time Dynkin games with mixed strategies, SIAM Journal on Control and Optimization 41(4) 1073–1088, 2002.
• A. N. Borodin, P. Salminen, Handbook of Brownian Motion — Facts and Formulae, Birkhäuser, Basel, 1996.