ReligiousExperienceType

formal source

  26namespace IndisputableMonolith.Philosophy.ReligiousExperienceFromJCost
  27open Cost
  28
  29inductive ReligiousExperienceType where
  30  | mystical | numinous | conversion | prayer | deathAwareness
  31  deriving DecidableEq, Repr, BEq, Fintype
  32
  33theorem religiousExperienceCount : Fintype.card ReligiousExperienceType = 5 := by decide
  34
  35/-- Four marks = configDim D - 1. -/
  36def fourMarks : ℕ := 4
  37theorem fourMarks_eq : fourMarks = 5 - 1 := by decide
  38
  39/-- Noetic quality = J = 0. -/
  40theorem noetic_quality_eq_equilibrium : Jcost 1 = 0 := Jcost_unit0
  41
  42/-- Transiency = J = 0 is unstable. -/
  43theorem transiency_instability {ε : ℝ} (hε : 0 < ε) :
  44    Jcost (1 + ε) > 0 := by
  45  apply Jcost_pos_of_ne_one
  46  · linarith
  47  · linarith
  48
  49structure ReligiousExperienceCert where
  50  five_types : Fintype.card ReligiousExperienceType = 5
  51  four_marks : fourMarks = 5 - 1
  52  noetic_quality : Jcost 1 = 0
  53  transiency : ∀ {ε : ℝ}, 0 < ε → Jcost (1 + ε) > 0
  54
  55def religiousExperienceCert : ReligiousExperienceCert where
  56  five_types := religiousExperienceCount
  57  four_marks := fourMarks_eq
  58  noetic_quality := noetic_quality_eq_equilibrium
  59  transiency := transiency_instability