zipfSize
plain-language theorem explainer
zipfSize defines the population S(r) at city rank r as 1/r for positive integers r and 0 for r=0. Urban scaling researchers and Recognition Science modelers cite it as the explicit base distribution for σ-conservation derivations of Zipf's law. The implementation is a direct conditional expression with natural-to-real coercion for the reciprocal term.
Claim. Define the population function $S : ℕ → ℝ$ by $S(r) = 0$ if $r = 0$ and $S(r) = 1/r$ otherwise, where $S(r)$ is the relative population at rank $r$ with $S(1) = 1$.
background
The module derives Zipf's law from σ-conservation on the inter-city flow graph, where a city's σ-charge equals its population fraction and total σ is conserved. The unique distribution maximising J-cost-symmetric entropy under fixed total σ is the Zipf form $S(r) ∝ 1/r$. The cost functional is $C(S) = Σ J(S(r)/S(1))$, minimised subject to $Σ S(r) = N_{total}$ (from MODULE_DOC). This definition supplies the explicit truncated form with exponent exactly 1. It draws on the J-cost functional from the imported Cost module and the general ranking conventions in the framework.
proof idea
The definition is a direct conditional expression. It returns 0 on the case r = 0 and otherwise returns the reciprocal after coercing the natural number r to a real. No lemmas from upstream results are invoked; the construction relies only on the built-in if-then-else and type embedding.
why it matters
This definition is the base for the rank-size product theorem proving $r · S(r) = 1$ and the σ-flow conservation result showing pairwise flows vanish. It realises the structural extremiser of the J-cost functional under σ-conservation, aligning with T5 J-uniqueness and the phi-ladder in the Recognition framework. It fills the explicit distribution step in Track F10 of Plan v5, with the open empirical question of city-size fits inside the [0.85, 1.15] exponent band (quoted from MODULE_DOC falsifier).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.