montyHallCert
plain-language theorem explainer
The master certificate for the Monty Hall problem is defined by assembling the outcome count, set cardinalities, and probability identities already established by counting on the joint sample space of prize location and player choice. A decision theorist would cite this to access the 1/3 versus 2/3 probabilities and the strict superiority of switching. The construction is a direct structure literal that references the pre-proved lemmas for each field.
Claim. The master certificate $C$ satisfies: the sample space has cardinality 9, the stay-winning outcomes have cardinality 3, the switch-winning outcomes have cardinality 6, the stay probability equals $1/3$, the switch probability equals $2/3$, the stay probability is strictly less than the switch probability, their sum is 1, the switch probability is twice the stay probability, every outcome is either a stay win or a switch win, and no outcome is both.
background
The module models the Monty Hall problem on the finite sample space consisting of all pairs of prize location and initial player choice, each drawn uniformly from three doors. For any pair the stay strategy wins exactly when the doors match and the switch strategy wins exactly when they differ; these classes are complementary and disjoint. The host's opening choice does not enter the win-probability calculation: the host always reveals a goat regardless of whether the player stays or switches.
proof idea
This is a definition that constructs the certificate record by direct assignment of each field to a sibling theorem or definition. The assignments delegate outcome count to the theorem proving nine outcomes via Finset.card_univ and Fintype.card_prod, stay and switch cards to the cardinality lemmas, probabilities to the equality theorems obtained by dividing the cards, and the remaining relations to the complementarity and strict inequality lemmas.
why it matters
The declaration completes the derivation of the classic 1/3 versus 2/3 result within the decision module. It supplies the concrete object that a user of the framework can invoke to obtain the probabilities without repeating the counting arguments. In the Recognition Science setting this serves as an illustration of how discrete enumeration replaces continuous probability measures for simple decision problems. The absence of downstream references indicates it functions as a terminal example rather than an intermediate lemma in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.