sigmaFlow
plain-language theorem explainer
The definition introduces σ-flow between city ranks r and s as the signed difference r·S(r) − s·S(s), where S is the population size at each rank. Urban scaling researchers deriving Zipf distributions from conservation laws would cite this quantity as the basic inter-city flow term. It is supplied by a direct algebraic abbreviation that subtracts the two weighted sizes.
Claim. The σ-flow between ranks $r$ and $s$ is defined by $r·S(r) - s·S(s)$, where $S$ denotes the city population size function obeying the rank-size product law $r·S(r)=1$ for $r≥1$.
background
In the Recognition Science model of urban systems, each city's σ-charge is identified with its fractional population. Total σ is conserved across the rank distribution, and the unique distribution that extremizes the J-cost functional $C(S)=Σ J(S(r)/S(1))$ under this constraint is the Zipf form $S(r)∝1/r$. The module works with an explicit truncated Zipf distribution and proves its conservation, monotonicity, and rank-size product properties. Upstream results supply the numerical rank function from the pre-temporal forcing order and structural guarantees that the underlying cost and ledger constructions remain collision-free.
proof idea
This is a direct definition that sets sigmaFlow r s equal to the difference of the two scaled sizes. No lemmas are applied; the expression is written out once and left as the primitive flow quantity for later use.
why it matters
The definition supplies the flow term required by sigma_conservation_pairwise, which vanishes for all ranks ≥1 and thereby feeds the ZipfFromCitySigmaCert structure. That certificate records the rank-size product invariant, the positivity and strict decrease of sizes, and the pairwise conservation statement, establishing Zipf's law with exponent exactly 1. The construction realizes the σ-conservation step of track F10, linking the J-cost minimization under fixed total σ to the eight-tick octave and phi-ladder structures already present in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.