dunbar_predicted
plain-language theorem explainer
Predicted stable group size equals the per-agent recognition budget multiplied by the summed tier weights. Primatologists and sociologists testing bandwidth limits on social ties cite this when deriving mean group sizes from recognition costs. The definition is a direct cast-and-multiply of the consciousness gap value at three dimensions with the five-tier phi-weighted sum.
Claim. The predicted mean stable group size is the real number $45 w$, where $w$ is the sum of five tier weights $1 + 1/φ + 1/φ² + 1/φ³ + 1/φ⁴$.
background
The module derives mean stable group size as a bandwidth bound on the multi-agent recognition ledger. Each pairwise relationship costs one unit of σ-flow per cycle. The per-agent budget is the consciousness gap at D=3, fixed at 45. Total weight sums the phi-scaled costs across five tiers of ties (close to acquaintance), where each tier costs 1/φ of the previous. Upstream perAgentBudget is defined as the natural number 45. Upstream totalWeight is the real sum tier0 + tier1 + tier2 + tier3 + tier4.
proof idea
One-line definition that casts perAgentBudget to real and multiplies by totalWeight.
why it matters
This definition supplies the core numerical prediction certified in DunbarFromBandwidthCert and stated in dunbar_one_statement. It realizes the bandwidth bound on group size from the Recognition Science model at D=3, using the phi-ladder from the forcing chain. The result places the classical 150 within the derived band below 225.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.