sigma_conservation_pairwise
plain-language theorem explainer
The theorem shows that the pairwise sigma-flow between any two cities of ranks r and s (both at least 1) is identically zero. Urban theorists deriving Zipf's law from sigma-conservation on the rank graph would cite this invariance as the structural reason the 1/r distribution is selected. The proof is a short algebraic reduction that unfolds the flow definition, substitutes the rank-size product identity twice, and simplifies via ring arithmetic.
Claim. For natural numbers $r, s$ with $r, s$ at least 1, the sigma-flow between the corresponding cities vanishes: $sigma(r, s) = 0$.
background
In this module the sigma-charge of a city is its population fraction relative to the largest city. The sigma-flow sigmaFlow r s is the net transfer implied by the rank-size assignment between two cities; the model requires total sigma to be conserved across the truncated distribution. The cost functional is defined as the sum of J-cost terms C(S) = sum J(S(r)/S(1)), and the Zipf distribution extremizes this under the conservation constraint. Upstream structures supply the J-cost definition from PhiForcingDerived and the ledger factorization from DAlembert that calibrate the underlying multiplicative group.
proof idea
The proof unfolds the definition of sigmaFlow. It rewrites the expression using the rank_size_product theorem applied separately to r (under 1 ≤ r) and to s (under 1 ≤ s). The ring tactic then reduces the resulting difference of products to zero.
why it matters
This supplies the sigma_conservation field inside the ZipfFromCitySigmaCert certificate and is packaged directly into the zipf_one_statement theorem that asserts the full rank-size product law together with exponent exactly 1. It realizes the sigma-conservation law on the city graph, the direct analogue of charge conservation in the Recognition framework, and closes the structural step that selects the Zipf distribution as the unique J-cost extremizer under fixed total sigma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.