def
definition
tierThreshold
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Archaeology.CivilizationComplexityFromZRung on GitHub at line 35.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
32
33theorem tierCount : Fintype.card ComplexityTier = 5 := by decide
34
35noncomputable def tierThreshold (k : ℕ) : ℝ := 100 * phi ^ (2 * k)
36
37theorem tierThreshold_pos (k : ℕ) : 0 < tierThreshold k :=
38 mul_pos (by norm_num) (pow_pos phi_pos _)
39
40theorem tierThreshold_ratio (k : ℕ) :
41 tierThreshold (k + 1) / tierThreshold k = phi ^ 2 := by
42 unfold tierThreshold
43 have hpos : 0 < 100 * phi ^ (2 * k) := mul_pos (by norm_num) (pow_pos phi_pos _)
44 rw [div_eq_iff hpos.ne']
45 ring
46
47structure CivilizationCert where
48 five_tiers : Fintype.card ComplexityTier = 5
49 threshold_pos : ∀ k, 0 < tierThreshold k
50 phi_sq_ratio : ∀ k, tierThreshold (k + 1) / tierThreshold k = phi ^ 2
51
52noncomputable def civilizationCert : CivilizationCert where
53 five_tiers := tierCount
54 threshold_pos := tierThreshold_pos
55 phi_sq_ratio := tierThreshold_ratio
56
57end IndisputableMonolith.Archaeology.CivilizationComplexityFromZRung