toRecognitionDistance
plain-language theorem explainer
The definition constructs a recognition distance on ledger configuration spaces by mapping the J-cost function and its metric properties directly to the RecognitionDistance structure. Researchers deriving physical metrics from Recognition Science would cite this when instantiating comparative recognition axioms. It is a direct structure definition that assigns the J field and delegates the four axioms to the corresponding JCostComparative proofs.
Claim. Let $L$ be a ledger space satisfying the RS configuration space axioms. Given a J-cost comparative recognizer $j$ on $L$, define the recognition distance $d$ by $d(x,y) := j.J(x,y)$, which satisfies non-negativity, $d(x,x)=0$, symmetry, and the triangle inequality by inheritance from the corresponding properties of $j$.
background
The RSBridge module shows how Recognition Science supplies concrete models for Recognition Geometry axioms. Ledger states form configuration spaces via the RSConfigSpace class, which asserts nonemptiness and decidable equality. The JCostComparative structure supplies a function J : L → L → ℝ together with proofs of non-negativity, self-zero distance, symmetry, and the triangle inequality; this J measures information cost of transitions between ledger states and serves as the comparative recognizer for RG7.
proof idea
One-line structure definition that sets the dist field to j.J and supplies the four metric axioms by direct projection from the nonneg, self_zero, symm, and triangle fields of the input JCostComparative.
why it matters
This supplies the metric for the comparative recognizer (RG7) in the RS instantiation of Recognition Geometry. It is referenced by the module status summary rsbridge_status, which records the mapping of RS structures to RG axioms. In the framework it connects the J-cost (from T5 uniqueness in the forcing chain) to metric emergence on recognition quotients, supporting the claim that physical space arises as a quotient under recognition equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.