module module

`IndisputableMonolith.Philosophy.ReligiousExperienceFromJCost`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (8)

inductive ReligiousExperienceType L29
theorem religiousExperienceCount L33
def fourMarks L36
theorem fourMarks_eq L37
theorem noetic_quality_eq_equilibrium L40
theorem transiency_instability L43
structure ReligiousExperienceCert L49
def religiousExperienceCert L55