IndisputableMonolith.Sociology.UrbanizationFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Urbanization Rate from Phi-Ladder — Tier F Urban Studies
   6
   7City size distributions follow Zipf's law: rank × population = constant.
   8In RS terms, adjacent city-size tiers differ in population by phi^2 ≈ 2.618
   9(the Gibrat-Zipf exponent is close to phi²/phi = phi ≈ 1.618 in log space).
  10
  11RS prediction: the urban hierarchy follows the phi-ladder with populations
  12at adjacent ranks ratio by phi^(-1) ≈ 0.618 (each higher rank is 1/phi
  13as populated as the next lower).
  14
  15Five canonical urbanization levels (hamlet, village, town, city, metropolis)
  16= configDim D = 5.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith.Sociology.UrbanizationFromPhiLadder
  22open Constants
  23
  24inductive UrbanLevel where
  25  | hamlet | village | town | city | metropolis
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem urbanLevelCount : Fintype.card UrbanLevel = 5 := by decide
  29
  30noncomputable def populationAtRung (k : ℕ) : ℝ := 100 * phi ^ k
  31
  32theorem populationRatio (k : ℕ) :
  33    populationAtRung (k + 1) / populationAtRung k = phi := by
  34  unfold populationAtRung
  35  have hpos : 0 < 100 * phi ^ k := mul_pos (by norm_num) (pow_pos phi_pos _)
  36  rw [pow_succ, div_eq_iff hpos.ne']
  37  ring
  38
  39structure UrbanizationCert where
  40  five_levels : Fintype.card UrbanLevel = 5
  41  phi_ratio : ∀ k, populationAtRung (k + 1) / populationAtRung k = phi
  42
  43noncomputable def urbanizationCert : UrbanizationCert where
  44  five_levels := urbanLevelCount
  45  phi_ratio := populationRatio
  46
  47end IndisputableMonolith.Sociology.UrbanizationFromPhiLadder
  48