`Compfiles/Usa1974P4.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

10 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1974, Problem 4

A, B, C play a series of games. Each game is between two players. The next game is between the winner and the person who was not playing. The series continues until one player has won two games. He wins the series. A is the weakest player, C the strongest. Each player has a fixed probability of winning against a given opponent. A chooses who plays the first game. Show that he should choose to play himself against B.

Imports (4)

Imported by 1 file

Compfiles.lean

inductive Usa1974P4.Player The three players of the series line 32 source

Source documentation

The three players of the series.

no axioms what this means

inductive Player | A | B | C
  deriving DecidableEq

/-- The player who sits out a game between `x` and `y`.
Only meaningful for `x ≠ y`; returns `A` on the diagonal. -/

def Usa1974P4.third The player who sits out a game between x and y line 37 source
Source documentation
The player who sits out a game between x and y. Only meaningful for x ≠ y; returns A on the diagonal.

standard axioms: propext what this means
Statement uses: Usa1974P4.Player
Proof uses: Usa1974P4.third.match_1, Unit, Usa1974P4.Player.C, Usa1974P4.Player.B, Usa1974P4.Player.A
```
def third : Player → Player → Player
  | .A, .B => .C
  | .B, .A => .C
  | .A, .C => .B
  | .C, .A => .B
  | .B, .C => .A
  | .C, .B => .A
  | _, _ => .A

/-- The probability that player `A` wins the series, where

* `win x y` is the probability that `x` beats `y` in a single game,
```
Mentions: Usa1974P4.Player
def Usa1974P4.probWinA Documented declaration: probWinA line 59 source
Source documentation
The probability that player A wins the series, where
- win x y is the probability that x beats y in a single game,
- the next game is played between w (the winner of the previous game) and i (the player who sat out the previous game); the loser of a game sits out the next one,
- hist is the list of winners of the games played so far, and
- n is a fuel bounding the number of games still to be played.
The series ends as soon as some player has won two games in total, so it lasts at most four games: if no one has won twice after three games then the three winners so far are three distinct players, and the fourth game is played between two of them, so its winner reaches two wins.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real, Nat, List
2 instances, coercions and auxiliary constants left out.
```
def probWinA (win : Player → Player → ℝ) :
    ℕ → Player → Player → List Player → ℝ
  | 0, _, _, _ => 0
  | n + 1, w, i, hist =>
      win w i * (if w ∈ hist then (if w = .A then 1 else 0)
                 else probWinA win n w (third w i) (w :: hist)) +
      win i w * (if i ∈ hist then (if i = .A then 1 else 0)
                 else probWinA win n i (third w i) (i :: hist))

