p_switch_real_eq
plain-language theorem explainer
The equality establishes that the real-valued switch-win probability equals exactly two thirds in the three-door Monty Hall model. Decision theorists or probability modelers working inside Recognition Science would cite it to anchor the classic counting result before comparing strategies. The proof is a one-line wrapper that unfolds the cast definition, rewrites via the already-proved rational-probability lemma, and simplifies the arithmetic.
Claim. Let $p$ denote the switch-win probability obtained by counting outcomes in the uniform sample space of prize and pick locations. Then the embedding of $p$ into the reals satisfies $p = 2/3$.
background
The module builds the Monty Hall sample space as all pairs of prize door and player pick, each chosen uniformly from three doors. Stay wins on the three diagonal outcomes while switch wins on the six off-diagonal outcomes, so the rational probabilities are one third and two thirds by direct cardinality. The upstream lemma p_switch_eq proves the rational equality by rewriting to the cardinality of the switch-winning set and normalizing the total count of nine outcomes. The definition p_switch_real simply casts that rational into the reals to enable direct comparison with other real quantities such as the stay probability.
proof idea
The term proof unfolds the definition of the real-valued switch probability, rewrites the body using the upstream equality p_switch_eq, pushes the natural-number cast through the division operator, and finishes with the ring tactic to obtain the arithmetic identity.
why it matters
This supplies the real form required by the downstream theorem switch_strictly_better_real, which concludes that the stay probability is strictly less than the switch probability. It completes the derivation of the classic two-thirds result inside the Recognition Science decision module (track E6), confirming that the framework's uniform counting on the nine-outcome space reproduces the standard Monty Hall conclusion without additional conditional-probability machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.