SwitchWins
plain-language theorem explainer
SwitchWins is the predicate on pairs in the Fin 3 by Fin 3 sample space that holds exactly when the player's pick differs from the prize location. Decision theorists and Recognition Science researchers cite it when partitioning outcomes to recover the 2/3 switch probability by direct cardinality. The definition is a single inequality on the pair components, with decidability obtained by unfolding and applying the standard instance for finite equality.
Claim. Let $Ω = Fin 3 × Fin 3$ be the sample space with first component the prize door and second component the player's pick. For $ω = (p, q) ∈ Ω$, the predicate SwitchWins($ω$) holds if and only if $q ≠ p$.
background
The Monty Hall module constructs the classic problem on the uniform measure over nine outcomes in Fin 3 × Fin 3. Outcome is the product type pairing prize location with initial pick. StayWins holds on the diagonal where pick equals prize; SwitchWins holds on the complementary off-diagonal. The host always opens a non-prize, non-pick door, leaving the switch choice well-defined but not altering the win sets themselves. Upstream structures supply J-cost convexity and spectral emergence of three generations, yet the local counting argument uses only finite-set cardinality on this discrete space.
proof idea
The declaration is a direct definition of the component inequality ω.2 ≠ ω.1. The accompanying Decidable instance unfolds the definition and invokes the standard decidable inequality instance on Fin 3.
why it matters
SwitchWins supplies the off-diagonal predicate required by MontyHallCert to record switchWinningSet.card = 6 and derive p_switch = 2/3. It completes the explicit counting derivation in track E6, replacing earlier placeholder probabilities with outcome enumeration on the three-door space. The construction aligns with the framework's emphasis on discrete finite structures consistent with D = 3 and the eight-tick octave, while remaining independent of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.