The OR Formalization Drive

Motivation

A stochastic processing network (SPN) — buffers holding waiting work, activities that consume items from buffers and produce items into others, driven by stochastic arrivals and service requirements — is stable, in the sense of mission I's Definition 3.6, exactly when its ambient Markov chain is positive recurrent. That definition is correct, but it is a statement about an infinite-state continuous-time Markov chain, and Markov chains of that kind almost never admit a hand-computed stationary distribution or a directly verifiable positive-recurrence criterion for anything beyond the smallest examples. What is needed is a method that turns "is this specific queueing network, under this specific control policy, stable?" into a tractable, purely deterministic question. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) supplies exactly this method in Chapter 6, and the theorem that licenses it — Theorem 6.2 — is introduced by the authors themselves as "the fulcrum that supports all other results developed in this book." Every stability theorem in the remaining eight chapters of the book (feedforward and generalized Jackson networks, the Rybko–Stolyar boundary, back-pressure control, proportionally fair allocation, task allocation, packet networks) is an application of this one theorem to a model-specific fluid model.

The method traces to Rybko and Stolyar's 1992 study of a single two-station network and to J. G. Dai's 1995 unification of fluid-limit stability arguments across general queueing networks (Annals of Applied Probability 5, 49–77), with independent contemporaneous work by A. Stolyar for discrete state spaces and a parallel probabilistic route through reflecting Brownian motion due to Dupuis and Williams (1994). This mission formalizes the version of the argument specific to Dai and Harrison's general SPN framework.

Setting

Under a fixed control policy, an SPN with $I$ buffers and $J$ activities generates four continuous-time processes: the cumulative departure process $D(t) \in \mathbb{Z}_+^I$, the cumulative service-completion process $F(t) \in \mathbb{Z}_+^J$, the cumulative service-effort process $T(t) \in \mathbb{R}_+^J$, and the buffer-contents process $Z(t) \in \mathbb{Z}_+^I$. The model's first-order data — the $I \times J$ material-requirement matrix $B$, the $I \times J$ expected-output matrix $\Gamma$, the vector $m$ of mean service times, the $K \times J$ capacity-consumption matrix $A$, the $K$-vector $b$ of server-pool capacities, and the vector $\lambda$ of external arrival rates — determine six basic relationships that Chapter 2 derives directly from the SPN's construction, and that this mission packages as IsFluidModelSolution.

To study scaling limits, Section 6.3 constructs, on one common probability space, a whole family of versions of the SPN's processes, one for each initial state $x$ of the ambient chain: the superscripted $D^x, F^x, T^x, Z^x$. Writing $|x|$ for the total initial buffer content, the fluid-scaled processes are

$$\big(\hat D^x, \hat F^x, \hat T^x, \hat Z^x\big)(t,\omega) := \tfrac{1}{|x|}\big(D^x, F^x, T^x, Z^x\big)(|x|t, \omega), \qquad t \ge 0.$$

A fluid limit path (Definition 6.6) is any limit of such a family, along a sequence of initial states with $|x_n| \to \infty$, uniform on compact time intervals (u.o.c.). A fluid model solution is any four-tuple satisfying the six equations above, whether or not it arises as an actual limit — a purely deterministic notion.

Formalization targets

Goal: Theorem 6.2 — fluid limit stability implies SPN stability

$$\text{fluid limit of the SPN is stable} \quad\Longrightarrow\quad \text{ambient Markov chain } X \text{ is positive recurrent},$$

where "fluid limit... is stable" (Definition 6.1) means: there is $\gamma > 0$ such that every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ has $\hat Z(t) = 0$ for all $t \ge \gamma |\hat Z(0)|$. This is the weakest possible target: it asserts only that fluid limit paths are eventually driven to zero, with no rate or further structure attached, and it is exactly the hypothesis every later chapter's Lyapunov argument is built to establish.

Supporting milestones

Theorem 6.5 (existence of fluid limits): along any sequence of initial states with $|x_n| \to \infty$, the fluid-scaled processes have a u.o.c.-convergent subsequence, and every such limit is automatically a fluid model solution — the bridge from the purely equational Definition 6.3 (used by every later chapter) to the genuinely stochastic Definition 6.1 (needed by this theorem). Its proof rests on two convergence lemmas (6.7: compactness of the scaled service-effort process via an equicontinuity argument; 6.8: the scaled completion process converges exactly when the scaled effort process does) and, behind Lemma 6.8, a uniform strong law of large numbers for a "delayed" random walk (Lemma 6.9). A separate uniform-integrability result (Lemma 6.10) supplies the remaining ingredient the goal theorem's proof needs to convert an almost-sure fluid-scale limit into the expectation bound mission I's Lemma 3.7 requires.

Significance

The result itself. Theorem 6.2 converts a probabilistic stability question about an infinite-state Markov chain into a real-analysis question about a deterministic dynamical system: does every solution of a fixed, checkable system of equations reach zero in finite time, uniformly in its starting size? Every one of the book's remaining eight chapters answers a version of this question for a specific policy and concludes SPN stability via this theorem alone — none of them re-derives positive recurrence directly.

Formalizing it. No prior formalization of fluid limits, fluid models, or scaling-limit stability of any stochastic system exists on Prove2Me (q=fluid limit, q=fluid model, q=u.o.c. convergence, q=queueing network stability all return zero hits). This mission is a from-scratch formalization of the model data, the fluid equations, the per-state process family, and the two notions of fluid stability, together with the five supporting results and the goal theorem that connects them — the shared infrastructure the rest of the fourteen-mission series depends on.

Difficulty

The obvious shortcut — state Theorem 6.2 using fluid model stability (Definition 6.3, the purely equational notion) in place of fluid limit stability (Definition 6.1) — would produce a strictly easier, unfaithful theorem: fluid model solutions are not restricted to arise as actual scaling limits, so the genuine content of Theorem 6.2 (that convergence of a stochastic family forces a probabilistic conclusion) would be lost, and the theorem would reduce to a tautology once Theorem 6.5 is assumed. The two notions are visually almost identical in the book's own text ("$\gamma|\hat Z(0)|$-attraction to the origin," applied to two different objects) and keeping them distinct is this mission's central discipline. A second difficulty is that Mathlib has no existing theory of stochastic-process scaling limits, u.o.c. convergence, or the specific renewal/SLLN machinery (Lemma 6.9's uniform strong law for a state-dependent "delayed" random walk) the proof needs — every one of these had to be defined from the ground up rather than instantiated from a general framework.

Formalization scope

The ambient chain's state space is an arbitrary countable type, following mission 01; the per-state process family SPNProcessFamily takes $D^x, F^x, T^x, Z^x$ as given real-valued functions satisfying exactly the pathwise properties (Eqs. 2.31–2.32) that Section 6.4's proofs use, since Chapter 2's construction of these processes from primitive stochastic elements is that chapter's own "recap" of already-established facts, not a numbered result of Chapter 6. UOCConverges is stated by its direct $\varepsilon$-$N$-on-every-compact-interval meaning, and Lemma 6.9's "$\sup_x$" is likewise stated by its direct $\varepsilon$-$N$ meaning rather than a Lean supremum expression, because the state space may be countably infinite and an explicit supremum over an unbounded-above family of reals would silently collapse to a junk value of zero in that case — a real risk of trivializing the statement that this formalization avoids outright. A formalization that reused FluidModelStable as the goal theorem's hypothesis, or that dropped $|\hat Z(0)|=1$ from Theorem 6.5, would each be a trivializing shortcut of exactly the kind ruled out above. The five definitions (FluidEquationData, IsFluidModelSolution, SPNProcessFamily, FluidLimitPath, FluidLimitStable) are the primary reusable contribution — the shared vocabulary every later mission in the series restates in its own namespace, since drafts do not import one another. Contributions completing the six by sorry proofs are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• J. G. Dai, "On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models," Annals of Applied Probability 5 (1995), 49–77.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• P. Dupuis and R. J. Williams, "Lyapunov functions for semimartingale reflecting Brownian motions," Annals of Probability 22 (1994), 680–702.

Motivation

Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.

The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.

Setting

A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class $i$ is served by a unique pool $p(i)$, and on completion a class-$i$ job becomes class $j$ with probability $P_{ij}$ (the routing matrix). $I(k)$ denotes the set of classes served by pool $k$. The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity ($\hat D = \hat F$) and the output matrix is $\Gamma_{ij} = P_{ji}$.

Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation $\sigma$, always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy $\beta = h(\hat z)$, where $\hat z$ is the updated job-count vector and $h$ is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.

Formalization targets

Goal: Theorem 7.5 — the FCFS fluid equation

For a queueing network under FCFS control, every fluid limit path $(\hat D, \hat F, \hat T, \hat Z)$ satisfies (6.1)-(6.6) and

$$\hat D_i\big(t + \hat W_k(t)\big) = \hat G_i(t), \qquad t \ge 0,\ i \in I(k),\ k \in K,$$

where $\hat G_i(t) = \lambda_i t + \sum_j P_{ji}\hat D_j(t)$ is the fluid arrival rate into class $i$ and $\hat W_k(t) = \sum_{i \in I(k)} m_i \hat Z_i(t)$ is pool $k$'s fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).

Supporting milestones

Theorem 7.2 (non-idling): $\sum_{i\in I(k)} \hat Z_i(t) > 0$ forces pool $k$'s aggregate service rate to run at full capacity $b_k$. Theorem 7.3 (non-preemptive SBP): the same conclusion with $I(k)$ sharpened to the priority set $H(j)$ (Eq. 7.5), for every buffer $j$. Theorem 7.8 (general relaxed control): under Assumption 7.6, $\hat Z_i(t) > 0$ forces $\hat T_i$'s derivative to equal $h_i(\hat Z(t))$ exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable $h$.

Significance

The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.

Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy all return zero hits, consistent with triage.json's record that none of this book's Chapters 6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing networks, their three named control-policy families, and the four policy-specific fluid equations Chapter 7 derives for them.

Difficulty

The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with $I(k)$ replaced by $H(j)$ — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at $t + \hat W_k(t)$ match arrivals at $t$), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on $\hat T$ or $\hat D$ alone, without introducing the auxiliary workload process $\hat W$, could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — "$\hat Z_i(t) = 0$ implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.

