Prove2Me

Column parity bound

Proved
GameSetMatch.hypergeomWeight_odd_le

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd MM and even ii: MPr⁡(Li odd)≤M−1M\Pr(L_i\text{ odd})\le M-1 (the argument for equation (23)).

Preamble
import Definitions.Def_GameSetMatchInternal
Formal statement
namespace GameSetMatch

/-- Column parity: for even `i` and odd `M`, `M·Pr(L odd) ≤ M − 1`. -/
theorem hypergeomWeight_odd_le (M n i : ℕ) (hM : Odd M) (hi : i ≤ M * n) (hi2 : Even i) :
    (M : ℝ) * ∑ l ∈ (Finset.range (n + 1)).filter Odd, hypergeomWeight M n i l ≤ M - 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