populationRatio
plain-language theorem explainer
populationRatio establishes that the population at rung k+1 on the phi-ladder is exactly phi times the population at rung k. Urban modelers working with Recognition Science predictions for city-size hierarchies cite this scaling to anchor Zipf-law exponents in the self-similar fixed point. The term proof unfolds the explicit population formula, clears the denominator via positivity, and reduces the ratio by power arithmetic plus ring normalization.
Claim. Let $p(k) = 100 phi^k$ denote the population at rung $k$. Then for every natural number $k$, $p(k+1)/p(k) = phi$.
background
The module UrbanizationFromPhiLadder treats city-size tiers as rungs on the phi-ladder. The upstream definition populationAtRung k := 100 * phi ^ k supplies the explicit formula. Module documentation states that city sizes obey Zipf's law and that Recognition Science predicts adjacent tiers scale by a factor tied to phi, with five canonical levels (hamlet to metropolis) matching configDim D = 5.
proof idea
The term proof unfolds populationAtRung to expose 100 * phi ^ k. It introduces a positivity hypothesis via mul_pos and pow_pos, rewrites the successor exponent with pow_succ and clears the division with div_eq_iff, then closes by ring.
why it matters
This result supplies the phi_ratio field inside the urbanizationCert definition that certifies the five-level urban hierarchy. It directly instantiates the phi-ladder scaling required by the Recognition Science framework, where phi is the self-similar fixed point forced at T6. The module records zero sorrys and zero axioms for the entire urbanization construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.