Linear bound on the majority advantage

Proved

GameSetMatch.majorityAdv_le_mul

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

label-aggregationmajority-voteprobabilityrandom-walktennis

$H_\ell(z)\le\ell z$ for $z\in[0,1]$ (equation (11)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- `H_ℓ(z) ≤ ℓ z`. -/
theorem majorityAdv_le_mul (l : ℕ) (z : ℝ) (hz0 : 0 ≤ z) (hz1 : z ≤ 1) : majorityAdv l z ≤ l * z := 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