modal_distance
The modal distance definition equips pairs of configurations with a real-valued measure given by the J-transition cost on their value and position fields. Researchers constructing the geometry of possibility spaces cite it when defining the metric on modal manifolds. The definition is a direct one-line delegation to the imported J_transition function.
claimThe modal distance between configurations $c_1$ and $c_2$ is $d(c_1,c_2)=J_*(c_1.v,c_2.v,c_1.p,c_2.p)$, where $J_*$ denotes the J-cost evaluated at the transition state between the two configurations.
background
Configurations are records carrying a real value and a position index; they label points in the possibility space. The J-transition function computes the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently cosh(log x)-1) between a pair of such points, drawing on the Recognition Composition Law. The ModalGeometry module imports this function together with the Config structure from the Possibility module to equip the space with a metric.
proof idea
One-line definition that applies J_transition directly to the value and position fields of the two input configurations.
why it matters in Recognition Science
The definition supplies the metric used by ModalManifold, PossibilityBall, and the lemmas modal_distance_nonneg, modal_distance_self, modal_distance_symm, identity_in_ball, and constructive_at_zero. It realizes the possibility metric required by the modal geometry construction, linking to J-uniqueness (T5) and the forcing chain. Downstream results rely on it to establish non-negativity, symmetry, and ball membership.
scope and limits
- Does not divide by any time-scale factor τ₀.
- Does not establish the triangle inequality.
- Does not extend to higher-dimensional configuration spaces.
- Does not incorporate curvature or connection data.
formal statement (Lean)
51noncomputable def modal_distance (c1 c2 : Config) : ℝ :=
proof body
Definition body.
52 J_transition c1.value c2.value c1.pos c2.pos
53
54/-- Modal distance is non-negative. -/