tier3
plain-language theorem explainer
Tier-3 weight assigns cost 1/φ³ to recognized faces inside the five-tier social bandwidth model. Researchers deriving Dunbar numbers from phi-ladder coordination costs cite this term when summing contributions to the total stable group size. It is introduced by direct definition as the reciprocal of phi cubed.
Claim. The weight for tier-3 social ties (recognized faces) equals $1/φ^3$, where $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The DunbarFromBandwidth module models stable group size as a bandwidth limit on multi-agent recognition ledgers. Each agent maintains a σ-budget of 45 units per cycle; ties are partitioned into five tiers whose costs decrease by successive factors of 1/φ. Tier 3 specifically captures recognized faces at relative cost 1/φ³. This weighting scheme follows the canonical RS coordination dividend and the recognition composition law.
proof idea
Direct definition that sets tier3 equal to the real number 1/φ³. No lemmas or tactics are invoked; the declaration serves as an atomic building block for the totalWeight sum and the positivity theorem.
why it matters
Supplies the third term in totalWeight, which enters both the positivity theorem tier_weights_pos and the bound totalWeight_lt_5. It instantiates the phi-ladder rung for recognized faces, contributing to the derivation of the classical Dunbar value near 145 as the five-tier sum and linking recognition costs to the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.