zipf_one_statement
plain-language theorem explainer
The theorem packages three results: the rank-size product r · S(r) equals 1 for every rank r ≥ 1, pairwise sigma-flows between ranks vanish, and the size function is exactly S(r) = 1/r. Urban modelers deriving city-size distributions from conservation principles would cite this as the explicit statement of Zipf's law with exponent 1. The proof is a one-line term that directly assembles the three upstream lemmas rank_size_product, sigma_conservation_pairwise, and zipf_exponent_one.
Claim. Let $S(r)$ denote the relative population at rank $r$ with $S(1) = 1$. Then for every natural number $r ≥ 1$, $r · S(r) = 1$; for every pair of ranks $r, s ≥ 1$, the sigma-flow $r · S(r) - s · S(s)$ equals zero; and $S(r) = 1/r$.
background
The module derives Zipf's law from σ-conservation on an inter-city flow graph. A city's σ-charge equals its population fraction; total σ is conserved. The cost functional is $C(S) = Σ J(S(r)/S(1))$ minimized subject to Σ S(r) = N_total. The unique extremiser is the Zipf distribution $S(r) ∝ 1/r$ with exponent exactly 1. zipfSize r is defined as 1/r for r > 0 (and 0 otherwise). sigmaFlow r s is the difference r · zipfSize r - s · zipfSize s. rank_size_product states that the product is invariant at 1. sigma_conservation_pairwise states that the flow vanishes identically. zipf_exponent_one rewrites the product law as the explicit power form with exponent 1.
proof idea
The proof is a term-mode construction of the conjunction. It directly references the three upstream theorems: rank_size_product supplies the invariant product, sigma_conservation_pairwise supplies the vanishing flows (via ring simplification after substitution), and zipf_exponent_one supplies the explicit 1/r form (via unfolding and simp). No additional tactics or reductions are performed.
why it matters
This declaration is the terminal packaging of the Zipf derivation in the Urban module (Track F10). It supplies the explicit statement that the structural σ-conservation forces the rank-size product to be invariant and therefore yields Zipf's law with exponent 1. The module doc notes the falsifier: observed city-size distributions whose best-fit exponent lies outside [0.85, 1.15]. No downstream results are recorded, indicating this is the final claim of the local development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.