noetic_quality_eq_equilibrium
plain-language theorem explainer
Noetic quality in religious experience is identified with the equilibrium condition Jcost 1 = 0. Researchers formalizing William James' four marks inside Recognition Science would cite this result. The proof is a direct term-mode application of the Jcost unit lemma from the Cost module.
Claim. The noetic quality of religious experience is identified with the equilibrium condition $J(1) = 0$, where the J-cost function satisfies $J(x) = (x-1)^2/(2x)$.
background
The module derives William James' four marks of religious experience from the J-cost framework. Noetic quality is defined as recognition equilibrium at J-cost zero. The J-cost is introduced in the Cost module as the squared ratio $J(x) = (x-1)^2/(2x)$, which is equivalent to the hyperbolic form from the forcing chain. This theorem sits inside the local setting that equates the four marks to configDim D - 1 = 4 and the five experience types to D = 5.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_unit0. That lemma itself reduces the claim by simp on the definition of Jcost at argument 1.
why it matters
This result supplies the noetic_quality field inside the religiousExperienceCert definition, which bundles five_types, four_marks, noetic_quality, and transiency into a single certificate. It realizes the explicit RS step that sets noetic quality equal to J-cost zero, closing the philosophy module with zero sorry and linking directly to J-uniqueness in the T5 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.