settlementLevelCount_eq
plain-language theorem explainer
The theorem fixes the number of canonical settlement levels at exactly five in the Recognition Science urban scaling model. Archaeologists and complexity theorists modeling Zipf hierarchies or Christaller central places would cite it to anchor population ratio predictions. The proof is a direct reflexivity step on the constant definition of settlementLevelCount.
Claim. The number of canonical settlement levels is five: $N = 5$, where $N$ denotes the count forced by configuration dimension equal to 5.
background
The module models settlement hierarchies (hamlet to metropolis) via the phi-ladder, with rank-size ratios scaling as phi^k. MODULE_DOC states that five levels are forced by configDim D = 5 and that adjacent-level population ratios equal phi^2 or phi^3, lying inside Christaller's empirical band of 3-7. The upstream definition settlementLevelCount : Nat := 5 supplies the concrete integer used throughout the module.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity (rfl) directly to the definition of settlementLevelCount.
why it matters
The equality is referenced inside the UrbanDensityCert constructor (DOWNSTREAM), which bundles count_eq with positivity and band-inclusion lemmas for the full certification. It supplies the structural count required by the module's plan-v7 claim that settlement scaling follows the phi-ladder, consistent with the Recognition Science forcing chain where discrete counts arise from self-similar fixed points.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.