module module moderate

`IndisputableMonolith.Decision.MontyHall`

Decision.MontyHall module encodes the Monty Hall setup inside Recognition Science by defining joint outcomes of prize location and initial pick, then constructing stay and switch winning sets with their cardinalities and probabilities. Decision theorists embedding classical paradoxes into cost-based frameworks would cite the definitions. The module consists of direct type and set constructions that draw on imported Cost primitives and Mathlib cardinality tools.

claimLet Outcome denote the set of pairs (prize location, initial pick). Define StayWins and SwitchWins as the corresponding winning subsets, with stayWinningSet_card and switchWinningSet_card their sizes; the probabilities are then $p_{stay} = |StayWins| / |Outcome|$ and $p_{switch} = |SwitchWins| / |Outcome|$.

background

The module belongs to the Decision domain and imports Constants, where the fundamental RS time quantum satisfies τ₀ = 1 tick, together with the Cost module that supplies the cost primitives used for decision evaluation. Its central object is Outcome, defined as the joint outcome of prize location and player's initial pick. Sibling declarations introduce outcome_count, stay_or_switch, not_both, the two winning sets, their cardinalities, and the two probabilities p_stay and p_switch.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies concrete outcome and probability objects to the Decision domain of the Recognition monolith. It draws directly on the Cost module for its underlying cost structure and populates the namespace with the joint-outcome definitions needed for later decision calculations. No downstream uses appear in the current dependency graph.

scope and limits

Does not derive the classical 2/3 switching probability from RS axioms.
Does not invoke the J-function, phi ladder, or eight-tick octave.
Does not model explicit host behavior or information revelation steps.
Does not connect the probabilities to any RS-native constants such as α or G.

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