totalWeight_pos
plain-language theorem explainer
The sum of the five φ-weighted tier costs for social relationships is strictly positive. Sociologists deriving mean stable group sizes from recognition budgets cite this to guarantee a positive predicted Dunbar number. The proof unfolds the total weight definition and applies linear arithmetic to the five individual tier positivity facts.
Claim. The total tier weight satisfies $0 < 1 + φ^{-1} + φ^{-2} + φ^{-3} + φ^{-4}$.
background
In the Recognition Science model each agent maintains pairwise relationships at a cost of one σ-flow unit per cycle. The per-agent budget is bounded by consciousnessGap 3 = 45. Social ties fall into five tiers whose successive costs are scaled by the coordination dividend 1/φ, the self-similar fixed point forced at T6. totalWeight is the sum of these five normalized weights over the φ-ladder.
proof idea
Unfold the definition of totalWeight. Obtain the five positivity hypotheses from the sibling result tier_weights_pos. Conclude by linear arithmetic.
why it matters
This positivity supplies one conjunct of the master certificate dunbarFromBandwidthCert and is invoked in dunbar_one_statement together with the upper bound totalWeight < 5. It closes the positivity half of the structural derivation that places the classical Dunbar 150 inside the band [60, 250] produced by the five-tier φ-weighting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.