stayWinningSet_card
plain-language theorem explainer
The theorem establishes that the stay-winning set in the Monty Hall sample space has cardinality three. Decision theorists deriving probabilities from finite outcome counts would reference this result to ground the stay probability at one third. The proof proceeds by a direct decision tactic that enumerates the concrete finite set of outcomes.
Claim. Let $S$ be the subset of outcomes in $Fin 3 times Fin 3$ where the player's pick equals the prize location. Then the cardinality of $S$ equals 3.
background
The module constructs the Monty Hall problem on the joint sample space $Omega := Fin 3 times Fin 3$ of (prize location, player pick) equipped with the uniform measure. The stay-winning set is obtained by filtering the universal Finset over the predicate StayWins, which holds exactly on the diagonal where pick equals prize. The companion definition outcome_count supplies the total cardinality nine, so the stay probability follows immediately as three-ninths.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the concrete finite set, confirming that the filter over StayWins yields exactly three elements.
why it matters
This cardinality supplies the stay card to montyHallCert and to monty_hall_one_statement, which together establish the 1/3 versus 2/3 probabilities. It completes the counting step in the module's derivation of conditional probabilities, consistent with the Recognition Science emphasis on discrete outcome enumeration before invoking the phi-ladder or J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.