layerSize
plain-language theorem explainer
layerSize(k) sets the size of the k-th tier in a phi-scaled model of Dunbar social networks to five times the golden ratio raised to twice the layer index. Social physicists or network theorists working within Recognition Science would cite this expression when deriving hierarchical relationship counts. The definition is introduced directly as an explicit formula on the phi-ladder.
Claim. For each natural number $k$, the size of the $k$-th social layer equals $5 phi^{2k}$, where $phi$ is the golden ratio.
background
The Dunbar Layers from Phi module models human social networks as recognition rungs on the phi-ladder. Adjacent layers scale by phi squared, reproducing the observed ratios 5/15, 15/50, 50/150 and 150/500. The base size of five matches the configuration dimension D equals five. The golden ratio phi is taken from the imported Constants module and satisfies the self-similar fixed-point property established earlier in the forcing chain.
proof idea
This is a direct definition that assigns to each natural number k the real number five multiplied by phi to the power of two times k.
why it matters
The definition supplies the explicit sizes required by DunbarLayersCert to certify five layers, positive values at every rung, and exact successive ratios of phi squared. It places the empirical Dunbar sequence inside the Recognition Science phi-ladder, connecting to the T6 fixed-point forcing and the eight-tick octave structure. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.