p_stay
plain-language theorem explainer
p_stay defines the stay-win probability as the ratio of stay-winning outcomes to the total number of outcomes in the prize-and-pick sample space. A researcher formalizing decision problems in Recognition Science would cite this when establishing baseline probabilities for the Monty Hall setup. The definition is a direct cardinality quotient with no additional lemmas required.
Claim. Let $Ω = Fin 3 × Fin 3$ be the sample space of prize location and initial player pick. Let $S$ be the subset of outcomes where the initial pick matches the prize. Then the stay-win probability equals the cardinality of $S$ divided by the cardinality of $Ω$.
background
The Monty Hall module constructs the sample space as the product type Outcome := Fin 3 × Fin 3, which contains nine equally likely pairs. The stay-winning set collects those pairs in which the pick equals the prize location. Module documentation notes that this replaces a prior placeholder definition and derives the classic probabilities by counting three stay wins against six switch wins on the nine-element space. Upstream results include the general probability construction from the quantum ledger and ledger factorization structures, which supply the uniform measure convention used here.
proof idea
The definition directly forms the quotient of the cardinality of the stay-winning set by the cardinality of the full outcome space. It is a pure definitional abbreviation requiring no lemmas or tactics.
why it matters
This supplies the concrete value packaged into the master certificate structure and invoked by the one-statement theorem establishing the 1/3 and 2/3 probabilities. It places the Monty Hall result inside the Recognition Science decision track by grounding it in explicit outcome counting on a finite discrete space. The construction aligns with the uniform measure and connects to the broader forcing chain through imported ledger and phi structures, while leaving open the full integration with J-cost accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.