urbanLevelCount
plain-language theorem explainer
The declaration asserts that the inductive type enumerating urbanization tiers contains exactly five elements. Urban theorists applying the Recognition Science phi-ladder to Zipf-distributed city hierarchies would cite this count when certifying the canonical five-tier model. The proof is a one-line decision procedure that enumerates the five explicit constructors.
Claim. The finite type of urbanization levels has cardinality five: $|U| = 5$, where $U$ consists of the tiers hamlet, village, town, city, metropolis.
background
The module models city-size distributions via Zipf's law recast in RS terms, where adjacent tiers differ in population by a factor of phi squared. The inductive type UrbanLevel enumerates the five canonical levels (hamlet, village, town, city, metropolis) that realize configDim D = 5. This cardinality result is referenced directly by the downstream urbanizationCert structure.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card of the inductive type UrbanLevel, whose five constructors are decidably enumerable.
why it matters
This supplies the five_levels component of the downstream urbanizationCert definition, completing the certification of the five-tier phi-ladder hierarchy. It instantiates the framework prediction that urbanization follows the same D = 5 configurational dimension used for spatial structure, consistent with the eight-tick octave and phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.