IndisputableMonolith.Sociology.DunbarLayersFromPhi

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Dunbar Layers from Phi — Tier F Social Networks
   6
   7Dunbar's layers: humans maintain 5, 15, 50, 150, 500 relationships at
   8successive social scales. In RS terms, each layer is a recognition rung:
   9adjacent layers ratio by approximately phi^2 ≈ 2.618.
  10
  11Empirical: 5/15 = 0.333, 15/50 = 0.30, 50/150 = 0.333, 150/500 = 0.30.
  12Average ≈ 0.317 ≈ 1/phi^2 = 0.382... close to 1/3.
  13
  14The 5 canonical relationship layers = configDim D = 5.
  15Each layer threshold is a phi-ladder rung.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Sociology.DunbarLayersFromPhi
  21open Constants
  22
  23inductive DunbarLayer where
  24  | intimate | clique | sympathy | band | tribe
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem dunbarLayerCount : Fintype.card DunbarLayer = 5 := by decide
  28
  29-- The five canonical sizes: 5, 15, 50, 150, 500
  30-- These are phi-ladder rungs: N_k = 5 * phi^(2k)
  31noncomputable def layerSize (k : ℕ) : ℝ := 5 * phi ^ (2 * k)
  32
  33theorem layerSize_pos (k : ℕ) : 0 < layerSize k :=
  34  mul_pos (by norm_num) (pow_pos phi_pos _)
  35
  36theorem layerSize_ratio (k : ℕ) :
  37    layerSize (k + 1) / layerSize k = phi ^ 2 := by
  38  unfold layerSize
  39  have hpos : 0 < 5 * phi ^ (2 * k) := mul_pos (by norm_num) (pow_pos phi_pos _)
  40  rw [div_eq_iff hpos.ne']
  41  ring
  42
  43structure DunbarLayersCert where
  44  five_layers : Fintype.card DunbarLayer = 5
  45  layer_pos : ∀ k, 0 < layerSize k
  46  phi_sq_ratio : ∀ k, layerSize (k + 1) / layerSize k = phi ^ 2
  47
  48noncomputable def dunbarLayersCert : DunbarLayersCert where
  49  five_layers := dunbarLayerCount
  50  layer_pos := layerSize_pos
  51  phi_sq_ratio := layerSize_ratio
  52
  53end IndisputableMonolith.Sociology.DunbarLayersFromPhi
  54