Formalization scope

Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally in this chapter's own namespace rather than imported, since drafts in this series do not import one another; the restatement is trimmed to the four raw processes $(D^x,F^x,T^x,Z^x)$ this chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized, applied to different index sets ($I(k)$ vs. $H(j)$) — the pathwise full-utilization identity (7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of the service-starting mechanism is out of scope for this chapter, exactly as it was for mission III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12) (rewritten via the material-balance equation to avoid needing the raw arrival process) and the fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the "delayed random walk" $V$ of Eq. (6.47). A formalization that dropped the workload shift $\hat W_k(t)$ from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication (which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions completing the four by sorry proofs — each of which needs the u.o.c.-convergence and dominated-convergence arguments mission III's own proofs still lack — are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• M. Bramson, "Convergence to equilibria for fluid models of FIFO queueing networks," Queueing Systems 22 (1996), 5–45.
• M. Bramson, "Instability of FIFO queueing networks," Annals of Applied Probability 4 (1994), 414–431.
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.

Motivation

An insurance company's surplus grows with premiums and falls with claims. In the Cramér–Lundberg model with a positive safety loading, the surplus drifts to $+\infty$ with probability one. De Finetti (1957) objected that a company does not accumulate capital indefinitely: surplus above some level is paid out to shareholders. He proposed choosing the payout policy to maximize the expected discounted dividends paid before ruin. This is the optimal dividend problem. It is one of the basic stochastic control problems of actuarial mathematics and corporate finance, and it serves as a test case for singular control of processes with jumps.

The classical answer is a barrier strategy: pay out whatever lifts the surplus above a level $a$ and nothing else. Jeanblanc and Shiryaev (1995) proved this optimal when the surplus is a Brownian motion with drift, and Gerber and Shiu studied the same Brownian setting. Azcue and Muler (2005) showed that it can fail in the Cramér–Lundberg model, where the optimal policy may be a band strategy. Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007) 156–180) treated a general spectrally negative Lévy process, a process with stationary independent increments and only downward jumps. They found the value of every barrier strategy in closed form through the scale function of the process and identified the best barrier level $c^*$. They also gave a verification condition under which the barrier at $c^*$ is optimal among all strategies. Loeffen (2008) later showed that the condition holds whenever the Lévy measure has a completely monotone density.

Setting

Let $X=(X_t)_{t\ge0}$ be a spectrally negative Lévy process on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ with $X_0=0$ and Lévy triplet $(c,\sigma,\nu)$. Its Laplace exponent is $\psi(\theta)=\log\mathbf E[e^{\theta X_1}]$, finite for $\theta\ge0$:

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}\bigl(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}}\bigr)\nu(dy).$$

Increments after time $s$ are independent of $\mathcal F_s$. Initial capital $x$ is added to $X$. The standing assumptions are the following: $X$ does not have monotone paths, $\mathbf E[X_1]>-\infty$, and either $\sigma>0$, $\int_{(-1,0)}|y|\,\nu(dy)=\infty$, or $\nu$ has a density.

A dividend strategy is a nondecreasing, left-continuous, adapted process $L$ with $L_0=0$. The risk process is $U_t=x+X_t-L_t$ and the ruin time is $\sigma^L=\inf\{t\ge0:U_t<0\}$. The strategy is admissible ($L\in\Pi$) if no lump sum exceeds the current reserves. Its value is

$$v_L(x)=\mathbf E\Bigl[\int_0^{\sigma^L}e^{-qt}\,dL_t\Bigr],\qquad v_*(x)=\sup_{L\in\Pi}v_L(x),$$

with discount rate $q>0$. For $C\in[0,\infty]$, $\Pi_{\le C}$ consists of the admissible strategies that keep $U_t\le C$ for $t>0$.

The $q$-scale function $W=W^{(q)}$ is the unique continuous nondecreasing function on $[0,\infty)$ with $\int_0^\infty e^{-\theta y}W(y)\,dy=1/(\psi(\theta)-q)$ for large $\theta$. It is extended by $W=0$ on $(-\infty,0)$. The barrier strategy $\pi_a$ reflects $x+X$ at the level $a$, paying $(x-a)^+$ at time $0$. The paper computes its value

$$v_a(x)=\frac{W(x)}{W'(a)}\ (0\le x\le a),\qquad v_a(x)=x-a+\frac{W(a)}{W'(a)}\ (x>a),$$

and the optimal barrier level is $c^*=\inf\{a>0: W'(a)\le W'(x)\ \forall x>0\}$, read as $0$ when this set is empty and $W'(0+)\le W'(x)$ for all $x>0$. The generator is

$$\Gamma f(x)=\tfrac{\sigma^2}{2}f''(x)+cf'(x)+\int_{(-\infty,0)}[f(x+y)-f(x)-f'(x)y\mathbf 1_{\{|y|<1\}}]\,\nu(dy).$$

Formalization targets

Goal: Theorem 2 (p. 14)

Assume $\sigma>0$, or $X$ has bounded variation, or $v_{c^*}\in C^2(0,\infty)$. Then $c^*<\infty$ and:

$$\text{(i)}\quad \pi_{c^*}\in\Pi_{\le c^*},\qquad v_{\pi_{c^*}}(x)=v_{c^*}(x)=\sup_{\pi\in\Pi_{\le c^*}}v_\pi(x)\quad(x\ge0);$$ $$\text{(ii)}\quad (\Gamma v_{c^*}-qv_{c^*})(x)\le0\ \ \forall x>c^*\ \Longrightarrow\ v_*(x)=v_{c^*}(x)\ (x\ge0),\ \ \pi_*=\pi_{c^*}.$$

The goal fixes no constants: the barrier level and the value function are both given by the scale function of the given process.

Milestones

