totalWeight
plain-language theorem explainer
The total weight sums the five geometrically decreasing tier costs in the social recognition model. Recognition theorists cite it to scale the per-agent budget into a predicted stable group size. The definition performs a direct arithmetic sum of the tier constants with no lemmas or tactics applied.
Claim. $W = 1 + φ^{-1} + φ^{-2} + φ^{-3} + φ^{-4}$, where each term is the relative maintenance cost of one social tier and φ is the golden ratio satisfying φ² = φ + 1.
background
Social ties are partitioned into five tiers whose costs decrease by the factor 1/φ at each step. Tier 0 costs one full unit for close ties, tier 1 costs 1/φ for casual contacts, tier 2 costs 1/φ² for acquaintances, tier 3 costs 1/φ³ for recognized faces, and tier 4 costs 1/φ⁴ for mere recognitions. This geometric weighting follows from the coordination dividend in the Recognition Composition Law.
proof idea
The definition is a direct arithmetic sum of the five preceding tier constants. No lemmas or tactics are required.
why it matters
The sum supplies the multiplier for the 45-unit per-agent budget inside the predicted group size, which is then bounded above by 225 in the master certificate DunbarFromBandwidthCert. It implements the five-tier phi-ladder that reproduces the classical Dunbar estimate of approximately 150 within the derived band [60, 250]. The quantity is referenced by the one-statement packaging theorem and the positivity and upper-bound lemmas that feed the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.