A scored set is a score contribution

Proved

GameSetMatch.scoredSetLaw_eq_scoreContribLaw

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

label-aggregationmajority-voteprobabilityrandom-walktennis

If $a+b+c=1$ and $a+c>0$ , the law of one scored set with win probability $q$ equals the score-contribution law with $r=a+c$ and advantage $\lambda(2q-1)$ , $\lambda=(a-c)/(a+c)$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- A scored set is a score contribution with `r = a + c` and advantage `λ(2q − 1)`,
`λ = (a − c)/(a + c)`. -/
theorem scoredSetLaw_eq_scoreContribLaw (a b c q : ℝ) (habc : a + b + c = 1) (hac : 0 < a + c) :
    scoredSetLaw a b c q = scoreContribLaw (a + c) ((a - c) / (a + c) * (2 * q - 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