Lemma 3: tie probability when r ≤ 1/2

Proved

GameSetMatch.tieProb_nested_lt

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd $M>1$ , $n\ge1$ , $0<x\le1$ , $0<r\le1/2$ : $Z_{nM}(r,x)<Z_n(r,H_M(x))$ (equation (27)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- **Lemma 3.** For odd `M > 1`, `n ≥ 1`, `0 < x < 1`... (`x ≤ 1` admitted), `0 < r ≤ 1/2`:
`Z_{nM}(r, x) < Z_n(r, H_M(x))`. -/
theorem tieProb_nested_lt (r x : ℝ) (M n : ℕ) (hM : Odd M) (hM1 : 1 < M) (hn : 1 ≤ n)
    (hr0 : 0 < r) (hr : r ≤ 1 / 2) (hx0 : 0 < x) (hx1 : x ≤ 1) :
    tieProb (scoreContribLaw r x) (n * M) < tieProb (scoreContribLaw r (majorityAdv M x)) n := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md, Section 5 (Lemma 3); independent_case_full_proof.md, Section 5

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