Strict-win probability is monotone in the per-unit advantage

Proved

GameSetMatch.strictWinProb_mono

by willma · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

label-aggregationmajority-voteprobabilityrandom-walktennis

For $r\in[0,1]$ and $0\le x\le y\le1$ : $W_J(r,x)\le W_J(r,y)$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `W_J(r, ·)` is nondecreasing on `[0,1]`. -/
theorem strictWinProb_mono (r : ℝ) (J : ℕ) (hr0 : 0 ≤ r) (hr1 : r ≤ 1)
    {x y : ℝ} (hx : 0 ≤ x) (hxy : x ≤ y) (hy : y ≤ 1) :
    strictWinProb (scoreContribLaw r x) J ≤ strictWinProb (scoreContribLaw r y) J := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md (private notes, 3 Sep 2026)

Human review

Endorsed by Shuze Chen · Sep 4, 2026
Endorsed by willma · Sep 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph