tier_weights_pos
plain-language theorem explainer
The theorem establishes strict positivity for each of the five tier weights in the recognition-bandwidth model of primate group size. Researchers deriving Dunbar bounds from sigma-flow budgets cite it to license the subsequent summation step. The proof is a term-mode refinement that unfolds each tier definition and applies div_pos against the known positivity of phi and its powers.
Claim. Let $t_0=1$ and $t_k=t_{k-1}/phi$ for $k=1,2,3,4$. Then $t_k>0$ for every $k=0,1,2,3,4$.
background
The DunbarFromBandwidth module models stable social ties as a multi-tier ledger whose per-agent sigma-budget is capped by the consciousness gap of 45. Each tier weight is obtained from the preceding one by the canonical coordination dividend $1/phi$, where phi is the self-similar fixed point forced in the T0-T8 chain. The five weights therefore form the partial geometric sum $1+1/phi+1/phi^2+1/phi^3+1/phi^4$ that appears in the classical Dunbar estimate.
proof idea
A single refine produces the five-tuple of inequalities. The tier0 case is discharged by norm_num after unfolding. The remaining cases are handled uniformly by the all_goals block: each unfolds its tier and invokes div_pos on a positive numerator together with phi_pos or pow_pos phi_pos.
why it matters
totalWeight_pos obtains the five positivity facts directly from tier_weights_pos and feeds the summed weight into the gap-multiplication that yields the Dunbar band. The result therefore supplies the algebraic prerequisite for the Track I3 derivation of mean stable group size from recognition bandwidth, consistent with the phi-ladder and eight-tick octave structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.