totalWeight_lt_5
plain-language theorem explainer
The sum of five-tier phi-weighted social tie costs equals 1 + 1/φ + 1/φ² + 1/φ³ + 1/φ⁴ and is strictly less than 5. Sociologists deriving stable group sizes from recognition budgets cite this bound to cap the predicted Dunbar number below 225. The proof unfolds the sum definition and applies 1 < φ repeatedly to bound each geometric term below 1, then closes with linear arithmetic.
Claim. Let φ denote the golden ratio. Then $1 + φ^{-1} + φ^{-2} + φ^{-3} + φ^{-4} < 5$.
background
In the Recognition Science model the per-agent σ-budget per cycle is the consciousness gap of 45 for three spatial dimensions. Social ties are partitioned into five tiers whose normalized costs form a geometric series with common ratio 1/φ, where φ satisfies φ² = φ + 1. totalWeight is defined as the sum of these five terms. The module imports the gap definition from Gap45.Derivation and the inequality 1 < φ from Constants and PhiSupport. Upstream lemmas one_lt_phi and phi_squared_bounds supply the strict lower bound on φ and the interval (2.5, 2.7) for φ² that control the term-by-term estimates.
proof idea
The tactic proof first unfolds totalWeight into the explicit sum of five terms. Four auxiliary facts are then proved: each 1/φ^k < 1 for k = 1 to 4. The k = 1 case rewrites div_lt_one and invokes one_lt_phi. The k = 2 case uses phi_squared_bounds inside linarith. The k = 3 and k = 4 cases apply pow_le_pow_right₀ to the base inequality 1 < φ. The final linarith step assembles the four strict inequalities into the target bound.
why it matters
The inequality supplies the missing numerical control that lets dunbarFromBandwidthCert, dunbar_one_statement and dunbar_predicted_lt_225 close the derivation of mean stable group size as perAgentBudget · totalWeight. It converts the fixed gap of 45 into the concrete upper limit 225 that comfortably contains the classical Dunbar value of 150. The result rests on the self-similar fixed-point property of φ forced in the T5–T6 steps of the unified forcing chain and on the five-tier truncation of the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.