zipfSize_one
plain-language theorem explainer
Rank-1 city size equals 1 by definition of the Zipf function in this model. Researchers working on derivations of Zipf's law from σ-conservation in urban systems cite this as the base case for the rank-size relation. The proof is a direct unfolding of the size definition combined with arithmetic simplification.
Claim. The population at rank 1 satisfies $S(1) = 1$, where $S(r) = 1/r$ for natural numbers $r ≥ 1$.
background
The module derives Zipf's law for city sizes from σ-conservation on the inter-city flow graph. A city's σ-charge equals its population fraction and total σ is conserved across the rank distribution. The cost functional C(S) = Σ J(S(r)/S(1)) is minimized subject to Σ S(r) = N_total, yielding the unique extremiser S(r) = S(1)/r with exponent 1.
proof idea
The proof unfolds the definition of zipfSize, which gives 1/1 = 1 for r = 1, and applies simplification to confirm the equality.
why it matters
This result supplies the rank-one size property to zipfFromCitySigmaCert, which collects the full certification of the Zipf distribution under σ-conservation. It fills the base case in the derivation of Zipf's law with exponent approximately 1 from the Recognition Science framework, specifically the σ-conservation and J-cost minimization in the urban track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.