fourMarks_eq
plain-language theorem explainer
Researchers formalizing William James's marks of religious experience within Recognition Science cite this result to equate the four marks with the configuration dimension minus one. It appears in the derivation of a certificate for religious experience types from J-cost equilibrium. The proof is a direct decision procedure confirming the numerical equality 4 = 5 - 1 from the prior definition of fourMarks.
Claim. The number of marks of religious experience equals the configuration dimension minus one: $4 = 5 - 1$.
background
In the module on Religious Experience from J-Cost, William James's four marks are formalized as ineffability, noetic quality, transiency, and passivity. Noetic quality is tied to J-cost zero at equilibrium, transiency to the instability of J = 0, and passivity to minimized cost. The upstream definition states that fourMarks equals 4 and equals configDim D minus 1, with D set to 5 to yield five experience types.
proof idea
This is a one-line wrapper that invokes the decide tactic to establish the equality between the defined value 4 and 5 minus 1.
why it matters
The result is referenced in religiousExperienceCert to supply the four_marks field alongside five_types from religiousExperienceCount, noetic_quality from equilibrium, and transiency from instability. It completes the formal link in the RS derivation where the four marks equal configDim D - 1, with D = 5 matching the five canonical types (mystical, numinous, conversion, prayer, death-awareness). This step anchors the philosophical formalization to the framework's dimensional counting without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.