modal_distance_zero_iff_actual
plain-language theorem explainer
Modal distance vanishes exactly when a possible configuration coincides with the actual world at unity. Researchers in modal metaphysics within Recognition Science would cite the equivalence to tie J-cost minimization to actuality. The proof splits the biconditional via constructor and substitutes the definitions of distance as defect together with actuality as the necessary configuration.
Claim. For any real number $x > 0$, the modal distance $d(x)$ satisfies $d(x) = 0$ if and only if $x = 1$, where $d(x)$ denotes the defect of $x$ and actuality is identified with the unique J-minimizer.
background
In the Recognition Science treatment of modal logic, possibility requires positive ratio so that $x > 0$ guarantees finite J-cost. Actuality is defined as necessity, which holds uniquely at the J-minimizer $x = 1$. Modal distance is introduced as the defect function measuring deviation from this minimum. The theorem belongs to the PH-013 module that resolves modal metaphysics by grounding necessity, possibility, and actuality in cost minimization. Upstream, the definition of modalDistance as defect x supplies the metric, while the sibling definitions of RSPossible and RSActual translate the hypotheses directly into $x > 0$ and $x = 1$.
proof idea
The proof applies the constructor tactic to split the biconditional into two implications. The forward direction combines the zero-distance assumption with the possibility hypothesis to witness actuality. The reverse direction projects the zero component from the actuality pair to recover that the distance is zero.
why it matters
This equivalence closes the identification of zero modal distance with actuality inside the modal ontology structure, confirming that cost minimization selects the actual world. It supports the RS modal resolution by linking the unique J-minimizer to the actual configuration. No downstream uses are recorded, yet the result underpins sibling claims such as actuality_is_j_minimum and actuality_is_unique. It touches the framework point that only the identity configuration achieves defect zero and is therefore both necessary and actual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.