switch_strictly_better
plain-language theorem explainer
Switching strictly beats staying in the Monty Hall counting model on the nine-element sample space. Decision theorists and probability instructors cite the result when presenting the classic paradox resolution via explicit enumeration. The proof rewrites the target inequality to the pair of already-established rational equalities and dispatches it by numerical normalization.
Claim. On the uniform probability space over prize location and player pick in $Fin 3 times Fin 3$, the stay-win probability satisfies $p_{stay} < p_{switch}$, where each probability is the ratio of the cardinality of its winning set to the total number of outcomes.
background
The module constructs the Monty Hall problem as a finite uniform probability space with nine outcomes. The stay-winning set is the diagonal where the player's pick matches the prize location (cardinality 3), and the switch-winning set is the complementary off-diagonal (cardinality 6). The functions p_stay and p_switch are defined as the respective cardinalities divided by nine. Upstream theorems p_stay_eq and p_switch_eq establish the explicit values 1/3 and 2/3.
proof idea
The proof is a one-line wrapper that rewrites the inequality using the lemmas p_stay_eq and p_switch_eq, then applies norm_num to confirm 1/3 < 2/3.
why it matters
The theorem supplies the strict inequality needed to assemble the master certificate montyHallCert and to complete the single-statement summary monty_hall_one_statement. It realizes the counting form of the Monty Hall theorem described in the module documentation for Track E6. In the Recognition Science setting it provides a concrete instance of decision under uncertainty that can be connected to the Recognition Composition Law, although the direct link to the forcing chain T0-T8 is left for later development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.