zipf_exponent_one
plain-language theorem explainer
zipf_exponent_one establishes that the population size at rank r equals exactly 1/r for every natural number r at least 1. Urban modelers deriving rank-size laws from conservation principles cite it to confirm the exponent is unity. The short tactic proof unfolds the size definition, rules out the zero case with omega, and simplifies the conditional expression.
Claim. For every natural number $r$ with $1leq r$, the relative city population $S(r)$ at rank $r$ satisfies $S(r)=1/r$.
background
The upstream definition zipfSize sets the relative population at rank r to 1/r for positive r (and 0 at r=0), with rank-1 city normalized to size 1. This explicit form is the candidate distribution obtained by minimizing the J-cost sum C(S) = sum J(S(r)/S(1)) subject to fixed total sigma across ranks. The module works in the setting of sigma-conservation on the inter-city flow graph, where each city's sigma-charge equals its population fraction and the unique extremizer is the Zipf form with exponent 1.
proof idea
The tactic proof unfolds zipfSize to expose the if-then-else, introduces r nonzero via omega, rewrites the conditional to the else branch with if_neg, and finishes with simp to obtain the target equality.
why it matters
The result is invoked inside zipfFromCitySigmaCert to build the master certificate and inside zipf_one_statement to package the rank-size product, sigma conservation, and exponent-one form. The module documentation presents it as the explicit verification step that the candidate distribution satisfies S(r) = 1/r^1, completing the structural derivation of Zipf's law from J-cost minimization under sigma conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.