stay_or_switch
plain-language theorem explainer
Every outcome in the Monty Hall sample space satisfies either the stay-win condition or the switch-win condition. Probability theorists modeling the classic problem would cite this result to establish the complementarity of the two strategies before computing their respective probabilities of 1/3 and 2/3. The proof is a direct case split on whether the player's pick matches the prize location.
Claim. For every outcome $ω$ in the sample space $Fin 3 × Fin 3$, either the stay strategy wins ($ω_2 = ω_1$) or the switch strategy wins ($ω_2 ≠ ω_1$).
background
The module models the Monty Hall problem with sample space $Ω = Fin 3 × Fin 3$, prize and pick each uniform over three doors. StayWins holds exactly when pick equals prize (diagonal cases). SwitchWins holds when they differ (off-diagonal cases), since the host always leaves the prize as the remaining unopened door.
proof idea
The proof unfolds the definitions of StayWins and SwitchWins, then performs case analysis on equality of the pair components. The matching case returns the left disjunct; the non-matching case returns the right disjunct.
why it matters
This result supplies the exhaustive partition required by the downstream montyHallCert certificate, which assembles cardinalities and probabilities. It completes the classical derivation of the switch advantage in the Decision track, confirming the two strategies partition the sample space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.