switchWinningSet
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not encode the host's specific choice rule beyond guaranteeing a goat is shown.
- Does not allow non-uniform priors on prize location.
- Does not generalize to $n > 3$ doors.
- Does not incorporate quantum or relativistic structure.
formal statement (Lean)
104def switchWinningSet : Finset Outcome :=
proof body
Definition body.
105 Finset.univ.filter (fun ω => SwitchWins ω)
106
107/-! ## §2. The two outcome sets are complementary -/
108
109/-- Every outcome either wins by staying or wins by switching. -/