module module

`IndisputableMonolith.CrossDomain.JPositivityUniversality`

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 (19)

def TurbulentCost L34
def DiseaseCost L35
def OffTargetCost L36
def OffEquilibriumGameCost L37
def MarketArbitrageGap L38
def BiasedReasoningCost L39
def RecognitionDeficit L40
theorem turbulent_cost L42
theorem disease_cost L43
theorem off_target_cost L44
theorem off_equilibrium_game_cost L45
theorem market_arbitrage_gap L47
theorem biased_reasoning_cost L49
theorem recognition_deficit L51
theorem all_seven_are_one L56
theorem symmetry_at_equilibrium L66
theorem minimum_at_one L70
structure JPositivityUniversalityCert L77
def jPositivityUniversalityCert L94