theorem
proved
fourMarks_eq
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Philosophy.ReligiousExperienceFromJCost on GitHub at line 37.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
60
61end IndisputableMonolith.Philosophy.ReligiousExperienceFromJCost