switch_strictly_better_real
plain-language theorem explainer
The declaration proves that the real probability of winning the Monty Hall game by staying with the initial choice is strictly smaller than the probability obtained by switching doors. Probability theorists and decision analysts would reference it when deriving the classic 1/3 versus 2/3 result from explicit outcome enumeration on a nine-element sample space. The proof reduces the claim to a numerical comparison by substituting the pre-established equalities for each probability.
Claim. Let $p_mathrm{stay}$ be the real probability of winning by staying and $p_mathrm{switch}$ the real probability of winning by switching, both obtained from the uniform measure on the sample space of prize location and initial pick. Then $p_mathrm{stay} < p_mathrm{switch}$.
background
The Monty Hall module constructs the sample space as pairs of prize location and player pick, each ranging over three doors. The stay-winning set consists of the three outcomes where pick matches prize; the switch-winning set comprises the remaining six. The probabilities are obtained by dividing the cardinalities by nine, yielding the rational values one-third and two-thirds before casting to reals.
proof idea
The proof applies the rewriting tactic to replace p_stay_real and p_switch_real by their respective equality theorems, which reduce them to the constants 1/3 and 2/3. The subsequent norm_num tactic then discharges the resulting numerical inequality 1/3 < 2/3.
why it matters
This theorem completes the master certificate for the Monty Hall problem by establishing the strict inequality between the two strategies. It sits downstream from the cardinality lemmas that count the diagonal and off-diagonal outcomes in the nine-element space. Within the Recognition Science framework it supplies a concrete instance of conditional probability derived from outcome enumeration, consistent with the emphasis on explicit counting before numerical evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.