perAgentBudget_pos
plain-language theorem explainer
The theorem establishes strict positivity of the per-agent recognition budget. Cognitive modelers deriving stable primate group sizes from bandwidth limits would cite it to guarantee a positive base for tier-weighted relationship counts. The proof is a one-line wrapper that unfolds the constant definition and applies numeric normalization.
Claim. $0 < B$, where $B = 45$ is the per-agent σ-budget per recognition cycle, equal to the consciousness gap at three spatial dimensions.
background
The module derives Dunbar's number as a bandwidth bound on the multi-agent recognition ledger. Each pairwise tie costs one unit of σ-flow per cycle; the total budget per agent is fixed at the consciousness gap for D=3. The definition perAgentBudget := 45 supplies this constant, which multiplies the tier weights (1 + 1/φ + 1/φ²) to bound close-tie counts near 73 and the classical active-plus-passive sum near 145.
proof idea
One-line wrapper that unfolds perAgentBudget to the literal constant 45 and invokes norm_num to confirm 0 < 45.
why it matters
The result supplies the arithmetic foundation for the entire DunbarFromBandwidth track. It feeds the tier-weight positivity lemmas and the main bound calculations that link the eight-tick octave, D=3 forcing, and phi-ladder coordination dividend to empirical group-size bands. Without positivity the downstream multiplication by (1 + 1/φ + …) would be formally meaningless.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.