dunbar_predicted_pos
plain-language theorem explainer
The theorem shows that the predicted stable group size, obtained as the product of the per-agent recognition budget and the summed tier weights, is strictly positive. Researchers working on bandwidth-limited social network models would cite this result to guarantee that the derived group size is a positive real before taking integer parts or comparing to empirical data. The proof is a direct term-mode application of the multiplication-positivity lemma after unfolding the product definition and confirming the budget constant is positive.
Claim. Let $g = 45$ be the per-agent recognition budget and let $w$ be the total tier weight. Then the predicted stable group size satisfies $0 < g w$.
background
In the Recognition Science treatment of Dunbar's number the per-agent budget is fixed at the consciousness gap for three spatial dimensions, yielding the constant 45. The total tier weight aggregates contributions from successive social tiers scaled by successive powers of $1/φ$, the canonical coordination dividend. Their product defines the predicted group size as a real number whose positivity is asserted here.
proof idea
Unfold the definition of the predicted size to the product of the budget constant and the total weight. Apply the mul_pos lemma; the first factor is shown positive by norm_num on the literal 45, while the second factor is supplied by the already-established totalWeight_pos lemma.
why it matters
The result is invoked inside dunbarFromBandwidthCert to complete the certificate that the predicted size lies in the interval (0,225). It therefore supplies one of the elementary positivity ingredients needed to place the bandwidth-derived group size inside the empirical band [60,250] reported in the module documentation. The derivation rests on the D=3 consciousness gap and the eight-tick octave structure that fixes the tier weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.