Odd best-ofs cannot tie
ProvedGameSetMatch.bestOfWinProb_eq_fairCoin_of_oddlabel-aggregationmajority-voteprobabilityrandom-walktennis
For odd : bestOfWinProb N q = bestOfFairCoinWinProb N q.
Preamble
import Definitions.Def_GameSetMatchInternal
Formal statement
namespace GameSetMatch
/-- An odd best-of cannot tie. -/
theorem bestOfWinProb_eq_fairCoin_of_odd (N : ℕ) (hN : Odd N) (q : ℝ) :
bestOfWinProb N q = bestOfFairCoinWinProb N q := by
sorry
end GameSetMatchSource
Mission statement 'Don't Label Twice: Game, Set, Match', parts (a)–(d)
Human review
Confirmed by the mission captain (proposal self-audit).