def
definition
settlementLevelCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Archaeology.UrbanDensityFromPhiLadder on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
29noncomputable section
30
31/-- Five canonical settlement levels (forced by configDim = 5). -/
32def settlementLevelCount : ℕ := 5
33
34theorem settlementLevelCount_eq : settlementLevelCount = 5 := rfl
35
36/-- φ-rung spacing between adjacent settlement levels. -/
37def settlementRungSpacing : ℕ := 3
38
39/-- Population ratio between adjacent settlement levels: φ³ ≈ 4.236. -/
40noncomputable def settlementPopRatio : ℝ := phi ^ settlementRungSpacing
41
42theorem settlementPopRatio_pos : 0 < settlementPopRatio := by
43 unfold settlementPopRatio; exact pow_pos phi_pos _
44
45theorem settlementPopRatio_in_Christaller_band :
46 (3 : ℝ) < settlementPopRatio ∧ settlementPopRatio < 8 := by
47 constructor
48 · unfold settlementPopRatio settlementRungSpacing
49 have hlo : (1.6 : ℝ) < phi := one_lt_phiPointSixOne
50 have : (1.6 : ℝ) ^ 3 < phi ^ 3 := by
51 have h1 : (1.6 : ℝ) ^ 3 = 4.096 := by norm_num
52 have h2 : phi ^ 3 > 4.096 := by nlinarith [phi_gt_onePointSixOne, phi_sq_eq, phi_pos]
53 linarith
54 linarith
55 · unfold settlementPopRatio settlementRungSpacing
56 have hhi : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
57 have : phi ^ 3 < 5 := by nlinarith [phi_lt_onePointSixTwo, phi_sq_eq, phi_pos]
58 linarith
59
60/-- J-cost on the settlement size ratio. -/
61def settlementCost (actual_pop expected_pop : ℝ) : ℝ :=
62 Jcost (actual_pop / expected_pop)