total_probability
The theorem establishes that stay and switch winning probabilities partition the sample space under the uniform measure on prize-pick pairs. Decision theorists and probability instructors would cite it when confirming the Monty Hall strategies are exhaustive and complementary. The proof is a one-line wrapper that substitutes the explicit values 1/3 and 2/3 then normalizes the arithmetic.
claimLet $p_ {stay}$ be the probability of winning by staying and $p_{switch}$ the probability of winning by switching, each defined as the cardinality of the respective winning set divided by the total number of outcomes in the sample space $Fin 3 times Fin 3$. Then $p_{stay} + p_{switch} = 1$.
background
The module models the Monty Hall problem on the finite sample space $Omega = Fin 3 times Fin 3$, with the first coordinate the prize door and the second the player's initial pick. The stay-winning set is the diagonal of three outcomes where prize equals pick; the switch-winning set is the six off-diagonal outcomes. The uniform measure assigns weight 1/9 to each of the nine outcomes. The host always opens a goat door, but this rule does not redistribute probability between the two strategies.
proof idea
The proof is a one-line wrapper that rewrites the sum using p_stay_eq and p_switch_eq, then applies norm_num to confirm that 1/3 + 2/3 equals 1.
why it matters in Recognition Science
This result supplies the partition property required by the Monty Hall master certificate MontyHallCert, which packages the outcome counts and probability values. It completes the derivation in the module's section on the Monty Hall theorem by showing the two strategies are exhaustive on the nine-element space. In the Recognition Science framework it illustrates how conditional-probability statements arise from direct finite enumeration without continuous measures.
scope and limits
- Does not model any specific host door-selection rule beyond guaranteeing a goat is revealed.
- Does not address non-uniform prize placement or biased player picks.
- Does not compute probabilities conditional on the particular door the host opens.
- Does not connect to J-cost, phi-ladder, or ledger structures from the foundation modules.
formal statement (Lean)
165theorem total_probability : p_stay + p_switch = 1 := by
proof body
Term-mode proof.
166 rw [p_stay_eq, p_switch_eq]
167 norm_num
168
169/-- The switch probability is exactly twice the stay probability. -/