StayWins
plain-language theorem explainer
Stay-winning outcomes are those where the player's initial pick matches the prize location in the three-door sample space. Researchers deriving conditional probabilities in decision theory cite this predicate to separate the diagonal events from the off-diagonal ones. The definition consists of a direct equality between the two components of each outcome pair.
Claim. For an outcome pair consisting of prize location and initial pick, each ranging over a three-element set, the stay-winning predicate holds exactly when the pick equals the prize.
background
The Monty Hall module constructs the sample space as the Cartesian product of two copies of the three-element set, one for prize location and one for the player's initial pick. This produces nine equiprobable outcomes. The joint outcome type is defined as this product, with the stay-winning predicate marking the three diagonal pairs where the components coincide.
proof idea
The declaration is introduced by direct definition as equality of the second and first components of the outcome pair. The accompanying decidability instance follows immediately from decidable equality on the finite set.
why it matters
This predicate populates the stay-winning set used in the Monty Hall master certificate, which records cardinalities three and six for the stay and switch events and derives the probabilities one-third and two-thirds. It is invoked to prove that the two strategies partition the sample space and that no outcome satisfies both conditions simultaneously. The construction replaces an earlier placeholder derivation with explicit counting, consistent with the Recognition Science emphasis on discrete enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.