module module high

`IndisputableMonolith.Decision.MontyHall`

The MontyHall module supplies the sample space and counting machinery for the Monty Hall decision problem inside Recognition Science. It defines the joint outcome of prize location and initial pick, then builds the stay and switch winning sets together with their cardinalities and probabilities. The module is used by any RS analysis that compares decision strategies under the cost structure. It is a pure definition module containing no proofs.

claimLet $Outcome$ be the set of pairs (prize location, initial pick). Define $stayWinningSet, switchWinningSet$ as the subsets of winning outcomes under each strategy, with $p_{stay} = |stayWinningSet| / |Outcome|$ and $p_{switch} = |switchWinningSet| / |Outcome|$.

background

The module sits in the Decision domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost formalism from the Cost module. Its central object is Outcome, the joint outcome consisting of prize location and the player's initial pick. From Outcome it derives outcome_count, the finite cardinality of the sample space, the subsets StayWins and SwitchWins, their cardinalities stayWinningSet_card and switchWinningSet_card, and the two probability values p_stay and p_switch.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module provides the concrete Monty Hall model that feeds decision-theoretic comparisons under the Recognition Composition Law. It supplies the probability objects that any later theorem on optimal switching strategies would cite. No downstream theorems are recorded in the current dependency graph.

scope and limits

Does not model the host's reveal action explicitly.
Does not prove p_switch > p_stay.
Does not link to the phi-ladder or mass formulas.
Does not assign numerical values to the probabilities.
Does not incorporate cost values from the Cost module.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (25)

abbrev Outcome L79
theorem outcome_count L82
def StayWins L86
def stayWinningSet L92
def SwitchWins L98
def switchWinningSet L104
theorem stay_or_switch L110
theorem not_both L117
theorem stayWinningSet_card L125
theorem switchWinningSet_card L130
def p_stay L137
def p_switch L140
theorem p_stay_eq L143
theorem p_switch_eq L149
theorem switch_strictly_better L159
theorem total_probability L165
theorem switch_eq_two_stay L170
def p_stay_real L177
def p_switch_real L180
theorem p_stay_real_eq L182
theorem p_switch_real_eq L188
theorem switch_strictly_better_real L194
structure MontyHallCert L212
def montyHallCert L225
theorem monty_hall_one_statement L249