/-- The probability that A wins the series when the first game is A against B. -/
```
Mentions: Usa1974P4.Player, Usa1974P4.third
def Usa1974P4.probFirstAB The probability that A wins the series when the first game is A against B line 69 source
Source documentation
The probability that A wins the series when the first game is A against B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real
Proof uses: Usa1974P4.probWinA, OfNat.ofNat, Nat, Usa1974P4.Player.A, Usa1974P4.Player.B, List.nil
1 instances, coercions and auxiliary constants left out.
```
def probFirstAB (win : Player → Player → ℝ) : ℝ := probWinA win 4 .A .B []
```
Mentions: Usa1974P4.Player, Usa1974P4.probWinA
def Usa1974P4.probFirstAC The probability that A wins the series when the first game is A against C line 72 source
Source documentation
The probability that A wins the series when the first game is A against C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real
Proof uses: Usa1974P4.probWinA, OfNat.ofNat, Nat, Usa1974P4.Player.A, Usa1974P4.Player.C, List.nil
1 instances, coercions and auxiliary constants left out.
```
def probFirstAC (win : Player → Player → ℝ) : ℝ := probWinA win 4 .A .C []
```
Mentions: Usa1974P4.Player, Usa1974P4.probWinA
def Usa1974P4.probFirstBC The probability that A wins the series when the first game is B against C line 75 source
Source documentation
The probability that A wins the series when the first game is B against C.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real
Proof uses: Usa1974P4.probWinA, OfNat.ofNat, Nat, Usa1974P4.Player.B, Usa1974P4.Player.C, List.nil
1 instances, coercions and auxiliary constants left out.
```
def probFirstBC (win : Player → Player → ℝ) : ℝ := probWinA win 4 .B .C []
…
```
Mentions: Usa1974P4.Player, Usa1974P4.probWinA
lemma Usa1974P4.probFirstAB_eq Documented declaration: probFirstAB_eq line 82 source
Source documentation
Expanding the game tree when the first game is A against B: writing XbY for "X beats Y", A wins the series exactly via the outcome sequences AbB · AbC, AbB · CbA · BbC · AbB, and BbA · CbB · AbC · AbB.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real, Eq, Usa1974P4.Player.B, Usa1974P4.Player.A, HSub.hSub, OfNat.ofNat, Usa1974P4.Player.C, Usa1974P4.probFirstAB, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, congr, ite, Membership.mem, List, List.nil, Usa1974P4.probWinA, Usa1974P4.third, List.cons, Eq.trans, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true, Or, True, False, eq_self, or_false and 62 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma probFirstAB_eq (win : Player → Player → ℝ)
    (hBA : win .B .A = 1 - win .A .B) (hCA : win .C .A = 1 - win .A .C)
    (hCB : win .C .B = 1 - win .B .C) :
    probFirstAB win =
      win .A .B * win .A .C + win .A .B * (1 - win .A .C) * win .B .C * win .A .B +
        (1 - win .A .B) * (1 - win .B .C) * win .A .C * win .A .B := by
…
```
Mentions: Usa1974P4.Player, Usa1974P4.probFirstAB
lemma Usa1974P4.probFirstAC_eq Expanding the game tree when the first game is A against C: A wins the series exactly via the outcome sequences AbC · AbB, AbC · BbA · CbB · AbC, and CbA · BbC · AbB · AbC line 94 source
Source documentation
Expanding the game tree when the first game is A against C: A wins the series exactly via the outcome sequences AbC · AbB, AbC · BbA · CbB · AbC, and CbA · BbC · AbB · AbC.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real, Eq, Usa1974P4.Player.B, Usa1974P4.Player.A, HSub.hSub, OfNat.ofNat, Usa1974P4.Player.C, Usa1974P4.probFirstAC, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, congr, ite, Membership.mem, List, List.nil, Usa1974P4.probWinA, Usa1974P4.third, List.cons, Eq.trans, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true, Or, True, False, eq_self, or_false and 60 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma probFirstAC_eq (win : Player → Player → ℝ)
    (hBA : win .B .A = 1 - win .A .B) (hCA : win .C .A = 1 - win .A .C)
    (hCB : win .C .B = 1 - win .B .C) :
    probFirstAC win =
      win .A .C * win .A .B + win .A .C * (1 - win .A .B) * (1 - win .B .C) * win .A .C +
        (1 - win .A .C) * win .B .C * win .A .B * win .A .C := by
…
```
Mentions: Usa1974P4.Player, Usa1974P4.probFirstAC
lemma Usa1974P4.probFirstBC_eq Expanding the game tree when the first game is B against C: A wins the series exactly via the outcome sequences BbC · AbB · AbC and CbB · AbC · AbB line 105 source
Source documentation
Expanding the game tree when the first game is B against C: A wins the series exactly via the outcome sequences BbC · AbB · AbC and CbB · AbC · AbB.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real, Eq, Usa1974P4.Player.B, Usa1974P4.Player.A, HSub.hSub, OfNat.ofNat, Usa1974P4.Player.C, Usa1974P4.probFirstBC, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, id, congrFun', congrArg, congr, ite, Membership.mem, List, List.nil, Usa1974P4.probWinA, Usa1974P4.third, List.cons, Eq.trans, ite_eq_right_of_eq_false, ite_eq_left_of_eq_true, Or, True, False, eq_self, or_false and 57 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma probFirstBC_eq (win : Player → Player → ℝ)
    (hBA : win .B .A = 1 - win .A .B) (hCA : win .C .A = 1 - win .A .C)
    (hCB : win .C .B = 1 - win .B .C) :
    probFirstBC win =
      win .B .C * win .A .B * win .A .C + (1 - win .B .C) * win .A .C * win .A .B := by
…
```
Mentions: Usa1974P4.Player, Usa1974P4.probFirstBC
problem Usa1974P4.usa1974_p4 line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa1974P4.Player, Real, Ne, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd, Usa1974P4.Player.A, Usa1974P4.Player.C, Usa1974P4.Player.B, Usa1974P4.probFirstBC, Usa1974P4.probFirstAB, Usa1974P4.probFirstAC
Proof uses: HSub.hSub, And.right, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring and 67 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.