Operations Research

Motivation

The $k$-server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$-server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

• 1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
• 1988–1990. Manasse, McGeoch, and Sleator introduce the $k$-server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$-server conjecture, in the symmetric finite setting of the paper.
• 1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
• 1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
• 1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$.
• 1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
• 2004. Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
• 2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
• 2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
• 2026. Coester, Koutsoupias, and Zbysiński post The $k$-server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$-competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the movement cost is the total distance traveled,

$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

• Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
• The service constraint. Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its cost is the total movement along this trajectory:

$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.

Finally, $A$ is $c$-competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$

Formalization targets

Goal — the $k$-server conjecture

$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$

The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

• M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
• A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
• M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
• M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
• E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
• E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
• C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
• S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
• E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

• 1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
• 1981. Beck and Fiala (Discrete Appl. Math.) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
• 1980s. Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
• 1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
• 1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
• 2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
• 2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
• 2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A sign vector is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$

The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
• W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
• N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
• N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
• D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
• B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

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

Motivation

A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range $\mathcal{Z}$, and let it degrade at a controlled rate outside, proportionally to the distance from $\mathcal{Z}$. That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.

Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most $\alpha \,\mathrm{dist}(\zeta, \mathcal{Z})$" has no direct meaning. What replaces it is the observation that a scalar inequality $a^Ty - b \le 0$ is the inclusion $a^Ty - b \in \mathbf{Q} \equiv \mathcal{R}_-$, and that the violation is the distance from the left hand side to $\mathbf{Q}$. In that form the notion lifts verbatim, and the whole chapter follows.

Setting

Definition 11.1.2. Consider an uncertain convex constraint

$$\Bigl[P^0 + \sum_{\ell=1}^L \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_{\ell=1}^L \zeta_\ell p^\ell\Bigr] \ \in\ \mathbf{Q}, \tag{11.1.4}$$

with $\mathbf{Q} \subseteq \mathcal{R}^k$ nonempty, closed and convex. Let the perturbation space split as $\mathcal{R}^L = \mathcal{R}^{L_1}\times\cdots\times\mathcal{R}^{L_S}$, each factor carrying a normal range $\mathcal{Z}^s$, a closed convex cone $\mathcal{L}^s$ and a norm $\|\cdot\|_s$, and let $\|\cdot\|_{\mathbf{Q}}$ be a norm on $\mathcal{R}^k$. A candidate $y$ is robust feasible with global sensitivities $\alpha_s$ if

$$\mathrm{dist}\bigl(P(y,\zeta), \mathbf{Q}\bigr) \ \le\ \sum_{s=1}^S \alpha_s\, \mathrm{dist}(\zeta^s, \mathcal{Z}^s|\mathcal{L}^s) \qquad \forall\, \zeta \in \mathcal{Z} + \mathcal{L}, \tag{11.1.6}$$

where $\mathrm{dist}(u,\mathbf{Q}) = \min_{v\in\mathbf{Q}}\|u - v\|_{\mathbf{Q}}$ and $\mathrm{dist}(\zeta^s,\mathcal{Z}^s|\mathcal{L}^s) = \min\{\|\zeta^s - v\|_s : v \in \mathcal{Z}^s,\ \zeta^s - v \in \mathcal{L}^s\}$.

The object that makes the analysis work is the recessive cone of $\mathbf{Q}$ (Definition 11.3.1): for any $\bar x \in \mathbf{Q}$,

$$\mathrm{Rec}(\mathbf{Q}) = \{h : \bar x + th \in \mathbf{Q}\ \ \forall t \ge 0\},$$

which does not depend on $\bar x$ and is a nonempty closed convex cone.

Formalization targets

Goal — Proposition 11.3.3, the decomposition of the conic GRC

A candidate $y$ is feasible for the GRC (11.1.6) if and only if it satisfies the system

