switchWinningSet_card
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not model the host's specific choice of which goat door to open.
- Does not extend to non-uniform distributions over prize or pick.
- Does not generalize the counting argument to more than three doors.
- Does not derive the result from the J-function or phi-ladder.
Lean usage
rw [switchWinningSet_card]formal statement (Lean)
130theorem switchWinningSet_card : switchWinningSet.card = 6 := by
proof body
Decided by rfl or decide.
131 decide
132
133/-! ## §4. Probabilities under the uniform measure -/
134
135/-- The probability of a stay-win under the uniform measure on
136`Fin 3 × Fin 3`. -/