Threshold Policies Extend to Three-Server Queues

A cone-preservation proof handles one fast and two identical slow servers, closing the first nontrivial case beyond Lin-Kumar’s two-server model.

Editorial Desk·July 28, 2026·5 min readtheoretical

Underlying Paper

Optimality of a Threshold Policy for a Queueing System with One Fast Server and Two Identical Slow Servers

This paper studies the optimal control problem of a queueing system with three servers: one fast server and two identical slow servers. The two-server version of this problem, with one fast server and one slow server, was introduced by Lin and Kumar (1984), and the optimal policy has been shown to be of threshold type. However, generalizing this result beyond the two-server setting has been considered an open problem. In this paper, we resolve the first nontrivial case by proving that a threshold policy is optimal for the three-server system considered. The core technical ideas in this paper are generated by GPT-5.5 Pro. We have included a short report describing the authors' interactions with GPT-5.5 Pro. The authors verified the proofs and rewrote the paper for better rigor, clarity, and exposition. In addition, three key lemmas have also been verified in Lean 4.

arXiv:2607.22580Submitted: Jul 28, 2026v1

Queueing control has a simple intuition that is hard to prove once heterogeneous servers interact: use the fast server when possible, and send work to slower servers only after congestion is high enough. Lin and Kumar’s 1984 model with one fast and one slow server has that threshold structure. This paper proves the corresponding result for the next case, a system with one fast server and two identical slow servers, where the multi-slow-server extension had remained open.

The result is theoretical rather than computational. The authors study a nonpreemptive queue with Poisson arrivals, exponential service, one fast server, and two slower servers with equal rates. The system state can be represented as (q,z,y)(q,z,y), where qq is the queue length, z{0,1}z \in \{0,1\} records whether the fast server is busy, and y{0,1,2}y \in \{0,1,2\} records how many slow servers are busy. The control question is when an arriving or waiting job should be assigned to an idle slow server rather than held for the fast server.

Core Contribution

The paper’s main contribution is a proof that an optimal policy has a threshold form in the three-server system. In practical terms, for each slow-server occupancy level, once it is optimal to route a job to a slow server at a given congestion level, it remains optimal at larger congestion levels. That monotonicity is the structural statement needed to describe the optimal policy by thresholds rather than by an arbitrary state-dependent rule.

The new ingredient is not a new queueing model; it is the proof architecture. Prior two-server arguments did not carry over cleanly because two slow servers introduce an additional dimension: the proof must compare states with different numbers of busy slow servers while preserving the total population structure. The paper addresses this by strengthening the value-iteration cone with an extra convexity condition across the number of busy slow servers.

Technical Approach

The authors reduce the original control problem to a simplified post-decision state, essentially tracking the total population visible to the fast server together with the number of busy slow servers. They first show that the fast server can be treated by a reduction lemma: an optimal policy never sends a customer to an idle slow server while the fast server is idle and work is available. That removes a source of avoidable heterogeneity before the threshold argument begins.

The proof then defines a cone of value functions satisfying inequalities labeled (K1)–(K6). These inequalities encode monotonicity in total population, convexity-type relations, and the additional condition needed for the two-slow-server case. The central step is to show that the dynamic-programming operator preserves this cone. The visual proof pages show the most mechanical part of that argument: the authors enumerate possible minimizers a(x,y){0,1,2}a(x,y) \in \{0,1,2\} and verify case by case that the transformed function fˉ\bar f still satisfies inequalities such as

fˉ(x,y)+fˉ(x+1,y+1)fˉ(x+1,y)fˉ(x,y+1)0.\bar f(x,y)+\bar f(x+1,y+1)-\bar f(x+1,y)-\bar f(x,y+1) \geq 0.

This is where the three-server setting becomes visibly more complex than the two-server setting. For y=0y=0, the proof checks multiple tuples of minimizers, including cases such as (0,0,1,2)(0,0,1,2), (0,1,2,2)(0,1,2,2), and (2,2,2,2)(2,2,2,2); for y=1y=1, fewer boundary cases remain because two slow servers are already busy. The value of the paper is partly in making that finite verification explicit rather than hiding it behind an informal monotonicity claim.

Results and Analysis

The main theorem proves optimality of a threshold policy for the average-cost problem. The route to average cost is standard but detailed: the authors first work with discounted costs, prove cone preservation for the discounted dynamic program, then pass to an average-cost optimality equation using Sennott’s framework. The appendix verifies the needed recurrence, Lyapunov, and bounded-difference assumptions. Lemma 7 then lifts the optimal policy from the reduced state space back to the original state space, showing that no admissible original policy can beat the reduced threshold policy in long-run average holding cost.

There are no simulations, charts, or numerical experiments. That is appropriate for the claim: the paper is proving a structural theorem, not estimating performance. The evidence is therefore only as strong as the mathematical verification. On that axis, the paper is careful. It exposes the finite case checks, cites the average-cost machinery used for the limiting argument, and reports that three key lemmas were also checked in Lean 4.

A separate appendix documents how GPT-5.5 Pro contributed to the proof search. The authors say the model produced the main proof ideas, including strengthening Koole’s value-iteration cone with convexity in the number of busy slow servers along fixed total population. They also document errors: early versions contained a minor algebraic mistake and informal coupling arguments, and the authors rewrote the paper for rigor and readability. That disclosure weakens any claim that the generated text itself was reliable, but it strengthens the provenance record for the final proof: the mathematical result is presented as author-verified, with partial formal verification rather than as an unexamined model output.

Caveats

The theorem resolves one carefully chosen extension: exactly one fast server and exactly two identical slow servers. It does not prove the general many-slow-server conjecture, does not handle nonidentical slow servers, and does not provide performance gains from using the threshold representation in computation. The authors’ own GPT interaction report also makes clear that the discovery process produced flawed drafts before the final argument stabilized. The contribution is best read as a resolved base case and a possible proof template for larger systems, not as a completed theory of heterogeneous multi-server routing.

Evidence Box

theoretical

Key Claims

  • Threshold policy is optimal for one fast and two identical slow servers
  • Strengthened value-iteration cone handles the first multi-slow-server case
  • Average-cost optimality follows from the discounted-cost structural proof
  • GPT-5.5 Pro generated core proof ideas later verified by the authors

Key Results

  • 3-server system proved: 1 fast server and 2 identical slow servers
  • State reduction uses (q,z,y) with z ∈ {0,1} and y ∈ {0,1,2}
  • Cone proof preserves 6 inequalities labeled K1–K6 under value iteration
  • 3 key lemmas additionally verified in Lean 4

Limitations & Caveats

  • No extension to more than 2 slow servers
  • Slow servers assumed identical
  • No numerical evaluation of threshold computation or cost savings
  • GPT-generated drafts contained algebraic and coupling-proof errors before author revision

Related Articles

Readers are encouraged to consult the original arXiv paper for complete details. SOTA Papers does not make claims beyond what is supported by the authors' reported evidence.