No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
62def tier0 : ℝ := 1
proof body
Definition body.
63
64/-- Tier-1 weight: 1/φ (casual contacts). -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
tier_weights_pos
in IndisputableMonolith.Sociology.DunbarFromBandwidth
decl_use
-
totalWeight
in IndisputableMonolith.Sociology.DunbarFromBandwidth
decl_use
-
totalWeight_lt_5
in IndisputableMonolith.Sociology.DunbarFromBandwidth
decl_use