p_stay_eq
plain-language theorem explainer
Establishes that the stay strategy wins the Monty Hall game with probability exactly one third under the uniform measure on the nine-element sample space of prize and pick pairs. Decision theorists and probability instructors cite it when deriving the baseline for the switching advantage from counting arguments. The proof is a direct algebraic reduction that unfolds the probability definition and substitutes the precomputed cardinalities of the stay-winning set and the full outcome space.
Claim. The stay-win probability equals $1/3$, where this probability is the ratio of the cardinality of outcomes in which the initial pick matches the prize location to the total number of outcomes in the sample space $Fin 3 times Fin 3$.
background
The module constructs the Monty Hall problem on the finite sample space of all pairs (prize door, player pick) with each ranging over three doors. The stay-winning outcomes are those where the pick equals the prize; the upstream outcome_count theorem states that the full sample space $Fin 3 times Fin 3$ has 9 outcomes. The stay probability is defined as the cardinality of the stay-winning set divided by the total outcome cardinality.
proof idea
The term-mode proof unfolds the definition of the stay probability, rewrites using the stayWinningSet_card theorem (which gives cardinality 3) and the outcome_count theorem (which gives total cardinality 9), then applies norm_num to reduce the resulting fraction to 1/3.
why it matters
This equality supplies the p_stay_value field inside the master montyHallCert certificate and is invoked directly by monty_hall_one_statement, switch_strictly_better, switch_eq_two_stay, total_probability, and p_stay_real_eq. It completes the counting derivation of the classic 1/3 versus 2/3 result in the Decision track, showing that the switching advantage follows from uniform measure on a product space without reference to J-uniqueness or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.