• Proposition 1 (p. 7): $v_{\pi_a}(x)=W(x)/W'(a)$ for $a>0$, $x\in[0,a]$.
• Lemma 2(i) (p. 15): $c^*<\infty$.
• Proposition 3(i) (p. 15): $v_a(x)\le v_{c^*}(x)$ for $x\in[0,c^*]$, $a\ge0$.
• Lemma 3(i) (p. 16): $v_{c^*}'(x)\ge1$ for $x>0$.
• Proposition 4(i) (p. 18): a $C^2$ (unbounded variation) or $C^1$ (bounded variation) solution $w$ of $\max\{\Gamma w-qw,1-w'\}=0$ on $(0,C)$ dominates $\sup_{\Pi_{\le C}}v_\pi$.
• Lemma 4 (p. 20): $(\Gamma v_{c^*}-qv_{c^*})(x)=0$ on $(0,c^*)$ when $c^*>0$.

Significance

The theorem gives an explicit solution to a singular control problem for a general Lévy model. The candidate value function and barrier level are expressed through one special function, $W^{(q)}$, and optimality over all strategies reduces to one inequality on $(c^*,\infty)$. It is the basis of the later literature on scale-function methods in dividend problems (Loeffen 2008, Kyprianou–Rivero–Song 2010, and the refracted and Parisian variants). Part (i) holds with no condition on the Lévy measure. Part (ii) shows exactly where barrier optimality can fail.

The paper's proofs use fluctuation identities (exit problems, excursion theory) and Itô's formula for semimartingales with jumps. None of these is in Mathlib. As far as is known, none of these results has been machine-checked. A formalization would produce a Lévy-process and scale-function layer, a formal model of singular control with jumps and lump-sum payments, and a checked verification argument. Each of these can be reused beyond this paper.

Difficulty

The analytic part is elementary once the value formula (5.1) is available: the choice of $c^*$, Proposition 3(i) and Lemma 3(i) follow from the shape of $W'$. The difficulty lies in the two probabilistic steps. Proposition 1 identifies the value of a reflected process through exit identities for $X$. Those identities rest on excursion theory, or on the martingale property of $e^{-qt}W(X_t)$ up to exit. The verification step, Proposition 4(i), needs Itô's formula for $w(U_t)$. Here $U$ is a jump process controlled by a left-continuous finite-variation process that may itself jump. The change-of-variables formula must also run under only $C^1$ regularity when $X$ has bounded variation. Just proving that $\Gamma w-qw\le0$ and $w'\ge1$ imply a supermartingale inequality does not settle the question: the lump-sum payments and the jumps of $X$ enter the Itô expansion separately and must each be bounded.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a structure carrying the triplet $(c,\sigma,\nu)$ and pathwise càdlàg paths with only downward jumps. It also carries independence of increments from the filtration and stationarity. Its law is fixed by the Laplace transform $\mathbf E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$. The standing assumptions of §2 and (3.3) are bundled as one predicate. The scale function is a hypothesis on a function argument $W$ (it is unique). $W'(0+)$ is an extended real, since it is $+\infty$ for unbounded variation without a Gaussian part.

Values of strategies and value functions lie in $[0,\infty]$. The dividend integral is a Lebesgue–Stieltjes integral over $[0,\sigma^L)\cup\{0\}$: it counts the lump sum at time $0$ and excludes a payment at the ruin instant.

Several conventions are fixed, and each is disclosed in the item it affects:

• Admissibility. The paper requires $L_{t+}-L_t<U_t$. The formalization uses $\le$, because the paper's own strategy of paying out everything at once needs it.
• Barrier level (5.2). Printed over $a>0$ and "all $x$", the defining set is empty for Brownian motion with nonpositive drift. The printed set (with $x>0$) is kept whenever it is nonempty; when it is empty and $W'(0+)\le W'(x)$ for all $x>0$ — the second alternative in the proof of Lemma 2(i) — $c^*=0$, and otherwise $c^*=\infty$.
• Printed slips. The integral $\int_{-1}^0 x\,\nu(dx)$ in (3.3) is read as $\int|x|\,\nu(dx)$. In (3.4), $e^{-\theta x}$ is read as $e^{-\theta y}$, and in Theorem 2(i), $\pi^*_c$ is read as $\pi_{c^*}$.
• Proposition 4(i) is stated for initial capital $x\le C$. Beyond $C$, $w$ is unconstrained and the printed claim fails.
• Lemma 4 carries the smoothness proviso of Theorem 2 on $(0,c^*)$.

A trivializing encoding is ruled out: the value is not a real supremum, the barrier strategy is constructed rather than assumed, and $c^*<\infty$ is a conclusion.

A complete development needs:

• Lévy processes and their Laplace exponents;
• scale functions and the exit identity $\mathbf E_x[e^{-qT}\mathbf 1_{\{X_T=a\}}]=W(x)/W(a)$;
• reflected processes;
• Itô's formula for jump semimartingales with finite-variation controls.

The Lévy and scale-function layer is shared with the companion mission on the bail-out problem. Contributions of general lemmas (Stieltjes integration by parts, optional stopping for càdlàg martingales) are welcome.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• P. Azcue, N. Muler, Optimal reinsurance and dividend distribution policies in the Cramér–Lundberg model, Math. Finance 15 (2005) 261–308.
• M. Jeanblanc-Picqué, A. N. Shiryaev, Optimization of the flow of dividends, Russian Math. Surveys 50 (1995) 257–277.
• R. L. Loeffen, On optimality of the barrier strategy in de Finetti's dividend problem for spectrally negative Lévy processes, Ann. Appl. Probab. 18 (2008) 1669–1680.
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Dividends, ruin and bail-out loans

An insurance company's surplus in the Cramér–Lundberg model grows linearly with premiums and falls by claims arriving as a compound Poisson process. When premium income exceeds the expected claims, the surplus drifts to infinity. De Finetti (1957) proposed that the surplus above a barrier should instead be paid to shareholders as dividends, and the resulting optimal dividend problem — maximize the expected discounted dividends — is a central problem of risk theory. A barrier policy, however, drives the surplus below zero with probability one. Harrison and Taylor (1978) and Løkka and Zervos studied, for Brownian motion, a variant with bail-out loans: ruin is forbidden, and the shareholders must inject capital whenever the surplus would become negative, at a cost $\varphi>1$ per unit.

Avram, Palmowski and Pistorius (Ann. Appl. Probab. 17 (2007)) solved the bail-out problem when the surplus is a general spectrally negative Lévy process, which includes the Cramér–Lundberg model, Brownian motion with drift and their sums. They showed that the optimal policy is a double barrier policy for every initial capital. This mission formalizes that result, Theorem 3 of the paper.

Timeline:

• 1957 — de Finetti introduces dividend barriers.
• 1978 — Harrison and Taylor: optimal control of a Brownian storage system with two reflecting barriers.
• 1995 — Jeanblanc and Shiryaev: optimal dividends for Brownian motion with drift.
• 2004 — Avram, Kyprianou and Pistorius: exit problems for spectrally negative Lévy processes reflected at their infimum and supremum, in terms of scale functions.
• 2007 — Avram, Palmowski and Pistorius: Theorems 1 and 3 of the present paper; Pistorius' pathwise construction of the doubly reflected process is used.

Setting

A spectrally negative Lévy process $X=\{X_t\}_{t\ge0}$ on a filtered probability space $(\Omega,\mathcal F,\mathbb F,P)$ starts at $X_0=0$, has càdlàg paths, is $\mathbb F$-adapted, and has stationary increments with $X_t-X_s$ independent of $\mathcal F_s$. Its jumps are all negative, and $E[e^{\theta X_t}]=e^{t\psi(\theta)}$ for $\theta\ge0$, where the Laplace exponent is

$$\psi(\theta)=c\theta+\tfrac{\sigma^2}{2}\theta^2+\int_{(-\infty,0)}(e^{\theta y}-1-\theta y\mathbf 1_{\{|y|<1\}})\,\nu(dy).$$

With initial capital $x\ge0$ the surplus is $x+X$. The standing assumptions are: $X$ does not have monotone paths; $E[X_1]>-\infty$ (so $\psi'(0+)=E[X_1]$ is finite); $\sigma>0$, or $\int_{(-1,0)}|y|\nu(dy)=\infty$, or $\nu$ has a density (condition (3.3)).

A policy $\bar\pi=(L,R)$ consists of nondecreasing adapted processes with $L_0=R_0=0$: cumulative dividends $L$ (left-continuous) and cumulative injected capital $R$ (right-continuous). The controlled surplus is $V_t=x+X_t-L_t+R_t$. The policy is admissible if $V_t\ge0$ for $t>0$ and $\int_0^\infty e^{-qt}dR_t<\infty$ almost surely. Its value and the value function are

$$\bar v_{\bar\pi}(x)=E\Bigl[\int_0^\infty e^{-qt}dL_t-\varphi\int_0^\infty e^{-qt}dR_t\Bigr],\qquad \bar v_*(x)=\sup_{\bar\pi\ \text{admissible}}\bar v_{\bar\pi}(x),$$

with discount rate $q>0$ and cost $\varphi>1$. The double-barrier strategy $\bar\pi_{0,a}$ pays out $(x-a)^+$ at once and then the minimal dividends and injections that keep $V$ in $[0,a]$: $dL$ is carried by $\{V=a\}$ and $dR$ by $\{V=0\}$.

The $q$-scale function $W=W^{(q)}$ vanishes on $(-\infty,0)$, is continuous and nondecreasing on $[0,\infty)$, and satisfies $\int_0^\infty e^{-\theta y}W(y)dy=1/(\psi(\theta)-q)$ for $\theta>\Phi(q)$, the largest root of $\psi=q$. Set $\overline W(y)=\int_0^yW$, $Z=1+q\overline W$, $\overline Z(y)=\int_0^yZ$. The candidate value of $\bar\pi_{0,a}$ is

$$\bar v_a(x)=\varphi\bigl(\overline Z(x)+\psi'(0+)/q\bigr)+Z(x)\frac{1-\varphi Z(a)}{qW(a)}\quad(0\le x\le a),\qquad \bar v_a(x)=x-a+\bar v_a(a)\quad(x>a),$$

and the barrier level is $d^*=\inf\{a>0:[\varphi Z(a)-1]W'(a)-\varphi qW(a)^2\le0\}$, with $\inf\emptyset=\infty$.

Formalization targets

Goal: Theorem 3

$$d^*<\infty,\qquad \bar v_*(x)=\bar v_{d^*}(x)\ \ (x\ge0),\qquad \bar\pi_{0,d^*}\ \text{exists, is admissible and attains }\bar v_*(x).$$

Milestones

• Lemma 1: $\overline W(y)/\overline W(a)\le W(y)/W(a)$ for $0\le y\le a$.
• Proposition 2, (3.17): the expected discounted undershoot $E_x[e^{-qT_0^-}X_{T_0^-}]$ in closed form.
• Theorem 1: the expected discounted dividends and injections of $\bar\pi_{0,a}$, $a>0$, in closed form; hence $\bar v_{\bar\pi_{0,a}}=\bar v_a$.
• Lemma 2(ii): $d^*=0$ if and only if $\sigma=0$ and $\nu(-\infty,0)\le q/(\varphi-1)$.
• Proposition 3(ii): $d^*<\infty$ and $\bar v_a\le\bar v_{d^*}$ for all levels $a$.
• Lemma 3(ii)–(iv): $1\le\bar v_{d^*}'\le\varphi$ with boundary slopes; $a\mapsto\bar v_a(x)$ nonincreasing for $a>d^*$; $\bar v_{d^*}$ concave.
• Lemma 5: $(\Gamma\bar v_{d^*}-q\bar v_{d^*})\le0$ on $(0,\infty)$, with equality on $(0,d^*)$.
• Proposition 4(ii): any $C^2$ solution of the variational inequality (5.9) dominates $\bar v_*$.

Significance

Theorem 3 answers the bail-out problem completely: for every initial capital and every spectrally negative Lévy surplus, the optimal policy is a double barrier with an explicit level and an explicit value in terms of scale functions. In the classical problem without injections (Theorem 2 of the same paper) the analogous conclusion needs an extra generator condition, and Azcue and Muler exhibited Cramér–Lundberg models where barrier policies are not optimal. The result is the basis of later work on dividends with capital injection, transaction costs and Parisian ruin.

The result has a published proof. What this mission adds is a machine-checked version. As far as is known, no part of the theory used — Lévy processes, scale functions, doubly reflected processes, the generator of a Lévy process, singular stochastic control — has been formalized in Lean's Mathlib.

Difficulty

The value function is a supremum over all adapted singular controls. Its upper bound requires a verification argument: Itô's formula for $e^{-qt}w(V_t)$ with a semimartingale $V$ that has jumps, a controlled bounded-variation part and a possibly nonzero continuous martingale part, followed by localization and limits. A function that satisfies the variational inequality only in the viscosity sense is not enough, so the candidate $\bar v_{d^*}$ must be shown to be regular enough and to satisfy $\Gamma\bar v_{d^*}-q\bar v_{d^*}\le0$ everywhere on $(0,\infty)$. Above the barrier this inequality does not follow from a martingale property: the paper derives it from concavity and a comparison with higher barriers, through the resolvent of the doubly reflected process. The lower bound requires the existence and value of the doubly reflected process, and computing that value needs fluctuation identities (two-sided exit, overshoot) that are themselves theorems about scale functions.

Formalization scope

Time is indexed by $\mathbb R_{\ge0}$. The process is a structure carrying the triplet $(c,\sigma,\nu)$, the paths, adaptedness, independence of future increments from $\mathcal F_s$, stationarity, the Laplace-exponent identity, and the usual conditions on the filtration. $P_x$ is the law of $x+X$. Policy values are computed as $E[\int e^{-qt}dL]-\varphi E[\int e^{-qt}dR]$ in the extended reals from two $[0,\infty]$-valued expectations, and the value function is a supremum in the extended reals; a policy with both expectations infinite gets $-\infty$. Stieltjes integrals include the jump at time $0$. The scale function is a hypothesis IsScaleFunction (it is unique), and $d^*$ lives in $[0,\infty]$, so an empty defining set gives $\infty$. The double-barrier strategy is characterized by the two-sided Skorokhod conditions plus mutual singularity of $dL$ and $dR$, which pins the level-$0$ policy of bounded-variation processes. These conditions hold almost surely, and they are stated on the post-decision surplus $V_{t+}=x+X_t-L_{t+}+R_t$: $dL$ is carried by $\{V_{t+}=a\}$ and $dR$ by $\{V_{t+}=0\}$. This is the paper's "minimal amount" (p. 4) and matches its construction on pp. 10–11. The closure-of-support wording of (4.2) on its own would also admit non-minimal lump dividends. Admissibility, $V_t\ge0$ for $t>0$ together with (2.3), is likewise required almost surely.

Printed slips corrected (milestone texts are verbatim):

• Theorem 3 and Proposition 3(ii) print "$\psi'(0+)<\infty$", which always holds; the intended $\psi'(0+)>-\infty$ is used.
• (3.3) prints $\int_{-1}^0x\,\nu(dx)=\infty$ for $\int_{(-1,0)}|x|\,\nu(dx)=\infty$.
• (3.4) prints $e^{-\theta x}$ in a $dy$-integral.
• p. 20 prints the extension $\bar v_{d^*}(x)+\varphi x$ for $\bar v_{d^*}(0)+\varphi x$.
• Lemma 3(iv) is printed for every $a>0$ but proved and used only for $a=d^*$, and is stated for $a=d^*$.
• Proposition 3(ii) at $a=0$ is stated only for bounded variation, where $\bar v_0$ is defined.

The goal cannot be satisfied trivially. It asserts equality of the value function with $\bar v_{d^*}$, not only an inequality. Existence of the optimal policy is part of the conclusion. Generator statements carry integrability of the jump integrand, so a non-integrable integrand cannot make them true with the junk value $0$.

A complete development needs Lévy processes and their Laplace exponents, scale functions, first-passage and two-sided exit identities, reflected and doubly reflected processes, Itô's formula for semimartingales with jumps, and a verification theorem for singular control. All of these are reusable well beyond this mission. Contributions of any of these foundations are welcome, as are proofs of the analytic milestones (Lemma 3, Proposition 3(ii)) from the scale-function properties.

Selected references

• F. Avram, Z. Palmowski, M. R. Pistorius, On the optimal dividend problem for a spectrally negative Lévy process, Ann. Appl. Probab. 17 (2007) 156–180. https://arxiv.org/abs/math/0702893
• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14 (2004) 215–238. https://doi.org/10.1214/aoap/1075828052
• M. R. Pistorius, On doubly reflected completely asymmetric Lévy processes, Stochastic Process. Appl. 107 (2003) 131–143. https://doi.org/10.1016/S0304-4149(03)00065-9
• J. M. Harrison, A. J. Taylor, Optimal control of a Brownian storage system, Stochastic Process. Appl. 6 (1978) 179–194. https://doi.org/10.1016/0304-4149(78)90059-5
• A. E. Kyprianou, Introductory Lectures on Fluctuations of Lévy Processes with Applications, Springer, 2006. https://doi.org/10.1007/978-3-540-31343-4

Motivation

Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).

Setting

A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, $b \equiv 1$), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.

Formalization targets

Goal: Theorem 8.25 — the Rybko–Stolyar-style boundary for a re-entrant line

The two-station, five-class re-entrant network's fluid model is globally stable if and only if

$$\lambda_1(m_1+m_3+m_5) < 1, \qquad \lambda_1(m_2+m_4) < 1, \qquad \lambda_1(m_2+m_5) < 1.$$

The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.

Supporting milestones

Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.

Significance

The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.

Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station" (q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to this material; this mission is a from-scratch formalization of global stability at both the Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class re-entrant line, and the assembly-with-side-business network.

Difficulty

Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible $(x_2,x_4)$ pairs with a wedge region, then separately solves an analogous system for $(x_1,x_3,x_5)$ — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.

Formalization scope

Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload operator are restated locally (drafts in this series do not import one another), as is mission VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable, even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly over an uninterpreted policy type and two predicates, since the concrete "simply structured non-idling policy" and "positive recurrence under a policy" notions belong to mission I's apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a structural property of an ordinary flat-indexed queueing network (a partial successor function encoding the deterministic route) rather than by re-introducing the book's own two-index type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2 serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not read off Figure 8.3 directly, though the two are cross-checked as consistent. The assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter 2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations (8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare ↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's instability construction — a formalization that dropped either direction of the iff, or that conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable, IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/ reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery this mission does not otherwise build — are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• A. N. Rybko and A. L. Stolyar, "Ergodicity of stochastic processes describing the operation of open queueing networks," Problemy Peredachi Informatsii 28 (1992), 3–26.
• J. G. Dai and J. H. Vande Vate, "The stability of two-station multitype fluid networks," Operations Research 48 (2000), 721–744.

Motivation

Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.

The case where the set lives in a subspace arises in practice. Taking $q$ rows of an optimal simplex tableau restricts the integer points to an affine subspace $f+W$ of $\mathbb R^q$ spanned by the tableau columns. When $W$ is irrational, its integer points span only a proper subspace $V\subsetneq W$. The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation $R_f(W)$) needs.

Timeline.

• Lovász (Geometry of numbers and integer programming, 1989) stated the characterization for rational subspaces (Proposition 3.1) and gave only a sketch of the proof. The irrational-hyperplane case is not visible in that sketch.
• Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543v1; Math. Oper. Res. 35(3), 2010, doi:10.1287/moor.1100.0461) gave a complete proof of Lovász's theorem for an arbitrary lattice of a linear space (Theorem 10). They also extended it to a space $W$ strictly larger than the span $V$ of the lattice (Theorem 9, equivalently Theorem 1 for $\mathbb Z^n$).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product and the open balls $B_\varepsilon(x)$. For $X\subseteq\mathbb R^n$, $\langle X\rangle$ denotes its linear span.

A lattice of a linear space $V$ is an additive group $\Lambda=\{\lambda_1a_1+\dots+\lambda_ma_m\mid\lambda_i\in\mathbb Z\}$ generated by linearly independent vectors $a_1,\dots,a_m$ with $\langle a_1,\dots,a_m\rangle=V$ (Definition 6, IsLatticeOf Λ V). A linear subspace $L\subseteq V$ is a $\Lambda$-subspace if it has a basis contained in $\Lambda$ (Definition 7, IsLambdaSubspace Λ V L). For $\mathbb Z^2$, the line $x_2=2x_1$ is a $\Lambda$-subspace and the line $x_2=\sqrt2x_1$ is not.

For sets $W,S$ the interior relative to $W$ is $\mathbf{int}_W(S)=\{x\in S\mid B_\varepsilon(x)\cap W\subseteq S\text{ for some }\varepsilon>0\}$ (intW W S). The relative interior is $\mathbf{relint}(S)=\mathbf{int}_{\operatorname{aff}(S)}(S)$.

Let $W\supseteq V$ be a linear space. A set $S$ is a $\Lambda$-free convex set of $W$ if $S\subseteq W$, $S$ is convex and $\Lambda\cap\mathbf{int}_W(S)=\emptyset$. It is maximal if no other $\Lambda$-free convex set of $W$ properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).

