totalPop
plain-language theorem explainer
The total population aggregates the Zipf sizes of the top N cities into their harmonic sum. Urban scaling researchers cite it when bounding aggregate population or verifying positivity under rank-size scaling. The definition is realized as a direct Finset summation over the per-rank zipfSize terms.
Claim. Let $H_N = sum_{r=1}^N 1/r$. Then totalPop(N) is defined to equal $H_N$, the sum of city populations for ranks 1 through N under the truncated Zipf law $S(r) = 1/r$.
background
The Urban.ZipfFromCitySigma module derives Zipf's law from σ-conservation on the inter-city flow graph. City populations obey the truncated Zipf law supplied by the upstream zipfSize definition: population at rank r equals 1/r (with S(1) normalized to 1). The module documentation states that the unique distribution maximizing J-cost-symmetric entropy under fixed total σ is the Zipf distribution S(r) ∝ 1/r. The total population is the finite sum of these sizes over the leading N cities, needed only to confirm positivity and finiteness.
proof idea
The definition is a one-line wrapper that applies the upstream zipfSize definition inside a Finset.range sum. No tactics or lemmas beyond the Finset summation primitive are required.
why it matters
This definition supplies the aggregate population quantity required by the downstream ZipfFromCitySigmaCert structure, which records the rank-size product law r · S(r) = 1 together with σ-conservation. It thereby supports the certification that the exponent equals exactly one, consistent with the Recognition framework's T6 self-similar fixed point and the Recognition Composition Law. The surrounding module derives the law from σ-conservation; the falsifier is any city-size distribution whose best-fit exponent lies outside [0.85, 1.15].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.