module module

`IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive`

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

declarations in this module (11)

structure SigmaPopulation L26
def sigmaSpread L32
def totalAbsSigma L36
structure Strategy L40
def spreadAfter L44
def loveStrategy L48
def selfishStrategy L52
theorem love_minimizes_sigma_spread L60
theorem sigmaSpread_nonneg L70
theorem love_is_fastest_equilibration L74
theorem selfish_strategies_increase_global_sigma L87