modal_distance_self
plain-language theorem explainer
The lemma establishes that modal distance vanishes when a configuration is compared to itself. Modal geometers working in Recognition Science cite it to anchor the zero-distance axiom of the possibility metric. The proof is a one-line term reduction that unfolds the distance definition and applies the self-transition property of the J-function.
Claim. Let $d$ be the modal distance on configurations, defined by $d(c_1,c_2)=J_transition(c_1,c_2)/τ_0$. Then $d(c,c)=0$ for every configuration $c$.
background
Modal distance is introduced in the ModalGeometry module as the function $d(c_1,c_2)=J_transition(c_1.value,c_2.value,c_1.pos,c_2.pos)$, which quantifies separation between possibility states. The underlying J-transition satisfies the Recognition Composition Law and reduces to zero on identical inputs. The lemma sits inside the modal geometry development that treats configurations as points in a space equipped with this distance, building directly on the Possibility module's self-transition result.
proof idea
The term proof unfolds the definition of modal_distance and invokes the J_transition_self lemma on the position field of the given configuration.
why it matters
The result supplies the identity axiom required for modal distance to function as a metric on possibility space. It closes the diagonal case for the metric properties developed in the same module and aligns with the self-similar fixed-point structure (T6) in the forcing chain. No downstream theorems yet depend on it, but it is a prerequisite for non-negativity, symmetry, and curvature statements in modal geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.