dunbarFromBandwidthCert
plain-language theorem explainer
This definition assembles a certificate that the predicted stable group size equals perAgentBudget times totalWeight and lies strictly between 0 and 225. Network theorists and primatologists would cite it to obtain the classical Dunbar interval as a derived consequence of a 45-unit recognition budget and five-tier phi weighting. The construction is a direct field assignment from five sibling lemmas that fix the budget numerically, bound the weight sum, and verify the product inequalities.
Claim. The certificate records the assertions $perAgentBudget = 45$, $0 < totalWeight < 5$, and $0 < dunbar_predicted < 225$, where $dunbar_predicted$ denotes the product of the per-agent budget and the summed phi-tier weights.
background
The module derives mean stable group size from the Recognition Science bandwidth model. Each agent is allocated a fixed sigma-flow budget given by consciousnessGap 3 = 45. Social ties are partitioned into five tiers whose relative costs follow the canonical phi-ladder: the total weight is the partial sum $1 + phi^{-1} + phi^{-2} + phi^{-3} + phi^{-4}$, which is shown to be positive and strictly less than 5. The predicted group size is the product of budget and total weight; the classical Dunbar value of approximately 150 arises when the sum is truncated at the active-plus-passive tiers. Upstream lemmas on the simplicial ledger and mechanism design from sigma supply the collision-free accounting that justifies treating pairwise recognition events as additive sigma-costs.
proof idea
The definition is a one-line wrapper that populates the five fields of the DunbarFromBandwidthCert structure. It obtains the budget equality directly from perAgentBudget_eq, the positivity and upper bound on totalWeight from the corresponding sibling lemmas, and the two inequalities on dunbar_predicted by unfolding the product definition and substituting the numerical budget value together with the weight bound.
why it matters
The certificate supplies the concrete bound required by the sociology track of Plan v5, confirming that the recognition-budget derivation yields a stable-group-size interval comfortably containing the empirical 150. It closes the local derivation without introducing new axioms and links the result to the phi-ladder and eight-tick octave already established in the forcing chain. No downstream theorems are recorded, leaving the certificate as a self-contained empirical interface whose falsification band is stated explicitly in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.