tier4
plain-language theorem explainer
Modelers deriving primate group sizes from recognition bandwidth cite this definition for the weight of the fourth tier of mere recognitions. It supplies the final term in the geometric series of tier weights that recovers the classical Dunbar number near 145 when multiplied by the consciousness gap of 45. The definition is a direct real-number assignment using the golden-ratio scaling fixed by the forcing chain.
Claim. Define the tier-4 weight by $w_4 := 1/φ^4$, where $φ$ is the golden ratio and the weight applies to the outermost tier of mere recognitions in the five-tier social model.
background
The DunbarFromBandwidth module derives stable group sizes as a bandwidth bound on the multi-agent recognition ledger. Each pairwise relationship costs one unit of σ-flow per cycle, with the per-agent budget fixed at the consciousness gap of 45. Tier weights decrease geometrically by the factor 1/φ, reflecting the coordination dividend from the Recognition Composition Law. Tier 0 carries weight 1 for closest ties, tier 1 weight 1/φ, tier 2 weight 1/φ², tier 3 weight 1/φ³, and tier 4 weight 1/φ⁴ for mere recognitions. The sum of the first three tiers yields the active bound near 73, while the full five-tier sum recovers the classical Dunbar value of approximately 145. This definition completes the totalWeight expression used to establish positivity of all weights and the strict inequality totalWeight < 5.
proof idea
This is a direct definition that evaluates to the real number 1 divided by phi raised to the fourth power. No lemmas are applied; the value follows from the tier scaling convention already fixed in the module.
why it matters
The definition feeds directly into totalWeight, tier_weights_pos, and totalWeight_lt_5. It fills the final slot in the five-tier expansion that produces the classical Dunbar number as 45 times the sum of the geometric series. The construction rests on the phi-ladder fixed by T6 in the UnifiedForcingChain and the RCL identity. It touches the open question of the empirical band 100–250 across studies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.