MontyHallCert
plain-language theorem explainer
MontyHallCert packages the numerical facts of the Monty Hall problem obtained by counting outcomes in the joint sample space of prize location and initial pick. A decision theorist or probability researcher would cite it when formalizing the classic paradox from explicit enumeration rather than presupposed fractions. The structure records cardinalities of the diagonal and off-diagonal subsets of Fin 3 times Fin 3 together with the induced uniform probabilities and their ordering.
Claim. Let $Ω = Fin 3 × Fin 3$. Let $S$ be the set of outcomes where the player's pick equals the prize location and $W$ the complementary set where they differ. Then $|Ω| = 9$, $|S| = 3$, $|W| = 6$, the stay probability equals $1/3$, the switch probability equals $2/3$, the stay probability is strictly less than the switch probability, their sum is 1, the switch probability is twice the stay probability, and every outcome lies in exactly one of $S$ or $W$.
background
The module treats the Monty Hall problem on the sample space $Ω := Fin 3 × Fin 3$, with the first coordinate the prize door and the second the player's initial choice, each drawn uniformly. Outcome is the type alias for this product. StayWins holds precisely when the pick equals the prize, forming the diagonal subset; SwitchWins holds on the off-diagonal complement. The upstream outcome_count theorem shows that the full space has cardinality 9 via Fintype.card_prod. The probabilities p_stay and p_switch are defined directly as the respective subset cardinalities divided by the space cardinality.
proof idea
The declaration is a structure definition whose fields record the listed cardinalities and derived equalities. No proof body is present; the fields are discharged downstream in montyHallCert by direct substitution of the lemmas outcome_count, stayWinningSet_card, switchWinningSet_card, p_stay_eq and p_switch_eq.
why it matters
This structure supplies the master certificate for the Monty Hall derivation in the Decision track. It is instantiated by montyHallCert and provides the explicit counting argument that switching wins with probability 2/3. The result supports the framework's preference for deriving probabilities from finite outcome enumeration rather than axiomatic labels, consistent with uniform measures used in the Cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.