The statements also use a polyhedron in $W$ ($W$ intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension $\dim(S)$ of the affine hull with $\dim\emptyset=-1$ (affDim), and a facet: a nonempty face $S\cap\{\langle a,x\rangle=b\}$ of a valid inequality with $\dim F=\dim S-1$. The recession cone is $\operatorname{rec}(S)=\{r\mid x+tr\in S\ \forall x\in S,\ t\ge0\}$ and the lineality space is $\operatorname{rec}(S)\cap-\operatorname{rec}(S)$.

Formalization targets

Goal: Theorem 9 (p. 8)

For a lattice $\Lambda$ of $V$ and a linear space $W\supseteq V$ with $\dim W\ge1$, a set $S$ is a maximal $\Lambda$-free convex set of $W$ if and only if

$$\text{(i) } S \text{ is a full-dimensional polyhedron in } W,\ S\cap V \text{ is maximal } \Lambda\text{-free in } V,\ F\mapsto F\cap V \text{ is a bijection of facets};$$ $$\text{(ii) } S=v+L \text{ is a hyperplane of } W \text{ with } L\cap V \text{ a hyperplane of } V \text{ that is not a } \Lambda\text{-subspace};$$ $$\text{(iii) } S \text{ is a half-space of } W \text{ containing } V \text{ on its boundary.}$$

Main milestone: Theorem 10 (p. 8)

For $\dim V\ge1$, $S$ is a maximal $\Lambda$-free convex set of $V$ if and only if either $S=P+L$ is a polyhedron with $P$ a polytope, $L$ a $\Lambda$-subspace and $\dim S=\dim P+\dim L=\dim V$, with no lattice point in $\mathbf{int}_V(S)$ and a lattice point in the relative interior of every facet; or $S=v+L$ is an affine hyperplane of $V$ whose direction $L$ is not a $\Lambda$-subspace.

Supporting milestones

Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ($S+\langle\operatorname{rec}S\rangle$ stays $\Lambda$-free), Lemma 17 (projection along a $\Lambda$-subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), $\mathbf{int}_W(S)\cap V=\mathbf{int}_V(S\cap V)$.

Significance

Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most $2^{\dim P}$) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have $V$ on their boundary, and the hyperplanes of (ii), whose trace on $V$ is a hyperplane of $V$ that is not a $\Lambda$-subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of $R_f(W)$ is the gauge of a maximal lattice-free convex set of $f+W$.

