Prove2Me

Adding two units to an odd best-of

Proved
GameSetMatch.majorityAdv_odd_succ_sub

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

label-aggregationmajority-voteprobabilityrandom-walktennis

H2j+3(x)−H2j+1(x)=(2j+2j+1)4−(j+1)x(1−x2)j+1H_{2j+3}(x)-H_{2j+1}(x)=\binom{2j+2}{j+1}4^{-(j+1)}x(1-x^2)^{j+1}.

Preamble
import Definitions.Def_GameSetMatchInternal
Formal statement
namespace GameSetMatch

/-- Adding two voters to an odd group. -/
theorem majorityAdv_odd_succ_sub (j : ℕ) (x : ℝ) :
    majorityAdv (2 * j + 3) x - majorityAdv (2 * j + 1) x
      = ((Nat.centralBinom (j + 1) : ℝ) / 4 ^ (j + 1)) * x * (1 - x ^ 2) ^ (j + 1) := 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