$$\text{(a)}\quad \Bigl[P^0 + \sum_\ell \zeta_\ell P^\ell\Bigr]y - \Bigl[p^0 + \sum_\ell \zeta_\ell p^\ell\Bigr] \in \mathbf{Q} \qquad \forall \zeta \in \mathcal{Z} = \mathcal{Z}^1\times \cdots\times\mathcal{Z}^S,$$ $$\text{(b}_s)\quad \mathrm{dist}\Bigl(\sum_{\ell} [P^\ell y - p^\ell](E_s\zeta^s)_\ell,\ \mathrm{Rec}(\mathbf{Q})\Bigr) \ \le\ \alpha_s \qquad \forall \zeta^s \in \mathcal{L}^s \text{ with } \|\zeta^s\|_s \le 1, \quad s = 1,\ldots,S .$$

Line (a) is the ordinary robust counterpart over the normal range. Each line (b$_s$) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to $\mathbf{Q}$ itself.

Supporting targets

$$\text{(Def 11.3.1)}\quad \mathrm{Rec}(\mathbf{Q}) \text{ is independent of the base point and is a nonempty closed convex cone},$$ $$\text{(Ex 11.3.2)}\quad \mathbf{Q} \text{ bounded} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \{0\}; \quad \mathbf{Q} \text{ a cone} \Rightarrow \mathrm{Rec}(\mathbf{Q}) = \mathbf{Q}; \quad \mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\},$$ $$\text{(Prop 11.4.1)}\quad \Psi_\Xi(\mathcal{M}) = \Psi_{\Xi_*}(\mathcal{M}^*), \qquad \Psi(\mathcal{M}) = \max\{\mathrm{dist}_{\|\cdot\|_F}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\} .$$

Significance

The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.

The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b$_s$) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function

$$\Psi(\mathcal{M}) = \max\bigl\{\mathrm{dist}(\mathcal{M}e, \mathbf{K}^F) : e \in \mathbf{K}^E,\ \|e\|_E \le 1\bigr\}$$

of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that $\Psi$ of a map with respect to a setup equals $\Psi$ of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on $\Psi$ be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.

The recessive cone results are the vocabulary. The one that earns its place is $\mathrm{Rec}\{u : Au - b \in \mathbf{K}\} = \{h : Ah \in \mathbf{K}\}$: the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.

Difficulty

The goal is an equivalence and the two directions are asymmetric.

Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix $\bar\zeta \in \mathcal{Z}$ and $\zeta^s$ in the unit ball of $\mathcal{L}^s$, and run $\zeta_i = \bar\zeta + i\,\zeta^s$ out along the cone. The GRC bounds the distance to $\mathbf{Q}$ by $\alpha_s i$, so there are $q_i \in \mathbf{Q}$ with $\|P(y,\bar\zeta) + i\Phi(y)E_s\zeta^s - q_i\|_{\mathbf{Q}} \le \alpha_s i$; the rescaled points $q_i/i$ stay bounded, and a limit point of them lies in $\mathrm{Rec}(\mathbf{Q})$ by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not $\mathbf{Q}$ — is what appears in lines (b$_s$).

Backward is a decomposition-and-assemble: split each $\zeta^s = \bar\zeta^s + \delta^s$ with $\bar\zeta^s \in \mathcal{Z}^s$, $\delta^s \in \mathcal{L}^s$ realizing the distance, get a point of $\mathbf{Q}$ from line (a) and a recession direction from each line (b$_s$), and add them — using that $\mathbf{Q} + \mathrm{Rec}(\mathbf{Q}) \subseteq \mathbf{Q}$.

Proposition 11.4.1 is a chain of polarity identities: the polar of $X + K$ is $X^o \cap (-K_*)$ for compact convex $X$ containing the origin, the polar of a norm ball of radius $\alpha$ is the dual-norm ball of radius $1/\alpha$, and bipolarity. Each step is standard and the composition is not.

Formalization scope

Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function $\Psi$.

Conventions committed to:

