Prove2Me

Lemma 1 — β(α+1)≤13α2+53β2\beta(\alpha+1) \le \frac13\alpha^2 + \frac53\beta^2 for nonnegative integers

Proved
CongestionPoA.AsymSum.lemma1

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

inequalityp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1price-of-anarchy

For every pair of nonnegative integers α,β\alpha,\beta,

β(α+1)≤13α2+53β2.\beta(\alpha+1)\le \frac13\alpha^2+\frac53\beta^2.

This elementary inequality is the arithmetic heart of the 5/25/2 bound for the average social cost: applied facility by facility with α=ne(A)\alpha=n_e(A) and β=ne(P)\beta=n_e(P), it turns the bound obtained from the Nash conditions into a bound by 13SUM(A)+53SUM(P)\frac13\mathrm{SUM}(A)+\frac53\mathrm{SUM}(P).

Formalization Note α\alpha and β\beta are natural numbers and the inequality is read in the reals. The hypothesis that they are integers is essential: for real α=0\alpha=0, β=1/2\beta=1/2 the left side is 1/21/2 and the right side is 5/125/12.

Preamble
import Mathlib
Formal statement
namespace CongestionPoA.AsymSum

/-- Christodoulou and Koutsoupias, *The Price of Anarchy of Finite Congestion Games*, STOC 2005,
PDF p. 3, Lemma 1: for every pair of nonnegative integers `α, β`,
`β(α + 1) ≤ (1/3)α² + (5/3)β²`.

**Formalization Note.** `α` and `β` range over `ℕ` and the inequality is read in `ℝ`. Integrality is
essential: over the reals the inequality fails at `α = 0`, `β = 1/2`. -/
theorem lemma1 (α β : ℕ) :
    (β : ℝ) * ((α : ℝ) + 1) ≤ (1 / 3 : ℝ) * (α : ℝ) ^ 2 + (5 / 3 : ℝ) * (β : ℝ) ^ 2 := by sorry

end CongestionPoA.AsymSum
Source
Christodoulou and Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, DOI 10.1145/1060590.1060600, PDF p. 3, Lemma 1
Human review

  • Endorsed by Shuze Chen · Oct 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph