p_switch
plain-language theorem explainer
The declaration defines the switch-win probability in the Monty Hall setup as the ratio of the cardinality of switchWinningSet to the total number of outcomes in the uniform sample space Fin 3 × Fin 3. Decision theorists and Recognition Science researchers working on explicit probability derivations cite it when establishing the classic 2/3 advantage for switching. It is a direct one-line cardinality ratio that feeds the master certificate and the equality theorem proving the value equals 2/3.
Claim. Let $S$ be the set of outcomes in the sample space $Fin 3 × Fin 3$ where the switch strategy wins. Then $p_{switch} := |S| / 9 ∈ ℚ$.
background
The module constructs the Monty Hall problem on the joint sample space $Ω = Fin 3 × Fin 3$ of prize location and initial player pick, each of the nine pairs carrying uniform weight 1/9. Outcome is the type alias for this space. switchWinningSet is the Finset of those pairs satisfying SwitchWins, i.e., the off-diagonal cases where pick ≠ prize.
proof idea
This is a one-line definition that directly computes the ratio of switchWinningSet.card to the cardinality of the full Finset of Outcome.
why it matters
It supplies the concrete switch probability that populates the MontyHallCert structure and appears inside the one-statement theorem monty_hall_one_statement. The downstream theorem p_switch_eq then proves the value equals 2/3 by unfolding the definition and invoking the cardinality facts stayWinningSet_card and outcome_count. In the Recognition Science framework this contributes to the Decision track (E6) by replacing an earlier placeholder assertion with an explicit counting derivation, feeding broader claims about strategy comparison under uniform measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.