# Verification report: AIM-PROBABILITY-0027

Result: complete proof of explicit stationary JSQ approximation bounds.
Author: Alper Ferudun, Mercury Software GmbH. Date: 28 September 2026.
Verification basis: originating-researcher detailed self-audit.
Not independently peer reviewed or formally verified.

## Mathematical scope

N unit-rate exponential servers, Poisson arrival rate 0 < lambda < N,
rho=lambda/N. The manuscript proves explicit total-variation bounds against
capacity-b JSQ for any integer b>=1, and against shortest-of-k routing with
or without replacement. It also proves sharp finite-buffer light-traffic
order Theta(lambda^(bN+1)) with N,b fixed.

The arguments explicitly establish recurrence, stationary moments, the
weak-majorization comparison, empty-state regeneration, Poisson-integral
convergence, linear growth and integrable generator identities. The full
proof does not assume coordinatewise JSQ domination by random routing.
The two arrival successors in the sampled-routing argument are coupled
below a third full-JSQ chain, not assumed ordered.

## Computational reproduction

The standard-library checker makes 126,180 assertions:

- 45,514 weak-majorization arrival comparisons.
- 45,514 ranked-service comparisons.
- 32,478 labelled monotone updates.
- 2,520 routing and drift checks.
- 102 capacity-generator identities.
- 20 exact finite-stationary examples.
- 32 further arbitrary-capacity stationary examples.

Stationary linear systems and transition algebra use rational arithmetic.
Floating Chernoff displays use a stated small rounding tolerance; the
symbolic bound is proved in the manuscript. Capacity-four versus capacity-two
TV values are diagnostics only, not the infinite-system error.
The release receipt records isolated runs in two Python runtimes, with
assertions enabled, and comparison to the preserved original report.

The archived official AIM Problem 1.35 matches the frozen source record
after typographical normalization. The source asks an open-ended quantitative
question, so the release records completion of this theorem and not closure
of every version of that programme.

## Manuscript checks

Six pages. Native desktop LaTeX compilation succeeded, Tectonic PDF export
succeeded, and all six final rendered pages were visually inspected. No
unresolved references, missing characters, overfull/underfull boxes or LaTeX
warnings remained. Author name is alone at the top; company and contact
details are in its footnote. AI assistance is disclosed in ordinary prose.

## Limitations and prior art

Constants may equal the trivial total-variation bound one at high load or
large N. There is no sharp many-server theorem, unbounded-test-function bound
or exact leading coefficient here. The methods are established prior art.
The bounded literature search is documented; originality is not certified.
Publication and a DOI do not imply peer review or endorsement.