Outcome
plain-language theorem explainer
The Outcome abbreviation sets the sample space for the Monty Hall problem as the Cartesian product of prize location and initial player choice, each ranging over three doors. Decision theorists and probability researchers cite this type when deriving stay and switch probabilities by direct enumeration of the nine outcomes. The definition is introduced as a direct type abbreviation that supplies the uniform measure domain for all subsequent counting lemmas in the module.
Claim. Let $Ω$ be the sample space of joint outcomes consisting of the prize door and the player's initial pick, where each component ranges over the set of three doors.
background
The Monty Hall module constructs a probability model with three doors. The prize is placed uniformly at random behind one door and the player selects a door uniformly at random. Their joint outcome is recorded as a pair in the product space Fin 3 × Fin 3, which contains exactly nine elements under the uniform measure. The module doc states that stay wins precisely when the pair lies on the diagonal and switch wins on the off-diagonal. Upstream results supply the Outcome type from BellInequality as a measurement label and the has class from AsteroidOreSpectroscopy for spectral classification, but the present abbreviation is self-contained for the counting argument.
proof idea
The declaration is a direct type abbreviation that equates Outcome to the product Fin 3 × Fin 3. No tactics or lemmas are applied; the abbreviation simply names the nine-element set that later theorems such as outcome_count and stay_or_switch enumerate by cardinality.
why it matters
Outcome supplies the domain for the MontyHallCert structure, which records the cardinalities 9, 3 and 6 together with the explicit values p_stay = 1/3 and p_switch = 2/3. The definition therefore replaces the earlier placeholder probabilities with an explicit counting derivation on the finite sample space. It advances the decision-theory track by grounding the classic 2/3 result in the same outcome-counting style used elsewhere in Recognition Science for discrete probability spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.