module module

`IndisputableMonolith.CrossDomain.JEquilibriumUniversality`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (12)

def NashEquilibrium L32
def MarketEquilibrium L33
def HealthEquilibrium L34
theorem nash_eq L36
theorem market_eq L37
theorem health_eq L38
theorem nash_eq_market L41
theorem market_eq_health L42
theorem all_three_equal L43
theorem shared_sensitivity L49
structure JEquilibriumUniversalityCert L52
def jEquilibriumUniversalityCert L60