UrbanLevel
plain-language theorem explainer
UrbanLevel enumerates five discrete urbanization tiers as the basis for phi-ladder modeling of city-size hierarchies. Researchers applying Recognition Science to Zipf distributions cite it to fix the discrete levels before certifying population ratios. The declaration is a direct inductive definition with five constructors that derives Fintype for immediate cardinality use.
Claim. The inductive type of urbanization levels is generated by the five constructors hamlet, village, town, city, and metropolis.
background
Recognition Science models urban hierarchies via the phi-ladder, where adjacent tiers differ in population by factors of phi. The module states that city-size distributions obey Zipf's law (rank times population constant) and translates this to a population ratio of phi^{-1} between adjacent ranks, with five levels matching configDim D=5. UrbanLevel supplies the concrete discrete set for these tiers.
proof idea
Direct inductive definition introducing the five constructors and deriving DecidableEq, Repr, BEq, and Fintype instances.
why it matters
UrbanLevel supplies the five levels required by the downstream UrbanizationCert structure, which asserts Fintype.card UrbanLevel = 5 together with the phi population ratio for every adjacent rung. It anchors the discrete enumeration needed to certify urbanization rates inside the phi-ladder framework. The definition closes the configDim D=5 step for this sociology application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.