  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.