outcome_count
plain-language theorem explainer
The declaration establishes that the joint sample space of prize locations and initial picks over three doors contains exactly nine outcomes. Decision theorists deriving the Monty Hall probabilities from explicit enumeration would cite it as the base counting step. The proof is a one-line term that reduces the cardinality of the product Finset to the product of the individual cardinalities via simplification.
Claim. Let $Omega$ be the set of all pairs $(prize, pick)$ with both ranging over the three doors. Then $|Omega| = 9$.
background
Outcome is defined as the product type Fin 3 × Fin 3, representing the joint choice of prize door and player's initial pick. The module models the classic Monty Hall setup with three doors, uniform random prize placement, uniform random initial pick, and a host who always opens a goat door; the stay strategy wins precisely on the diagonal pairs while the switch strategy wins on the six off-diagonal pairs. The upstream Outcome definition supplies this product type directly; the unrelated BellInequality Outcome concerns measurement values +1 or -1 and is not used here.
proof idea
The proof is a one-line term proof that applies simp to Finset.card_univ and Fintype.card_prod. These lemmas equate the cardinality of the universal Finset over a Fintype to the Fintype cardinality and equate the cardinality of a product type to the product of its factors; with Outcome equal to Fin 3 × Fin 3 the product 3 × 3 yields 9.
why it matters
This supplies the first clause of the MontyHallCert structure, which is then used to derive p_stay = 1/3 and p_switch = 2/3 via the stayWinningSet_card and switchWinningSet_card lemmas. It replaces the earlier placeholder module that asserted the probabilities without derivation. Within Recognition Science the construction shows how a classical decision problem reduces to finite outcome counting whose arithmetic is compatible with the phi-ladder and eight-tick octave, though the module's connection note leaves the precise embedding open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.