modal_distance
plain-language theorem explainer
Modal distance equips the space of configurations with a metric derived from transition-state J-costs. Researchers on modal manifolds cite it to induce the topology and balls on possibility space. The definition is a direct one-line reference to the four-argument J_transition function.
Claim. The modal distance between configurations $c_1$ and $c_2$ is $d(c_1,c_2) := J_{transition}(c_1.value, c_2.value, c_1.pos, c_2.pos)$, where $J_{transition}$ is the J-cost evaluated at the transition state between the given values and positions.
background
In ModalGeometry the points are elements of Config, the structure imported from Possibility that carries a value, a position, and a time index. J_transition, drawn from both ActivationEnergy and Possibility, returns the J-cost at the transition state; its one-argument form in Chemistry is $J(x^*)$, while the modal version accepts two values and two positions. The module sets the local setting for a two-dimensional manifold (value plus time) whose metric is this distance function.
proof idea
One-line wrapper that applies the J_transition function from the possibility module.
why it matters
The definition supplies the metric for ModalManifold, PossibilityBall, standard_modal_manifold and the supporting lemmas modal_distance_nonneg, modal_distance_self, modal_distance_symm, identity_in_ball, constructive_at_zero. It realizes the possibility metric described in the module doc-comment and connects to T5 J-uniqueness in the forcing chain. Downstream lemmas rely on it to establish non-negativity, symmetry and ball membership.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.