switchWinningSet
plain-language theorem explainer
The declaration defines the Finset of outcomes in the Monty Hall sample space where switching wins. Decision theorists and Recognition Science researchers cite it when deriving the 2/3 switch probability from uniform counting on nine joint outcomes. The definition is a direct filter of the full outcome universe by the predicate that the initial pick differs from the prize location.
Claim. Let $S = Finset.univ.filter (fun ω => SwitchWins ω)$ where $Ω = Fin 3 × Fin 3$ is the sample space of (prize location, player pick) and $SwitchWins(ω)$ holds precisely when the second component of $ω$ differs from the first.
background
The module models the Monty Hall problem on the joint sample space $Ω = Fin 3 × Fin 3$ of prize location and initial player pick, each chosen uniformly. Outcome is the abbrev for this product type, giving nine equally likely points. SwitchWins is the predicate $ω.2 ≠ ω.1$, which marks the six off-diagonal outcomes where switching reaches the prize after the host reveals a goat.
proof idea
This is a one-line definition that applies Finset.univ.filter to the complete set of nine outcomes using the decidable predicate SwitchWins.
why it matters
switchWinningSet supplies the cardinality-6 set required by MontyHallCert and monty_hall_one_statement to establish $p_switch = 2/3$. It completes the classical counting argument that stay and switch probabilities are complementary on the uniform measure, feeding the Recognition Science derivation of decision probabilities without invoking conditional redistribution by the host.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.