Lemma 1: the majority of all points is optimal among player-symmetric rules

Proved

GameSetMatch.symmetric_rule_le_majority

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

label-aggregationmajority-voteprobabilityrandom-walktennis

Let $J$ independent points each be won with probability $(1+s)/2$ , $s\in[0,1]$ . Let $f$ assign to every configuration of the $J$ point results a number in $[-1,1]$ (the conditional expected sign of the match result: $+1$ our win, $-1$ our opponent's, $0$ a fair coin), and suppose $f$ is player-symmetric: negating every point result negates $f$ . Then the expectation of $f$ is at most $H_J(s)$ , the advantage of taking the majority of all $J$ points.

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- **Lemma 1 (pairing).** Among player-symmetric rules deciding a match from `J` independent
points (each won w.p. `(1+s)/2`), the majority of all points maximises the expected match
result. `f x` is the conditional expected sign of the result (`+1` our win, `−1` theirs, `0` a
fair coin); player symmetry means flipping every point negates `f`. -/
theorem symmetric_rule_le_majority (J : ℕ) (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1)
    (f : (Fin J → Bool) → ℝ) (hf : ∀ x, |f x| ≤ 1)
    (hsym : ∀ x, f (fun i => !(x i)) = -f x) :
    ∑ x : Fin J → Bool, (∏ i, if x i then (1 + s) / 2 else (1 - s) / 2) * f x
      ≤ majorityAdv J s := 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