cert
plain-language theorem explainer
Archaeologists and urban theorists modeling Zipf or Christaller scaling can cite this definition to obtain a machine-checked certificate that the phi-ladder forces exactly five settlement levels whose adjacent population ratios lie strictly between 3 and 8. The certificate is assembled from three prior lemmas that fix the level count by reflexivity, establish positivity of the ratio via power positivity, and place the ratio inside the Christaller interval by direct unfolding and comparison with phi. This supplies the concrete witness requiredby
Claim. Let $N$ be the number of levels in the settlement hierarchy and $r$ the population ratio between adjacent levels. The term cert is the explicit witness of type UrbanDensityCert satisfying $N=5$, $0<r$, and $3<r<8$.
background
The module derives settlement hierarchies from the phi-ladder, with rung spacing set by phi so that population ratios become powers of phi. The structure UrbanDensityCert packages three required properties: the level count equals 5 (forced by configDim D=5), the ratio is positive, and the ratio lies in (3,8) to match Christaller's empirical range. Upstream, settlementLevelCount_eq states settlementLevelCount=5 by rfl and carries the comment 'phi-rung spacing between adjacent settlement levels.' settlementPopRatio_pos proves 0<settlementPopRatio by pow_pos phi_pos, while settlementPopRatio_in_Christaller_band proves the interval bounds by unfolding and comparison with phi^3.
proof idea
The definition constructs the certificate by direct record assembly, assigning the three fields of UrbanDensityCert from the lemmas settlementLevelCount_eq, settlementPopRatio_pos, and settlementPopRatio_in_Christaller_band. No tactics or reductions are performed beyond the field projections.
why it matters
This definition supplies the concrete witness that closes the structural theorem for urban density scaling inside the Recognition Science framework. It links the phi-ladder (T6 self-similar fixed point) to the five-level hierarchy required by configDim D=5 and places the ratio inside the Christaller band, fulfilling the module's claim of a zero-sorry structural theorem. No downstream uses are recorded, leaving open its later incorporation into cross-domain meta-counts such as count_eq.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.