These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.

Difficulty

The obvious argument separates each lattice point from $S$ by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when $S$ is bounded. For unbounded $S$, the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a $\Lambda$-subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to $W$ and to $V$ separately. Identity (6) holds only when $\mathbf{int}_W(S)$ meets $V$, and the half-space case (iii) is exactly the case where it does not.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and $\Lambda$ is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as $\mathbb Z+\sqrt2\mathbb Z$ is excluded. Dimensions are integers with $\dim\emptyset=-1$, and facets are nonempty, so no dimension equation holds through truncated subtraction.

Two readings of the page are fixed.

1. Theorem 9 assumes $\dim W\ge1$ and Theorem 10 assumes $\dim V\ge1$. For $W=V=\{0\}$ the only maximal set is $\emptyset$, which satisfies none of the listed cases, so the printed statements are false there.
2. Identity (6) is stated under the three hypotheses its proof uses, not inside the case analysis of Theorem 9.

The paper's Theorem 1 (the same result for $\mathbb Z^n$ and affine $W$) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in $\mathbb R^m$, discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.

Selected references

• A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Math. Oper. Res. 35(3), 2010; arXiv:1701.06543v1. https://arxiv.org/abs/1701.06543
• L. Lovász, Geometry of numbers and integer programming, in: Mathematical Programming: Recent Developments and Applications, 1989, pp. 177–210.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Oper. Res. 19, 1971. https://doi.org/10.1287/opre.19.1.19
• A. Barvinok, A Course in Convexity, Graduate Studies in Mathematics 54, AMS, 2002. https://doi.org/10.1090/gsm/054

