totalPop_pos
plain-language theorem explainer
The theorem establishes that the total population, defined as the sum of Zipf city sizes from rank 1 to N, is strictly positive for every natural number N at least 1. Urban modelers deriving Zipf distributions from sigma conservation would cite this to guarantee that population aggregates remain positive and well-defined. The proof unfolds the sum, verifies the first term is positive via the individual size positivity lemma, confirms non-negativity of the rest, and applies the finite-sum positivity criterion.
Claim. For any natural number $N$ with $N$ at least 1, the total population $P(N) = sum_{r=1}^N S(r) > 0$, where $S(r)$ denotes the population of the city of rank $r$ in the truncated Zipf distribution.
background
In the Recognition Science urban model, each city's sigma-charge equals its population fraction and total sigma is conserved across the rank distribution. The cost functional is $C(S) = sum J(S(r)/S(1))$, where J is the cost from the phi-forcing structure; the unique minimizer under fixed total sigma is the Zipf law $S(r) = S(1)/r$. The totalPop function aggregates these sizes up to finite rank N. This positivity result rests on the underlying positivity of individual city sizes, which trace to the J-uniqueness and phi-ladder constructions in the foundation modules.
proof idea
The proof unfolds the definition of totalPop as a Finset sum. It shows the zero index lies in the range via mem_range and omega, invokes positivity of the first zipfSize term, establishes non-negativity of all remaining terms by the same positivity lemma, and concludes via Finset.sum_pos' that the sum is positive.
why it matters
This result supplies the positivity component required by the ZipfFromCitySigmaCert structure, which collects rank-size product invariance, strict anti-monotonicity, and pairwise sigma conservation. It completes the structural derivation that the truncated Zipf distribution satisfies the conservation law while remaining positive, aligning with the module's claim that the distribution maximizes J-cost-symmetric entropy under fixed total sigma. The theorem sits inside the urban track (F10) and inherits the eight-tick octave and D=3 spatial setting from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.