zipfSize_pos
plain-language theorem explainer
Rank-r city size is strictly positive for every natural number r at least 1. Researchers building σ-conservation models of urban hierarchies cite this to guarantee that partial sums over city populations remain positive. The short tactic proof unfolds the piecewise definition of zipfSize, excludes the r=0 case with omega, and applies positivity to the reciprocal.
Claim. For every natural number $r$ with $r ≥ 1$, the rank-$r$ population size $S(r) = 1/r$ satisfies $S(r) > 0$.
background
The module derives Zipf's law for city sizes 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))$, and the unique minimizer under fixed total population is the Zipf distribution $S(r) = S(1)/r$ with exponent 1. zipfSize is the explicit truncated form: for $r > 0$ it returns $1/r$ (with rank-1 normalized to size 1). The upstream rank definitions supply ordering by J-cost or forcing stage, which the urban model re-uses to index cities.
proof idea
The tactic proof unfolds zipfSize, obtains $r ≠ 0$ via omega, rewrites away the zero branch, and closes with the positivity tactic on the resulting positive reciprocal.
why it matters
This result supplies the size_pos field inside the ZipfFromCitySigmaCert certificate and is invoked by totalPop_pos to keep the population sum strictly positive. It anchors the basic well-definedness step in the module's derivation of Zipf's law with exponent 1 from σ-conservation (track F10). Within the Recognition framework it ensures the discrete distribution used for J-cost minimization and pairwise conservation checks remains non-negative before summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.