92 unfold totalWeight 93 obtain ⟨h0, h1, h2, h3, h4⟩ := tier_weights_pos 94 linarith 95 96/-- Total weight summed over tiers equals `1 + 1/φ + 1/φ² + 1/φ³ + 1/φ⁴`, 97which by the φ²=φ+1 identity simplifies to `(φ⁵ + φ⁴ + φ³ + φ² + φ)/φ⁵`, 98and since `φ⁵ = 5φ + 3` and `φ + 1 + φ⁻¹ + φ⁻² = (φ⁴+φ³+φ²+φ)/φ³`, 99the closed-form value is `(2φ⁵ - 1)/φ⁴`. We just need `> 0` for the 100master cert; the empirical Dunbar number is read off directly. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.