modalDistance
plain-language theorem explainer
Modal distance is defined as the defect functional J(x) on the reals, serving as the measure of deviation from the actual world in the modal ontology of Recognition Science. Researchers formalizing modal logic via J-cost minimization would cite this definition when establishing properties of necessity and possibility. It is implemented as a direct alias to the defect function imported from LawOfExistence.
Claim. The modal distance of a configuration $x$ is defined by $modalDistance(x) := J(x)$, where $J$ is the defect functional.
background
The module develops the Recognition Science treatment of modal concepts under PH-013. Modal logic is grounded in J-cost: necessity is the unique minimizer of J at x=1, possibility requires positive ratio, actuality is the J-minimum, and accessibility follows cost-decreasing paths to the minimum.
proof idea
One-line wrapper that applies the defect functional from LawOfExistence.
why it matters
This definition supplies the distance measure for the PH-013 modal certificate. It feeds actual_has_zero_modal_distance (showing zero distance at x=1), modal_distance_nonneg (non-negativity under RSPossible), modal_distance_zero_iff_actual (zero distance iff actual), and ph013_modal_certificate (full resolution of necessity, possibility, and actuality). It anchors the J-cost grounding of modal metaphysics and links to the forcing chain via the unique minimizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.