• Norms are functions carrying an explicit predicate, not typeclass instances. Chapter 11 quantifies over arbitrary norms $\|\cdot\|_{\mathbf{Q}}$ and $\|\cdot\|_s$ on fixed coordinate spaces, and a statement must be able to range over them; a typeclass instance would fix one norm per type. IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and nonnegativity follows from them.
• The dual norm is a predicate, not a construction. $\|f\|^* = \sup\{f^Te : \|e\| \le 1\}$ is asserted as a least upper bound of the set of values, so no supremum is taken on faith.
• Distances are infima, not minima. The source writes $\min$, which is correct because the sets are closed; writing $\inf$ avoids carrying an attainment proof into every statement, and agrees with the minimum whenever the source's own hypotheses hold.
• The recessive cone is indexed by a base point. Definition 11.3.1 defines it at an arbitrary $\bar x \in \mathbf{Q}$ and then asserts independence of the choice; that assertion is one of the published items, so the definition cannot presuppose it.
• The perturbation is carried as a family of blocks, $\zeta = (\zeta^1,\ldots,\zeta^S)$ with $\zeta^s \in \mathcal{R}^{L_s}$, rather than as a single vector in $\mathcal{R}^L$ together with the embeddings $E_s$. This is the same data and removes the index bookkeeping of $E_s$ from every statement.
• $\Psi$ is a predicate on a real number, as for the dual norm and for the same reason.
• §11.2 and §11.5 are out of scope: the definition of a tight safe approximation of a GRC and the worked analysis of nonexpansive dynamical systems. The first is a definition the chapter uses only to phrase §11.4's programme, the second an application.

Selected references

• A. Ben-Tal, L. El Ghaoui and A. Nemirovski, Robust Optimization, Princeton University Press, 2009. Chapter 11, §§11.1, 11.3-11.4, pp. 281-294; Chapter 3 for the linear case. https://doi.org/10.1515/9781400831050
• A. Ben-Tal, S. Boyd and A. Nemirovski, Extending scope of robust optimization: comprehensive robust counterparts of uncertain problems, Mathematical Programming 107 (2006), 63-89. https://doi.org/10.1007/s10107-005-0679-z
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$

It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

$$2^n - 1 \text{ pivots}$$

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within

$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

• L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
• S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
• É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
• G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
• O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
• S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
• Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
• X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
• X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
• D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
• B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

Motivation

The multiarmed bandit problem asks how a gambler should allocate successive plays among $n$ independent projects, each of which changes state only when it is played, so as to maximize the expected total-discounted reward. Gittins and Jones (1974) showed that it is optimal to play, at every epoch, a project of greatest Gittins index, a number computed from that project alone. The result underlies job scheduling on a single machine, sequential clinical trials and many stochastic resource-allocation models.

Weber (1992) gave a short proof of the index theorem through prevailing charges, and used the same idea to prove a result that was new: the optimal value is a submodular function of the set of projects that are available. Submodularity of the value says that the marginal worth of an extra project shrinks as more projects are on hand. Two consequences appear in the paper: for statistically identical projects started in a common state, the optimal value is concave in their number; and a bound of Tsitsiklis (1986) for a problem with a retirement option is a special case.

Timeline. Gittins and Jones (1974): the index theorem, by an interchange argument (book-length treatment in Gittins (1989)). Whittle (1980): a proof through a retirement option. Varaiya, Walrand and Buyukkoc (1985): the interchange argument in a general setting. Tsitsiklis (1986): a short proof of the index theorem, including the bound $V(S)\le V(\{i,1\})+V(S\setminus\{i\})-M$ for a retirement bandit. Weber (1992): the prevailing-charge proof and the submodularity of the value (Theorem 4).

Setting

There are $n$ bandits $j\in\{1,\dots,n\}$. Bandit $j$ is a Markov chain on a state space $S$ with transition kernel $P$; at each epoch $t=0,1,2,\dots$ the gambler plays one bandit $j(t)$, receives the reward $r(x_{j(t)}(t))$, the played bandit moves one step of its chain and the others stay where they are. Rewards are nonnegative and uniformly bounded, and $0<\beta<1$ is the discount factor. The initial states $x(0)=x$ are fixed. A policy chooses $j(t)$ from the history; its value is $V_\pi(x)=\mathbb E_\pi\big[\sum_{t\ge0}\beta^t r(x_{j(t)}(t))\big]$.

For a set of bandits $I\subseteq\{1,\dots,n\}$, the restricted problem $P(I)$ is the same game played with the bandits of $I$ only, each started in its state in $x$, and

$$V(I)=\sup_\pi V_\pi\quad\text{over the policies of }P(I),\qquad V(\emptyset)=0 .$$

