p_switch_eq
plain-language theorem explainer
Switching wins with probability exactly 2/3 under the uniform measure on the nine-element sample space of prize locations and initial picks. Decision theorists working in the Recognition Science decision track would cite this as the derived counting value for the switch strategy. The proof is a short term reduction that unfolds the probability definition, substitutes the precomputed cardinalities of the switch-winning set and total outcomes, and normalizes the resulting fraction.
Claim. Under the uniform probability measure on the sample space of prize locations and player picks, the probability that the switch strategy wins is exactly $2/3$.
background
The module constructs the Monty Hall sample space as the product Fin 3 × Fin 3, with the uniform measure placing weight 1/9 on each of the nine outcomes. The switch-winning set consists of the six off-diagonal pairs where the initial pick differs from the prize location. The definition of p_switch is the ratio of the cardinality of this set to the total number of outcomes.
proof idea
The proof unfolds the definition of p_switch, rewrites using the theorems switchWinningSet_card and outcome_count to replace the expression with 6/9, and applies norm_num to obtain 2/3.
why it matters
This supplies the exact switch probability inserted into the master certificate montyHallCert and the one-statement theorem monty_hall_one_statement. It completes the explicit counting derivation that replaces the earlier placeholder probabilities in the decision module. The result shows that the host's opening rule does not redistribute probability between the stay and switch strategies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.