`totalCoalitionTypes`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim
domain: GameTheory
line: 47 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.CoalitionSizeFromConfigDim on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  44def configDim : ℕ := 3
  45
  46/-- Total coalition types: 2^D - 1. -/
  47def totalCoalitionTypes : ℕ := 2 ^ configDim - 1
  48
  49theorem totalCoalitionTypes_eq : totalCoalitionTypes = 7 := by
  50  unfold totalCoalitionTypes configDim; norm_num
  51
  52/-- Minimum winning coalition size: ceil(2^(D-1)). -/
  53def mwcSize : ℕ := 2 ^ (configDim - 1)
  54
  55theorem mwcSize_eq : mwcSize = 4 := by
  56  unfold mwcSize configDim; norm_num
  57
  58/-- MWC size is at most half of total coalition types (rounded up). -/
  59theorem mwcSize_le_half :
  60    2 * mwcSize ≤ totalCoalitionTypes + 1 := by
  61  simp [mwcSize_eq, totalCoalitionTypes_eq]
  62
  63/-- MWC size is positive. -/
  64theorem mwcSize_pos : 0 < mwcSize := by
  65  rw [mwcSize_eq]; norm_num
  66
  67structure CoalitionSizeCert where
  68  total_eq : totalCoalitionTypes = 7
  69  mwc_eq : mwcSize = 4
  70  mwc_le_half : 2 * mwcSize ≤ totalCoalitionTypes + 1
  71  mwc_pos : 0 < mwcSize
  72
  73noncomputable def cert : CoalitionSizeCert where
  74  total_eq := totalCoalitionTypes_eq
  75  mwc_eq := mwcSize_eq
  76  mwc_le_half := mwcSize_le_half
  77  mwc_pos := mwcSize_pos

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.