rank_size_product_invariant
plain-language theorem explainer
The theorem establishes invariance of the rank-size product for any two ranks r and s at least 1 in the truncated Zipf distribution. Urban modelers deriving city-size laws from σ-conservation would cite this as a structural corollary. The proof is a one-line wrapper that applies the rank-size product lemma to both sides and equates the constants.
Claim. For natural numbers $r, s$ with $r, s$ at least 1, $r$ times the population at rank $r$ equals $s$ times the population at rank $s$, where the population function is the Zipf size $S(r) = 1/r$.
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; the unique distribution maximising J-cost-symmetric entropy under fixed total σ is the Zipf form $S(r) = 1/r$ with exponent 1. The zipfSize definition sets population at rank r to 1/r for r at least 1 (with rank-1 size normalised to 1). The upstream rank_size_product theorem proves that the product r times S(r) equals 1 for each r at least 1. This invariant is the key structural property used here. The local setting follows Track F10 of Plan v5, proving σ-conservation, monotonicity, and the rank-size product law for the truncated Zipf distribution.
proof idea
The proof is a one-line wrapper that rewrites both sides of the equality using the rank_size_product theorem applied to r and to s respectively.
why it matters
This result confirms the invariance property central to the Zipf derivation in the Recognition Science urban model. It supports the pairwise σ-flow balance statements in the same module and aligns with the structural argument that the extremiser of the cost functional C(S) equals sum J(S(r)/S(1)) under σ-conservation is the Zipf distribution. It touches the open question of how well real city distributions match the predicted exponent near 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.