The fair charge $\gamma(y)$ of a state $y$ is the largest ratio of expected discounted reward to expected discounted time over stopping times $\tau\ge1$ of a single bandit started at $y$ (Weber's (4)). On a fixed realisation, where bandit $j$ passes through states $\omega_j(0)=x_j,\omega_j(1),\dots$ on its successive plays, the prevailing charge after $k$ plays is $\gamma_{jk}=\min_{0\le v\le k}\gamma(\omega_j(v))$, a nonincreasing sequence. $U_t(I)$ is the sum of the first $t$ terms of the interleaving of the sequences $(\gamma_{jk})_{k\ge0}$, $j\in I$, into nonincreasing order.

Formalization targets

Goal: Theorem 4, eq. (9)

$$V(I\cap J)+V(I\cup J)\le V(I)+V(J)\qquad\text{for all }I,J\subseteq\{1,\dots,n\}.$$

This holds for arbitrary bandits (no identical-bandit hypothesis) under the standing assumptions of the paper's Section 1.

Milestones on the path

1. Eq. (10): for nonincreasing nonnegative sequences and every $t\ge0$, $U_t(I\cap J)+U_t(I\cup J)\le U_t(I)+U_t(J)$. A deterministic inequality.
2. The representation used in the last line of the proof:

$$V(I)=\mathbb E\Big[\sum_{t\ge0}\beta^t\big(U_{t+1}(I)-U_t(I)\big)\Big],$$

the expectation over independent realisations of the bandits' state sequences.

Consequences stated in the paper

3. Identical bandits started in a common state: $m\mapsto V$ of the $m$-bandit problem is nondecreasing and concave.
4. Tsitsiklis's bound: if bandit $b$ always pays $(1-\beta)M$, then $V(S)\le V(\{i,b\})+V(S\setminus\{i\})-M$ for $i\ne b$.

Significance

Submodularity of the value is a structural fact about the bandit problem that the index theorem alone does not give: the index theorem identifies an optimal policy for a fixed set of projects, while (9) compares optimal values across sets. It yields diminishing returns from adding projects, the concavity of the value in the number of identical projects, and Tsitsiklis's retirement bound, which separates one project from the rest. Bounds of this kind are used when choosing which projects to make available before allocation begins.

Theorem 1 of the paper, the optimality of the Gittins index policy, is already on Prove2Me as BanditAlgorithm.gittins_index_theorem (Proved, Shuze Chen), together with the discounted Markov bandit model and the Gittins index (GittinsIndex, Shuze Chen) and a finite-horizon form of the prevailing-charge coupling (BanditAlgorithm.gittins_finite_prevailing_charge_eq_stack_coupling_value, Harry_Xu). This mission builds on those items. Theorem 4, inequality (10) and the infinite-horizon representation of $V(I)$ have no machine-checked proof that we know of. The other two missions of this series formalize Weber's Theorem 2 (mission 1, a suboptimality bound by prevailing charges) and Theorem 3 (mission 2, a suboptimality bound by index gaps); this mission does not depend on them.

Difficulty

Inequality (10) concerns sums of largest terms of merged sequences; it fails without nonnegativity when $I$ and $J$ are disjoint, and a proof must use both the monotonicity of each sequence and the sign of the terms. The representation of $V(I)$ requires the fair-game property of prevailing charges in infinite horizon: that the optimal policy of $P(I)$ collects in expectation exactly the discounted charges it pays, and that, on a common probability space of independent bandit trajectories, the charges paid by the optimal policy are the nonincreasing interleaving. The finite-horizon coupling is on the platform; passing to infinite horizon, identifying the interleaving with the play of an index policy, and handling ties and measurability are the remaining work. Finally, (10) is an undiscounted, pathwise statement while (9) compares discounted expectations, so the two must be connected through series of increments of $U_t$ and an exchange of expectation and series.

Formalization scope

The model is the published BanditAlgorithm discounted Markov bandit: one standard Borel state space $S$, one kernel $P$ and one measurable reward $r$ shared by all bandits; bandits with different dynamics are encoded by a disjoint union of state spaces. $r$ is the mean reward. The value of a policy is the series of per-round expected rewards (markovBanditDiscountedValue), equal to the expectation of the discounted sum for bounded rewards. The fair charge $\gamma$ is the published gittinsIndex.

Explicit readings of the paper's phrases:

• "the restriction of the problem to bandits in $I$": the $|I|$-armed game whose arms are the bandits of $I$ in increasing order, started at their states in $x$ (restrictedValue), with $V(\emptyset)=0$ set explicitly;
• "the maximal expected total-discounted reward": the supremum over all history-dependent randomized policies;
• "a fixed realisation of the states through which bandit $j$ evolves": a point of the product of independent Markov chain laws Measure.pi (fun j => markovChainMeasure P (x j));
• "interleaving into nonincreasing order … summing the first $t$ elements": partialInterleavedSum, the maximum over allocations of $t$ plays of the sum of initial segments, equal to the interleaving sum for nonincreasing sequences, with $U_t(\emptyset)=0$; the sequences start at $k=0$ (the printed $\{\gamma_{jk}\}_{k=1}^\infty$ is a misprint);
• "multiplying (10) by $\beta^t$, summing": the discounted charge is $\sum_t\beta^t(U_{t+1}-U_t)$, the increments of $U_t$;
• "rewards are nonnegative and uniformly bounded", $0<\beta<1$: binders of every probabilistic statement, together with StandardBorelSpace S and Measurable r;
• "concave increasing": nondecreasing and with nonincreasing increments, including $n=0$;
• "bandit 1 always pays $(1-\beta)M$": an absorbing initial state with reward $(1-\beta)M$.

Trivializing formalizations are ruled out: $V(\emptyset)$ and $U_t(\emptyset)$ are defined as $0$ rather than obtained from a supremum over an empty type, the supremum defining $V(I)$ is over a nonempty family bounded by $C/(1-\beta)$, $U_t$ is a maximum over a finite nonempty set, and the hypotheses are satisfiable (checked on a one-bandit instance).

A complete development needs: the infinite-horizon prevailing-charge identity for index policies, measurability of the charge stacks (the measurability of gittinsIndex is on the platform), and a combinatorial lemma on merges of nonincreasing sequences. Inequality (10) and the merge lemmas are reusable beyond bandits, for sums of largest elements and weighted rank functions of uniform matroids.

Selected references

• R. Weber, On the Gittins index for multiarmed bandits, Ann. Appl. Probab. 2(4), 1024–1033, 1992. https://doi.org/10.1214/aoap/1177005588
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani, ed.), North-Holland, 241–266, 1974.
• J. C. Gittins, Bandit Processes and Dynamic Allocation Indices, Wiley, 1989.
• P. Whittle, Multiarmed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42, 143–149, 1980.
• P. Varaiya, J. Walrand, C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30, 426–439, 1985.
• J. N. Tsitsiklis, A lemma on the multiarmed bandit problem, IEEE Trans. Automat. Control 31, 576–577, 1986.
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. https://doi.org/10.1017/9781108571401

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$. Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ($L_\infty$) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$.

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

