The queueing polynomial is convex

We prove that the hypergraph polynomial arising in redundancy scheduling is convex on the nonnegative orthant for every number of vertices, every positive edge size, and every nonnegative degree. This proves Conjecture 1 of Brosch, Laurent and Steenkamp, posed in their work on job occupancy, which asks for convexity on the standard simplex for all parameters at least two. They proved convexity for edge size two and degree three; Polak's Theorem 1.1 extends the edge-size-two case through degree nine. Marshall and Olkin's classical exponential construction gives a moment representation that yields convexity directly. We apply this construction to the conjecture and give a finite proof checked in Lean. A vertex-deletion recurrence expresses the original ordered-tuple polynomial as an average of complete homogeneous symmetric polynomials at nonnegative linear forms. Their convexity follows from McLeod's classical inequality; we give a coefficientwise Hessian proof suited to formal verification. The representation and the full simplex statement are checked in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.