Motivation

Every control policy formalized so far in this series — HLSPS (mission VI), back-pressure/ max-weight (mission VIII) — allocates service effort to entire job classes as indivisible units. Proportional fairness takes a different starting point: it is a general-purpose recipe for dividing a shared, continuously divisible resource among competing demands, originally developed for bandwidth allocation in communication networks and later adopted throughout economics and operations research as the canonical notion of a "fair" allocation. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Chapter 10 to showing that proportional fairness, applied dynamically to a processing network's current buffer contents, is not just an attractive fairness criterion but a maximally stable control policy — stable throughout the entire subcritical region of any unitary network. This mission formalizes the static optimization problem underlying proportional fairness, its key structural properties, the resulting fluid model, and the deepest single theorem of the chapter: fluid stability under the standard load condition, proved via a Lyapunov function that is explicitly not Lipschitz continuous — a genuine departure from every other stability proof in the book.

Setting

The PF allocation function $\psi(z)$ solves, for a demand vector $z \in \mathbb R^I_+$, the concave optimization problem $\max_{x \in \mathcal A} \sum_i z_i \log(x_i)$ (Eq. 10.3-10.4) over a bounded, closed, convex, monotone capacity-constraint set $\mathcal A$. When $\mathcal A$ has the special "aggregate" structure induced by grouping classes with identical resource requirements into demand groups, $\psi$ satisfies a resource-relevant aggregation property (Proposition 10.2): its value depends on the full demand vector only through group-level aggregates. Applying $\psi$ dynamically — recomputing it from the current buffer-content vector at every decision time — to a unitary network (one-to-one correspondence between job classes and service types) under relaxed control defines the PF control policy, whose fluid limit is the PF fluid model (Definition 10.3, Eqs. 10.29-10.35).

Formalization targets

Goal: Theorem 10.5 — fluid stability of the PF control policy

If the load condition (10.37) — an equivalent, group-level-aggregate reformulation of the standard load condition $\rho < b$ — holds, then the PF fluid model is stable. Combined with Theorem 6.2 (mission III) and Corollary 5.6, this is the technical core of showing PF control is maximally stable, exactly the same shape of result as mission VIII's back-pressure theorem, but for a policy defined by a fundamentally different (utility-maximization, rather than weighted-throughput-maximization) principle.

Supporting milestones

Lemma 10.1 establishes that $\psi$ is well-defined at all (existence), essentially unique where it matters (uniqueness on positive-demand coordinates), extreme, scale-invariant, and continuous — six properties that everything downstream depends on. Proposition 10.2 is the aggregation property described above. Proposition 10.4 restates the standard load condition in the group-level-aggregate coordinates Theorem 10.5's proof actually uses. Lemmas 10.6, 10.7, 10.8, and 10.9 develop the properties of the entropy Lyapunov function $\varphi(t) := \sum_i Z_i(t)\log(\dot D_i(t)/\alpha_i)$ (Eq. 10.38) that Theorem 10.5's proof needs: nonnegativity (and strict positivity away from the origin), continuity on $(0,\infty)$, a uniform upper bound on its Dini derivative, and a pointwise bound on that derivative at regular points, in terms of the fluid-scale departure and content rates.

Significance

The result itself. Theorem 10.5 shows that proportional fairness — motivated purely by a static fairness axiom (Eq. 10.14) with no reference to queueing dynamics at all — turns out to be a maximally stable dynamic control policy once applied recursively to a unitary network's evolving buffer contents. This is a substantive and non-obvious fact: nothing in PF's static definition anticipates a stability guarantee, and the book's own text stresses the mismatch between PF's static motivation (utility/fairness) and the metric of interest for a queueing system (buffer content, response time). Unlike essentially every other stability proof in the book, Theorem 10.5's proof uses a Lyapunov function ($\varphi$) that is provably not absolutely continuous, which is why it needs Lemma 8.11's more delicate Dini-derivative extinction criterion (mission V) rather than the simpler Lipschitz-based criteria (Lemmas 8.5/8.6) used everywhere else.

Formalizing it. A live prior-art check (GET /theorems?q=proportional%20fairness, q=entropy, q=concave%20optimization) finds no relevant hits — the one "entropy" result on the platform is an unrelated matrix-multiplication construction. This mission formalizes the concave PF optimization problem, its allocation function, the aggregation property, and the entropy Lyapunov machinery entirely from scratch, reusing only Mathlib's general convex-analysis and EReal substrate.

Difficulty

The chapter's own convention $\log(0) = -\infty$, $0\log(0) = 0$ (Eq. 10.2) cannot be captured by Mathlib's Real.log, whose value at 0 is 0, not -\infty — a silent substitution would corrupt exactly the boundary behavior Lemma 10.1(a)'s existence/uniqueness argument turns on (distinguishing feasible points with $x_i=0$ for some $i \in \mathcal I_+(z)$, which must be strictly dominated, from those without). This mission instead defines the PF objective via EReal, using an explicit extended logarithm (⊥ at 0) and Mathlib's own convention that EReal multiplication satisfies 0 * y = 0 for every y — which reproduces the book's 0 log(0) = 0 rule automatically, with no case split, a pleasant instance of genuine Mathlib substrate reuse resolving what looked like a from-scratch formalization problem. A second difficulty is structural: $\psi$ is not merely "a maximizer" but a specific maximizer, normalized to zero on every coordinate with zero demand (Eq. 10.5) — needed so that Lemma 10.1(c)/(d)'s scale-invariance and continuity statements are about a genuine function of $z$, not merely about an arbitrarily-chosen selection from a possibly-multivalued correspondence.

Formalization scope

IsPFDomain, f, IsPFMaximizer, and psi formalize Section 10.1's optimization problem directly, with IsPFMaximizer phrased as "feasible and dominates every feasible alternative" (avoiding sSup/⨆ entirely, per this series' junk-value-avoidance convention). IsTotalArrivalRates (restating Eq. 2.38) and RegularPoint (restating Definition 8.7) are restated locally, matching this series' convention that drafts do not import one another. diniUpperRight duplicates mission V's LyapunovCriteria.diniUpperRight verbatim — this chunk's own BRIEF.md dependency list does not include mission V, so, per the same restate-not-import convention, it is restated here rather than cross-imported (the duplication is intentional and documented, not an oversight). Lemma 10.7 (continuity of $\varphi$ on $(0,\infty)$) is added beyond BRIEF.md's own disposition table: the book itself lists it as one of "the following five lemmas" (10.6, 10.7, 10.8, 10.9, 10.11) that suffice to prove Theorem 10.5, on the same page as Lemmas 10.6/10.8/10.9 — a planning-time omission caught during drafting and documented in HARD.md. Lemma 10.11 itself, though stated on the same page, is not included here: the companion chunk (10-proportional-fairness-applications) explicitly begins at "Lemma 10.11 onward," and its own negative-drift conclusion is exactly what completes Theorem 10.5's proof — a dependency this mission's goal theorem does not need to expose in its own statement, since (10.37) is already the theorem's complete, book-stated hypothesis. IsPFDomain, IsPFMaximizer, psi, groupAggregate, IsPFFluidModelSolution, and phi are the primary reusable contributions; contributions completing the eight by sorry proofs, especially Lemma 10.1's six-part argument and the entropy-Lyapunov lemmas' analysis (Section B.4's preliminary results), are welcome.

Selected references

• J. G. Dai and J. Michael Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press (forthcoming), pre-publication draft 2020-4-2. http://spnbook.org
• F. P. Kelly, A. K. Maulloo, and D. K. H. Tan, "Rate control for communication networks: shadow prices, proportional fairness and stability," Journal of the Operational Research Society 49 (1998), 237–252.
• R. Srikant and L. Ying, Communication Networks: An Optimization, Control, and Stochastic Networks Perspective, Cambridge University Press, 2014.

Motivation

Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below $3/2$ unless P = NP; closing the gap between $3/2$ and $2$ has been open since.

The restricted assignment problem is the special case in which every job $j$ has a single size $p_j$ and may only run on a given set $\Gamma(j)$ of machines. The $3/2$ hardness already holds here, and the best known algorithms were still $2$-approximations. Every linear program previously used for the problem has integrality gap $2$, so a better LP lower bound was the natural target.

Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most $33/17 \approx 1.9412$. Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than $2$.

