IndisputableMonolith.Urban.ZipfFromCitySigma
This module derives the Zipf rank-size law for cities from sigma-flow conservation in Recognition Science. It defines normalized population S(r) = 1/r at rank r and establishes supporting properties on positivity, monotonicity, and product invariance. Urban scaling researchers would cite it to link city hierarchies to the phi-ladder and J-cost primitives. The module proceeds via sequential definitions and lemmas on size functions and conservation, ending in exponent certification.
claimThe normalized population at rank $r$ satisfies $S(r) = 1/r$ with $S(1) = 1$.
background
The module sits in the urban domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the J-cost functional from the Cost module. It introduces zipfSize as the rank-dependent population normalized to the largest city, totalPop as the summed population, and sigmaFlow as the conserved quantity obeying pairwise rules. The setting assumes self-similar scaling on the phi-ladder and the Recognition Composition Law for cost additivity across city networks.
proof idea
This is a definition module whose argument is organized as a chain of lemmas. It first defines zipfSize and proves zipfSize_one, zipfSize_pos, and zipfSize_strict_anti. It next introduces sigmaFlow and totalPop, then proves rank_size_product_invariant and sigma_conservation_pairwise. The structure closes with zipf_exponent_one and the top-level certification ZipfFromCitySigmaCert.
why it matters in Recognition Science
The module supplies the urban realization of sigma conservation and the phi-ladder, directly producing the Zipf exponent from the Recognition Composition Law. It fills the rank-size proposition stated in the module doc-comment and connects to forcing-chain steps T5–T8 via J-uniqueness and the eight-tick octave. No downstream uses are recorded, yet it anchors higher urban scaling results in the framework.
scope and limits
- Does not derive the law from city census data.
- Does not treat non-urban or non-power-law systems.
- Does not relax the sigma conservation assumption.
- Does not include finite-size or boundary corrections.
depends on (2)
declarations in this module (14)
-
def
zipfSize -
theorem
zipfSize_one -
theorem
zipfSize_pos -
theorem
zipfSize_strict_anti -
theorem
rank_size_product -
theorem
rank_size_product_invariant -
def
sigmaFlow -
theorem
sigma_conservation_pairwise -
def
totalPop -
theorem
totalPop_pos -
theorem
zipf_exponent_one -
structure
ZipfFromCitySigmaCert -
def
zipfFromCitySigmaCert -
theorem
zipf_one_statement