switchWinningSet_card
plain-language theorem explainer
The theorem asserts that the switch-winning outcomes in the Monty Hall sample space number exactly six out of nine equally likely prize-and-pick pairs. Decision theorists and probability researchers working in the Recognition Science setting would cite this cardinality when deriving the two-thirds switch success rate from direct enumeration. The proof reduces to a single decision procedure that evaluates the finite set size by exhaustive computation.
Claim. Let the sample space consist of all pairs of prize location and initial pick, each ranging over three doors. Let $S$ be the subset of pairs in which the prize location differs from the initial pick. Then the cardinality of $S$ equals 6.
background
The module builds the Monty Hall problem on the finite sample space of prize locations and player picks, each drawn uniformly from three doors and yielding nine outcomes under the uniform measure. The switch-winning set is the collection of outcomes satisfying the switch-win condition, which coincides exactly with the off-diagonal pairs in the three-by-three grid. This replaces earlier placeholder probability labels with explicit counting, consistent with the Recognition Science approach of deriving decision probabilities from discrete uniform measures on finite sets.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to evaluate the cardinality equality on the finite filtered set.
why it matters
This cardinality supplies the switch-card value required by the master certificate and the one-statement Monty Hall theorem, which together establish the switch probability of two-thirds. It thereby completes the explicit counting argument for the classic result inside the Recognition Science decision track, aligning with the framework's use of discrete outcome sets without reference to the forcing chain or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.