ReligiousExperienceCert
plain-language theorem explainer
ReligiousExperienceCert packages four conditions that certify a religious experience inside the J-cost model: exactly five enumerated types, four marks equal to dimension minus one, zero cost at the unit equilibrium, and strictly positive cost under any positive perturbation. A researcher formalizing subjective experience within Recognition Science would cite this structure to link William James' marks to the cost function. The declaration is a bare structure definition with no proof body or tactics.
Claim. A structure is defined by the conjunction of: the set of religious experience types has cardinality 5; the number of marks equals $5-1$; the J-cost function satisfies $J(1)=0$; and $J(1+ε)>0$ for every real $ε>0$.
background
The module formalizes William James' four marks of religious experience using the J-cost function imported from the Cost module. J-cost vanishes at the recognition equilibrium point 1 and rises under any deviation, supplying the noetic quality and transiency marks. The inductive type ReligiousExperienceType enumerates five constructors (mystical, numinous, conversion, prayer, deathAwareness) whose cardinality supplies the fifth mark count. The constant fourMarks is defined directly as 4, matching configDim D minus one.
proof idea
The declaration is a structure definition containing four fields. Each field is a direct equation or quantified statement that references the sibling definitions ReligiousExperienceType and fourMarks; no lemmas or tactics are applied.
why it matters
The structure supplies the type for the downstream definition religiousExperienceCert, which populates the fields from the module's equality lemmas. It encodes the RS derivation of James' marks from J-cost equilibrium and instability, tying the five-type count to configDim D and the four-mark count to D minus one. The construction remains open to further embedding into the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.