`is`

definition

show as: view math explainer →

module: IndisputableMonolith.GameTheory.MechanismDesignFromSigma
domain: GameTheory
line: 388 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.GameTheory.MechanismDesignFromSigma on GitHub at line 388.

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

 385in the two-agent argument.
 386
 387Done at `n = 2` here because that is where the σ-conservation
 388structure is cleanest. The combinatorial extension is mechanical
 389and adds no RS-relevant content. The `n`-agent statement is the
 390right next file: `MechanismDesignFromSigmaGeneralN.lean`.
 391-/
 392
 393end MechanismDesignFromSigma
 394end GameTheory
 395end IndisputableMonolith

papers checked against this theorem

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