dunbar_predicted_lt_225
plain-language theorem explainer
The declaration shows that the recognition-derived prediction for mean stable group size lies strictly below 225. Researchers working on the bandwidth model of social cognition would cite this to bound the classical Dunbar estimate of 150. The short tactic proof substitutes the explicit budget value 45 and reduces the product inequality via nlinarith on the total-weight bound.
Claim. The predicted stable group size satisfies $dunbar_predicted < 225$, where $dunbar_predicted$ equals the product of the per-agent recognition budget (equal to 45) and the summed five-tier weight (strictly less than 5).
background
In the Recognition Science framework the mean stable group size emerges as the product of the per-agent recognition budget and a five-tier weight sum. The budget equals the consciousness gap at three spatial dimensions, fixed at 45. The tier weights are successive powers of the inverse golden ratio, summing to a quantity strictly between 0 and 5. The upstream result totalWeight_lt_5 supplies the strict upper bound of 5, while totalWeight_pos guarantees positivity. These combine with the definition of the predicted size to close the numerical bound.
proof idea
The proof first unfolds the definition of the predicted size. It then obtains the equality perAgentBudget = 45 by direct computation. Finally it rewrites the equality and applies nlinarith to the conjunction of totalWeight < 5 and totalWeight > 0.
why it matters
This inequality supplies the upper bound required by the master certificate dunbarFromBandwidthCert. It appears in the one-statement summary theorem that packages the entire derivation. The result confirms that the phi-weighted bandwidth model produces a band containing the empirical Dunbar value of approximately 150, consistent with the eight-tick octave and D=3 structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.