UrbanizationCert
plain-language theorem explainer
UrbanizationCert packages the two core predictions of the phi-ladder model for city sizes: exactly five discrete levels and geometric population growth by the golden ratio phi at each rung. Sociologists or complexity theorists working on Zipf's law would cite this structure when formalizing scale-free urban hierarchies. The definition is a direct record type that bundles the Fintype cardinality of UrbanLevel with the ratio property of populationAtRung.
Claim. The structure $UrbanizationCert$ consists of a proof that the set of urban levels has cardinality 5 together with the assertion that the population at rung $k+1$ divided by the population at rung $k$ equals the golden ratio $phi$ for every natural number $k$.
background
In the Recognition Science treatment of urbanization, city sizes are organized on a phi-ladder where population scales geometrically with rung index. The inductive type UrbanLevel enumerates five discrete tiers (hamlet, village, town, city, metropolis) whose Fintype cardinality is fixed at 5. The auxiliary function populationAtRung assigns to each natural number rung $k$ the value $100 times phi^k$, so that adjacent rungs differ by the factor phi. This module imports the golden-ratio constant from Constants and the phi_ratio definition from the quasicrystal development, which supplies the inverse $1/phi$ as an energy proxy. The local theoretical setting asserts that the urban hierarchy follows the phi-ladder with five canonical levels corresponding to configuration dimension D = 5, consistent with Zipf's law in log space.
proof idea
The declaration is a structure definition with no proof body. It simply records the two predicates: the Fintype.card of UrbanLevel equals 5, which follows from the five constructors of the inductive type, and the universal quantification over $k$ of the population ratio equaling phi, which holds by direct substitution into the definition of populationAtRung.
why it matters
This structure supplies the certificate type consumed by the downstream definition urbanizationCert, which constructs an explicit inhabitant using urbanLevelCount and populationRatio. It fills the role of packaging the two core empirical predictions of the phi-ladder model for urban systems, linking the five-level hierarchy (configDim D = 5) to the geometric growth factor phi. Within the Recognition framework the construction closes the loop from the forcing chain T5-T8 through the Recognition Composition Law to a concrete sociological observable, with no open scaffolding remaining in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.