dunbar_one_statement
plain-language theorem explainer
The theorem establishes that the per-agent recognition budget equals 45, the summed tier weights lie strictly between 0 and 5, and the predicted stable group size is less than 225. Primatologists and social theorists studying bandwidth-limited group sizes would cite this as the compact reference containing the classical Dunbar estimate. The proof is a term-mode constructor that directly assembles four supporting lemmas into the required conjunction.
Claim. Let $b$ be the per-agent recognition budget per cycle and $w$ the total weight summed over five tiers of social ties. Then $b=45$, $0<w<5$, and the predicted mean stable group size $d=b·w$ satisfies $d<225$.
background
Recognition Science models stable group size as a bandwidth constraint on the multi-agent recognition ledger. The per-agent budget is defined as consciousnessGap at three spatial dimensions and equals 45 units per cycle. Total weight is the sum of five tier weights with successive costs scaled by inverse powers of the golden ratio, so that $w=1+φ^{-1}+φ^{-2}+φ^{-3}+φ^{-4}$ where $φ$ is the self-similar fixed point from the forcing chain. The predicted group size is the product of budget and total weight. Upstream lemmas establish the budget equality by reflexivity, the strict upper bound $w<5$ via $φ$-power inequalities, and the product bound by unfolding the definition.
proof idea
The proof is a term-mode constructor that packages four prior results: the reflexivity proof of the budget equality, the positivity theorem for total weight, the strict upper bound totalWeight < 5 obtained from successive divisions by $φ$, and the product inequality obtained by unfolding dunbar_predicted and substituting the budget and weight facts.
why it matters
This one-statement theorem consolidates the derivation of Dunbar's number from recognition bandwidth in the Sociology track. It sits downstream of the tier-weight definitions and the consciousnessGap at D=3, supplying a compact reference for the falsifiable band containing the empirical range 100-250. The result links the eight-tick octave and phi-ladder directly to a sociological prediction; the open question of precise cross-species calibration remains for empirical data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.