• 1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$.
• 1984. Megiddo extends the method to every fixed $d$, with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
• 1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$. Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
• 1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$. An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$, and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$. Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$. It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$, then $A$ row by row, then $b$. A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$, answers whether $a^Tx^*<b$, $=b$ or $>b$. Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$, the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

$$\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.$$

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

1. One query settles half of $n$ hyperplanes on the line ($A(1)=1$, $B(1)=\tfrac12$).
2. $v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$, so there is a basis in which all $a_{ij}\ne0$.
3. For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$, $H_k$.
4. A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$, and the middle hyperplane settles one of them.
5. Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
6. $C(d)\log n$ queries settle all $n$ hyperplanes.
7. If a hyperplane contains no optimal point, all optimal points lie on one side of it.
8. The oracle, Case I: at an optimum relative to $\{x_d=0\}$, two auxiliary systems decide the side or certify global optimality.
9. The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$, systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$, so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$, including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$. The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$, when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

• Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
• Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$. The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$. The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
• Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
• Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$. A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
• Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
• Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$, where the page's last sentence says $\{x_d<0\}$. The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$, the hypothesis its argument uses, since linear independence alone does not give it.
• Not included. Approach II and its bound $O(n(\log n)^{d^2})$, the remarks on slowly growing $d$, the randomized variants, and the applications of §1.
• Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

• N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
• N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
• M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
• K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
• R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
• B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046