p_stay_real
plain-language theorem explainer
This definition embeds the stay-win probability, obtained by counting three favorable outcomes out of nine in the Monty Hall sample space, into the real numbers. Decision theorists working within Recognition Science would cite it when establishing the baseline for comparing stay versus switch strategies. It is implemented as a direct type coercion from the rational value defined by set cardinality.
Claim. Let $p_{stay}$ be the rational probability of winning by staying, defined as the cardinality of the stay-winning set divided by the total number of outcomes under the uniform measure on $Fin 3 times Fin 3$. Then $p_{stay, real}$ is the image of this value in the real numbers.
background
The module constructs the Monty Hall sample space as pairs of prize location and player pick, each ranging over three doors, with uniform measure assigning weight 1/9 to each of nine outcomes. The stay-winning set consists of the three diagonal cases where pick equals prize. The sibling definition p_stay computes the probability as this cardinality divided by nine, yielding the rational 1/3. The current declaration casts that rational to type ℝ. Upstream results supply the general pattern of probability as a non-negative real: the Born-rule form in QuantumLedger, the transition amplitude squared in SMatrixUnitarity, and the normalized Boltzmann factor in BoltzmannDistribution.
proof idea
This declaration is a one-line wrapper that coerces the rational p_stay to type ℝ.
why it matters
It supplies the real-valued stay probability required by the equality theorem p_stay_real_eq, which proves the value equals 1/3, and by the comparison theorem switch_strictly_better_real establishing that switching is strictly superior. This completes the explicit derivation of the Monty Hall probabilities by outcome enumeration in the Decision module, aligning with the Recognition Science approach of building probabilities from finite sample spaces. The module positions the result as part of track E6 for conditional-probability theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.