layerSize_pos
plain-language theorem explainer
The theorem shows that layer sizes remain strictly positive for every natural number index in the phi-scaled Dunbar model. Social network theorists working within Recognition Science would cite it to ensure each tier count exceeds zero before assembling the full certification. The proof is a one-line wrapper that invokes mul_pos on the constant factor five and a power of phi.
Claim. For every natural number $k$, the $k$-th layer size satisfies $0 < 5 phi^{2k}$, where $phi$ denotes the golden ratio.
background
The Dunbar Layers from Phi module treats social network tiers as recognition rungs on the phi-ladder. Layer sizes follow the explicit formula five times phi raised to twice the rung index, producing the observed approximate ratio of one over phi squared between adjacent layers. The module imports the constants file that supplies phi and records zero sorry statements for the entire development.
proof idea
The proof is a one-line wrapper that applies the mul_pos lemma to the constant five and the power term. It calls pow_pos on phi_pos to establish that the exponentiated golden ratio stays positive for any natural exponent.
why it matters
This result supplies the layer_pos field inside dunbarLayersCert, which completes the certification of the five-layer structure together with the layer count and the phi-squared ratio. It anchors the phi-ladder construction used for social scales, consistent with the self-similar fixed point forced in the unified chain. No open scaffolding remains after this positivity step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.