not_both
plain-language theorem explainer
No outcome in the Monty Hall sample space satisfies both the stay-win and switch-win predicates simultaneously. This mutual-exclusion fact is cited by the master certificate that assembles the 1/3 and 2/3 probabilities via direct counting. The proof unfolds the two predicates and derives an immediate contradiction from their conjunction.
Claim. For every outcome $ω ∈ Fin 3 × Fin 3$, it is not the case that both the pick equals the prize and the pick differs from the prize.
background
The module constructs the Monty Hall sample space as the product $Fin 3 × Fin 3$, with the first coordinate the prize door and the second the player's initial pick. StayWins holds exactly on the diagonal where pick equals prize; SwitchWins holds on the complementary off-diagonal where they differ. The module states that these predicates partition the nine equiprobable outcomes, with the host's opening rule serving only to make the switch choice available.
proof idea
The term proof unfolds StayWins and SwitchWins, then applies rintro to the assumed conjunction. The resulting equality and inequality are contradictory, so the second hypothesis is applied directly to the first to close the goal.
why it matters
The lemma is invoked by montyHallCert, the master certificate that records the outcome counts and the derived probabilities 1/3 and 2/3. It supplies the complementarity step required by the counting argument in the module's derivation of classical decision probabilities. Within the Recognition Science framework it anchors the decision track (E6) to the underlying phi-ladder structure, though the link remains at the level of the finite sample space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.