fourMarks
plain-language theorem explainer
This definition assigns the constant four to the number of marks of religious experience, matching the configuration dimension minus one when that dimension equals five. Philosophers of religion or RS modelers cite it to link William James' empirical criteria to the formal J-cost framework. The assignment is a direct constant declaration with no further computation or lemmas.
Claim. The number of marks of religious experience equals four, which satisfies four equals the configuration dimension minus one.
background
The module formalizes William James' four marks of religious experience using J-cost from the Cost import. Noetic quality corresponds to J-cost zero at recognition equilibrium. Transiency follows because the zero-cost state is unstable under any positive perturbation. Passivity holds because the minimum cost is attained without active choice. The module sets five canonical experience types equal to the configuration dimension and four marks equal to that dimension minus one.
proof idea
This is a direct definition that assigns the natural number four. No lemmas are applied and no tactics are used.
why it matters
The definition supplies the numerical value referenced by the equality theorem that sets it to five minus one and by the ReligiousExperienceCert structure that also encodes five types, J-cost zero for noetic quality, and instability for transiency. It completes the RS mapping of James' marks onto the configuration dimension of five, consistent with the module's derivation that J-cost zero yields noetic quality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.