Theorem 4, second sentence, PDF p. 6 — on s₁ ≤ s₂ ≤ φs₁, R = 1 + s₂/(s₁ + s₂) ≤ φ, with equality at s₂/s₁ = φ

Proved

WorstCaseEq.Speeds.R_le_goldenRatio

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

golden-ratiop2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1price-of-anarchy

Let $\varphi=(1+\sqrt5)/2$ be the golden ratio and let $0<s_1\le s_2\le\varphi s_1$ . Then

R=1+\frac{s_2}{s_1+s_2}\le\varphi,

and $R=\varphi$ when $s_2/s_1=\varphi$ .

So the lower bound of Theorem 4 is largest, equal to the golden ratio, at the edge $s_2=\varphi s_1$ of the range on which it applies.

Formalization Note The ratio condition $s_2/s_1=\varphi$ is written $s_2=\varphi s_1$ , equivalent because $s_1>0$ . The golden ratio is Mathlib's Real.goldenRatio.

Preamble

import Mathlib
import Definitions.Def_agt_games
import Definitions.Def_WorstCaseEq_Speeds_Model

Formal statement

namespace WorstCaseEq.Speeds

theorem R_le_goldenRatio (s₁ s₂ : ℝ) (h₁ : 0 < s₁) (h₁₂ : s₁ ≤ s₂)
    (hφ : s₂ ≤ Real.goldenRatio * s₁) :
    1 + s₂ / (s₁ + s₂) ≤ Real.goldenRatio ∧
      (s₂ = Real.goldenRatio * s₁ → 1 + s₂ / (s₁ + s₂) = Real.goldenRatio) := by sorry

end WorstCaseEq.Speeds

Source

Koutsoupias & Papadimitriou, Worst-case equilibria (journal version, 2009), PDF p. 6, Theorem 4 (second sentence)

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph