monty_hall_one_statement
plain-language theorem explainer
Decision theorists cite the Monty Hall one-statement theorem for the exact probabilities derived from the uniform measure on the nine-element sample space of prize location and initial choice. The result asserts that the stay-winning set has cardinality three while the switch-winning set has cardinality six, so the stay probability equals one third, the switch probability equals two thirds, the inequality holds, and the switch probability is exactly twice the stay probability. The proof assembles these facts in a single term-mode conjunction of
Claim. Let $Ω = Fin 3 × Fin 3$ be the sample space of (prize location, initial pick) pairs with the uniform measure. Let $S$ be the set of outcomes where the stay strategy wins (prize equals pick) and $W$ the set where the switch strategy wins (prize differs from pick). Then $|S| = 3$, $|W| = 6$, the stay-win probability equals $1/3$, the switch-win probability equals $2/3$, the stay probability is strictly less than the switch probability, and the switch probability equals twice the stay probability.
background
The module builds the Monty Hall problem as a counting exercise on the finite sample space $Ω = Fin 3 × Fin 3$. Each pair (prize, pick) receives equal weight $1/9$ under the uniform measure. The stay-winning set is the diagonal where prize equals pick; the switch-winning set is the complementary off-diagonal. The host always reveals a goat, leaving the prize behind one of the two remaining doors, but this action does not redistribute the win sets.
proof idea
The proof is a term-mode conjunction that packages six already-proved facts: the cardinality of the stay-winning set, the cardinality of the switch-winning set, the equality for p_stay, the equality for p_switch, the strict inequality between them, and the doubling relation. No additional tactics are required beyond the tuple constructor.
why it matters
This declaration supplies the compact summary statement for the Monty Hall result in the decision module. It collects the counting argument that replaces the earlier placeholder definitions of the probabilities. Within the Recognition Science framework the example illustrates how conditional choice under uniform measure yields a factor-of-two advantage for the informed strategy, consistent with the broader emphasis on information and cost in decision processes. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.