module module moderate

`IndisputableMonolith.Sociology.DunbarFromBandwidth`

This module defines the per-agent σ-budget as the consciousness gap evaluated at D=3, supplying the recognition cost foundation for tiered social bandwidth. Cognitive scientists or RS sociologists would cite these definitions when deriving network-size limits from the phi-ladder and J-cost. The module is a pure definition block containing perAgentBudget together with tier weights, totalWeight, and their elementary positivity and bounding lemmas.

claimDefine the per-agent budget by $\sigma_{\rm budget} := \text{consciousnessGap}(D=3)$. Introduce tier weights $w_0,\dots,w_4$ and total weight $W=\sum w_i$ satisfying $W<5$ together with the positivity statements $w_i>0$.

background

The module imports the RS time quantum $\tau_0=1$ tick from Constants and the cost machinery from the Cost module. It works in the D=3 sector fixed by the T8 step of the forcing chain. The central object is the per-agent $\sigma$-budget per recognition cycle, identified with consciousnessGap at three spatial dimensions; the remaining declarations introduce five social tiers, their weights, and the total weight together with sign and bound lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the bandwidth parameter that would feed any downstream theorem linking the eight-tick octave and D=3 to cognitive limits such as Dunbar numbers. It closes the interface between the core forcing chain (T5–T8) and the sociology domain, though the dependency graph currently lists no parent theorems.

scope and limits

Does not derive a numerical Dunbar number.
Does not incorporate empirical social-network data.
Does not address stability under variation of the gap parameter.
Does not generalize the construction beyond D=3.

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