p_switch_real
plain-language theorem explainer
p_switch_real casts the rational switch-win probability from the Monty Hall counting argument to the reals. Decision theorists working in the Recognition Science framework cite it when embedding discrete outcome counts into real arithmetic for comparisons. It is realized as a direct type coercion from the upstream p_switch definition.
Claim. $p_{switch,real} : ℝ := p_{switch}$, where $p_{switch}$ denotes the rational probability of winning by switching, obtained as the ratio of switch-winning outcomes to the total sample space size under the uniform measure.
background
The Monty Hall module constructs the sample space as pairs of prize location and initial pick over three doors, each assigned probability 1/9. Upstream p_switch is defined as switchWinningSet.card divided by the cardinality of all outcomes, which equals the rational 2/3. The module documentation states that stay wins exactly on the diagonal where pick equals prize, switch wins on the complementary off-diagonal, and the host's reveal does not redistribute probability but only enables the second choice.
proof idea
It is a one-line definition that coerces the rational value of p_switch into the real numbers.
why it matters
This definition supplies the real-valued switch probability required by the parent theorems p_switch_real_eq, which proves equality to 2/3, and switch_strictly_better_real, which establishes strict superiority over the stay probability. It completes the combinatorial derivation in the Decision module, linking the uniform counting argument to real analysis without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.