modal_distance_symm
plain-language theorem explainer
Modal distance between two configurations is symmetric. Researchers building topology on possibility spaces in Recognition Science cite this to confirm the distance satisfies metric axioms. The proof is a term-mode one-liner that unfolds the distance definition and applies the symmetry of the J-transition on configuration positions.
Claim. Let $d$ be the modal distance on configurations. For any configurations $c_1$ and $c_2$, $d(c_1,c_2)=d(c_2,c_1)$.
background
In the Modal Geometry module, configurations carry position data drawn from the possibility space. Modal distance is built from the J-cost function $J(x)=(x+x^{-1})/2-1$, which obeys the Recognition Composition Law and is strictly convex with unique minimum at $x=1$. Upstream structures establish J-cost minimization, ledger factorization over positive reals, and the discrete phi-tier organization of physical quantities. The lemma appears immediately after the distance definition and before the possibility-ball construction, supplying the symmetry needed for a metric topology.
proof idea
The proof is a one-line term wrapper. It unfolds the modal distance definition to expose the J-transition expression, then applies the exact symmetry lemma for that transition on the position components of the two configurations.
why it matters
The result supplies the symmetry axiom required for modal distance to serve as a metric on the possibility space. It directly enables the subsequent definitions of possibility balls, identity-in-ball, and connected components listed among sibling declarations. Within the Recognition framework it aligns with the J-uniqueness step (T5) and the eight-tick octave (T7) by ensuring the distance respects the underlying phi-ladder structure. No open questions are addressed; the lemma closes a basic property needed for the topology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.