• 1990: Lenstra, Shmoys, Tardos, 2-approximation for unrelated machines, and $3/2$ hardness already for restricted assignment.
• 2006: Bansal and Sviridenko introduce the configuration LP for the max–min variant (the Santa Claus problem).
• 2008: Feige shows the configuration LP has constant integrality gap for restricted Santa Claus, and Asadpour, Feige and Saberi (2008) give a local search proof of a factor-4 gap.
• 2011: Svensson adapts that local search to makespan and proves the gap $33/17$ for restricted assignment (arXiv:1011.1168).

Setting

An instance consists of finite sets $J$ (jobs) and $M$ (machines), sizes $p_j \ge 0$, and for each job a set $\Gamma(j) \subseteq M$. A schedule is a map $\sigma : J \to M$ with $\sigma(j) \in \Gamma(j)$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$, and the makespan is the largest load. $\mathrm{OPT}$ is the least makespan of a schedule.

For a target makespan $T$, a configuration for machine $i$ is a set $C \subseteq J$ of jobs that may all run on $i$ ($i \in \Gamma(j)$ for $j \in C$) with $p(C) = \sum_{j \in C} p_j \le T$. Write $\mathcal C(i,T)$ for the set of configurations. The configuration LP asks for $x_{i,C} \ge 0$ with

$$\text{[C-LP]}\qquad \sum_{C \in \mathcal C(i,T)} x_{i,C} \le 1 \quad (i \in M), \qquad \sum_{i \in M}\ \sum_{C \in \mathcal C(i,T),\ C \ni j} x_{i,C} \ge 1 \quad (j \in J).$$

Its dual has variables $y_i, z_j \ge 0$ and constraints $y_i \ge \sum_{j \in C} z_j$ for all $i$ and $C \in \mathcal C(i,T)$. $\mathrm{OPT}_{LP}$ is the least $T$ at which [C-LP] is feasible, and $\mathrm{OPT}_{LP} \le \mathrm{OPT}$.

In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.

Formalization targets

Goal: Theorem 4.1

For every instance with $p \ge 0$ and every $T \ge 0$,

$$\text{[C-LP] feasible at } T \ \Longrightarrow\ \exists\, \sigma : J \to M,\ \ \sigma(j) \in \Gamma(j)\ \forall j,\quad \sum_{j : \sigma(j) = i} p_j \le \tfrac{33}{17}\, T \ \ \forall i .$$

Equivalently $\mathrm{OPT} \le \tfrac{33}{17}\,\mathrm{OPT}_{LP}$. The statement is scale-free and does not define $\mathrm{OPT}_{LP}$.

Milestones

The milestones follow the paper's proof, which normalizes $\mathrm{OPT}_{LP} = 1$ and sets $R = 16/17$:

1. a dual solution with $\sum_i y_i < \sum_j z_j$ makes [C-LP] infeasible;
2. the local search, Algorithm 2 (ExtendSchedule), keeps its partial schedule valid (load at most $1 + R$, at most one big job per machine);
3. when the algorithm has no potential move, an explicit pair $(y^*, z^*)$ is dual feasible (Claim 4.7) and has $\sum y^* < \sum z^*$ (Claim 4.8);
4. hence, if [C-LP] is feasible, a potential move always exists (Lemma 4.6);
5. the algorithm has no infinite run (Lemma 4.9);
6. [C-LP] feasible at $T = 1$ gives a schedule of makespan at most $1 + 16/17$.

Three facts from Section 2 complete the list: normalization by scaling, $\mathrm{OPT}_{LP} \le \mathrm{OPT}$, and monotonicity of feasibility in $T$.

Significance

The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor-$2$ algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within $33/17 + \epsilon$. The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to $11/6$ (Jansen and Rohwedder, 2017) along the same lines.

The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:

• a reusable definition of the configuration LP and its dual certificate;
• a precise, nondeterministic model of a local search whose termination rests on a lexicographic potential;
• a check of a proof that has many cases. The formalization already exposed two edge cases:
  • Claim 4.8 fails when $j_{\mathrm{new}}$ has size $0$ and no admissible machine;
  • the termination proof needs positive job sizes. With a job of size $0$, the algorithm can move it back and forth between two tied machines forever.

The milestones are stated with the corresponding hypotheses.

Difficulty

The obvious approach, rounding a fractional configuration solution, loses a factor $2$. If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.

The milestones along the paper's route are hard for two reasons. First, the dual pair $(y^*, z^*)$ rounds job sizes down by class (big to $11/17$, medium to $9/17$). Proving $\sum y^* < \sum z^*$ requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.

Formalization scope

Jobs and machines are finite types with decidable equality, sizes are real numbers with $p_j \ge 0$, and admissible machines are a Finset per job. Schedules are total maps $J \to M$ with $\sigma(j) \in \Gamma(j)$ stated explicitly. Partial schedules are maps $J \to$ Option M. Constants are exact rationals in $\mathbb R$. Values of moves live in Lex (ℝ × ℝ).

Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.

Three statements would trivialize the goal, and the formalization rules them out:

• a schedule allowed to use machines outside $\Gamma(j)$;
• a target $T < 0$;
• an LP missing either constraint row.

Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.

Useful contributions include:

• the weak-duality certificate;
• the scaling and monotonicity facts;
• the invariants of reachable states (each job lies in at most one blocker, blockers on a machine are never reassigned while present);
• the two claims and the termination argument.

The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.

Selected references

• O. Svensson, Santa Claus Schedules Jobs on Unrelated Machines, arXiv:1011.1168v2, 2011; SIAM J. Comput. 41(5), 2012. https://arxiv.org/abs/1011.1168
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Math. Programming 46, 1990. https://doi.org/10.1007/BF01585745
• N. Bansal, M. Sviridenko, The Santa Claus problem, STOC 2006. https://doi.org/10.1145/1132516.1132522
• A. Asadpour, U. Feige, A. Saberi, Santa Claus meets hypergraph matchings, APPROX 2008; ACM Trans. Algorithms 8(3), 2012. https://doi.org/10.1145/2229163.2229168
• K. Jansen, L. Rohwedder, On the configuration-LP of the restricted assignment problem, SODA 2017. https://arxiv.org/abs/1611.01934

Motivation

A Russian option is a perpetual American-type claim that pays, when the holder exercises at time $\tau$, the maximum of the asset price seen so far, discounted by $e^{-\alpha\tau}$. It was introduced by Shepp and Shiryaev for the Black–Scholes market (Shepp–Shiryaev 1993), where the underlying log-price is a Brownian motion with drift. Empirical work on asset returns (skewness, heavy tails, downward jumps) motivates replacing the Brownian motion by a Lévy process with negative jumps only. Avram, Kyprianou and Pistorius (2004) solve the Russian optimal stopping problem in that model in closed form, in terms of the scale functions of the process.

Timeline. 1993: Shepp and Shiryaev solve the Russian problem for geometric Brownian motion; Duffie and Harrison give its no-arbitrage price. Graversen and Peskir, and Kyprianou and Pistorius, treat further variants within the Black–Scholes market (the works the paper cites in §6). 2004: Avram, Kyprianou and Pistorius solve it for every spectrally negative Lévy process, covering both unbounded and bounded variation, using the exit problem of the reflected process $Y=\overline X-X$ (their Theorem 1, the subject of the first mission of this series).

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with a right-continuous filtration, and $X=\{X_t,\ t\ge0\}$ a spectrally negative Lévy process for $\mathbf F$: $X_0=0$, càdlàg paths with no positive jumps, independent and stationary increments with $X_{s+t}-X_s$ independent of $\mathcal F_s$, and paths that are not monotone. The standing assumption of the paper is that $X$ has unbounded variation, or bounded variation and a Lévy measure absolutely continuous with respect to Lebesgue measure.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$, and $\Phi(q)$ is the largest root of $\psi(\theta)=q$. For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$. Then $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$. The tilted scale functions $W_v^{(p)}$ are those of the exponent $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$.

