p_switch
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not model any host strategy beyond always revealing a goat door.
- Does not treat non-uniform priors on prize location.
- Does not extend to variants with more than three doors.
- Does not incorporate player beliefs or Bayesian updating.
Lean usage
rw [p_switch] at hformal statement (Lean)
140def p_switch : ℚ := switchWinningSet.card / (Finset.univ : Finset Outcome).card
proof body
Definition body.
141
142/-- **STAY-WINS-WITH-PROBABILITY-1/3.** -/