IndisputableMonolith.Decision.MontyHall

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Monty Hall as a Conditional-Probability Theorem (Track E6)
   7
   8Replaces the earlier placeholder version of this module. The earlier
   9file defined `p_stay := 1/3` and `p_switch := 2/3` and proved
  10`1/3 < 2/3`. That was a label, not a derivation.
  11
  12This file builds the actual Monty Hall sample space, the host's
  13opening rule, and proves switch-wins-with-probability-`2/3` by
  14counting outcomes.
  15
  16## The model
  17
  18There are three doors `d : Fin 3`. The prize is placed uniformly at
  19random behind one door (`prize : Fin 3`). The player picks a door
  20uniformly at random (`pick : Fin 3`). The host then opens a door
  21that is (a) not the player's pick and (b) not the prize. After the
  22host opens, the player either stays with `pick` or switches to the
  23unique remaining unopened door.
  24
  25For any pair `(prize, pick)`, the player's stay-strategy wins iff
  26`pick = prize`; the switch-strategy wins iff `pick ≠ prize`. These
  27are exactly complementary on the sample space.
  28
  29## What we prove
  30
  31Let `Ω := Fin 3 × Fin 3` be the joint sample space of `(prize, pick)`,
  32each of size 3. The uniform measure assigns each of the 9 outcomes
  33weight `1/9`.
  34
  35- `stay_winning_outcomes` has `card = 3` (the diagonal `prize = pick`).
  36- `switch_winning_outcomes` has `card = 6` (the off-diagonal).
  37- Therefore stay-probability `= 3/9 = 1/3`, switch-probability
  38  `= 6/9 = 2/3`.
  39
  40The host's opening choice does **not** enter the win-probability
  41calculation: the host always reveals a goat regardless of whether
  42the player stays or switches. The host's role is to make the second
  43choice possible, not to redistribute probability.
  44
  45## Connection to RS
  46
  47The Monty Hall result is a σ-conserving Bayesian update on the
  48three-door information ledger. The total probability mass is
  49conserved (1) under the host's announcement; the conditional
  50probability that the prize is behind the unopened door (given the
  51host's reveal) carries the full mass that was previously distributed
  52between "the prize is behind one of the two doors I didn't pick."
  53That distribution is `(1/3, 1/3)` before the host opens, but after
  54the host's reveal the mass is concentrated on the single remaining
  55unopened door, giving `2/3`.
  56
  57In the σ-conservation language: the host's announcement is a
  58zero-σ-cost observation (it conveys structure, not energy). The
  59posterior on "prize behind unopened door not picked" thus inherits
  60the full `2/3` prior mass.
  61
  62## Status
  63
  64THEOREM: derived from outcome counting on `Fin 3 × Fin 3`.
  65
  66No HYPOTHESIS, no axiom, no `sorry`. The theorem is a counting
  67statement about a finite product space.
  68-/
  69
  70namespace IndisputableMonolith
  71namespace Decision
  72namespace MontyHall
  73
  74open Constants Cost
  75
  76/-! ## §1. The sample space and outcome predicates -/
  77
  78/-- Joint outcome: prize location and player's initial pick. -/
  79abbrev Outcome : Type := Fin 3 × Fin 3
  80
  81/-- The full sample space `Fin 3 × Fin 3` has 9 outcomes. -/
  82theorem outcome_count : (Finset.univ : Finset Outcome).card = 9 := by
  83  simp [Finset.card_univ, Fintype.card_prod]
  84
  85/-- Stay-winning outcomes: `pick = prize` (the diagonal). -/
  86def StayWins (ω : Outcome) : Prop := ω.2 = ω.1
  87
  88instance (ω : Outcome) : Decidable (StayWins ω) :=
  89  decEq ω.2 ω.1
  90
  91/-- The set of stay-winning outcomes. -/
  92def stayWinningSet : Finset Outcome :=
  93  Finset.univ.filter (fun ω => StayWins ω)
  94
  95/-- Switch-winning outcomes: `pick ≠ prize` (the off-diagonal). The
  96host opens one of the two non-prize, non-pick doors; the unique
  97remaining unopened door is the prize. -/
  98def SwitchWins (ω : Outcome) : Prop := ω.2 ≠ ω.1
  99
 100instance (ω : Outcome) : Decidable (SwitchWins ω) := by
 101  unfold SwitchWins; infer_instance
 102
 103/-- The set of switch-winning outcomes. -/
 104def switchWinningSet : Finset Outcome :=
 105  Finset.univ.filter (fun ω => SwitchWins ω)
 106
 107/-! ## §2. The two outcome sets are complementary -/
 108
 109/-- Every outcome either wins by staying or wins by switching. -/
 110theorem stay_or_switch (ω : Outcome) : StayWins ω ∨ SwitchWins ω := by
 111  unfold StayWins SwitchWins
 112  by_cases h : ω.2 = ω.1
 113  · exact Or.inl h
 114  · exact Or.inr h
 115
 116/-- No outcome wins by both. -/
 117theorem not_both (ω : Outcome) : ¬ (StayWins ω ∧ SwitchWins ω) := by
 118  unfold StayWins SwitchWins
 119  rintro ⟨h₁, h₂⟩
 120  exact h₂ h₁
 121
 122/-! ## §3. Counting the outcome sets -/
 123
 124/-- The diagonal of `Fin 3 × Fin 3` has cardinality 3. -/
 125theorem stayWinningSet_card : stayWinningSet.card = 3 := by
 126  -- Compute by `decide`: the filter is a concrete subset of a concrete finite type.
 127  decide
 128
 129/-- The off-diagonal has cardinality 6 (= 9 − 3). -/
 130theorem switchWinningSet_card : switchWinningSet.card = 6 := by
 131  decide
 132
 133/-! ## §4. Probabilities under the uniform measure -/
 134
 135/-- The probability of a stay-win under the uniform measure on
 136`Fin 3 × Fin 3`. -/
 137def p_stay : ℚ := stayWinningSet.card / (Finset.univ : Finset Outcome).card
 138
 139/-- The probability of a switch-win under the uniform measure. -/
 140def p_switch : ℚ := switchWinningSet.card / (Finset.univ : Finset Outcome).card
 141
 142/-- **STAY-WINS-WITH-PROBABILITY-1/3.** -/
 143theorem p_stay_eq : p_stay = 1 / 3 := by
 144  unfold p_stay
 145  rw [stayWinningSet_card, outcome_count]
 146  norm_num
 147
 148/-- **SWITCH-WINS-WITH-PROBABILITY-2/3.** -/
 149theorem p_switch_eq : p_switch = 2 / 3 := by
 150  unfold p_switch
 151  rw [switchWinningSet_card, outcome_count]
 152  norm_num
 153
 154/-! ## §5. The Monty Hall theorem -/
 155
 156/-- **MONTY HALL THEOREM (counting form).** Switching strictly beats
 157staying: the switch strategy wins on twice as many outcomes as the
 158stay strategy. -/
 159theorem switch_strictly_better : p_stay < p_switch := by
 160  rw [p_stay_eq, p_switch_eq]
 161  norm_num
 162
 163/-- The two probabilities sum to 1: every outcome is either a stay-win
 164or a switch-win. -/
 165theorem total_probability : p_stay + p_switch = 1 := by
 166  rw [p_stay_eq, p_switch_eq]
 167  norm_num
 168
 169/-- The switch probability is exactly twice the stay probability. -/
 170theorem switch_eq_two_stay : p_switch = 2 * p_stay := by
 171  rw [p_stay_eq, p_switch_eq]
 172  norm_num
 173
 174/-! ## §6. Real-valued reformulation (for downstream RS use) -/
 175
 176/-- The stay-win probability cast to `ℝ`. -/
 177noncomputable def p_stay_real : ℝ := (p_stay : ℝ)
 178
 179/-- The switch-win probability cast to `ℝ`. -/
 180noncomputable def p_switch_real : ℝ := (p_switch : ℝ)
 181
 182theorem p_stay_real_eq : p_stay_real = 1 / 3 := by
 183  unfold p_stay_real
 184  rw [p_stay_eq]
 185  push_cast
 186  ring
 187
 188theorem p_switch_real_eq : p_switch_real = 2 / 3 := by
 189  unfold p_switch_real
 190  rw [p_switch_eq]
 191  push_cast
 192  ring
 193
 194theorem switch_strictly_better_real : p_stay_real < p_switch_real := by
 195  rw [p_stay_real_eq, p_switch_real_eq]
 196  norm_num
 197
 198/-! ## §7. Master certificate -/
 199
 200/-- **MONTY HALL MASTER CERTIFICATE.**
 201
 202Five clauses, all derived from outcome counting on `Fin 3 × Fin 3`:
 203
 2041. The sample space has 9 outcomes.
 2052. Stay-winning outcomes: 3 (the diagonal).
 2063. Switch-winning outcomes: 6 (the off-diagonal).
 2074. `p_stay = 1/3` and `p_switch = 2/3`.
 2085. Switching is strictly better; total probability is 1.
 209
 210This is not a label-and-arithmetic statement; the `1/3` and `2/3`
 211are derived from `Finset.card` on the actual sample space. -/
 212structure MontyHallCert where
 213  outcome_count : (Finset.univ : Finset Outcome).card = 9
 214  stay_card : stayWinningSet.card = 3
 215  switch_card : switchWinningSet.card = 6
 216  p_stay_value : p_stay = 1 / 3
 217  p_switch_value : p_switch = 2 / 3
 218  switch_better : p_stay < p_switch
 219  total_probability : p_stay + p_switch = 1
 220  switch_double_stay : p_switch = 2 * p_stay
 221  outcomes_complementary : ∀ ω : Outcome, StayWins ω ∨ SwitchWins ω
 222  outcomes_disjoint : ∀ ω : Outcome, ¬ (StayWins ω ∧ SwitchWins ω)
 223
 224/-- The master certificate is inhabited. -/
 225def montyHallCert : MontyHallCert where
 226  outcome_count := outcome_count
 227  stay_card := stayWinningSet_card
 228  switch_card := switchWinningSet_card
 229  p_stay_value := p_stay_eq
 230  p_switch_value := p_switch_eq
 231  switch_better := switch_strictly_better
 232  total_probability := total_probability
 233  switch_double_stay := switch_eq_two_stay
 234  outcomes_complementary := stay_or_switch
 235  outcomes_disjoint := not_both
 236
 237/-! ## §8. One-statement summary -/
 238
 239/-- **MONTY HALL ONE-STATEMENT THEOREM.**
 240
 241On the joint sample space `Fin 3 × Fin 3` of (prize location, player
 242pick), under the uniform measure:
 243
 244(1) Stay-winning outcomes are the diagonal `pick = prize` (count 3).
 245(2) Switch-winning outcomes are the off-diagonal `pick ≠ prize`
 246    (count 6).
 247(3) Therefore `p_stay = 1/3` and `p_switch = 2/3`.
 248(4) Switching is strictly better, by exactly a factor of 2. -/
 249theorem monty_hall_one_statement :
 250    stayWinningSet.card = 3 ∧
 251    switchWinningSet.card = 6 ∧
 252    p_stay = 1 / 3 ∧
 253    p_switch = 2 / 3 ∧
 254    p_stay < p_switch ∧
 255    p_switch = 2 * p_stay :=
 256  ⟨stayWinningSet_card, switchWinningSet_card,
 257   p_stay_eq, p_switch_eq, switch_strictly_better, switch_eq_two_stay⟩
 258
 259end MontyHall
 260end Decision
 261end IndisputableMonolith
 262