JCostComparative
plain-language theorem explainer
JCostComparative encodes the J-cost as a function on ledger states L that vanishes on equal states, is non-negative, symmetric, and obeys the triangle inequality. Researchers deriving emergent geometry from recognition processes would reference this when equipping configuration spaces with distance-like structures. The declaration is a pure structural definition requiring no computational steps or lemmas.
Claim. Let $L$ be a type equipped with an RS configuration space structure. A J-cost comparative structure on $L$ consists of a map $J : L → L → ℝ$ satisfying $J(ℓ,ℓ)=0$ for all $ℓ$, $J(ℓ₁,ℓ₂) ≥ 0$ for all $ℓ₁,ℓ₂$, $J(ℓ₁,ℓ₂)=J(ℓ₂,ℓ₁)$, and the triangle inequality $J(ℓ₁,ℓ₃) ≤ J(ℓ₁,ℓ₂) + J(ℓ₂,ℓ₃)$ for all $ℓ₁,ℓ₂,ℓ₃$.
background
In the Recognition Geometry bridge module, ledger states from Recognition Science are modeled as elements of a configuration space via the RSConfigSpace class, which requires the space to be nonempty and to have decidable equality. The J-cost function measures the information cost of transitioning between such states, providing the metric structure needed for Recognition Geometry. Upstream, cost functions are defined in MultiplicativeRecognizerL4 and ObserverForcing as derived costs from comparators and recognition events, respectively, while the Triangle structure from ReggeCalculus supplies the geometric intuition for the inequality.
proof idea
This is a structural definition with an empty proof body. It directly encodes the four metric axioms as fields of the structure: self_zero, nonneg, symm, and triangle. No lemmas are applied; the declaration serves as the interface that downstream functions such as toRecognitionDistance consume by projecting the fields into a RecognitionDistance instance.
why it matters
JCostComparative supplies the metric-like structure that allows Recognition Science to instantiate Recognition Geometry's distance axioms. It is used by toRecognitionDistance to construct an explicit RecognitionDistance from the J function, and appears in rsbridge_status to confirm that RS satisfies the geometric requirements. This fills the step where metrics emerge from comparative recognition in the bridge between the 8-tick cycle and spatial dimensions, directly supporting the claim that physical space is the recognition quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.