Prove2Me

Adding one unit to an odd best-of changes nothing

Proved
GameSetMatch.majorityAdv_even_eq

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

label-aggregationmajority-voteprobabilityrandom-walktennis

H2j+2(x)=H2j+1(x)H_{2j+2}(x)=H_{2j+1}(x).

Preamble
import Definitions.Def_GameSetMatchInternal
Formal statement
namespace GameSetMatch

/-- Adding one voter to an odd group changes nothing. -/
theorem majorityAdv_even_eq (j : ℕ) (x : ℝ) : majorityAdv (2 * j + 2) x = majorityAdv (2 * j + 1) 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