p_stay_real_eq
plain-language theorem explainer
The theorem establishes that the real-valued stay-win probability equals one third in the three-door Monty Hall sample space. Decision theorists and probability modelers cite it when deriving the baseline 1/3 versus 2/3 split from explicit outcome counting. The proof is a short tactic sequence that unfolds the real cast, rewrites via the integer probability equality, pushes the cast, and closes with ring simplification.
Claim. Let $p$ denote the stay-win probability on the uniform sample space of prize locations and player picks. Then the real-valued version satisfies $p = 1/3$.
background
The Monty Hall module defines the sample space as pairs of prize location and player pick, each ranging over Fin 3, yielding nine equally likely outcomes. The stay-winning set is the diagonal where prize equals pick (cardinality 3), so the rational probability p_stay is defined as that cardinality divided by the total outcome count of 9. The auxiliary definition p_stay_real simply casts this rational value into the reals.
proof idea
The proof unfolds p_stay_real to expose the cast of p_stay, rewrites the left-hand side using the upstream theorem p_stay_eq that already establishes the rational equality, applies push_cast to move the cast inside the division, and finishes with ring to obtain the identity 3/9 = 1/3 inside the reals.
why it matters
This equality supplies the numerical value required by the downstream theorem switch_strictly_better_real, which combines it with the corresponding switch probability to obtain the strict inequality 1/3 < 2/3. Inside the Recognition Science program the result illustrates how a finite counting argument yields the classic decision outcome without conditional-probability updates, thereby furnishing a concrete formalized example within the Decision track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.