module module high

`IndisputableMonolith.Sociology.DunbarFromBandwidth`

The module defines the per-agent σ-budget per recognition cycle, equating it to the consciousness gap at D=3, and introduces tier weights under the RS cost structure. Sociologists and network theorists would cite it to ground observed social layers in fundamental recognition costs. The module supplies a sequence of definitions for the budget and weights together with elementary positivity and bound lemmas.

claimThe per-agent budget satisfies $σ = $ consciousness gap at $D=3$, with tier weights $w_k$ ($k=0$ to $4$) obeying $w_k > 0$ and total weight $<5$.

background

Recognition Science fixes constants in native units with $c=1$ and derives all structure from the J-cost functional equation. The upstream Constants module supplies the base time quantum $τ_0 = 1$ tick. The Cost module provides the recognition cost functions. This sociology module applies those objects at three spatial dimensions to introduce the per-agent σ-budget, identified with the consciousness gap, as the fundamental resource per recognition cycle.

proof idea

This is a definition module. It defines perAgentBudget, proves equality to consciousnessGap at D=3 together with positivity, then defines tier0 through tier4, totalWeight, and establishes positivity of the tier weights plus the strict bound totalWeight < 5.

why it matters in Recognition Science

The module supplies the bandwidth foundation that places social tier structures inside the Recognition framework, linking directly to the eight-tick octave and D=3 from the unified forcing chain. It enables future derivations of Dunbar-like numbers from per-agent costs. No downstream uses are recorded yet.

scope and limits

Does not derive explicit numerical values for group sizes.
Does not incorporate empirical anthropological data.
Does not model network dynamics or evolution.
Does not address cross-cultural variations.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (18)

def perAgentBudget L53
theorem perAgentBudget_eq L55
theorem perAgentBudget_pos L56
def tier0 L62
def tier1 L65
def tier2 L68
def tier3 L71
def tier4 L74
def totalWeight L77
theorem tier_weights_pos L80
theorem totalWeight_pos L91
theorem totalWeight_lt_5 L101
def dunbar_predicted L129
theorem dunbar_predicted_pos L131
theorem dunbar_predicted_lt_225 L137
structure DunbarFromBandwidthCert L148
def dunbarFromBandwidthCert L155
theorem dunbar_one_statement L166