urbanizationCert
plain-language theorem explainer
The declaration assembles a concrete instance of the urbanization certificate by supplying the five-level cardinality and the consecutive-rung population ratio. Modelers of city-size hierarchies under Recognition Science would cite it to embed the phi-ladder into Zipf-law predictions. The definition is a direct record construction that invokes the cardinality theorem for urban levels and the ratio theorem for rung populations.
Claim. The urbanization certificate is the structure whose five-level field satisfies $|U| = 5$ for the type $U$ of urban tiers and whose ratio field satisfies $P(k+1)/P(k) = phi$ for all natural numbers $k$, where $P$ denotes population at rung $k$.
background
The module models city-size distributions on the phi-ladder, with adjacent tiers differing by the golden ratio. The referenced UrbanizationCert structure requires exactly two fields: the cardinality of UrbanLevel equals 5 (hamlet to metropolis) and the population ratio between consecutive rungs equals phi. This rests on the upstream phi_ratio definition from the quasicrystal module, which sets the constant to $1/phi$, and on the populationRatio theorem that unfolds populationAtRung and reduces the ratio algebraically to phi.
proof idea
The definition is a one-line record construction that supplies the five_levels field from the urbanLevelCount theorem and the phi_ratio field from the populationRatio theorem.
why it matters
This definition completes the UrbanizationCert structure that encodes the five-level urban hierarchy predicted by the phi-ladder in Recognition Science. It supplies the concrete witness required for the sociology tier, where the five levels match configDim D = 5 and the ratio property follows from the self-similar fixed point. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.