Nothing ignored: win-loss advantage is the majority advantage

Proved

GameSetMatch.winLossAdv_one_eq_majorityAdv

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

label-aggregationmajority-voteprobabilityrandom-walktennis

winLossAdv 1 x J = majorityAdv J x for all real $x$ and all $J$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- With nothing ignored, the win-loss advantage of `J` contributions is `H_J`. -/
theorem winLossAdv_one_eq_majorityAdv (x : ℝ) (J : ℕ) : winLossAdv 1 x J = majorityAdv J x := 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