module module

`IndisputableMonolith.Sociology.DunbarFromBandwidth`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

def perAgentBudget L53
theorem perAgentBudget_eq L55
theorem perAgentBudget_pos L56
def tier0 L62
def tier1 L65
def tier2 L68
def tier3 L71
def tier4 L74
def totalWeight L77
theorem tier_weights_pos L80
theorem totalWeight_pos L91
theorem totalWeight_lt_5 L101
def dunbar_predicted L129
theorem dunbar_predicted_pos L131
theorem dunbar_predicted_lt_225 L137
structure DunbarFromBandwidthCert L148
def dunbarFromBandwidthCert L155
theorem dunbar_one_statement L166