switch_eq_two_stay
plain-language theorem explainer
The switch probability equals twice the stay probability under the uniform measure on the joint sample space of prize location and player pick. Decision theorists and instructors of elementary probability would cite this when establishing the classic 2/3 versus 1/3 advantage. The proof is a one-line algebraic reduction that substitutes the already-proved numerical values for each probability and normalizes.
Claim. $p_ {switch} = 2 p_ {stay}$ where $p_ {stay}$ is the probability of winning by staying and $p_ {switch}$ is the probability of winning by switching, both computed as cardinality ratios over the nine equally likely outcomes in the sample space of prize and pick locations.
background
The Monty Hall module builds the sample space as the Cartesian product of two copies of Fin 3, one for prize location and one for the player's initial pick, equipped with the uniform counting measure. Stay-winning outcomes are the three diagonal pairs where pick equals prize; switch-winning outcomes are the six off-diagonal pairs. The probability definitions are therefore the ratios of these cardinalities to the total of nine outcomes. Upstream results p_stay_eq and p_switch_eq already establish the concrete values 1/3 and 2/3 by direct application of the cardinality lemmas stayWinningSet_card, switchWinningSet_card and outcome_count.
proof idea
The proof is a one-line wrapper that rewrites the goal using p_stay_eq and p_switch_eq, then invokes norm_num to verify the arithmetic identity 2/3 = 2 * (1/3).
why it matters
The equality is used directly by montyHallCert (the master certificate) and monty_hall_one_statement (the consolidated one-statement theorem). It supplies the final numerical relation needed to certify the Monty Hall result inside the Decision track, where probability is realized by uniform counting as in the QuantumLedger and BoltzmannDistribution modules. The declaration therefore closes the elementary derivation without invoking the phi-ladder, J-cost or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.