Fix $r\ge0$ with $\psi(1)=r$ (the risk-neutral condition), and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$. For $z\ge0$, under $\mathbb P^1_{-z}$ the process starts at $-z$ with running maximum $\overline X_t=\max\{0,\sup_{u\le t}X_u\}$, and the reflected process $Y=\overline X-X$ starts at $Y_0=z$. The passage time is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$. Fix $\alpha>0$ and put $q=\alpha+r$.

The Russian optimal stopping problem (28) is

$$w^R(z)=\sup_\tau\ \mathbb E^1_{-z}\big[e^{-\alpha\tau+Y_\tau}\big],$$

the supremum over all $\mathbb P^1$-almost surely finite $\mathbf F$-stopping times. The option price is $V_r(M_0,S_0)=S_0\,w^R(\log(M_0/S_0))$.

Formalization targets

Goal: Theorem 2

With the optimal level (30) and the candidate value

$$\kappa^*=\inf\{x:\ Z^{(q)}(x)\le qW^{(q)}(x)\},\qquad u(z)=e^zZ^{(q)}(\kappa^*-z),$$

for every $z\ge0$,

$$w^R(z)=u(z)=\mathbb E^1_{-z}\big[e^{-\alpha\tau_{\kappa^*}+Y_{\tau_{\kappa^*}}}\big],$$

and $\tau_{\kappa^*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time.

Milestones

1. Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$.
2. Lemma 1: $Z^{(q)}(x)/W^{(q)}(x)\to q/\Phi(q)$ as $x\to\infty$ (for $q\ge0$, with the paper's convention for $0/\Phi(0)$).
3. Remark 3: $W_v(0+)=0$ if and only if $X$ has unbounded variation.
4. Corollary 1, (29): the value of stopping at $\tau_k$,

$$\mathbb E^1_{-z}\big(e^{-\alpha\tau_k+Y_{\tau_k}}\big)=e^z\Big(Z^{(q)}(k-z)+\frac{Z^{(q)}(k)-qW^{(q)}(k)}{W^{(q)\prime}(k)-W^{(q)}(k)}W^{(q)}(k-z)\Big).$$

5. Lemma 2 (i): for $q>r$, $f=Z^{(q)}-qW^{(q)}$ decreases on $[0,\infty)$ to $-\infty$.
6. Lemma 2 (ii): $\kappa^*=0$ if $W^{(q)}(0+)\ge q^{-1}$; otherwise $\kappa^*>0$ is the unique root of $f$.
7. The stopped process $e^{-\alpha(t\wedge\tau_{\kappa^*})}u(Y_{t\wedge\tau_{\kappa^*}})$ is a $\mathbb P^1$-martingale.
8. $\mathbb E^1_{-z}[e^{-\alpha t+Y_t}Z^{(q)}(\kappa^*-Y_t)]\le e^zZ^{(q)}(\kappa^*-z)$.
9. $e^{-\alpha t}u(Y_t)$ is a $\mathbb P^1$-supermartingale.

Significance

The result. Theorem 2 gives the price of the perpetual Russian option and its optimal exercise rule for every exponential spectrally negative Lévy market. The rule is to exercise when the ratio of the running maximum to the current price first reaches $e^{\kappa^*}$. The level is explicit through scale functions, and it separates the regimes: for bounded variation with $W^{(q)}(0+)\ge q^{-1}$, immediate exercise is optimal. The theorem is the model case of a general method: an optimal stopping problem for a functional of $(X,\overline X)$ is reduced, by a change of measure, to one for the reflected process, and solved by verification. The same method underlies the Canadized Russian option (third mission of the series).

Formalizing it. The result is proved in the paper; it has no machine-checked proof. This mission produces a Lean statement of the full verification theorem, including admissibility of $\tau_{\kappa^*}$. It also states the analytic facts about scale functions that the proof relies on (Lemmas 1, 2 and Remarks 3, 4), which apply to any problem phrased in scale functions.

Difficulty

The obvious route is the classical verification: show that $e^{-\alpha t}u(Y_t)$ is a supermartingale, apply optional stopping, and check equality at $\tau_{\kappa^*}$. The first step fails as a direct Itô computation. In the unbounded-variation case $u$ is only $C^1$ at $\kappa^*$, and in the bounded-variation case only continuous there. The generator of $Y$ is nonlocal, so smoothness away from $\kappa^*$ does not control the jump part of the process across the boundary. The equality case needs the exact value of stopping at $\tau_k$ (Corollary 1). That value requires the overshoot of $Y$ over $k$, which is caused by a downward jump of $X$, and the exit problem of the reflected process. Finally, $\mathbb P^1$ is not equivalent to $\mathbb P$ on $\mathcal F_\infty$, so passing from $\mathbb P$-facts to $\mathbb P^1$-facts is valid only on each $\mathcal F_t$.

Formalization scope

Conventions committed to in Lean:

• Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in $[0,\infty]$ (WithTop ℝ≥0), and the payoff is set to $0$ on $\{\tau=\infty\}$, a $\mathbb P^1$-null event for admissible $\tau$.
• The spectrally negative Lévy process is a structure: measurable marginals, $X_0=0$, independent increments, stationary increments, càdlàg paths, no positive jumps, not almost surely monotone. Paths start at $0$, are càdlàg, and have no positive jumps for every $\omega$, not merely almost surely. Adaptedness, independence of increments from the past, and right-continuity of $\mathbf F$ are added for the filtered version.
• "The usual conditions" are read as right-continuity only; completeness is not imposed. $\mathbb P^1$ is typically singular to $\mathbb P$ on $\mathcal F_\infty$, so a complete $\mathcal F_0$ would contradict (3).
• "Unbounded variation" means "not almost surely of bounded variation on compacts". Condition (AC) is stated through jumps: no jump lands in a Lebesgue-null set, almost surely. The standing assumption is "bounded variation implies (AC)".
• $\psi$ is Mathlib's cumulant generating function; "$\psi(v)<\infty$" is integrability of $e^{vX_1}$.
• $W^{(q)}$ is a definite description (choice among functions with the properties of Definition 2) for $q\ge0$, and the series (5) for $q<0$. $Z^{(q)}$ integrates over $(-\infty,x]$.
• $\mathbb P^1$ is data (a probability measure $\mathbb Q$) with $\mathbb Q|_{\mathcal F_t}=e^{X_t-rt}\cdot\mathbb P|_{\mathcal F_t}$ for all $t$. $\mathbb P^1_{-z}$ is encoded by the reflected process with prior maximum $0$ and starting point $-z$.
• The value function is a supremum in $[0,\infty]$ of lower Lebesgue integrals. Expectation identities (Corollary 1, the display on p. 230) are stated in $[0,\infty]$ and thereby assert finiteness.
• $W^{(q)}(0+)$ is Function.rightLim, and $\kappa^*$ is the real infimum (30); its nonemptiness is Lemma 2, not a hypothesis. $\tau_0=0$ extends the paper's $\tau_k$, $k>0$.
• Readings of informal words: "decreases monotonically" is strict decrease on $[0,\infty)$; "the unique root" is on $[0,\infty)$; Lemma 1 is formalized for $q\ge0$, with $0/\Phi(0)$ read as $\lim_{\theta\downarrow0}\theta/\Phi(\theta)$ as the paper stipulates; Remarks 3 and 4 for real $q$, $u$ only. The p. 230 martingale, bound and supermartingale claims are stated under the standing assumption, covering all three cases of the proof.

A trivializing formalization is ruled out: the supremum ranges over every $\mathbb P^1$-a.s. finite stopping time of the given filtration (not only passage times, not a smaller filtration), and it is taken in $[0,\infty]$, where no junk value of an unbounded real supremum can occur.

Infrastructure a complete development needs: Lévy processes on path space, their Laplace exponents and Esscher transforms, scale functions (existence, uniqueness, smoothness under the standing assumption), the reflected process and the exit identity of Theorem 1, optional stopping for continuous-time supermartingales, and Itô/change-of-variables formulas for semimartingales with jumps. The scale-function and Esscher layers are reusable for the other missions of this series and for any fluctuation-theory problem. Contributions to any of these layers, or to the milestones separately, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• L. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3(3), 631–640, 1993. https://doi.org/10.1214/aoap/1177005715
• J. Bertoin, Lévy Processes, Cambridge Tracts in Mathematics 121, Cambridge University Press, 1996. ISBN 0-521-56243-0
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014. https://doi.org/10.1007/978-3-642-37632-0