DunbarFromBandwidthCert
plain-language theorem explainer
The structure certifies that the predicted Dunbar number lies strictly between 0 and 225 when the per-agent budget equals 45 and the summed tier weight lies between 0 and 5. Sociologists modeling group size from recognition costs would cite the certificate to bound the classical 150 estimate. It is realized as a record whose five fields are populated from sibling definitions and positivity lemmas.
Claim. Let $B = 45$ be the per-agent recognition budget in units of recognition flow and let $W$ be the total weight summed over five tiers of social ties. Define the predicted stable group size by $D = B W$. The certificate asserts $B = 45$, $0 < W < 5$, and $0 < D < 225$.
background
Recognition Science models stable social groups as limited by per-agent bandwidth in the recognition-flow ledger. The per-agent budget is fixed at the consciousness gap for three spatial dimensions, yielding the constant 45. Total tier weight aggregates five levels of relationship strength, each scaled by successive factors of $1/φ$ to encode the coordination dividend from the Recognition Composition Law. The predicted Dunbar number is the direct product of budget and total weight. Upstream results supply the definition of this product, the fixed budget value, and the positivity of the summed weights. The module situates the construction as a real derivation of mean stable group size from bandwidth constraints, with empirical means expected in the 100-250 interval.
proof idea
The structure is introduced by direct field assignment. Each field pulls its value from a sibling definition or lemma: the budget equality from the constant definition, the weight bounds from positivity and upper-bound lemmas, and the predicted bounds from the product definition combined with those weight inequalities.
why it matters
This definition supplies the bounding certificate that feeds the master dunbarFromBandwidthCert. It realizes the module's claim that bandwidth produces group sizes comfortably containing the classical 150 value. The construction draws on the D=3 spatial dimension for the gap constant and the phi-ladder for tier weights, closing one step in the sociology track of the forcing chain. It touches the open question of precise cross-cultural calibration within the predicted band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.